Do not unnecessarily break sharing during SSA renaming (part 1: types)

Instead of editing the object in place, return an optional<typet> that is set
if, and only if, a modification took place.

Author: tautschnig

src/goto-symex/goto_symex_state.cpp

@@ -281,10 +281,13 @@ ssa_exprt goto_symex_statet::rename_ssa(ssa_exprt ssa, const namespacet &ns)
   return ssa;
 }
 
-/// Ensure `rename_ssa` gets compiled for L0
+// explicitly instantiate templates
 template ssa_exprt goto_symex_statet::rename_ssa<goto_symex_statet::L0>(
   ssa_exprt ssa,
   const namespacet &ns);
+template ssa_exprt goto_symex_statet::rename_ssa<goto_symex_statet::L1>(
+  ssa_exprt ssa,
+  const namespacet &ns);
 
 template <goto_symex_statet::levelt level>
 exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
@@ -298,17 +301,15 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
 
     if(level == L0)
     {
-      ssa = rename_ssa<L0>(std::move(ssa), ns);
+      set_l0_indices(ssa, ns);
     }
     else if(level == L1)
     {
-      ssa = rename_ssa<L1>(std::move(ssa), ns);
+      set_l1_indices(ssa, ns);
     }
     else if(level==L2)
     {
       set_l1_indices(ssa, ns);
-      rename<level>(expr.type(), ssa.get_identifier(), ns);
-      ssa.update_type();
 
       if(l2_thread_read_encoding(ssa, ns))
       {
@@ -327,15 +328,40 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
         if(p_it != propagation.end())
           expr=p_it->second; // already L2
         else
+        {
+          if(
+            auto renamed_type =
+              rename_type<level>(expr.type(), ssa.get_identifier(), ns))
+          {
+            ssa.type() = std::move(*renamed_type);
+            ssa.update_type();
+          }
+
           set_l2_indices(ssa, ns);
+        }
       }
     }
+
+    if(
+      auto renamed_type =
+        rename_type<level>(expr.type(), ssa.get_identifier(), ns))
+    {
+      ssa.type() = std::move(*renamed_type);
+      ssa.update_type();
+    }
   }
   else if(expr.id()==ID_symbol)
   {
     // we never rename function symbols
-    if(as_const(expr).type().id() == ID_code)
-      rename<level>(expr.type(), to_symbol_expr(expr).get_identifier(), ns);
+    if(expr.type().id() == ID_code)
+    {
+      if(
+        auto renamed_type = rename_type<level>(
+          expr.type(), to_symbol_expr(expr).get_identifier(), ns))
+      {
+        expr.type() = std::move(*renamed_type);
+      }
+    }
     else
       expr = rename<level>(ssa_exprt{expr}, ns);
   }
@@ -348,7 +374,10 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
   }
   else
   {
-    rename<level>(expr.type(), irep_idt(), ns);
+    if(auto renamed_type = rename_type<level>(expr.type(), irep_idt(), ns))
+    {
+      expr.type() = std::move(*renamed_type);
+    }
 
     // do this recursively
     Forall_operands(it, expr)
@@ -555,8 +584,13 @@ void goto_symex_statet::rename_address(exprt &expr, const namespacet &ns)
     // only do L1!
     set_l1_indices(ssa, ns);
 
-    rename<level>(expr.type(), ssa.get_identifier(), ns);
-    ssa.update_type();
+    if(
+      auto renamed_type =
+        rename_type<level>(expr.type(), ssa.get_identifier(), ns))
+    {
+      ssa.type() = std::move(*renamed_type);
+      ssa.update_type();
+    }
   }
   else if(expr.id()==ID_symbol)
   {
@@ -680,11 +714,27 @@ void goto_symex_statet::rename(
   typet &type,
   const irep_idt &l1_identifier,
   const namespacet &ns)
+{
+  if(auto renamed = rename_type<level>(type, l1_identifier, ns))
+    type = std::move(*renamed);
+}
+
+// explicitly instantiate templates
+template void goto_symex_statet::rename<goto_symex_statet::L2>(
+  typet &type,
+  const irep_idt &l1_identifier,
+  const namespacet &ns);
+
+template <goto_symex_statet::levelt level>
+optionalt<typet> goto_symex_statet::rename_type(
+  const typet &type,
+  const irep_idt &l1_identifier,
+  const namespacet &ns)
 {
   // 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
+    return {};
 
   // rename all the symbols with their last known value
   // to the given level
@@ -706,46 +756,100 @@ void goto_symex_statet::rename(
          to_array_type(type).is_incomplete() ||
          to_array_type(type_prev).is_complete())
       {
-        type=l1_type_entry.first->second;
-        return;
+        return l1_type_entry.first->second;
       }
     }
   }
 
