Merge pull request #7541 from qinheping/loop-contracts-dfcc

CONTRACTS: Dynamic frames for loop contracts

Author: qinheping

regression/contracts-dfcc/detect_loop_locals/main.c

@@ -0,0 +1,12 @@
+#include <stdlib.h>
+
+int main()
+{
+  unsigned char *i = malloc(5);
+
+  while(i != i + 5)
+    __CPROVER_loop_invariant(1 == 1)
+    {
+      const char lower = *i++;
+    }
+}

regression/contracts-dfcc/detect_loop_locals/test.desc

@@ -0,0 +1,10 @@
+CORE dfcc-only
+main.c
+--dfcc main --apply-loop-contracts
+^\[main.assigns.\d+\].*line 10 Check that i is assignable: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks that loop local variables do not cause explicit checks.

regression/contracts-dfcc/detect_loop_locals2/main.c

@@ -0,0 +1,28 @@
+static void foo()
+{
+  unsigned i;
+
+  for(i = 0; i < 16; i++)
+    __CPROVER_loop_invariant(1 == 1)
+    {
+      int v = 1;
+    }
+}
+
+static void bar()
+{
+  unsigned i;
+
+  for(i = 0; i < 16; i++)
+    __CPROVER_loop_invariant(1 == 1)
+    {
+      int v = 1;
+    }
+}
+
+int main()
+{
+  bar();
+  foo();
+  foo();
+}

regression/contracts-dfcc/detect_loop_locals2/test.desc

@@ -0,0 +1,11 @@
+CORE dfcc-only
+main.c
+--dfcc main --apply-loop-contracts
+^\[bar.assigns.\d+\].*Check that i is assignable: SUCCESS$
+^\[foo.assigns.\d+\].*Check that i is assignable: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks that loop local variables do not cause explicit checks 

regression/contracts-dfcc/github_6168_infinite_unwinding_bug/main.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+#include <stdlib.h>
+
+static int adder(const int *a, const int *b)
+{
+  return (*a + *b);
+}
+
+int main()
+{
+  int x = 1024;
+
+  int (*local_adder)(const int *, const int *) = adder;
+
+  while(x > 0)
+    __CPROVER_loop_invariant(1 == 1)
+    {
+      x += local_adder(&x, &x); // loop detection fails
+      //x += adder(&x, &x);       // works fine
+    }
+}

regression/contracts-dfcc/github_6168_infinite_unwinding_bug/test.desc

@@ -0,0 +1,13 @@
+CORE dfcc-only
+main.c
+--dfcc main --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+^\[main.loop_assigns.\d+\] line 15 Check assigns clause inclusion for loop .*: SUCCESS$
+^\[main.loop_invariant_base.\d+\] line 15 Check invariant before entry for loop .*: SUCCESS$
+^\[main.loop_invariant_step.\d+\] line 15 Check invariant after step for loop .*: SUCCESS$
+^\[main.loop_step_unwinding.\d+\] line 15 Check step was unwound for loop .*: SUCCESS$
+--
+--
+This is guarding against an issue described in https://github.com/diffblue/cbmc/issues/6168.

regression/contracts-dfcc/history-index/main.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+
+int main()
+{
+  int i, n, x[10];
+  __CPROVER_assume(x[0] == x[9]);
+  while(i < n)
+    __CPROVER_loop_invariant(x[0] == __CPROVER_loop_entry(x[0]))
+    {
+      x[0] = x[9] - 1;
+      x[0]++;
+    }
+  assert(x[0] == x[9]);
+}

regression/contracts-dfcc/history-index/test.desc

@@ -0,0 +1,10 @@
+CORE dfcc-only
+main.c
+--dfcc main --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^Tracking history of index expressions is not supported yet\.
+--
+This test checks that `ID_index` expressions are allowed within history variables.

regression/contracts-dfcc/history-invalid/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+
+int foo(int x)
+{
+  return x;
+}
+
+int main()
+{
+  int i, n, x[10];
+  __CPROVER_assume(x[0] == x[9]);
+  while(i < n)
+    __CPROVER_loop_invariant(x[0] == __CPROVER_loop_entry(foo(x[0])))
+    {
+      x[0] = x[9] - 1;
+      x[0]++;
+    }
+  assert(x[0] == x[9]);
+}

regression/contracts-dfcc/history-invalid/test.desc

@@ -0,0 +1,11 @@
+CORE dfcc-only
+main.c
+--dfcc --apply-loop-contracts
+^main.c.* error: Tracking history of side_effect expressions is not supported yet.$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test ensures that expressions with side effect, such as function calls,
+may not be used in history variables.

regression/contracts-dfcc/invar_assigns_empty/main.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+
+int main()
+{
+  while(1 == 1)
+    __CPROVER_assigns() __CPROVER_loop_invariant(1 == 1)
+    {
+    }
+}

regression/contracts-dfcc/invar_assigns_empty/test.desc

@@ -0,0 +1,14 @@
+CORE dfcc-only
+main.c
+--dfcc main --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[main.loop_assigns.\d+\] line 5 Check assigns clause inclusion for loop .*: SUCCESS$
+^\[main.loop_invariant_base.\d+\] line 5 Check invariant before entry for loop .*: SUCCESS$
+^\[main.loop_invariant_step.\d+\] line 5 Check invariant after step for loop .*: SUCCESS$
+^\[main.loop_step_unwinding.\d+\] line 5 Check step was unwound for loop .*: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that empty assigns clause is supported 
+in loop contracts.

regression/contracts-dfcc/invar_assigns_opt/main.c

