Function contracts: adding a loop-freeness check before assigns clause checking instrumentation

Author: Remi Delmas

src/goto-instrument/contracts/contracts.cpp

@@ -39,6 +39,7 @@ Date: February 2016
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
 #include <util/replace_symbol.h>
+#include <util/simplify_expr.h>
 #include <util/std_code.h>
 
 #include "memory_predicates.h"
@@ -1105,7 +1106,9 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function)
     return true;
   }
 
-  if(check_for_looped_mallocs(function_obj->second.body))
+  auto &goto_program = function_obj->second.body;
+
+  if(check_for_looped_mallocs(goto_program))
   {
     return true;
   }
@@ -1126,14 +1129,17 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function)
   for(const auto &param : to_code_type(target.type).parameters())
     assigns.add_to_write_set(ns.lookup(param.get_identifier()).symbol_expr());
 
-  auto instruction_it = function_obj->second.body.instructions.begin();
+  auto instruction_it = goto_program.instructions.begin();
   for(const auto &car : assigns.get_write_set())
   {
     auto snapshot_instructions = car.generate_snapshot_instructions();
     insert_before_swap_and_advance(
-      function_obj->second.body, instruction_it, snapshot_instructions);
+      goto_program, instruction_it, snapshot_instructions);
   };
 
+  // restore internal coherence in the programs
+  goto_functions.update();
+
   // Full inlining of the function body
   // Inlining is performed so that function calls to a same function
   // occurring under different write sets get instrumented specifically
@@ -1145,9 +1151,17 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function)
     decorated.get_recursive_function_warnings_count() == 0,
     "Recursive functions found during inlining");
 
-  // restore internal invariants
+  // clean up possible fake loops that are due to `IF 0!=0 GOTO i` instructions
+  simplify_gotos(goto_program);
+
+  // restore internal coherence in the programs
   goto_functions.update();
 
+  INVARIANT(
+    is_loop_free(goto_program),
+    "Loops remain in function '" + id2string(function) +
+      "', assigns clause checking instrumentation cannot be applied.");
+
   // Insert write set inclusion checks.
   check_frame_conditions(
     function_obj->first,
@@ -1613,3 +1627,62 @@ bool code_contractst::is_auxiliary_decl_dead_or_assign(
   return false;
 }
 
+void code_contractst::simplify_gotos(goto_programt &goto_program)
+{
+  for(auto &instruction : goto_program.instructions)
+  {
+    if(instruction.is_goto())
+    {
+      const auto &condition = instruction.get_condition();
+      const auto &simplified = simplify_expr(condition, ns);
+      if(simplified.is_false())
+        instruction.turn_into_skip();
+    }
+  }
+}
+
+bool code_contractst::is_loop_free(const goto_programt &goto_program)
+{
+  // create cfg from instruction list
+  cfg_baset<empty_cfg_nodet> cfg;
+  cfg(goto_program);
+
+  // check that all nodes are there
+  INVARIANT(
+    goto_program.instructions.size() == cfg.size(),
+    "Instruction list vs CFG size mismatch.");
+
+  //compute SCCs
+  std::vector<node_indext> node_to_scc(cfg.size(), -1);
+  auto nof_sccs = cfg.SCCs(node_to_scc);
+
+  // compute size of each SCC
+  std::vector<int> scc_size(nof_sccs, 0);
+  for(auto scc : node_to_scc)
+  {
+    INVARIANT(
+      0 <= scc && scc < nof_sccs, "Could not determine SCC for instruction");
+    scc_size[scc]++;
+  }
+
+  // check they are all of size 1
+  for(int scc_id = 0; scc_id < nof_sccs; scc_id++)
+  {
+    auto size = scc_size[scc_id];
+    if(size > 1)
+    {
+      log.error() << "Found CFG SCC with size " << size << messaget::eom;
+      for(const auto &node_id : node_to_scc)
+      {
+        if(node_to_scc[node_id] == scc_id)
+        {
+          const auto &pc = cfg[node_id].PC;
+          goto_program.output_instruction(ns, "", log.error(), *pc);
+          log.error() << messaget::eom;
+        }
+      }
+      return false;
+    }
+  }
+  return true;
+}

src/goto-instrument/contracts/contracts.h

@@ -223,6 +223,13 @@ class code_contractst
   bool is_auxiliary_decl_dead_or_assign(
     const goto_programt::targett &instruction_it);
 
+  /// Turns goto instructions `IF cond GOTO label` where the condition
+  /// statically simplifies to `false` into SKIP instructions.
+  void simplify_gotos(goto_programt &goto_program);
+
+  /// Returns true iff the given program is loop-free,
+  /// i.e. if each SCC of its CFG contains a single element.
+  bool is_loop_free(const goto_programt &goto_program);
 };
 
 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACTS_H