Add nondet assignment to non-zero'd allocations in symex

This change means that if a generation zero symex variable is seen it can be assumed to not have been allocated at any point and still have its default values. We use this knowledge to then not add a guard on a phi merge that has a gen zero on its lhs or rhs, instead just simply assigning the other side directly.

Author: JohnDumbell

regression/cbmc-java/phi-merge_uninitialized_values/PhiMergeUninitialized.class

@@ -0,0 +1,54 @@
+public class PhiMergeUninitialized {
+
+    public int dynamicAllocationUninitialized(Boolean trigger) {
+
+        Ephemeral obj;
+        if (trigger) {
+            obj = new Ephemeral(42);
+        } else {
+            obj = new Aetherial(20);
+        }
+
+        assert obj.val == 20;
+        return obj.val;
+    }
+
+    private Ephemeral field;
+
+    public int fieldUninitialized(Boolean trigger) {
+        if (trigger) {
+            field = new Ephemeral(42);
+        }
+
+        assert field.val == 42;
+        return field.val;
+    }
+
+    private static Ephemeral staticField;
+
+    public int staticFieldUninitialized(Boolean trigger) {
+        if (trigger) {
+            staticField = new Ephemeral(42);
+        } else {
+            staticField = new Aetherial(76);
+        }
+
+        assert staticField.val == 76;
+        return staticField.val;
+    }
+
+    class Ephemeral {
+        Ephemeral(int value) {
+            val = value;
+        }
+
+        int val;
+    }
+
+    class Aetherial extends Ephemeral {
+        Aetherial(int value) {
+            super(value);
+        }
+    }
+}
+

regression/cbmc-java/phi-merge_uninitialized_values/PhiMergeUninitialized.java

@@ -0,0 +1,16 @@
+CORE 
+PhiMergeUninitialized.class
+--function PhiMergeUninitialized.fieldUninitialized --show-vcc
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+--
+^.*:\s+(dynamic_object|new_tmp)[0-9]+(@[0-9]+)?#0\)
+^.*\?\s+(dynamic_object|new_tmp)[0-9]+(@[0-9]+)?#0\s+:
+--
+These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
+statement:
+
+ (guard ? dynamic_object2@3#1 : dynamic_object3@3#0)
+
+Should not appear. First regex deals with when the gen zero is the latter position, second when it's in the former.

regression/cbmc-java/phi-merge_uninitialized_values/field.desc

@@ -0,0 +1,16 @@
+CORE 
+PhiMergeUninitialized.class
+--function PhiMergeUninitialized.dynamicAllocationUninitialized --show-vcc
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+--
+^.*:\s+(dynamic_object|new_tmp)[0-9]+(@[0-9]+)?#0\)
+^.*\?\s+(dynamic_object|new_tmp)[0-9]+(@[0-9]+)?#0\s+:
+--
+These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
+statement:
+
+ (guard ? dynamic_object2@3#1 : dynamic_object3@3#0)
+
+Should not appear. First regex deals with when the gen zero is the latter position, second when it's in the former.

regression/cbmc-java/phi-merge_uninitialized_values/local.desc

@@ -0,0 +1,16 @@
+CORE 
+PhiMergeUninitialized.class
+--function PhiMergeUninitialized.staticFieldUninitialized --show-vcc
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+--
+^.*:\s+(dynamic_object|new_tmp)[0-9]+(@[0-9]+)?#0\)
+^.*\?\s+(dynamic_object|new_tmp)[0-9]+(@[0-9]+)?#0\s+:
+--
+These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
+statement:
+
+ (guard ? dynamic_object2@3#1 : dynamic_object3@3#0)
+
+Should not appear. First regex deals with when the gen zero is the latter position, second when it's in the former.

regression/cbmc-java/phi-merge_uninitialized_values/static_field.desc

@@ -0,0 +1,16 @@
+CORE 
+test.c
+--function dynamicAllocationUninitialized --show-vcc
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+--
+^.*:\s+dynamic_object[0-9]+(@[0-9]+)?#0\)
+^.*\?\s+dynamic_object[0-9]+(@[0-9]+)?#0\s+:
+--
+These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
+statement:
+
+ (guard ? dynamic_object2@3#1 : dynamic_object3@3#0)
+
+Should not appear. First regex deals with when the gen zero is the latter position, second when it's in the former.

regression/cbmc/phi-merge_uninitialized_values/dynamic.desc

@@ -0,0 +1,16 @@
+CORE 
+test.c
+--function globalUninitialized --show-vcc
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+--
+^.*:\s+global(@[0-9]+)?#0\)
+^.*\?\s+global(@[0-9]+)?#0\s+:
+--
+These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
+statement:
+
+ (guard ? global#1 : global#0)
+
+Should not appear. First regex deals with when the gen zero is the latter position, second when it's in the former.

regression/cbmc/phi-merge_uninitialized_values/global.desc

@@ -0,0 +1,16 @@
+CORE 
+test.c
+--function localUninitialized --show-vcc
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+--
+^.*:\s+local(@[0-9]+)?#0\)
+^.*\?\s+local(@[0-9]+)?#0\s+:
+--
+These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
+statement:
+
+ (guard ? local#1 : local#0)
+
+Should not appear. First regex deals with when the gen zero is the latter position, second when it's in the former.

regression/cbmc/phi-merge_uninitialized_values/local.desc

@@ -0,0 +1,16 @@
+CORE 
+test.c
+--function staticLocalUninitialized --show-vcc
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+--
+^.*:\s+staticLocal(@[0-9]+)?#0\)
+^.*\?\s+staticLocal(@[0-9]+)?#0\s+:
+--
+These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
+statement:
+
+ (guard ? staticLocal#1 : dynamic_object#0)
+
+Should not appear. First regex deals with when the gen zero is the latter position, second when it's in the former.

regression/cbmc/phi-merge_uninitialized_values/static_local.desc

@@ -0,0 +1,56 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void dynamicAllocationUninitialized(int trigger)
+{
+  int *obj;
+  if(trigger)
+  {
+    obj = (int *)malloc(sizeof(int));
+    *obj = 42;
+  }
+  else
+  {
+    obj = (int *)malloc(sizeof(int));
+    *obj = 76;
+  }
+
+  assert(*obj == 42);
+}
+
+int global;
+void globalUninitialized(int trigger)
+{
+  if(trigger)
+  {
+    global = 44;
+  }
+  else
+  {
+    global = 20;
+  }
+
+  assert(global == 44);
+}
+
+void staticLocalUninitialized(int trigger)
+{
+  static int staticLocal;
+  if(trigger)
+  {
+    staticLocal = 43;
+  }
+
+  assert(staticLocal == 43);
+}
+
+void localUninitialized(int trigger)
+{
+  int local;
+  if(trigger)
+  {
+    local = 24;
+  }
+
+  assert(local == 24);
+}

regression/cbmc/phi-merge_uninitialized_values/test.c

@@ -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

@@ -425,10 +425,22 @@ void goto_symext::phi_function(
 
     exprt rhs;
 
+    // Don't add a conditional to the assignment when:
+    //  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)
+    {
+      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);