Code contracts: do not interleave checking and instrumenting

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,18 +888,24 @@
 
   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;
+    const auto &loop_body = loop_head_and_content.second;
     // Skip empty loops and self-looped node.
-    if(loop_content.size() <= 1)
+    if(loop_body.size() <= 1)
       continue;
 
     auto loop_head = loop_head_and_content.first;
     auto loop_end = loop_head;
 
     // Find the last back edge to `loop_head`
-    for(const auto &t : loop_content)
+    for(const auto &t : loop_body)
     {
       if(
         t->is_goto() && t->get_target() == loop_head &&
@@ -914,6 +920,41 @@
       throw 0;
     }
 
+    // By definition the `loop_body` 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_body` belong within
+    // the [loop_head, loop_end] target range.
+
+    // Check 1. (i \in loop_body) ==> loop_head <= i <= loop_end
+    for(const auto &i : loop_body)
+    {
+      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_body))
+          .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 +1002,7 @@
     }
 
     const auto idx = loop_nesting_graph.add_node(
-      loop_content,
+      loop_head_end.second.second,
       loop_head,
       loop_end,
       assigns_clause,
@@ -974,30 +1015,6 @@
       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(

src/goto-programs/restrict_function_pointers.cpp

@@ -35,7 +35,7 @@ void for_each_function_call(GotoFunctionT &&goto_function, Handler handler)
     handler);
 }
 
-static void restrict_function_pointer(
+[[nodiscard]] static bool restrict_function_pointer(
   message_handlert &message_handler,
   symbol_tablet &symbol_table,
   goto_programt &goto_program,
@@ -54,7 +54,7 @@ static void restrict_function_pointer(
   const auto &original_function = location->call_function();
 
   if(!can_cast_expr<dereference_exprt>(original_function))
-    return;
+    return false;
 
   // because we run the label function pointer calls transformation pass before
   // this stage a dereference can only dereference a symbol expression
@@ -66,7 +66,7 @@ static void restrict_function_pointer(
     restrictions.restrictions.find(pointer_symbol.get_identifier());
 
   if(restriction_iterator == restrictions.restrictions.end())
-    return;
+    return false;
 
   const namespacet ns(symbol_table);
   std::unordered_set<symbol_exprt, irep_hash> candidates;
@@ -80,6 +80,8 @@ static void restrict_function_pointer(
     function_id,
     location,
     candidates);
+
+  return true;
 }
 } // namespace
 
@@ -180,15 +182,19 @@ void restrict_function_pointers(
   {
     goto_functiont &goto_function = function_item.second;
 
+    bool did_something = false;
     for_each_function_call(goto_function, [&](const goto_programt::targett it) {
-      restrict_function_pointer(
+      did_something |= restrict_function_pointer(
         message_handler,
         goto_model.symbol_table,
         goto_function.body,
         function_item.first,
         restrictions,
         it);
     });
+
+    if(did_something)
+      goto_function.body.update();
   }
 }