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

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,29 @@
+#include <stdlib.h>
+#include <assert.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 &);