Symex: protect level2

We really should protect the level 2 name map to prevent "allocating" a new generation
by just making one up in the local name map, cf. applying for one properly using
increase_generation.

Author: smowton

src/goto-symex/auto_objects.cpp

@@ -91,8 +91,9 @@ void goto_symext::trigger_auto_object(const exprt &expr, statet &state)
       if(has_prefix(id2string(symbol.base_name), "auto_object"))
       {
         // done already?
-        if(state.level2.current_names.find(ssa_expr.get_identifier())==
-           state.level2.current_names.end())
+        if(
+          state.get_level2().current_names.find(ssa_expr.get_identifier()) ==
+          state.get_level2().current_names.end())
         {
           initialize_auto_object(expr, state);
         }

src/goto-symex/goto_state.h

@@ -29,8 +29,15 @@ class goto_statet
   /// Distance from entry
   unsigned depth = 0;
 
+protected:
   symex_level2t level2;
 
+public:
+  const symex_level2t &get_level2() const
+  {
+    return level2;
+  }
+
   /// Uses level 1 names, and is used to do dereferencing
   value_sett value_set;
 
@@ -72,6 +79,13 @@ class goto_statet
     : guard(true_exprt(), guard_manager), source(_source)
   {
   }
+
+  void move_from(goto_statet &&other_state)
+  {
+    level2 = std::move(other_state.level2);
+    propagation = std::move(other_state.propagation);
+    value_set = std::move(other_state.value_set);
+  }
 };
 
 #endif // CPROVER_GOTO_SYMEX_GOTO_STATE_H

src/goto-symex/goto_symex_state.h

@@ -212,6 +212,12 @@ class goto_symex_statet final : public goto_statet
   /// isn't an expression keyed by it.
   void increase_generation_if_exists(const irep_idt identifier);
 
+  /// Drops an L1 name from the local L2 map
+  void drop_l1_name(symex_renaming_levelt::current_namest::const_iterator it)
+  {
+    level2.current_names.erase(it);
+  }
+
 private:
   std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider;
 

src/goto-symex/symex_atomic_section.cpp

@@ -70,7 +70,7 @@ void goto_symext::symex_atomic_end(statet &state)
   for(const auto &pair : state.written_in_atomic_section)
   {
     ssa_exprt w = pair.first;
-    w.set_level_2(state.level2.current_count(w.get_identifier()));
+    w.set_level_2(state.get_level2().current_count(w.get_identifier()));
 
     // guard is the disjunction over writes
     PRECONDITION(!pair.second.empty());

src/goto-symex/symex_function_call.cpp

@@ -349,8 +349,8 @@ static void pop_frame(goto_symext::statet &state)
     state.level1.restore_from(frame.old_level1);
 
     // clear function-locals from L2 renaming
-    for(auto c_it = state.level2.current_names.begin();
-        c_it != state.level2.current_names.end();) // no ++c_it
+    for(auto c_it = state.get_level2().current_names.begin();
+        c_it != state.get_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
@@ -364,7 +364,7 @@ static void pop_frame(goto_symext::statet &state)
       }
       auto cur = c_it;
       ++c_it;
-      state.level2.current_names.erase(cur);
+      state.drop_l1_name(cur);
     }
   }
 

src/goto-symex/symex_goto.cpp

@@ -325,9 +325,7 @@ void goto_symext::merge_goto(goto_statet &&goto_state, statet &state)
   {
     if(state.guard.is_false())
     {
-      state.level2 = std::move(goto_state.level2);
-      state.propagation = std::move(goto_state.propagation);
-      state.value_set = std::move(goto_state.value_set);
+      state.move_from(std::move(goto_state));
     }
     else
     {
@@ -516,17 +514,17 @@ void goto_symext::phi_function(
   statet &dest_state)
 {
   if(
-    goto_state.level2.current_names.empty() &&
-    dest_state.level2.current_names.empty())
+    goto_state.get_level2().current_names.empty() &&
+    dest_state.get_level2().current_names.empty())
     return;
 
   guardt diff_guard = goto_state.guard;
   // this gets the diff between the guards
   diff_guard -= dest_state.guard;
 
   for_each2(
-    goto_state.level2.current_names,
-    dest_state.level2.current_names,
+    goto_state.get_level2().current_names,
+    dest_state.get_level2().current_names,
     [&](const ssa_exprt &ssa, unsigned goto_count, unsigned dest_count) {
       merge_names(
         goto_state,

src/goto-symex/symex_start_thread.cpp

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