Function contracts: check for the presence of loops before assigns clause instrumentation.

Author: Remi Delmas

regression/contracts/assigns_validity_pointer_01/test.desc

@@ -8,7 +8,6 @@ SUCCESS
 // bar
 ASSERT \*foo::x > 0
 IF ¬\(\*foo::x = 3\) THEN GOTO \d
-IF ¬\(.*0.* = NULL\) THEN GOTO \d
 ASSIGN .*::tmp_if_expr := \(\*\(.*0.*\) = 5 \? true : false\)
 ASSIGN .*::tmp_if_expr\$\d := .*::tmp_if_expr \? true : false
 ASSUME .*::tmp_if_expr\$\d

regression/contracts/function_check_02/main.c

@@ -15,10 +15,16 @@ int initialize(int *arr)
   )
 // clang-format on
 {
-  for(int i = 0; i < 10; i++)
-  {
-    arr[i] = i;
-  }
+  arr[0] = 0;
+  arr[1] = 1;
+  arr[2] = 2;
+  arr[3] = 3;
+  arr[4] = 4;
+  arr[5] = 5;
+  arr[6] = 6;
+  arr[7] = 7;
+  arr[8] = 8;
+  arr[9] = 9;
 
   return 0;
 }

regression/contracts/loop-freeness-check/main.c

@@ -0,0 +1,16 @@
+int foo(int *arr)
+  // clang-format off
+  __CPROVER_assigns(__CPROVER_POINTER_OBJECT(arr))
+// clang-format off
+{
+  for(int i = 0; i < 10; i++)
+    arr[i] = i;
+
+  return 0;
+}
+
+int main()
+{
+  int arr[10];
+  foo(arr);
+}

regression/contracts/loop-freeness-check/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-contract foo
+^--- begin invariant violation report ---$
+^Invariant check failed$
+^Condition: is_loop_free\(.*\)
+^Reason: Loops remain in function 'foo', assigns clause checking instrumentation cannot be applied\.$
+^EXIT=(127|134)$
+^SIGNAL=0$
+--
+--
+This test checks that loops that remain in the program when attempting to 
+instrument assigns clauses are detected and trigger an INVARIANT.

regression/contracts/quantifiers-exists-ensures-enforce/main.c

@@ -7,10 +7,16 @@ int f1(int *arr)
   })
 // clang-format on
 {
-  for(int i = 0; i < 10; i++)
-  {
-    arr[i] = i;
-  }
+  arr[0] = 0;
+  arr[1] = 1;
+  arr[2] = 2;
+  arr[3] = 3;
+  arr[4] = 4;
+  arr[5] = 5;
+  arr[6] = 6;
+  arr[7] = 7;
+  arr[8] = 8;
+  arr[9] = 9;
 
   return 0;
 }
@@ -24,10 +30,16 @@ int f2(int *arr)
   })
 // clang-format on
 {
-  for(int i = 0; i < 10; i++)
-  {
-    arr[i] = 0;
-  }
+  arr[0] = 0;
+  arr[1] = 1;
+  arr[2] = 2;
+  arr[3] = 3;
+  arr[4] = 4;
+  arr[5] = 5;
+  arr[6] = 6;
+  arr[7] = 7;
+  arr[8] = 8;
+  arr[9] = 9;
 
   return 0;
 }

regression/contracts/quantifiers-exists-requires-enforce/main.c

@@ -1,7 +1,7 @@
 #include <stdbool.h>
 #include <stdlib.h>
 
-#define MAX_LEN 64
+#define MAX_LEN 10
 
 // clang-format off
 bool f1(int *arr, int len)
@@ -18,11 +18,27 @@ bool f1(int *arr, int len)
 // clang-format on
 {
   bool found_four = false;
-  for(int i = 0; i <= MAX_LEN; i++)
-  {
-    if(i < len)
-      found_four |= (arr[i] == 4);
-  }
+  if(0 < len)
+    found_four |= (arr[0] == 4);
+  if(1 < len)
+    found_four |= (arr[1] == 4);
+  if(2 < len)
+    found_four |= (arr[2] == 4);
+  if(3 < len)
+    found_four |= (arr[3] == 4);
+  if(4 < len)
+    found_four |= (arr[4] == 4);
+  if(5 < len)
+    found_four |= (arr[5] == 4);
+  if(6 < len)
+    found_four |= (arr[6] == 4);
+  if(7 < len)
+    found_four |= (arr[7] == 4);
+  if(8 < len)
+    found_four |= (arr[8] == 4);
+
+  if(9 < len)
+    found_four |= (arr[9] == 4);
 
   // clang-format off
   return (len > 0 ==> found_four);

regression/contracts/quantifiers-forall-ensures-enforce/main.c

@@ -1,6 +1,6 @@
 #include <stdlib.h>
 
-#define MAX_LEN 16
+#define MAX_LEN 10
 
 // clang-format off
 int f1(int *arr, int len)
@@ -12,11 +12,27 @@ int f1(int *arr, int len)
   })
 // clang-format on
 {
-  for(int i = 0; i < MAX_LEN; i++)
-  {
-    if(i < len)
-      arr[i] = 0;
-  }
+  if(0 < len)
+    arr[0] = 0;
+  if(1 < len)
+    arr[1] = 0;
+  if(2 < len)
+    arr[2] = 0;
+  if(3 < len)
+    arr[3] = 0;
+  if(4 < len)
+    arr[4] = 0;
+  if(5 < len)
+    arr[5] = 0;
+  if(6 < len)
+    arr[6] = 0;
+  if(7 < len)
+    arr[7] = 0;
+  if(8 < len)
+    arr[8] = 0;
+  if(9 < len)
+    arr[9] = 0;
+
   return 0;
 }
 

