Merge pull request #8222 from tautschnig/cleanup/no-follow-goto-symex

goto-symex: Replace uses of namespacet::follow

Author: kroening

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<struct_tag_typet>(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<pointer_typet>(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);

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(

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<level>(array_type.element_type(), irep_idt(), ns);
     array_type.size() = rename<level>(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();
 

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);

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<array_typet>(type) && can_cast_expr<symbol_exprt>(expr) &&
-    to_array_type(type).size().get_bool(ID_C_SSA_symbol))
+    can_cast_type<array_typet>(expr.type()) &&
+    can_cast_expr<symbol_exprt>(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<c_bool_typet>(field_type) ||
       can_cast_type<bool_typet>(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
     {

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.

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()))