diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index fe9f7edb259..94a8e90de84 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -698,13 +698,22 @@ jobs: - name: Fetch dependencies run: | sudo apt-get update - sudo apt-get install --no-install-recommends -y g++ gdb flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache z3 + sudo apt-get install --no-install-recommends -y g++ gdb flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache # remove libgcc-s1, which isn't normally available in Ubuntu 18.04 target=$(dpkg-query -W --showformat='${Version}\n' gcc-8-base | head -n 1) # libgcc1 uses an epoch, thus the extra 1: 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 z3 4.11.0 from the python wheel package, extract it and make sure it can be deployed + run: | + sudo apt-get install --no-install-recommends -y unzip + # download the z3 python wheel package + wget -O z3.4.11.0.whl https://github.com/Z3Prover/z3/releases/download/z3-4.11.0/z3_solver-4.11.0.0-py2.py3-none-manylinux1_x86_64.whl + # unpack the bundle using python + unzip z3.4.11.0.whl + # make z3 executable and move it in /usr/local/bin + chmod u+x ./z3_solver-4.11.0.0.data/data/bin/z3 + mv ./z3_solver-4.11.0.0.data/data/bin/z3 /usr/local/bin/ + 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 diff --git a/regression/cbmc-incr-smt2/arrays/array_of.c b/regression/cbmc-incr-smt2/arrays/array_of.c new file mode 100644 index 00000000000..9db909d4fda --- /dev/null +++ b/regression/cbmc-incr-smt2/arrays/array_of.c @@ -0,0 +1,12 @@ +int main() +{ + int example_array[10000]; + unsigned int index; + __CPROVER_assume(index < 999); + + __CPROVER_array_set(example_array, 43); + __CPROVER_assert(example_array[index] != 43, "False array condition"); + + __CPROVER_array_set(example_array, 42); + __CPROVER_assert(example_array[index] == 42, "Valid array condition"); +} diff --git a/regression/cbmc-incr-smt2/arrays/array_of.desc b/regression/cbmc-incr-smt2/arrays/array_of.desc new file mode 100644 index 00000000000..03c974c3464 --- /dev/null +++ b/regression/cbmc-incr-smt2/arrays/array_of.desc @@ -0,0 +1,13 @@ +CORE +array_of.c + +Passing problem to incremental SMT2 solving +line \d+ False array condition: FAILURE +line \d+ Valid array condition: SUCCESS +^EXIT=10$ +^SIGNAL=0$ +-- +-- +Test using __CPROVER_array_set consisting in an `array_of` node which sets all values of a given +array to a given value. +This test uses a forall SMT statement. 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 b0c4446f43e..e3558754414 100644 --- a/regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc +++ b/regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc @@ -3,7 +3,7 @@ control_flow.c --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_AUFBV\) +Sending command to SMT2 solver - \(set-logic ALL\) Sending command to SMT2 solver - \(declare-fun |goto_symex::&92;guard#1| \(\) Bool\) Sending command to SMT2 solver - \(define-fun |B1| \(\) Bool |goto_symex::&92;guard#1|\) Sending command to SMT2 solver - \(declare-fun |main::1::x!0@1#1| \(\) \(_ BitVec 32\)\) 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 23a11981adf..3baacbdd299 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 @@ -3,7 +3,7 @@ test.c --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_AUFBV\) +Sending command to SMT2 solver - \(set-logic ALL\) Sending command to SMT2 solver - \(define-fun |B0| \(\) Bool true\) Sending command to SMT2 solver - \(declare-fun |main::1::x!0@1#1| \(\) \(_ BitVec 32\)\) Sending command to SMT2 solver - \(define-fun |B1| \(\) Bool \(|=| |main::1::x!0@1#1| |main::1::x!0@1#1|\)\) diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index e9579e3b797..9e706da4bb0 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -906,8 +906,10 @@ static smt_termt convert_expr_to_smt( const array_of_exprt &array_of, const sub_expression_mapt &converted) { - UNIMPLEMENTED_FEATURE( - "Generation of SMT formula for array of expression: " + array_of.pretty()); + // This function is unreachable as the `array_of_exprt` nodes are already + // fully converted by the incremental decision procedure functions + // (smt2_incremental_decision_proceduret::define_array_function). + UNHANDLED_CASE; } static smt_termt convert_expr_to_smt( @@ -1353,9 +1355,10 @@ static smt_termt convert_expr_to_smt( const array_exprt &array_construction, const sub_expression_mapt &converted) { - UNIMPLEMENTED_FEATURE( - "Generation of SMT formula for array construction expression: " + - array_construction.pretty()); + // This function is unreachable as the `array_exprt` nodes are already fully + // converted by the incremental decision procedure functions + // (smt2_incremental_decision_proceduret::define_array_function). + UNHANDLED_CASE; } static smt_termt convert_expr_to_smt( diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index a12af74f896..4d6a1241a58 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -71,6 +71,7 @@ static std::vector gather_dependent_expressions(const exprt &expr) if( can_cast_expr(expr_node) || can_cast_expr(expr_node) || + can_cast_expr(expr_node) || can_cast_expr(expr_node)) { dependent_expressions.push_back(expr_node); @@ -79,17 +80,10 @@ static std::vector gather_dependent_expressions(const exprt &expr) return dependent_expressions; } -void smt2_incremental_decision_proceduret::define_array_function( - const array_exprt &array) +void smt2_incremental_decision_proceduret::initialize_array_elements( + const array_exprt &array, + const smt_identifier_termt &array_identifier) { - const smt_sortt array_sort = convert_type_to_smt_sort(array.type()); - INVARIANT( - array_sort.cast(), - "Converting array typed expression to SMT should result in a term of array " - "sort."); - const smt_identifier_termt array_identifier = smt_identifier_termt{ - "array_" + std::to_string(array_sequence()), array_sort}; - solver_process->send(smt_declare_function_commandt{array_identifier, {}}); const std::vector &elements = array.operands(); const typet &index_type = array.type().index_type(); for(std::size_t i = 0; i < elements.size(); ++i) @@ -100,6 +94,39 @@ void smt2_incremental_decision_proceduret::define_array_function( convert_expr_to_smt(elements.at(i)))}; solver_process->send(element_definition); } +} + +void smt2_incremental_decision_proceduret::initialize_array_elements( + const array_of_exprt &array, + const smt_identifier_termt &array_identifier) +{ + const smt_sortt index_type = + convert_type_to_smt_sort(array.type().index_type()); + const smt_identifier_termt array_index_identifier{ + id2string(array_identifier.identifier()) + "_index", index_type}; + const smt_termt element_value = convert_expr_to_smt(array.what()); + + const smt_assert_commandt elements_definition{smt_forall_termt{ + {array_index_identifier}, + smt_core_theoryt::equal( + smt_array_theoryt::select(array_identifier, array_index_identifier), + element_value)}}; + solver_process->send(elements_definition); +} + +template +void smt2_incremental_decision_proceduret::define_array_function( + const t_exprt &array) +{ + const smt_sortt array_sort = convert_type_to_smt_sort(array.type()); + INVARIANT( + array_sort.cast(), + "Converting array typed expression to SMT should result in a term of array " + "sort."); + const smt_identifier_termt array_identifier{ + "array_" + std::to_string(array_sequence()), array_sort}; + solver_process->send(smt_declare_function_commandt{array_identifier, {}}); + initialize_array_elements(array, array_identifier); expression_identifiers.emplace(array, array_identifier); } @@ -168,9 +195,14 @@ void smt2_incremental_decision_proceduret::define_dependent_functions( solver_process->send(function); } } - if(const auto array_expr = expr_try_dynamic_cast(current)) + else if(const auto array_expr = expr_try_dynamic_cast(current)) define_array_function(*array_expr); - if( + else if( + const auto array_of_expr = expr_try_dynamic_cast(current)) + { + define_array_function(*array_of_expr); + } + else if( const auto nondet_symbol = expr_try_dynamic_cast(current)) { @@ -213,8 +245,7 @@ smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret( { solver_process->send( smt_set_option_commandt{smt_option_produce_modelst{true}}); - solver_process->send(smt_set_logic_commandt{ - smt_logic_quantifier_free_arrays_uninterpreted_functions_bit_vectorst{}}); + solver_process->send(smt_set_logic_commandt{smt_logic_allt{}}); solver_process->send(object_size_function.declaration); } diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h index 23b50799a5b..f89fee0b8ab 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h @@ -55,11 +55,29 @@ class smt2_incremental_decision_proceduret final protected: // Implementation of protected decision_proceduret member function. resultt dec_solve() override; - /// \brief Defines a function of array sort and asserts the element values. + /// \brief Defines a function of array sort and asserts the element values + /// from `array_exprt` or `array_of_exprt`. /// \details /// The new array function identifier is added to the /// `expression_identifiers` map. - void define_array_function(const array_exprt &array); + /// \note Statically fails if the template type is not a `array_exprt` or + /// `array_of_exprt`. + template + void define_array_function(const t_exprt &array); + /// \brief Generate and send to the SMT solver clauses asserting that each + /// array element is as specified by \p array. + void initialize_array_elements( + const array_exprt &array, + const smt_identifier_termt &array_identifier); + /// \brief Generate and send to the SMT solver clauses asserting that each + /// array element is as specified by \p array. + /// \note This function uses a forall SMT2 term. Using it in combination with + /// arrays, bit vectors and uninterpreted functions requires the `ALL` SMT + /// logic that is not in the SMT 2.6 standard, but that it has been tested + /// working on Z3 and CVC5. + void initialize_array_elements( + const array_of_exprt &array, + const smt_identifier_termt &array_identifier); /// \brief Defines any functions which \p expr depends on, which have not yet /// been defined, along with their dependencies in turn. void define_dependent_functions(const exprt &expr); diff --git a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index a06c8e77ee7..a5e5c564edc 100644 --- a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -171,9 +171,7 @@ TEST_CASE( test.sent_commands == std::vector{ smt_set_option_commandt{smt_option_produce_modelst{true}}, - smt_set_logic_commandt{ - // NOLINTNEXTLINE(whitespace/line_length) - smt_logic_quantifier_free_arrays_uninterpreted_functions_bit_vectorst{}}, + smt_set_logic_commandt{smt_logic_allt{}}, test.object_size_function.declaration}); test.sent_commands.clear(); SECTION("Set symbol to true.") @@ -615,5 +613,36 @@ TEST_CASE( smt_declare_function_commandt{index_term, {}}, smt_assert_commandt{smt_core_theoryt::equal( foo_term, smt_array_theoryt::select(array_term, index_term))}}; + REQUIRE(test.sent_commands == expected_commands); + } + SECTION("array_of_exprt - all elements set to a given value") + { + const array_of_exprt array_of_expr{ + from_integer(42, value_type), array_type}; + test.sent_commands.clear(); + test.procedure.set_to( + equal_exprt{ + foo.symbol_expr(), index_exprt{array_of_expr, index.symbol_expr()}}, + true); + const auto foo_term = smt_identifier_termt{"foo", smt_bit_vector_sortt{8}}; + const auto array_term = smt_identifier_termt{ + "array_0", + smt_array_sortt{smt_bit_vector_sortt{32}, smt_bit_vector_sortt{8}}}; + const auto index_term = + smt_identifier_termt{"index", smt_bit_vector_sortt{32}}; + const auto forall_term = + smt_identifier_termt{"array_0_index", smt_bit_vector_sortt{32}}; + const std::vector expected_commands{ + smt_declare_function_commandt{foo_term, {}}, + smt_declare_function_commandt{array_term, {}}, + smt_assert_commandt{smt_forall_termt{ + {forall_term}, + smt_core_theoryt::equal( + smt_array_theoryt::select(array_term, forall_term), + smt_bit_vector_constant_termt{42, 8})}}, + smt_declare_function_commandt{index_term, {}}, + smt_assert_commandt{smt_core_theoryt::equal( + foo_term, smt_array_theoryt::select(array_term, index_term))}}; + REQUIRE(test.sent_commands == expected_commands); } }