Full implementation of loop variants

Long Pham · Long Pham · commit 00608b6b12d9 · 2021-07-02T16:26:57.000Z
diff --git a/regression/contracts/invar_check_multiple_loops/test.desc b/regression/contracts/invar_check_multiple_loops/test.desc
@@ -5,8 +5,10 @@ main.c
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
 ^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.3\] .* Check loop invariant before entry: SUCCESS$
-^\[main.4\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.3\] .* Check decreases clause on loop iteration: SUCCESS$
+^\[main.4\] .* Check loop invariant before entry: SUCCESS$
+^\[main.5\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.6\] .* Check decreases clause on loop iteration: SUCCESS$
 ^\[main.assertion.1\] .* assertion x == y \+ 2 \* n: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
diff --git a/regression/contracts/invar_check_nested_loops/main.c b/regression/contracts/invar_check_nested_loops/main.c
@@ -7,7 +7,7 @@ int main()
 
   for(int i = 0; i < n; ++i)
     // clang-format off
-    __CPROVER_loop_invariant(i <= n && s == i)
+    __CPROVER_loop_invariant(0 <= i && i <= n && s == i)
     __CPROVER_decreases(n - i)
     // clang-format on
     {
diff --git a/regression/contracts/invar_check_nested_loops/test.desc b/regression/contracts/invar_check_nested_loops/test.desc
@@ -4,9 +4,11 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.4\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.5\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.6\] .* Check decreases clause on loop iteration: SUCCESS$
 ^\[main.2\] .* Check loop invariant before entry: SUCCESS$
 ^\[main.3\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.4\] .* Check decreases clause on loop iteration: SUCCESS$
 ^\[main.assertion.1\] .* assertion s == n: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
diff --git a/regression/contracts/variant_function_call_fail/main.c b/regression/contracts/variant_function_call_fail/main.c
@@ -0,0 +1,23 @@
+#define N 10
+
+int foo(int i);
+
+int main()
+{
+  int i = 0;
+  while(i != N)
+    // clang-format off
+    __CPROVER_loop_invariant(0 <= i && i <= N) 
+    __CPROVER_decreases(foo(i))
+    // clang-format on
+    {
+      i++;
+    }
+
+  return 0;
+}
+
+int foo(int i)
+{
+  return N - i;
+}
diff --git a/regression/contracts/variant_function_call_fail/test.desc b/regression/contracts/variant_function_call_fail/test.desc
@@ -0,0 +1,14 @@
+CORE
+main.c
+--apply-loop-contracts
+^Decreases clause is not side-effect free. \(at: file main.c line .* function main\)$
+^EXIT=70$
+^SIGNAL=0$
+--
+--
+This test fails because the decreases clause contains a function call. Decreases
+clauses must not contain loops, since we want to ensure that the
+calculation of decreases clauses will terminate. To enforce this requirement, 
+for now, we simply ban decreases clauses from containing function calls. 
+In the future, we may allow function calls (but definitely not loops) to appear
+inside decreases clauses. 
diff --git a/regression/contracts/variant_missing_invariant_warning/main.c b/regression/contracts/variant_missing_invariant_warning/main.c
@@ -0,0 +1,13 @@
+int main()
+{
+  unsigned i = 10;
+  while(i != 0)
+    // clang-format off
+    __CPROVER_decreases(i)
+    // clang-format on
+    {
+      i--;
+    }
+
+  return 0;
+}
diff --git a/regression/contracts/variant_missing_invariant_warning/test.desc b/regression/contracts/variant_missing_invariant_warning/test.desc
@@ -0,0 +1,14 @@
+CORE
+main.c
+--apply-loop-contracts
+activate-multi-line-match
+^The loop at file main.c line 4 function main does not have a loop invariant, but has a decreases clause. Hence, a default loop invariant \('true'\) is being used.$
+^\[main.1\].*Check loop invariant before entry: SUCCESS$
+^\[main.2\].*Check that loop invariant is preserved: SUCCESS$
+^\[main.3\].*Check decreases clause on loop iteration: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This test succeeds, but it gives a warning that the user has not provided a loop
+invariant. Hence, a default loop invariant (i.e. true) will be used. 
diff --git a/regression/contracts/variant_not_decreasing_fail/main.c b/regression/contracts/variant_not_decreasing_fail/main.c
@@ -0,0 +1,16 @@
+
+int main()
+{
+  int i = 0;
+  int N = 10;
+  while(i != N)
+    // clang-format off
+    __CPROVER_loop_invariant(0 <= i && i <= N) 
+    __CPROVER_decreases(i)
+    // clang-format on
+    {
+      i++;
+    }
+
+  return 0;
+}
diff --git a/regression/contracts/variant_not_decreasing_fail/test.desc b/regression/contracts/variant_not_decreasing_fail/test.desc
@@ -0,0 +1,14 @@
+CORE
+main.c
+--apply-loop-contracts
+^main.c function main$
+^\[main.1\] .* Check loop invariant before entry: SUCCESS$
+^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.3\] .* Check decreases clause on loop iteration: FAILURE$
+^.* 1 of 3 failed \(2 iterations\)$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This test fails because the decreases clause is not monotinically decreasing.
diff --git a/regression/contracts/variant_parsing_statement_fail/test.desc b/regression/contracts/variant_parsing_statement_fail/test.desc
@@ -1,13 +1,13 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 activate-multi-line-match
 ^main.c.*error: syntax error before 'int'\n.*__CPROVER_decreases\(int x = 0\)$
 ^PARSING ERROR$
 ^EXIT=(1|64)$
 ^SIGNAL=0$
 --
 --
