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,9 @@
+CORE 
+PhiMergeUninitialized.class
+--function PhiMergeUninitialized.dynamicAllocationUninitialized --show-vcc
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+--
+^.*: (dynamic_object|new_tmp[0-9]+(@[0-9]+)?)[0-9]+#0\)
+^.*\? (dynamic_object|new_tmp[0-9]+(@[0-9]+)?)[0-9]+#0

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

@@ -0,0 +1,9 @@
+CORE 
+PhiMergeUninitialized.class
+--function PhiMergeUninitialized.localUninitialized --show-vcc
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+--
+^.*: (dynamic_object|new_tmp[0-9]+(@[0-9]+)?)[0-9]+#0\)
+^.*\? (dynamic_object|new_tmp[0-9]+(@[0-9]+)?)[0-9]+#0

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

@@ -0,0 +1,9 @@
+CORE 
+PhiMergeUninitialized.class
+--function PhiMergeUninitialized.staticLocalUninitialized --show-vcc
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+--
+^.*: (dynamic_object|new_tmp[0-9]+(@[0-9]+)?)[0-9]+#0\)
+^.*\? (dynamic_object|new_tmp[0-9]+(@[0-9]+)?)[0-9]+#0

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

@@ -0,0 +1,9 @@
+CORE 
+test.c
+--function dynamicAllocationUninitialized --show-vcc
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+--
+^.*: (dynamic_object|new_tmp[0-9]+(@[0-9]+)?)[0-9]+#0\)
+^.*\? (dynamic_object|new_tmp[0-9]+(@[0-9]+)?)[0-9]+#0

regression/cbmc/phi-merge_uninitialized_values/local.desc

@@ -0,0 +1,9 @@
+CORE 
+test.c
+--function staticLocalUninitialized --show-vcc
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+--
+^.*: (dynamic_object|new_tmp[0-9]+(@[0-9]+)?)[0-9]+#0\)
+^.*\? (dynamic_object|new_tmp[0-9]+(@[0-9]+)?)[0-9]+#0

regression/cbmc/phi-merge_uninitialized_values/static_global.desc

@@ -0,0 +1,34 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void dynamicAllocationUninitialized(int trigger)
+{
+  int *obj;
+  obj = malloc(sizeof(int));
+  if(trigger)
+  {
+    *obj = 42;
+  }
+  else
+  {
+    *obj = 20;
+  }
+
+  assert(*obj == 20);
+}
+
+int *staticLocal;
+int staticLocalUninitialized(int trigger)
+{
+  staticLocal = malloc(sizeof(int));
+  if(trigger)
+  {
+    *staticLocal = 42;
+  }
+  else
+  {
+    *staticLocal = 76;
+  }
+
+  assert(*staticLocal == 76);
+}

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 &);