Explicitly initialise non-static objects with non-deterministic values

Author: tautschnig

regression/cbmc/constant_folding2/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc/graphml_witness1/test.desc

@@ -54,12 +54,6 @@ main.c
       <data key="startline">21</data>
     </edge>
     <node id="[0-9\.]*"/>
-    <edge source="[0-9\.]*" target="[0-9\.]*">
-      <data key="originfile">main.c</data>
-      <data key="startline">29</data>
-      <data key="assumption.scope">main</data>
-    </edge>
-    <node id="[0-9\.]*"/>
     <edge source="[0-9\.]*" target="[0-9\.]*">
       <data key="originfile">main.c</data>
       <data key="startline">15</data>

regression/cbmc/struct10/main.c

@@ -1,3 +1,4 @@
+<<<<<<< HEAD
 #include <assert.h>
 
 struct S
@@ -8,12 +9,25 @@ struct S
 struct T
 {
   struct S a[2];
+=======
+struct test_struct
+{
+  int a[2];
+  int b;
+>>>>>>> 2846e8c... Explicitly initialise non-static objects with non-deterministic values
 };
 
 int main()
 {
+<<<<<<< HEAD
   struct T t;
   t.a[1].x = 42;
   assert(t.a[1].x == 42);
   return 0;
+=======
+  struct test_struct test;
+  test.a[1] = 1;
+  test.b = 1;
+  __CPROVER_assert(test.a[1] == 0, "");
+>>>>>>> 2846e8c... Explicitly initialise non-static objects with non-deterministic values
 }

regression/cbmc/struct10/test.desc

@@ -1,8 +1,24 @@
 CORE
 main.c
+<<<<<<< HEAD
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+=======
+--trace
+test.a\[1ll?\]=1 \(00000000000000000000000000000001\)$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+\(\?\)
+--
+Earlier versions of non-deterministic initialisation would cause trace output
+including
+
+test.a[1l]={ .a={ 0, 1 }, .b=0 }.a[1l] (?)
+>>>>>>> 2846e8c... Explicitly initialise non-static objects with non-deterministic values

src/goto-programs/graphml_witness.cpp

@@ -145,13 +145,15 @@ static bool filter_out(
   const goto_tracet::stepst::const_iterator &prev_it,
   goto_tracet::stepst::const_iterator &it)
 {
+  // use the goto program's assignment type as declarations may be
+  // recorded as (non-deterministic) assignments in the trace
   if(it->hidden &&
      (!it->pc->is_assign() ||
       to_code_assign(it->pc->code).rhs().id()!=ID_side_effect ||
       to_code_assign(it->pc->code).rhs().get(ID_statement)!=ID_nondet))
     return true;
 
-  if(!it->is_assignment() && !it->is_goto() && !it->is_assert())
+  if(!it->pc->is_assign() && !it->is_goto() && !it->is_assert())
     return true;
 
   // we filter out steps with the same source location

src/goto-symex/goto_symex.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include "goto_symex.h"
 
 #include <util/simplify_expr.h>
+#include <util/zero_initializer.h>
 
 unsigned goto_symext::dynamic_counter=0;
 
@@ -27,3 +28,31 @@ nondet_symbol_exprt symex_nondet_generatort::operator()(typet &type)
   nondet_symbol_exprt new_expr(identifier, type);
   return new_expr;
 }
+<<<<<<< HEAD
+=======
+
+void goto_symext::replace_nondet(exprt &expr)
+{
+  if(expr.id()==ID_side_effect &&
+     expr.get(ID_statement)==ID_nondet)
+  {
+    exprt nondet = nondet_initializer(
+      expr.type(), expr.source_location(), ns, log.get_message_handler());
+
+    // recursively replace nondet fields in structs or arrays
+    if(nondet.id() != ID_side_effect)
+    {
+      replace_nondet(nondet);
+      expr.swap(nondet);
+      return;
+    }
+
+    nondet_symbol_exprt new_expr = build_symex_nondet(expr.type());
+    new_expr.add_source_location()=expr.source_location();
+    expr.swap(new_expr);
+  }
+  else
+    Forall_operands(it, expr)
+      replace_nondet(*it);
+}
+>>>>>>> 2846e8c... Explicitly initialise non-static objects with non-deterministic values

src/goto-symex/goto_symex.h

@@ -250,7 +250,26 @@ class goto_symext
 
   // guards
 
+<<<<<<< HEAD
   const irep_idt guard_identifier;
+=======
+  irep_idt guard_identifier;
+
+  // symex
+  irep_idt init_l1;
+
+  virtual void symex_transition(
+    statet &,
+    goto_programt::const_targett to,
+    bool is_backwards_goto=false);
+
+  virtual void symex_transition(statet &state)
+  {
+    goto_programt::const_targett next=state.source.pc;
+    ++next;
+    symex_transition(state, next);
+  }
+>>>>>>> 2846e8c... Explicitly initialise non-static objects with non-deterministic values
 
   virtual void symex_goto(statet &);
   virtual void symex_start_thread(statet &);

src/goto-symex/symex_builtin_functions.cpp

@@ -178,9 +178,23 @@ void goto_symext::symex_allocate(
   }
   else
   {
+<<<<<<< HEAD
     const exprt nondet = build_symex_nondet(object_type);
     const code_assignt assignment(value_symbol.symbol_expr(), nondet);
     symex_assign(state, assignment);
+=======
+    side_effect_expr_nondett init(object_type);
+    replace_nondet(init);
+
+    guardt guard;
+    symex_assign_symbol(
+      state,
+      ssa_exprt(value_symbol.symbol_expr()),
+      nil_exprt(),
+      init,
+      guard,
+      symex_targett::assignment_typet::HIDDEN);
+>>>>>>> 2846e8c... Explicitly initialise non-static objects with non-deterministic values
   }
 
   exprt rhs;

src/goto-symex/symex_decl.cpp

@@ -15,8 +15,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/std_expr.h>
 
-#include <pointer-analysis/add_failed_symbols.h>
-
 #include <analyses/dirty.h>
 
 void goto_symext::symex_decl(statet &state)
@@ -45,6 +43,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   state.rename(ssa.type(), l1_identifier, ns);
   ssa.update_type();
 
+<<<<<<< HEAD
   // in case of pointers, put something into the value set
   if(ns.follow(expr.type()).id()==ID_pointer)
   {
@@ -76,6 +75,25 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   state.record_events=false;
   state.rename(ssa, ns);
   state.record_events=record_events;
+=======
+  // L2 renaming
+  // inlining may yield multiple declarations of the same identifier
+  // within the same L1 context
+  if(state.level2.current_names.find(l1_identifier)==
+     state.level2.current_names.end())
+    state.level2.current_names[l1_identifier]=std::make_pair(ssa, 0);
+  init_l1 = l1_identifier;
+
+  // optimisation: skip non-deterministic initialisation if the next instruction
+  // will take care of initialisation (but ensure int x=x; is handled properly)
+  goto_programt::const_targett next = std::next(state.source.pc);
+  if(
+    next->is_assign() && to_code_assign(next->code).lhs() == expr &&
+    to_code_assign(next->code).rhs().is_constant())
+  {
+    return;
+  }
+>>>>>>> 2846e8c... Explicitly initialise non-static objects with non-deterministic values
 
   // we hide the declaration of auxiliary variables
   // and if the statement itself is hidden
@@ -84,10 +102,16 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
     state.top().hidden_function ||
     state.source.pc->source_location.get_hide();
 
-  target.decl(
-    state.guard.as_expr(),
+  side_effect_expr_nondett init(ssa.type());
+  replace_nondet(init);
+
+  guardt guard;
+  symex_assign_symbol(
+    state,
     ssa,
-    state.source,
+    nil_exprt(),
+    init,
+    guard,
     hidden?
       symex_targett::assignment_typet::HIDDEN:
       symex_targett::assignment_typet::STATE);