From c4636939fb04b9c1e7e536c9736e2ed7dc2e9b61 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 3 Sep 2024 20:25:43 +0000
Subject: [PATCH] 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
---
 regression/cbmc/Local_out_of_scope5/main.c    | 16 ++++++++++++++++
 regression/cbmc/Local_out_of_scope5/test.desc |  8 ++++++++
 src/goto-symex/goto_state.h                   |  2 ++
 src/goto-symex/goto_symex_state.h             |  3 +--
 src/goto-symex/symex_main.cpp                 |  2 ++
 src/goto-symex/symex_start_thread.cpp         |  4 ++++
 6 files changed, 33 insertions(+), 2 deletions(-)
 create mode 100644 regression/cbmc/Local_out_of_scope5/main.c
 create mode 100644 regression/cbmc/Local_out_of_scope5/test.desc

diff --git a/regression/cbmc/Local_out_of_scope5/main.c b/regression/cbmc/Local_out_of_scope5/main.c
new file mode 100644
index 00000000000..bc7981cd6df
--- /dev/null
+++ b/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;
+  }
+}
diff --git a/regression/cbmc/Local_out_of_scope5/test.desc b/regression/cbmc/Local_out_of_scope5/test.desc
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ b/regression/cbmc/Local_out_of_scope5/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/goto-symex/goto_state.h b/src/goto-symex/goto_state.h
index 5fa398048bc..bda115284a0 100644
--- a/src/goto-symex/goto_state.h
+++ b/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;
diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h
index fa7c06895f5..ec17bf8e416 100644
--- a/src/goto-symex/goto_symex_state.h
+++ b/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)
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index de1e7f1f388..234249ddd67 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/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;
diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp
index 0681eb60413..da331d8ffba 100644
--- a/src/goto-symex/symex_start_thread.cpp
+++ b/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();