Explicitly initialise non-static objects with non-deterministic values

Author: tautschnig

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>

src/goto-programs/graphml_witness.cpp

@@ -173,13 +173,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->is_assignment() ||
+     (!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

@@ -6,8 +6,11 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
+#include <util/message.h>
 #include <util/simplify_expr.h>
 
+#include <linking/zero_initializer.h>
+
 #include "goto_symex.h"
 
 unsigned goto_symext::nondet_count=0;
@@ -48,6 +51,21 @@ void goto_symext::replace_nondet(exprt &expr)
   if(expr.id()==ID_side_effect &&
      expr.get(ID_statement)==ID_nondet)
   {
+    null_message_handlert null_message;
+    exprt nondet=
+      nondet_initializer(
+        expr.type(),
+        expr.source_location(),
+        ns,
+        null_message);
+
+    if(nondet.id()!=ID_side_effect)
+    {
+      replace_nondet(nondet);
+      expr.swap(nondet);
+      return;
+    }
+
     exprt new_expr(ID_nondet_symbol, expr.type());
     new_expr.set(ID_identifier, "symex::nondet"+std::to_string(nondet_count++));
     new_expr.add_source_location()=expr.source_location();

src/goto-symex/symex_builtin_functions.cpp

@@ -173,6 +173,18 @@ void goto_symext::symex_malloc(
 
   new_symbol_table.add(value_symbol);
 
+  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::HIDDEN);
+
   address_of_exprt rhs;
 
   if(object_type.id()==ID_array)

src/goto-symex/symex_decl.cpp

@@ -11,8 +11,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/rename.h>
 #include <util/std_expr.h>
 
-#include <pointer-analysis/add_failed_symbols.h>
-
 #include <analyses/dirty.h>
 
 #include "goto_symex.h"
@@ -72,42 +70,22 @@ 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())
-    {
-      address_of_exprt address_of_expr;
-      address_of_expr.object()=failed;
-      address_of_expr.type()=expr.type();
-      rhs=address_of_expr;
-    }
-    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;
+
+  // 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=state.source.pc;
+  ++next;
+  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
@@ -116,10 +94,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::HIDDEN:symex_targett::STATE);
 
   assert(state.dirty);

src/linking/zero_initializer.cpp

@@ -13,13 +13,15 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/std_types.h>
 #include <util/std_expr.h>
+#include <util/std_code.h>
 #include <util/pointer_offset_size.h>
 
 #include <ansi-c/c_types.h>
 #include <ansi-c/expr2c.h>
 
 #include "zero_initializer.h"
 