-  // expand struct and union tag types
-  type = ns.follow(type);
+  optionalt<typet> result;
 
   if(type.id()==ID_array)
   {
     auto &array_type = to_array_type(type);
-    rename<level>(array_type.subtype(), irep_idt(), ns);
-    array_type.size() = rename<level>(std::move(array_type.size()), ns);
+    auto renamed_subtype =
+      rename_type<level>(array_type.subtype(), irep_idt(), ns);
+    auto renamed_size = rename<level>(array_type.size(), ns);
+
+    if(renamed_subtype.has_value() || renamed_size != array_type.size())
+    {
+      array_typet result_type = array_type;
+
+      if(renamed_subtype.has_value())
+        result_type.subtype() = std::move(*renamed_subtype);
+
+      if(renamed_size != array_type.size())
+        result_type.size() = std::move(renamed_size);
+
+      result = std::move(result_type);
+    }
   }
   else if(type.id() == ID_struct || type.id() == ID_union)
   {
-    struct_union_typet &s_u_type=to_struct_union_type(type);
-    struct_union_typet::componentst &components=s_u_type.components();
+    struct_union_typet s_u_type = to_struct_union_type(type);
+    bool modified = false;
 
-    for(auto &component : components)
+    struct_union_typet::componentst::iterator comp_it =
+      s_u_type.components().begin();
+    for(auto &component : to_struct_union_type(type).components())
     {
       // be careful, or it might get cyclic
       if(component.type().id() == ID_array)
       {
         auto &array_type = to_array_type(component.type());
-        array_type.size() = rename<level>(std::move(array_type.size()), ns);
+        auto renamed_expr = rename<level>(array_type.size(), ns);
+        if(renamed_expr != array_type.size())
+        {
+          to_array_type(comp_it->type()).size() = std::move(renamed_expr);
+          modified = true;
+        }
       }
       else if(component.type().id() != ID_pointer)
-        rename<level>(component.type(), irep_idt(), ns);
+      {
+        if(
+          auto renamed_type =
+            rename_type<level>(component.type(), irep_idt(), ns))
+        {
+          comp_it->type() = std::move(*renamed_type);
+          modified = true;
+        }
+      }
+
+      ++comp_it;
     }
+
+    if(modified)
+      result = std::move(s_u_type);
   }
   else if(type.id()==ID_pointer)
   {
-    rename<level>(to_pointer_type(type).subtype(), irep_idt(), ns);
+    if(
+      auto renamed_subtype =
+        rename_type<level>(to_pointer_type(type).subtype(), irep_idt(), ns))
+    {
+      pointer_typet pointer_type = to_pointer_type(type);
+      pointer_type.subtype() = std::move(*renamed_subtype);
+      result = std::move(pointer_type);
+    }
+  }
+  else if(type.id() == ID_symbol_type)
+  {
+    const symbolt &symbol = ns.lookup(to_symbol_type(type));
+    result = rename_type<level>(symbol.type, l1_identifier, ns);
+    if(!result.has_value())
+      result = symbol.type;
+  }
+  else if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
+  {
+    const symbolt &symbol = ns.lookup(to_tag_type(type));
+    result = rename_type<level>(symbol.type, l1_identifier, ns);
+    if(!result.has_value())
+      result = symbol.type;
   }
 
-  if(level==L2 &&
-     !l1_identifier.empty())
-    l1_type_entry.first->second=type;
+  if(level == L2 && !l1_identifier.empty() && result.has_value())
+    l1_type_entry.first->second = *result;
+
+  return result;
 }
 
 static void get_l1_name(exprt &expr)

src/goto-symex/goto_symex_state.h

@@ -201,6 +201,11 @@ class goto_symex_statet final : public goto_statet
 protected:
   template <levelt>
   void rename_address(exprt &expr, const namespacet &ns);
+  template <levelt>
+  optionalt<typet> rename_type(
+    const typet &type,
+    const irep_idt &l1_identifier,
+    const namespacet &ns);
 
   /// Update level 0 values.
   void set_l0_indices(ssa_exprt &expr, const namespacet &ns);