Make set_indices a template

This makes the interface of goto_symex_statet simpler and can simplify
code of function templates using set_indices

Author: romainbrenguier

src/goto-symex/goto_symex_state.cpp

@@ -156,20 +156,23 @@ class goto_symex_is_constantt : public is_constantt
   }
 };
 
+template <>
 renamedt<ssa_exprt, L0>
-goto_symex_statet::set_l0_indices(ssa_exprt ssa_expr, const namespacet &ns)
+goto_symex_statet::set_indices<L0>(ssa_exprt ssa_expr, const namespacet &ns)
 {
   return level0(std::move(ssa_expr), ns, source.thread_nr);
 }
 
+template <>
 renamedt<ssa_exprt, L1>
-goto_symex_statet::set_l1_indices(ssa_exprt ssa_expr, const namespacet &ns)
+goto_symex_statet::set_indices<L1>(ssa_exprt ssa_expr, const namespacet &ns)
 {
   return level1(level0(std::move(ssa_expr), ns, source.thread_nr));
 }
 
+template <>
 renamedt<ssa_exprt, L2>
-goto_symex_statet::set_l2_indices(ssa_exprt ssa_expr, const namespacet &ns)
+goto_symex_statet::set_indices<L2>(ssa_exprt ssa_expr, const namespacet &ns)
 {
   return level2(level1(level0(std::move(ssa_expr), ns, source.thread_nr)));
 }
@@ -206,7 +209,7 @@ void goto_symex_statet::assignment(
   const auto level2_it =
     level2.current_names.emplace(l1_identifier, std::make_pair(lhs, 0)).first;
   symex_renaming_levelt::increase_counter(level2_it);
-  const renamedt<ssa_exprt, L2> l2_lhs = set_l2_indices(std::move(lhs), ns);
+  const renamedt<ssa_exprt, L2> l2_lhs = set_indices<L2>(std::move(lhs), ns);
   lhs = l2_lhs.get();
 
   // in case we happen to be multi-threaded, record the memory access
@@ -262,12 +265,12 @@ ssa_exprt goto_symex_statet::rename_ssa(ssa_exprt ssa, const namespacet &ns)
     "rename_ssa can only be used for levels L0 and L1");
   if(level == L0)
   {
-    const renamedt<ssa_exprt, L0> ssa_l0 = set_l0_indices(std::move(ssa), ns);
+    const renamedt<ssa_exprt, L0> ssa_l0 = set_indices<L0>(std::move(ssa), ns);
     ssa = ssa_l0.get();
   }
   else if(level == L1)
   {
-    const renamedt<ssa_exprt, L1> ssa_l1 = set_l1_indices(std::move(ssa), ns);
+    const renamedt<ssa_exprt, L1> ssa_l1 = set_indices<L1>(std::move(ssa), ns);
     ssa = ssa_l1.get();
   }
   else
@@ -304,7 +307,8 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
     }
     else if(level==L2)
     {
-      const renamedt<ssa_exprt, L1> ssa_l1 = set_l1_indices(std::move(ssa), ns);
+      const renamedt<ssa_exprt, L1> ssa_l1 =
+        set_indices<L1>(std::move(ssa), ns);
       ssa = ssa_l1.get();
       rename<level>(expr.type(), ssa.get_identifier(), ns);
       ssa.update_type();
@@ -328,7 +332,7 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
         else
         {
           const renamedt<ssa_exprt, L2> l2_ssa =
-            set_l2_indices(std::move(ssa), ns);
+            set_indices<L2>(std::move(ssa), ns);
           ssa = l2_ssa.get();
         }
       }
@@ -444,7 +448,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
     if(!no_write.op().is_false())
       cond |= guardt{no_write.op()};
 
-    const renamedt<ssa_exprt, L2> l2_true_case = set_l2_indices(ssa_l1, ns);
+    const renamedt<ssa_exprt, L2> l2_true_case = set_indices<L2>(ssa_l1, ns);
 
     if(a_s_read.second.empty())
     {
@@ -454,7 +458,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
       symex_renaming_levelt::increase_counter(level2_it);
       a_s_read.first=level2.current_count(l1_identifier);
     }
-    const renamedt<ssa_exprt, L2> l2_false_case = set_l2_indices(ssa_l1, ns);
+    const renamedt<ssa_exprt, L2> l2_false_case = set_indices<L2>(ssa_l1, ns);
 
     if_exprt tmp{cond.as_expr(), l2_true_case.get(), l2_false_case.get()};
 
@@ -479,7 +483,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
       symex_targett::assignment_typet::PHI);
 
     const renamedt<ssa_exprt, L2> ssa_l2 =
-      set_l2_indices(std::move(ssa_l1), ns);
+      set_indices<L2>(std::move(ssa_l1), ns);
     expr = ssa_l2.get();
 
     a_s_read.second.push_back(guard);
@@ -497,14 +501,14 @@ bool goto_symex_statet::l2_thread_read_encoding(
   if(!record_events)
   {
     const renamedt<ssa_exprt, L2> ssa_l2 =
-      set_l2_indices(std::move(ssa_l1), ns);
+      set_indices<L2>(std::move(ssa_l1), ns);
     expr = ssa_l2.get();
     return true;
   }
 
   // produce a fresh L2 name
   symex_renaming_levelt::increase_counter(level2_it);
-  const renamedt<ssa_exprt, L2> ssa_l2 = set_l2_indices(std::move(ssa_l1), ns);
+  const renamedt<ssa_exprt, L2> ssa_l2 = set_indices<L2>(std::move(ssa_l1), ns);
   expr = ssa_l2.get();
 
   // and record that
@@ -562,7 +566,7 @@ void goto_symex_statet::rename_address(exprt &expr, const namespacet &ns)
     ssa_exprt &ssa=to_ssa_expr(expr);
 
     // only do L1!
-    const renamedt<ssa_exprt, L1> ssa_l1 = set_l1_indices(std::move(ssa), ns);
+    const renamedt<ssa_exprt, L1> ssa_l1 = set_indices<L1>(std::move(ssa), ns);
     ssa = ssa_l1.get();
     rename<level>(expr.type(), ssa.get_identifier(), ns);
     ssa.update_type();

src/goto-symex/goto_symex_state.h

@@ -113,14 +113,9 @@ class goto_symex_statet final : public goto_statet
   template <levelt>
   void rename_address(exprt &expr, const namespacet &ns);
 
-  /// Update level 0 values.
-  renamedt<ssa_exprt, L0> set_l0_indices(ssa_exprt expr, const namespacet &ns);
-
-  /// Update level 0 and 1 values.
-  renamedt<ssa_exprt, L1> set_l1_indices(ssa_exprt expr, const namespacet &ns);
-
-  /// Update level 0, 1 and 2 values.
-  renamedt<ssa_exprt, L2> set_l2_indices(ssa_exprt expr, const namespacet &ns);
+  /// Update values up to \c level.
+  template <levelt level>
+  renamedt<ssa_exprt, level> set_indices(ssa_exprt expr, const namespacet &ns);
 
   // this maps L1 names to (L2) types
   typedef std::unordered_map<irep_idt, typet> l1_typest;