+template<bool nondet>
 class zero_initializert:public messaget
 {
 public:
@@ -68,7 +70,8 @@ Function: zero_initializert::zero_initializer_rec
 
 \*******************************************************************/
 
-exprt zero_initializert::zero_initializer_rec(
+template<bool nondet>
+exprt zero_initializert<nondet>::zero_initializer_rec(
   const typet &type,
   const source_locationt &source_location)
 {
@@ -85,31 +88,55 @@ exprt zero_initializert::zero_initializer_rec(
      type_id==ID_floatbv ||
      type_id==ID_fixedbv)
   {
-    exprt result=from_integer(0, type);
+    exprt result;
+    if(nondet)
+      result=side_effect_expr_nondett(type);
+    else
+      result=from_integer(0, type);
+
     result.add_source_location()=source_location;
     return result;
   }
   else if(type_id==ID_rational ||
           type_id==ID_real)
   {
-    constant_exprt result(ID_0, type);
+    exprt result;
+    if(nondet)
+      result=side_effect_expr_nondett(type);
+    else
+      result=constant_exprt(ID_0, type);
+
     result.add_source_location()=source_location;
     return result;
   }
   else if(type_id==ID_verilog_signedbv ||
           type_id==ID_verilog_unsignedbv)
   {
-    std::size_t width=to_bitvector_type(type).get_width();
-    std::string value(width, '0');
+    exprt result;
+    if(nondet)
+      result=side_effect_expr_nondett(type);
+    else
+    {
+      std::size_t width=to_bitvector_type(type).get_width();
+      std::string value(width, '0');
+
+      result=constant_exprt(value, type);
+    }
 
-    constant_exprt result(value, type);
     result.add_source_location()=source_location;
     return result;
   }
   else if(type_id==ID_complex)
   {
-    exprt sub_zero=zero_initializer_rec(type.subtype(), source_location);
-    complex_exprt result(sub_zero, sub_zero, to_complex_type(type));
+    exprt result;
+    if(nondet)
+      result=side_effect_expr_nondett(type);
+    else
+    {
+      exprt sub_zero=zero_initializer_rec(type.subtype(), source_location);
+      result=complex_exprt(sub_zero, sub_zero, to_complex_type(type));
+    }
+
     result.add_source_location()=source_location;
     return result;
   }
@@ -148,6 +175,13 @@ exprt zero_initializert::zero_initializer_rec(
       }
       else if(to_integer(array_type.size(), array_size))
       {
+        if(nondet)
+        {
+          exprt result=side_effect_expr_nondett(type);
+          result.add_source_location()=source_location;
+          return result;
+        }
+
         error().source_location=source_location;
         error() << "failed to zero-initialize array of non-fixed size `"
                 << to_string(array_type.size()) << "'" << eom;
@@ -178,6 +212,13 @@ exprt zero_initializert::zero_initializer_rec(
 
     if(to_integer(vector_type.size(), vector_size))
     {
+      if(nondet)
+      {
+        exprt result=side_effect_expr_nondett(type);
+        result.add_source_location()=source_location;
+        return result;
+      }
+
       error().source_location=source_location;
       error() << "failed to zero-initialize vector of non-fixed size `"
               << to_string(vector_type.size()) << "'" << eom;
@@ -308,7 +349,14 @@ exprt zero_initializert::zero_initializer_rec(
   }
   else if(type_id==ID_string)
   {
-    return constant_exprt(irep_idt(), type);
+    exprt result;
+    if(nondet)
+      result=side_effect_expr_nondett(type);
+    else
+      result=constant_exprt(irep_idt(), type);
+
+    result.add_source_location()=source_location;
+    return result;
   }
   else
   {
@@ -337,7 +385,29 @@ exprt zero_initializer(
   const namespacet &ns,
   message_handlert &message_handler)
 {
-  zero_initializert z_i(ns, message_handler);
+  zero_initializert<false> z_i(ns, message_handler);
+  return z_i(type, source_location);
+}
+
+/*******************************************************************\
+
+Function: nondet_initializer
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+exprt nondet_initializer(
+  const typet &type,
+  const source_locationt &source_location,
+  const namespacet &ns,
+  message_handlert &message_handler)
+{
+  zero_initializert<true> z_i(ns, message_handler);
   return z_i(type, source_location);
 }
 
@@ -363,7 +433,38 @@ exprt zero_initializer(
 
   try
   {
-    zero_initializert z_i(ns, mh);
+    zero_initializert<false> z_i(ns, mh);
+    return z_i(type, source_location);
+  }
+  catch(int)
+  {
+    throw oss.str();
+  }
+}
+
+/*******************************************************************\
+
+Function: nondet_initializer
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+exprt nondet_initializer(
+  const typet &type,
+  const source_locationt &source_location,
+  const namespacet &ns)
+{
+  std::ostringstream oss;
+  stream_message_handlert mh(oss);
+
+  try
+  {
+    zero_initializert<true> z_i(ns, mh);
     return z_i(type, source_location);
   }
   catch(int)

src/linking/zero_initializer.h

@@ -21,10 +21,21 @@ exprt zero_initializer(
   const namespacet &,
   message_handlert &);
 
+exprt nondet_initializer(
+  const typet &,
+  const source_locationt &,
+  const namespacet &,
+  message_handlert &);
+
 // throws a char* in case of failure
 exprt zero_initializer(
   const typet &,
   const source_locationt &,
   const namespacet &);
 
+exprt nondet_initializer(
+  const typet &type,
+  const source_locationt &source_location,
+  const namespacet &ns);
+
 #endif // CPROVER_LINKING_ZERO_INITIALIZER_H