Skip phi assignment if one of the merged states has an uninitialised object

tautschnig · tautschnig · commit 8f1745deba0c · 2018-12-02T09:21:02.000Z
With level-2 counters incremented on declaration and non-deterministic initialisation upon allocation, the only remaining sources are pointer dereferencing, where uninitialised objects necessarily refer to invalid objects. This is a cleaner implementation of 369f077. Removing only the code introduced in 369f077 would yield a wrong result for regression/cbmc/Local_out_of_scope3. Fixes: #1630
diff --git a/regression/cbmc-concurrency/thread_local2/main.c b/regression/cbmc-concurrency/thread_local2/main.c
@@ -0,0 +1,11 @@
+int __CPROVER_thread_local thlocal = 4;
+
+int main()
+{
+  int loc;
+
+  loc = 123;
+
+__CPROVER_ASYNC_3:
+  thlocal = loc, __CPROVER_assert(thlocal == 123, "hello");
+}
diff --git a/regression/cbmc-concurrency/thread_local2/test.desc b/regression/cbmc-concurrency/thread_local2/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
@@ -218,17 +218,6 @@ void goto_symext::symex_assign_symbol(
   guardt &guard,
   assignment_typet assignment_type)
 {
-  // do not assign to L1 objects that have gone out of scope --
-  // pointer dereferencing may yield such objects; parameters do not
-  // have an L2 entry set up beforehand either, so exempt them from
-  // this check (all other L1 objects should have seen a declaration)
-  const symbolt *s;
-  if(!ns.lookup(lhs.get_object_name(), s) &&
-     !s->is_parameter &&
-     !lhs.get_level_1().empty() &&
-     state.level2.current_count(lhs.get_identifier())==0)
-    return;
-
   exprt ssa_rhs=rhs;
 
   // put assignment guard into the rhs
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
@@ -452,17 +452,23 @@ void goto_symext::phi_function(
     //  1. Either guard is false, so we can't follow that branch.
     //  2. Either identifier is of generation zero, and so hasn't been
     //     initialized and therefor an invalid target.
-    if(dest_state.guard.is_false())
-      rhs=goto_state_rhs;
-    else if(goto_state.guard.is_false())
-      rhs=dest_state_rhs;
-    else if(goto_state.level2_current_count(l1_identifier) == 0)
+    if(
+      dest_state.guard.is_false() ||
+      dest_state.level2.current_count(l1_identifier) == 0)
     {
-      rhs = dest_state_rhs;
+      if(goto_state.level2_current_count(l1_identifier) == 0)
+        continue;
+
+      rhs = goto_state_rhs;
     }
-    else if(dest_state.level2.current_count(l1_identifier) == 0)
+    else if(
+      goto_state.guard.is_false() ||
+      goto_state.level2_current_count(l1_identifier) == 0)
     {
-      rhs = goto_state_rhs;
+      if(dest_state.level2.current_count(l1_identifier) == 0)
+        continue;
+
+      rhs = dest_state_rhs;
     }
     else
     {
