From e743f02fc3d41057083af2145ca98044147a0059 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 19 Dec 2018 12:21:39 +0000
Subject: [PATCH 1/2] Fix handling of extern symbols in phi_function

In 646cf29941499, initialisation of dynamic objects was added, but extern
symbols were not considered. Includes a test that fails without this fix.
---
 regression/cbmc/extern3/main.c    | 11 +++++++++++
 regression/cbmc/extern3/test.desc | 10 ++++++++++
 src/goto-symex/symex_goto.cpp     |  4 ++--
 3 files changed, 23 insertions(+), 2 deletions(-)
 create mode 100644 regression/cbmc/extern3/main.c
 create mode 100644 regression/cbmc/extern3/test.desc

diff --git a/regression/cbmc/extern3/main.c b/regression/cbmc/extern3/main.c
new file mode 100644
index 00000000000..0b623409d55
--- /dev/null
+++ b/regression/cbmc/extern3/main.c
@@ -0,0 +1,11 @@
+#include <assert.h>
+
+extern int x;
+
+int main(int argc, char *argv[])
+{
+  if(argc > 5)
+    x = 42;
+
+  __CPROVER_assert(x == 42, "should fail");
+}
diff --git a/regression/cbmc/extern3/test.desc b/regression/cbmc/extern3/test.desc
new file mode 100644
index 00000000000..578c27b1fa2
--- /dev/null
+++ b/regression/cbmc/extern3/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+The change to phi_function of 646cf29941499 failed to consider the case of
+extern variables, which we leave uninitialised.
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index 05429aa412d..02ff399b22a 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -473,11 +473,11 @@ static void merge_names(
     rhs = goto_state_rhs;
   else if(goto_state.guard.is_false())
     rhs = dest_state_rhs;
-  else if(goto_count == 0)
+  else if(goto_count == 0 && symbol.value.is_not_nil())
   {
     rhs = dest_state_rhs;
   }
-  else if(dest_count == 0)
+  else if(dest_count == 0 && symbol.value.is_not_nil())
   {
     rhs = goto_state_rhs;
   }

From eaa7d93ac4d9882149fb0952c7d1177ce1840236 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 14 May 2018 11:59:23 +0100
Subject: [PATCH 2/2] Skip phi assignment if one of the merged states has an
 uninitialised object

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 369f077d2e. Removing only the code
introduced in 369f077d2e would yield a wrong result for
regression/cbmc/Local_out_of_scope3.

Fixes: #1630
---
 regression/cbmc-concurrency/thread_local2/main.c    | 11 +++++++++++
 regression/cbmc-concurrency/thread_local2/test.desc |  8 ++++++++
 src/goto-symex/symex_assign.cpp                     | 11 -----------
 src/goto-symex/symex_goto.cpp                       |  9 ++++++++-
 4 files changed, 27 insertions(+), 12 deletions(-)
 create mode 100644 regression/cbmc-concurrency/thread_local2/main.c
 create mode 100644 regression/cbmc-concurrency/thread_local2/test.desc

diff --git a/regression/cbmc-concurrency/thread_local2/main.c b/regression/cbmc-concurrency/thread_local2/main.c
new file mode 100644
index 00000000000..a2a67473b9d
--- /dev/null
+++ 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
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ 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
index 9297145c1f5..fde8a2b3bdb 100644
--- 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
index 02ff399b22a..3823cfecff0 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -423,7 +423,14 @@ static void merge_names(
   if(goto_count == dest_count)
     return; // not at all changed
 
-  // changed!
+  // changed - but only on a branch that is now dead, and the other branch is
+  // uninitialized/invalid
+  if(
+    (dest_state.guard.is_false() && goto_count == 0) ||
+    (goto_state.guard.is_false() && dest_count == 0))
+  {
+    return;
+  }
 
   // shared variables are renamed on every access anyway, we don't need to
   // merge anything