Allow instrumentation of loops with "holes"

Our assigns clause instrumentation works over a sequence of instructions ignoring control flow edges. In #6701 a safety check was added to bail out on attempting to instrument loops that contain "holes" -- instructions that appear within the [head, end] sequence for the loop, but are not part of the computed "natural loop" because of control flow.
In this PR, we remove this restriction and allow instrumenting such loops by masking out instructions outside of the computed natural loop.

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`.
@@ -1070,11 +1071,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)
@@ -1089,49 +1088,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)
@@ -1194,13 +1150,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