From bb590f6bd0f2c9b3241c7c494b43c16ef104360e Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Thu, 30 Jun 2022 19:21:49 +0100 Subject: [PATCH 1/3] Add array_exprt to smt conversion --- .../smt2_incremental_decision_procedure.cpp | 61 +++++++++++++++++-- .../smt2_incremental_decision_procedure.h | 7 ++- .../smt2_incremental_decision_procedure.cpp | 43 +++++++++++++ 3 files changed, 106 insertions(+), 5 deletions(-) diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index f47a547e51c..0e4e5594db0 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -12,6 +12,7 @@ #include #include +#include #include #include #include @@ -64,7 +65,9 @@ static std::vector gather_dependent_expressions(const exprt &expr) { std::vector dependent_expressions; expr.visit_pre([&](const exprt &expr_node) { - if(can_cast_expr(expr_node)) + if( + can_cast_expr(expr_node) || + can_cast_expr(expr_node)) { dependent_expressions.push_back(expr_node); } @@ -72,6 +75,32 @@ static std::vector gather_dependent_expressions(const exprt &expr) return dependent_expressions; } +void smt2_incremental_decision_proceduret::define_array_function( + const array_exprt &array) +{ + const auto array_sort = + convert_type_to_smt_sort(array.type()).cast(); + INVARIANT( + array_sort, + "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 std::size_t index_width = + array_sort->index_sort().cast()->bit_width(); + for(std::size_t i = 0; i < elements.size(); ++i) + { + const smt_assert_commandt element_definition{smt_core_theoryt::equal( + smt_array_theoryt::select( + array_identifier, smt_bit_vector_constant_termt{i, index_width}), + convert_expr_to_smt(elements.at(i)))}; + solver_process->send(element_definition); + } + expression_identifiers.emplace(array, array_identifier); +} + /// \brief Defines any functions which \p expr depends on, which have not yet /// been defined, along with their dependencies in turn. void smt2_incremental_decision_proceduret::define_dependent_functions( @@ -123,10 +152,29 @@ void smt2_incremental_decision_proceduret::define_dependent_functions( solver_process->send(function); } } + if(const auto array_expr = expr_try_dynamic_cast(current)) + define_array_function(*array_expr); to_be_defined.pop(); } } +/// Replaces the sub expressions of \p expr which have been defined as separate +/// functions in the smt solver, using the \p expression_identifiers map. +static exprt substitute_identifiers( + exprt expr, + const std::unordered_map + &expression_identifiers) +{ + expr.visit_pre([&](exprt &node) -> void { + auto find_result = expression_identifiers.find(node); + if(find_result == expression_identifiers.cend()) + return; + const auto type = find_result->first.type(); + node = symbol_exprt{find_result->second.identifier(), type}; + }); + return expr; +} + smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret( const namespacet &_ns, std::unique_ptr _solver_process, @@ -164,15 +212,20 @@ void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined( smt_termt smt2_incremental_decision_proceduret::convert_expr_to_smt(const exprt &expr) { - track_expression_objects(expr, ns, object_map); + const exprt substituted = + substitute_identifiers(expr, expression_identifiers); + track_expression_objects(substituted, ns, object_map); associate_pointer_sizes( - expr, + substituted, ns, pointer_sizes_map, object_map, object_size_function.make_application); return ::convert_expr_to_smt( - expr, object_map, pointer_sizes_map, object_size_function.make_application); + substituted, + object_map, + pointer_sizes_map, + object_size_function.make_application); } exprt smt2_incremental_decision_proceduret::handle(const exprt &expr) diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h index 4cba084c631..727dc9fe0ad 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h @@ -55,6 +55,11 @@ 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. + /// \details + /// The new array function identifier is added to the + /// `expression_identifiers` map. + void define_array_function(const array_exprt &array); /// \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); @@ -81,7 +86,7 @@ class smt2_incremental_decision_proceduret final { return next_id++; } - } handle_sequence; + } handle_sequence, array_sequence; std::unordered_map expression_handle_identifiers; diff --git a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index c673c42a6c7..70c267e3d6a 100644 --- a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -9,6 +9,7 @@ #include #include +#include #include #include #include @@ -517,3 +518,45 @@ TEST_CASE( } } } + +TEST_CASE( + "smt2_incremental_decision_proceduret array commands.", + "[core][smt2_incremental]") +{ + auto test = decision_procedure_test_environmentt::make(); + const auto index_type = signedbv_typet{32}; + const symbolt index = make_test_symbol("index", index_type); + const auto value_type = signedbv_typet{8}; + const symbolt foo = make_test_symbol("foo", value_type); + const auto array_type = array_typet{value_type, from_integer(2, index_type)}; + SECTION("array_exprt - list of literal array elements") + { + const array_exprt array_literal{ + {from_integer(9, value_type), from_integer(12, value_type)}, array_type}; + test.sent_commands.clear(); + test.procedure.set_to( + equal_exprt{ + foo.symbol_expr(), index_exprt{array_literal, 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 std::vector expected_commands{ + smt_declare_function_commandt{foo_term, {}}, + smt_declare_function_commandt{array_term, {}}, + smt_assert_commandt{smt_core_theoryt::equal( + smt_array_theoryt::select( + array_term, smt_bit_vector_constant_termt{0, 32}), + smt_bit_vector_constant_termt{9, 8})}, + smt_assert_commandt{smt_core_theoryt::equal( + smt_array_theoryt::select( + array_term, smt_bit_vector_constant_termt{1, 32}), + smt_bit_vector_constant_termt{12, 8})}, + smt_declare_function_commandt{index_term, {}}, + smt_assert_commandt{smt_core_theoryt::equal( + foo_term, smt_array_theoryt::select(array_term, index_term))}}; + } +} From 010090bfe0dc90b3a794cd21643e224a201b4d9d Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 5 Jul 2022 11:57:10 +0100 Subject: [PATCH 2/3] Add regression test --- regression/cbmc-incr-smt2/arrays/array_literal.c | 13 +++++++++++++ .../cbmc-incr-smt2/arrays/array_literal.desc | 16 ++++++++++++++++ 2 files changed, 29 insertions(+) create mode 100644 regression/cbmc-incr-smt2/arrays/array_literal.c create mode 100644 regression/cbmc-incr-smt2/arrays/array_literal.desc diff --git a/regression/cbmc-incr-smt2/arrays/array_literal.c b/regression/cbmc-incr-smt2/arrays/array_literal.c new file mode 100644 index 00000000000..a041b566f2b --- /dev/null +++ b/regression/cbmc-incr-smt2/arrays/array_literal.c @@ -0,0 +1,13 @@ +int main() +{ + int example_array[] = {5, 4, 3, 2, 1}; + unsigned int index; + __CPROVER_assume(index < 5); + __CPROVER_assert(example_array[index] != 42, "Non-existent element"); + __CPROVER_assert(example_array[index] != 5, "Index 0"); + __CPROVER_assert(example_array[index] != 4, "Index 1"); + __CPROVER_assert(example_array[index] != 3, "Index 2"); + __CPROVER_assert(example_array[index] != 2, "Index 3"); + __CPROVER_assert(example_array[index] != 1, "Index 4"); + __CPROVER_assert(example_array[index] == 5 - index, "Index value relation"); +} diff --git a/regression/cbmc-incr-smt2/arrays/array_literal.desc b/regression/cbmc-incr-smt2/arrays/array_literal.desc new file mode 100644 index 00000000000..fd734db215d --- /dev/null +++ b/regression/cbmc-incr-smt2/arrays/array_literal.desc @@ -0,0 +1,16 @@ +CORE +array_literal.c + +Passing problem to incremental SMT2 solving +line \d+ Non-existent element: SUCCESS +line \d+ Index 0: FAILURE +line \d+ Index 1: FAILURE +line \d+ Index 2: FAILURE +line \d+ Index 3: FAILURE +line \d+ Index 4: FAILURE +line \d+ Index value relation: SUCCESS +^EXIT=10$ +^SIGNAL=0$ +-- +-- +Test of reading an array which is initialised using an array literal. From 4d5d52915aa6ff9c07899aed07b8a2fdb1ea2afe Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Mon, 11 Jul 2022 14:11:04 +0100 Subject: [PATCH 3/3] Avoid assuming that converted arrays have bit vector indices This means that there will be fewer changes required if we ever change the encoding of arrays such that they do not have a bit vector sorted index. It also means that there is no need to add an invariant for this previously implicitly assumed property. --- .../smt2_incremental_decision_procedure.cpp | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index 0e4e5594db0..87885a25622 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -2,6 +2,7 @@ #include "smt2_incremental_decision_procedure.h" +#include #include #include #include @@ -78,23 +79,21 @@ static std::vector gather_dependent_expressions(const exprt &expr) void smt2_incremental_decision_proceduret::define_array_function( const array_exprt &array) { - const auto array_sort = - convert_type_to_smt_sort(array.type()).cast(); + const smt_sortt array_sort = convert_type_to_smt_sort(array.type()); INVARIANT( - array_sort, + 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}; + "array_" + std::to_string(array_sequence()), array_sort}; solver_process->send(smt_declare_function_commandt{array_identifier, {}}); const std::vector &elements = array.operands(); - const std::size_t index_width = - array_sort->index_sort().cast()->bit_width(); + const typet &index_type = array.type().index_type(); for(std::size_t i = 0; i < elements.size(); ++i) { + const smt_termt index = convert_expr_to_smt(from_integer(i, index_type)); const smt_assert_commandt element_definition{smt_core_theoryt::equal( - smt_array_theoryt::select( - array_identifier, smt_bit_vector_constant_termt{i, index_width}), + smt_array_theoryt::select(array_identifier, index), convert_expr_to_smt(elements.at(i)))}; solver_process->send(element_definition); }