Merge pull request diffblue#415 from diffblue/CBMC_merge_2018-05-15

Cbmc merge 2018-05-15

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

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

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

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

cbmc/regression/cbmc-java/phi-merge_uninitialized_values/local.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.

cbmc/regression/cbmc-java/phi-merge_uninitialized_values/static_field.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.

cbmc/regression/cbmc/phi-merge_uninitialized_values/dynamic.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.

cbmc/regression/cbmc/phi-merge_uninitialized_values/global.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.

cbmc/regression/cbmc/phi-merge_uninitialized_values/local.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.

cbmc/regression/cbmc/phi-merge_uninitialized_values/static_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.

cbmc/regression/cbmc/phi-merge_uninitialized_values/test.c

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

cbmc/regression/test.pl

@@ -174,7 +174,7 @@ ($$$$$$$$$)
             binmode $fh;
             my $whole_file = <$fh>;
             $whole_file =~ s/\r\n/\n/g;
-            my $is_match = $whole_file =~ /$result/;
+            my $is_match = $whole_file =~ /$result/m;
             $r = ($included ? !$is_match : $is_match);
           }
           else

cbmc/scripts/glucose-syrup-patch

@@ -43,6 +43,36 @@ diff -rupNw glucose-syrup/core/SolverTypes.h glucose-syrup-patched/core/SolverTy
 
      friend class ClauseAllocator;
 
+diff -rupNw glucose-syrup/mtl/Clone.h glucose-syrup-patched/mtl/Clone.h
+--- glucose-syrup/mtl/Clone.h	2014-10-03 11:10:22.000000000 +0200
++++ glucose-syrup-patched/mtl/Clone.h	2018-05-10 12:35:25.150491249 +0200
+@@ -8,6 +8,6 @@ namespace Glucose {
+         public:
+           virtual Clone* clone() const = 0;
+     };
+-};
++}
+
+ #endif
+\ No newline at end of file
+diff -rupNw glucose-syrup/mtl/Clone.h~ glucose-syrup-patched/mtl/Clone.h~
+--- glucose-syrup/mtl/Clone.h~	1970-01-01 01:00:00.000000000 +0100
++++ glucose-syrup-patched/mtl/Clone.h~	2018-04-21 16:58:22.950005391 +0200
+@@ -0,0 +1,13 @@
++#ifndef Glucose_Clone_h
++#define Glucose_Clone_h
++
++
++namespace Glucose {
++
++    class Clone {
++        public:
++          virtual Clone* clone() const = 0;
++    };
++};
++
++#endif
+\ No newline at end of file
 diff -rupNw glucose-syrup/mtl/IntTypes.h glucose-syrup-patched/mtl/IntTypes.h
 --- glucose-syrup/mtl/IntTypes.h	2014-10-03 11:10:22.000000000 +0200
 +++ glucose-syrup-patched/mtl/IntTypes.h	2018-04-21 16:58:22.950005391 +0200

cbmc/src/goto-programs/goto_trace.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening
 #include <ostream>
 
 #include <util/arith_tools.h>
+#include <util/format_expr.h>
 #include <util/symbol.h>
 
 #include <ansi-c/printf_formatter.h>
@@ -61,61 +62,45 @@ void goto_trace_stept::output(
     UNREACHABLE;
   }
 
-  if(type==typet::ASSERT || type==typet::ASSUME || type==typet::GOTO)
+  if(is_assert() || is_assume() || is_goto())
     out << " (" << cond_value << ")";
+  else if(is_function_call() || is_function_return())
+    out << ' ' << identifier;
 
   if(hidden)
     out << " hidden";
 
-  out << "\n";
+  out << '\n';
+
+  if(is_assignment())
+  {
+    out << "  " << format(full_lhs)
+        << " = " << format(full_lhs_value)
+        << '\n';
+  }
 
   if(!pc->source_location.is_nil())
-    out << pc->source_location << "\n";
-
-  if(pc->is_goto())
-    out << "GOTO   ";
-  else if(pc->is_assume())
-    out << "ASSUME ";
-  else if(pc->is_assert())
-    out << "ASSERT ";
-  else if(pc->is_dead())
-    out << "DEAD   ";
-  else if(pc->is_other())
-    out << "OTHER  ";
-  else if(pc->is_assign())
-    out << "ASSIGN ";
-  else if(pc->is_decl())
-    out << "DECL   ";
-  else if(pc->is_function_call())
-    out << "CALL   ";
-  else
-    out << "(?)    ";
+    out << pc->source_location << '\n';
 
-  out << "\n";
+  out << pc->type << '\n';
 
-  if((pc->is_other() && lhs_object.is_not_nil()) || pc->is_assign())
-  {
-    irep_idt identifier=lhs_object.get_object_name();
-    out << "  " << from_expr(ns, identifier, lhs_object.get_original_expr())
-        << " = " << from_expr(ns, identifier, lhs_object_value)
-        << "\n";
-  }
-  else if(pc->is_assert())
+  if(pc->is_assert())
   {
     if(!cond_value)
     {
-      out << "Violated property:" << "\n";
+      out << "Violated property:" << '\n';
       if(pc->source_location.is_nil())
-        out << "  " << pc->source_location << "\n";
+        out << "  " << pc->source_location << '\n';
 
-      if(comment!="")
-        out << "  " << comment << "\n";
-      out << "  " << from_expr(ns, pc->function, pc->guard) << "\n";
-      out << "\n";
+      if(!comment.empty())
+        out << "  " << comment << '\n';
+
+      out << "  " << format(pc->guard) << '\n';
+      out << '\n';
     }
   }
 
-  out << "\n";
+  out << '\n';
 }
 
 std::string trace_value_binary(

cbmc/src/goto-symex/goto_symex.cpp

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