nondet_initializer to build deep non-deterministic expressions

Create a side_effect_expr_nondett for all PODs or types of unknown/unbounded
size, and arrays/structs/vectors/unions of non-deterministic expressions. For
example, struct { int; float; } will yield a struct{nondet(int), nondet(float)}.

Author: tautschnig

src/util/expr_initializer.cpp

@@ -18,8 +18,10 @@ Author: Daniel Kroening, [email protected]
 #include "message.h"
 #include "namespace.h"
 #include "pointer_offset_size.h"
+#include "std_code.h"
 #include "std_expr.h"
 
+template <bool nondet>
 class zero_initializert:public messaget
 {
 public:
@@ -46,7 +48,8 @@ class zero_initializert:public messaget
     const source_locationt &source_location);
 };
 
-exprt zero_initializert::zero_initializer_rec(
+template <bool nondet>
+exprt zero_initializert<nondet>::zero_initializer_rec(
   const typet &type,
   const source_locationt &source_location)
 {
@@ -63,31 +66,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
+    {
+      const 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;
   }
@@ -119,12 +146,26 @@ exprt zero_initializert::zero_initializer_rec(
 
       if(array_type.size().id()==ID_infinity)
       {
+        if(nondet)
+        {
+          side_effect_expr_nondett result(type);
+          result.add_source_location() = source_location;
+          return result;
+        }
+
         array_of_exprt value(tmpval, array_type);
         value.add_source_location()=source_location;
         return value;
       }
       else if(to_integer(array_type.size(), array_size))
       {
+        if(nondet)
+        {
+          side_effect_expr_nondett result(type);
+          result.add_source_location() = source_location;
+          return result;
+        }
+
         error().source_location=source_location;
         error() << "failed to zero-initialize array of non-fixed size `"
                 << format(array_type.size()) << "'" << eom;
@@ -154,6 +195,13 @@ exprt zero_initializert::zero_initializer_rec(
 
     if(to_integer(vector_type.size(), vector_size))
     {
+      if(nondet)
+      {
+        side_effect_expr_nondett result(type);
+        result.add_source_location() = source_location;
+        return result;
+      }
+
       error().source_location=source_location;
       error() << "failed to zero-initialize vector of non-fixed size `"
               << format(vector_type.size()) << "'" << eom;
@@ -282,7 +330,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
   {
@@ -298,7 +353,17 @@ 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);
+}
+
+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);
 }
 
@@ -312,7 +377,26 @@ 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();
+  }
+}
+
+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/util/expr_initializer.h

@@ -24,10 +24,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_UTIL_EXPR_INITIALIZER_H