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,56 @@
+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 local;
+
+    public int localUninitialized(Boolean trigger) {
+        if (trigger) {
+            local = new Ephemeral(42);
+        } else {
+            local = new Aetherial(50);
+        }
+
+        assert local.val == 42;
+        return local.val;
+    }
+
+    private static Ephemeral staticLocal;
+
+    public int staticLocalUninitialized(Boolean trigger) {
+        if (trigger) {
+            staticLocal = new Ephemeral(42);
+        } else {
+            staticLocal = new Aetherial(76);
+        }
+
+        assert staticLocal.val == 76;
+        return staticLocal.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,15 @@
+CORE 
+PhiMergeUninitialized.class
+--function PhiMergeUninitialized.localUninitialized --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:
+
+ (guard ? dynamic_object2@3#1 : dynamic_object3@3#0)
+
+First regex deals with the form : variable#0), second deals with ? variable#0 :

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

@@ -0,0 +1,15 @@
+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:
+
+ (guard ? dynamic_object2@3#1 : dynamic_object3@3#0)
+
+First regex deals with the form : variable#0), second deals with ? variable#0 :

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

@@ -0,0 +1,15 @@
+CORE 
+PhiMergeUninitialized.class
+--function PhiMergeUninitialized.staticLocalUninitialized --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:
+
+ (guard ? dynamic_object2@3#1 : dynamic_object3@3#0)
+
+First regex deals with the form : variable#0), second deals with ? variable#0 :

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

@@ -0,0 +1,15 @@
+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:
+
+ (guard ? dynamic_object2@3#1 : dynamic_object3@3#0)
+
+First regex deals with the form : variable#0), second deals with ? variable#0 :

regression/cbmc/phi-merge_uninitialized_values/dynamic.desc

@@ -0,0 +1,15 @@
+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:
+
+ (guard ? dynamic_object2@3#1 : dynamic_object3@3#0)
+
+First regex deals with the form : variable#0), second deals with ? variable#0 :

regression/cbmc/phi-merge_uninitialized_values/global.desc

@@ -0,0 +1,15 @@
+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:
+
+ (guard ? dynamic_object2@3#1 : dynamic_object3@3#0)
+
+First regex deals with the form : variable#0), second deals with ? variable#0 :

regression/cbmc/phi-merge_uninitialized_values/local.desc

@@ -0,0 +1,15 @@
+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:
+
+ (guard ? dynamic_object2@3#1 : dynamic_object3@3#0)
+
+First regex deals with the form : variable#0), second deals with ? variable#0 :

regression/cbmc/phi-merge_uninitialized_values/static_local.desc

@@ -0,0 +1,55 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void dynamicAllocationUninitialized(int trigger)
+{
+  int *obj;
+  obj = (int*)malloc(sizeof(int));
+  if(trigger)
+  {
+    *obj = 42;
+  }
+  else
+  {
+    *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);