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);
+}