Merge pull request #6352 from feliperodri/frame-condition-havoc-fix

Check frame conditions before __CPROVER_havoc_object

Author: feliperodri

regression/contracts/assigns_enforce_20/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int x = 0;
+
+void foo(int *y) __CPROVER_assigns()
+{
+  __CPROVER_havoc_object(y);
+  x = 2;
+}
+
+int main()
+{
+  int *y = malloc(sizeof(*y));
+  *y = 0;
+  foo(y);
+  assert(x == 2);
+  return 0;
+}

regression/contracts/assigns_enforce_20/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^\[foo.\d+\] line \d+ Check that \*y is assignable: FAILURE$
+^\[foo.\d+\] line \d+ Check that x is assignable: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+Checks whether contract enforcement works with __CPROVER_havoc_object.

src/goto-instrument/contracts/contracts.cpp

@@ -715,14 +715,7 @@ void code_contractst::instrument_assign_statement(
       assigns_clause.add_to_local_write_set(lhs);
   }
 
-  goto_programt alias_assertion;
-  alias_assertion.add(goto_programt::make_assertion(
-    assigns_clause.generate_containment_check(lhs),
-    instruction_iterator->source_location));
-  alias_assertion.instructions.back().source_location.set_comment(
-    "Check that " + from_expr(ns, lhs.id(), lhs) + " is assignable");
-  insert_before_swap_and_advance(
-    program, instruction_iterator, alias_assertion);
+  add_containment_check(program, assigns_clause, instruction_iterator, lhs);
 }
 
 void code_contractst::instrument_call_statement(
@@ -766,37 +759,24 @@ void code_contractst::instrument_call_statement(
   }
   else if(called_name == "free")
   {
-    goto_programt alias_assertion;
     const exprt &lhs_dereference = dereference_exprt(
       to_typecast_expr(instruction_iterator->call_arguments().front()).op());
-    alias_assertion.add(goto_programt::make_assertion(
-      assigns_clause.generate_containment_check(lhs_dereference),
-      instruction_iterator->source_location));
-    alias_assertion.instructions.back().source_location.set_comment(
-      "Check that " + from_expr(ns, lhs_dereference.id(), lhs_dereference) +
-      " is assignable");
+    add_containment_check(
+      program, assigns_clause, instruction_iterator, lhs_dereference);
     assigns_clause.remove_from_local_write_set(lhs_dereference);
     assigns_clause.remove_from_global_write_set(lhs_dereference);
-    insert_before_swap_and_advance(
-      program, instruction_iterator, alias_assertion);
     return;
   }
 
   if(
     instruction_iterator->call_lhs().is_not_nil() &&
     instruction_iterator->call_lhs().id() == ID_symbol)
   {
-    const auto alias_expr = assigns_clause.generate_containment_check(
+    add_containment_check(
+      program,
+      assigns_clause,
+      instruction_iterator,
       instruction_iterator->call_lhs());
-
-    goto_programt alias_assertion;
-    alias_assertion.add(goto_programt::make_assertion(
-      alias_expr, instruction_iterator->source_location));
-    alias_assertion.instructions.back().source_location.set_comment(
-      "Check that " + from_expr(ns, alias_expr.id(), alias_expr) +
-      " is assignable");
-    insert_before_swap_and_advance(
-      program, instruction_iterator, alias_assertion);
   }
 
   const symbolt &called_symbol = ns.lookup(called_name);
@@ -972,9 +952,33 @@ void code_contractst::check_frame_conditions(
     {
       assigns.remove_from_local_write_set(instruction_it->get_dead().symbol());
     }
+    else if(
+      instruction_it->is_other() &&
+      instruction_it->get_other().get_statement() == ID_havoc_object)
+    {
+      const exprt &havoc_argument = dereference_exprt(
+        to_typecast_expr(instruction_it->get_other().operands().front()).op());
+      add_containment_check(program, assigns, instruction_it, havoc_argument);
+      assigns.remove_from_local_write_set(havoc_argument);
+      assigns.remove_from_global_write_set(havoc_argument);
+    }
   }
 }
 
+void code_contractst::add_containment_check(
+  goto_programt &program,
+  const assigns_clauset &assigns,
+  goto_programt::instructionst::iterator &instruction_it,
+  const exprt &expr)
+{
+  goto_programt assertion;
+  assertion.add(goto_programt::make_assertion(
+    assigns.generate_containment_check(expr), instruction_it->source_location));
+  assertion.instructions.back().source_location.set_comment(
+    "Check that " + from_expr(ns, expr.id(), expr) + " is assignable");
+  insert_before_swap_and_advance(program, instruction_it, assertion);
+}
+
 bool code_contractst::enforce_contract(const irep_idt &function)
 {
   // Add statements to the source function

src/goto-instrument/contracts/contracts.h

@@ -152,6 +152,14 @@ class code_contractst
   /// assigned memory is within the assignable memory frame.
   void check_frame_conditions(goto_programt &, assigns_clauset &);
 
+  /// Inserts an assertion into the goto program to ensure that
+  /// an expression is within the assignable memory frame.
+  void add_containment_check(
+    goto_programt &,
+    const assigns_clauset &,
+    goto_programt::instructionst::iterator &,
+    const exprt &);
+
   /// Check if there are any malloc statements which may be repeated because of
   /// a goto statement that jumps back.
   bool check_for_looped_mallocs(const goto_programt &program);