added lots of sanity checks to loop contracts

Our loop contracts instrumentation routine makes some assumptions regarding the structure of loops. In this commit, I have added checks to verify them before we start instrumenting.

Author: SaswatPadhi

regression/contracts/loop_contracts_reject_overlapping_loops/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+
+int main()
+{
+  int i = 0, j = 0, k = 0;
+
+  while(j < 10)
+  {
+    while(k < 10)
+      __CPROVER_loop_invariant(1 == 1)
+      {
+        while(i < 10)
+        {
+          i++;
+        }
+      }
+    j++;
+  }
+}

regression/contracts/loop_contracts_reject_overlapping_loops/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--apply-loop-contracts
+activate-multi-line-match
+Inner loop at: file main.c line 12 function main does not have contracts, but an enclosing loop does.\nPlease provide contracts for this loop, or unwind it first.
+^EXIT=(6|10)$
+^SIGNAL=0$
+--
+--
+This test checks that our instrumentation routines verify that inner loops
+either have contracts or are unwound, if any enclosing loop has contracts.

src/goto-instrument/contracts/contracts.cpp

@@ -140,62 +140,15 @@ void code_contractst::check_apply_loop_contracts(
   goto_functionst::goto_functiont &goto_function,
   const local_may_aliast &local_may_alias,
   goto_programt::targett loop_head,
+  goto_programt::targett loop_end,
   const loopt &loop,
+  exprt assigns_clause,
+  exprt invariant,
+  exprt decreases_clause,
   const irep_idt &mode)
 {
-  PRECONDITION(!loop.empty());
-
   const auto loop_head_location = loop_head->source_location();
 
-  // find the last back edge
-  goto_programt::targett loop_end = loop_head;
-  for(const auto &t : loop)
-  {
-    if(
-      t->is_goto() && t->get_target() == loop_head &&
-      t->location_number > loop_end->location_number)
-      loop_end = t;
-  }
-
-  // check for assigns, invariant, and decreases clauses
-  auto assigns_clause = static_cast<const exprt &>(
-    loop_end->get_condition().find(ID_C_spec_assigns));
-  auto invariant = static_cast<const exprt &>(
-    loop_end->get_condition().find(ID_C_spec_loop_invariant));
-  auto decreases_clause = static_cast<const exprt &>(
-    loop_end->get_condition().find(ID_C_spec_decreases));
-
-  if(invariant.is_nil())
-  {
-    if(decreases_clause.is_nil() && assigns_clause.is_nil())
-    {
-      // no contracts to enforce, so return
-      return;
-    }
-    else
-    {
-      invariant = true_exprt();
-      // assigns clause is missing; we will try to automatic inference
-      log.warning() << "The loop at " << loop_head_location.as_string()
-                    << " does not have an invariant in its contract.\n"
-                    << "Hence, a default invariant ('true') is being used.\n"
-                    << "This choice is sound, but verification may fail"
-                    << " if it is be too weak to prove the desired properties."
-                    << messaget::eom;
-    }
-  }
-  else
-  {
-    invariant = conjunction(invariant.operands());
-    if(decreases_clause.is_nil())
-    {
-      log.warning() << "The loop at " << loop_head_location.as_string()
-                    << " does not have a decreases clause in its contract.\n"
-                    << "Termination of this loop will not be verified."
-                    << messaget::eom;
-    }
-  }
-
   // Vector representing a (possibly multidimensional) decreases clause
   const auto &decreases_clause_exprs = decreases_clause.operands();
 
@@ -1022,20 +975,144 @@ void code_contractst::apply_loop_contract(
 
   struct loop_graph_nodet : public graph_nodet<empty_edget>
   {
-    typedef const goto_programt::targett &targett;
-    typedef const typename natural_loops_mutablet::loopt &loopt;
-
-    targett target;
-    loopt loop;
-
-    loop_graph_nodet(targett t, loopt l) : target(t), loop(l)
+    const typename natural_loops_mutablet::loopt &content;
+    const goto_programt::targett head_target, end_target;
+    exprt assigns_clause, invariant, decreases_clause;
+
+    loop_graph_nodet(
+      const typename natural_loops_mutablet::loopt &loop,
+      const goto_programt::targett head,
+      const goto_programt::targett end,
+      const exprt &assigns,
+      const exprt &inv,
+      const exprt &decreases)
+      : content(loop),
+        head_target(head),
+        end_target(end),
+        assigns_clause(assigns),
+        invariant(inv),
+        decreases_clause(decreases)
     {
     }
   };
   grapht<loop_graph_nodet> loop_nesting_graph;
 
-  for(const auto &loop : natural_loops.loop_map)
-    loop_nesting_graph.add_node(loop.first, loop.second);
+  std::list<size_t> to_check_contracts_on_children;
+
+  for(const auto &loop_head_and_content : natural_loops.loop_map)
+  {
+    const auto &loop_content = loop_head_and_content.second;
+    if(loop_content.empty())
+      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)
+    {
+      if(
+        t->is_goto() && t->get_target() == loop_head &&
+        t->location_number > loop_end->location_number)
+        loop_end = t;
+    }
+
+    if(loop_end == loop_head)
+    {
+      log.error() << "Could not find end of the loop starting at: "
+                  << loop_head->source_location() << messaget::eom;
+      throw 0;
+    }
+
+    exprt assigns_clause =
+      static_cast<const exprt &>(loop_end->condition().find(ID_C_spec_assigns));
+    exprt invariant = static_cast<const exprt &>(
+      loop_end->get_condition().find(ID_C_spec_loop_invariant));
+    exprt decreases_clause = static_cast<const exprt &>(
+      loop_end->get_condition().find(ID_C_spec_decreases));
+
+    if(invariant.is_nil())
+    {
+      if(decreases_clause.is_not_nil() || assigns_clause.is_not_nil())
+      {
+        invariant = true_exprt{};
+        // assigns clause is missing; we will try to automatic inference
+        log.warning()
+          << "The loop at " << loop_head->source_location().as_string()
+          << " does not have an invariant in its contract.\n"
+          << "Hence, a default invariant ('true') is being used.\n"
+          << "This choice is sound, but verification may fail"
+          << " if it is be too weak to prove the desired properties."
+          << messaget::eom;
+      }
+    }
+    else
+    {
+      invariant = conjunction(invariant.operands());
+      if(decreases_clause.is_nil())
+      {
+        log.warning() << "The loop at "
+                      << loop_head->source_location().as_string()
+                      << " does not have a decreases clause in its contract.\n"
+                      << "Termination of this loop will not be verified."
+                      << messaget::eom;
+      }
+    }
+
+    const auto idx = loop_nesting_graph.add_node(
+      loop_content,
+      loop_head,
+      loop_end,
+      assigns_clause,
+      invariant,
+      decreases_clause);
+
+    if(
+      assigns_clause.is_nil() && invariant.is_nil() &&
+      decreases_clause.is_nil())
+      continue;
+
+    to_check_contracts_on_children.push_back(idx);
+
+    // If the loop has contracts to be enforced, then
+    // reject irregular loops that have "holes" within their body,
+    // while allowing instructions that are okay to be "out of loop".
+    for(auto i = loop_head; i < loop_end; ++i)
+    {
+      if(loop_content.contains(i))
+        continue;
+
+      // `break` or `goto` out of loop, are okay
+      if(i->is_goto() && !loop_content.contains(i->get_target()))
+        continue;
+
+      // `assume false`, is okay
+      if(i->is_assume() && i->get_condition().is_false())
+        continue;
+
+      // `set return value` followed by `dead`s, are okay
+      if(i->is_set_return_value())
+      {
+        do
+          i++;
+        while(i->is_dead());
+
+        // because we increment `i` in the outer `for` loop
+        i--;
+
+        // the `goto` for `return` will be handled in next iteration
+        continue;
+      }
+
+      log.error() << "Cannot enforce contracts on irregular loop at: "
+                  << loop_head->source_location()
+                  << ".\nLoop body must be a contiguous set of instructions."
+                  << messaget::eom;
+      log.debug() << "Out-of-loop-body instruction:" << messaget::eom;
+      goto_function.body.output_instruction(ns, function_name, log.debug(), *i);
+      throw 0;
+    }
+  }
 
   for(size_t outer = 0; outer < loop_nesting_graph.size(); ++outer)
   {
@@ -1044,23 +1121,69 @@ void code_contractst::apply_loop_contract(
       if(inner == outer)
         continue;
 
-      if(loop_nesting_graph[outer].loop.contains(
-           loop_nesting_graph[inner].target))
+      if(loop_nesting_graph[outer].content.contains(
+           loop_nesting_graph[inner].head_target))
+      {
+        if(!loop_nesting_graph[outer].content.contains(
+             loop_nesting_graph[inner].end_target))
+        {
+          log.error()
+            << "Overlapping loops at:\n"
+            << loop_nesting_graph[outer].head_target->source_location()
+            << "\nand\n"
+            << loop_nesting_graph[inner].head_target->source_location()
+            << "\nLoops must be nested or sequential for contracts to be "
+               "enforced."
+            << messaget::eom;
+        }
         loop_nesting_graph.add_edge(inner, outer);
+      }
+    }
+  }
+
+  // make sure all children of a contractified loop also have contracts
+  while(!to_check_contracts_on_children.empty())
+  {
+    const auto loop_idx = to_check_contracts_on_children.front();
+    to_check_contracts_on_children.pop_front();
+
+    const auto &loop_node = loop_nesting_graph[loop_idx];
+    if(
+      loop_node.assigns_clause.is_nil() && loop_node.invariant.is_nil() &&
+      loop_node.decreases_clause.is_nil())
+    {
+      log.error()
+        << "Inner loop at: " << loop_node.head_target->source_location()
+        << " does not have contracts, but an enclosing loop does.\n"
+        << "Please provide contracts for this loop, or unwind it first."
+        << messaget::eom;
+      throw 0;
     }
+
+    for(const auto child_idx : loop_nesting_graph.get_predecessors(loop_idx))
+      to_check_contracts_on_children.push_back(child_idx);
   }
 
   // Iterate over the (natural) loops in the function, in topo-sorted order,
   // and apply any loop contracts that we find.
   for(const auto &idx : loop_nesting_graph.topsort())
   {
     const auto &loop_node = loop_nesting_graph[idx];
+    if(
+      loop_node.assigns_clause.is_nil() && loop_node.invariant.is_nil() &&
+      loop_node.decreases_clause.is_nil())
+      continue;
+
     check_apply_loop_contracts(
       function_name,
       goto_function,
       local_may_alias,
-      loop_node.target,
-      loop_node.loop,
+      loop_node.head_target,
+      loop_node.end_target,
+      loop_node.content,
+      loop_node.assigns_clause,
+      loop_node.invariant,
+      loop_node.decreases_clause,
       symbol_table.lookup_ref(function_name).mode);
   }
 }

src/goto-instrument/contracts/contracts.h

@@ -102,7 +102,11 @@ class code_contractst
     goto_functionst::goto_functiont &goto_function,
     const local_may_aliast &local_may_alias,
     goto_programt::targett loop_head,
+    goto_programt::targett loop_end,
     const loopt &loop,
+    exprt assigns_clause,
+    exprt invariant,
+    exprt decreases_clause,
     const irep_idt &mode);
 
   // for "helper" classes to update symbol table.