Code contracts: do not interleave checking and instrumenting

Loop normalisation must first check that all loops described via
`natural_loopst` are of the expected shape and then start inserting or
transforming instructions. Else, and depending on loop shapes and loop
nesting, the instruction iterators held in the `natural_loopst` may no
longer be adequate descriptions of the loops. (The iterators weren't
invalidated, but would no longer point to heads or loop ends.)

Author: tautschnig

Diff for: src/goto-instrument/contracts/contracts.cpp

@@ -888,6 +888,12 @@ void code_contractst::apply_loop_contract(
 
   std::list<size_t> to_check_contracts_on_children;
 
+  std::map<
+    goto_programt::targett,
+    std::pair<goto_programt::targett, natural_loops_mutablet::loopt>,
+    goto_programt::target_less_than>
+    loop_head_ends;
+
   for(const auto &loop_head_and_content : natural_loops.loop_map)
   {
     const auto &loop_content = loop_head_and_content.second;
@@ -914,6 +920,42 @@ void code_contractst::apply_loop_contract(
       throw 0;
     }
 
+    // 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 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)
+    {
+      if(
+        loop_head->location_number > i->location_number ||
+        i->location_number > loop_end->location_number)
+      {
+        log.conditional_output(
+          log.error(), [&i, &loop_head](messaget::mstreamt &mstream) {
+            mstream << "Computed loop at " << loop_head->source_location()
+                    << "contains an instruction beyond [loop_head, loop_end]:"
+                    << messaget::eom;
+            i->output(mstream);
+            mstream << messaget::eom;
+          });
+        throw 0;
+      }
+    }
+
+    if(!loop_head_ends
+          .emplace(loop_head, std::make_pair(loop_end, loop_content))
+          .second)
+      UNREACHABLE;
+  }
+
+  for(auto &loop_head_end : loop_head_ends)
+  {
+    auto loop_head = loop_head_end.first;
+    auto loop_end = loop_head_end.second.first;
     // After loop-contract instrumentation, jumps to the `loop_head` will skip
     // some instrumented instructions. So we want to make sure that there is
     // only one jump targeting `loop_head` from `loop_end` before loop-contract
@@ -961,7 +1003,7 @@ void code_contractst::apply_loop_contract(
     }
 
     const auto idx = loop_nesting_graph.add_node(
-      loop_content,
+      loop_head_end.second.second,
       loop_head,
       loop_end,
       assigns_clause,
@@ -974,30 +1016,6 @@ void code_contractst::apply_loop_contract(
       continue;
 
     to_check_contracts_on_children.push_back(idx);
-
-    // 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 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)
-    {
-      if(std::distance(loop_head, i) < 0 || std::distance(i, loop_end) < 0)
-      {
-        log.conditional_output(
-          log.error(), [&i, &loop_head](messaget::mstreamt &mstream) {
-            mstream << "Computed loop at " << loop_head->source_location()
-                    << "contains an instruction beyond [loop_head, loop_end]:"
-                    << messaget::eom;
-            i->output(mstream);
-            mstream << messaget::eom;
-          });
-        throw 0;
-      }
-    }
   }
 
   for(size_t outer = 0; outer < loop_nesting_graph.size(); ++outer)

Diff for: src/goto-instrument/contracts/dynamic-frames/dfcc_check_loop_normal_form.cpp

@@ -19,6 +19,12 @@ void dfcc_check_loop_normal_form(goto_programt &goto_program, messaget &log)
   // instruction span for each loop
   std::vector<std::pair<goto_programt::targett, goto_programt::targett>> spans;
 
+  std::map<
+    goto_programt::targett,
+    goto_programt::targett,
+    goto_programt::target_less_than>
+    latch_head_pairs;
+
   for(auto &loop : natural_loops.loop_map)
   {
     auto head = loop.first;
@@ -132,7 +138,15 @@ void dfcc_check_loop_normal_form(goto_programt &goto_program, messaget &log)
         "nested loop head and latch are in outer loop");
     }
 
+    if(!latch_head_pairs.emplace(latch, head).second)
+      UNREACHABLE;
+  }
+
     // all checks passed, now we perform some instruction rewriting
+  for(auto &entry_pair : latch_head_pairs)
+  {
+    auto latch = entry_pair.first;
+    auto head = entry_pair.second;
 
     // Convert conditional latch into exiting + unconditional latch.
     // ```