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. 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/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index 8406b464d37..a9e68ea6ed1 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -4,8 +4,10 @@ #include #include #include +#include #include #include +#include #include #include #include @@ -22,9 +24,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 @@ -36,12 +51,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(), @@ -92,7 +108,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: " + @@ -104,8 +122,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. @@ -205,9 +227,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)) @@ -220,21 +244,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: " + @@ -268,25 +298,47 @@ 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}; + } + 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); 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 { @@ -296,12 +348,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 { @@ -311,12 +365,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 { @@ -326,15 +382,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 { @@ -343,14 +400,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 { @@ -360,78 +418,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: " + @@ -442,11 +523,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()) { @@ -460,14 +542,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 = @@ -476,14 +561,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 = @@ -492,12 +579,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) { @@ -505,7 +595,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 { @@ -514,7 +604,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()) && @@ -523,7 +615,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 { @@ -532,8 +624,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()); @@ -546,13 +643,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 @@ -562,7 +657,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. @@ -571,8 +668,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()); @@ -585,15 +687,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 @@ -604,15 +702,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(), @@ -622,7 +723,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 { @@ -632,39 +733,91 @@ static smt_termt convert_expr_to_smt(const mult_exprt &multiply) } } -static smt_termt convert_expr_to_smt(const address_of_exprt &address_of) +#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 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()); } -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 = @@ -694,80 +847,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) @@ -777,56 +950,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: " + @@ -849,10 +1038,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); @@ -876,10 +1067,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); @@ -906,12 +1099,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)) @@ -947,75 +1142,103 @@ 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, + const smt_object_mapt &object_map) { if(const auto symbol = expr_try_dynamic_cast(expr)) { @@ -1023,24 +1246,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)) { @@ -1049,115 +1272,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) @@ -1167,37 +1392,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, object_map); } 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) @@ -1211,99 +1436,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) @@ -1313,7 +1538,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, @@ -1321,26 +1546,73 @@ 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, const smt_object_mapt &object_map) +{ +#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, 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/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/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/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/convert_expr_to_smt.cpp b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp index 3b7393f5ce5..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( @@ -66,6 +75,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( @@ -902,20 +929,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]") @@ -1040,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}))); + } +} 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)); + } +}