Split set_ssa_indices function

The level is already known when we call this function so the cases can
be kept in different functions.

Author: romainbrenguier

src/goto-symex/goto_symex_state.cpp

@@ -211,7 +211,7 @@ void goto_symex_statet::assignment(
   if(level2.current_names.find(l1_identifier)==level2.current_names.end())
     level2.current_names[l1_identifier]=std::make_pair(lhs, 0);
   level2.increase_counter(l1_identifier);
-  set_ssa_indices(lhs, ns, L2);
+  set_l2_indices(lhs, ns);
 
   // in case we happen to be multi-threaded, record the memory access
   bool is_shared=l2_thread_write_encoding(lhs, ns);
@@ -253,37 +253,34 @@ void goto_symex_statet::assignment(
   #endif
 }
 
-void goto_symex_statet::set_ssa_indices(
+void goto_symex_statet::set_l0_indices(
   ssa_exprt &ssa_expr,
-  const namespacet &ns,
-  levelt level)
+  const namespacet &ns)
 {
-  switch(level)
-  {
-  case L0:
-    level0(ssa_expr, ns, source.thread_nr);
-    break;
-
-  case L1:
-    if(!ssa_expr.get_level_2().empty())
-      return;
-    if(!ssa_expr.get_level_1().empty())
-      return;
-    level0(ssa_expr, ns, source.thread_nr);
-    level1(ssa_expr);
-    break;
+  level0(ssa_expr, ns, source.thread_nr);
+}
 
-  case L2:
-    if(!ssa_expr.get_level_2().empty())
-      return;
-    level0(ssa_expr, ns, source.thread_nr);
-    level1(ssa_expr);
-    ssa_expr.set_level_2(level2.current_count(ssa_expr.get_identifier()));
-    break;
+void goto_symex_statet::set_l1_indices(
+  ssa_exprt &ssa_expr,
+  const namespacet &ns)
+{
+  if(!ssa_expr.get_level_2().empty())
+    return;
+  if(!ssa_expr.get_level_1().empty())
+    return;
+  level0(ssa_expr, ns, source.thread_nr);
+  level1(ssa_expr);
+}
 
-  default:
-    UNREACHABLE;
-  }
+void goto_symex_statet::set_l2_indices(
+  ssa_exprt &ssa_expr,
+  const namespacet &ns)
+{
+  if(!ssa_expr.get_level_2().empty())
+    return;
+  level0(ssa_expr, ns, source.thread_nr);
+  level1(ssa_expr);
+  ssa_expr.set_level_2(level2.current_count(ssa_expr.get_identifier()));
 }
 
 void goto_symex_statet::rename(
@@ -298,15 +295,21 @@ void goto_symex_statet::rename(
   {
     ssa_exprt &ssa=to_ssa_expr(expr);
 
-    if(level==L0 || level==L1)
+    if(level == L0)
+    {
+      set_l0_indices(ssa, ns);
+      rename(expr.type(), ssa.get_identifier(), ns, level);
+      ssa.update_type();
+    }
+    else if(level == L1)
     {
-      set_ssa_indices(ssa, ns, level);
+      set_l1_indices(ssa, ns);
       rename(expr.type(), ssa.get_identifier(), ns, level);
       ssa.update_type();
     }
     else if(level==L2)
     {
-      set_ssa_indices(ssa, ns, L1);
+      set_l1_indices(ssa, ns);
       rename(expr.type(), ssa.get_identifier(), ns, level);
       ssa.update_type();
 
@@ -327,7 +330,7 @@ void goto_symex_statet::rename(
         if(p_it != propagation.end())
           expr=p_it->second; // already L2
         else
-          set_ssa_indices(ssa, ns, L2);
+          set_l2_indices(ssa, ns);
       }
     }
   }
@@ -453,7 +456,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
       cond=or_exprt(no_write.op(), cond);
 
     if_exprt tmp(cond, ssa_l1, ssa_l1);
-    set_ssa_indices(to_ssa_expr(tmp.true_case()), ns, L2);
+    set_l2_indices(to_ssa_expr(tmp.true_case()), ns);
 
     if(a_s_read.second.empty())
     {
@@ -485,7 +488,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
       source,
       symex_targett::assignment_typet::PHI);
 
-    set_ssa_indices(ssa_l1, ns, L2);
+    set_l2_indices(ssa_l1, ns);
     expr=ssa_l1;
 
     a_s_read.second.push_back(guard);
@@ -501,14 +504,14 @@ bool goto_symex_statet::l2_thread_read_encoding(
   // No event and no fresh index, but avoid constant propagation
   if(!record_events)
   {
-    set_ssa_indices(ssa_l1, ns, L2);
+    set_l2_indices(ssa_l1, ns);
     expr=ssa_l1;
     return true;
   }
 
   // produce a fresh L2 name
   level2.increase_counter(l1_identifier);
-  set_ssa_indices(ssa_l1, ns, L2);
+  set_l2_indices(ssa_l1, ns);
   expr=ssa_l1;
 
   // and record that
@@ -570,7 +573,7 @@ void goto_symex_statet::rename_address(
     ssa_exprt &ssa=to_ssa_expr(expr);
 
     // only do L1!
-    set_ssa_indices(ssa, ns, L1);
+    set_l1_indices(ssa, ns);
 
     rename(expr.type(), ssa.get_identifier(), ns, level);
     ssa.update_type();

src/goto-symex/goto_symex_state.h

@@ -92,7 +92,10 @@ class goto_symex_statet final
 protected:
   void rename_address(exprt &expr, const namespacet &ns, levelt level);
 
-  void set_ssa_indices(ssa_exprt &expr, const namespacet &ns, levelt level=L2);
+  void set_l0_indices(ssa_exprt &expr, const namespacet &ns);
+  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;