From f0aa1f9e49b45db64d642f3b30279fd46db30b2c Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Mon, 4 Jan 2021 16:20:20 +0000 Subject: [PATCH 1/3] Add support for running CBMC in a Docker container. Add a Dockerfile that allows CBMC to be built and run in a Docker container. The Dockerfile is setup in a way that allows multi-stage builds, so that it's built in one container, and then the build artifacts are being copied in another. --- Dockerfile | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 Dockerfile diff --git a/Dockerfile b/Dockerfile new file mode 100644 index 00000000000..627b7ea5831 --- /dev/null +++ b/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 From 37a6c9f7fda93571f3010d4904c5c3bfd822fec4 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 6 Jan 2021 13:50:27 +0000 Subject: [PATCH 2/3] Add instructions for using the Dockerfile in COMPILING.md --- COMPILING.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/COMPILING.md b/COMPILING.md index e4e5dece720..c11c46ba4ea 100644 --- a/COMPILING.md +++ b/COMPILING.md @@ -300,6 +300,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 From fbcc05b3d2ec5c2b1a7254c7f23b707c8dcfe590 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 6 Jan 2021 14:33:44 +0000 Subject: [PATCH 3/3] Add a Dockerfile github action. This adds a github action that builds CBMC in a Docker container, and then exercises a small suite of smoke tests on it to make sure that the image is sound. --- .github/workflows/pull-request-checks.yaml | 21 +++++++++++++++++++ .github/workflows/smoke_test_assets/Test.java | 6 ++++++ .github/workflows/smoke_test_assets/test.c | 9 ++++++++ 3 files changed, 36 insertions(+) create mode 100644 .github/workflows/smoke_test_assets/Test.java create mode 100644 .github/workflows/smoke_test_assets/test.c diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index f190db489c9..9c1aa287c45 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.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 diff --git a/.github/workflows/smoke_test_assets/Test.java b/.github/workflows/smoke_test_assets/Test.java new file mode 100644 index 00000000000..eb27c41854d --- /dev/null +++ b/.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); + } +} diff --git a/.github/workflows/smoke_test_assets/test.c b/.github/workflows/smoke_test_assets/test.c new file mode 100644 index 00000000000..5e32995f692 --- /dev/null +++ b/.github/workflows/smoke_test_assets/test.c @@ -0,0 +1,9 @@ +#include + +#define return_val 0; + +int main(void) +{ + assert(1 == 1); + return return_val; +}