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

regression/contracts-dfcc/skip_loop_instrumentation/harness.c

@@ -0,0 +1,29 @@
+int global;
+
+int harness(int argc)
+{
+  global = 0;
+  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
+harness.c --function harness
+--dfcc harness --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

@@ -640,14 +640,26 @@ 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()));
+}
+
+#include <iostream>
 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;
@@ -746,6 +758,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,10 @@ 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 +327,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

@@ -1254,7 +1254,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