From 3f27e151468f187f05f9cf8361246e8506a0d369 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 11 Nov 2020 14:00:07 +0000 Subject: [PATCH 1/2] Add a linux+clang+make github actions pull request check job. This replaces a codebuild job that had not been ported yet, so that codebuild can be safely deactivated as a CI provider, having all the configurations ported so far. --- .github/workflows/pull-request-checks.yaml | 39 ++++++++++++++++++++++ 1 file changed, 39 insertions(+) diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index a3a4ddf7316..5edd6b480c3 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -59,6 +59,45 @@ jobs: env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2 make -C jbmc/regression test-parallel JOBS=2 + check-ubuntu-20_04-make-clang: + runs-on: ubuntu-20.04 + env: + CC: "/usr/bin/clang" + CXX: "/usr/bin/clang++" + steps: + - uses: actions/checkout@v2 + with: + submodules: recursive + - name: Fetch dependencies + env: + # This is needed in addition to -yq to prevent apt-get from asking for + # user input + DEBIAN_FRONTEND: noninteractive + run: | + sudo apt-get update + sudo apt-get install --no-install-recommends -yq clang-10 clang++-10 gdb maven jq flex bison libxml2-utils cpanminus + make -C src minisat2-download + cpanm Thread::Pool::Simple + - name: Build with make + run: | + make -C src -j2 + make -C unit -j2 + make -C jbmc/src -j2 + make -C jbmc/unit -j2 + - name: Run unit tests + run: | + make -C unit test + make -C jbmc/unit test + - name: Running expected failure unit tests + run: | + make TAGS="[!shouldfail]" -C unit test + make TAGS="[!shouldfail]" -C jbmc/unit test + - name: Run regression tests + run: | + make -C regression test-parallel JOBS=2 + make -C regression/cbmc test-paths-lifo + env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2 + make -C jbmc/regression test-parallel JOBS=2 check-ubuntu-20_04-cmake-gcc: runs-on: ubuntu-20.04 steps: From 81ecf05baee6d776646be80252c00d291682eca2 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 17 Feb 2021 14:35:34 +0000 Subject: [PATCH 2/2] Enable ccache for the linux*make*clang job. --- .github/workflows/pull-request-checks.yaml | 27 ++++++++++++++++++---- 1 file changed, 22 insertions(+), 5 deletions(-) diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index 5edd6b480c3..ddd699c7658 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -62,8 +62,8 @@ jobs: check-ubuntu-20_04-make-clang: runs-on: ubuntu-20.04 env: - CC: "/usr/bin/clang" - CXX: "/usr/bin/clang++" + CC: "ccache /usr/bin/clang" + CXX: "ccache /usr/bin/clang++" steps: - uses: actions/checkout@v2 with: @@ -75,20 +75,36 @@ jobs: DEBIAN_FRONTEND: noninteractive run: | sudo apt-get update - sudo apt-get install --no-install-recommends -yq clang-10 clang++-10 gdb maven jq flex bison libxml2-utils cpanminus + sudo apt-get install --no-install-recommends -yq clang-10 clang++-10 gdb maven jq flex bison libxml2-utils cpanminus ccache make -C src minisat2-download cpanm Thread::Pool::Simple + - name: Prepare ccache + uses: actions/cache@v2 + with: + path: .ccache + key: ${{ runner.os }}-20.04-make-clang-${{ github.ref }}-${{ github.sha }}-PR + restore-keys: | + ${{ runner.os }}-20.04-make-clang-${{ github.ref }} + ${{ runner.os }}-20.04-make-clang + - name: ccache environment + run: | + echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV + echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV + - name: Zero ccache stats and limit in size + run: ccache -z --max-size=500M - name: Build with make run: | make -C src -j2 make -C unit -j2 make -C jbmc/src -j2 make -C jbmc/unit -j2 + - name: Print ccache stats + run: ccache -s - name: Run unit tests run: | make -C unit test make -C jbmc/unit test - - name: Running expected failure unit tests + - name: Run expected failure unit tests run: | make TAGS="[!shouldfail]" -C unit test make TAGS="[!shouldfail]" -C jbmc/unit test @@ -97,7 +113,8 @@ jobs: make -C regression test-parallel JOBS=2 make -C regression/cbmc test-paths-lifo env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2 - make -C jbmc/regression test-parallel JOBS=2 + make -C jbmc/regression test-parallel JOBS=2 + check-ubuntu-20_04-cmake-gcc: runs-on: ubuntu-20.04 steps: