goto-symex: move level1 map to goto_statet

A local variable may have left the scope on a branch, but may still
exist via another path. Upon merging paths we must not lose such
objects.

Fixes: #8437

Author: tautschnig

regression/cbmc/Local_out_of_scope5/main.c

@@ -0,0 +1,16 @@
+int main()
+{
+  int jumpguard;
+  jumpguard = jumpguard | 1;
+label_1:
+  while(1)
+  {
+    int canary = 1;
+    if(jumpguard == 0)
+    {
+      goto label_1;
+    }
+    __CPROVER_assert(canary, "should pass");
+    break;
+  }
+}

regression/cbmc/Local_out_of_scope5/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/goto-symex/goto_state.h

@@ -38,6 +38,8 @@ class goto_statet
   symex_level2t level2;
 
 public:
+  symex_level1t level1;
+
   /// This is used for eliminating repeated complicated dereferences.
   /// \see goto_symext::dereference_rec
   sharing_mapt<exprt, symbol_exprt, false, irep_hash> dereference_cache;

src/goto-symex/goto_symex_state.h

@@ -70,8 +70,6 @@ class goto_symex_statet final : public goto_statet
   guard_managert &guard_manager;
   symex_target_equationt *symex_target;
 
-  symex_level1t level1;
-
   /// Rewrites symbol expressions in \ref exprt, applying a suffix to each
   /// symbol reflecting its most recent version, which differs depending on
   /// which level you requested. Each level also updates its predecessors, so
@@ -188,6 +186,7 @@ class goto_symex_statet final : public goto_statet
     irep_idt function_id;
     guardt guard;
     call_stackt call_stack;
+    symex_level1t level1;
     std::map<irep_idt, unsigned> function_frame;
     unsigned atomic_section_id = 0;
     explicit threadt(guard_managert &guard_manager)

src/goto-symex/symex_main.cpp

@@ -291,6 +291,8 @@ switch_to_thread(goto_symex_statet &state, const unsigned int thread_nb)
   state.source.pc = state.threads[thread_nb].pc;
   state.source.function_id = state.threads[thread_nb].function_id;
 
+  state.level1.restore_from(state.threads[thread_nb].level1);
+
   state.guard = state.threads[thread_nb].guard;
   // A thread's initial state is certainly reachable:
   state.reachable = true;

src/goto-symex/symex_start_thread.cpp

@@ -117,6 +117,10 @@ void goto_symext::symex_start_thread(statet &state)
     }
   }
 
+  // retain the current set of objects so as to restore when symbolically
+  // executing the thread
+  new_thread.level1 = state.level1;
+
   // initialize all variables marked thread-local
   const symbol_tablet &symbol_table=ns.get_symbol_table();