Make symex_level0 a function

A functor without state is just a function.

Author: romainbrenguier

src/goto-symex/goto_symex_state.cpp

@@ -135,21 +135,22 @@ template <>
 renamedt<ssa_exprt, L0>
 goto_symex_statet::set_indices<L0>(ssa_exprt ssa_expr, const namespacet &ns)
 {
-  return level0(std::move(ssa_expr), ns, source.thread_nr);
+  return symex_level0(std::move(ssa_expr), ns, source.thread_nr);
 }
 
 template <>
 renamedt<ssa_exprt, L1>
 goto_symex_statet::set_indices<L1>(ssa_exprt ssa_expr, const namespacet &ns)
 {
-  return level1(level0(std::move(ssa_expr), ns, source.thread_nr));
+  return level1(symex_level0(std::move(ssa_expr), ns, source.thread_nr));
 }
 
 template <>
 renamedt<ssa_exprt, L2>
 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)));
+  return level2(
+    level1(symex_level0(std::move(ssa_expr), ns, source.thread_nr)));
 }
 
 renamedt<ssa_exprt, L2> goto_symex_statet::assignment(

src/goto-symex/goto_symex_state.h

@@ -70,7 +70,6 @@ class goto_symex_statet final : public goto_statet
   guard_managert &guard_manager;
   symex_target_equationt *symex_target;
 
-  symex_level0t level0;
   symex_level1t level1;
 
   /// Rewrites symbol expressions in \ref exprt, applying a suffix to each

src/goto-symex/renamed.h

@@ -49,7 +49,8 @@ class renamedt : private underlyingt
     return static_cast<underlyingt &>(*this);
   };
 
-  friend struct symex_level0t;
+  friend renamedt<ssa_exprt, L0>
+  symex_level0(ssa_exprt, const namespacet &, unsigned);
   friend struct symex_level1t;
   friend struct symex_level2t;
   friend class goto_symex_statet;

src/goto-symex/renaming_level.cpp

@@ -30,8 +30,8 @@ void get_variables(
   }
 }
 
-renamedt<ssa_exprt, L0> symex_level0t::
-operator()(ssa_exprt ssa_expr, const namespacet &ns, unsigned thread_nr) const
+renamedt<ssa_exprt, L0>
+symex_level0(ssa_exprt ssa_expr, const namespacet &ns, unsigned thread_nr)
 {
   // already renamed?
   if(!ssa_expr.get_level_0().empty())

src/goto-symex/renaming_level.h

@@ -37,19 +37,14 @@ void get_variables(
   const symex_renaming_levelt &current_names,
   std::unordered_set<ssa_exprt, irep_hash> &vars);
 
-/// Functor to set the level 0 renaming of SSA expressions.
+/// Set the level 0 renaming of SSA expressions.
 /// Level 0 corresponds to threads.
 /// The renaming is built for one particular interleaving.
-struct symex_level0t
-{
-  /// Rename \p ssa_expr using \p thread_nr as L0 tag, unless \p ssa_expr is
-  /// a guard, a shared variable or a function. \p ns is queried to decide
-  /// whether we are in one of these cases.
-  renamedt<ssa_exprt, L0> operator()(
-    ssa_exprt ssa_expr,
-    const namespacet &ns,
-    unsigned thread_nr) const;
-};
+/// Rename \p ssa_expr using \p thread_nr as L0 tag, unless \p ssa_expr is
+/// a guard, a shared variable or a function. \p ns is queried to decide
+/// whether we are in one of these cases.
+renamedt<ssa_exprt, L0>
+symex_level0(ssa_exprt ssa_expr, const namespacet &ns, unsigned thread_nr);
 
 /// Functor to set the level 1 renaming of SSA expressions.
 /// Level 1 corresponds to function frames.

src/goto-symex/symex_start_thread.cpp

@@ -67,8 +67,7 @@ void goto_symext::symex_start_thread(statet &state)
     ssa_exprt lhs(pair.second.first.get_original_expr());
 
     // get L0 name for current thread
-    const renamedt<ssa_exprt, L0> l0_lhs =
-      symex_level0t{}(std::move(lhs), ns, t);
+    const renamedt<ssa_exprt, L0> l0_lhs = symex_level0(std::move(lhs), ns, t);
     const irep_idt &l0_name = l0_lhs.get().get_identifier();
     std::size_t l1_index = path_storage.get_unique_l1_index(l0_name, 0);
     CHECK_RETURN(l1_index == 0);

unit/goto-symex/symex_level0.cpp

@@ -72,7 +72,7 @@ SCENARIO("Level 0 renaming", "[core][goto-symex][symex-level0]")
 
     WHEN("The non-shared symbol is renamed")
     {
-      auto renamed = symex_level0t{}(ssa_nonshared, ns, 423);
+      auto renamed = symex_level0(ssa_nonshared, ns, 423);
 
       THEN("Its L0 tag is set to the thread index")
       {
@@ -82,7 +82,7 @@ SCENARIO("Level 0 renaming", "[core][goto-symex][symex-level0]")
 
     WHEN("The shared symbol is renamed")
     {
-      auto renamed = symex_level0t{}(ssa_shared, ns, 423);
+      auto renamed = symex_level0(ssa_shared, ns, 423);
 
       THEN("Its L0 tag is unchanged")
       {
@@ -92,7 +92,7 @@ SCENARIO("Level 0 renaming", "[core][goto-symex][symex-level0]")
 
     WHEN("The guard is renamed")
     {
-      auto renamed = symex_level0t{}(ssa_guard, ns, 423);
+      auto renamed = symex_level0(ssa_guard, ns, 423);
 
       THEN("Its L0 tag is unchanged")
       {
@@ -104,7 +104,7 @@ SCENARIO("Level 0 renaming", "[core][goto-symex][symex-level0]")
 
     WHEN("The function is renamed")
     {
-      auto renamed = symex_level0t{}(ssa_fun, ns, 423);
+      auto renamed = symex_level0(ssa_fun, ns, 423);
 
       THEN("Its L0 tag is unchanged")
       {