Do not unnecessarily break sharing during renaming (part 3: expressions)

Not all subexpressions (or types) change during renaming. Only actually write to
the result when there was a change. This preserves sharing.

Performance results for this and parts 1 and 2 of the renaming combined:
On SV-COMP's ReachSafety-ECA benchmarks the time spent in
goto_symex_state::rename(exprt &, ...) is now 1944 seconds, when previously it
was 2326 seconds. On the other hand, the time spent in merge_ireps did not
improve, the number of recursive operator== calls in fact was higher (6930718243
rising to from 5710509892).

The time spent in goto_symex_statet::rename(typet &, ...) increases from 530
seconds to 568 seconds, which suggests there is room for improvement.

Author: tautschnig

src/goto-symex/goto_symex_state.cpp

@@ -14,7 +14,6 @@ Author: Daniel Kroening, [email protected]
 #include <cstdlib>
 #include <iostream>
 
-#include <util/as_const.h>
 #include <util/base_exceptions.h>
 #include <util/exception_utils.h>
 #include <util/expr_util.h>
@@ -291,13 +290,31 @@ template ssa_exprt goto_symex_statet::rename_ssa<goto_symex_statet::L1>(
 
 template <goto_symex_statet::levelt level>
 exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
+{
+  if(auto renamed = rename_expr<level>(expr, ns))
+    return *renamed;
+  else
+    return expr;
+}
+
+// explicitly instantiate templates
+template exprt goto_symex_statet::rename<goto_symex_statet::L1>(
+  exprt expr,
+  const namespacet &ns);
+template exprt goto_symex_statet::rename<goto_symex_statet::L2>(
+  exprt expr,
+  const namespacet &ns);
+
+template <goto_symex_statet::levelt level>
+optionalt<exprt>
+goto_symex_statet::rename_expr(const exprt &expr, const namespacet &ns)
 {
   // rename all the symbols with their last known value
 
   if(expr.id()==ID_symbol &&
      expr.get_bool(ID_C_SSA_symbol))
   {
-    ssa_exprt &ssa=to_ssa_expr(expr);
+    ssa_exprt ssa = to_ssa_expr(expr);
 
     if(level == L0)
     {
@@ -326,7 +343,7 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
         auto p_it = propagation.find(ssa.get_identifier());
 
         if(p_it != propagation.end())
-          expr=p_it->second; // already L2
+          return p_it->second; // already L2
         else
         {
           if(
@@ -340,6 +357,8 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
           set_l2_indices(ssa, ns);
         }
       }
+
+      return std::move(ssa);
     }
 
     if(
@@ -349,6 +368,8 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
       ssa.type() = std::move(*renamed_type);
       ssa.update_type();
     }
+
+    return std::move(ssa);
   }
   else if(expr.id()==ID_symbol)
   {
@@ -359,11 +380,19 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
         auto renamed_type = rename_type<level>(
           expr.type(), to_symbol_expr(expr).get_identifier(), ns))
       {
-        expr.type() = std::move(*renamed_type);
+        exprt result = expr;
+        result.type() = std::move(*renamed_type);
+        return std::move(result);
       }
+      else
+        return {};
     }
+
+    ssa_exprt ssa(expr);
+    if(auto renamed = rename_expr<level>(ssa, ns))
+      return renamed;
     else
-      expr = rename<level>(ssa_exprt{expr}, ns);
+      return std::move(ssa);
   }
   else if(expr.id()==ID_address_of)
   {
@@ -375,29 +404,47 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
       address_of_exprt result = address_of_expr;
       result.object() = std::move(*renamed_object);
       to_pointer_type(result.type()).subtype() = result.object().type();
-      expr = std::move(result);
+      return std::move(result);
     }
+    else
+      return {};
   }
   else
   {
+    exprt result = expr;
+    bool modified = false;
+
     if(auto renamed_type = rename_type<level>(expr.type(), irep_idt(), ns))
     {
-      expr.type() = std::move(*renamed_type);
+      result.type() = std::move(*renamed_type);
+      modified = true;
     }
 
     // do this recursively
-    Forall_operands(it, expr)
-      *it = rename<level>(std::move(*it), ns);
+    exprt::operandst::iterator op_it = result.operands().begin();
+    forall_operands(it, expr)
+    {
+      if(auto renamed_op = rename_expr<level>(*it, ns))
+      {
+        *op_it = std::move(*renamed_op);
+        modified = true;
+      }
+      ++op_it;
+    }
 
-    const exprt &c_expr = as_const(expr);
     INVARIANT(
       (expr.id() != ID_with ||
-       c_expr.type() == to_with_expr(c_expr).old().type()) &&
+       expr.type() == to_with_expr(expr).old().type()) &&
         (expr.id() != ID_if ||
-         (c_expr.type() == to_if_expr(c_expr).true_case().type() &&
-          c_expr.type() == to_if_expr(c_expr).false_case().type())),
+         (expr.type() == to_if_expr(expr).true_case().type() &&
+          expr.type() == to_if_expr(expr).false_case().type())),
       "Type of renamed expr should be the same as operands for with_exprt and "
       "if_exprt");
