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 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)