Detect loop locals with goto_rw in DFCC

qinheping · qinheping · commit 7dab9d8dbc63 · 2024-10-31T10:19:33.000-05:00
diff --git a/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/main.c b/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
diff --git a/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/main.c b/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)
diff --git a/regression/contracts-dfcc/invar_assigns_opt/main.c b/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)
diff --git a/regression/contracts-dfcc/invar_check_break_fail/main.c b/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)
diff --git a/regression/contracts-dfcc/invar_check_break_fail/test.desc b/regression/contracts-dfcc/invar_check_break_fail/test.desc
@@ -3,9 +3,9 @@ main.c
 --dfcc main --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.loop_invariant_base.\d+\] line 8 Check invariant before entry for loop .*: SUCCESS$
-^\[main.loop_invariant_step.\d+\] line 8 Check invariant after step for loop .*: SUCCESS$
-^\[main.loop_step_unwinding.\d+\] line 8 Check step was unwound for loop .*: SUCCESS$
+^\[main.loop_invariant_base.\d+\] line 6 Check invariant before entry for loop .*: SUCCESS$
+^\[main.loop_invariant_step.\d+\] line 6 Check invariant after step for loop .*: SUCCESS$
+^\[main.loop_step_unwinding.\d+\] line 6 Check step was unwound for loop .*: SUCCESS$
 ^\[main.assigns.\d+\] .* Check that r is assignable: SUCCESS$
 ^\[main\.assertion\.\d+\] .* assertion r == 0: FAILURE$
 ^VERIFICATION FAILED$
diff --git a/regression/contracts-dfcc/invar_check_break_pass/main.c b/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)
diff --git a/regression/contracts-dfcc/invar_check_break_pass/test.desc b/regression/contracts-dfcc/invar_check_break_pass/test.desc
@@ -3,10 +3,10 @@ main.c
 --dfcc main --apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.loop_invariant_base.\d+\] line 8 Check invariant before entry for loop .*: SUCCESS$
-^\[main.loop_invariant_step.\d+\] line 8 Check invariant after step for loop .*: SUCCESS$
-^\[main.loop_step_unwinding.\d+\] line 8 Check step was unwound for loop .*: SUCCESS$
-^\[main.loop_decreases.\d+\] line 8 Check variant decreases after step for loop .*: SUCCESS$
+^\[main.loop_invariant_base.\d+\] line 6 Check invariant before entry for loop .*: SUCCESS$
+^\[main.loop_invariant_step.\d+\] line 6 Check invariant after step for loop .*: SUCCESS$
+^\[main.loop_step_unwinding.\d+\] line 6 Check step was unwound for loop .*: SUCCESS$
+^\[main.loop_decreases.\d+\] line 6 Check variant decreases after step for loop .*: SUCCESS$
 ^\[main.assigns.\d+\] .* Check that r is assignable: SUCCESS$
 ^\[main\.assertion\.\d+\] .* assertion r == 0 || r == 1: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts-dfcc/invar_check_continue/main.c b/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)
diff --git a/regression/contracts-dfcc/invar_check_continue/test.desc b/regression/contracts-dfcc/invar_check_continue/test.desc
@@ -3,11 +3,11 @@ main.c
 --dfcc main --apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.loop_assigns.\d+\] line 8 Check assigns clause inclusion for loop .*: SUCCESS$
-^\[main.loop_invariant_base.\d+\] line 8 Check invariant before entry for loop .*: SUCCESS$
-^\[main.loop_invariant_step.\d+\] line 8 Check invariant after step for loop .*: SUCCESS$
-^\[main.loop_step_unwinding.\d+\] line 8 Check step was unwound for loop .*: SUCCESS$
-^\[main.loop_decreases.\d+\] line 8 Check variant decreases after step for loop .*: SUCCESS$
+^\[main.loop_assigns.\d+\] line 6 Check assigns clause inclusion for loop .*: SUCCESS$
+^\[main.loop_invariant_base.\d+\] line 6 Check invariant before entry for loop .*: SUCCESS$
+^\[main.loop_invariant_step.\d+\] line 6 Check invariant after step for loop .*: SUCCESS$
+^\[main.loop_step_unwinding.\d+\] line 6 Check step was unwound for loop .*: SUCCESS$
+^\[main.loop_decreases.\d+\] line 6 Check variant decreases after step for loop .*: SUCCESS$
 ^\[main.assigns.\d+\] .* Check that r is assignable: SUCCESS$
 ^\[main\.assertion\.\d+\] .* assertion r == 0: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts-dfcc/invar_check_multiple_loops/main.c b/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)
diff --git a/regression/contracts-dfcc/invar_check_nested_loops/main.c b/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)
diff --git a/regression/contracts-dfcc/invar_check_pointer_modifies-01/main.c b/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)
diff --git a/regression/contracts-dfcc/invar_check_pointer_modifies-02/main.c b/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)
diff --git a/regression/contracts-dfcc/invar_check_sufficiency/main.c b/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)
diff --git a/regression/contracts-dfcc/invar_loop-entry_check/main.c b/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;
 
