Don't phi-merge uninitialized objects

Author: JohnDumbell

regression/cbmc-java/PhiMergeConstantPropogation/Main.class

@@ -0,0 +1,30 @@
+public class Main {
+
+    public int phiMerge(Boolean trigger) {
+
+        Ephemeral obj;
+        if (trigger) {
+            obj = new Ephemeral(42);
+        } else {
+            obj = new Temp(20);
+        }
+
+        assert obj.val == 20;
+        return obj.val;
+    }
+
+    class Ephemeral {
+        Ephemeral(int value) {
+            val = value;
+        }
+
+        int val;
+    }
+
+    class Temp extends Ephemeral {
+        Temp(int value) {
+            super(value);
+        }
+    }
+}
+

regression/cbmc-java/PhiMergeConstantPropogation/Main.java

@@ -0,0 +1,7 @@
+CORE 
+Main.class
+--function Main.phiMerge --show-vcc
+activate-multi-line-match
+^.*dynamic_object2#2 == \{ \.@class_identifier="java::Main\$Temp",\s*\.@lock=false \}$
+^EXIT=0$
+^SIGNAL=0$

regression/cbmc-java/PhiMergeConstantPropogation/test.desc

@@ -174,7 +174,7 @@ ($$$$$$$$$)
             binmode $fh;
             my $whole_file = <$fh>;
             $whole_file =~ s/\r\n/\n/g;
-            my $is_match = $whole_file =~ /$result/;
+            my $is_match = $whole_file =~ /$result/m;
             $r = ($included ? !$is_match : $is_match);
           }
           else

regression/test.pl

@@ -22,13 +22,19 @@ void goto_symext::do_simplify(exprt &expr)
     simplify(expr, ns);
 }
 
+nondet_symbol_exprt goto_symext::build_symex_nondet(typet &type)
+{
+  irep_idt identifier = "symex::nondet" + std::to_string(nondet_count++);
+  nondet_symbol_exprt new_expr(identifier, type);
+  return new_expr;
+}
+
 void goto_symext::replace_nondet(exprt &expr)
 {
   if(expr.id()==ID_side_effect &&
      expr.get(ID_statement)==ID_nondet)
   {
-    irep_idt identifier="symex::nondet"+std::to_string(nondet_count++);
-    nondet_symbol_exprt new_expr(identifier, expr.type());
+    nondet_symbol_exprt new_expr = build_symex_nondet(expr.type());
     new_expr.add_source_location()=expr.source_location();
     expr.swap(new_expr);
   }

src/goto-symex/goto_symex.cpp

@@ -376,6 +376,8 @@ class goto_symext
     exprt &code,
     const irep_idt &identifier);
 
+  nondet_symbol_exprt build_symex_nondet(typet &type);
+
   // exceptions
   void symex_throw(statet &);
   void symex_catch(statet &);

src/goto-symex/goto_symex.h

@@ -184,6 +184,12 @@ void goto_symext::symex_allocate(
     else
       throw "failed to zero initialize dynamic object";
   }
+  else
+  {
+    exprt nondet = build_symex_nondet(object_type);
+    code_assignt assignment(value_symbol.symbol_expr(), nondet);
+    symex_assign(state, assignment);
+  }
 
   exprt rhs;
 

src/goto-symex/symex_builtin_functions.cpp

@@ -429,6 +429,14 @@ void goto_symext::phi_function(
       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)
+    {
+      rhs = dest_state_rhs;
+    }
+    else if(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);