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

@@ -0,0 +1,13 @@
+struct test_struct
+{
+  int a[2];
+  int b;
+};
+
+int main()
+{
+  struct test_struct test;
+  test.a[1] = 1;
+  test.b = 1;
+  __CPROVER_assert(test.a[1] == 0, "");
+}

regression/cbmc/struct10/test.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+--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] (?)

src/goto-programs/graphml_witness.cpp

@@ -144,13 +144,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, kroening@kroening.com
 #include "goto_symex.h"
 
 #include <util/simplify_expr.h>
+#include <util/zero_initializer.h>
 
 unsigned goto_symext::nondet_count=0;
 unsigned goto_symext::dynamic_counter=0;
@@ -34,6 +35,17 @@ 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);

src/goto-symex/goto_symex.h

@@ -271,6 +271,8 @@ class goto_symext
   irep_idt guard_identifier;
 
   // symex
+  irep_idt init_l1;
+
   virtual void symex_transition(
     statet &,
     goto_programt::const_targett to,

src/goto-symex/symex_assign.cpp

@@ -204,11 +204,20 @@ void goto_symext::symex_assign_symbol(
   // have an L2 entry set up beforehand either, so exempt them from
   // this check (all other L1 objects should have seen a declaration)
   const symbolt *s;
-  if(!ns.lookup(lhs.get_object_name(), s) &&
-     !s->is_parameter &&
-     !lhs.get_level_1().empty() &&
-     state.level2.current_count(lhs.get_identifier())==0)
+  if(
+    init_l1 != lhs.get_identifier() && !ns.lookup(lhs.get_object_name(), s) &&
+    !s->is_parameter && !lhs.get_level_1().empty() &&
+    state.level2.current_count(lhs.get_identifier()) == 0)
+  {
     return;
+  }
+  else if(init_l1 == lhs.get_identifier())
+  {
+    // the assignment about to happen is the initialisation, clear the
+    // identifier to make sure future steps are not treated as initialisation
+    // steps (and we thus cannot reach the early return above
+    init_l1.clear();
+  }
 
   exprt ssa_rhs=rhs;
 

src/goto-symex/symex_builtin_functions.cpp

@@ -185,9 +185,17 @@ void goto_symext::symex_allocate(
   }
   else
   {
-    exprt nondet = build_symex_nondet(object_type);
-    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);
   }
 
   exprt rhs;

src/goto-symex/symex_decl.cpp

@@ -16,8 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/rename.h>
 #include <util/std_expr.h>
 
-#include <pointer-analysis/add_failed_symbols.h>
-
 #include <analyses/dirty.h>
 
 void goto_symext::symex_decl(statet &state)
@@ -51,37 +49,23 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   state.rename(ssa.type(), l1_identifier, ns);
   ssa.update_type();
 
-  // in case of pointers, put something into the value set
-  if(ns.follow(expr.type()).id()==ID_pointer)
-  {
-    exprt failed=
-      get_failed_symbol(expr, ns);
-
-    exprt rhs;
-
-    if(failed.is_not_nil())
-      rhs=address_of_exprt(failed, to_pointer_type(expr.type()));
-    else
-      rhs=exprt(ID_invalid);
-
-    state.rename(rhs, ns, goto_symex_statet::L1);
-    state.value_set.assign(ssa, rhs, ns, true, false);
-  }
-
-  // prevent propagation
-  state.propagation.remove(l1_identifier);
-
   // 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);
-  state.level2.increase_counter(l1_identifier);
-  const bool record_events=state.record_events;
-  state.record_events=false;
-  state.rename(ssa, ns);
-  state.record_events=record_events;
+  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;
+  }
 
   // we hide the declaration of auxiliary variables
   // and if the statement itself is hidden
@@ -90,10 +74,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);