Move renaming_level classes to a new file

Author: romainbrenguier

src/goto-symex/Makefile

@@ -10,6 +10,7 @@ SRC = auto_objects.cpp \
       path_storage.cpp \
       postcondition.cpp \
       precondition.cpp \
+      renaming_level.cpp \
       show_program.cpp \
       show_vcc.cpp \
       slice.cpp \

src/goto-symex/goto_symex_state.cpp

@@ -38,50 +38,6 @@ goto_symex_statet::goto_symex_statet()
 
 goto_symex_statet::~goto_symex_statet()=default;
 
-void goto_symex_statet::level0t::operator()(
-  ssa_exprt &ssa_expr,
-  const namespacet &ns,
-  unsigned thread_nr)
-{
-  // already renamed?
-  if(!ssa_expr.get_level_0().empty())
-    return;
-
-  const irep_idt &obj_identifier=ssa_expr.get_object_name();
-
-  // guards are not L0-renamed
-  if(obj_identifier=="goto_symex::\\guard")
-    return;
-
-  const symbolt *s;
-  const bool found_l0 = !ns.lookup(obj_identifier, s);
-  INVARIANT(found_l0, "level0: failed to find " + id2string(obj_identifier));
-
-  // don't rename shared variables or functions
-  if(s->type.id()==ID_code ||
-     s->is_shared())
-    return;
-
-  // rename!
-  ssa_expr.set_level_0(thread_nr);
-}
-
-void goto_symex_statet::level1t::operator()(ssa_exprt &ssa_expr)
-{
-  // already renamed?
-  if(!ssa_expr.get_level_1().empty())
-    return;
-
-  const irep_idt l0_name=ssa_expr.get_l1_object_identifier();
-
-  current_namest::const_iterator it=current_names.find(l0_name);
-  if(it==current_names.end())
-    return;
-
-  // rename!
-  ssa_expr.set_level_1(it->second.second);
-}
-
 /// write to a variable
 static bool check_renaming(const exprt &expr);
 

src/goto-symex/goto_symex_state.h

@@ -27,6 +27,7 @@ Author: Daniel Kroening, [email protected]
 #include <pointer-analysis/value_set.h>
 #include <goto-programs/goto_function.h>
 
+#include "renaming_level.h"
 #include "symex_target_equation.h"
 
 // central data structure: state
@@ -60,86 +61,9 @@ class goto_symex_statet final
   // we remember all L1 renamings
   std::set<irep_idt> l1_history;
 
-  struct renaming_levelt
-  {
-    virtual ~renaming_levelt() { }
-
-    typedef std::map<irep_idt, std::pair<ssa_exprt, unsigned> > current_namest;
-    current_namest current_names;
-
-    unsigned current_count(const irep_idt &identifier) const
-    {
-      const auto it = current_names.find(identifier);
-      return it==current_names.end()?0:it->second.second;
-    }
-
-    void increase_counter(const irep_idt &identifier)
-    {
-      PRECONDITION(current_names.find(identifier) != current_names.end());
-      ++current_names[identifier].second;
-    }
-
-    void get_variables(std::unordered_set<ssa_exprt, irep_hash> &vars) const
-    {
-      for(current_namest::const_iterator it=current_names.begin();
-          it!=current_names.end();
-          it++)
-        vars.insert(it->second.first);
-    }
-  };
-
-  // level 0 -- threads!
-  // renaming built for one particular interleaving
-  struct level0t:public renaming_levelt
-  {
-    void operator()(
-      ssa_exprt &ssa_expr,
-      const namespacet &ns,
-      unsigned thread_nr);
-
-    level0t() { }
-    virtual ~level0t() { }
-  } level0;
-
-  // level 1 -- function frames
-  // this is to preserve locality in case of recursion
-
-  struct level1t:public renaming_levelt
-  {
-    void operator()(ssa_exprt &ssa_expr);
-
-    void restore_from(const current_namest &other)
-    {
-      current_namest::iterator it=current_names.begin();
-      for(current_namest::const_iterator
-          ito=other.begin();
-          ito!=other.end();
-          ++ito)
-      {
-        while(it!=current_names.end() && it->first<ito->first)
-          ++it;
-        if(it==current_names.end() || ito->first<it->first)
-          current_names.insert(it, *ito);
-        else if(it!=current_names.end())
-        {
-          PRECONDITION(it->first == ito->first);
-          it->second=ito->second;
-          ++it;
-        }
-      }
-    }
-
-    level1t() { }
-    virtual ~level1t() { }
-  } level1;
-
-  // level 2 -- SSA
-
-  struct level2t:public renaming_levelt
-  {
-    level2t() { }
-    virtual ~level2t() { }
-  } level2;
+  symex_level0t level0;
+  symex_level1t level1;
+  symex_level2t level2;
 
   // this maps L1 names to (L2) constants
   class propagationt
@@ -198,7 +122,7 @@ class goto_symex_statet final
   {
   public:
     unsigned depth;
-    level2t::current_namest level2_current_names;
+    symex_level2t::current_namest level2_current_names;
     value_sett value_set;
     guardt guard;
     symex_targett::sourcet source;

src/goto-symex/renaming_level.cpp

@@ -0,0 +1,57 @@
+/*******************************************************************\
+
+Module: Symbolic Execution
+
+Author: Romain Brenguier, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Renaming levels
+
+#include "renaming_level.h"
+
+#include <util/namespace.h>
+#include <util/ssa_expr.h>
+#include <util/symbol.h>
+
+void symex_level0t::
+operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr)
+{
+  // already renamed?
+  if(!ssa_expr.get_level_0().empty())
+    return;
+
+  const irep_idt &obj_identifier = ssa_expr.get_object_name();
+
+  // guards are not L0-renamed
+  if(obj_identifier == "goto_symex::\\guard")
+    return;
+
+  const symbolt *s;
+  const bool found_l0 = !ns.lookup(obj_identifier, s);
+  INVARIANT(found_l0, "level0: failed to find " + id2string(obj_identifier));
+
+  // don't rename shared variables or functions
+  if(s->type.id() == ID_code || s->is_shared())
+    return;
+
+  // rename!
+  ssa_expr.set_level_0(thread_nr);
+}
+
+void symex_level1t::operator()(ssa_exprt &ssa_expr)
+{
+  // already renamed?
+  if(!ssa_expr.get_level_1().empty())
+    return;
+
+  const irep_idt l0_name = ssa_expr.get_l1_object_identifier();
+
+  current_namest::const_iterator it = current_names.find(l0_name);
+  if(it == current_names.end())
+    return;
+
+  // rename!
+  ssa_expr.set_level_1(it->second.second);
+}

src/goto-symex/renaming_level.h

@@ -0,0 +1,94 @@
+/*******************************************************************\
+
+Module: Symbolic Execution
+
+Author: Romain Brenguier, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Renaming levels
+
+#ifndef CPROVER_GOTO_SYMEX_RENAMING_LEVEL_H
+#define CPROVER_GOTO_SYMEX_RENAMING_LEVEL_H
+
+#include <map>
+#include <unordered_set>
+
+#include <util/irep.h>
+#include <util/ssa_expr.h>
+
+struct renaming_levelt
+{
+  virtual ~renaming_levelt() = default;
+
+  typedef std::map<irep_idt, std::pair<ssa_exprt, unsigned>> current_namest;
+  current_namest current_names;
+
+  unsigned current_count(const irep_idt &identifier) const
+  {
+    const auto it = current_names.find(identifier);
+    return it == current_names.end() ? 0 : it->second.second;
+  }
+
+  void increase_counter(const irep_idt &identifier)
+  {
+    PRECONDITION(current_names.find(identifier) != current_names.end());
+    ++current_names[identifier].second;
+  }
+
+  void get_variables(std::unordered_set<ssa_exprt, irep_hash> &vars) const
+  {
+    for(const auto &pair : current_names)
+      vars.insert(pair.second.first);
+  }
+};
+
+// level 0 -- threads!
+// renaming built for one particular interleaving
+struct symex_level0t : public renaming_levelt
+{
+  void
+  operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr);
+
+  symex_level0t() = default;
+  ~symex_level0t() override = default;
+};
+
+// level 1 -- function frames
+// this is to preserve locality in case of recursion
+
+struct symex_level1t : public renaming_levelt
+{
+  void operator()(ssa_exprt &ssa_expr);
+
+  void restore_from(const current_namest &other)
+  {
+    auto it = current_names.begin();
+    for(const auto &pair : other)
+    {
+      while(it != current_names.end() && it->first < pair.first)
+        ++it;
+      if(it == current_names.end() || pair.first < it->first)
+        current_names.insert(it, pair);
+      else if(it != current_names.end())
+      {
+        PRECONDITION(it->first == pair.first);
+        it->second = pair.second;
+        ++it;
+      }
+    }
+  }
+
+  symex_level1t() = default;
+  ~symex_level1t() override = default;
+};
+
+// level 2 -- SSA
+struct symex_level2t : public renaming_levelt
+{
+  symex_level2t() = default;
+  ~symex_level2t() override = default;
+};
+
+#endif // CPROVER_GOTO_SYMEX_RENAMING_LEVEL_H

src/goto-symex/symex_function_call.cpp

@@ -330,10 +330,9 @@ void goto_symext::pop_frame(statet &state)
     state.level1.restore_from(frame.old_level1);
 
     // clear function-locals from L2 renaming
-    for(goto_symex_statet::renaming_levelt::current_namest::iterator
-        c_it=state.level2.current_names.begin();
-        c_it!=state.level2.current_names.end();
-       ) // no ++c_it
+    for(renaming_levelt::current_namest::iterator c_it =
+          state.level2.current_names.begin();
+        c_it != state.level2.current_names.end();) // no ++c_it
     {
       const irep_idt l1_o_id=c_it->second.first.get_l1_object_identifier();
       // could use iteration over local_objects as l1_o_id is prefix
@@ -345,8 +344,7 @@ void goto_symext::pop_frame(statet &state)
         ++c_it;
         continue;
       }
-      goto_symex_statet::renaming_levelt::current_namest::iterator
-        cur=c_it;
+      renaming_levelt::current_namest::iterator cur = c_it;
       ++c_it;
       state.level2.current_names.erase(cur);
     }
@@ -393,7 +391,7 @@ void goto_symext::locality(
     const irep_idt l0_name=ssa.get_identifier();
 
     // save old L1 name for popping the frame
-    statet::level1t::current_namest::const_iterator c_it=
+    symex_level1t::current_namest::const_iterator c_it =
       state.level1.current_names.find(l0_name);
 
     if(c_it!=state.level1.current_names.end())

src/goto-symex/symex_start_thread.cpp

@@ -52,9 +52,9 @@ void goto_symext::symex_start_thread(statet &state)
   // create a copy of the local variables for the new thread
   statet::framet &frame=state.top();
 
-  for(goto_symex_statet::renaming_levelt::current_namest::const_iterator
-      c_it=state.level2.current_names.begin();
-      c_it!=state.level2.current_names.end();
+  for(renaming_levelt::current_namest::const_iterator c_it =
+        state.level2.current_names.begin();
+      c_it != state.level2.current_names.end();
       ++c_it)
   {
     const irep_idt l1_o_id=c_it->second.first.get_l1_object_identifier();