diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 63bfaa3fff0..43c482998e7 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2363,8 +2363,7 @@ exprt c_typecheck_baset::do_special_functions( typecheck_function_call_arguments(expr); - unary_exprt object_size_expr( - ID_object_size, expr.arguments()[0], size_type()); + object_size_exprt object_size_expr(expr.arguments()[0], size_type()); object_size_expr.add_source_location() = source_location; return std::move(object_size_expr); diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp index 26a11444880..6a8492275c0 100644 --- a/src/ansi-c/goto_check_c.cpp +++ b/src/ansi-c/goto_check_c.cpp @@ -1476,7 +1476,7 @@ bool goto_check_ct::requires_pointer_primitive_check(const exprt &expr) // pointer_object and pointer_offset just extract a subset of bits from the // pointer. If that pointer was unconstrained (non-deterministic), the result // will equally be non-deterministic. - return expr.id() == ID_object_size || expr.id() == ID_r_ok || + return can_cast_expr(expr) || expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok || expr.id() == ID_is_dynamic_object; } diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index bb1294a50f4..c46a472b438 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -700,14 +700,15 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr) return bv_utils.sign_extension(offset_bv, width); } else if( - expr.id() == ID_object_size && - to_unary_expr(expr).op().type().id() == ID_pointer) + const auto object_size = expr_try_dynamic_cast(expr)) { // we postpone until we know the objects - std::size_t width=boolbv_width(expr.type()); + std::size_t width = boolbv_width(object_size->type()); postponed_list.emplace_back( - prop.new_variables(width), convert_bv(to_unary_expr(expr).op()), expr); + prop.new_variables(width), + convert_bv(object_size->pointer()), + *object_size); return postponed_list.back().bv; } @@ -935,10 +936,11 @@ void bv_pointerst::do_postponed( prop.l_set_to_true(prop.limplies(l1, l2)); } } - else if(postponed.expr.id()==ID_object_size) + else if( + const auto postponed_object_size = + expr_try_dynamic_cast(postponed.expr)) { - const auto &type = - to_pointer_type(to_unary_expr(postponed.expr).op().type()); + const auto &type = to_pointer_type(postponed_object_size->pointer().type()); const auto &objects = pointer_logic.objects; std::size_t number=0; @@ -955,7 +957,7 @@ void bv_pointerst::do_postponed( continue; const exprt object_size = typecast_exprt::conditional_cast( - size_expr.value(), postponed.expr.type()); + size_expr.value(), postponed_object_size->type()); // only compare object part pointer_typet pt = pointer_type(expr.type()); diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index d7f25ef79a4..b3044b21f2b 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -25,7 +25,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -233,10 +232,9 @@ void smt2_convt::write_footer() void smt2_convt::define_object_size( const irep_idt &id, - const exprt &expr) + const object_size_exprt &expr) { - PRECONDITION(expr.id() == ID_object_size); - const exprt &ptr = to_unary_expr(expr).op(); + const exprt &ptr = expr.pointer(); std::size_t size_width = boolbv_width(expr.type()); std::size_t pointer_width = boolbv_width(ptr.type()); std::size_t number = 0; @@ -2018,9 +2016,10 @@ void smt2_convt::convert_expr(const exprt &expr) out << ")"; // mk-... or concat } - else if(expr.id()==ID_object_size) + else if( + const auto object_size = expr_try_dynamic_cast(expr)) { - out << "|" << object_sizes[expr] << "|"; + out << "|" << object_sizes[*object_size] << "|"; } else if(expr.id()==ID_let) { @@ -4848,22 +4847,18 @@ void smt2_convt::find_symbols(const exprt &expr) defined_expressions[expr]=id; } } - else if(expr.id() == ID_object_size) + else if( + const auto object_size = expr_try_dynamic_cast(expr)) { - const exprt &op = to_unary_expr(expr).op(); - - if(op.type().id()==ID_pointer) + if(object_sizes.find(*object_size) == object_sizes.end()) { - if(object_sizes.find(expr)==object_sizes.end()) - { - const irep_idt id = - "object_size." + std::to_string(object_sizes.size()); - out << "(declare-fun |" << id << "| () "; - convert_type(expr.type()); - out << ")" << "\n"; + const irep_idt id = "object_size." + std::to_string(object_sizes.size()); + out << "(declare-fun |" << id << "| () "; + convert_type(object_size->type()); + out << ")" + << "\n"; - object_sizes[expr]=id; - } + object_sizes[*object_size] = id; } } // clang-format off diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index ef6cffe1be0..5d78e834c95 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -10,13 +10,14 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_SOLVERS_SMT2_SMT2_CONV_H #define CPROVER_SOLVERS_SMT2_SMT2_CONV_H +#include +#include +#include + #include #include #include -#include -#include - #if !HASH_CODE # include #endif @@ -216,7 +217,7 @@ class smt2_convt : public stack_decision_proceduret void convert_address_of_rec( const exprt &expr, const pointer_typet &result_type); - void define_object_size(const irep_idt &id, const exprt &expr); + void define_object_size(const irep_idt &id, const object_size_exprt &expr); // keeps track of all non-Boolean symbols and their value struct identifiert @@ -256,7 +257,7 @@ class smt2_convt : public stack_decision_proceduret /// smt2 formula. std::unordered_map set_values; - defined_expressionst object_sizes; + std::map object_sizes; typedef std::set smt2_identifierst; smt2_identifierst smt2_identifiers; diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index a9e68ea6ed1..2594cf02446 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -1192,6 +1192,15 @@ static smt_termt convert_expr_to_smt( "Generation of SMT formula for vector expression: " + vector.pretty()); } +static smt_termt convert_expr_to_smt( + const object_size_exprt &object_size, + const sub_expression_mapt &converted) +{ + UNIMPLEMENTED_FEATURE( + "Generation of SMT formula for object_size expression: " + + object_size.pretty()); +} + static smt_termt convert_expr_to_smt(const let_exprt &let, const sub_expression_mapt &converted) { @@ -1530,12 +1539,10 @@ static smt_termt dispatch_expr_to_smt_conversion( { return convert_expr_to_smt(*vector, converted); } -#if 0 - else if(expr.id()==ID_object_size) + if(const auto object_size = expr_try_dynamic_cast(expr)) { - out << "|" << object_sizes[expr] << "|"; + return convert_expr_to_smt(*object_size, converted); } -#endif if(const auto let = expr_try_dynamic_cast(expr)) { return convert_expr_to_smt(*let, converted); diff --git a/src/util/pointer_expr.h b/src/util/pointer_expr.h index 0ff34c48888..913ebac4479 100644 --- a/src/util/pointer_expr.h +++ b/src/util/pointer_expr.h @@ -989,4 +989,39 @@ inline pointer_object_exprt &to_pointer_object_expr(exprt &expr) return ret; } +/// Expression for finding the size (in bytes) of the object a pointer points +/// to. +class object_size_exprt : public unary_exprt +{ +public: + explicit object_size_exprt(exprt pointer, typet type) + : unary_exprt(ID_object_size, std::move(pointer), std::move(type)) + { + } + + exprt &pointer() + { + return op(); + } + + const exprt &pointer() const + { + return op(); + } +}; + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_object_size; +} + +inline void validate_expr(const object_size_exprt &value) +{ + validate_operands(value, 1, "Object size expression must have one operand."); + DATA_INVARIANT( + can_cast_type(value.pointer().type()), + "Object size expression must have pointer typed operand."); +} + #endif // CPROVER_UTIL_POINTER_EXPR_H diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp index 5264e42a191..2a921fe8316 100644 --- a/src/util/pointer_predicates.cpp +++ b/src/util/pointer_predicates.cpp @@ -32,7 +32,7 @@ exprt same_object(const exprt &p1, const exprt &p2) exprt object_size(const exprt &pointer) { - return unary_exprt(ID_object_size, pointer, size_type()); + return object_size_exprt(pointer, size_type()); } exprt pointer_offset(const exprt &pointer) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 5c7c98e298d..0302da75c94 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2398,9 +2398,10 @@ simplify_exprt::resultt<> simplify_exprt::simplify_node(exprt node) { r = simplify_is_invalid_pointer(to_unary_expr(expr)); } - else if(expr.id()==ID_object_size) + else if( + const auto object_size = expr_try_dynamic_cast(expr)) { - r = simplify_object_size(to_unary_expr(expr)); + r = simplify_object_size(*object_size); } else if(expr.id()==ID_good_pointer) { diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index ca2e49b9bef..0e536cd5efb 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -58,6 +58,7 @@ class multi_ary_exprt; class mult_exprt; class namespacet; class not_exprt; +class object_size_exprt; class plus_exprt; class pointer_object_exprt; class pointer_offset_exprt; @@ -173,7 +174,7 @@ class simplify_exprt NODISCARD resultt<> simplify_byte_update(const byte_update_exprt &); NODISCARD resultt<> simplify_byte_extract(const byte_extract_exprt &); NODISCARD resultt<> simplify_pointer_object(const pointer_object_exprt &); - NODISCARD resultt<> simplify_object_size(const unary_exprt &); + NODISCARD resultt<> simplify_object_size(const object_size_exprt &); NODISCARD resultt<> simplify_is_dynamic_object(const unary_exprt &); NODISCARD resultt<> simplify_is_invalid_pointer(const unary_exprt &); NODISCARD resultt<> simplify_good_pointer(const unary_exprt &); diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index f6d26a1de44..43d1f3ee195 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -640,11 +640,11 @@ simplify_exprt::simplify_is_invalid_pointer(const unary_exprt &expr) } simplify_exprt::resultt<> -simplify_exprt::simplify_object_size(const unary_exprt &expr) +simplify_exprt::simplify_object_size(const object_size_exprt &expr) { auto new_expr = expr; bool no_change = true; - exprt &op = new_expr.op(); + exprt &op = new_expr.pointer(); auto op_result = simplify_object(op); if(op_result.has_changed()) diff --git a/unit/util/pointer_expr.cpp b/unit/util/pointer_expr.cpp index 91c8e0cbfa1..07fe9e725ca 100644 --- a/unit/util/pointer_expr.cpp +++ b/unit/util/pointer_expr.cpp @@ -122,3 +122,63 @@ TEST_CASE("pointer_object_exprt", "[core][util]") } } } + +TEST_CASE("object_size_exprt", "[core][util]") +{ + const exprt pointer = symbol_exprt{"foo", pointer_type(void_type())}; + const object_size_exprt object_size{pointer, size_type()}; + SECTION("Is equivalent to free function.") + { + CHECK(::object_size(pointer) == object_size); + } + SECTION("Result type") + { + CHECK(object_size.type() == size_type()); + } + SECTION("Pointer operand accessor") + { + CHECK(object_size.pointer() == pointer); + } + SECTION("Downcasting") + { + const exprt &upcast = object_size; + CHECK(expr_try_dynamic_cast(upcast)); + CHECK_FALSE(expr_try_dynamic_cast(upcast)); + SECTION("Validation") + { + SECTION("Invalid operand") + { + unary_exprt invalid_type = object_size; + invalid_type.op().type() = bool_typet{}; + const cbmc_invariants_should_throwt invariants_throw; + REQUIRE_THROWS_MATCHES( + expr_try_dynamic_cast(invalid_type), + invariant_failedt, + invariant_failure_containing( + "Object size expression must have pointer typed operand.")); + } + SECTION("Missing operand") + { + exprt missing_operand = object_size; + missing_operand.operands().clear(); + const cbmc_invariants_should_throwt invariants_throw; + REQUIRE_THROWS_MATCHES( + expr_try_dynamic_cast(missing_operand), + invariant_failedt, + invariant_failure_containing( + "Object size expression must have one operand")); + } + SECTION("Too many operands") + { + exprt two_operands = object_size; + two_operands.operands().push_back(pointer); + const cbmc_invariants_should_throwt invariants_throw; + REQUIRE_THROWS_MATCHES( + expr_try_dynamic_cast(two_operands), + invariant_failedt, + invariant_failure_containing( + "Object size expression must have one operand")); + } + } + } +}