diff --git a/src/goto-symex/auto_objects.cpp b/src/goto-symex/auto_objects.cpp index ed5683dbd68..ead827225ea 100644 --- a/src/goto-symex/auto_objects.cpp +++ b/src/goto-symex/auto_objects.cpp @@ -34,11 +34,14 @@ exprt goto_symext::make_auto_object(const typet &type, statet &state) void goto_symext::initialize_auto_object(const exprt &expr, statet &state) { - const typet &type=ns.follow(expr.type()); + DATA_INVARIANT( + expr.type().id() != ID_struct, + "no L2-renamed expression expected, all struct-like types should be tags"); - if(type.id()==ID_struct) + if( + auto struct_tag_type = type_try_dynamic_cast(expr.type())) { - const struct_typet &struct_type=to_struct_type(type); + const struct_typet &struct_type = ns.follow_tag(*struct_tag_type); for(const auto &comp : struct_type.components()) { @@ -47,10 +50,9 @@ void goto_symext::initialize_auto_object(const exprt &expr, statet &state) initialize_auto_object(member_expr, state); } } - else if(type.id()==ID_pointer) + else if(auto pointer_type = type_try_dynamic_cast(expr.type())) { - const pointer_typet &pointer_type=to_pointer_type(type); - const typet &base_type = pointer_type.base_type(); + const typet &base_type = pointer_type->base_type(); // we don't like function pointers and // we don't like void * @@ -59,11 +61,11 @@ void goto_symext::initialize_auto_object(const exprt &expr, statet &state) // could be NULL nondeterministically address_of_exprt address_of_expr( - make_auto_object(base_type, state), pointer_type); + make_auto_object(base_type, state), *pointer_type); if_exprt rhs( side_effect_expr_nondett(bool_typet(), expr.source_location()), - null_pointer_exprt(pointer_type), + null_pointer_exprt(*pointer_type), address_of_expr); symex_assign(state, expr, rhs); diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp index a0cb3e1658d..1b3cd036f5c 100644 --- a/src/goto-symex/field_sensitivity.cpp +++ b/src/goto-symex/field_sensitivity.cpp @@ -99,7 +99,10 @@ exprt field_sensitivityt::apply( be.op().type().id() == ID_union_tag) && is_ssa_expr(be.op()) && be.offset().is_constant()) { - const union_typet &type = to_union_type(ns.follow(be.op().type())); + const union_typet &type = + be.op().type().id() == ID_union_tag + ? ns.follow_tag(to_union_tag_type(be.op().type())) + : to_union_type(be.op().type()); for(const auto &comp : type.components()) { ssa_exprt tmp = to_ssa_expr(be.op()); @@ -221,9 +224,12 @@ exprt field_sensitivityt::get_fields( (!disjoined_fields_only && (ssa_expr.type().id() == ID_union || ssa_expr.type().id() == ID_union_tag))) { - const struct_union_typet &type = - to_struct_union_type(ns.follow(ssa_expr.type())); - const struct_union_typet::componentst &components = type.components(); + const struct_union_typet::componentst &components = + (ssa_expr.type().id() == ID_struct_tag || + ssa_expr.type().id() == ID_union_tag) + ? ns.follow_tag(to_struct_or_union_tag_type(ssa_expr.type())) + .components() + : to_struct_union_type(ssa_expr.type()).components(); exprt::operandst fields; fields.reserve(components.size()); @@ -371,7 +377,10 @@ void field_sensitivityt::field_assignments_rec( else if( ssa_rhs.type().id() == ID_struct || ssa_rhs.type().id() == ID_struct_tag) { - const struct_typet &type = to_struct_type(ns.follow(ssa_rhs.type())); + const struct_typet &type = + ssa_rhs.type().id() == ID_struct_tag + ? ns.follow_tag(to_struct_tag_type(ssa_rhs.type())) + : to_struct_type(ssa_rhs.type()); const struct_union_typet::componentst &components = type.components(); PRECONDITION( @@ -409,7 +418,10 @@ void field_sensitivityt::field_assignments_rec( else if( ssa_rhs.type().id() == ID_union || ssa_rhs.type().id() == ID_union_tag) { - const union_typet &type = to_union_type(ns.follow(ssa_rhs.type())); + const union_typet &type = + ssa_rhs.type().id() == ID_union_tag + ? ns.follow_tag(to_union_tag_type(ssa_rhs.type())) + : to_union_type(ssa_rhs.type()); const struct_union_typet::componentst &components = type.components(); PRECONDITION( diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 6755b5636d5..9ac435c89a4 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -741,17 +741,22 @@ void goto_symex_statet::rename( } } - // expand struct and union tag types - type = ns.follow(type); - if(type.id()==ID_array) { auto &array_type = to_array_type(type); rename(array_type.element_type(), irep_idt(), ns); array_type.size() = rename(std::move(array_type.size()), ns).get(); } - else if(type.id() == ID_struct || type.id() == ID_union) + else if( + type.id() == ID_struct || type.id() == ID_union || + type.id() == ID_struct_tag || type.id() == ID_union_tag) { + // expand struct and union tag types + if(type.id() == ID_struct_tag) + type = ns.follow_tag(to_struct_tag_type(type)); + else if(type.id() == ID_union_tag) + type = ns.follow_tag(to_union_tag_type(type)); + struct_union_typet &s_u_type=to_struct_union_type(type); struct_union_typet::componentst &components=s_u_type.components(); diff --git a/src/goto-symex/shadow_memory.cpp b/src/goto-symex/shadow_memory.cpp index f587f29e39c..b5f5b0358d4 100644 --- a/src/goto-symex/shadow_memory.cpp +++ b/src/goto-symex/shadow_memory.cpp @@ -30,8 +30,9 @@ void shadow_memoryt::initialize_shadow_memory( exprt expr, const shadow_memory_field_definitionst::field_definitiont &fields) { - typet type = ns.follow(expr.type()); - clean_pointer_expr(expr, type); + // clean_pointer_expr may change the type + typet type = expr.type(); + clean_pointer_expr(expr); for(const auto &field_pair : fields) { const symbol_exprt &shadow = add_field(state, expr, field_pair.first, type); diff --git a/src/goto-symex/shadow_memory_util.cpp b/src/goto-symex/shadow_memory_util.cpp index 32aa569e307..b86a725b067 100644 --- a/src/goto-symex/shadow_memory_util.cpp +++ b/src/goto-symex/shadow_memory_util.cpp @@ -249,11 +249,12 @@ exprt deref_expr(const exprt &expr) return dereference_exprt(expr); } -void clean_pointer_expr(exprt &expr, const typet &type) +void clean_pointer_expr(exprt &expr) { if( - can_cast_type(type) && can_cast_expr(expr) && - to_array_type(type).size().get_bool(ID_C_SSA_symbol)) + can_cast_type(expr.type()) && + can_cast_expr(expr) && + to_array_type(expr.type()).size().get_bool(ID_C_SSA_symbol)) { remove_array_type_l2(expr.type()); exprt original_expr = to_ssa_expr(expr).get_original_expr(); @@ -448,12 +449,17 @@ exprt compute_or_over_bytes( can_cast_type(field_type) || can_cast_type(field_type), "Can aggregate bytes with *or* only if the shadow memory type is _Bool."); - const typet type = ns.follow(expr.type()); - if(type.id() == ID_struct || type.id() == ID_union) + if( + expr.type().id() == ID_struct || expr.type().id() == ID_union || + expr.type().id() == ID_struct_tag || expr.type().id() == ID_union_tag) { + const auto &components = + (expr.type().id() == ID_struct_tag || expr.type().id() == ID_union_tag) + ? ns.follow_tag(to_struct_or_union_tag_type(expr.type())).components() + : to_struct_union_type(expr.type()).components(); exprt::operandst values; - for(const auto &component : to_struct_union_type(type).components()) + for(const auto &component : components) { if(component.get_is_padding()) { @@ -464,9 +470,9 @@ exprt compute_or_over_bytes( } return or_values(values, field_type); } - else if(type.id() == ID_array) + else if(expr.type().id() == ID_array) { - const array_typet &array_type = to_array_type(type); + const array_typet &array_type = to_array_type(expr.type()); if(array_type.size().is_constant()) { exprt::operandst values; @@ -495,7 +501,10 @@ exprt compute_or_over_bytes( if(is_union) { extract_bytes_of_bv( - conditional_cast_floatbv_to_unsignedbv(expr), type, field_type, values); + conditional_cast_floatbv_to_unsignedbv(expr), + expr.type(), + field_type, + values); } else { @@ -998,11 +1007,14 @@ normalize(const object_descriptor_exprt &expr, const namespacet &ns) else if(object.id() == ID_member) { const member_exprt &member_expr = to_member_expr(object); + const auto &struct_op = member_expr.struct_op(); const struct_typet &struct_type = - to_struct_type(ns.follow(member_expr.struct_op().type())); + struct_op.type().id() == ID_struct_tag + ? ns.follow_tag(to_struct_tag_type(struct_op.type())) + : to_struct_type(struct_op.type()); offset += *member_offset(struct_type, member_expr.get_component_name(), ns); - object = member_expr.struct_op(); + object = struct_op; } else { diff --git a/src/goto-symex/shadow_memory_util.h b/src/goto-symex/shadow_memory_util.h index 5f2de25c277..4b12eed37bf 100644 --- a/src/goto-symex/shadow_memory_util.h +++ b/src/goto-symex/shadow_memory_util.h @@ -75,8 +75,7 @@ irep_idt extract_field_name(const exprt &string_expr); /// L2 symbols and string constants not having char-pointer type. /// \param expr The pointer to the original memory, e.g. as passed to /// __CPROVER_field_get. -/// \param type The followed type of expr. -void clean_pointer_expr(exprt &expr, const typet &type); +void clean_pointer_expr(exprt &expr); /// Wraps a given expression into a `dereference_exprt` unless it is an /// `address_of_exprt` in which case it just unboxes it and returns its content. diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 4bfdca6dbab..c829e4b1d8c 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -168,7 +168,10 @@ void symex_assignt::assign_from_struct( const struct_exprt &rhs, const exprt::operandst &guard) { - const auto &components = to_struct_type(ns.follow(lhs.type())).components(); + const auto &components = + lhs.type().id() == ID_struct_tag + ? ns.follow_tag(to_struct_tag_type(lhs.type())).components() + : to_struct_type(lhs.type()).components(); PRECONDITION(rhs.operands().size() == components.size()); for(const auto &comp_rhs : make_range(components).zip(rhs.operands()))