Detect loop locals with goto_rw in DFCC

regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/main.c

@@ -1,8 +1,11 @@
 void foo()
 {
-  int nondet_var;
-  int __VERIFIER_var;
-  int __CPROVER_var;
+  // Initialize them with `nondet_int` to avoid them being ignored by DFCC.
+  // DFCC ignores variables that are not read/written to outside the loop
+  // or in the loop contracts.
+  int nondet_var = nondet_int();
+  int __VERIFIER_var = nondet_int();
+  int __CPROVER_var = nondet_int();
   for(int i = 10; i > 0; i--)
     // clang-format off
   __CPROVER_assigns(i)

regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/main.c

@@ -1,8 +1,11 @@
 void foo()
 {
-  int nondet_var;
-  int __VERIFIER_var;
-  int __CPROVER_var;
+  // Initialize them with `nondet_int` to avoid them being ignored by DFCC.
+  // DFCC ignores variables that are not read/written to outside the loop
+  // or in the loop contracts.
+  int nondet_var = nondet_int();
+  int __VERIFIER_var = nondet_int();
+  int __CPROVER_var = nondet_int();
   for(int i = 10; i > 0; i--)
     // clang-format off
   __CPROVER_assigns(i,nondet_var, __VERIFIER_var, __CPROVER_var)

regression/contracts-dfcc/invar_loop-entry_check/main.c

@@ -12,7 +12,7 @@ void main()
   x1 = &z1;
 
   while(y1 > 0)
-    __CPROVER_loop_invariant(*x1 == __CPROVER_loop_entry(*x1))
+    __CPROVER_loop_invariant(y1 >= 0 && *x1 == __CPROVER_loop_entry(*x1))
     {
       --y1;
       *x1 = *x1 + 1;
@@ -24,7 +24,7 @@ void main()
   x2 = z2;
 
   while(y2 > 0)
-    __CPROVER_loop_invariant(x2 == __CPROVER_loop_entry(x2))
+    __CPROVER_loop_invariant(y2 >= 0 && x2 == __CPROVER_loop_entry(x2))
     {
       --y2;
       x2 = x2 + 1;
@@ -34,11 +34,12 @@ void main()
 
   int y3;
   s s0, s1, *s2 = &s0;
+  s0.n = malloc(sizeof(int));
   s2->n = malloc(sizeof(int));
   s1.n = s2->n;
 
   while(y3 > 0)
-    __CPROVER_loop_invariant(s2->n == __CPROVER_loop_entry(s2->n))
+    __CPROVER_loop_invariant(y3 >= 0 && s2->n == __CPROVER_loop_entry(s2->n))
     {
       --y3;
       s0.n = s0.n + 1;

regression/contracts-dfcc/invar_loop-entry_check/test.desc

@@ -11,10 +11,10 @@ main.c
 ^\[main.loop_invariant_base.\d+] line 26 Check invariant before entry for loop .*: SUCCESS$
 ^\[main.loop_invariant_step.\d+] line 26 Check invariant after step for loop .*: SUCCESS$
 ^\[main.loop_step_unwinding.\d+] line 26 Check step was unwound for loop .*: SUCCESS$
-^\[main.loop_assigns.\d+] line 40 Check assigns clause inclusion for loop .*: SUCCESS$
-^\[main.loop_invariant_base.\d+] line 40 Check invariant before entry for loop .*: SUCCESS$
-^\[main.loop_invariant_step.\d+] line 40 Check invariant after step for loop .*: SUCCESS$
-^\[main.loop_step_unwinding.\d+] line 40 Check step was unwound for loop .*: SUCCESS$
+^\[main.loop_assigns.\d+] line 41 Check assigns clause inclusion for loop .*: SUCCESS$
+^\[main.loop_invariant_base.\d+] line 41 Check invariant before entry for loop .*: SUCCESS$
+^\[main.loop_invariant_step.\d+] line 41 Check invariant after step for loop .*: SUCCESS$
+^\[main.loop_step_unwinding.\d+] line 41 Check step was unwound for loop .*: SUCCESS$
 ^\[main\.assertion\.\d+\] .* assertion \*x1 == z1: SUCCESS$
 ^\[main\.assertion\.\d+\] .* assertion x2 == z2: SUCCESS$
 ^\[main.assigns.\d+\] .* Check that y1 is assignable: SUCCESS$

regression/contracts-dfcc/invar_loop-entry_fail/main.c

@@ -6,7 +6,7 @@ void main()
   x = z;
 
   while(y > 0)
-    __CPROVER_loop_invariant(x == __CPROVER_loop_entry(x))
+    __CPROVER_loop_invariant(y >= 0 && x == __CPROVER_loop_entry(x))
     {
       --y;
       x = x + 1;

regression/contracts-dfcc/loop_assigns_inference-02/main.c

@@ -10,11 +10,14 @@ void main()
 void foo()
 {
   int *b = malloc(SIZE * sizeof(int));
+  int *j;
   for(unsigned i = 0; i < SIZE; i++)
     // clang-format off
     __CPROVER_loop_invariant(i <= SIZE)
     // clang-format on
     {
+      j = malloc(SIZE * sizeof(int));
       b[i] = 1;
+      free(j);
     }
 }

regression/contracts-dfcc/loop_assigns_inference-02/test.desc

@@ -3,12 +3,12 @@ main.c
 --no-malloc-may-fail --dfcc main --apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[foo.loop_assigns.\d+\] line 13 Check assigns clause inclusion for loop .*: SUCCESS$
-^\[foo.loop_assigns.\d+\] line 13 Check assigns clause inclusion for loop .*: SUCCESS$
-^\[foo.loop_invariant_base.\d+\] line 13 Check invariant before entry for loop .*: SUCCESS$
-^\[foo.loop_invariant_base.\d+\] line 13 Check invariant before entry for loop .*: SUCCESS$
-^\[foo.loop_invariant_step.\d+\] line 13 Check invariant after step for loop .*: SUCCESS$
-^\[foo.loop_step_unwinding.\d+\] line 13 Check step was unwound for loop .*: SUCCESS$
+^\[foo.loop_assigns.\d+\] line 14 Check assigns clause inclusion for loop .*: SUCCESS$
+^\[foo.loop_assigns.\d+\] line 14 Check assigns clause inclusion for loop .*: SUCCESS$
+^\[foo.loop_invariant_base.\d+\] line 14 Check invariant before entry for loop .*: SUCCESS$
+^\[foo.loop_invariant_base.\d+\] line 14 Check invariant before entry for loop .*: SUCCESS$
+^\[foo.loop_invariant_step.\d+\] line 14 Check invariant after step for loop .*: SUCCESS$
+^\[foo.loop_step_unwinding.\d+\] line 14 Check step was unwound for loop .*: SUCCESS$
 ^\[foo.assigns.\d+\] .* Check that i is assignable: SUCCESS$
 ^\[foo.assigns.\d+\] .* Check that b\[(.*)i\] is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$

regression/contracts-dfcc/loop_assigns_inference-03/main.c

@@ -7,7 +7,7 @@ void main()
   int b[SIZE];
   for(unsigned i = 0; i < SIZE; i++)
     // clang-format off
-    __CPROVER_loop_invariant(i <= SIZE)
+    __CPROVER_loop_invariant((i == 0 || b[0] == 1) && i <= SIZE)
     // clang-format on
     {
       b[i] = 1;

src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp

@@ -253,26 +253,6 @@ static bool is_assigned(dirtyt &dirty, const irep_idt &ident, assignst assigns)
   return false;
 }
 
-/// Collect identifiers that are local to this loop only
-/// (excluding nested loop).
-static std::unordered_set<irep_idt> gen_loop_locals_set(
-  const dfcc_loop_nesting_grapht &loop_nesting_graph,
-  const std::size_t loop_id)
-{
-  std::unordered_set<irep_idt> loop_locals;
-  for(const auto &target : loop_nesting_graph[loop_id].instructions)
-  {
-    auto loop_id_opt = dfcc_get_loop_id(target);
-    if(
-      target->is_decl() && loop_id_opt.has_value() &&
-      loop_id_opt.value() == loop_id)
-    {
-      loop_locals.insert(target->decl_symbol().get_identifier());
-    }
-  }
-  return loop_locals;
-}
-
 /// Compute subset of locals that must be tracked in the loop's write set.
 /// A local must be tracked if it is dirty or if it may be assigned by one
 /// of the inner loops.
@@ -329,6 +309,7 @@ static struct contract_clausest default_loop_contract_clauses(
   const dfcc_loop_nesting_grapht &loop_nesting_graph,
   const std::size_t loop_id,
   const irep_idt &function_id,
+  goto_functiont &goto_function,
   local_may_aliast &local_may_alias,
   const bool check_side_effect,
   message_handlert &message_handler,
@@ -381,7 +362,7 @@ static struct contract_clausest default_loop_contract_clauses(
     {
       // infer assigns clause targets if none given
       auto inferred = dfcc_infer_loop_assigns(
-        local_may_alias, loop.instructions, loop.head->source_location(), ns);
+        local_may_alias, goto_function, loop, message_handler, ns);
       log.warning() << "No assigns clause provided for loop " << function_id
                     << "." << loop.latch->loop_number << " at "
                     << loop.head->source_location() << ". The inferred set {";
@@ -416,6 +397,7 @@ static dfcc_loop_infot gen_dfcc_loop_info(
   const dfcc_loop_nesting_grapht &loop_nesting_graph,
   const std::size_t loop_id,
   const irep_idt &function_id,
+  goto_functiont &goto_function,
   const std::map<std::size_t, dfcc_loop_infot> &loop_info_map,
   dirtyt &dirty,
   local_may_aliast &local_may_alias,
@@ -424,20 +406,37 @@ static dfcc_loop_infot gen_dfcc_loop_info(
   dfcc_libraryt &library,
   symbol_table_baset &symbol_table)
 {
-  std::unordered_set<irep_idt> loop_locals =
-    gen_loop_locals_set(loop_nesting_graph, loop_id);
+  const namespacet ns(symbol_table);
+  std::unordered_set<irep_idt> loop_locals = gen_loop_locals_set(
+    function_id,
+    goto_function,
+    loop_nesting_graph[loop_id],
+    message_handler,
+    ns);
+
+  // Exclude locals of inner nested loops.
+  for(const auto &inner_loop : loop_nesting_graph.get_predecessors(loop_id))
+  {
+    INVARIANT(
+      loop_info_map.find(inner_loop) != loop_info_map.end(),
+      "DFCC should gen_dfcc_loop_info for inner loops first.");
+    for(const auto &inner_local : loop_info_map.at(inner_loop).local)
+    {
+      loop_locals.erase(inner_local);
+    }
+  }
 
   std::unordered_set<irep_idt> loop_tracked = gen_tracked_set(
     loop_nesting_graph.get_predecessors(loop_id),
     loop_locals,
     dirty,
     loop_info_map);
 
-  const namespacet ns(symbol_table);
   struct contract_clausest contract_clauses = default_loop_contract_clauses(
     loop_nesting_graph,
     loop_id,
     function_id,
+    goto_function,
     local_may_alias,
     check_side_effect,
     message_handler,
@@ -559,6 +558,7 @@ dfcc_cfg_infot::dfcc_cfg_infot(
          loop_nesting_graph,
          loop_id,
          function_id,
+         goto_function,
          loop_info_map,
          dirty,
          local_may_alias,

src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp

@@ -13,6 +13,7 @@ Author: Remi Delmas, delmasrd@amazon.com
 #include <util/pointer_expr.h>
 #include <util/std_code.h>
 
+#include <analyses/goto_rw.h>
 #include <goto-instrument/contracts/utils.h>
 #include <goto-instrument/havoc_utils.h>
 
@@ -46,23 +47,127 @@ depends_on(const exprt &expr, std::unordered_set<irep_idt> identifiers)
   return false;
 }
 
+/// Collect identifiers that are local to this loop.
+/// A identifier is or is equivalent to a loop local if
+/// 1. it is declared inside the loop, or
+/// 2. there is no write or read of it outside the loop.
+/// 3. it is not used in loop contracts.
+std::unordered_set<irep_idt> gen_loop_locals_set(
+  const irep_idt &function_id,
+  goto_functiont &goto_function,
+  const dfcc_loop_nesting_graph_nodet &loop_node,
+  message_handlert &message_handler,
+  const namespacet &ns)
+{
+  std::unordered_set<irep_idt> loop_locals;
+  std::unordered_set<irep_idt> non_loop_locals;
+
+  const auto &loop = loop_node.instructions;
+
+  // All identifiers declared outside the loop.
+  std::unordered_set<irep_idt> non_loop_decls;
+  // Ranges of all read/write outside the loop.
+  rw_range_sett non_loop_rw_range_set(ns, message_handler);
+
+  Forall_goto_program_instructions(i_it, goto_function.body)
+  {
+    // All variables declared in loops are loop locals.
+    if(i_it->is_decl() && loop.contains(i_it))
+    {
+      loop_locals.insert(i_it->decl_symbol().get_identifier());
+    }
+    // Record all other declared variables and their ranges.
+    else if(i_it->is_decl())
+    {
+      non_loop_decls.insert(i_it->decl_symbol().get_identifier());
+    }
+    // Record all writing/reading outside the loop.
+    else if(
+      (i_it->is_assign() || i_it->is_function_call()) && !loop.contains(i_it))
+    {
+      goto_rw(function_id, i_it, non_loop_rw_range_set);
+    }
+  }
+
+  // Check if declared variables are loop locals.
+  for(const auto &decl_id : non_loop_decls)
+  {
+    bool is_loop_local = true;
+    // No write to the declared variable.
+    for(const auto &writing_rw : non_loop_rw_range_set.get_w_set())
+    {
+      if(decl_id == writing_rw.first)
+      {
+        is_loop_local = false;
+        break;
+      }
+    }
+
+    // No read to the declared variable.
+    for(const auto &writing_rw : non_loop_rw_range_set.get_r_set())
+    {
+      if(decl_id == writing_rw.first)
+      {
+        is_loop_local = false;
+        break;
+      }
+    }
+
+    const auto latch_target = loop_node.latch;
+
+    // Loop locals are not used in loop contracts.
+    for(const auto &id :
+        find_symbol_identifiers(get_loop_assigns(latch_target)))
+    {
+      if(decl_id == id)
+      {
+        is_loop_local = false;
+        break;
+      }
+    }
+
+    for(const auto &id :
+        find_symbol_identifiers(get_loop_invariants(latch_target, false)))
+    {
+      if(decl_id == id)
+      {
+        is_loop_local = false;
+        break;
+      }
+    }
+
+    for(const auto &id :
+        find_symbol_identifiers(get_loop_decreases(latch_target, false)))
+    {
+      if(decl_id == id)
+      {
+        is_loop_local = false;
+        break;
+      }
+    }
+
+    // Collect all loop locals.
+    if(is_loop_local)
+      loop_locals.insert(decl_id);
+  }
+
+  return loop_locals;
+}
+
 assignst dfcc_infer_loop_assigns(
   const local_may_aliast &local_may_alias,
-  const loopt &loop_instructions,
-  const source_locationt &loop_head_location,
+  goto_functiont &goto_function,
+  const dfcc_loop_nesting_graph_nodet &loop,
+  message_handlert &message_handler,
   const namespacet &ns)
 {
   // infer
   assignst assigns;
-  infer_loop_assigns(local_may_alias, loop_instructions, assigns);
+  infer_loop_assigns(local_may_alias, loop.instructions, assigns);
 
   // compute locals
-  std::unordered_set<irep_idt> loop_locals;
-  for(const auto &target : loop_instructions)
-  {
-    if(target->is_decl())
-      loop_locals.insert(target->decl_symbol().get_identifier());
-  }
+  std::unordered_set<irep_idt> loop_locals =
+    gen_loop_locals_set(irep_idt(), goto_function, loop, message_handler, ns);
 
   // widen or drop targets that depend on loop-locals or are non-constant,
   // ie. depend on other locations assigned by the loop.