regression/contracts/quantifiers-forall-ensures-enforce/test.desc

@@ -4,10 +4,11 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
-^\[f1.\d+\] line \d+ Check that arr\[\(.*\)i\] is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that arr\[\(.*\)\d\] is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+^\[f1.\d+\] line \d+ Check that arr\[\(.*\)\d\] is assignable: FAILURE$
 --
 The purpose of this test is to ensure that we can safely use __CPROVER_forall
 within positive contexts (enforced ENSURES clauses).

regression/contracts/quantifiers-forall-requires-enforce/main.c

@@ -12,8 +12,16 @@ bool f1(int *arr)
 // clang-format on
 {
   bool is_identity = true;
-  for(int i = 0; i < 10; ++i)
-    is_identity &= (arr[i] == i);
+  is_identity &= (arr[0] == 0);
+  is_identity &= (arr[1] == 1);
+  is_identity &= (arr[2] == 2);
+  is_identity &= (arr[3] == 3);
+  is_identity &= (arr[4] == 4);
+  is_identity &= (arr[5] == 5);
+  is_identity &= (arr[6] == 6);
+  is_identity &= (arr[7] == 7);
+  is_identity &= (arr[8] == 8);
+  is_identity &= (arr[9] == 9);
   return is_identity;
 }
 

regression/contracts/quantifiers-nested-01/main.c

@@ -11,10 +11,16 @@ int f1(int *arr)
   })
 // clang-format on
 {
-  for(int i = 0; i < 10; i++)
-  {
-    arr[i] = i;
-  }
+  arr[0] = 0;
+  arr[1] = 1;
+  arr[2] = 2;
+  arr[3] = 3;
+  arr[4] = 4;
+  arr[5] = 5;
+  arr[6] = 6;
+  arr[7] = 7;
+  arr[8] = 8;
+  arr[9] = 9;
 
   return 0;
 }

regression/contracts/quantifiers-nested-03/main.c

@@ -10,10 +10,16 @@ __CPROVER_assigns(__CPROVER_POINTER_OBJECT(arr))
   )
 // clang-format on
 {
-  for(int i = 0; i < 10; i++)
-  {
-    arr[i] = i;
-  }
+  arr[0] = 0;
+  arr[1] = 1;
+  arr[2] = 2;
+  arr[3] = 3;
+  arr[4] = 4;
+  arr[5] = 5;
+  arr[6] = 6;
+  arr[7] = 7;
+  arr[8] = 8;
+  arr[9] = 9;
 
   return 0;
 }

src/goto-instrument/contracts/contracts.cpp

@@ -1128,7 +1128,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;
   }
@@ -1149,14 +1151,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
@@ -1168,9 +1173,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, ns);
+
+  // restore internal coherence in the programs
   goto_functions.update();
 
+  INVARIANT(
+    is_loop_free(goto_program, ns, log),
+    "Loops remain in function '" + id2string(function) +
+      "', assigns clause checking instrumentation cannot be applied.");
+
   // Insert write set inclusion checks.
   check_frame_conditions(
     function_obj->first,

src/goto-instrument/contracts/utils.cpp

@@ -10,9 +10,13 @@ Date: September 2021
 
 #include "utils.h"
 
+#include <goto-programs/cfg.h>
 #include <util/fresh_symbol.h>
+#include <util/graph.h>
+#include <util/message.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_predicates.h>
+#include <util/simplify_expr.h>
 
 goto_programt::instructiont &
 add_pragma_disable_assigns_check(goto_programt::instructiont &instr)
@@ -210,3 +214,66 @@ bool is_auxiliary_decl_dead_or_assign(
   return false;
 }
 
+void simplify_gotos(goto_programt &goto_program, namespacet &ns)
+{
+  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 is_loop_free(
+  const goto_programt &goto_program,
+  namespacet &ns,
+  messaget &log)
+{
+  // 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
+  using idxt = graph_nodet<empty_cfg_nodet>::node_indext;
+  std::vector<idxt> 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(size_t 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;
+}