Merge pull request #6808 from padhi-aws-forks/loop-holes-fix

Allow instrumentation of loops with "holes"

Author: SaswatPadhi

regression/contracts/loop_assigns-04/test.desc

@@ -15,4 +15,4 @@ The alias analysis in this case returns `unknown`,
 and so we must manually annotate an assigns clause on the loop.
 
 Note that the annotated assigns clause in this case is an underapproximation,
-because `i`assigns. is also assigned in the loop and should be marked as assignable.
+because `i` is also assigned in the loop and should be marked as assignable.

regression/contracts/loop_assigns-05/test.desc

@@ -7,7 +7,6 @@ main.c
 ^\[body_2.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$
 ^\[body_3.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$
 ^\[incr.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$
-^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
 ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
 ^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
 ^\[main.assertion.\d+\] .* assertion j == 9: SUCCESS$

regression/contracts/loop_assigns_scoped_local_statics/test.desc

@@ -7,7 +7,6 @@ main.c
 ^\[body_2.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$
 ^\[body_3.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$
 ^\[incr.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$
-^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
 ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
 ^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
 ^\[main.assertion.\d+\] .* assertion j == 9: SUCCESS$

regression/contracts/loop_body_with_hole/main.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+#include <stdbool.h>
+
+int main()
+{
+  unsigned n, k, sum_to_k = 0;
+  bool flag = false;
+
+  for(unsigned i = 0; i < n; ++i)
+    // clang-format off
+  __CPROVER_loop_invariant(0 <= i && i <= n)
+    // clang-format on
+    {
+      if(i == k)
+      {
+        flag = true;
+        break;
+      }
+      sum_to_k += i;
+    }
+}

regression/contracts/loop_body_with_hole/test.desc

@@ -0,0 +1,25 @@
+CORE
+main.c
+--apply-loop-contracts
+^\[main\.\d+\] line \d+ Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] line \d+ Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] line \d+ Check that loop instrumentation was not truncated: SUCCESS$
+^\[main\.assigns\.\d+\] line \d+ Check that i is valid: SUCCESS$
+^\[main\.assigns\.\d+\] line \d+ Check that i is assignable: SUCCESS$
+^\[main\.assigns\.\d+\] line \d+ Check that sum_to_k is valid: SUCCESS$
+^\[main\.assigns\.\d+\] line \d+ Check that sum_to_k is assignable: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+--
+^\[main\.assigns\.\d+\] line \d+ Check that flag is assignable: .*$
+--
+This test checks that we only instrument instructions contained within
+the computed natural loops. In a previous commit, an exception was added to
+ensure this and it was triggered whenever an instruction within [head,end]
+of a loop was not contained within the computed natural loop's "contents".
+In this commit, we remove the exception and instead mask out such instructions.
+
+The statement
+  flag = true;
+in main.c generates such an assignment instruction.
+We have added a negative regex to ensure that this instruction is not instrumented.

regression/contracts/loop_guard_with_side_effects/test.desc

@@ -8,11 +8,8 @@ main.c
 \[main\.\d+\] line \d+ Check loop invariant before entry: SUCCESS$
 \[main\.\d+\] line \d+ Check that loop invariant is preserved: SUCCESS$
 \[main.assigns\.\d+\] line \d+ Check that i is assignable: SUCCESS$
-\[main.assigns\.\d+\] line \d+ Check that j is assignable: SUCCESS$
-\[main.assigns\.\d+\] line \d+ Check that k is assignable: SUCCESS$
 \[main.assigns\.\d+\] line \d+ Check that i is valid: SUCCESS$
 \[main.assigns\.\d+\] line \d+ Check that j is valid: SUCCESS$
-\[main.assigns\.\d+\] line \d+ Check that i is assignable: SUCCESS$
 \[main.overflow\.\d+\] line \d+ arithmetic overflow on unsigned \+ in i \+ 1u: SUCCESS
 \[main.assertion\.\d+\] line \d+ assertion i == k: SUCCESS$
 \[main.overflow\.\d+\] line \d+ arithmetic overflow on unsigned \+ in k \+ \(unsigned int\)1: SUCCESS

regression/contracts/loop_guard_with_side_effects_fail/test.desc

@@ -6,10 +6,7 @@ main.c
 \[main\.\d+\] line \d+ Check loop invariant before entry: SUCCESS$
 \[main\.\d+\] line \d+ Check that loop invariant is preserved: SUCCESS$
 \[main.assigns\.\d+\] line \d+ Check that i is assignable: SUCCESS$
-\[main.assigns\.\d+\] line \d+ Check that j is assignable: SUCCESS$
-\[main.assigns\.\d+\] line \d+ Check that k is assignable: SUCCESS$
 \[main.assigns\.\d+\] line \d+ Check that i is valid: SUCCESS$
-\[main.assigns\.\d+\] line \d+ Check that i is assignable: SUCCESS$
 \[main.assertion\.\d+\] line \d+ assertion i == k: SUCCESS$
 ^EXIT=(6|10)$
 ^SIGNAL=0$

src/goto-instrument/contracts/contracts.cpp

@@ -449,7 +449,8 @@ void code_contractst::check_apply_loop_contracts(
     loop_end,
     skip_function_paramst::NO,
     // do not use CFG info for now
-    cfg_empty_info);
+    cfg_empty_info,
+    [&loop](const goto_programt::targett &t) { return loop.contains(t); });
 
   // Now we begin instrumenting at the loop_end.
   // `pre_loop_end_instrs` are to be inserted before `loop_end`.
@@ -1081,11 +1082,9 @@ void code_contractst::apply_loop_contract(
     // By definition the `loop_content` is a set of instructions computed
     // by `natural_loops` based on the CFG.
     // Since we perform assigns clause instrumentation by sequentially
-    // traversing instructions from `loop_head` to `loop_end`, here check that:
-    // 1. All instructions in `loop_content` are contained within the
-    //    [loop_head, loop_end] iterator range
-    // 2. All instructions in the [loop_head, loop_end] range are contained
-    //    in the `loop_content` set, except for the exceptions explained below.
+    // traversing instructions from `loop_head` to `loop_end`,
+    // here we ensure that all instructions in `loop_content` belong within
+    // the [loop_head, loop_end] target range
 
     // Check 1. (i \in loop_content) ==> loop_head <= i <= loop_end
     for(const auto &i : loop_content)
@@ -1100,49 +1099,6 @@ void code_contractst::apply_loop_contract(
         throw 0;
       }
     }
-
-    // Check 2. (loop_head <= i <= loop_end) ==> (i \in loop_content)
-    //
-    // We allow the following exceptions in this check:
-    // - `SKIP` or `LOCATION` instructions which are no-op
-    // - `ASSUME(false)` instructions which are introduced by function pointer
-    //    or nested loop transformations, and have no successor instructions
-    // - `SET_RETURN_VALUE` instructions followed by an uninterrupted sequence
-    //    of `DEAD` instructions and a `GOTO` jump out of the loop,
-    //    which model C `return` statements.
-    // - `GOTO` jumps out of the loops, which model C `break` statements.
-    // These instructions are allowed to be missing from `loop_content`,
-    // and may be safely ignored for the purpose of our instrumentation.
-    for(auto i = loop_head; i != loop_end; ++i)
-    {
-      if(loop_content.contains(i))
-        continue;
-
-      if(i->is_skip() || i->is_location())
-        continue;
-
-      if(i->is_goto() && !loop_content.contains(i->get_target()))
-        continue;
-
-      if(i->is_assume() && i->get_condition().is_false())
-        continue;
-
-      if(i->is_set_return_value())
-      {
-        do
-          i++;
-        while(i != loop_end && i->is_dead());
-
-        // because we increment `i` in the outer `for` loop
-        i--;
-        continue;
-      }
-
-      log.error() << "Computed loop at: " << loop_head->source_location()
-                  << "is missing an instruction:" << messaget::eom;
-      goto_function.body.output_instruction(ns, function_name, log.error(), *i);
-      throw 0;
-    }
   }
 
   for(size_t outer = 0; outer < loop_nesting_graph.size(); ++outer)
@@ -1205,13 +1161,22 @@ void code_contractst::apply_loop_contract(
       loop_node.decreases_clause.is_nil())
       continue;
 
+    // Computed loop "contents" needs to be refreshed to include any newly
+    // introduced instrumentation, e.g. havoc instructions for assigns clause,
+    // on inner loops in to the outer loop's contents.
+    // Else, during the outer loop instrumentation these instructions will be
+    // "masked" just as any other instruction not within its "contents."
+
+    goto_functions.update();
+    natural_loops_mutablet updated_loops(goto_function.body);
+
     check_apply_loop_contracts(
       function_name,
       goto_function,
       local_may_alias,
       loop_node.head_target,
       loop_node.end_target,
-      loop_node.content,
+      updated_loops.loop_map[loop_node.head_target],
       loop_node.assigns_clause,
       loop_node.invariant,
       loop_node.decreases_clause,

src/goto-instrument/contracts/instrument_spec_assigns.cpp

@@ -314,12 +314,15 @@ void instrument_spec_assignst::instrument_instructions(
   goto_programt::targett instruction_it,
   const goto_programt::targett &instruction_end,
   skip_function_paramst skip_function_params,
-  optionalt<cfg_infot> &cfg_info_opt)
+  optionalt<cfg_infot> &cfg_info_opt,
+  const std::function<bool(const goto_programt::targett &)> &pred)
 {
   while(instruction_it != instruction_end)
   {
     // Skip instructions marked as disabled for assigns clause checking
-    if(has_disable_assigns_check_pragma(instruction_it))
+    if(
+      has_disable_assigns_check_pragma(instruction_it) ||
+      (pred && !pred(instruction_it)))
     {
       instruction_it++;
       if(cfg_info_opt.has_value())
@@ -541,7 +544,7 @@ exprt instrument_spec_assignst::target_validity_expr(
   // the target's `start_address` pointer satisfies w_ok with the expected size
   // (or is NULL if we allow it explicitly).
   // This assertion will be falsified whenever `start_address` is invalid or
-  // not of the right size (or is NULL if we dot not allow it expliclitly).
+  // not of the right size (or is NULL if we do not allow it explicitly).
   auto result =
     or_exprt{not_exprt{car.condition()},
              w_ok_exprt{car.target_start_address(), car.target_size()}};

src/goto-instrument/contracts/instrument_spec_assigns.h

@@ -444,12 +444,25 @@ class instrument_spec_assignst
     optionalt<cfg_infot> &cfg_info_opt,
     goto_programt &dest);
 
+  /// Instruments a sequence of instructions with inclusion checks.
+  ///   If `pred` is not provided,
+  ///     then all instructions are instrumented.
+  ///   If `pred` is provided,
+  ///     then only the instructions that satisfy pred are instrumented.
+  ///
+  /// \param body goto program containing the instructions
+  /// \param instruction_it target to the first instruction of the sequence
+  /// \param instruction_end target to the last instruction of the sequence
+  /// \param skip_function_params the argument to the free operator
+  /// \param cfg_info_opt allows target set pruning if available
+  /// \param pred a predicate on targets to check if they should be instrumented
   void instrument_instructions(
     goto_programt &body,
     goto_programt::targett instruction_it,
     const goto_programt::targett &instruction_end,
     skip_function_paramst skip_function_params,
-    optionalt<cfg_infot> &cfg_info_opt);
+    optionalt<cfg_infot> &cfg_info_opt,
+    const std::function<bool(const goto_programt::targett &)> &pred = {});
 
   /// Inserts the detected static local symbols into a target container.
   /// \tparam C The type of the target container