From d873708a30e5860ab19727bedc370f270ad9601d Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 22 Mar 2022 15:56:47 +0000 Subject: [PATCH 1/3] Change regression testing suite to support running tests with cvc5. This allows us to test against more than one solvers in the new backend (currently tested - cvc5, z3). This ensures that we don't invariably issue output that is solver specific, tying the new backend to a single solver by accident. --- regression/cbmc-incr-smt2/CMakeLists.txt | 16 +++++++++++++--- .../overflow_behaviour.desc | 2 +- .../polynomial.desc | 2 +- .../simple_equation.desc | 2 +- .../unsigned_behaviour.desc | 2 +- .../bitvector-bitwise-operators/bitwise.desc | 2 +- .../bitvector-bitwise-operators/shift_left.desc | 2 +- .../bitvector-bitwise-operators/shift_right.c | 4 ++++ .../bitvector-bitwise-operators/shift_right.desc | 2 +- .../bitvector-flag-tests/div_by_zero.desc | 2 +- .../bitvector-flag-tests/signed_overflow.desc | 2 +- .../control_flow.desc | 4 ++-- .../incremental_solver_called.desc | 4 ++-- .../nondeterministic-int-assert/stdbool.desc | 4 ++-- .../nondeterministic-int-assert/trace.desc | 4 ++-- .../nondeterministic-int-assert/valid_unsat.desc | 4 ++-- 16 files changed, 36 insertions(+), 22 deletions(-) diff --git a/regression/cbmc-incr-smt2/CMakeLists.txt b/regression/cbmc-incr-smt2/CMakeLists.txt index 06a41cf3496..6b00d1fc51d 100644 --- a/regression/cbmc-incr-smt2/CMakeLists.txt +++ b/regression/cbmc-incr-smt2/CMakeLists.txt @@ -1,10 +1,20 @@ if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows") - set(exclude_win_broken_tests -X winbug) + set(exclude_win_broken_tests "-X;winbug") else() set(exclude_win_broken_tests "") endif() -add_test_pl_tests( - "$ --validate-goto-model --validate-ssa-equation --slice-formula" ${exclude_win_broken_tests} +add_test_pl_profile( + "cbmc-incr-smt2-z3" + "$ --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation --slice-formula" + "-C;${exclude_win_broken_tests};-s;new-smt-z3" + "CORE" +) + +add_test_pl_profile( + "cbmc-incr-smt2-cvc5" + "$ --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation --slice-formula" + "-C;${exclude_win_broken_tests};-s;new-smt-cvc5" + "CORE" ) diff --git a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/overflow_behaviour.desc b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/overflow_behaviour.desc index 4e2f90d69b1..d45e6ebe787 100644 --- a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/overflow_behaviour.desc +++ b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/overflow_behaviour.desc @@ -1,6 +1,6 @@ CORE overflow_behaviour.c ---incremental-smt2-solver 'z3 --smt2 -in' --trace +--trace \[main\.assertion\.1\] line \d+ Wrap-around to INT_MIN when adding to INT_MAX: SUCCESS \[main\.assertion\.2\] line \d+ Wrap-around to INT_MAX when subtracting from INT_MIN: SUCCESS \[main\.assertion\.3\] line \d+ INT_MAX minus INT_MIN equals -1: SUCCESS diff --git a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/polynomial.desc b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/polynomial.desc index 6149a33f6d1..55f19120fb0 100644 --- a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/polynomial.desc +++ b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/polynomial.desc @@ -1,6 +1,6 @@ CORE polynomial.c ---incremental-smt2-solver 'z3 --smt2 -in' --trace +--trace \[main\.assertion\.1\] line \d+ No negative solution: FAILURE \[main\.assertion\.2\] line \d+ No positive solution: FAILURE x=-8\ \(11111111 11111111 11111111 11111000\) diff --git a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/simple_equation.desc b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/simple_equation.desc index 8ae4bae24b7..499ccbe044b 100644 --- a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/simple_equation.desc +++ b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/simple_equation.desc @@ -1,6 +1,6 @@ CORE simple_equation.c ---incremental-smt2-solver 'z3 --smt2 -in' --trace --verbosity 10 +--trace --verbosity 10 \[main\.assertion\.1\] line \d+ a plus a always equals two times a: SUCCESS \[main\.assertion\.2\] line \d+ a minus a always equals 0: SUCCESS \[main\.assertion\.3\] line \d+ a plus its additive inverse equals 0: SUCCESS diff --git a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/unsigned_behaviour.desc b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/unsigned_behaviour.desc index db0157d613b..52ecdacce30 100644 --- a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/unsigned_behaviour.desc +++ b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/unsigned_behaviour.desc @@ -1,6 +1,6 @@ CORE unsigned_behaviour.c ---incremental-smt2-solver 'z3 --smt2 -in' --trace +--trace \[main\.assertion\.1\] line \d+ a plus b should be more than 27: FAILURE \[main\.assertion\.2\] line \d+ a plus b should be more than 27: FAILURE \[main\.assertion\.3\] line \d+ c plus d should be more than 27: FAILURE diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/bitwise.desc b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/bitwise.desc index e5431ba76e6..44db46465de 100644 --- a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/bitwise.desc +++ b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/bitwise.desc @@ -1,6 +1,6 @@ CORE bitwise_ops.c ---incremental-smt2-solver 'z3 --smt2 -in' --slice-formula +--slice-formula \[main\.assertion\.1\] line \d+ This is going to fail for bit-opposites: FAILURE \[main\.assertion\.2\] line \d+ This is going to hold for all values != 0: SUCCESS \[main\.assertion\.3\] line \d+ This is going to fail for the same value in A and B: FAILURE diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_left.desc b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_left.desc index e6248c053ea..ffe947dd21e 100644 --- a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_left.desc +++ b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_left.desc @@ -1,6 +1,6 @@ CORE shift_left.c ---incremental-smt2-solver 'z3 --smt2 -in' --slice-formula +--slice-formula \[main\.assertion\.1\] line \d Shifted result should be greater than one: FAILURE ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.c b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.c index 301fe1a180b..02a4471cd04 100644 --- a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.c +++ b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.c @@ -10,6 +10,10 @@ int main() { int first; uint8_t second; + // This assumption is here in order to constrain the value the solver + // can produce to just 128 so that we don't get test failures for different + // values returned by different SMT solvers. + __CPROVER_assume((second & 1) == 0); int place; __CPROVER_assume(place >= 1); diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.desc b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.desc index d7e290ae8b8..dc7a14fd911 100644 --- a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.desc +++ b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.desc @@ -1,6 +1,6 @@ CORE shift_right.c ---incremental-smt2-solver 'z3 --smt2 -in' --slice-formula --trace +--slice-formula --trace \[main\.assertion\.1\] line \d+ Right shifting a uint with leftmost bit set is a logical shift: FAILURE \[main\.assertion\.2\] line \d+ Right shifting a positive number has a lower bound of 0: SUCCESS \[main\.assertion\.3\] line \d+ Right shifting a negative number has a lower bound value of -1: SUCCESS diff --git a/regression/cbmc-incr-smt2/bitvector-flag-tests/div_by_zero.desc b/regression/cbmc-incr-smt2/bitvector-flag-tests/div_by_zero.desc index 9f093877f9f..0279e9b9725 100644 --- a/regression/cbmc-incr-smt2/bitvector-flag-tests/div_by_zero.desc +++ b/regression/cbmc-incr-smt2/bitvector-flag-tests/div_by_zero.desc @@ -1,6 +1,6 @@ CORE div_by_zero.c ---incremental-smt2-solver 'z3 --smt2 -in' --div-by-zero-check --trace +--div-by-zero-check --trace \[main\.division-by-zero\.1\] line \d division by zero in x / y: FAILURE \[main\.division-by-zero\.2\] line \d+ division by zero in x / z: SUCCESS y=0 diff --git a/regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.desc b/regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.desc index 9c561b2433b..8b3cce08da5 100644 --- a/regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.desc +++ b/regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.desc @@ -1,6 +1,6 @@ CORE signed_overflow.c ---incremental-smt2-solver 'z3 --smt2 -in' --signed-overflow-check --trace +--signed-overflow-check --trace ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc b/regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc index cb971aec828..cdf8a033eec 100644 --- a/regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc +++ b/regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc @@ -1,7 +1,7 @@ CORE control_flow.c ---incremental-smt2-solver 'z3 --smt2 -in' --verbosity 10 -Passing problem to incremental SMT2 solving via "z3 --smt2 -in" +--verbosity 10 +Passing problem to incremental SMT2 solving via Sending command to SMT2 solver - \(set-option :produce-models true\) Sending command to SMT2 solver - \(set-logic QF_UFBV\) Sending command to SMT2 solver - \(declare-fun |goto_symex::&92;guard#1| \(\) Bool\) diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc b/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc index 38b41075e78..4212286e9fd 100644 --- a/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc +++ b/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc @@ -1,7 +1,7 @@ CORE test.c ---incremental-smt2-solver 'z3 --smt2 -in' --verbosity 10 -Passing problem to incremental SMT2 solving via "z3 --smt2 -in" +--verbosity 10 +Passing problem to incremental SMT2 solving via Sending command to SMT2 solver - \(set-option :produce-models true\) Sending command to SMT2 solver - \(set-logic QF_UFBV\) Sending command to SMT2 solver - \(define-fun |B0| \(\) Bool true\) diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/stdbool.desc b/regression/cbmc-incr-smt2/nondeterministic-int-assert/stdbool.desc index 2135ea76791..61d49d1fbe5 100644 --- a/regression/cbmc-incr-smt2/nondeterministic-int-assert/stdbool.desc +++ b/regression/cbmc-incr-smt2/nondeterministic-int-assert/stdbool.desc @@ -1,7 +1,7 @@ CORE stdbool_example.c ---incremental-smt2-solver 'z3 --smt2 -in' --trace -Passing problem to incremental SMT2 solving via "z3 --smt2 -in" +--trace +Passing problem to incremental SMT2 solving via VERIFICATION FAILED equal=FALSE\s*\([0 ]+\) equal=TRUE\s*\([0 ]+1\) diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/trace.desc b/regression/cbmc-incr-smt2/nondeterministic-int-assert/trace.desc index d7546c34f8c..69bdd2bf605 100644 --- a/regression/cbmc-incr-smt2/nondeterministic-int-assert/trace.desc +++ b/regression/cbmc-incr-smt2/nondeterministic-int-assert/trace.desc @@ -1,7 +1,7 @@ CORE trace.c ---incremental-smt2-solver 'z3 --smt2 -in' --trace -Passing problem to incremental SMT2 solving via "z3 --smt2 -in" +--trace +Passing problem to incremental SMT2 solving via Assert of inequality to 4\.: FAILURE Assert of inequality to 2\.: FAILURE y=4 diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/valid_unsat.desc b/regression/cbmc-incr-smt2/nondeterministic-int-assert/valid_unsat.desc index e34ae2426b4..7535bf54fa0 100644 --- a/regression/cbmc-incr-smt2/nondeterministic-int-assert/valid_unsat.desc +++ b/regression/cbmc-incr-smt2/nondeterministic-int-assert/valid_unsat.desc @@ -1,7 +1,7 @@ CORE valid_unsat.c ---incremental-smt2-solver 'z3 --smt2 -in' --verbosity 10 -Passing problem to incremental SMT2 solving via "z3 --smt2 -in" +--verbosity 10 +Passing problem to incremental SMT2 solving via Sending command to SMT2 solver - \(check-sat\) Solver response - unsat VERIFICATION SUCCESSFUL From 69d37a6e122bc8783006e6f107930d88bb99e07e Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 30 Mar 2022 15:25:44 +0100 Subject: [PATCH 2/3] Change `Makefile` in `regression/cbmc-incr-smt2` to support testing with multiple solvers. Previously the command that was enabling the new SMT backend (and providing the script for invoking the appropriate SMT solver) was passed as part of the options passed in `test.desc`. Since this was removed, and passed as part of the test configuration in the `CMakeLists.txt`, we need to do the same here. --- regression/cbmc-incr-smt2/Makefile | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/regression/cbmc-incr-smt2/Makefile b/regression/cbmc-incr-smt2/Makefile index 603200de746..a5e36136c30 100644 --- a/regression/cbmc-incr-smt2/Makefile +++ b/regression/cbmc-incr-smt2/Makefile @@ -9,8 +9,13 @@ else exclude_broken_windows_tests= endif -test: - @../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation --slice-formula" $(exclude_broken_windows_tests) +test: test.z3 test.cvc5 + +test.z3: + @../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation --slice-formula" $(exclude_broken_windows_tests) + +test.cvc5: + @../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation --slice-formula" $(exclude_broken_windows_tests) tests.log: ../test.pl test From fbd7662aa9a04e371b7c96843622cd1399214b1b Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Mon, 4 Apr 2022 14:34:37 +0100 Subject: [PATCH 3/3] Add missing cvc-5 download step from Ubuntu-18.04 package building job. --- .github/workflows/pull-request-checks.yaml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index 7ccd3142784..7d8faeeb126 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -634,6 +634,12 @@ jobs: sudo apt-get install -y --allow-downgrades --reinstall gcc g++ libgcc-s1- libstdc++6=$target liblsan0=$target libtsan0=$target libcc1-0=$target libgcc1=1:$target gdb=8.1.1-0ubuntu1 - name: Confirm z3 solver is available and log the version installed run: z3 --version + - name: Download cvc-5 from the releases page and make sure it can be deployed + run: | + wget -O cvc5 https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux + chmod u+x cvc5 + mv cvc5 /usr/local/bin + cvc5 --version - name: Prepare ccache uses: actions/cache@v2 with: