Document renaming_level struct

Author: romainbrenguier

src/goto-symex/renaming_level.h

@@ -18,34 +18,43 @@ Author: Romain Brenguier, [email protected]
 #include <util/irep.h>
 #include <util/ssa_expr.h>
 
+/// Wrapper for a \c current_names map, which maps each identifier to an SSA
+/// expression and a counter.
+/// This is extended by the different symex_level structures which are used
+/// during symex to ensure static single assignment (SSA) form.
 struct renaming_levelt
 {
   virtual ~renaming_levelt() = default;
 
+  /// Map identifier to ssa_exprt and counter
   typedef std::map<irep_idt, std::pair<ssa_exprt, unsigned>> current_namest;
   current_namest current_names;
 
+  /// Counter corresponding to an identifier
   unsigned current_count(const irep_idt &identifier) const
   {
     const auto it = current_names.find(identifier);
     return it == current_names.end() ? 0 : it->second.second;
   }
 
+  /// Increase the counter corresponding to an identifier
   void increase_counter(const irep_idt &identifier)
   {
     PRECONDITION(current_names.find(identifier) != current_names.end());
     ++current_names[identifier].second;
   }
 
+  /// Add the \c ssa_exprt of current_names to vars
   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
+/// Functor to set the level 0 renaming of SSA expressions.
+/// Level 0 corresponds to threads.
+/// The renaming is built for one particular interleaving.
 struct symex_level0t : public renaming_levelt
 {
   void
@@ -55,20 +64,23 @@ struct symex_level0t : public renaming_levelt
   ~symex_level0t() override = default;
 };
 
-// level 1 -- function frames
-// this is to preserve locality in case of recursion
-
+/// Functor to set the level 1 renaming of SSA expressions.
+/// Level 1 corresponds to function frames.
+/// This is to preserve locality in case of recursion
 struct symex_level1t : public renaming_levelt
 {
   void operator()(ssa_exprt &ssa_expr);
 
+  /// Insert the content of \p other into this renaming
   void restore_from(const current_namest &other);
 
   symex_level1t() = default;
   ~symex_level1t() override = default;
 };
 
-// level 2 -- SSA
+/// Functor to set the level 2 renaming of SSA expressions.
+/// Level 2 corresponds to SSA.
+/// This is to ensure each variable is only assigned once.
 struct symex_level2t : public renaming_levelt
 {
   symex_level2t() = default;