-This test fails because the loop variant is a statement (more precisely, 
+This test fails because the decreases clause is a statement (more precisely, 
 an assignment) rather than an expression (more precisely, an ACSL binding
 expression).
diff --git a/regression/contracts/variant_parsing_tuple_fail/test.desc b/regression/contracts/variant_parsing_tuple_fail/test.desc
@@ -1,13 +1,13 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 activate-multi-line-match
 ^main.c.*error: syntax error before ','\n.*__CPROVER_decreases\(N - i, 42\)$
 ^PARSING ERROR$
 ^EXIT=(1|64)$
 ^SIGNAL=0$
 --
 --
-This test fails because the loop variant has two arguments instead of just one.
-Currently, we only support loop variants of single arguments - we do not
-support loop variants of tuples (yet). 
+This test fails because the decreases clause has two arguments instead of just one.
+Currently, we only support decreases clauses of single arguments - we do not
+support decreases clauses of tuples (yet). 
diff --git a/regression/contracts/variant_side_effects_fail/main.c b/regression/contracts/variant_side_effects_fail/main.c
@@ -0,0 +1,15 @@
+int main()
+{
+  int i = 0;
+  int N = 10;
+  while(i != N)
+    // clang-format off
+    __CPROVER_loop_invariant(0 <= i && i <= N)
+    __CPROVER_decreases((N+=0) - i)
+    // clang-format on
+    {
+      i++;
+    }
+
+  return 0;
+}
diff --git a/regression/contracts/variant_side_effects_fail/test.desc b/regression/contracts/variant_side_effects_fail/test.desc
@@ -0,0 +1,13 @@
+CORE
+main.c
+--apply-loop-contracts
+^Decreases clause is not side-effect free. \(at: file main.c line .* function main\)$
+^EXIT=70$
+^SIGNAL=0$
+--
+--
+This test fails because the decreases clause contains a side effect, namely
+incrementing variable N by zero. In this case, although the value of N
+remains unchanged after the increment operation, we read from and write to N. 
+So this constitues a side effect. Decreases clauses are banned from containing 
+side effects, since decreases clauses should not modify program states. 
diff --git a/regression/contracts/variant_weak_invariant_fail/main.c b/regression/contracts/variant_weak_invariant_fail/main.c
@@ -0,0 +1,16 @@
+
+int main()
+{
+  int i = 0;
+  int N = 10;
+  while(i != N)
+    // clang-format off
+    __CPROVER_loop_invariant(i <= N)
+    __CPROVER_decreases(N - i)
+    // clang-format on
+    {
+      i++;
+    }
+
+  return 0;
+}
diff --git a/regression/contracts/variant_weak_invariant_fail/test.desc b/regression/contracts/variant_weak_invariant_fail/test.desc
@@ -0,0 +1,15 @@
+CORE
+main.c
+--apply-loop-contracts
+^main.c function main$
+^\[main.1\] .* Check loop invariant before entry: SUCCESS$
+^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.3\] .* Check decreases clause on loop iteration: FAILURE$
+^.* 1 of 3 failed \(2 iterations\)$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This test fails because the loop invariant is not strong enough for the
+termination proof. We must add 0 <= i to the loop invariant. 
diff --git a/regression/contracts/variant_while_true_pass/main.c b/regression/contracts/variant_while_true_pass/main.c
@@ -0,0 +1,20 @@
+
+int main()
+{
+  int i = 0;
+  int N = 10;
+  while(1 == 1)
+    // clang-format off
+    __CPROVER_loop_invariant(0 <= i && i <= N)
+    __CPROVER_decreases(N - i)
+    // clang-format on
+    {
+      if(i == 10)
+      {
+        break;
+      }
+      i++;
+    }
+
+  return 0;
+}
diff --git a/regression/contracts/variant_while_true_pass/test.desc b/regression/contracts/variant_while_true_pass/test.desc
@@ -0,0 +1,16 @@
+CORE
+main.c
+--apply-loop-contracts
+^main.c function main$
+^\[main.1\] .* Check loop invariant before entry: SUCCESS$
+^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.3\] .* Check decreases clause on loop iteration: SUCCESS$
+^.*0 of 3 failed \(1 iterations\)$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This test succeeds. The purpose of this test is to check whether a decreases
+clause can successfully prove the termination of a loop (i) whose exit condition
+is 1 == 1 (i.e. true) and (ii) that will eventually exit via a break statement. 
diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp
diff --git a/src/goto-instrument/code_contracts.h b/src/goto-instrument/code_contracts.h
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h

Original file line number	Diff line number	Diff line change
`@@ -7,7 +7,7 @@ int main()`
`7`	`7`
`8`	`8`	`for(int i = 0; i < n; ++i)`
`9`	`9`	`// clang-format off`
`10`		`- __CPROVER_loop_invariant(i <= n && s == i)`
	`10`	`+ __CPROVER_loop_invariant(0 <= i && i <= n && s == i)`
`11`	`11`	`__CPROVER_decreases(n - i)`
`12`	`12`	`// clang-format on`
`13`	`13`	`{`