Explicit nondet initialisation

jbmc/regression/jbmc-strings/long_string/test_abort.desc

@@ -3,7 +3,7 @@ Test.class
 --function Test.checkAbort --trace
 ^EXIT=10$
 ^SIGNAL=0$
-dynamic_object[0-9]*=\(assignment removed\)
+dynamic_object[0-9]*=.*\?.*
 --
 --
 This tests that the object does not appear in the trace, because concretizing

regression/cbmc/Initialization7/test.desc

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

regression/cbmc/constant_folding2/test.desc

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

regression/cbmc/constant_folding3/main.c

@@ -0,0 +1,18 @@
+typedef struct _pair
+{
+  int x;
+  int y;
+} pair;
+
+int __VERIFIER_nondet_int();
+
+int main (void)
+{
+  pair p1 = { .x = 0, .y = __VERIFIER_nondet_int() };
+  pair p2 = {};
+  p2.x = __VERIFIER_nondet_int();
+
+  __CPROVER_assert(p1.x == p2.y, "true by constant propagation");
+
+  return 0;
+}

regression/cbmc/constant_folding3/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+^Generated 1 VCC\(s\), 0 remaining after simplification$
+--
+^warning: ignoring

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

regression/goto-instrument/print_global_state_size1/main.c

@@ -3,7 +3,7 @@
 uint32_t some_global_var;
 int8_t other_global_var;
 
-int main(int argc, char *argv[])
+int main()
 {
   return 0;
 }

src/ansi-c/c_typecheck_argc_argv.cpp

@@ -42,6 +42,7 @@ void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol)
     argc_symbol.type=op0.type();
     argc_symbol.is_static_lifetime=true;
     argc_symbol.is_lvalue=true;
+    argc_symbol.value = side_effect_expr_nondett(op0.type());
 
     if(argc_symbol.type.id()!=ID_signedbv &&
        argc_symbol.type.id()!=ID_unsignedbv)
@@ -81,6 +82,7 @@ void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol)
     argv_symbol.type=argv_type;
     argv_symbol.is_static_lifetime=true;
     argv_symbol.is_lvalue=true;
+    argv_symbol.value = side_effect_expr_nondett(argv_type);
 
     symbolt *argv_new_symbol;
     move_symbol(argv_symbol, argv_new_symbol);
@@ -99,6 +101,7 @@ void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol)
     envp_size_symbol.name="envp_size'";
     envp_size_symbol.type=op0.type(); // same type as argc!
     envp_size_symbol.is_static_lifetime=true;
+    envp_size_symbol.value = side_effect_expr_nondett(op0.type());
     move_symbol(envp_size_symbol, envp_new_size_symbol);
 
     if(envp_symbol.type.id()!=ID_pointer)
@@ -113,6 +116,7 @@ void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol)
 
     envp_symbol.type.id(ID_array);
     envp_symbol.type.add(ID_size).swap(size_expr);
+    envp_symbol.value = side_effect_expr_nondett(envp_symbol.type);
 
     symbolt *envp_new_symbol;
     move_symbol(envp_symbol, envp_new_symbol);

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/goto_symex_state.cpp

@@ -155,6 +155,8 @@ class goto_symex_is_constantt : public is_constantt
       */
       return false;
     }
+    else if(expr.id() == ID_nondet_symbol)
+      return true;
 
     return is_constantt::is_constant(expr);
   }

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

src/linking/static_lifetime_init.cpp

@@ -63,16 +63,13 @@ void static_lifetime_init(
       continue;
 
     // special values
-    if(identifier==CPROVER_PREFIX "constant_infinity_uint" ||
-       identifier==CPROVER_PREFIX "memory" ||
-       identifier=="__func__" ||
-       identifier=="__FUNCTION__" ||
-       identifier=="__PRETTY_FUNCTION__" ||
-       identifier=="argc'" ||
-       identifier=="argv'" ||
-       identifier=="envp'" ||
-       identifier=="envp_size'")
+    if(
+      identifier == CPROVER_PREFIX "constant_infinity_uint" ||
+      identifier == CPROVER_PREFIX "memory" || identifier == "__func__" ||
+      identifier == "__FUNCTION__" || identifier == "__PRETTY_FUNCTION__")
+    {
       continue;
+    }
 
     // just for linking
     if(has_prefix(id, CPROVER_PREFIX "architecture_"))

src/pointer-analysis/value_set.cpp

@@ -389,7 +389,9 @@ void value_sett::get_value_set_rec(
 
   const typet &expr_type=ns.follow(expr.type());
 
-  if(expr.id()==ID_unknown || expr.id()==ID_invalid)
+  if(
+    expr.id() == ID_unknown || expr.id() == ID_invalid ||
+    expr.id() == ID_nondet_symbol)
   {
     insert(dest, exprt(ID_unknown, original_type));
   }
@@ -1195,9 +1197,9 @@ void value_sett::assign(
                 "type:\n"+type.pretty();
 
         rhs_member=make_member(rhs, name, ns);
-
-        assign(lhs_member, rhs_member, ns, false, add_to_sets);
       }
+
+      assign(lhs_member, rhs_member, ns, false, add_to_sets);
     }
   }
   else if(type.id()==ID_array)