[CONTRACTS] Support for Kani Loop Contracts

src/goto-instrument/contracts/contracts.cpp

@@ -42,6 +42,7 @@
 #include "instrument_spec_assigns.h"
 #include "memory_predicates.h"
 #include "utils.h"
+#include "utils_kani.h"
 
 #include <algorithm>
 #include <map>
@@ -53,6 +54,7 @@
   goto_programt::targett loop_head,
   goto_programt::targett loop_end,
   const loopt &loop,
+  const goto_programt::instructionst &eval_ins,
   exprt assigns_clause,
   exprt invariant,
   exprt decreases_clause,
@@ -165,6 +167,15 @@
       .symbol_expr();
   pre_loop_head_instrs.add(
     goto_programt::make_decl(initial_invariant_val, loop_head_location));
+
+  // instrument instructions to evaluate invariants before assert(inv)
+  // or assume(inv)
+  for(const auto &in : eval_ins)
+  {
+    auto new_in = goto_programt::instructiont(in);
+    pre_loop_head_instrs.add(std::move(new_in));
+  }
+
   {
     // Although the invariant at this point will not have side effects,
     // it is still a C expression, and needs to be "goto_convert"ed.
@@ -326,6 +337,14 @@
   pre_loop_head_instrs.add(
     goto_programt::make_assignment(in_loop_havoc_block, false_exprt{}));
 
+  // instrument instructions to evaluate invariants before assert(inv)
+  // or assume(inv)
+  for(const auto &in : eval_ins)
+  {
+    auto new_in = goto_programt::instructiont(in);
+    pre_loop_head_instrs.add(std::move(new_in));
+  }
+
   // Insert the second block of pre_loop_head_instrs: the havocing code.
   // We do not `add_pragma_disable_assigns_check`,
   // so that the enclosing scope's assigns clause instrumentation
@@ -336,6 +355,13 @@
   // We use a block scope for assumption, since it's immediately goto converted,
   // and doesn't need to be kept around.
   {
+    // instrument instructions to evaluate invariants before assert(inv)
+    // or assume(inv)
+    for(const auto &in : eval_ins)
+    {
+      auto new_in = goto_programt::instructiont(in);
+      pre_loop_head_instrs.add(std::move(new_in));
+    }
     code_assumet assumption{invariant};
     assumption.add_source_location() = loop_head_location;
     converter.goto_convert(assumption, pre_loop_head_instrs, mode);
@@ -437,6 +463,13 @@
   // We use a block scope for assertion, since it's immediately goto converted,
   // and doesn't need to be kept around.
   {
+    // instrument instructions to evaluate invariants before assert(inv)
+    // or assume(inv)
+    for(const auto &in : eval_ins)
+    {
+      auto new_in = goto_programt::instructiont(in);
+      pre_loop_end_instrs.add(std::move(new_in));
+    }
     code_assertt assertion{invariant};
     assertion.add_source_location() = loop_head_location;
     assertion.add_source_location().set_comment(
@@ -839,8 +872,15 @@
     return;
 
   inlining_decoratort decorated(log.get_message_handler());
-  goto_function_inline(
-    goto_functions, function_name, ns, log.get_message_handler());
+
+  // For kani loop contracts, we postponed the inlining after
+  // get the loop invariants as they are a sequence of instructions
+  // rather than only an expression
+  if(!apply_kani_loop_contracts)
+  {
+    goto_function_inline(
+      goto_functions, function_name, ns, log.get_message_handler());
+  }
 
   INVARIANT(
     decorated.get_recursive_call_set().size() == 0,
@@ -866,18 +906,21 @@
   {
     const typename natural_loops_mutablet::loopt &content;
     const goto_programt::targett head_target, end_target;
+    goto_programt::instructionst eval_instrs;
     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 goto_programt::instructionst ins,
       const exprt &assigns,
       const exprt &inv,
       const exprt &decreases)
       : content(loop),
         head_target(head),
         end_target(end),
+        eval_instrs(ins),
         assigns_clause(assigns),
         invariant(inv),
         decreases_clause(decreases)
@@ -894,6 +937,12 @@
     goto_programt::target_less_than>
     loop_head_ends;
 
+  // Preprocess loops from kani
+  if(apply_kani_loop_contracts)
+  {
+    annotate_kani_loop_invariants(goto_function.body, log);
+  }
+
   for(const auto &loop_head_and_content : natural_loops.loop_map)
   {
     const auto &loop_body = loop_head_and_content.second;
@@ -966,13 +1015,22 @@
       goto_function.body, loop_head, goto_programt::make_skip());
     loop_end->set_target(loop_head);
 
+    goto_programt::instructionst eval_instrs;
+
     exprt assigns_clause =
       static_cast<const exprt &>(loop_end->condition().find(ID_C_spec_assigns));
     exprt invariant = static_cast<const exprt &>(
       loop_end->condition().find(ID_C_spec_loop_invariant));
     exprt decreases_clause = static_cast<const exprt &>(
       loop_end->condition().find(ID_C_spec_decreases));
 
+    // get kani loop invariants and the evaluation instructions.
+    if(apply_kani_loop_contracts)
+    {
+      get_kani_invariants(
+        goto_function, loop_head, invariant.operands(), eval_instrs);
+    }
+
     if(invariant.is_nil())
     {
       if(decreases_clause.is_not_nil() || assigns_clause.is_not_nil())
@@ -1005,6 +1063,7 @@
       loop_head_end.second.second,
       loop_head,
       loop_end,
+      eval_instrs,
       assigns_clause,
       invariant,
       decreases_clause);
@@ -1017,6 +1076,13 @@
     to_check_contracts_on_children.push_back(idx);
   }
 
+  // The postponed inlining
+  if(apply_kani_loop_contracts)
+  {
+    goto_function_inline(
+      goto_functions, function_name, ns, log.get_message_handler());
+  }
+
   for(size_t outer = 0; outer < loop_nesting_graph.size(); ++outer)
   {
     for(size_t inner = 0; inner < loop_nesting_graph.size(); ++inner)
@@ -1104,6 +1170,7 @@
       loop_node.head_target,
       loop_node.end_target,
       updated_loops.loop_map[loop_node.head_target],
+      loop_node.eval_instrs,
       loop_node.assigns_clause,
       loop_node.invariant,
       loop_node.decreases_clause,

src/goto-instrument/contracts/contracts.h

@@ -33,6 +33,10 @@ Date: February 2016
 #define HELP_LOOP_CONTRACTS                                                    \
   " {y--apply-loop-contracts} \t check and use loop contracts when provided\n"
 
+#define FLAG_KANI_LOOP_CONTRACTS "apply-kani-loop-contracts"
+#define HELP_KANI_LOOP_CONTRACTS                                               \
+  " {y--apply-kani-loop-contracts} \t check loop contracts from kani\n"
+
 #define FLAG_LOOP_CONTRACTS_NO_UNWIND "loop-contracts-no-unwind"
 #define HELP_LOOP_CONTRACTS_NO_UNWIND                                          \
   " {y--loop-contracts-no-unwind} \t do not unwind transformed loops\n"
@@ -122,6 +126,7 @@ class code_contractst
     goto_programt::targett loop_head,
     goto_programt::targett loop_end,
     const loopt &loop,
+    const goto_programt::instructionst &eval_ins,
     exprt assigns_clause,
     exprt invariant,
     exprt decreases_clause,
@@ -144,6 +149,9 @@ class code_contractst
   // Unwind transformed loops after applying loop contracts or not.
   bool unwind_transformed_loops = true;
 
+  // Unwind transformed loops after applying loop contracts or not.
+  bool apply_kani_loop_contracts = false;
+
 protected:
   goto_modelt &goto_model;
   symbol_tablet &symbol_table;

src/goto-instrument/contracts/utils_kani.cpp

@@ -0,0 +1,156 @@
+/*******************************************************************\
+
+Module: Utility functions for Kani code contracts.
+
+Author: Qinheping Hu, qinhh@amazon.com
+
+\*******************************************************************/
+
+#include "utils_kani.h"
+
+#include <analyses/natural_loops.h>
+
+bool is_kani_loop_invariant(const goto_programt::instructiont instr)
+{
+  if(!instr.is_function_call())
+    return false;
+
+  auto s = id2string(to_symbol_expr(instr.call_function()).get_identifier());
+  return (s.find("kani_loop_invariant") != std::string::npos) &&
+         (s.find("kani_loop_invariant_") == std::string::npos);
+}
+
+bool is_kani_loop_invariant_begin(const goto_programt::instructiont instr)
+{
+  if(!instr.is_function_call())
+    return false;
+
+  auto s = id2string(to_symbol_expr(instr.call_function()).get_identifier());
+  return s.find("kani_loop_invariant_begin") != std::string::npos;
+}
+
+bool is_kani_loop_invariant_end(const goto_programt::instructiont instr)
+{
+  if(!instr.is_function_call())
+    return false;
+
+  auto s = id2string(to_symbol_expr(instr.call_function()).get_identifier());
+  return s.find("kani_loop_invariant_end") != std::string::npos;
+}
+
+void annotate_kani_loop_invariants(goto_programt &body, messaget &log)
+{
+  // The place holder function call
+  //   kani_loop_invariant(cond)
+  // indicate its successor loop latch contains loop invariants.
+  // So for each such function call, we find the loop end for it and
+  // annotate loop contracts to the loop end.
+  // Note that here we only annotate 'true' to indicate it contains
+  // loop contracts. And will later get the loop contracts with another pass.
+
+  natural_loops_mutablet natural_loops(body);
+  std::set<goto_programt::targett, goto_programt::target_less_than>
+    loop_latches;
+
+  // Collect all latches
+  for(const auto &loop_head_and_content : natural_loops.loop_map)
+  {
+    const auto &loop_content = loop_head_and_content.second;
+    // Skip empty loops and self-looped node.
+    if(loop_content.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)
+    {
+      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;
+    }
+    loop_latches.insert(loop_end);
+  }
+
+  // Go through all instructions in the body to find the placeholder
+  //    kani_loop_invariant()
+  for(auto it = body.instructions.begin(); it != body.instructions.end(); it++)
+  {
+    if(is_kani_loop_invariant(*it))
+    {
+      auto temp_it = it;
+      while(!loop_latches.count(temp_it))
+      {
+        temp_it = body.get_successors(temp_it).front();
+      }
+
+      auto op = and_exprt(true_exprt(), true_exprt());
+
+      temp_it->condition_nonconst().add(ID_C_spec_loop_invariant).swap(op);
+    }
+  }
+}
+
+void get_kani_invariants(
+  const goto_functiont &goto_function,
+  const goto_programt::const_targett &loop_head,
+  exprt::operandst &invariant_clauses,
+  goto_programt::instructionst &eval_instructions)
+{
+  // The loop invariants in kani goto are passed as the instructions
+  // right before the loop head, and between two placeholder function
+  // calls kani_loop_invariant_begin() and kani_loop_invariant_end().
+  auto &body = goto_function.body;
+
+  for(auto it = body.instructions.begin(); it != body.instructions.end(); it++)
+  {
+    // first find the loop head
+    if(it == loop_head)
+    {
+      // skip irrelevant instructions until we see the placeholder
+      while(!is_kani_loop_invariant_end(*it))
+      {
+        it--;
+      }
+      // skip the placeholder
+      it--;
+
+      // copy and store all instructions between the two placeholders
+      while(!is_kani_loop_invariant_begin(*it))
+      {
+        // except for goto and dead
+        // because here the goto is not a real goto, but just goto the next
+        // instruction.
+        // Dead instructions are for those temporary variables and can be
+        // safely ignored here.
+        if(!it->is_goto() && !it->is_dead())
+        {
+          auto new_instruction = goto_programt::instructiont(*it);
+          new_instruction.target_number =
+            goto_programt::instructiont::nil_target;
+          eval_instructions.push_front(new_instruction);
+        }
+
+        // The only function call assign the evaluated result to a boolean
+        // variable. We will use the result variable as loop invariants.
+        if(it->is_function_call())
+        {
+          invariant_clauses.push_back(
+            typecast_exprt(it->call_lhs(), bool_typet()));
+        }
+        it--;
+      }
+      return;
+    }
+  }
+  UNREACHABLE;
+}