From 48790512ed3f92140240fc1d742ce0988cb1db39 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Thu, 7 Apr 2022 19:51:20 +0100 Subject: [PATCH 1/7] Add conversion of null pointer to smt terms --- .../smt2_incremental/convert_expr_to_smt.cpp | 10 ++++++++++ .../smt2_incremental/convert_expr_to_smt.cpp | 18 ++++++++++++++++++ 2 files changed, 28 insertions(+) diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index 8406b464d37..cba9c585faf 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -6,6 +6,7 @@ #include #include #include +#include #include #include #include @@ -268,6 +269,15 @@ struct sort_based_literal_convertert : public smt_sort_const_downcast_visitort static smt_termt convert_expr_to_smt(const constant_exprt &constant_literal) { + if(is_null_pointer(constant_literal)) + { + const size_t bit_width = + type_checked_cast(constant_literal.type()).get_width(); + // An address of 0 encodes an object identifier of 0 for the NULL object + // and an offset of 0 into the object. + const auto address = 0; + return smt_bit_vector_constant_termt{address, bit_width}; + } const auto sort = convert_type_to_smt_sort(constant_literal.type()); sort_based_literal_convertert converter(constant_literal); sort.accept(converter); diff --git a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp index 3b7393f5ce5..d29fde45243 100644 --- a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -66,6 +66,24 @@ TEST_CASE( convert_expr_to_smt(from_integer({-1}, signedbv_typet{16})) == smt_bit_vector_constant_termt{65535, 16}); } + SECTION("Null pointer") + { + // These config lines are necessary because pointer widths depend on the + // configuration. + config.ansi_c.mode = configt::ansi_ct::flavourt::GCC; + config.ansi_c.set_arch_spec_i386(); + const smt_termt null_pointer_term = + smt_bit_vector_constant_termt{0, config.ansi_c.pointer_width}; + CHECK( + convert_expr_to_smt(null_pointer_exprt{pointer_type(void_type())}) == + null_pointer_term); + CHECK( + convert_expr_to_smt(null_pointer_exprt{ + pointer_type(unsignedbv_typet{100})}) == null_pointer_term); + CHECK( + convert_expr_to_smt(null_pointer_exprt{ + pointer_type(pointer_type(void_type()))}) == null_pointer_term); + } } TEST_CASE( From 79766cb3916bd91cf0fa363cc510a39dae8f6870 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Thu, 7 Apr 2022 19:51:21 +0100 Subject: [PATCH 2/7] Add object tracking --- src/solvers/Makefile | 1 + .../smt2_incremental/object_tracking.cpp | 88 +++++++++++++++ .../smt2_incremental/object_tracking.h | 90 ++++++++++++++++ unit/Makefile | 1 + .../smt2_incremental/object_tracking.cpp | 101 ++++++++++++++++++ 5 files changed, 281 insertions(+) create mode 100644 src/solvers/smt2_incremental/object_tracking.cpp create mode 100644 src/solvers/smt2_incremental/object_tracking.h create mode 100644 unit/solvers/smt2_incremental/object_tracking.cpp diff --git a/src/solvers/Makefile b/src/solvers/Makefile index d44caf4c234..ded67c8d273 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -195,6 +195,7 @@ SRC = $(BOOLEFORCE_SRC) \ smt2/smt2irep.cpp \ smt2_incremental/construct_value_expr_from_smt.cpp \ smt2_incremental/convert_expr_to_smt.cpp \ + smt2_incremental/object_tracking.cpp \ smt2_incremental/smt_bit_vector_theory.cpp \ smt2_incremental/smt_commands.cpp \ smt2_incremental/smt_core_theory.cpp \ diff --git a/src/solvers/smt2_incremental/object_tracking.cpp b/src/solvers/smt2_incremental/object_tracking.cpp new file mode 100644 index 00000000000..00e14808d2b --- /dev/null +++ b/src/solvers/smt2_incremental/object_tracking.cpp @@ -0,0 +1,88 @@ +// Author: Diffblue Ltd. + +#include "object_tracking.h" + +#include +#include +#include +#include +#include + +exprt find_object_base_expression(const address_of_exprt &address_of) +{ + auto current = std::ref(address_of.object()); + while( + !(can_cast_expr(current) || + can_cast_expr(current) || + can_cast_expr(current) || + can_cast_expr(current))) + { + if(const auto index = expr_try_dynamic_cast(current.get())) + { + // For the case `my_array[bar]` the base expression is `my_array`. + current = index->array(); + continue; + } + if(const auto member = expr_try_dynamic_cast(current.get())) + { + // For the case `my_struct.field_name` the base expression is `my_struct`. + current = member->compound(); + continue; + } + INVARIANT( + false, + "Unable to find base object of expression: " + + current.get().pretty(1, 0)); + } + return current.get(); +} + +static decision_procedure_objectt make_null_object() +{ + decision_procedure_objectt null_object; + null_object.unique_id = 0; + null_object.base_expression = null_pointer_exprt{pointer_type(void_type())}; + return null_object; +} + +smt_object_mapt initial_smt_object_map() +{ + smt_object_mapt object_map; + decision_procedure_objectt null_object = make_null_object(); + exprt base = null_object.base_expression; + object_map.emplace(std::move(base), std::move(null_object)); + return object_map; +} + +void track_expression_objects( + const exprt &expression, + const namespacet &ns, + smt_object_mapt &object_map) +{ + find_object_base_expressions( + expression, [&](const exprt &object_base) -> void { + const auto find_result = object_map.find(object_base); + if(find_result != object_map.cend()) + return; + decision_procedure_objectt object; + object.base_expression = object_base; + object.unique_id = object_map.size(); + object.size = size_of_expr(object_base.type(), ns); + object_map.emplace_hint(find_result, object_base, std::move(object)); + }); +} + +bool objects_are_already_tracked( + const exprt &expression, + const smt_object_mapt &object_map) +{ + bool all_objects_tracked = true; + find_object_base_expressions( + expression, [&](const exprt &object_base) -> void { + const auto find_result = object_map.find(object_base); + if(find_result != object_map.cend()) + return; + all_objects_tracked = false; + }); + return all_objects_tracked; +} diff --git a/src/solvers/smt2_incremental/object_tracking.h b/src/solvers/smt2_incremental/object_tracking.h new file mode 100644 index 00000000000..034547eac38 --- /dev/null +++ b/src/solvers/smt2_incremental/object_tracking.h @@ -0,0 +1,90 @@ +// Author: Diffblue Ltd. + +#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_OBJECT_TRACKING_H +#define CPROVER_SOLVERS_SMT2_INCREMENTAL_OBJECT_TRACKING_H + +#include +#include + +#include + +/// Information the decision procedure holds about each object. +struct decision_procedure_objectt +{ + /// The expression for the root of the object. This is expression equivalent + /// to deferencing a pointer to this object with a zero offset. + exprt base_expression; + /// Number which uniquely identifies this particular object. + std::size_t unique_id; + /// Expression which evaluates to the size of the object in bytes. + optionalt size; +}; + +/// The model of addresses we use consists of a unique object identifier and an +/// offset. In order to encode the offset identifiers we need to assign unique +/// identifiers to the objects. This function finds the base object expression +/// in an address of expression for which a unique identifier needs to be +/// assigned. +exprt find_object_base_expression(const address_of_exprt &address_of); + +/// Arbitary expressions passed to the decision procedure may have multiple +/// address of operations as its sub expressions. This means the overall +/// expression may contain multiple base objects which need to be assigned +/// unique identifiers. +/// \param expression +/// The expression within which to find base objects. +/// \param output_object +/// This function is called with each of the base object expressions found, as +/// they are found. +/// \details +/// The found objects are returned through an output function in order to +/// separate the implementation of the storage and deduplication of the +/// results from finding the object expressions. The type of \p output_object +/// is a template parameter in order to eliminate potential performance +/// overheads of using `std::function`. +template +void find_object_base_expressions( + const exprt &expression, + const output_object_functiont &output_object) +{ + expression.visit_pre([&](const exprt &node) { + if(const auto address_of = expr_try_dynamic_cast(node)) + { + output_object(find_object_base_expression(*address_of)); + } + }); +} + +/// Mapping from an object's base expression to the set of information about it +/// which we track. +using smt_object_mapt = + std::unordered_map; + +/// Constructs an initial object map containing the null object. The null object +/// must be added at construction in order to ensure it is allocated a unique +/// identifier of 0. +smt_object_mapt initial_smt_object_map(); + +/// \brief +/// Finds all the object expressions in the given expression and adds them to +/// the object map for cases where the map does not contain them already. +/// \param expression +/// The expression within which to find and base object expressions. +/// \param ns +/// The namespace used to look up the size of object types. +/// \param object_map +/// The map into which any new tracking information should be inserted. +void track_expression_objects( + const exprt &expression, + const namespacet &ns, + smt_object_mapt &object_map); + +/// Finds whether all base object expressions in the given expression are +/// already tracked in the given object map. This supports writing invariants +/// on the base object expressions already being tracked in the map in contexts +/// where the map is const. +bool objects_are_already_tracked( + const exprt &expression, + const smt_object_mapt &object_map); + +#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_OBJECT_TRACKING_H diff --git a/unit/Makefile b/unit/Makefile index 6259c418f96..5d241997937 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -102,6 +102,7 @@ SRC += analyses/ai/ai.cpp \ solvers/smt2/smt2irep.cpp \ solvers/smt2_incremental/construct_value_expr_from_smt.cpp \ solvers/smt2_incremental/convert_expr_to_smt.cpp \ + solvers/smt2_incremental/object_tracking.cpp \ solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp \ solvers/smt2_incremental/smt_bit_vector_theory.cpp \ solvers/smt2_incremental/smt_commands.cpp \ diff --git a/unit/solvers/smt2_incremental/object_tracking.cpp b/unit/solvers/smt2_incremental/object_tracking.cpp new file mode 100644 index 00000000000..8e640ae9a17 --- /dev/null +++ b/unit/solvers/smt2_incremental/object_tracking.cpp @@ -0,0 +1,101 @@ +// Author: Diffblue Ltd. + +#include +#include +#include +#include +#include + +#include +#include + +#include +#include + +TEST_CASE("find_object_base_expression", "[core][smt2_incremental]") +{ + const typet base_type = pointer_typet{unsignedbv_typet{8}, 18}; + const symbol_exprt object_base{"base", base_type}; + const symbol_exprt index{"index", base_type}; + const pointer_typet pointer_type{base_type, 12}; + std::string description; + optionalt address_of; + using rowt = std::pair; + std::tie(description, address_of) = GENERATE_REF( + rowt{"Address of symbol", {object_base, pointer_type}}, + rowt{"Address of index", {index_exprt{object_base, index}, pointer_type}}, + rowt{ + "Address of struct member", + {member_exprt{object_base, "baz", unsignedbv_typet{8}}, pointer_type}}, + rowt{ + "Address of index of struct member", + {index_exprt{ + member_exprt{object_base, "baz", unsignedbv_typet{8}}, index}, + pointer_type}}, + rowt{ + "Address of struct member at index", + {member_exprt{ + index_exprt{object_base, index}, "baz", unsignedbv_typet{8}}, + pointer_type}}); + SECTION(description) + { + CHECK(find_object_base_expression(*address_of) == object_base); + } +} + +TEST_CASE("Tracking object base expressions", "[core][smt2_incremental]") +{ + const typet base_type = pointer_typet{signedbv_typet{16}, 18}; + const symbol_exprt foo{"foo", base_type}; + const symbol_exprt bar{"bar", base_type}; + const symbol_exprt index{"index", base_type}; + const pointer_typet pointer_type{base_type, 32}; + const exprt bar_address = address_of_exprt{bar, pointer_type}; + const exprt compound_expression = and_exprt{ + equal_exprt{ + address_of_exprt{index_exprt{foo, index}, pointer_type}, bar_address}, + notequal_exprt{ + address_of_exprt{ + member_exprt{foo, "baz", unsignedbv_typet{8}}, pointer_type}, + bar_address}}; + SECTION("Find base expressions") + { + std::vector expressions; + find_object_base_expressions(compound_expression, [&](const exprt &expr) { + expressions.push_back(expr); + }); + CHECK(expressions == std::vector{bar, foo, bar, foo}); + } + smt_object_mapt object_map = initial_smt_object_map(); + SECTION("Check initial object map has null pointer") + { + REQUIRE(object_map.size() == 1); + const exprt null_pointer = null_pointer_exprt{::pointer_type(void_type())}; + CHECK(object_map.begin()->first == null_pointer); + CHECK(object_map.begin()->second.unique_id == 0); + CHECK(object_map.begin()->second.base_expression == null_pointer); + } + symbol_tablet symbol_table; + namespacet ns{symbol_table}; + SECTION("Check objects of compound expression not yet tracked") + { + CHECK_FALSE(objects_are_already_tracked(compound_expression, object_map)); + } + track_expression_objects(compound_expression, ns, object_map); + SECTION("Tracking expression objects") + { + CHECK(object_map.size() == 3); + const auto foo_object = object_map.find(foo); + REQUIRE(foo_object != object_map.end()); + CHECK(foo_object->second.base_expression == foo); + CHECK(foo_object->second.unique_id == 2); + const auto bar_object = object_map.find(bar); + REQUIRE(bar_object != object_map.end()); + CHECK(bar_object->second.base_expression == bar); + CHECK(bar_object->second.unique_id == 1); + } + SECTION("Confirming objects are tracked.") + { + CHECK(objects_are_already_tracked(compound_expression, object_map)); + } +} From 3a353a650df1ef2aa3aaebe2e273ee4da4cd9d4d Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Thu, 7 Apr 2022 19:51:22 +0100 Subject: [PATCH 3/7] Extend unit test of extract_bits conversion with integer bounds Because instances of this expression are constructed using integer bounds rather than bit vector bounds, as part of the left shift overflow checks. --- .../smt2_incremental/convert_expr_to_smt.cpp | 38 +++++++++++++------ 1 file changed, 26 insertions(+), 12 deletions(-) diff --git a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp index d29fde45243..3dc2a13e16b 100644 --- a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -920,20 +920,34 @@ TEST_CASE( "[core][smt2_incremental]") { const typet operand_type = unsignedbv_typet{8}; - const exprt input = extractbits_exprt{ - symbol_exprt{"foo", operand_type}, - from_integer(4, operand_type), - from_integer(2, operand_type), - unsignedbv_typet{3}}; + std::string description; + exprt input; + using rowt = std::pair; + std::tie(description, input) = GENERATE_REF( + rowt{ + "Bit vector typed bounds", + extractbits_exprt{ + symbol_exprt{"foo", operand_type}, + from_integer(4, operand_type), + from_integer(2, operand_type), + unsignedbv_typet{3}}}, + rowt{ + "Constant integer bounds", + extractbits_exprt{ + symbol_exprt{"foo", operand_type}, 4, 2, unsignedbv_typet{3}}}); const smt_termt expected_result = smt_bit_vector_theoryt::extract(4, 2)( smt_identifier_termt{"foo", smt_bit_vector_sortt{8}}); - CHECK(convert_expr_to_smt(input) == expected_result); - const cbmc_invariants_should_throwt invariants_throw; - CHECK_THROWS(convert_expr_to_smt(extractbits_exprt{ - symbol_exprt{"foo", operand_type}, - symbol_exprt{"bar", operand_type}, - symbol_exprt{"bar", operand_type}, - unsignedbv_typet{3}})); + SECTION(description) + { + INFO("Input expression - " + input.pretty(1, 0)); + CHECK(convert_expr_to_smt(input) == expected_result); + const cbmc_invariants_should_throwt invariants_throw; + CHECK_THROWS(convert_expr_to_smt(extractbits_exprt{ + symbol_exprt{"foo", operand_type}, + symbol_exprt{"bar", operand_type}, + symbol_exprt{"bar", operand_type}, + unsignedbv_typet{3}})); + } } TEST_CASE("expr to smt conversion for type casts", "[core][smt2_incremental]") From a0f253e77252c5c4d3b339e10c79a1e9bcd28bbb Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Thu, 7 Apr 2022 19:51:23 +0100 Subject: [PATCH 4/7] Add support for converting integer constants into bit vectors This is required for the following refactor because it requires all sub-expressions to be convertible to smt terms whereas the current implementation only requires sub expressions which are recursed into to be convertible. These integer constants which need converting can be found as sub expressions of extract bits expressions. --- src/solvers/smt2_incremental/convert_expr_to_smt.cpp | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index cba9c585faf..63dc3326321 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -278,6 +278,15 @@ static smt_termt convert_expr_to_smt(const constant_exprt &constant_literal) const auto address = 0; return smt_bit_vector_constant_termt{address, bit_width}; } + if(constant_literal.type() == integer_typet{}) + { + // This is converting integer constants into bit vectors for use with + // bit vector based smt logics. As bit vector widths are not specified for + // non bit vector types, this chooses a width based on the minimum needed + // to hold the integer constant value. + const auto value = numeric_cast_v(constant_literal); + return smt_bit_vector_constant_termt{value, address_bits(value + 1)}; + } const auto sort = convert_type_to_smt_sort(constant_literal.type()); sort_based_literal_convertert converter(constant_literal); sort.accept(converter); From eb2070a9907890348a991f8f5d84634483354229 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Thu, 7 Apr 2022 19:51:24 +0100 Subject: [PATCH 5/7] Refactor expr to smt term conversion to be non-recursive --- .../smt2_incremental/convert_expr_to_smt.cpp | 596 ++++++++++++------ 1 file changed, 401 insertions(+), 195 deletions(-) diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index 63dc3326321..e32cca707ee 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -23,9 +23,22 @@ #include #include +/// Post order visitation is used in order to construct the the smt terms bottom +/// upwards without using recursion to traverse the input `exprt`. Therefore +/// the `convert_expr_to_smt` overload for any given type of `exprt`, will +/// be passed a sub_expression_map which already contains the result of +/// converting that expressions operands to smt terms. This has the advantages +/// of - +/// * avoiding the deeply nested call stacks associated with recursion. +/// * supporting wider scope for the conversion of specific types of `exprt`, +/// without inflating the parameter list / scope for all conversions. +using sub_expression_mapt = + std::unordered_map; + /// \brief Converts operator expressions with 2 or more operands to terms /// expressed as binary operator application. /// \param expr: The expression to convert. +/// \param converted: Map for looking up previously converted sub expressions. /// \param factory: The factory function which makes applications of the /// relevant smt term, when applied to the term operands. /// \details The conversion used is left associative for instances with 3 or @@ -37,12 +50,13 @@ template static smt_termt convert_multiary_operator_to_terms( const multi_ary_exprt &expr, + const sub_expression_mapt &converted, const factoryt &factory) { PRECONDITION(expr.operands().size() >= 2); const auto operand_terms = - make_range(expr.operands()).map([](const exprt &expr) { - return convert_expr_to_smt(expr); + make_range(expr.operands()).map([&](const exprt &expr) { + return converted.at(expr); }); return std::accumulate( ++operand_terms.begin(), @@ -93,7 +107,9 @@ static smt_termt convert_expr_to_smt(const symbol_exprt &symbol_expr) convert_type_to_smt_sort(symbol_expr.type())}; } -static smt_termt convert_expr_to_smt(const nondet_symbol_exprt &nondet_symbol) +static smt_termt convert_expr_to_smt( + const nondet_symbol_exprt &nondet_symbol, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for nondet symbol expression: " + @@ -105,8 +121,12 @@ static smt_termt make_not_zero(const smt_termt &input, const typet &source_type) { if(input.get_sort().cast()) return input; - return smt_core_theoryt::distinct( - input, convert_expr_to_smt(from_integer(0, source_type))); + if(const auto bit_vector_sort = input.get_sort().cast()) + { + return smt_core_theoryt::distinct( + input, smt_bit_vector_constant_termt{0, *bit_vector_sort}); + } + UNREACHABLE; } /// \brief Returns a cast to C bool expressed in smt terms. @@ -206,9 +226,11 @@ static smt_termt convert_bit_vector_cast( return *converter.result; } -static smt_termt convert_expr_to_smt(const typecast_exprt &cast) +static smt_termt convert_expr_to_smt( + const typecast_exprt &cast, + const sub_expression_mapt &converted) { - const auto from_term = convert_expr_to_smt(cast.op()); + const auto &from_term = converted.at(cast.op()); const typet &from_type = cast.op().type(); const typet &to_type = cast.type(); if(const auto bool_type = type_try_dynamic_cast(to_type)) @@ -221,21 +243,27 @@ static smt_termt convert_expr_to_smt(const typecast_exprt &cast) "Generation of SMT formula for type cast expression: " + cast.pretty()); } -static smt_termt convert_expr_to_smt(const floatbv_typecast_exprt &float_cast) +static smt_termt convert_expr_to_smt( + const floatbv_typecast_exprt &float_cast, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for floating point type cast expression: " + float_cast.pretty()); } -static smt_termt convert_expr_to_smt(const struct_exprt &struct_construction) +static smt_termt convert_expr_to_smt( + const struct_exprt &struct_construction, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for struct construction expression: " + struct_construction.pretty()); } -static smt_termt convert_expr_to_smt(const union_exprt &union_construction) +static smt_termt convert_expr_to_smt( + const union_exprt &union_construction, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for union construction expression: " + @@ -293,19 +321,23 @@ static smt_termt convert_expr_to_smt(const constant_exprt &constant_literal) return *converter.result; } -static smt_termt convert_expr_to_smt(const concatenation_exprt &concatenation) +static smt_termt convert_expr_to_smt( + const concatenation_exprt &concatenation, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for concatenation expression: " + concatenation.pretty()); } -static smt_termt convert_expr_to_smt(const bitand_exprt &bitwise_and_expr) +static smt_termt convert_expr_to_smt( + const bitand_exprt &bitwise_and_expr, + const sub_expression_mapt &converted) { if(operands_are_of_type(bitwise_and_expr)) { return convert_multiary_operator_to_terms( - bitwise_and_expr, smt_bit_vector_theoryt::make_and); + bitwise_and_expr, converted, smt_bit_vector_theoryt::make_and); } else { @@ -315,12 +347,14 @@ static smt_termt convert_expr_to_smt(const bitand_exprt &bitwise_and_expr) } } -static smt_termt convert_expr_to_smt(const bitor_exprt &bitwise_or_expr) +static smt_termt convert_expr_to_smt( + const bitor_exprt &bitwise_or_expr, + const sub_expression_mapt &converted) { if(operands_are_of_type(bitwise_or_expr)) { return convert_multiary_operator_to_terms( - bitwise_or_expr, smt_bit_vector_theoryt::make_or); + bitwise_or_expr, converted, smt_bit_vector_theoryt::make_or); } else { @@ -330,12 +364,14 @@ static smt_termt convert_expr_to_smt(const bitor_exprt &bitwise_or_expr) } } -static smt_termt convert_expr_to_smt(const bitxor_exprt &bitwise_xor) +static smt_termt convert_expr_to_smt( + const bitxor_exprt &bitwise_xor, + const sub_expression_mapt &converted) { if(operands_are_of_type(bitwise_xor)) { return convert_multiary_operator_to_terms( - bitwise_xor, smt_bit_vector_theoryt::make_xor); + bitwise_xor, converted, smt_bit_vector_theoryt::make_xor); } else { @@ -345,15 +381,16 @@ static smt_termt convert_expr_to_smt(const bitxor_exprt &bitwise_xor) } } -static smt_termt convert_expr_to_smt(const bitnot_exprt &bitwise_not) +static smt_termt convert_expr_to_smt( + const bitnot_exprt &bitwise_not, + const sub_expression_mapt &converted) { const bool operand_is_bitvector = can_cast_type(bitwise_not.op().type()); if(operand_is_bitvector) { - return smt_bit_vector_theoryt::make_not( - convert_expr_to_smt(bitwise_not.op())); + return smt_bit_vector_theoryt::make_not(converted.at(bitwise_not.op())); } else { @@ -362,14 +399,15 @@ static smt_termt convert_expr_to_smt(const bitnot_exprt &bitwise_not) } } -static smt_termt convert_expr_to_smt(const unary_minus_exprt &unary_minus) +static smt_termt convert_expr_to_smt( + const unary_minus_exprt &unary_minus, + const sub_expression_mapt &converted) { const bool operand_is_bitvector = can_cast_type(unary_minus.op().type()); if(operand_is_bitvector) { - return smt_bit_vector_theoryt::negate( - convert_expr_to_smt(unary_minus.op())); + return smt_bit_vector_theoryt::negate(converted.at(unary_minus.op())); } else { @@ -379,78 +417,101 @@ static smt_termt convert_expr_to_smt(const unary_minus_exprt &unary_minus) } } -static smt_termt convert_expr_to_smt(const unary_plus_exprt &unary_plus) +static smt_termt convert_expr_to_smt( + const unary_plus_exprt &unary_plus, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for unary plus expression: " + unary_plus.pretty()); } -static smt_termt convert_expr_to_smt(const sign_exprt &is_negative) +static smt_termt convert_expr_to_smt( + const sign_exprt &is_negative, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for \"is negative\" expression: " + is_negative.pretty()); } -static smt_termt convert_expr_to_smt(const if_exprt &if_expression) +static smt_termt convert_expr_to_smt( + const if_exprt &if_expression, + const sub_expression_mapt &converted) { return smt_core_theoryt::if_then_else( - convert_expr_to_smt(if_expression.cond()), - convert_expr_to_smt(if_expression.true_case()), - convert_expr_to_smt(if_expression.false_case())); + converted.at(if_expression.cond()), + converted.at(if_expression.true_case()), + converted.at(if_expression.false_case())); } -static smt_termt convert_expr_to_smt(const and_exprt &and_expression) +static smt_termt convert_expr_to_smt( + const and_exprt &and_expression, + const sub_expression_mapt &converted) { return convert_multiary_operator_to_terms( - and_expression, smt_core_theoryt::make_and); + and_expression, converted, smt_core_theoryt::make_and); } -static smt_termt convert_expr_to_smt(const or_exprt &or_expression) +static smt_termt convert_expr_to_smt( + const or_exprt &or_expression, + const sub_expression_mapt &converted) { return convert_multiary_operator_to_terms( - or_expression, smt_core_theoryt::make_or); + or_expression, converted, smt_core_theoryt::make_or); } -static smt_termt convert_expr_to_smt(const xor_exprt &xor_expression) +static smt_termt convert_expr_to_smt( + const xor_exprt &xor_expression, + const sub_expression_mapt &converted) { return convert_multiary_operator_to_terms( - xor_expression, smt_core_theoryt::make_xor); + xor_expression, converted, smt_core_theoryt::make_xor); } -static smt_termt convert_expr_to_smt(const implies_exprt &implies) +static smt_termt convert_expr_to_smt( + const implies_exprt &implies, + const sub_expression_mapt &converted) { return smt_core_theoryt::implies( - convert_expr_to_smt(implies.op0()), convert_expr_to_smt(implies.op1())); + converted.at(implies.op0()), converted.at(implies.op1())); } -static smt_termt convert_expr_to_smt(const not_exprt &logical_not) +static smt_termt convert_expr_to_smt( + const not_exprt &logical_not, + const sub_expression_mapt &converted) { - return smt_core_theoryt::make_not(convert_expr_to_smt(logical_not.op())); + return smt_core_theoryt::make_not(converted.at(logical_not.op())); } -static smt_termt convert_expr_to_smt(const equal_exprt &equal) +static smt_termt convert_expr_to_smt( + const equal_exprt &equal, + const sub_expression_mapt &converted) { return smt_core_theoryt::equal( - convert_expr_to_smt(equal.op0()), convert_expr_to_smt(equal.op1())); + converted.at(equal.op0()), converted.at(equal.op1())); } -static smt_termt convert_expr_to_smt(const notequal_exprt ¬_equal) +static smt_termt convert_expr_to_smt( + const notequal_exprt ¬_equal, + const sub_expression_mapt &converted) { return smt_core_theoryt::distinct( - convert_expr_to_smt(not_equal.op0()), convert_expr_to_smt(not_equal.op1())); + converted.at(not_equal.op0()), converted.at(not_equal.op1())); } -static smt_termt convert_expr_to_smt(const ieee_float_equal_exprt &float_equal) +static smt_termt convert_expr_to_smt( + const ieee_float_equal_exprt &float_equal, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for floating point equality expression: " + float_equal.pretty()); } -static smt_termt -convert_expr_to_smt(const ieee_float_notequal_exprt &float_not_equal) +static smt_termt convert_expr_to_smt( + const ieee_float_notequal_exprt &float_not_equal, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for floating point not equal expression: " + @@ -461,11 +522,12 @@ template static smt_termt convert_relational_to_smt( const binary_relation_exprt &binary_relation, const unsigned_factory_typet &unsigned_factory, - const signed_factory_typet &signed_factory) + const signed_factory_typet &signed_factory, + const sub_expression_mapt &converted) { PRECONDITION(binary_relation.lhs().type() == binary_relation.rhs().type()); - const auto lhs = convert_expr_to_smt(binary_relation.lhs()); - const auto rhs = convert_expr_to_smt(binary_relation.rhs()); + const auto &lhs = converted.at(binary_relation.lhs()); + const auto &rhs = converted.at(binary_relation.rhs()); const typet operand_type = binary_relation.lhs().type(); if(lhs.get_sort().cast()) { @@ -479,14 +541,17 @@ static smt_termt convert_relational_to_smt( binary_relation.pretty()); } -static optionalt try_relational_conversion(const exprt &expr) +static optionalt try_relational_conversion( + const exprt &expr, + const sub_expression_mapt &converted) { if(const auto greater_than = expr_try_dynamic_cast(expr)) { return convert_relational_to_smt( *greater_than, smt_bit_vector_theoryt::unsigned_greater_than, - smt_bit_vector_theoryt::signed_greater_than); + smt_bit_vector_theoryt::signed_greater_than, + converted); } if( const auto greater_than_or_equal = @@ -495,14 +560,16 @@ static optionalt try_relational_conversion(const exprt &expr) return convert_relational_to_smt( *greater_than_or_equal, smt_bit_vector_theoryt::unsigned_greater_than_or_equal, - smt_bit_vector_theoryt::signed_greater_than_or_equal); + smt_bit_vector_theoryt::signed_greater_than_or_equal, + converted); } if(const auto less_than = expr_try_dynamic_cast(expr)) { return convert_relational_to_smt( *less_than, smt_bit_vector_theoryt::unsigned_less_than, - smt_bit_vector_theoryt::signed_less_than); + smt_bit_vector_theoryt::signed_less_than, + converted); } if( const auto less_than_or_equal = @@ -511,12 +578,15 @@ static optionalt try_relational_conversion(const exprt &expr) return convert_relational_to_smt( *less_than_or_equal, smt_bit_vector_theoryt::unsigned_less_than_or_equal, - smt_bit_vector_theoryt::signed_less_than_or_equal); + smt_bit_vector_theoryt::signed_less_than_or_equal, + converted); } return {}; } -static smt_termt convert_expr_to_smt(const plus_exprt &plus) +static smt_termt convert_expr_to_smt( + const plus_exprt &plus, + const sub_expression_mapt &converted) { if(std::all_of( plus.operands().cbegin(), plus.operands().cend(), [](exprt operand) { @@ -524,7 +594,7 @@ static smt_termt convert_expr_to_smt(const plus_exprt &plus) })) { return convert_multiary_operator_to_terms( - plus, smt_bit_vector_theoryt::add); + plus, converted, smt_bit_vector_theoryt::add); } else { @@ -533,7 +603,9 @@ static smt_termt convert_expr_to_smt(const plus_exprt &plus) } } -static smt_termt convert_expr_to_smt(const minus_exprt &minus) +static smt_termt convert_expr_to_smt( + const minus_exprt &minus, + const sub_expression_mapt &converted) { const bool both_operands_bitvector = can_cast_type(minus.lhs().type()) && @@ -542,7 +614,7 @@ static smt_termt convert_expr_to_smt(const minus_exprt &minus) if(both_operands_bitvector) { return smt_bit_vector_theoryt::subtract( - convert_expr_to_smt(minus.lhs()), convert_expr_to_smt(minus.rhs())); + converted.at(minus.lhs()), converted.at(minus.rhs())); } else { @@ -551,8 +623,13 @@ static smt_termt convert_expr_to_smt(const minus_exprt &minus) } } -static smt_termt convert_expr_to_smt(const div_exprt ÷) +static smt_termt convert_expr_to_smt( + const div_exprt ÷, + const sub_expression_mapt &converted) { + const smt_termt &lhs = converted.at(divide.lhs()); + const smt_termt &rhs = converted.at(divide.rhs()); + const bool both_operands_bitvector = can_cast_type(divide.lhs().type()) && can_cast_type(divide.rhs().type()); @@ -565,13 +642,11 @@ static smt_termt convert_expr_to_smt(const div_exprt ÷) { if(both_operands_unsigned) { - return smt_bit_vector_theoryt::unsigned_divide( - convert_expr_to_smt(divide.lhs()), convert_expr_to_smt(divide.rhs())); + return smt_bit_vector_theoryt::unsigned_divide(lhs, rhs); } else { - return smt_bit_vector_theoryt::signed_divide( - convert_expr_to_smt(divide.lhs()), convert_expr_to_smt(divide.rhs())); + return smt_bit_vector_theoryt::signed_divide(lhs, rhs); } } else @@ -581,7 +656,9 @@ static smt_termt convert_expr_to_smt(const div_exprt ÷) } } -static smt_termt convert_expr_to_smt(const ieee_float_op_exprt &float_operation) +static smt_termt convert_expr_to_smt( + const ieee_float_op_exprt &float_operation, + const sub_expression_mapt &converted) { // This case includes the floating point plus, minus, division and // multiplication operations. @@ -590,8 +667,13 @@ static smt_termt convert_expr_to_smt(const ieee_float_op_exprt &float_operation) float_operation.pretty()); } -static smt_termt convert_expr_to_smt(const mod_exprt &truncation_modulo) +static smt_termt convert_expr_to_smt( + const mod_exprt &truncation_modulo, + const sub_expression_mapt &converted) { + const smt_termt &lhs = converted.at(truncation_modulo.lhs()); + const smt_termt &rhs = converted.at(truncation_modulo.rhs()); + const bool both_operands_bitvector = can_cast_type(truncation_modulo.lhs().type()) && can_cast_type(truncation_modulo.rhs().type()); @@ -604,15 +686,11 @@ static smt_termt convert_expr_to_smt(const mod_exprt &truncation_modulo) { if(both_operands_unsigned) { - return smt_bit_vector_theoryt::unsigned_remainder( - convert_expr_to_smt(truncation_modulo.lhs()), - convert_expr_to_smt(truncation_modulo.rhs())); + return smt_bit_vector_theoryt::unsigned_remainder(lhs, rhs); } else { - return smt_bit_vector_theoryt::signed_remainder( - convert_expr_to_smt(truncation_modulo.lhs()), - convert_expr_to_smt(truncation_modulo.rhs())); + return smt_bit_vector_theoryt::signed_remainder(lhs, rhs); } } else @@ -623,15 +701,18 @@ static smt_termt convert_expr_to_smt(const mod_exprt &truncation_modulo) } } -static smt_termt -convert_expr_to_smt(const euclidean_mod_exprt &euclidean_modulo) +static smt_termt convert_expr_to_smt( + const euclidean_mod_exprt &euclidean_modulo, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for euclidean modulo expression: " + euclidean_modulo.pretty()); } -static smt_termt convert_expr_to_smt(const mult_exprt &multiply) +static smt_termt convert_expr_to_smt( + const mult_exprt &multiply, + const sub_expression_mapt &converted) { if(std::all_of( multiply.operands().cbegin(), @@ -641,7 +722,7 @@ static smt_termt convert_expr_to_smt(const mult_exprt &multiply) })) { return convert_multiary_operator_to_terms( - multiply, smt_bit_vector_theoryt::multiply); + multiply, converted, smt_bit_vector_theoryt::multiply); } else { @@ -651,39 +732,48 @@ static smt_termt convert_expr_to_smt(const mult_exprt &multiply) } } -static smt_termt convert_expr_to_smt(const address_of_exprt &address_of) +static smt_termt convert_expr_to_smt( + const address_of_exprt &address_of, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for address of expression: " + address_of.pretty()); } -static smt_termt convert_expr_to_smt(const array_of_exprt &array_of) +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()); } -static smt_termt -convert_expr_to_smt(const array_comprehension_exprt &array_comprehension) +static smt_termt convert_expr_to_smt( + const array_comprehension_exprt &array_comprehension, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for array comprehension expression: " + array_comprehension.pretty()); } -static smt_termt convert_expr_to_smt(const index_exprt &index) +static smt_termt convert_expr_to_smt( + const index_exprt &index, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for index expression: " + index.pretty()); } template -static smt_termt -convert_to_smt_shift(const factoryt &factory, const shiftt &shift) +static smt_termt convert_to_smt_shift( + const factoryt &factory, + const shiftt &shift, + const sub_expression_mapt &converted) { - const smt_termt first_operand = convert_expr_to_smt(shift.op0()); - const smt_termt second_operand = convert_expr_to_smt(shift.op1()); + const smt_termt &first_operand = converted.at(shift.op0()); + const smt_termt &second_operand = converted.at(shift.op1()); const auto first_bit_vector_sort = first_operand.get_sort().cast(); const auto second_bit_vector_sort = @@ -713,80 +803,100 @@ convert_to_smt_shift(const factoryt &factory, const shiftt &shift) } } -static smt_termt convert_expr_to_smt(const shift_exprt &shift) +static smt_termt convert_expr_to_smt( + const shift_exprt &shift, + const sub_expression_mapt &converted) { // TODO: Dispatch for rotation expressions. A `shift_exprt` can be a rotation. if(const auto left_shift = expr_try_dynamic_cast(shift)) { return convert_to_smt_shift( - smt_bit_vector_theoryt::shift_left, *left_shift); + smt_bit_vector_theoryt::shift_left, *left_shift, converted); } if(const auto right_logical_shift = expr_try_dynamic_cast(shift)) { return convert_to_smt_shift( - smt_bit_vector_theoryt::logical_shift_right, *right_logical_shift); + smt_bit_vector_theoryt::logical_shift_right, + *right_logical_shift, + converted); } if(const auto right_arith_shift = expr_try_dynamic_cast(shift)) { return convert_to_smt_shift( - smt_bit_vector_theoryt::arithmetic_shift_right, *right_arith_shift); + smt_bit_vector_theoryt::arithmetic_shift_right, + *right_arith_shift, + converted); } UNIMPLEMENTED_FEATURE( "Generation of SMT formula for shift expression: " + shift.pretty()); } -static smt_termt convert_expr_to_smt(const with_exprt &with) +static smt_termt convert_expr_to_smt( + const with_exprt &with, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for with expression: " + with.pretty()); } -static smt_termt convert_expr_to_smt(const update_exprt &update) +static smt_termt convert_expr_to_smt( + const update_exprt &update, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for update expression: " + update.pretty()); } -static smt_termt convert_expr_to_smt(const member_exprt &member_extraction) +static smt_termt convert_expr_to_smt( + const member_exprt &member_extraction, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for member extraction expression: " + member_extraction.pretty()); } -static smt_termt -convert_expr_to_smt(const is_dynamic_object_exprt &is_dynamic_object) +static smt_termt convert_expr_to_smt( + const is_dynamic_object_exprt &is_dynamic_object, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for is dynamic object expression: " + is_dynamic_object.pretty()); } -static smt_termt -convert_expr_to_smt(const is_invalid_pointer_exprt &is_invalid_pointer) +static smt_termt convert_expr_to_smt( + const is_invalid_pointer_exprt &is_invalid_pointer, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for is invalid pointer expression: " + is_invalid_pointer.pretty()); } -static smt_termt convert_expr_to_smt(const string_constantt &is_invalid_pointer) +static smt_termt convert_expr_to_smt( + const string_constantt &is_invalid_pointer, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for is invalid pointer expression: " + is_invalid_pointer.pretty()); } -static smt_termt convert_expr_to_smt(const extractbit_exprt &extract_bit) +static smt_termt convert_expr_to_smt( + const extractbit_exprt &extract_bit, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for extract bit expression: " + extract_bit.pretty()); } -static smt_termt convert_expr_to_smt(const extractbits_exprt &extract_bits) +static smt_termt convert_expr_to_smt( + const extractbits_exprt &extract_bits, + const sub_expression_mapt &converted) { - const smt_termt from = convert_expr_to_smt(extract_bits.src()); + const smt_termt &from = converted.at(extract_bits.src()); const auto upper_value = numeric_cast(extract_bits.upper()); const auto lower_value = numeric_cast(extract_bits.lower()); if(upper_value && lower_value) @@ -796,56 +906,72 @@ static smt_termt convert_expr_to_smt(const extractbits_exprt &extract_bits) extract_bits.pretty()); } -static smt_termt convert_expr_to_smt(const replication_exprt &replication) +static smt_termt convert_expr_to_smt( + const replication_exprt &replication, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for bit vector replication expression: " + replication.pretty()); } -static smt_termt convert_expr_to_smt(const byte_extract_exprt &byte_extraction) +static smt_termt convert_expr_to_smt( + const byte_extract_exprt &byte_extraction, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for byte extract expression: " + byte_extraction.pretty()); } -static smt_termt convert_expr_to_smt(const byte_update_exprt &byte_update) +static smt_termt convert_expr_to_smt( + const byte_update_exprt &byte_update, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for byte update expression: " + byte_update.pretty()); } -static smt_termt convert_expr_to_smt(const abs_exprt &absolute_value_of) +static smt_termt convert_expr_to_smt( + const abs_exprt &absolute_value_of, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for absolute value of expression: " + absolute_value_of.pretty()); } -static smt_termt convert_expr_to_smt(const isnan_exprt &is_nan_expr) +static smt_termt convert_expr_to_smt( + const isnan_exprt &is_nan_expr, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for is not a number expression: " + is_nan_expr.pretty()); } -static smt_termt convert_expr_to_smt(const isfinite_exprt &is_finite_expr) +static smt_termt convert_expr_to_smt( + const isfinite_exprt &is_finite_expr, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for is finite expression: " + is_finite_expr.pretty()); } -static smt_termt convert_expr_to_smt(const isinf_exprt &is_infinite_expr) +static smt_termt convert_expr_to_smt( + const isinf_exprt &is_infinite_expr, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for is infinite expression: " + is_infinite_expr.pretty()); } -static smt_termt convert_expr_to_smt(const isnormal_exprt &is_normal_expr) +static smt_termt convert_expr_to_smt( + const isnormal_exprt &is_normal_expr, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for is infinite expression: " + @@ -868,10 +994,12 @@ static smt_termt most_significant_bit_is_set(const smt_termt &input) extract_most_significant_bit(input), smt_bit_vector_constant_termt{1, 1}); } -static smt_termt convert_expr_to_smt(const plus_overflow_exprt &plus_overflow) +static smt_termt convert_expr_to_smt( + const plus_overflow_exprt &plus_overflow, + const sub_expression_mapt &converted) { - const smt_termt left = convert_expr_to_smt(plus_overflow.lhs()); - const smt_termt right = convert_expr_to_smt(plus_overflow.rhs()); + const smt_termt &left = converted.at(plus_overflow.lhs()); + const smt_termt &right = converted.at(plus_overflow.rhs()); if(operands_are_of_type(plus_overflow)) { const auto add_carry_bit = smt_bit_vector_theoryt::zero_extend(1); @@ -895,10 +1023,12 @@ static smt_termt convert_expr_to_smt(const plus_overflow_exprt &plus_overflow) plus_overflow.pretty()); } -static smt_termt convert_expr_to_smt(const minus_overflow_exprt &minus_overflow) +static smt_termt convert_expr_to_smt( + const minus_overflow_exprt &minus_overflow, + const sub_expression_mapt &converted) { - const smt_termt left = convert_expr_to_smt(minus_overflow.lhs()); - const smt_termt right = convert_expr_to_smt(minus_overflow.rhs()); + const smt_termt &left = converted.at(minus_overflow.lhs()); + const smt_termt &right = converted.at(minus_overflow.rhs()); if(operands_are_of_type(minus_overflow)) { return smt_bit_vector_theoryt::unsigned_less_than(left, right); @@ -925,12 +1055,14 @@ static smt_termt convert_expr_to_smt(const minus_overflow_exprt &minus_overflow) minus_overflow.pretty()); } -static smt_termt convert_expr_to_smt(const mult_overflow_exprt &mult_overflow) +static smt_termt convert_expr_to_smt( + const mult_overflow_exprt &mult_overflow, + const sub_expression_mapt &converted) { PRECONDITION(mult_overflow.lhs().type() == mult_overflow.rhs().type()); const auto &operand_type = mult_overflow.lhs().type(); - const smt_termt left = convert_expr_to_smt(mult_overflow.lhs()); - const smt_termt right = convert_expr_to_smt(mult_overflow.rhs()); + const smt_termt &left = converted.at(mult_overflow.lhs()); + const smt_termt &right = converted.at(mult_overflow.rhs()); if( const auto unsigned_type = type_try_dynamic_cast(operand_type)) @@ -966,75 +1098,102 @@ static smt_termt convert_expr_to_smt(const mult_overflow_exprt &mult_overflow) mult_overflow.pretty()); } -static smt_termt convert_expr_to_smt(const shl_overflow_exprt &shl_overflow) +static smt_termt convert_expr_to_smt( + const shl_overflow_exprt &shl_overflow, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for shift left overflow expression: " + shl_overflow.pretty()); } -static smt_termt convert_expr_to_smt(const array_exprt &array_construction) +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()); } -static smt_termt convert_expr_to_smt(const literal_exprt &literal) +static smt_termt convert_expr_to_smt( + const literal_exprt &literal, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for literal expression: " + literal.pretty()); } -static smt_termt convert_expr_to_smt(const forall_exprt &for_all) +static smt_termt convert_expr_to_smt( + const forall_exprt &for_all, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for for all expression: " + for_all.pretty()); } -static smt_termt convert_expr_to_smt(const exists_exprt &exists) +static smt_termt convert_expr_to_smt( + const exists_exprt &exists, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for exists expression: " + exists.pretty()); } -static smt_termt convert_expr_to_smt(const vector_exprt &vector) +static smt_termt convert_expr_to_smt( + const vector_exprt &vector, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for vector expression: " + vector.pretty()); } -static smt_termt convert_expr_to_smt(const bswap_exprt &byte_swap) +static smt_termt +convert_expr_to_smt(const let_exprt &let, const sub_expression_mapt &converted) +{ + UNIMPLEMENTED_FEATURE( + "Generation of SMT formula for let expression: " + let.pretty()); +} + +static smt_termt convert_expr_to_smt( + const bswap_exprt &byte_swap, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for byte swap expression: " + byte_swap.pretty()); } -static smt_termt convert_expr_to_smt(const popcount_exprt &population_count) +static smt_termt convert_expr_to_smt( + const popcount_exprt &population_count, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for population count expression: " + population_count.pretty()); } -static smt_termt -convert_expr_to_smt(const count_leading_zeros_exprt &count_leading_zeros) +static smt_termt convert_expr_to_smt( + const count_leading_zeros_exprt &count_leading_zeros, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for count leading zeros expression: " + count_leading_zeros.pretty()); } -static smt_termt -convert_expr_to_smt(const count_trailing_zeros_exprt &count_trailing_zeros) +static smt_termt convert_expr_to_smt( + const count_trailing_zeros_exprt &count_trailing_zeros, + const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( "Generation of SMT formula for byte swap expression: " + count_trailing_zeros.pretty()); } -smt_termt convert_expr_to_smt(const exprt &expr) +static smt_termt dispatch_expr_to_smt_conversion( + const exprt &expr, + const sub_expression_mapt &converted) { if(const auto symbol = expr_try_dynamic_cast(expr)) { @@ -1042,24 +1201,24 @@ smt_termt convert_expr_to_smt(const exprt &expr) } if(const auto nondet = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*nondet); + return convert_expr_to_smt(*nondet, converted); } if(const auto cast = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*cast); + return convert_expr_to_smt(*cast, converted); } if( const auto float_cast = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*float_cast); + return convert_expr_to_smt(*float_cast, converted); } if(const auto struct_construction = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*struct_construction); + return convert_expr_to_smt(*struct_construction, converted); } if(const auto union_construction = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*union_construction); + return convert_expr_to_smt(*union_construction, converted); } if(const auto constant_literal = expr_try_dynamic_cast(expr)) { @@ -1068,115 +1227,117 @@ smt_termt convert_expr_to_smt(const exprt &expr) if( const auto concatenation = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*concatenation); + return convert_expr_to_smt(*concatenation, converted); } if(const auto bitwise_and_expr = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*bitwise_and_expr); + return convert_expr_to_smt(*bitwise_and_expr, converted); } if(const auto bitwise_or_expr = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*bitwise_or_expr); + return convert_expr_to_smt(*bitwise_or_expr, converted); } if(const auto bitwise_xor = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*bitwise_xor); + return convert_expr_to_smt(*bitwise_xor, converted); } if(const auto bitwise_not = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*bitwise_not); + return convert_expr_to_smt(*bitwise_not, converted); } if(const auto unary_minus = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*unary_minus); + return convert_expr_to_smt(*unary_minus, converted); } if(const auto unary_plus = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*unary_plus); + return convert_expr_to_smt(*unary_plus, converted); } if(const auto is_negative = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*is_negative); + return convert_expr_to_smt(*is_negative, converted); } if(const auto if_expression = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*if_expression); + return convert_expr_to_smt(*if_expression, converted); } if(const auto and_expression = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*and_expression); + return convert_expr_to_smt(*and_expression, converted); } if(const auto or_expression = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*or_expression); + return convert_expr_to_smt(*or_expression, converted); } if(const auto xor_expression = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*xor_expression); + return convert_expr_to_smt(*xor_expression, converted); } if(const auto implies = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*implies); + return convert_expr_to_smt(*implies, converted); } if(const auto logical_not = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*logical_not); + return convert_expr_to_smt(*logical_not, converted); } if(const auto equal = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*equal); + return convert_expr_to_smt(*equal, converted); } if(const auto not_equal = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*not_equal); + return convert_expr_to_smt(*not_equal, converted); } if( const auto float_equal = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*float_equal); + return convert_expr_to_smt(*float_equal, converted); } if( const auto float_not_equal = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*float_not_equal); + return convert_expr_to_smt(*float_not_equal, converted); } - if(const auto converted_relational = try_relational_conversion(expr)) + if( + const auto converted_relational = + try_relational_conversion(expr, converted)) { return *converted_relational; } if(const auto plus = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*plus); + return convert_expr_to_smt(*plus, converted); } if(const auto minus = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*minus); + return convert_expr_to_smt(*minus, converted); } if(const auto divide = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*divide); + return convert_expr_to_smt(*divide, converted); } if( const auto float_operation = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*float_operation); + return convert_expr_to_smt(*float_operation, converted); } if(const auto truncation_modulo = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*truncation_modulo); + return convert_expr_to_smt(*truncation_modulo, converted); } if( const auto euclidean_modulo = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*euclidean_modulo); + return convert_expr_to_smt(*euclidean_modulo, converted); } if(const auto multiply = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*multiply); + return convert_expr_to_smt(*multiply, converted); } #if 0 else if(expr.id() == ID_floatbv_rem) @@ -1186,37 +1347,37 @@ smt_termt convert_expr_to_smt(const exprt &expr) #endif if(const auto address_of = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*address_of); + return convert_expr_to_smt(*address_of, converted); } if(const auto array_of = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*array_of); + return convert_expr_to_smt(*array_of, converted); } if( const auto array_comprehension = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*array_comprehension); + return convert_expr_to_smt(*array_comprehension, converted); } if(const auto index = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*index); + return convert_expr_to_smt(*index, converted); } if(const auto shift = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*shift); + return convert_expr_to_smt(*shift, converted); } if(const auto with = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*with); + return convert_expr_to_smt(*with, converted); } if(const auto update = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*update); + return convert_expr_to_smt(*update, converted); } if(const auto member_extraction = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*member_extraction); + return convert_expr_to_smt(*member_extraction, converted); } #if 0 else if(expr.id()==ID_pointer_offset) @@ -1230,99 +1391,99 @@ smt_termt convert_expr_to_smt(const exprt &expr) const auto is_dynamic_object = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*is_dynamic_object); + return convert_expr_to_smt(*is_dynamic_object, converted); } if( const auto is_invalid_pointer = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*is_invalid_pointer); + return convert_expr_to_smt(*is_invalid_pointer, converted); } if(const auto string_constant = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*string_constant); + return convert_expr_to_smt(*string_constant, converted); } if(const auto extract_bit = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*extract_bit); + return convert_expr_to_smt(*extract_bit, converted); } if(const auto extract_bits = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*extract_bits); + return convert_expr_to_smt(*extract_bits, converted); } if(const auto replication = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*replication); + return convert_expr_to_smt(*replication, converted); } if( const auto byte_extraction = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*byte_extraction); + return convert_expr_to_smt(*byte_extraction, converted); } if(const auto byte_update = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*byte_update); + return convert_expr_to_smt(*byte_update, converted); } if(const auto absolute_value_of = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*absolute_value_of); + return convert_expr_to_smt(*absolute_value_of, converted); } if(const auto is_nan_expr = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*is_nan_expr); + return convert_expr_to_smt(*is_nan_expr, converted); } if(const auto is_finite_expr = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*is_finite_expr); + return convert_expr_to_smt(*is_finite_expr, converted); } if(const auto is_infinite_expr = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*is_infinite_expr); + return convert_expr_to_smt(*is_infinite_expr, converted); } if(const auto is_normal_expr = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*is_normal_expr); + return convert_expr_to_smt(*is_normal_expr, converted); } if( const auto plus_overflow = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*plus_overflow); + return convert_expr_to_smt(*plus_overflow, converted); } if( const auto minus_overflow = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*minus_overflow); + return convert_expr_to_smt(*minus_overflow, converted); } if( const auto mult_overflow = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*mult_overflow); + return convert_expr_to_smt(*mult_overflow, converted); } if(const auto shl_overflow = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*shl_overflow); + return convert_expr_to_smt(*shl_overflow, converted); } if(const auto array_construction = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*array_construction); + return convert_expr_to_smt(*array_construction, converted); } if(const auto literal = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*literal); + return convert_expr_to_smt(*literal, converted); } if(const auto for_all = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*for_all); + return convert_expr_to_smt(*for_all, converted); } if(const auto exists = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*exists); + return convert_expr_to_smt(*exists, converted); } if(const auto vector = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*vector); + return convert_expr_to_smt(*vector, converted); } #if 0 else if(expr.id()==ID_object_size) @@ -1332,7 +1493,7 @@ smt_termt convert_expr_to_smt(const exprt &expr) #endif if(const auto let = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*let); + return convert_expr_to_smt(*let, converted); } INVARIANT( expr.id() != ID_constraint_select_one, @@ -1340,26 +1501,71 @@ smt_termt convert_expr_to_smt(const exprt &expr) expr.pretty()); if(const auto byte_swap = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*byte_swap); + return convert_expr_to_smt(*byte_swap, converted); } if(const auto population_count = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*population_count); + return convert_expr_to_smt(*population_count, converted); } if( const auto count_leading_zeros = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*count_leading_zeros); + return convert_expr_to_smt(*count_leading_zeros, converted); } if( const auto count_trailing_zeros = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*count_trailing_zeros); + return convert_expr_to_smt(*count_trailing_zeros, converted); } UNIMPLEMENTED_FEATURE( "Generation of SMT formula for unknown kind of expression: " + expr.pretty()); } + +#ifndef CPROVER_INVARIANT_DO_NOT_CHECK +template +struct at_scope_exitt +{ + explicit at_scope_exitt(functiont exit_function) + : exit_function(exit_function) + { + } + ~at_scope_exitt() + { + exit_function(); + } + functiont exit_function; +}; + +template +at_scope_exitt at_scope_exit(functiont exit_function) +{ + return at_scope_exitt(exit_function); +} +#endif + +smt_termt convert_expr_to_smt(const exprt &expr) +{ +#ifndef CPROVER_INVARIANT_DO_NOT_CHECK + static bool in_conversion = false; + INVARIANT( + !in_conversion, + "Conversion of expr to smt should be non-recursive. " + "Re-entrance found in conversion of " + + expr.pretty(1, 0)); + in_conversion = true; + const auto end_conversion = at_scope_exit([&]() { in_conversion = false; }); +#endif + sub_expression_mapt sub_expression_map; + expr.visit_post([&](const exprt &expr) { + const auto find_result = sub_expression_map.find(expr); + if(find_result != sub_expression_map.cend()) + return; + smt_termt term = dispatch_expr_to_smt_conversion(expr, sub_expression_map); + sub_expression_map.emplace_hint(find_result, expr, std::move(term)); + }); + return std::move(sub_expression_map.at(expr)); +} From 908d76ee46b57ade2c201832db34cef1a5305345 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Thu, 7 Apr 2022 19:51:25 +0100 Subject: [PATCH 6/7] Add conversion of address_of(symbol) to SMT terms --- .../smt2_incremental/convert_expr_to_smt.cpp | 57 ++++++++- .../smt2_incremental/convert_expr_to_smt.h | 4 +- .../smt2_incremental_decision_procedure.cpp | 16 ++- .../smt2_incremental_decision_procedure.h | 10 +- .../smt2_incremental/convert_expr_to_smt.cpp | 114 ++++++++++++++++++ 5 files changed, 191 insertions(+), 10 deletions(-) diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index e32cca707ee..a9e68ea6ed1 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -4,6 +4,7 @@ #include #include #include +#include #include #include #include @@ -732,10 +733,53 @@ static smt_termt convert_expr_to_smt( } } +#ifndef CPROVER_INVARIANT_DO_NOT_CHECK +static mp_integer power2(unsigned exponent) +{ + mp_integer result; + result.setPower2(exponent); + return result; +} +#endif + +/// \details +/// This conversion constructs a bit vector representation of the memory +/// address. This address is composed of 2 concatenated bit vector components. +/// The first part is the base object's unique identifier. The second is the +/// offset into that object. For address of symbols the offset will be 0. The +/// offset may be non-zero for cases such as the address of a member field of a +/// struct or a the address of a non-zero index into an array. static smt_termt convert_expr_to_smt( const address_of_exprt &address_of, - const sub_expression_mapt &converted) + const sub_expression_mapt &converted, + const smt_object_mapt &object_map) { + const auto type = type_try_dynamic_cast(address_of.type()); + INVARIANT( + type, "Result of the address_of operator should have pointer type."); + const auto base = find_object_base_expression(address_of); + const auto object = object_map.find(base); + INVARIANT( + object != object_map.end(), + "Objects should be tracked before converting their address to SMT terms"); + const std::size_t object_id = object->second.unique_id; + INVARIANT( + object_id < power2(config.bv_encoding.object_bits), + "There should be sufficient bits to encode unique object identifier."); + const smt_termt object_bit_vector = + smt_bit_vector_constant_termt{object_id, config.bv_encoding.object_bits}; + INVARIANT( + type->get_width() > config.bv_encoding.object_bits, + "Pointer should be wider than object_bits in order to allow for offset " + "encoding."); + const size_t offset_bits = type->get_width() - config.bv_encoding.object_bits; + if( + const auto symbol = + expr_try_dynamic_cast(address_of.object())) + { + const smt_bit_vector_constant_termt offset{0, offset_bits}; + return smt_bit_vector_theoryt::concat(object_bit_vector, offset); + } UNIMPLEMENTED_FEATURE( "Generation of SMT formula for address of expression: " + address_of.pretty()); @@ -1193,7 +1237,8 @@ static smt_termt convert_expr_to_smt( static smt_termt dispatch_expr_to_smt_conversion( const exprt &expr, - const sub_expression_mapt &converted) + const sub_expression_mapt &converted, + const smt_object_mapt &object_map) { if(const auto symbol = expr_try_dynamic_cast(expr)) { @@ -1347,7 +1392,7 @@ static smt_termt dispatch_expr_to_smt_conversion( #endif if(const auto address_of = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*address_of, converted); + return convert_expr_to_smt(*address_of, converted, object_map); } if(const auto array_of = expr_try_dynamic_cast(expr)) { @@ -1547,7 +1592,8 @@ at_scope_exitt at_scope_exit(functiont exit_function) } #endif -smt_termt convert_expr_to_smt(const exprt &expr) +smt_termt +convert_expr_to_smt(const exprt &expr, const smt_object_mapt &object_map) { #ifndef CPROVER_INVARIANT_DO_NOT_CHECK static bool in_conversion = false; @@ -1564,7 +1610,8 @@ smt_termt convert_expr_to_smt(const exprt &expr) const auto find_result = sub_expression_map.find(expr); if(find_result != sub_expression_map.cend()) return; - smt_termt term = dispatch_expr_to_smt_conversion(expr, sub_expression_map); + smt_termt term = + dispatch_expr_to_smt_conversion(expr, sub_expression_map, object_map); sub_expression_map.emplace_hint(find_result, expr, std::move(term)); }); return std::move(sub_expression_map.at(expr)); diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.h b/src/solvers/smt2_incremental/convert_expr_to_smt.h index 1bd7dd8331e..bc5b752698c 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.h +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.h @@ -3,6 +3,7 @@ #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H #define CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H +#include #include #include @@ -15,6 +16,7 @@ smt_sortt convert_type_to_smt_sort(const typet &type); /// \brief Converts the \p expression to an smt encoding of the same expression /// stored as term ast (abstract syntax tree). -smt_termt convert_expr_to_smt(const exprt &expression); +smt_termt +convert_expr_to_smt(const exprt &expression, const smt_object_mapt &object_map); #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index 0692522363a..18abf96bc1b 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -132,7 +132,8 @@ smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret( : ns{_ns}, number_of_solver_calls{0}, solver_process(std::move(_solver_process)), - log{message_handler} + log{message_handler}, + object_map{initial_smt_object_map()} { solver_process->send( smt_set_option_commandt{smt_option_produce_modelst{true}}); @@ -157,6 +158,13 @@ void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined( solver_process->send(function); } +smt_termt +smt2_incremental_decision_proceduret::convert_expr_to_smt(const exprt &expr) +{ + track_expression_objects(expr, ns, object_map); + return ::convert_expr_to_smt(expr, object_map); +} + exprt smt2_incremental_decision_proceduret::handle(const exprt &expr) { log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) { @@ -193,7 +201,11 @@ exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const { if(gather_dependent_expressions(expr).empty()) { - descriptor = convert_expr_to_smt(expr); + INVARIANT( + objects_are_already_tracked(expr, object_map), + "Objects in expressions being read should already be tracked from " + "point of being set/handled."); + descriptor = ::convert_expr_to_smt(expr, object_map); } else { diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h index 7d84ad8707d..d5fd6a77cfb 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h @@ -6,11 +6,13 @@ #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H -#include -#include #include #include +#include +#include +#include + #include #include #include @@ -55,6 +57,9 @@ class smt2_incremental_decision_proceduret final /// been defined, along with their dependencies in turn. void define_dependent_functions(const exprt &expr); void ensure_handle_for_expr_defined(const exprt &expr); + /// \brief Add objects in \p expr to object_map if needed and convert to smt. + /// \note This function is non-const because it mutates the object_map. + smt_termt convert_expr_to_smt(const exprt &expr); const namespacet &ns; @@ -78,6 +83,7 @@ class smt2_incremental_decision_proceduret final expression_handle_identifiers; std::unordered_map expression_identifiers; + smt_object_mapt object_map; }; #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H diff --git a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp index 3dc2a13e16b..b51909dac56 100644 --- a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -7,13 +7,17 @@ #include #include #include +#include #include +#include #include +#include #include #include #include #include +#include #include TEST_CASE("\"typet\" to smt sort conversion", "[core][smt2_incremental]") @@ -38,6 +42,11 @@ TEST_CASE("\"typet\" to smt sort conversion", "[core][smt2_incremental]") } } +smt_termt convert_expr_to_smt(const exprt &expression) +{ + return convert_expr_to_smt(expression, initial_smt_object_map()); +} + TEST_CASE("\"symbol_exprt\" to smt term conversion", "[core][smt2_incremental]") { CHECK( @@ -1072,3 +1081,108 @@ TEST_CASE("expr to smt conversion for type casts", "[core][smt2_incremental]") } } } + +TEST_CASE( + "expr to smt conversion for address of operator", + "[core][smt2_incremental]") +{ + // The config lines are necessary to ensure that pointer width in configured. + config.ansi_c.mode = configt::ansi_ct::flavourt::GCC; + config.ansi_c.set_arch_spec_x86_64(); + const symbol_tablet symbol_table; + const namespacet ns{symbol_table}; + smt_object_mapt object_map = initial_smt_object_map(); + const symbol_exprt foo{"foo", unsignedbv_typet{32}}; + const symbol_exprt bar{"bar", unsignedbv_typet{32}}; + SECTION("Address of symbol") + { + const address_of_exprt address_of_foo{foo}; + track_expression_objects(address_of_foo, ns, object_map); + INFO("Expression " + address_of_foo.pretty(1, 0)); + SECTION("8 object bits") + { + config.bv_encoding.object_bits = 8; + const auto converted = convert_expr_to_smt(address_of_foo, object_map); + CHECK(object_map.at(foo).unique_id == 1); + CHECK( + converted == smt_bit_vector_theoryt::concat( + smt_bit_vector_constant_termt{1, 8}, + smt_bit_vector_constant_termt{0, 56})); + } + SECTION("16 object bits") + { + config.bv_encoding.object_bits = 16; + const auto converted = convert_expr_to_smt(address_of_foo, object_map); + CHECK(object_map.at(foo).unique_id == 1); + CHECK( + converted == smt_bit_vector_theoryt::concat( + smt_bit_vector_constant_termt{1, 16}, + smt_bit_vector_constant_termt{0, 48})); + } + } + SECTION("Invariant checks") + { + const cbmc_invariants_should_throwt invariants_throw; + SECTION("Address of should result in a pointer") + { + exprt address_of = address_of_exprt{foo}; + address_of.type() = bool_typet{}; + REQUIRE_THROWS_MATCHES( + convert_expr_to_smt(address_of, object_map), + invariant_failedt, + invariant_failure_containing( + "Result of the address_of operator should have pointer type.")); + } + SECTION("Objects should already be tracked") + { + REQUIRE_THROWS_MATCHES( + convert_expr_to_smt(address_of_exprt{foo}, object_map), + invariant_failedt, + invariant_failure_containing("Objects should be tracked before " + "converting their address to SMT terms")); + } + SECTION("There should be enough bits for object id") + { + config.bv_encoding.object_bits = 8; + const address_of_exprt address_of_foo{foo}; + track_expression_objects(address_of_foo, ns, object_map); + object_map.at(foo).unique_id = 256; + REQUIRE_THROWS_MATCHES( + convert_expr_to_smt(address_of_exprt{foo}, object_map), + invariant_failedt, + invariant_failure_containing("There should be sufficient bits to " + "encode unique object identifier.")); + } + SECTION("Pointer should be wide enough to encode offset") + { + config.bv_encoding.object_bits = 64; + const address_of_exprt address_of_foo{foo}; + track_expression_objects(address_of_foo, ns, object_map); + object_map.at(foo).unique_id = 256; + REQUIRE_THROWS_MATCHES( + convert_expr_to_smt(address_of_exprt{foo}, object_map), + invariant_failedt, + invariant_failure_containing("Pointer should be wider than object_bits " + "in order to allow for offset encoding.")); + } + } + SECTION("Comparison of address of operations.") + { + config.bv_encoding.object_bits = 8; + const exprt comparison = + notequal_exprt{address_of_exprt{foo}, address_of_exprt{bar}}; + track_expression_objects(comparison, ns, object_map); + INFO("Expression " + comparison.pretty(1, 0)); + const auto converted = convert_expr_to_smt(comparison, object_map); + CHECK(object_map.at(foo).unique_id == 2); + CHECK(object_map.at(bar).unique_id == 1); + CHECK( + converted == smt_core_theoryt::distinct( + smt_bit_vector_theoryt::concat( + smt_bit_vector_constant_termt{2, 8}, + smt_bit_vector_constant_termt{0, 56}), + smt_bit_vector_theoryt::concat( + smt_bit_vector_constant_termt{1, 8}, + smt_bit_vector_constant_termt{0, 56}))); + } +} From 41629bef1bb9d473a5995ebdd812fe0aa28c5fd2 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Thu, 7 Apr 2022 19:51:27 +0100 Subject: [PATCH 7/7] Add incremental smt2 with null pointers regression test --- .../cbmc-incr-smt2/pointers/null_pointer.c | 21 +++++++++++++++++++ .../cbmc-incr-smt2/pointers/null_pointer.desc | 17 +++++++++++++++ 2 files changed, 38 insertions(+) create mode 100644 regression/cbmc-incr-smt2/pointers/null_pointer.c create mode 100644 regression/cbmc-incr-smt2/pointers/null_pointer.desc diff --git a/regression/cbmc-incr-smt2/pointers/null_pointer.c b/regression/cbmc-incr-smt2/pointers/null_pointer.c new file mode 100644 index 00000000000..e924c72accc --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers/null_pointer.c @@ -0,0 +1,21 @@ +#include +#include +#include +#include + +int main() +{ + int notdet_int; + int *ptr; + bool notdet_bool; + if(notdet_bool) + { + ptr = ¬det_int; + assert(((uint64_t)ptr) > 1); + } + else + { + ptr = NULL; + } + assert(((uint64_t)ptr) != 0); +} diff --git a/regression/cbmc-incr-smt2/pointers/null_pointer.desc b/regression/cbmc-incr-smt2/pointers/null_pointer.desc new file mode 100644 index 00000000000..11f09ea271f --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers/null_pointer.desc @@ -0,0 +1,17 @@ +CORE +null_pointer.c +--trace +Passing problem to incremental SMT2 solving +line 14 assertion \(\(uint64_t\)ptr\) > 1: SUCCESS +line 20 assertion \(\(uint64_t\)ptr\) != 0: FAILURE +notdet_bool=FALSE \(0+\) +^EXIT=10$ +^SIGNAL=0$ +-- +notdet_bool=TRUE +-- +Tests for null related functionality. + * Assignment of the value NULL to a pointer. + * Comparison of NULL pointer value against 0. + * Check that the address of a non-null pointer is not an offset into the NULL + object.