CONTRACTS: redirect checks to outer write set for loops that get skipped

A couple of KOWNBUG tests with do-while loops are now working.

regression/contracts-dfcc/loop_contracts_do_while/nested.desc

@@ -1,9 +1,9 @@
-KNOWNBUG
+CORE
 nested.c
 --dfcc main --apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 --
-We spuriously report that x is not assignable.
+We properly skip the instrumentation of both loops.

regression/contracts-dfcc/loop_contracts_reject_loops_two_latches/test.desc

@@ -1,10 +1,11 @@
 CORE dfcc-only
 main.c
 --dfcc main --apply-loop-contracts
-^EXIT=10$
+^EXIT=0$
 ^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
 --
-^Found loop with more than one latch instruction$
 --
 This test checks that our loop contract instrumentation first transforms loops
-so as to only have a single loop latch.
+so as to only have a single loop latch, and skips instrumentation if the result
+has no contract.

regression/contracts-dfcc/skip_loop_instrumentation/across_functions.c

@@ -0,0 +1,25 @@
+int foo()
+{
+  int x = 0;
+  while(x < 10)
+  {
+    ++x;
+  }
+  return x;
+}
+
+int main()
+{
+  int x = 0;
+
+  for(int i = 0; i < 10; ++i)
+    __CPROVER_loop_invariant(0 <= x && x <= 10)
+    {
+      if(x < 10)
+        x++;
+    }
+
+  x += foo();
+
+  __CPROVER_assert(x <= 20, "");
+}

regression/contracts-dfcc/skip_loop_instrumentation/across_functions.desc

@@ -0,0 +1,11 @@
+CORE
+across_functions.c
+--dfcc main --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+This test case checks that when instrumentation of any look is skipped, we
+redirect write set checks to the parent write set.

regression/contracts-dfcc/skip_loop_instrumentation/main.c

@@ -0,0 +1,29 @@
+int global;
+
+int main()
+{
+  global = 0;
+  int argc = 1;
+  do
+  {
+    int local;
+    global = 1;
+    local = 1;
+    for(int i = 0; i < 1; i++)
+    {
+      local = 1;
+      global = 2;
+      int j = 0;
+      while(j < 1)
+      {
+        local = 1;
+        global = 3;
+        j++;
+      }
+      __CPROVER_assert(global == 3, "case3");
+    }
+    __CPROVER_assert(global == 3, "case3");
+  } while(0);
+  __CPROVER_assert(global == 3, "case1");
+  return 0;
+}

regression/contracts-dfcc/skip_loop_instrumentation/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--dfcc main --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+This test case checks that when the instrumentation of nested loops is skipped, we redirect the write set checks to the
+outer write set.

src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp

@@ -628,14 +628,25 @@ void dfcc_cfg_infot::output(std::ostream &out) const
   }
 }
 
+std::size_t dfcc_cfg_infot::get_first_id_not_skipped_or_top_level_id(
+  const std::size_t loop_id) const
+{
+  if(is_top_level_id(loop_id) || !get_loop_info(loop_id).must_skip())
+  {
+    return loop_id;
+  }
+  return get_first_id_not_skipped_or_top_level_id(
+    get_outer_loop_identifier(loop_id).value_or(top_level_id()));
+}
+
 const exprt &
 dfcc_cfg_infot::get_write_set(goto_programt::const_targett target) const
 {
   auto loop_id_opt = dfcc_get_loop_id(target);
   PRECONDITION(
     loop_id_opt.has_value() &&
     is_valid_loop_or_top_level_id(loop_id_opt.value()));
-  auto loop_id = loop_id_opt.value();
+  auto loop_id = get_first_id_not_skipped_or_top_level_id(loop_id_opt.value());
   if(is_top_level_id(loop_id))
   {
     return top_level_write_set;
@@ -734,6 +745,11 @@ bool dfcc_cfg_infot::is_top_level_id(const std::size_t id) const
   return id == loop_info_map.size();
 }
 
+size_t dfcc_cfg_infot::top_level_id() const
+{
+  return loop_info_map.size();
+}
+
 bool dfcc_cfg_infot::must_track_decl_or_dead(
   goto_programt::const_targett target) const
 {

src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h

@@ -144,6 +144,13 @@ class dfcc_loop_infot
   /// this loop. This is the one that must be passed as argument to write set
   /// functions.
   const symbol_exprt addr_of_write_set_var;
+
+  /// Returns true if the loop has no invariant and no decreases clause
+  /// and its instrumentation must be skipped.
+  const bool must_skip() const
+  {
+    return invariant.is_nil() && decreases.empty();
+  }
 };
 
 /// Computes natural loops, enforces normal form conditions, computes the
@@ -248,7 +255,9 @@ class dfcc_cfg_infot
   /// \brief Returns the loop info for that loop_id.
   const dfcc_loop_infot &get_loop_info(const std::size_t loop_id) const;
 
-  /// \brief Returns the write set variable for that instruction.
+  /// \brief Returns the write set variable to use for the given instruction
+  /// Returns the write set for the loop, or one of the outer loops,
+  /// or top level, passing through all loops that are [must_skip]
   const exprt &get_write_set(goto_programt::const_targett target) const;
 
   /// \brief Returns the set of local variable for the scope where that
@@ -270,6 +279,11 @@ class dfcc_cfg_infot
     return topsorted_loops;
   }
 
+  /// \brief Returns the id of the first outer loop (including this one) that
+  /// is not skipped, or the top level id.
+  std::size_t
+  get_first_id_not_skipped_or_top_level_id(const std::size_t loop_id) const;
+
   /// Finds the DFCC id of the loop that contains the given loop, returns
   /// nullopt when the loop has no outer loop.
   const std::optional<std::size_t>
@@ -314,6 +328,9 @@ class dfcc_cfg_infot
   /// True iff \p id is in the valid range for a loop id for this function.
   bool is_top_level_id(const std::size_t id) const;
 
+  /// Returns the top level ID
+  size_t top_level_id() const;
+
   /// Loop identifiers sorted from most deeply nested to less deeply nested
   std::vector<std::size_t> topsorted_loops;
 

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp

@@ -1239,7 +1239,7 @@ void dfcc_instrumentt::apply_loop_contracts(
   for(const auto &loop_id : cfg_info.get_loops_toposorted())
   {
     const auto &loop = cfg_info.get_loop_info(loop_id);
-    if(loop.invariant.is_nil() && loop.decreases.empty())
+    if(loop.must_skip())
     {
       // skip loops that do not have contracts
       log.warning() << "loop " << function_id << "." << loop.cbmc_loop_id