Merge pull request #3559 from romainbrenguier/optimize/get_l1_name

Optimize remove_level_2

Author: romainbrenguier

src/goto-symex/goto_symex_state.cpp

@@ -25,6 +25,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <analyses/dirty.h>
 
+static void get_l1_name(exprt &expr);
+
 goto_symex_statet::goto_symex_statet()
   : depth(0),
     symex_target(nullptr),
@@ -220,7 +222,7 @@ void goto_symex_statet::assignment(
     get_l1_name(l1_rhs);
 
     ssa_exprt l1_lhs(lhs);
-    get_l1_name(l1_lhs);
+    l1_lhs.remove_level_2();
 
     if(run_validation_checks)
     {
@@ -750,7 +752,7 @@ void goto_symex_statet::get_original_name(typet &type) const
   }
 }
 
-void goto_symex_statet::get_l1_name(exprt &expr) const
+static void get_l1_name(exprt &expr)
 {
   // do not reset the type !
 

src/goto-symex/goto_symex_state.h

@@ -97,9 +97,6 @@ class goto_symex_statet final
   void set_l1_indices(ssa_exprt &expr, const namespacet &ns);
   void set_l2_indices(ssa_exprt &expr, const namespacet &ns);
 
-  // only required for value_set.assign
-  void get_l1_name(exprt &expr) const;
-
   // this maps L1 names to (L2) types
   typedef std::unordered_map<irep_idt, typet> l1_typest;
   l1_typest l1_types;

src/util/ssa_expr.cpp

@@ -13,6 +13,10 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 
+/// If \p expr is a symbol "s" add to \p os "s!l0@l1#l2" and to \p l1_object_os
+/// "s!l0@l1".
+/// If \p expr is a member or index expression, recursively apply the procedure
+/// and add ".component_name" or "[index]" to \p os.
 static void build_ssa_identifier_rec(
   const exprt &expr,
   const irep_idt &l0,
@@ -82,7 +86,7 @@ bool ssa_exprt::can_build_identifier(const exprt &expr)
     return false;
 }
 
-std::pair<irep_idt, irep_idt> ssa_exprt::build_identifier(
+static std::pair<irep_idt, irep_idt> build_identifier(
   const exprt &expr,
   const irep_idt &l0,
   const irep_idt &l1,
@@ -95,3 +99,14 @@ std::pair<irep_idt, irep_idt> ssa_exprt::build_identifier(
 
   return std::make_pair(irep_idt(oss.str()), irep_idt(l1_object_oss.str()));
 }
+
+void ssa_exprt::update_identifier()
+{
+  const irep_idt &l0 = get_level_0();
+  const irep_idt &l1 = get_level_1();
+  const irep_idt &l2 = get_level_2();
+
+  auto idpair = build_identifier(get_original_expr(), l0, l1, l2);
+  set_identifier(idpair.first);
+  set(ID_L1_object_identifier, idpair.second);
+}

src/util/ssa_expr.h

@@ -101,7 +101,7 @@ class ssa_exprt:public symbol_exprt
   void remove_level_2()
   {
     remove(ID_L2);
-    update_identifier();
+    set_identifier(get_l1_object_identifier());
   }
 
   const irep_idt get_level_0() const
@@ -119,22 +119,7 @@ class ssa_exprt:public symbol_exprt
     return get(ID_L2);
   }
 
-  void update_identifier()
-  {
-    const irep_idt &l0=get_level_0();
-    const irep_idt &l1=get_level_1();
-    const irep_idt &l2=get_level_2();
-
-    auto idpair=build_identifier(get_original_expr(), l0, l1, l2);
-    set_identifier(idpair.first);
-    set(ID_L1_object_identifier, idpair.second);
-  }
-
-  static std::pair<irep_idt, irep_idt> build_identifier(
-    const exprt &src,
-    const irep_idt &l0,
-    const irep_idt &l1,
-    const irep_idt &l2);
+  void update_identifier();
 
   /* Used to determine whether or not an identifier can be built
    * before trying and getting an exception */