goto_symex: rename type symbols only when needed

Renaming a type is rarely needed: this is necessary only if the type
contains a struct that contains a variable-sized member, which is a gcc
extension.  The key benefit of not renaming in all other cases is that
struct and union tag types no longer get expanded.

Author: Daniel Kroening

src/goto-symex/goto_symex_state.cpp

@@ -625,6 +625,52 @@ void goto_symex_statet::rename_address(
   }
 }
 
+static bool requires_renaming(const typet &type, const namespacet &ns)
+{
+  if(type.id() == ID_array)
+  {
+    const auto &array_type = to_array_type(type);
+    return requires_renaming(array_type.subtype(), ns) ||
+           !array_type.size().is_constant();
+  }
+  else if(
+    type.id() == ID_struct || type.id() == ID_union || type.id() == ID_class)
+  {
+    const struct_union_typet &s_u_type = to_struct_union_type(type);
+    const struct_union_typet::componentst &components = s_u_type.components();
+
+    for(auto &component : components)
+    {
+      // be careful, or it might get cyclic
+      if(component.type().id() != ID_pointer)
+        return requires_renaming(component.type(), ns);
+    }
+
+    return false;
+  }
+  else if(type.id() == ID_pointer)
+  {
+    return requires_renaming(to_pointer_type(type).subtype(), ns);
+  }
+  else if(type.id() == ID_symbol_type)
+  {
+    const symbolt &symbol = ns.lookup(to_symbol_type(type));
+    return requires_renaming(symbol.type, ns);
+  }
+  else if(type.id() == ID_union_tag)
+  {
+    const symbolt &symbol = ns.lookup(to_union_tag_type(type));
+    return requires_renaming(symbol.type, ns);
+  }
+  else if(type.id() == ID_struct_tag)
+  {
+    const symbolt &symbol = ns.lookup(to_struct_tag_type(type));
+    return requires_renaming(symbol.type, ns);
+  }
+
+  return false;
+}
+
 void goto_symex_statet::rename(
   typet &type,
   const irep_idt &l1_identifier,
@@ -633,7 +679,6 @@ void goto_symex_statet::rename(
 {
   // rename all the symbols with their last known value
   // to the given level
-
   std::pair<l1_typest::iterator, bool> l1_type_entry;
   if(level==L2 &&
      !l1_identifier.empty())
@@ -657,6 +702,11 @@ void goto_symex_statet::rename(
     }
   }
 
+  // check whether there are symbol expressions in the type; if not, there
+  // is no need to expand the struct/union tags in the type
+  if(!requires_renaming(type, ns))
+    return; // no action
+
   if(type.id()==ID_array)
   {
     auto &array_type = to_array_type(type);