added __CPROVER_havoc(...)

Author: kroening

regression/cbmc/havoc_object1/main.c

@@ -0,0 +1,34 @@
+int main()
+{
+  int i=0;
+  __CPROVER_havoc_object(&i);
+  __CPROVER_assert(i==0, "i==0"); // should fail
+
+  int array[10];
+  for(i=0; i<10; i++) array[i]=i;
+
+  __CPROVER_havoc_object(array);
+  __CPROVER_assert(array[3]==3, "array[3]"); // should fail
+
+  struct { int i, j; } some_struct = { 1, 2 };
+  __CPROVER_havoc_object(&some_struct.j);
+  __CPROVER_assert(some_struct.i==1, "struct i"); // should fail
+  __CPROVER_assert(some_struct.j==2, "struct j"); // should fail
+
+  // now conditional
+  _Bool c;
+  int *p=c?&i:&some_struct.i;
+  i=20;
+  some_struct.i=30;
+  __CPROVER_havoc_object(p);
+  if(c)
+  {
+    __CPROVER_assert(i==20, "i==20 (A)"); // should fail
+    __CPROVER_assert(some_struct.i==30, "some_struct.i==30 (A)"); // should pass
+  }
+  else
+  {
+    __CPROVER_assert(i==20, "i==20 (B)"); // should pass
+    __CPROVER_assert(some_struct.i==30, "some_struct.i==30 (B)"); // should fail
+  }
+}

regression/cbmc/havoc_object1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\*\* 6 of 8 failed.*$
+--

src/ansi-c/ansi_c_internal_additions.cpp

@@ -114,6 +114,7 @@ void ansi_c_internal_additions(std::string &code)
     "void __CPROVER_assert(__CPROVER_bool assertion, const char *description);\n"
     // NOLINTNEXTLINE(whitespace/line_length)
     "void __CPROVER_precondition(__CPROVER_bool precondition, const char *description);\n"
+    "void __CPROVER_havoc_object(void *);\n"
     "__CPROVER_bool __CPROVER_equal();\n"
     "__CPROVER_bool __CPROVER_same_object(const void *, const void *);\n"
     "__CPROVER_bool __CPROVER_invalid_pointer(const void *);\n"

src/goto-programs/builtin_functions.cpp

@@ -1159,6 +1159,29 @@ void goto_convertt::do_function_call_symbol(
       throw 0;
     }
   }
+  else if(identifier==CPROVER_PREFIX "havoc_object")
+  {
+    if(arguments.size()!=1)
+    {
+      error().source_location=function.find_source_location();
+      error() << "`" << identifier << "' expected to have one argument"
+              << eom;
+      throw 0;
+    }
+
+    if(lhs.is_not_nil())
+    {
+      error().source_location=function.find_source_location();
+      error() << identifier << " expected not to have LHS" << eom;
+      throw 0;
+    }
+
+    goto_programt::targett t=dest.add_instruction(OTHER);
+    t->source_location=function.source_location();
+    t->code=codet(ID_havoc_object);
+    t->code.add_source_location()=function.source_location();
+    t->code.copy_to_operands(arguments[0]);
+  }
   else if(identifier==CPROVER_PREFIX "printf")
   {
     do_printf(lhs, function, arguments, dest);

src/goto-symex/goto_symex.h

@@ -262,6 +262,9 @@ class goto_symext
   void symex_assign_rec(statet &state, const code_assignt &code);
   virtual void symex_assign(statet &state, const code_assignt &code);
 
+  // havocs the given object
+  void havoc_rec(statet &, const guardt &, const exprt &);
+
   typedef symex_targett::assignment_typet assignment_typet;
 
   void symex_assign_rec(

src/goto-symex/symex_other.cpp

@@ -17,10 +17,67 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/rename.h>
 #include <util/base_type.h>
 #include <util/std_expr.h>
+#include <util/std_code.h>
 #include <util/byte_operators.h>
 
 #include <util/c_types.h>
 
+void goto_symext::havoc_rec(
+  statet &state,
+  const guardt &guard,
+  const exprt &dest)
+{
+  if(dest.id()==ID_symbol)
+  {
+    exprt lhs;
+
+    if(guard.is_true())
+      lhs=dest;
+    else
+      lhs=if_exprt(
+        guard.as_expr(), dest, exprt("NULL-object", dest.type()));
+
+    code_assignt assignment;
+    assignment.lhs()=lhs;
+    assignment.rhs()=side_effect_expr_nondett(dest.type());
+
+    symex_assign(state, assignment);
+  }
+  else if(dest.id()==ID_byte_extract_little_endian ||
+          dest.id()==ID_byte_extract_big_endian)
+  {
+    havoc_rec(state, guard, to_byte_extract_expr(dest).op());
+  }
+  else if(dest.id()==ID_if)
+  {
+    const if_exprt &if_expr=to_if_expr(dest);
+
+    guardt guard_t=state.guard;
+    guard_t.add(if_expr.cond());
+    havoc_rec(state, guard_t, if_expr.true_case());
+
+    guardt guard_f=state.guard;
+    guard_f.add(not_exprt(if_expr.cond()));
+    havoc_rec(state, guard_f, if_expr.false_case());
+  }
+  else if(dest.id()==ID_typecast)
+  {
+    havoc_rec(state, guard, to_typecast_expr(dest).op());
+  }
+  else if(dest.id()==ID_index)
+  {
+    havoc_rec(state, guard, to_index_expr(dest).array());
+  }
+  else if(dest.id()==ID_member)
+  {
+    havoc_rec(state, guard, to_member_expr(dest).struct_op());
+  }
+  else
+  {
+    // consider printing a warning
+  }
+}
+
 void goto_symext::symex_other(
   const goto_functionst &goto_functions,
   statet &state)
@@ -213,6 +270,17 @@ void goto_symext::symex_other(
   {
     target.memory_barrier(state.guard.as_expr(), state.source);
   }
+  else if(statement==ID_havoc_object)
+  {
+    DATA_INVARIANT(code.operands().size()==1,
+                   "havoc_object must have one operand");
+
+    // we need to add dereferencing for the first operand
+    exprt object=dereference_exprt(code.op0(), empty_typet());
+    clean_expr(object, state, true);
+
+    havoc_rec(state, guardt(), object);
+  }
   else
     throw "unexpected statement: "+id2string(statement);
 }

src/util/irep_ids.def

@@ -830,6 +830,7 @@ IREP_ID_TWO(C_java_generic_type, #java_generic_type)
 IREP_ID_TWO(C_java_generics_class_type, #java_generics_class_type)
 IREP_ID_TWO(generic_types, #generic_types)
 IREP_ID_TWO(type_variables, #type_variables)
+IREP_ID_ONE(havoc_object)
 
 #undef IREP_ID_ONE
 #undef IREP_ID_TWO