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

regression/contracts-dfcc/loop_contracts_do_while/main.c

@@ -5,9 +5,11 @@ int main()
   int x = 0;
 
   do
-  {
-    x++;
-  } while(x < 10) __CPROVER_loop_invariant(0 <= x && x <= 10);
+    __CPROVER_loop_invariant(0 <= x && x <= 10)
+    {
+      x++;
+    }
+  while(x < 10);
 
-  assert(x == 10);
+  assert(x <= 10);
 }

regression/contracts-dfcc/loop_contracts_do_while/nested.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int main()
+{
+  int x = 0;
+
+  do
+  {
+    do
+    {
+      x++;
+    } while(0);
+  } while(0);
+
+  assert(x <= 10);
+}

regression/contracts-dfcc/loop_contracts_do_while/nested.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+nested.c
+--dfcc main --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+We spuriously report that x is not assignable.

regression/contracts-dfcc/loop_contracts_reject_loops_two_latches/test.desc

@@ -1,10 +1,10 @@
 CORE dfcc-only
 main.c
 --dfcc main --apply-loop-contracts
-^Found loop with more than one latch instruction$
-^EXIT=(6|10)$
+^EXIT=10$
 ^SIGNAL=0$
 --
+^Found loop with more than one latch instruction$
 --
-This test checks that our loop contract instrumentation verifies that loops
-nested in loops with contracts also have contracts.
+This test checks that our loop contract instrumentation first transforms loops
+so as to only have a single loop latch.

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)

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.
     // ```

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1174,6 +1174,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     }
 
     do_indirect_call_and_rtti_removal();
+    log.status() << "Trying to force one backedge per target" << messaget::eom;
+    ensure_one_backedge_per_target(goto_model);
 
     const irep_idt harness_id(cmdline.get_value(FLAG_DFCC));
 
@@ -1232,13 +1234,13 @@ void goto_instrument_parse_optionst::instrument_goto_program()
       to_exclude_from_nondet_static,
       log.get_message_handler());
   }
-
-  if(
-    !use_dfcc &&
-    (cmdline.isset(FLAG_LOOP_CONTRACTS) || cmdline.isset(FLAG_REPLACE_CALL) ||
-     cmdline.isset(FLAG_ENFORCE_CONTRACT)))
+  else if((cmdline.isset(FLAG_LOOP_CONTRACTS) ||
+           cmdline.isset(FLAG_REPLACE_CALL) ||
+           cmdline.isset(FLAG_ENFORCE_CONTRACT)))
   {
     do_indirect_call_and_rtti_removal();
+    log.status() << "Trying to force one backedge per target" << messaget::eom;
+    ensure_one_backedge_per_target(goto_model);
     code_contractst contracts(goto_model, log);
 
     std::set<std::string> to_replace(