From 96113314ed5def41ecac63853f385eb4ce18e509 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 16 Jul 2025 10:00:51 +0000 Subject: [PATCH 1/3] CI: Make smt2_solver available to all regression tests We will want to use the solver for more than just selected CBMC regressions. --- .github/workflows/pull-request-checks.yaml | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index 547045d083c..08ab8093cb3 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -72,9 +72,10 @@ jobs: make TAGS="[!shouldfail]" -C jbmc/unit test IPASIR=$PWD/riss.git/riss - name: Run regression tests run: | + export PATH=$PATH:`pwd`/src/solvers make -C regression test-parallel JOBS=${{env.linux-vcpus}} LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss make -C regression/cbmc test-paths-lifo - env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2 + make -C regression/cbmc test-cprover-smt2 make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}} - name: Check cleanup run: | @@ -153,9 +154,10 @@ jobs: make TAGS="[!shouldfail]" -C jbmc/unit test - name: Run regression tests run: | + export PATH=$PATH:`pwd`/src/solvers make -C regression test-parallel JOBS=${{env.linux-vcpus}} make -C regression/cbmc test-paths-lifo - env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2 + make -C regression/cbmc test-cprover-smt2 make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}} # This job has been copied from the one above it, and modified to only build CBMC @@ -339,9 +341,10 @@ jobs: make TAGS="[!shouldfail]" -C jbmc/unit test - name: Run regression tests run: | + export PATH=$PATH:`pwd`/src/solvers make -C regression test-parallel JOBS=${{env.linux-vcpus}} make -C regression/cbmc test-paths-lifo - env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2 + make -C regression/cbmc test-cprover-smt2 make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}} # This job takes approximately 17 to 41 minutes @@ -689,7 +692,9 @@ jobs: - name: Run JBMC unit tests run: cd jbmc/unit; ./unit_tests - name: Run regression tests - run: make -C regression test-parallel JOBS=4 + run: | + export PATH=$PATH:`pwd`/src/solvers + make -C regression test-parallel JOBS=4 - name: Run JBMC regression tests run: make -C jbmc/regression test-parallel JOBS=4 @@ -855,7 +860,9 @@ jobs: - name: Download minisat with make run: make -C src minisat2-download - name: Build CBMC with make - run: make CXX=clcache BUILD_ENV=MSVC -j${{env.windows-vcpus}} -C src + run: | + make CXX=clcache BUILD_ENV=MSVC -j${{env.windows-vcpus}} -C src + echo "$pwd\src\solvers;" >> $env:GITHUB_PATH - name: Build unit tests with make run: make CXX=clcache BUILD_ENV=MSVC -j${{env.windows-vcpus}} -C unit all - name: Build jbmc with make From 9a1df4bef208dc92104d7863d553b1cf9236c052 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 2 Jul 2025 13:40:18 +0200 Subject: [PATCH 2/3] SMT2 back-end: flatten with_exprt operands Solvers without datatypes support require flattening towards bitvectors. This is also true for array-typed expressions when the array is not at the top level (despite possible array-theory support). This changes makes sure we will flatten such array-typed expressions. --- regression/contracts-dfcc/CMakeLists.txt | 19 +++-- .../contracts-dfcc/array_struct_smt/main.c | 17 ++++ .../contracts-dfcc/array_struct_smt/test.desc | 12 +++ src/solvers/smt2/smt2_conv.cpp | 77 +++++++++++-------- 4 files changed, 86 insertions(+), 39 deletions(-) create mode 100644 regression/contracts-dfcc/array_struct_smt/main.c create mode 100644 regression/contracts-dfcc/array_struct_smt/test.desc diff --git a/regression/contracts-dfcc/CMakeLists.txt b/regression/contracts-dfcc/CMakeLists.txt index 872fdc9f247..e27d19fa289 100644 --- a/regression/contracts-dfcc/CMakeLists.txt +++ b/regression/contracts-dfcc/CMakeLists.txt @@ -41,10 +41,15 @@ add_test_pl_profile( #) # solver appears on the PATH in Windows already -#if(NOT "${CMAKE_SYSTEM_NAME}" STREQUAL "Windows") -# set_property( -# TEST "cbmc-cprover-smt2-CORE" -# PROPERTY ENVIRONMENT -# "PATH=$ENV{PATH}:$" -# ) -#endif() +if(NOT "${CMAKE_SYSTEM_NAME}" STREQUAL "Windows") + set_property( + TEST "contracts-dfcc-CORE" + PROPERTY ENVIRONMENT + "PATH=$ENV{PATH}:$" + ) + set_property( + TEST "contracts-non-dfcc-CORE" + PROPERTY ENVIRONMENT + "PATH=$ENV{PATH}:$" + ) +endif() diff --git a/regression/contracts-dfcc/array_struct_smt/main.c b/regression/contracts-dfcc/array_struct_smt/main.c new file mode 100644 index 00000000000..81f114fd838 --- /dev/null +++ b/regression/contracts-dfcc/array_struct_smt/main.c @@ -0,0 +1,17 @@ +typedef struct +{ + int coeffs[2]; +} mlk_poly; + +// clang-format off +void mlk_poly_add(mlk_poly *r, const mlk_poly *b) + __CPROVER_ensures(r->coeffs[0] == __CPROVER_old(*r).coeffs[0] + b->coeffs[0]) + __CPROVER_assigns(__CPROVER_object_upto(r, sizeof(mlk_poly))); +// clang-format on + +int main() +{ + mlk_poly r[1]; + mlk_poly b[1]; + mlk_poly_add(&r[0], &b[0]); +} diff --git a/regression/contracts-dfcc/array_struct_smt/test.desc b/regression/contracts-dfcc/array_struct_smt/test.desc new file mode 100644 index 00000000000..44e2363660d --- /dev/null +++ b/regression/contracts-dfcc/array_struct_smt/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--dfcc main --replace-call-with-contract mlk_poly_add _ --no-array-field-sensitivity --cprover-smt2 +^\[mlk_poly_add.overflow.1\] line 8 arithmetic overflow on signed \+ +^\*\* 1 of \d+ failed +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +Make sure the SMT back-end produces valid SMT2 when structs and arrays are +nested in each other. diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 3eb0204573a..92fd79459b2 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -4400,50 +4400,63 @@ void smt2_convt::convert_with(const with_exprt &expr) } else { + auto convert_operand = [this](const exprt &op) + { + // may need to flatten array-theory arrays in there + if(op.type().id() == ID_array && use_array_theory(op)) + flatten_array(op); + else if(op.type().id() == ID_bool) + flatten2bv(op); + else + convert_expr(op); + }; + std::size_t struct_width=boolbv_width(struct_type); // figure out the offset and width of the member const boolbv_widtht::membert &m = boolbv_width.get_member(struct_type, component_name); - out << "(let ((?withop "; - convert_expr(expr.old()); - out << ")) "; - if(m.width==struct_width) { - // the struct is the same as the member, no concat needed, - // ?withop won't be used - convert_expr(value); - } - else if(m.offset==0) - { - // the member is at the beginning - out << "(concat " - << "((_ extract " << (struct_width-1) << " " - << m.width << ") ?withop) "; - convert_expr(value); - out << ")"; // concat - } - else if(m.offset+m.width==struct_width) - { - // the member is at the end - out << "(concat "; - convert_expr(value); - out << " ((_ extract " << (m.offset - 1) << " 0) ?withop))"; + // the struct is the same as the member, no concat needed + convert_operand(value); } else { - // most general case, need two concat-s - out << "(concat (concat " - << "((_ extract " << (struct_width-1) << " " - << (m.offset+m.width) << ") ?withop) "; - convert_expr(value); - out << ") ((_ extract " << (m.offset-1) << " 0) ?withop)"; - out << ")"; // concat - } + out << "(let ((?withop "; + convert_operand(expr.old()); + out << ")) "; + + if(m.offset == 0) + { + // the member is at the beginning + out << "(concat " + << "((_ extract " << (struct_width - 1) << " " << m.width + << ") ?withop) "; + convert_operand(value); + out << ")"; // concat + } + else if(m.offset + m.width == struct_width) + { + // the member is at the end + out << "(concat "; + convert_operand(value); + out << " ((_ extract " << (m.offset - 1) << " 0) ?withop))"; + } + else + { + // most general case, need two concat-s + out << "(concat (concat " + << "((_ extract " << (struct_width - 1) << " " + << (m.offset + m.width) << ") ?withop) "; + convert_operand(value); + out << ") ((_ extract " << (m.offset - 1) << " 0) ?withop)"; + out << ")"; // concat + } - out << ")"; // let ?withop + out << ")"; // let ?withop + } } } else if(expr_type.id() == ID_union || expr_type.id() == ID_union_tag) From 769f7a22dc0161afd3209d681fd8bf161d983fee Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 23 Jul 2025 10:44:05 +0000 Subject: [PATCH 3/3] SMT2 back-end: ite-conversion must uphold type consistency WITH expressions in an ite expression could previously trigger one-sided expression flattening. --- .../contracts-dfcc/array_struct_smt-02/main.c | 24 +++++++++++++++ .../array_struct_smt-02/test.desc | 10 +++++++ src/solvers/smt2/smt2_conv.cpp | 30 +++++++++++++++++-- 3 files changed, 62 insertions(+), 2 deletions(-) create mode 100644 regression/contracts-dfcc/array_struct_smt-02/main.c create mode 100644 regression/contracts-dfcc/array_struct_smt-02/test.desc diff --git a/regression/contracts-dfcc/array_struct_smt-02/main.c b/regression/contracts-dfcc/array_struct_smt-02/main.c new file mode 100644 index 00000000000..e8b5a028c91 --- /dev/null +++ b/regression/contracts-dfcc/array_struct_smt-02/main.c @@ -0,0 +1,24 @@ +typedef struct +{ + int coeffs[1]; +} mld_poly; + +typedef struct +{ + mld_poly vec[1]; +} mld_polyveck; + +int main() +{ + mld_polyveck h; + + // clang-format off + for(unsigned int i = 0; i < 1; ++i) + __CPROVER_loop_invariant(i <= 1) + { + h.vec[i].coeffs[0] = 1; + } + // clang-format on + + return 0; +} diff --git a/regression/contracts-dfcc/array_struct_smt-02/test.desc b/regression/contracts-dfcc/array_struct_smt-02/test.desc new file mode 100644 index 00000000000..43568980840 --- /dev/null +++ b/regression/contracts-dfcc/array_struct_smt-02/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--dfcc main --apply-loop-contracts _ --cprover-smt2 +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +Make sure the SMT back-end produces valid SMT2 when structs and arrays are +nested in each other. diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 92fd79459b2..80a9b973847 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -1407,9 +1407,35 @@ void smt2_convt::convert_expr(const exprt &expr) out << "(ite "; convert_expr(if_expr.cond()); out << " "; - convert_expr(if_expr.true_case()); + if( + expr.type().id() == ID_array && !use_array_theory(if_expr.true_case()) && + use_array_theory(if_expr.false_case())) + { + unflatten(wheret::BEGIN, expr.type()); + + convert_expr(if_expr.true_case()); + + unflatten(wheret::END, expr.type()); + } + else + { + convert_expr(if_expr.true_case()); + } out << " "; - convert_expr(if_expr.false_case()); + if( + expr.type().id() == ID_array && use_array_theory(if_expr.true_case()) && + !use_array_theory(if_expr.false_case())) + { + unflatten(wheret::BEGIN, expr.type()); + + convert_expr(if_expr.false_case()); + + unflatten(wheret::END, expr.type()); + } + else + { + convert_expr(if_expr.false_case()); + } out << ")"; } else if(expr.id()==ID_and ||