From 4ace868acc0488aeacd57d3817dd80a47b570788 Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Thu, 26 Apr 2018 15:23:01 +0100
Subject: [PATCH] Symex: don't phi-merge Java dynamic objects with
 uninitialised data

Previously given code like "A a = null; if(x) a = new A(); // PHI", at the merge point marked PHI
symex would merge two versions of the newly allocated dynamic object: the one initialised by the A()
constructor, and the one carrying uninitialised data (an unbound symbol with a name like dynamic_object1#0)

This means all subsequent accesses to the dynamic object would operate on `x ? dynamic_object1#2 : dynamic_object1#0`,
stymying future constant propagation and expression simplification.

By observing that in Java having a pointer to an object implies it has been initialised, we can safely throw away
the dynamic_object1#0 case and thus improve constant propagation.
---
 src/goto-symex/goto_symex.h   |  3 +++
 src/goto-symex/symex_goto.cpp | 20 ++++++++++++++++++++
 2 files changed, 23 insertions(+)

diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index 7d7edb8891f..c5228bb270f 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -318,6 +318,9 @@ class goto_symext
     const statet::goto_statet &goto_state,
     statet &dest);
 
+  bool may_assume_unreachable_if_uninitialised(const symbolt &object_symbol)
+    const;
+
   void phi_function(
     const statet::goto_statet &goto_state,
     statet &);
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index e25add14741..3f1218aefa7 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -344,6 +344,14 @@ void goto_symext::merge_value_sets(
   dest.value_set.make_union(src.value_set);
 }
 
+bool goto_symext::may_assume_unreachable_if_uninitialised(
+  const symbolt &object_symbol) const
+{
+  return
+    language_mode == ID_java &&
+    ns.follow(object_symbol.type).id() == ID_struct;
+}
+
 void goto_symext::phi_function(
   const statet::goto_statet &goto_state,
   statet &dest_state)
@@ -424,11 +432,23 @@ void goto_symext::phi_function(
     }
 
     exprt rhs;
+    bool object_unreachable_if_uninitialised =
+      may_assume_unreachable_if_uninitialised(symbol);
 
     if(dest_state.guard.is_false())
       rhs=goto_state_rhs;
     else if(goto_state.guard.is_false())
       rhs=dest_state_rhs;
+    else if(object_unreachable_if_uninitialised &&
+            goto_state.level2_current_count(l1_identifier) == 0)
+    {
+      rhs = dest_state_rhs;
+    }
+    else if(object_unreachable_if_uninitialised &&
+            dest_state.level2.current_count(l1_identifier) == 0)
+    {
+      rhs = goto_state_rhs;
+    }
     else
     {
       rhs=if_exprt(diff_guard.as_expr(), goto_state_rhs, dest_state_rhs);