From 369f077d2efe8ffee0aa54b2583ba36ffbeb07c8 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 11 Jul 2017 16:19:33 +0100
Subject: [PATCH] Do not assign to objects that have gone out of scope

Pointer dereferencing may yield objects that have meanwhile gone out of scope.
Assigning to them is unnecessary, and performing a merge on those would yield
inconsistent equations (as witnessed by the included regression test).

Filtering out the merge in phi nodes is not easily possible as there are several
cases where it is permissible that only one of the states entering the phi node
has an (L1) object, such as declarations only seen in one branch.

Fixes: #1115
---
 regression/cbmc/Local_out_of_scope3/main.c    | 24 +++++++++++++++++++
 regression/cbmc/Local_out_of_scope3/test.desc |  8 +++++++
 src/goto-symex/symex_assign.cpp               | 11 +++++++++
 3 files changed, 43 insertions(+)
 create mode 100644 regression/cbmc/Local_out_of_scope3/main.c
 create mode 100644 regression/cbmc/Local_out_of_scope3/test.desc

diff --git a/regression/cbmc/Local_out_of_scope3/main.c b/regression/cbmc/Local_out_of_scope3/main.c
new file mode 100644
index 00000000000..977efe689a7
--- /dev/null
+++ b/regression/cbmc/Local_out_of_scope3/main.c
@@ -0,0 +1,24 @@
+unsigned int *GLOBAL_POINTER[1];
+
+int index;
+
+void f(void)
+{
+  unsigned int actual=0u;
+  GLOBAL_POINTER[0] = &actual;
+
+  if(index==0)
+    *GLOBAL_POINTER[index] = 1u;
+  else
+    actual = 2u;
+
+  __CPROVER_assume(1u == actual);
+}
+
+void main(void)
+{
+  index=nondet_int();
+  f();
+  f();
+  __CPROVER_assert(0==1, "");
+}
diff --git a/regression/cbmc/Local_out_of_scope3/test.desc b/regression/cbmc/Local_out_of_scope3/test.desc
new file mode 100644
index 00000000000..6de79559914
--- /dev/null
+++ b/regression/cbmc/Local_out_of_scope3/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 047f3be8325..de5ba76df76 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -209,6 +209,17 @@ 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