CONTRACTS: add inductive checks for assigns clauses

Author: qinheping

regression/contracts/loop_assigns-02/test.desc

@@ -5,9 +5,9 @@ main.c
 ^SIGNAL=0$
 ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
 ^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
-^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: FAILURE$
+^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is inductively assignable: FAILURE$
 ^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.\d+\] .* assertion b->data\[5\] == 0: FAILURE$
+^\*\* 1 of 12 failed \(2 iterations\)
 ^VERIFICATION FAILED$
 --
 --

src/goto-instrument/contracts/contracts.cpp

@@ -89,10 +89,9 @@ void code_contractst::check_apply_loop_contracts(
   //
   //                               ... preamble ...
   //                        ,-     initialize loop_entry history vars;
-  //                        |      entered_loop = false
-  // loop assigns check     |      initial_invariant_val = invariant_expr;
-  //  - unchecked, temps    |      in_base_case = true;
-  // func assigns check     |      snapshot (write_set);
+  // loop assigns check     |      entered_loop = false
+  //  - unchecked, temps    |      initial_invariant_val = invariant_expr;
+  // func assigns check     |      in_base_case = true;
   //  - disabled via pragma |      goto HEAD;
   //                        |    STEP:
   //                  --.   |      assert (initial_invariant_val);
@@ -104,10 +103,12 @@ void code_contractst::check_apply_loop_contracts(
   // loop assigns check     ,-     ... eval guard ...
   //  + assertions added    |      if (!guard)
   // func assigns check     |        goto EXIT;
-  //  - disabled via pragma `-     ... loop body ...
+  //  - disabled via pragma |      snapshot (write_set);
+  //                        `-     ... loop body ...
   //                        ,-     entered_loop = true
   //                        |      if (in_base_case)
   //                        |        goto STEP;
+  //                        |      assert CAR_begin in CAR_end
   // loop assigns check     |      assert (invariant_expr);
   //  - unchecked, temps    |      new_variant_val = decreases_clause_expr;
   // func assigns check     |      assert (new_variant_val < old_variant_val);
@@ -256,9 +257,8 @@ void code_contractst::check_apply_loop_contracts(
 
   // Insert instrumentation
   // This must be done before havocing the write set.
-  // FIXME: this is not true for write set targets that
-  // might depend on other write set targets.
-  pre_loop_head_instrs.destructive_append(snapshot_instructions);
+  goto_function.body.destructive_insert(
+    std::next(loop_head), snapshot_instructions);
 
   // Insert a jump to the loop head
   // (skipping over the step case initialization code below)
@@ -387,6 +387,17 @@ void code_contractst::check_apply_loop_contracts(
   pre_loop_end_instrs.add(goto_programt::make_goto(
     step_case_target, in_base_case, loop_head_location));
 
+  // Adding checks that demonstrating that the loop assigns clause is an
+  // inductive invariant.
+  // CAR_begin should be included in CAR_end
+  goto_programt assigns_inductive_check_instrs;
+  for(const auto &target : to_havoc)
+  {
+    instrument_spec_assigns.check_inclusion_induction(
+      target, assigns_inductive_check_instrs);
+    pre_loop_end_instrs.destructive_append(assigns_inductive_check_instrs);
+  }
+
   // The following code is only reachable in the step case,
   // i.e., when in_base_case == false,
   // because of the unconditional jump above.

src/goto-instrument/contracts/instrument_spec_assigns.cpp

@@ -149,7 +149,17 @@ void instrument_spec_assignst::check_inclusion_assignment(
   // create temporary car but do not track
   const auto car = create_car_expr(true_exprt{}, lhs);
   create_snapshot(car, dest);
-  inclusion_check_assertion(car, false, true, dest);
+  inclusion_check_assertion(car, false, true, false, dest);
+}
+
+void instrument_spec_assignst::check_inclusion_induction(
+  const exprt &lhs,
+  goto_programt &dest) const
+{
+  // create temporary car but do not track
+  const auto car = create_car_expr(true_exprt{}, lhs);
+  create_snapshot(car, dest);
+  inclusion_check_assertion(car, false, true, true, dest);
 }
 
 void instrument_spec_assignst::track_static_locals(goto_programt &dest)
@@ -313,7 +323,7 @@ void instrument_spec_assignst::
   create_snapshot(car, dest);
 
   // check inclusion, allowing null and not allowing stack allocated locals
-  inclusion_check_assertion(car, true, false, dest);
+  inclusion_check_assertion(car, true, false, false, dest);
 
   // invalidate aliases of the freed object
   invalidate_heap_and_spec_aliases(car, dest);
@@ -680,6 +690,7 @@ void instrument_spec_assignst::inclusion_check_assertion(
   const car_exprt &car,
   bool allow_null_lhs,
   bool include_stack_allocated,
+  bool is_inductive_check,
   goto_programt &dest) const
 {
   source_locationt source_location(car.source_location());
@@ -705,7 +716,10 @@ void instrument_spec_assignst::inclusion_check_assertion(
   else
     comment += id2string(orig_comment);
 
-  comment += " is assignable";
+  if(is_inductive_check)
+    comment += " is inductively assignable";
+  else
+    comment += " is assignable";
   source_location.set_comment(comment);
 
   dest.add(goto_programt::make_assertion(

src/goto-instrument/contracts/instrument_spec_assigns.h

@@ -442,6 +442,12 @@ class instrument_spec_assignst
     const exprt &expr,
     goto_programt &dest);
 
+  /// Generates inclusion check instructions for inductive checks of
+  /// the write set
+  /// \param lhs the assignment lhs or argument to havoc/havoc_object
+  /// \param dest destination program to append instructions to
+  void check_inclusion_induction(const exprt &lhs, goto_programt &dest) const;
+
   /// Instruments a sequence of instructions with inclusion checks.
   ///   If `pred` is not provided,
   ///     then all instructions are instrumented.
@@ -547,11 +553,13 @@ class instrument_spec_assignst
   /// \param allow_null_lhs if true, allow the lhs to be NULL
   /// \param include_stack_allocated if true, include stack allocated targets
   /// in the inclusion check.
+  /// \param is_inductive_check if true, assertions are for inductive check.
   /// \param dest destination program to append instructions to
   void inclusion_check_assertion(
     const car_exprt &lhs,
     bool allow_null_lhs,
     bool include_stack_allocated,
+    bool is_inductive_check,
     goto_programt &dest) const;
 
   /// \brief Adds an assignment in dest to invalidate the tracked car if

src/goto-instrument/havoc_utils.cpp

@@ -31,15 +31,6 @@ void havoc_utilst::append_havoc_code_for_expr(
   const exprt &expr,
   goto_programt &dest) const
 {
-  if(expr.id() == ID_index || expr.id() == ID_dereference)
-  {
-    address_of_exprt address_of_expr(expr);
-    if(!is_constant(address_of_expr))
-    {
-      append_object_havoc_code_for_expr(location, address_of_expr, dest);
-      return;
-    }
-  }
   append_scalar_havoc_code_for_expr(location, expr, dest);
 }
 

src/goto-instrument/havoc_utils.h

@@ -64,12 +64,6 @@ class havoc_utilst
 
   /// \brief Append goto instructions to havoc a single expression `expr`
   ///
-  /// If `expr` is an array index or object dereference expression,
-  /// with a non-constant offset, e.g. a[i] or *(b+i) with a non-constant `i`,
-  /// then instructions are generated to havoc the entire underlying object.
-  /// Otherwise, e.g. for a[0] or *(b+i) when `i` is a known constant,
-  /// the instructions are generated to only havoc the scalar value of `expr`.
-  ///
   /// \param location The source location to annotate on the havoc instruction
   /// \param expr The expression to havoc
   /// \param dest The destination goto program to append the instructions to