Merge pull request #5715 from NlightNFotis/dockerfile

Introduction of Dockerfile for building and running CBMC in a Docker container.

Author: NlightNFotis

.github/workflows/pull-request-checks.yaml

@@ -349,3 +349,24 @@ jobs:
       - uses: actions/checkout@v2
       - name: Check for unused irep ids
         run: ./scripts/string_table_check.sh
+
+  check-docker-image:
+    runs-on: ubuntu-20.04
+    steps:
+      - uses: actions/checkout@v2
+        with:
+          submodules: recursive
+      - name: Download test dependencies
+        run: sudo apt install openjdk-11-jdk-headless
+      - name: Build docker image
+        run: docker build -t cbmc .
+      - name: Smoke test goto-cc
+        run: docker run -v ${PWD}/.github/workflows/smoke_test_assets:/mnt/smoke -t cbmc goto-cc -o /mnt/smoke/test.goto /mnt/smoke/test.c
+      - name: Smoke test cbmc
+        run: docker run -v ${PWD}/.github/workflows/smoke_test_assets:/mnt/smoke -t cbmc cbmc /mnt/smoke/test.goto
+      - name: Smoke test jbmc
+        run: |
+          javac .github/workflows/smoke_test_assets/Test.java
+          docker run -v ${PWD}/.github/workflows/smoke_test_assets:/mnt/smoke -t cbmc jbmc --classpath /mnt/smoke Test
+      - name: Smoke test goto-analyzer
+        run: docker run -v ${PWD}/.github/workflows/smoke_test_assets:/mnt/smoke -t cbmc goto-analyzer /mnt/smoke/test.goto --unreachable-functions

.github/workflows/smoke_test_assets/Test.java

@@ -0,0 +1,6 @@
+public class Test {
+    public static void main(String[] args) {
+        System.out.println("Hi");
+        assert(1 == 1);
+    }
+}

.github/workflows/smoke_test_assets/test.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+
+#define return_val 0;
+
+int main(void)
+{
+  assert(1 == 1);
+  return return_val;
+}

COMPILING.md

@@ -301,6 +301,21 @@ the need to integrate JBMC as a separate project. Be aware that you need to
 change the build location (Select project in Eclipse -> Properties -> C/C++ 
 Build) to one of the src directories.
 
+# WORKING WITH DOCKER
+
+To compile and run the tools in a Docker container, do the following:
+
+1. From the root folder of the project, run `$ docker build -t cbmc .`
+2. After the building phase has finished, there should be a new 
+   image with the CProver binaries installed under `/usr/local/bin/`.
+
+   To start a container using that image as a base, run `$ docker run -i -t cbmc`
+   This will result in dropping you to a new terminal inside the container. To
+   load files for analysis into the container, one way is by mounting the folder
+   that contains the tests to the container. A possible invocation that does that
+   is: `$ docker run --mount type=bind,source=local/path/with/files,target=/mnt/analysis -i t cbmc`. In the
+   resulting container, the files present in the local file system under
+   `local/path/with/files` will be present under `/mnt/analysis`. 
 
 # OPTIONS AND VARIABLES
 

Dockerfile

@@ -0,0 +1,27 @@
+FROM ubuntu:20.04 as builder
+ENV DEBIAN_FRONTEND noninteractive
+ENV DEBCONF_NONINTERACTIVE_SEEN true
+# Timezone data is needed during the installation of dependencies,
+# since cmake depends on the tzdata package. In an interactive terminal,
+# the user selects the timezone at installation time. Since this needs
+# to be a non-interactive terminal, we need to setup some sort of default.
+# The UTC one seemed the most suitable one.
+RUN echo 'tzdata tzdata/Areas select Etc' | debconf-set-selections; \
+    echo 'tzdata tzdata/Zones/Etc select UTC' | debconf-set-selections; \
+    apt-get update && apt-get upgrade -y && apt-get install --no-install-recommends -y \
+    cmake \
+    ninja-build \
+    gcc \
+    g++ \
+    maven \
+    flex \
+    bison \
+    libxml2-utils \
+    patch
+COPY . /tmp/cbmc
+WORKDIR /tmp/cbmc
+RUN cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ && cd build; ninja -j2
+
+FROM ubuntu:20.04 as runner
+COPY --from=builder /tmp/cbmc/build/bin/* /usr/local/bin/
+RUN apt-get update && apt-get install -y gcc