Detect loop locals with goto_rw in DFCC

regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/main.c

@@ -1,11 +1,11 @@
 void foo()
 {
-  int nondet_var;
-  int __VERIFIER_var;
-  int __CPROVER_var;
+  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)
+   __CPROVER_assigns(i)
   __CPROVER_loop_invariant(0 <= i && i <= 10)
   __CPROVER_decreases(i)
     // clang-format on

regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/main.c

@@ -1,8 +1,8 @@
 void foo()
 {
-  int nondet_var;
-  int __VERIFIER_var;
-  int __CPROVER_var;
+  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_assigns_opt/main.c

@@ -17,7 +17,7 @@ int foo()
     }
   assert(r1 == 0);
 
-  int r2, s2 = 1;
+  int r2 = nondet_int(), s2 = 1;
   __CPROVER_assume(r2 >= 0);
   while(r2 > 0)
     __CPROVER_assigns(r2, s2) __CPROVER_loop_invariant(r2 >= 0 && s2 == 1)

regression/contracts-dfcc/invar_check_break_fail/main.c

@@ -1,8 +1,6 @@
-#include <assert.h>
-
 int main()
 {
-  int r;
+  int r = nondet_int();
   __CPROVER_assume(r >= 0);
 
   while(r > 0)

regression/contracts-dfcc/invar_check_break_pass/main.c

@@ -1,8 +1,6 @@
-#include <assert.h>
-
 int main()
 {
-  int r;
+  int r = nondet_int();
   __CPROVER_assume(r >= 0);
 
   while(r > 0)

regression/contracts-dfcc/invar_check_continue/main.c

@@ -1,8 +1,6 @@
-#include <assert.h>
-
 int main()
 {
-  int r;
+  int r = nondet_int();
   __CPROVER_assume(r >= 0);
 
   while(r > 0)

regression/contracts-dfcc/invar_check_multiple_loops/main.c

@@ -2,7 +2,7 @@
 
 int main()
 {
-  int r, n, x, y;
+  int r, n, x = nondet_int(), y = nondet_int();
   __CPROVER_assume(n > 0 && x == y);
 
   for(r = 0; r < n; ++r)

regression/contracts-dfcc/invar_check_nested_loops/main.c

@@ -2,7 +2,7 @@
 
 int main()
 {
-  int n, s = 0;
+  int n = nondet_int(), s = 0;
   __CPROVER_assume(n >= 0);
 
   for(int i = 0; i < n; ++i)
@@ -11,7 +11,7 @@ int main()
     __CPROVER_decreases(n - i)
     // clang-format on
     {
-      int a, b;
+      int a = nondet_int(), b = nondet_int();
       __CPROVER_assume(b >= 0 && a == b);
 
       while(a > 0)

regression/contracts-dfcc/invar_check_pointer_modifies-01/main.c

@@ -6,7 +6,7 @@ void main()
   char *data = malloc(1);
   *data = 42;
 
-  unsigned i;
+  unsigned i = nondet_int();
   while(i > 0)
     // clang-format off
     __CPROVER_loop_invariant(*data == 42)

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

@@ -8,7 +8,7 @@ void main()
   copy = data;
   *data = 42;
 
-  unsigned i;
+  unsigned i = nondet_int();
   while(i > 0)
     // clang-format off
     __CPROVER_loop_invariant(*data == 42)

regression/contracts-dfcc/invar_check_sufficiency/main.c

@@ -2,7 +2,7 @@
 
 int main()
 {
-  int r;
+  int r = nondet_int();
   __CPROVER_assume(r >= 0);
 
   while(r > 0)

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

@@ -8,7 +8,7 @@ typedef struct
 
 void main()
 {
-  int *x1, y1, z1;
+  int *x1, y1 = nondet_int(), z1;
   x1 = &z1;
 
   while(y1 > 0)
@@ -20,7 +20,7 @@ void main()
     }
   assert(*x1 == z1);
 
-  int x2, y2, z2;
+  int x2, y2 = nondet_int(), z2;
   x2 = z2;
 
   while(y2 > 0)
@@ -32,8 +32,9 @@ void main()
     }
   assert(x2 == z2);
 
-  int y3;
+  int y3 = nondet_int();
   s s0, s1, *s2 = &s0;
+  s0.n = nondet_int();
   s2->n = malloc(sizeof(int));
   s1.n = s2->n;
 

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

@@ -2,7 +2,7 @@
 
 void main()
 {
-  int x, y, z;
+  int x = nondet_int(), y = nondet_int(), z = nondet_int();
   x = z;
 
   while(y > 0)

regression/contracts-dfcc/invar_loop_constant_fail/main.c

@@ -2,7 +2,7 @@
 
 int main()
 {
-  int r;
+  int r = nondet_int();
   int s = 1;
   __CPROVER_assume(r >= 0);
   while(r > 0)

regression/contracts-dfcc/invar_loop_constant_no_modify/main.c

@@ -2,7 +2,7 @@
 
 int main()
 {
-  int r;
+  int r = nondet_int();
   int s = 1;
   __CPROVER_assume(r >= 0);
   while(r > 0)

regression/contracts-dfcc/invar_loop_constant_pass/main.c

@@ -2,7 +2,7 @@
 
 int main()
 {
-  int r, s = 1;
+  int r = nondet_int(), s = 1;
   __CPROVER_assume(r >= 0);
   while(r > 0)
     // clang-format off

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

@@ -12,4 +12,5 @@ void main()
     {
       b[i] = 1;
     }
+  assert(b[0] = 1);
 }

regression/contracts-dfcc/loop_assigns_target_base_idents/main.c

@@ -6,6 +6,9 @@ int foo() __CPROVER_assigns()
   char buf1[SIZE];
   char buf2[SIZE];
   char buf3[SIZE];
+  buf1[0]= 0;
+  buf2[0]= 0;
+  buf3[0]= 0;
   size_t i = 0;
   while(i < SIZE)
     // clang-format off

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,12 @@ 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.instructions,
+        loop.head->source_location(),
+        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 +402,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 +411,25 @@ 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].instructions,
+    message_handler,
+    ns);
 
   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 +551,7 @@ dfcc_cfg_infot::dfcc_cfg_infot(
          loop_nesting_graph,
          loop_id,
          function_id,
+         goto_function,
          loop_info_map,
          dirty,
          local_may_alias,