From 63237ae6e1c427228d28425682c06be3bc2b0d16 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Mon, 7 Sep 2020 21:06:38 +0200 Subject: [PATCH 01/15] cbmc: test compile Xen In the past, changes to CPROVER tools resulted in a broken build for systems software like e.g. Xen. To avoid this issue in the future, we want to integrate Xen compilation into continuous testing. This allows to identify issues early, and fix them appropriately. Signed-off-by: Norbert Manthey --- .github/workflows/build-and-test-Xen.yml | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/.github/workflows/build-and-test-Xen.yml b/.github/workflows/build-and-test-Xen.yml index 7aab6780232..f52a3e7a5c4 100644 --- a/.github/workflows/build-and-test-Xen.yml +++ b/.github/workflows/build-and-test-Xen.yml @@ -22,5 +22,17 @@ jobs: run: make -C src minisat2-download run: make -C src cbmc.dir goto-cc.dir goto-diff.dir + - name: get one-line-scan + run: git clone https://github.com/awslabs/one-line-scan.git + - name: get Xen 4.13 run: git clone git://xenbits.xen.org/xen.git xen_4_13 && cd xen_4_13 && git reset --hard RELEASE-4.13.0 + + - name: compile Xen with CBMC via one-line-scan + run: ls + run: pwd + run: ls src/* + run: ln -sf src/goto-cc/goto-cc src/goto-cc/goto-ld + run: ln -sf src/goto-cc/goto-cc src/goto-cc/goto-as + run: ln -sf src/goto-cc/goto-cc src/goto-cc/goto-g++ + run: PATH=$PATH:src/cbmc:src/goto-cc one-line-scan/one-line-scan --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- make -C xen xen -j $(nproc) -k From 6f13454b5d4eb4b5904667d61d8fc325e954525f Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Tue, 8 Sep 2020 11:17:36 +0200 Subject: [PATCH 02/15] workflows: check xen on PR Signed-off-by: Norbert Manthey --- .github/workflows/build-and-test-Xen.yml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/.github/workflows/build-and-test-Xen.yml b/.github/workflows/build-and-test-Xen.yml index f52a3e7a5c4..39f51a31117 100644 --- a/.github/workflows/build-and-test-Xen.yml +++ b/.github/workflows/build-and-test-Xen.yml @@ -1,6 +1,8 @@ name: Build and Test Xen -on: [push] +on: + pull_request: + branches: [ develop ] jobs: Linux: From 01702e9ceb2c899421e7da590a936c24a71bf4e1 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Tue, 8 Sep 2020 11:29:38 +0200 Subject: [PATCH 03/15] README: add a space --- .github/workflows/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/README.md b/.github/workflows/README.md index 95d5ec21cc1..0ab3e0b2dd0 100644 --- a/.github/workflows/README.md +++ b/.github/workflows/README.md @@ -1,4 +1,4 @@ -# CBMC packages +# CBMC packages This project builds installation packages for the tip of the develop branch for MacOS, Windows, and Ubuntu. From a0e41e10972bf878376a0dc5427cea485b23b9cd Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Tue, 8 Sep 2020 11:32:52 +0200 Subject: [PATCH 04/15] rename workflow file Signed-off-by: Norbert Manthey --- .../workflows/{build-and-test-Xen.yml => build-and-test-Xen.yaml} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename .github/workflows/{build-and-test-Xen.yml => build-and-test-Xen.yaml} (100%) diff --git a/.github/workflows/build-and-test-Xen.yml b/.github/workflows/build-and-test-Xen.yaml similarity index 100% rename from .github/workflows/build-and-test-Xen.yml rename to .github/workflows/build-and-test-Xen.yaml From a482270c1c7943dce4673cb0107b94febae1260f Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Tue, 8 Sep 2020 11:38:54 +0200 Subject: [PATCH 05/15] workflows: extend PR Signed-off-by: Norbert Manthey --- .github/workflows/pull-request-checks.yaml | 35 ++++++++++++++++++++++ 1 file changed, 35 insertions(+) diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index 3488a530a9e..9073ceafc17 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -176,3 +176,38 @@ jobs: - uses: actions/checkout@v2 - name: Check for unused irep ids run: ./scripts/string_table_check.sh + + CompileXen: + runs-on: ubuntu-18.04 + steps: + - uses: actions/checkout@v2 + with: + submodules: true + - name: Install Packages + env: + # This is needed in addition to -yq to prevent apt-get from asking for + # user input + DEBIAN_FRONTEND: noninteractive + run: sudo apt-get install coreutils \ + build-essential gcc git make flex bison \ + software-properties-common libwww-perl python \ + bin86 gdb bcc liblzma-dev python-dev gettext iasl \ + uuid-dev libncurses5-dev libncursesw5-dev pkg-config \ + libgtk2.0-dev libyajl-dev sudo time + - name: build CBMC tools + run: | + make -C src minisat2-download + make -C src cbmc.dir goto-cc.dir goto-diff.dir + - name: get one-line-scan + run: git clone https://github.com/awslabs/one-line-scan.git + - name: get Xen 4.13 + run: git clone git://xenbits.xen.org/xen.git xen_4_13 && cd xen_4_13 && git reset --hard RELEASE-4.13.0 + - name: compile Xen with CBMC via one-line-scan + run: | + ls + pwd + ls src/* + ln -sf src/goto-cc/goto-cc src/goto-cc/goto-ld + ln -sf src/goto-cc/goto-cc src/goto-cc/goto-as + ln -sf src/goto-cc/goto-cc src/goto-cc/goto-g++ + PATH=$PATH:src/cbmc:src/goto-cc one-line-scan/one-line-scan --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- make -C xen xen -j $(nproc) -k From a6ed24739723437eed36e12b6bc4609e74be4fe3 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Tue, 8 Sep 2020 11:44:08 +0200 Subject: [PATCH 06/15] workflow: fix xen --- .github/workflows/build-and-test-Xen.yaml | 62 +++++++++++------------ 1 file changed, 31 insertions(+), 31 deletions(-) diff --git a/.github/workflows/build-and-test-Xen.yaml b/.github/workflows/build-and-test-Xen.yaml index 39f51a31117..468f6080260 100644 --- a/.github/workflows/build-and-test-Xen.yaml +++ b/.github/workflows/build-and-test-Xen.yaml @@ -5,36 +5,36 @@ on: branches: [ develop ] jobs: - Linux: - + CompileXen: runs-on: ubuntu-18.04 - steps: - - name: Install Packages - run: sudo apt-get install coreutils \ - build-essential gcc git make flex bison \ - software-properties-common libwww-perl python \ - bin86 gdb bcc liblzma-dev python-dev gettext iasl \ - uuid-dev libncurses5-dev libncursesw5-dev pkg-config \ - libgtk2.0-dev libyajl-dev sudo time - - - uses: actions/checkout@v1 - - - name: build CBMC tools - run: make -C src minisat2-download - run: make -C src cbmc.dir goto-cc.dir goto-diff.dir - - - name: get one-line-scan - run: git clone https://github.com/awslabs/one-line-scan.git - - - name: get Xen 4.13 - run: git clone git://xenbits.xen.org/xen.git xen_4_13 && cd xen_4_13 && git reset --hard RELEASE-4.13.0 - - - name: compile Xen with CBMC via one-line-scan - run: ls - run: pwd - run: ls src/* - run: ln -sf src/goto-cc/goto-cc src/goto-cc/goto-ld - run: ln -sf src/goto-cc/goto-cc src/goto-cc/goto-as - run: ln -sf src/goto-cc/goto-cc src/goto-cc/goto-g++ - run: PATH=$PATH:src/cbmc:src/goto-cc one-line-scan/one-line-scan --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- make -C xen xen -j $(nproc) -k + - uses: actions/checkout@v2 + with: + submodules: true + - name: Install Packages + env: + # This is needed in addition to -yq to prevent apt-get from asking for + # user input + DEBIAN_FRONTEND: noninteractive + run: | + sudo apt-get install -y coreutils build-essential gcc git make flex bison software-properties-common libwww-perl python + sudo apt-get install -y bin86 gdb bcc liblzma-dev python-dev gettext iasl uuid-dev libncurses5-dev libncursesw5-dev pkg-config + sudo apt-get install -y libgtk2.0-dev libyajl-dev sudo time + - name: build CBMC tools + run: | + make -C src minisat2-download + make -C src cbmc.dir goto-cc.dir goto-diff.dir + - name: get one-line-scan + run: git clone -b path-addition https://github.com/awslabs/one-line-scan.git + - name: get Xen 4.13 + run: git clone git://xenbits.xen.org/xen.git xen_4_13 && cd xen_4_13 && git reset --hard RELEASE-4.13.0 + - name: compile Xen with CBMC via one-line-scan + run: | + ls + pwd + ls src/goto-cc/goto-cc + ln -s src/goto-cc/goto-cc src/goto-cc/goto-ld + ln -s src/goto-cc/goto-cc src/goto-cc/goto-as + ln -s src/goto-cc/goto-cc src/goto-cc/goto-g++ + one-line-scan/one-line-scan --add-to-path src/cbmc --add-to-path src/goto-cc --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- env + one-line-scan/one-line-scan --add-to-path src/cbmc --add-to-path src/goto-cc --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- make -C xen xen -j $(nproc) -k From a4dfdf706a29f3a3553731b1c28bfe9fa21f0a9b Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Fri, 25 Sep 2020 11:54:00 +0200 Subject: [PATCH 07/15] trigger again Signed-off-by: Norbert Manthey --- .github/workflows/build-and-test-Xen.yaml | 2 -- 1 file changed, 2 deletions(-) diff --git a/.github/workflows/build-and-test-Xen.yaml b/.github/workflows/build-and-test-Xen.yaml index 468f6080260..cf13f4cc9a4 100644 --- a/.github/workflows/build-and-test-Xen.yaml +++ b/.github/workflows/build-and-test-Xen.yaml @@ -30,8 +30,6 @@ jobs: run: git clone git://xenbits.xen.org/xen.git xen_4_13 && cd xen_4_13 && git reset --hard RELEASE-4.13.0 - name: compile Xen with CBMC via one-line-scan run: | - ls - pwd ls src/goto-cc/goto-cc ln -s src/goto-cc/goto-cc src/goto-cc/goto-ld ln -s src/goto-cc/goto-cc src/goto-cc/goto-as From b8407e1fc0a2109d208cc5bdd91cd12732460bdf Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Fri, 25 Sep 2020 13:21:40 +0200 Subject: [PATCH 08/15] split steps more Signed-off-by: Norbert Manthey --- .github/workflows/build-and-test-Xen.yaml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/.github/workflows/build-and-test-Xen.yaml b/.github/workflows/build-and-test-Xen.yaml index cf13f4cc9a4..674b4e1273f 100644 --- a/.github/workflows/build-and-test-Xen.yaml +++ b/.github/workflows/build-and-test-Xen.yaml @@ -28,11 +28,14 @@ jobs: run: git clone -b path-addition https://github.com/awslabs/one-line-scan.git - name: get Xen 4.13 run: git clone git://xenbits.xen.org/xen.git xen_4_13 && cd xen_4_13 && git reset --hard RELEASE-4.13.0 - - name: compile Xen with CBMC via one-line-scan + - name: prepare compile Xen with CBMC via one-line-scan run: | - ls src/goto-cc/goto-cc ln -s src/goto-cc/goto-cc src/goto-cc/goto-ld ln -s src/goto-cc/goto-cc src/goto-cc/goto-as ln -s src/goto-cc/goto-cc src/goto-cc/goto-g++ - one-line-scan/one-line-scan --add-to-path src/cbmc --add-to-path src/goto-cc --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- env - one-line-scan/one-line-scan --add-to-path src/cbmc --add-to-path src/goto-cc --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- make -C xen xen -j $(nproc) -k + - name: check links for compile Xen with CBMC via one-line-scan + run: ls src/goto-cc/goto-cc + - name: check compile Xen with CBMC via one-line-scan + run: one-line-scan/one-line-scan --add-to-path src/cbmc --add-to-path src/goto-cc --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- env + - name: compile Xen with CBMC via one-line-scan + run: one-line-scan/one-line-scan --add-to-path src/cbmc --add-to-path src/goto-cc --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- make -C xen xen -j $(nproc) -k From 7a1590ea88994f1300b500c4565370cb73ce87b0 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Fri, 25 Sep 2020 14:01:17 +0200 Subject: [PATCH 09/15] improve ls, use plain for checking Signed-off-by: Norbert Manthey --- .github/workflows/build-and-test-Xen.yaml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/build-and-test-Xen.yaml b/.github/workflows/build-and-test-Xen.yaml index 674b4e1273f..4b6fa54bffe 100644 --- a/.github/workflows/build-and-test-Xen.yaml +++ b/.github/workflows/build-and-test-Xen.yaml @@ -34,8 +34,8 @@ jobs: ln -s src/goto-cc/goto-cc src/goto-cc/goto-as ln -s src/goto-cc/goto-cc src/goto-cc/goto-g++ - name: check links for compile Xen with CBMC via one-line-scan - run: ls src/goto-cc/goto-cc + run: ls src/goto-cc - name: check compile Xen with CBMC via one-line-scan - run: one-line-scan/one-line-scan --add-to-path src/cbmc --add-to-path src/goto-cc --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- env + run: one-line-scan/one-line-scan --add-to-path src/cbmc --add-to-path src/goto-cc --no-analysis --no-gotocc --plain --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- env - name: compile Xen with CBMC via one-line-scan run: one-line-scan/one-line-scan --add-to-path src/cbmc --add-to-path src/goto-cc --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- make -C xen xen -j $(nproc) -k From 816d9e0863f2955bf33ea4e3fb512a1e6ebd87f0 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Fri, 25 Sep 2020 15:03:48 +0200 Subject: [PATCH 10/15] use full path for PATH Signed-off-by: Norbert Manthey --- .github/workflows/build-and-test-Xen.yaml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/build-and-test-Xen.yaml b/.github/workflows/build-and-test-Xen.yaml index 4b6fa54bffe..2fa646dfe44 100644 --- a/.github/workflows/build-and-test-Xen.yaml +++ b/.github/workflows/build-and-test-Xen.yaml @@ -36,6 +36,6 @@ jobs: - name: check links for compile Xen with CBMC via one-line-scan run: ls src/goto-cc - name: check compile Xen with CBMC via one-line-scan - run: one-line-scan/one-line-scan --add-to-path src/cbmc --add-to-path src/goto-cc --no-analysis --no-gotocc --plain --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- env + run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-cc --no-analysis --no-gotocc --plain --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- env - name: compile Xen with CBMC via one-line-scan - run: one-line-scan/one-line-scan --add-to-path src/cbmc --add-to-path src/goto-cc --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- make -C xen xen -j $(nproc) -k + run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-cc --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- make -C xen xen -j $(nproc) -k From a9996d392da1944d9b58b70e6ebb0b9b56fa72d8 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Mon, 28 Sep 2020 14:06:07 +0200 Subject: [PATCH 11/15] check tools explicitly Signed-off-by: Norbert Manthey --- .github/workflows/build-and-test-Xen.yaml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/.github/workflows/build-and-test-Xen.yaml b/.github/workflows/build-and-test-Xen.yaml index 2fa646dfe44..bc63673e6cc 100644 --- a/.github/workflows/build-and-test-Xen.yaml +++ b/.github/workflows/build-and-test-Xen.yaml @@ -36,6 +36,12 @@ jobs: - name: check links for compile Xen with CBMC via one-line-scan run: ls src/goto-cc - name: check compile Xen with CBMC via one-line-scan - run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-cc --no-analysis --no-gotocc --plain --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- env + run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff --add-to-path $(pwd)/src/goto-cc --no-analysis --no-gotocc --plain --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- env + - name: check goto-ld + run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff --add-to-path $(pwd)/src/goto-cc --no-analysis --no-gotocc --plain --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- which goto-ld + - name: check goto-as + run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff --add-to-path $(pwd)/src/goto-cc --no-analysis --no-gotocc --plain --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- which goto-as + - name: check goto-diff + run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff --add-to-path $(pwd)/src/goto-cc --no-analysis --no-gotocc --plain --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- which goto-diff - name: compile Xen with CBMC via one-line-scan run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-cc --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- make -C xen xen -j $(nproc) -k From 56826a9452b6151b8b98584a0c647bf3d6be8b26 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Mon, 28 Sep 2020 14:47:06 +0200 Subject: [PATCH 12/15] fix links Signed-off-by: Norbert Manthey --- .github/workflows/build-and-test-Xen.yaml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/.github/workflows/build-and-test-Xen.yaml b/.github/workflows/build-and-test-Xen.yaml index bc63673e6cc..0590ec83507 100644 --- a/.github/workflows/build-and-test-Xen.yaml +++ b/.github/workflows/build-and-test-Xen.yaml @@ -30,11 +30,11 @@ jobs: run: git clone git://xenbits.xen.org/xen.git xen_4_13 && cd xen_4_13 && git reset --hard RELEASE-4.13.0 - name: prepare compile Xen with CBMC via one-line-scan run: | - ln -s src/goto-cc/goto-cc src/goto-cc/goto-ld - ln -s src/goto-cc/goto-cc src/goto-cc/goto-as - ln -s src/goto-cc/goto-cc src/goto-cc/goto-g++ + ln -s goto-cc src/goto-cc/goto-ld + ln -s goto-cc src/goto-cc/goto-as + ln -s goto-cc src/goto-cc/goto-g++ - name: check links for compile Xen with CBMC via one-line-scan - run: ls src/goto-cc + run: ls -l src/goto-cc - name: check compile Xen with CBMC via one-line-scan run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff --add-to-path $(pwd)/src/goto-cc --no-analysis --no-gotocc --plain --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- env - name: check goto-ld @@ -44,4 +44,4 @@ jobs: - name: check goto-diff run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff --add-to-path $(pwd)/src/goto-cc --no-analysis --no-gotocc --plain --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- which goto-diff - name: compile Xen with CBMC via one-line-scan - run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-cc --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- make -C xen xen -j $(nproc) -k + run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff --add-to-path $(pwd)/src/goto-cc --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- make -C xen xen -j $(nproc) -k From 0b2e3fbe56b082bff91bc5504e1b7d0df15e6d7b Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Tue, 29 Sep 2020 09:49:44 +0200 Subject: [PATCH 13/15] fix build command Signed-off-by: Norbert Manthey --- .github/workflows/build-and-test-Xen.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/build-and-test-Xen.yaml b/.github/workflows/build-and-test-Xen.yaml index 0590ec83507..1e14c209f0d 100644 --- a/.github/workflows/build-and-test-Xen.yaml +++ b/.github/workflows/build-and-test-Xen.yaml @@ -44,4 +44,4 @@ jobs: - name: check goto-diff run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff --add-to-path $(pwd)/src/goto-cc --no-analysis --no-gotocc --plain --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- which goto-diff - name: compile Xen with CBMC via one-line-scan - run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff --add-to-path $(pwd)/src/goto-cc --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- make -C xen xen -j $(nproc) -k + run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff --add-to-path $(pwd)/src/goto-cc --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- make -C xen -j $(nproc) -k From c036788167c31a06eb0e8b607c130c60c8f4b7cc Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Tue, 29 Sep 2020 10:40:36 +0200 Subject: [PATCH 14/15] use actual xen repository Signed-off-by: Norbert Manthey --- .github/workflows/build-and-test-Xen.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/build-and-test-Xen.yaml b/.github/workflows/build-and-test-Xen.yaml index 1e14c209f0d..5f36b05d66d 100644 --- a/.github/workflows/build-and-test-Xen.yaml +++ b/.github/workflows/build-and-test-Xen.yaml @@ -44,4 +44,4 @@ jobs: - name: check goto-diff run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff --add-to-path $(pwd)/src/goto-cc --no-analysis --no-gotocc --plain --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- which goto-diff - name: compile Xen with CBMC via one-line-scan - run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff --add-to-path $(pwd)/src/goto-cc --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- make -C xen -j $(nproc) -k + run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff --add-to-path $(pwd)/src/goto-cc --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- make -C xen_4_13 xen -j $(nproc) -k From ff60774f773944b7fbccd156ba5143e7f72f49a5 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Tue, 29 Sep 2020 14:52:24 +0200 Subject: [PATCH 15/15] make change production like Signed-off-by: Norbert Manthey --- .github/workflows/build-and-test-Xen.yaml | 18 +++++------------- 1 file changed, 5 insertions(+), 13 deletions(-) diff --git a/.github/workflows/build-and-test-Xen.yaml b/.github/workflows/build-and-test-Xen.yaml index 5f36b05d66d..5adb7afd156 100644 --- a/.github/workflows/build-and-test-Xen.yaml +++ b/.github/workflows/build-and-test-Xen.yaml @@ -27,21 +27,13 @@ jobs: - name: get one-line-scan run: git clone -b path-addition https://github.com/awslabs/one-line-scan.git - name: get Xen 4.13 - run: git clone git://xenbits.xen.org/xen.git xen_4_13 && cd xen_4_13 && git reset --hard RELEASE-4.13.0 + run: git clone git://xenbits.xen.org/xen.git xen_4_13 && cd xen_4_13 && git reset --hard RELEASE-4.13.0 && pwd - name: prepare compile Xen with CBMC via one-line-scan run: | ln -s goto-cc src/goto-cc/goto-ld ln -s goto-cc src/goto-cc/goto-as ln -s goto-cc src/goto-cc/goto-g++ - - name: check links for compile Xen with CBMC via one-line-scan - run: ls -l src/goto-cc - - name: check compile Xen with CBMC via one-line-scan - run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff --add-to-path $(pwd)/src/goto-cc --no-analysis --no-gotocc --plain --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- env - - name: check goto-ld - run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff --add-to-path $(pwd)/src/goto-cc --no-analysis --no-gotocc --plain --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- which goto-ld - - name: check goto-as - run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff --add-to-path $(pwd)/src/goto-cc --no-analysis --no-gotocc --plain --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- which goto-as - - name: check goto-diff - run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff --add-to-path $(pwd)/src/goto-cc --no-analysis --no-gotocc --plain --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- which goto-diff - - name: compile Xen with CBMC via one-line-scan - run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff --add-to-path $(pwd)/src/goto-cc --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- make -C xen_4_13 xen -j $(nproc) -k + - name: compile Xen with CBMC via one-line-scan, and check for goto-cc section + run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff --add-to-path $(pwd)/src/goto-cc --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- make -C xen_4_13 xen -j $(nproc) -k || true + - name: check for goto-cc section in xen-syms binary + run: objdump -h xen_4_13/xen/xen-syms | grep "goto-cc"