+
+    if(modified)
+      return std::move(result);
+    else
+      return {};
   }
   return expr;
 }
@@ -616,9 +663,9 @@ goto_symex_statet::rename_address(const exprt &expr, const namespacet &ns)
     auto renamed_array = rename_address<level>(index_expr.array(), ns);
 
     // the index is not an address
-    auto renamed_index = rename<level>(index_expr.index(), ns);
+    auto renamed_index = rename_expr<level>(index_expr.index(), ns);
 
-    if(renamed_array.has_value() || renamed_index != index_expr.index())
+    if(renamed_array.has_value() || renamed_index.has_value())
     {
       index_exprt result = index_expr;
 
@@ -628,8 +675,8 @@ goto_symex_statet::rename_address(const exprt &expr, const namespacet &ns)
         result.type() = to_array_type(result.array().type()).subtype();
       }
 
-      if(renamed_index != index_expr.index())
-        result.index() = std::move(renamed_index);
+      if(renamed_index.has_value())
+        result.index() = std::move(*renamed_index);
 
       return std::move(result);
     }
@@ -640,18 +687,18 @@ goto_symex_statet::rename_address(const exprt &expr, const namespacet &ns)
   {
     // the condition is not an address
     const if_exprt &if_expr = to_if_expr(expr);
-    auto renamed_cond = rename<level>(if_expr.cond(), ns);
+    auto renamed_cond = rename_expr<level>(if_expr.cond(), ns);
     auto renamed_true = rename_address<level>(if_expr.true_case(), ns);
     auto renamed_false = rename_address<level>(if_expr.false_case(), ns);
 
     if(
-      renamed_cond != if_expr.cond() || renamed_true.has_value() ||
+      renamed_cond.has_value() || renamed_true.has_value() ||
       renamed_false.has_value())
     {
       if_exprt result = if_expr;
 
-      if(renamed_cond != if_expr.cond())
-        result.cond() = std::move(renamed_cond);
+      if(renamed_cond.has_value())
+        result.cond() = std::move(*renamed_cond);
 
       if(renamed_true.has_value())
       {
@@ -851,17 +898,17 @@ optionalt<typet> goto_symex_statet::rename_type(
     auto &array_type = to_array_type(type);
     auto renamed_subtype =
       rename_type<level>(array_type.subtype(), irep_idt(), ns);
-    auto renamed_size = rename<level>(array_type.size(), ns);
+    auto renamed_size = rename_expr<level>(array_type.size(), ns);
 
-    if(renamed_subtype.has_value() || renamed_size != array_type.size())
+    if(renamed_subtype.has_value() || renamed_size.has_value())
     {
       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);
+      if(renamed_size.has_value())
+        result_type.size() = std::move(*renamed_size);
 
       result = std::move(result_type);
     }
@@ -878,11 +925,11 @@ optionalt<typet> goto_symex_statet::rename_type(
       // be careful, or it might get cyclic
       if(component.type().id() == ID_array)
       {
-        auto &array_type = to_array_type(component.type());
-        auto renamed_expr = rename<level>(array_type.size(), ns);
-        if(renamed_expr != array_type.size())
+        if(
+          auto renamed_expr =
+            rename_expr<level>(to_array_type(component.type()).size(), ns))
         {
-          to_array_type(comp_it->type()).size() = std::move(renamed_expr);
+          to_array_type(comp_it->type()).size() = std::move(*renamed_expr);
           modified = true;
         }
       }

src/goto-symex/goto_symex_state.h

@@ -202,6 +202,8 @@ class goto_symex_statet final : public goto_statet
   template <levelt>
   optionalt<exprt> rename_address(const exprt &expr, const namespacet &ns);
   template <levelt>
+  optionalt<exprt> rename_expr(const exprt &expr, const namespacet &ns);
+  template <levelt>
   optionalt<typet> rename_type(
     const typet &type,
     const irep_idt &l1_identifier,