@@ -0,0 +1,31 @@
+#include <assert.h>
+
+int main()
+{
+  foo();
+}
+
+int foo()
+{
+  int r1, s1 = 1;
+  __CPROVER_assume(r1 >= 0);
+  while(r1 > 0)
+    __CPROVER_loop_invariant(r1 >= 0 && s1 == 1) __CPROVER_decreases(r1)
+    {
+      s1 = 1;
+      r1--;
+    }
+  assert(r1 == 0);
+
+  int r2, s2 = 1;
+  __CPROVER_assume(r2 >= 0);
+  while(r2 > 0)
+    __CPROVER_assigns(r2, s2) __CPROVER_loop_invariant(r2 >= 0 && s2 == 1)
+      __CPROVER_decreases(r2)
+    {
+      s2 = 1;
+      r2--;
+    }
+  assert(r2 == 0);
+  return 0;
+}

regression/contracts-dfcc/invar_assigns_opt/test.desc

@@ -0,0 +1,28 @@
+CORE dfcc-only
+main.c
+--dfcc main --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[foo.loop_assigns.\d+\] line 12 Check assigns clause inclusion for loop .*: SUCCESS$
+^\[foo.loop_invariant_base.\d+\] line 12 Check invariant before entry for loop .*: SUCCESS$
+^\[foo.loop_invariant_step.\d+\] line 12 Check invariant after step for loop .*: SUCCESS$
+^\[foo.loop_step_unwinding.\d+\] line 12 Check step was unwound for loop .*: SUCCESS$
+^\[foo.loop_decreases.\d+\] line 12 Check variant decreases after step for loop .*: SUCCESS$
+^\[foo.loop_assigns.\d+\] line 22 Check assigns clause inclusion for loop .*: SUCCESS$
+^\[foo.loop_assigns.\d+\] line 22 Check assigns clause inclusion for loop .*: SUCCESS$
+^\[foo.loop_invariant_base.\d+\] line 22 Check invariant before entry for loop .*: SUCCESS$
+^\[foo.loop_invariant_base.\d+\] line 22 Check invariant before entry for loop .*: SUCCESS$
+^\[foo.loop_invariant_step.\d+\] line 22 Check invariant after step for loop .*: SUCCESS$
+^\[foo.loop_step_unwinding.\d+\] line 22 Check step was unwound for loop .*: SUCCESS$
+^\[foo.loop_decreases.\d+\] line 22 Check variant decreases after step for loop .*: SUCCESS$
+^\[foo.assertion.\d+\] .* assertion r1 == 0: SUCCESS$
+^\[foo.assigns.\d+\] .* Check that s2 is assignable: SUCCESS$
+^\[foo.assigns.\d+\] .* Check that r2 is assignable: SUCCESS$
+^\[foo.assertion.\d+\] .* assertion r2 == 0: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that adding assigns clause is optional
+and that if a proof does not require it, then adding an
+appropriate assigns clause does not lead to any 
+unexpected behavior. 

regression/contracts-dfcc/invar_check_break_fail/main.c

@@ -0,0 +1,25 @@
+#include <assert.h>
+
+int main()
+{
+  int r;
+  __CPROVER_assume(r >= 0);
+
+  while(r > 0)
+    __CPROVER_loop_invariant(r >= 0)
+    {
+      --r;
+      if(r <= 1)
+      {
+        break;
+      }
+      else
+      {
+        --r;
+      }
+    }
+
+  assert(r == 0);
+
+  return 0;
+}

regression/contracts-dfcc/invar_check_break_fail/test.desc

@@ -0,0 +1,16 @@
+CORE dfcc-only
+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.assigns.\d+\] .* Check that r is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion r == 0: FAILURE$
+^VERIFICATION FAILED$
+--
+This test is expected to fail along the code path where r is an even integer
+before entering the loop.
+The program is simply incompatible with the desired property in this case --
+there is no loop invariant that can establish the required assertion.

regression/contracts-dfcc/invar_check_break_pass/main.c

@@ -0,0 +1,28 @@
+#include <assert.h>
+
+int main()
+{
+  int r;
+  __CPROVER_assume(r >= 0);
+
+  while(r > 0)
+    // clang-format off
+    __CPROVER_loop_invariant(r >= 0)
+    __CPROVER_decreases(r)
+    // clang-format on
+    {
+      --r;
+      if(r <= 1)
+      {
+        break;
+      }
+      else
+      {
+        --r;
+      }
+    }
+
+  assert(r == 0 || r == 1);
+
+  return 0;
+}

regression/contracts-dfcc/invar_check_break_pass/test.desc

@@ -0,0 +1,14 @@
+CORE dfcc-only
+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.assigns.\d+\] .* Check that r is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion r == 0 || r == 1: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+This test checks that conditionals and `break` are correctly handled.

regression/contracts-dfcc/invar_check_continue/main.c

@@ -0,0 +1,28 @@
+#include <assert.h>
+
+int main()
+{
+  int r;
+  __CPROVER_assume(r >= 0);
+
+  while(r > 0)
+    // clang-format off
+    __CPROVER_loop_invariant(r >= 0)
+    __CPROVER_decreases(r)
+    // clang-format on
+    {
+      --r;
+      if(r < 5)
+      {
+        continue;
+      }
+      else
+      {
+        --r;
+      }
+    }
+
+  assert(r == 0);
+
+  return 0;
+}

regression/contracts-dfcc/invar_check_continue/test.desc

@@ -0,0 +1,15 @@
+CORE dfcc-only
+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.assigns.\d+\] .* Check that r is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion r == 0: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+This test checks that conditionals and `continue` are correctly handled.