diff --git a/jbmc/unit/java_bytecode/java_trace_validation/java_trace_validation.cpp b/jbmc/unit/java_bytecode/java_trace_validation/java_trace_validation.cpp index 4232513efcb..af884aae201 100644 --- a/jbmc/unit/java_bytecode/java_trace_validation/java_trace_validation.cpp +++ b/jbmc/unit/java_bytecode/java_trace_validation/java_trace_validation.cpp @@ -22,12 +22,13 @@ TEST_CASE("java trace validation", "[core][java_trace_validation]") { const exprt plain_expr = exprt(); const exprt expr_with_data = exprt("id", java_int_type()); - const symbol_exprt valid_symbol_expr = symbol_exprt("id", java_int_type()); + const symbol_exprt valid_symbol_expr = + symbol_exprt("id", struct_typet{{{"member", java_int_type()}}}); const symbol_exprt invalid_symbol_expr = symbol_exprt(java_int_type()); const member_exprt valid_member = member_exprt(valid_symbol_expr, "member", java_int_type()); - const member_exprt invalid_member = - member_exprt(plain_expr, "member", java_int_type()); + exprt invalid_member = unary_exprt{ID_member, plain_expr, java_int_type()}; + invalid_member.set(ID_component_name, "member"); const constant_exprt invalid_constant = constant_exprt("", java_int_type()); const constant_exprt valid_constant = constant_exprt("0", java_int_type()); const index_exprt valid_index = index_exprt( @@ -88,7 +89,8 @@ TEST_CASE("java trace validation", "[core][java_trace_validation]") INFO("valid member structure") REQUIRE(check_member_structure(valid_member)); INFO("invalid member structure, no symbol operand") - REQUIRE_FALSE(check_member_structure(invalid_member)); + REQUIRE_FALSE(check_member_structure( + static_cast(invalid_member))); } SECTION("can_evaluate_to_constant") diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp index 6b98b4df0b6..4900ca5c336 100644 --- a/src/goto-programs/string_abstraction.cpp +++ b/src/goto-programs/string_abstraction.cpp @@ -817,24 +817,32 @@ bool string_abstractiont::build(const exprt &object, exprt &dest, bool write) if(object.id()==ID_member) { const member_exprt &o_mem=to_member_expr(object); - dest=member_exprt(exprt(), o_mem.get_component_name(), abstract_type); - return build_wrap( - o_mem.struct_op(), to_member_expr(dest).compound(), write); + exprt compound; + if(build_wrap(o_mem.struct_op(), compound, write)) + return true; + dest = member_exprt{ + std::move(compound), o_mem.get_component_name(), abstract_type}; + return false; } if(object.id()==ID_dereference) { const dereference_exprt &o_deref=to_dereference_expr(object); - dest=dereference_exprt(exprt(), abstract_type); - return build_wrap( - o_deref.pointer(), to_dereference_expr(dest).pointer(), write); + exprt pointer; + if(build_wrap(o_deref.pointer(), pointer, write)) + return true; + dest = dereference_exprt{std::move(pointer)}; + return false; } if(object.id()==ID_index) { const index_exprt &o_index=to_index_expr(object); - dest=index_exprt(exprt(), o_index.index(), abstract_type); - return build_wrap(o_index.array(), to_index_expr(dest).array(), write); + exprt array; + if(build_wrap(o_index.array(), array, write)) + return true; + dest = index_exprt{std::move(array), o_index.index()}; + return false; } // handle pointer stuff diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index e0538948a18..44136651bdc 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -1192,7 +1192,10 @@ void value_sett::get_reference_set_rec( if(object.id()==ID_unknown) insert(dest, exprt(ID_unknown, expr.type())); - else + else if( + object.type().id() == ID_struct || + object.type().id() == ID_struct_tag || object.type().id() == ID_union || + object.type().id() == ID_union_tag) { offsett o = it->second; @@ -1218,6 +1221,8 @@ void value_sett::get_reference_set_rec( else insert(dest, exprt(ID_unknown, expr.type())); } + else + insert(dest, exprt(ID_unknown, expr.type())); } return; diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index 08fe2023242..4254bc96bd0 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -916,11 +916,10 @@ void value_set_fit::get_reference_set_sharing_rec( if(object.id()==ID_unknown) insert(dest, exprt(ID_unknown, expr.type())); else if( - object.id() == ID_dynamic_object && obj_type.id() != ID_struct && - obj_type.id() != ID_union && obj_type.id() != ID_struct_tag && - obj_type.id() != ID_union_tag) + obj_type.id() != ID_struct && obj_type.id() != ID_union && + obj_type.id() != ID_struct_tag && obj_type.id() != ID_union_tag) { - // we catch dynamic objects of the wrong type, + // we catch objects of the wrong type, // to avoid non-integral typecasts. insert(dest, exprt(ID_unknown, expr.type())); } diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 35b8d13f020..05da37e5845 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -2789,12 +2789,20 @@ class member_exprt:public unary_exprt member_exprt(exprt op, const irep_idt &component_name, typet _type) : unary_exprt(ID_member, std::move(op), std::move(_type)) { + const auto &compound_type_id = compound().type().id(); + PRECONDITION( + compound_type_id == ID_struct_tag || compound_type_id == ID_union_tag || + compound_type_id == ID_struct || compound_type_id == ID_union); set_component_name(component_name); } member_exprt(exprt op, const struct_typet::componentt &c) : unary_exprt(ID_member, std::move(op), c.type()) { + const auto &compound_type_id = compound().type().id(); + PRECONDITION( + compound_type_id == ID_struct_tag || compound_type_id == ID_union_tag || + compound_type_id == ID_struct || compound_type_id == ID_union); set_component_name(c.get_name()); } diff --git a/unit/analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp b/unit/analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp index 2c243267d3c..4efe8b4f6ba 100644 --- a/unit/analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp +++ b/unit/analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp @@ -33,10 +33,13 @@ SCENARIO( // struct val2 = {.a = 1, .b = 4, .c = 5} auto val2 = std::map{{"a", 1}, {"b", 4}, {"c", 5}}; - // index_exprt for reading from an array - const member_exprt a(nil_exprt(), "a", integer_typet()); - const member_exprt b(nil_exprt(), "b", integer_typet()); - const member_exprt c(nil_exprt(), "c", integer_typet()); + // member_exprt for reading from a struct + exprt dummy = nil_exprt{}; + dummy.type() = struct_typet{ + {{"a", integer_typet{}}, {"b", integer_typet{}}, {"c", integer_typet{}}}}; + const auto a = member_exprt(dummy, "a", integer_typet()); + const auto b = member_exprt(dummy, "b", integer_typet()); + const auto c = member_exprt(dummy, "c", integer_typet()); auto object_factory = variable_sensitivity_object_factoryt::configured_with( vsd_configt::constant_domain()); diff --git a/unit/analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.cpp b/unit/analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.cpp index 1725466161d..7815a100116 100644 --- a/unit/analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.cpp +++ b/unit/analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.cpp @@ -19,6 +19,10 @@ full_struct_abstract_objectt::constant_struct_pointert build_struct( auto struct_type = to_struct_type(starting_value.type()); size_t comp_index = 0; + + auto nil_with_type = nil_exprt(); + nil_with_type.type() = struct_type; + for(const exprt &op : starting_value.operands()) { const auto &component = struct_type.components()[comp_index]; @@ -26,7 +30,7 @@ full_struct_abstract_objectt::constant_struct_pointert build_struct( environment, ns, std::stack(), - member_exprt(nil_exprt(), component.get_name(), component.type()), + member_exprt(nil_with_type, component.get_name(), component.type()), environment.eval(op, ns), false); diff --git a/unit/goto-symex/expr_skeleton.cpp b/unit/goto-symex/expr_skeleton.cpp index f0066ad7844..b73e3691da4 100644 --- a/unit/goto-symex/expr_skeleton.cpp +++ b/unit/goto-symex/expr_skeleton.cpp @@ -15,27 +15,32 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com SCENARIO("expr skeleton", "[core][goto-symex][symex-assign][expr-skeleton]") { - const symbol_exprt foo{"foo", typet{}}; + const signedbv_typet int_type{32}; + const array_typet array_type{int_type, from_integer(2, size_type())}; + const symbol_exprt foo_a{"foo", array_type}; + const symbol_exprt foo_s{"foo", struct_typet{{{"field1", array_type}}}}; + GIVEN("Skeletons `☐`, `☐[index]` and `☐.field1`") { const expr_skeletont empty_skeleton; - const signedbv_typet int_type{32}; - const expr_skeletont index_skeleton = - expr_skeletont::remove_op0(index_exprt{ - array_exprt{{}, array_typet{int_type, from_integer(2, size_type())}}, - from_integer(1, size_type())}); - const expr_skeletont member_skeleton = expr_skeletont::remove_op0( - member_exprt{symbol_exprt{"struct1", typet{}}, "field1", int_type}); + const expr_skeletont index_skeleton = expr_skeletont::remove_op0( + index_exprt{array_exprt{{}, array_type}, from_integer(1, size_type())}); + const expr_skeletont member_skeleton = + expr_skeletont::remove_op0(member_exprt{ + symbol_exprt{"struct1", struct_typet{{{"field1", array_type}}}}, + "field1", + array_type}); THEN( "Applying the skeletons to `foo` gives `foo`, `foo[index]` and " "`foo.field1` respectively") { - REQUIRE(empty_skeleton.apply(foo) == foo); + REQUIRE(empty_skeleton.apply(foo_a) == foo_a); REQUIRE( - index_skeleton.apply(foo) == - index_exprt{foo, from_integer(1, size_type()), int_type}); + index_skeleton.apply(foo_a) == + index_exprt{foo_a, from_integer(1, size_type()), int_type}); REQUIRE( - member_skeleton.apply(foo) == member_exprt{foo, "field1", int_type}); + member_skeleton.apply(foo_s) == + member_exprt(foo_s, "field1", array_type)); } THEN( "The composition of `☐[index]` with `☐.field1` applied to `foo` gives " @@ -44,10 +49,10 @@ SCENARIO("expr skeleton", "[core][goto-symex][symex-assign][expr-skeleton]") const expr_skeletont composition = index_skeleton.compose(member_skeleton); REQUIRE( - composition.apply(foo) == - index_exprt{member_exprt{foo, "field1", int_type}, - from_integer(1, size_type()), - int_type}); + composition.apply(foo_s) == index_exprt{ + member_exprt(foo_s, "field1", array_type), + from_integer(1, size_type()), + int_type}); } THEN( "The composition of `☐[index]` with `☐` applied to `foo` gives " @@ -55,8 +60,8 @@ SCENARIO("expr skeleton", "[core][goto-symex][symex-assign][expr-skeleton]") { const expr_skeletont composition = index_skeleton.compose(empty_skeleton); REQUIRE( - composition.apply(foo) == - index_exprt{foo, from_integer(1, size_type()), int_type}); + composition.apply(foo_a) == + index_exprt{foo_a, from_integer(1, size_type()), int_type}); } } } diff --git a/unit/pointer-analysis/value_set.cpp b/unit/pointer-analysis/value_set.cpp index 108b550bb09..537362c32f4 100644 --- a/unit/pointer-analysis/value_set.cpp +++ b/unit/pointer-analysis/value_set.cpp @@ -135,7 +135,8 @@ SCENARIO( WHEN("We query what (a1 WITH x = NULL).x points to") { with_exprt a1_with( - a1_symbol.symbol_expr(), member_exprt(nil_exprt(), A_x), null_A_ptr); + a1_symbol.symbol_expr(), exprt{ID_member_name}, null_A_ptr); + a1_with.where().set(ID_component_name, A_x.get_name()); member_exprt member_of_with(a1_with, A_x); @@ -153,7 +154,8 @@ SCENARIO( WHEN("We query what (a1 WITH x = NULL).y points to") { with_exprt a1_with( - a1_symbol.symbol_expr(), member_exprt(nil_exprt(), A_x), null_A_ptr); + a1_symbol.symbol_expr(), exprt{ID_member_name}, null_A_ptr); + a1_with.where().set(ID_component_name, A_x.get_name()); member_exprt member_of_with(a1_with, A_y); @@ -171,7 +173,8 @@ SCENARIO( WHEN("We query what (a1 WITH x = NULL) points to") { with_exprt a1_with( - a1_symbol.symbol_expr(), member_exprt(nil_exprt(), A_x), null_A_ptr); + a1_symbol.symbol_expr(), exprt{ID_member_name}, null_A_ptr); + a1_with.where().set(ID_component_name, A_x.get_name()); const std::vector maybe_matching_with_result = value_set.get_value_set(a1_with, ns); diff --git a/unit/solvers/smt2_incremental/object_tracking.cpp b/unit/solvers/smt2_incremental/object_tracking.cpp index fe5e2a1325a..4617580ec4b 100644 --- a/unit/solvers/smt2_incremental/object_tracking.cpp +++ b/unit/solvers/smt2_incremental/object_tracking.cpp @@ -12,41 +12,12 @@ #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", base_type}, 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 qux{"qux", struct_typet{}}; 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}; @@ -55,7 +26,7 @@ TEST_CASE("Tracking object base expressions", "[core][smt2_incremental]") 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}, + member_exprt(qux, "baz", unsignedbv_typet{8}), pointer_type}, bar_address}}; SECTION("Find base expressions") { @@ -63,7 +34,7 @@ TEST_CASE("Tracking object base expressions", "[core][smt2_incremental]") find_object_base_expressions(compound_expression, [&](const exprt &expr) { expressions.push_back(expr); }); - CHECK(expressions == std::vector{bar, foo, bar, foo}); + CHECK(expressions == std::vector{bar, qux, bar, foo}); } smt_object_mapt object_map = initial_smt_object_map(); SECTION("Check initial object map has null pointer") @@ -83,11 +54,11 @@ TEST_CASE("Tracking object base expressions", "[core][smt2_incremental]") track_expression_objects(compound_expression, ns, object_map); SECTION("Tracking expression objects") { - CHECK(object_map.size() == 3); + CHECK(object_map.size() == 4); 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); + CHECK(foo_object->second.unique_id == 3); const auto bar_object = object_map.find(bar); REQUIRE(bar_object != object_map.end()); CHECK(bar_object->second.base_expression == bar);