diff --git a/regression/contracts-dfcc/invar_loop-entry_check/test.desc b/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$
diff --git a/regression/contracts-dfcc/invar_loop-entry_fail/main.c b/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)
diff --git a/regression/contracts-dfcc/invar_loop_constant_fail/main.c b/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)
diff --git a/regression/contracts-dfcc/invar_loop_constant_no_modify/main.c b/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)
diff --git a/regression/contracts-dfcc/invar_loop_constant_pass/main.c b/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
diff --git a/regression/contracts-dfcc/loop_assigns_inference-02/main.c b/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);
     }
 }
diff --git a/regression/contracts-dfcc/loop_assigns_inference-02/test.desc b/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$
diff --git a/regression/contracts-dfcc/loop_assigns_inference-03/main.c b/regression/contracts-dfcc/loop_assigns_inference-03/main.c
@@ -12,4 +12,5 @@ void main()
     {
       b[i] = 1;
     }
+  assert(b[0] = 1);
 }
diff --git a/regression/contracts-dfcc/loop_assigns_target_base_idents/main.c b/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
diff --git a/regression/contracts-dfcc/quantifiers-loop-02/main.c b/regression/contracts-dfcc/quantifiers-loop-02/main.c
@@ -4,6 +4,7 @@
 void main()
 {
   int N, a[MAX_ARRAY_SIZE];
+  a[0] = nondet_int();
   __CPROVER_assume(0 <= N && N < MAX_ARRAY_SIZE);
 
   for(int i = 0; i < N; ++i)
diff --git a/regression/contracts-dfcc/quantifiers-loop-02/test.desc b/regression/contracts-dfcc/quantifiers-loop-02/test.desc
@@ -3,12 +3,12 @@ main.c
 --dfcc main --apply-loop-contracts _ --z3
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.loop_assigns.\d+\] line 9 Check assigns clause inclusion for loop .*: SUCCESS$
-^\[main.loop_assigns.\d+\] line 9 Check assigns clause inclusion for loop .*: SUCCESS$
-^\[main.loop_invariant_base.\d+\] line 9 Check invariant before entry for loop .*: SUCCESS$
-^\[main.loop_invariant_base.\d+\] line 9 Check invariant before entry for loop .*: SUCCESS$
-^\[main.loop_invariant_step.\d+\] line 9 Check invariant after step for loop .*: SUCCESS$
-^\[main.loop_step_unwinding.\d+\] line 9 Check step was unwound for loop .*: SUCCESS$
+^\[main.loop_assigns.\d+\] line 10 Check assigns clause inclusion for loop .*: SUCCESS$
+^\[main.loop_assigns.\d+\] line 10 Check assigns clause inclusion for loop .*: SUCCESS$
+^\[main.loop_invariant_base.\d+\] line 10 Check invariant before entry for loop .*: SUCCESS$
+^\[main.loop_invariant_base.\d+\] line 10 Check invariant before entry for loop .*: SUCCESS$
+^\[main.loop_invariant_step.\d+\] line 10 Check invariant after step for loop .*: SUCCESS$
+^\[main.loop_step_unwinding.\d+\] line 10 Check step was unwound for loop .*: SUCCESS$
 ^\[main.assigns.\d+\] line .* Check that i is assignable: SUCCESS$
 ^\[main.assigns.\d+\] line .* Check that a\[(\(signed (long (long )?)?int\))?i\] is assignable: SUCCESS$
 ^\[main.assertion.\d+\] line .* assertion .*: SUCCESS$
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.h
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp

Original file line number	Diff line number	Diff line change
`@@ -17,7 +17,7 @@ int foo()`
`17`	`17`	`}`
`18`	`18`	`assert(r1 == 0);`
`19`	`19`
`20`		`- int r2, s2 = 1;`
	`20`	`+ int r2 = nondet_int(), s2 = 1;`
`21`	`21`	`__CPROVER_assume(r2 >= 0);`
`22`	`22`	`while(r2 > 0)`
`23`	`23`	`__CPROVER_assigns(r2, s2) __CPROVER_loop_invariant(r2 >= 0 && s2 == 1)`
Original file line number	Diff line number	Diff line change
`@@ -1,8 +1,6 @@`
`1`		`-#include <assert.h>`
`2`		`-`
`3`	`1`	`int main()`
`4`	`2`	`{`
`5`		`- int r;`
	`3`	`+ int r = nondet_int();`
`6`	`4`	`__CPROVER_assume(r >= 0);`
`7`	`5`
`8`	`6`	`while(r > 0)`
Original file line number	Diff line number	Diff line change
`@@ -2,7 +2,7 @@`
`2`	`2`
`3`	`3`	`int main()`
`4`	`4`	`{`
`5`		`- int r, n, x, y;`
	`5`	`+ int r, n, x = nondet_int(), y = nondet_int();`
`6`	`6`	`__CPROVER_assume(n > 0 && x == y);`
`7`	`7`
`8`	`8`	`for(r = 0; r < n; ++r)`