Merge pull request #6701 from padhi-aws-forks/loop-contracts-simplify

CONTRACTS: Several fixes and sanity checks for loop contracts instrumentation

Author: SaswatPadhi

regression/contracts/invar_check_nested_loops/test.desc

@@ -9,9 +9,9 @@ main.c
 ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
 ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
 ^\[main\.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
-^\[main.assigns.\d+] line 23 Check that s is assignable: SUCCESS$
-^\[main.assigns.\d+] line 24 Check that a is assignable: SUCCESS$
-^\[main.assigns.\d+] line 27 Check that s is assignable: SUCCESS$
+^\[main.assigns.\d+] .* line 23 Check that s is assignable: SUCCESS$
+^\[main.assigns.\d+] .* line 24 Check that a is assignable: SUCCESS$
+^\[main.assigns.\d+] .* line 27 Check that s is assignable: SUCCESS$
 ^\[main\.assertion.\d+\] .* assertion s == n: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --

regression/contracts/loop_contracts_reject_overlapping_loops/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+
+int main()
+{
+  int i = 0, j = 0, k = 0;
+
+  while(j < 10)
+  {
+    while(k < 10)
+      __CPROVER_loop_invariant(1 == 1)
+      {
+        while(i < 10)
+        {
+          i++;
+        }
+      }
+    j++;
+  }
+}

regression/contracts/loop_contracts_reject_overlapping_loops/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--apply-loop-contracts
+activate-multi-line-match
+Inner loop at: file main.c line 12 function main does not have contracts, but an enclosing loop does.\nPlease provide contracts for this loop, or unwind it first.
+^EXIT=(6|10)$
+^SIGNAL=0$
+--
+--
+This test checks that our instrumentation routines verify that inner loops
+either have contracts or are unwound, if any enclosing loop has contracts.

regression/contracts/loop_guard_with_side_effects/main.c

@@ -0,0 +1,29 @@
+#include <assert.h>
+#include <limits.h>
+#include <stdbool.h>
+
+bool check(unsigned *i, unsigned *j, unsigned *k)
+{
+  (*j)++;
+  return *i < *k;
+}
+
+int main()
+{
+  unsigned i, j, k;
+  __CPROVER_assume(k < UINT_MAX);
+
+  i = j = 0;
+
+  while(check(&i, &j, &k))
+    // clang-format off
+    __CPROVER_assigns(i, j)
+    __CPROVER_loop_invariant(0 <= i && i == j && i <= k)
+    // clang-format on
+    {
+      i++;
+    }
+
+  assert(i == k);
+  assert(j == k + 1);
+}

regression/contracts/loop_guard_with_side_effects/test.desc

@@ -0,0 +1,26 @@
+CORE
+main.c
+--apply-loop-contracts _ --unsigned-overflow-check
+\[check.assigns\.\d+\] line \d+ Check that \*j is assignable: SUCCESS$
+\[check.overflow\.\d+\] line \d+ arithmetic overflow on unsigned \+ in \*j \+ 1u: SUCCESS
+\[check.overflow\.\d+\] line \d+ arithmetic overflow on unsigned \+ in \*j \+ 1u: SUCCESS
+\[check.assigns\.\d+\] line \d+ Check that return_value_check is assignable: SUCCESS$
+\[main\.\d+\] line \d+ Check loop invariant before entry: SUCCESS$
+\[main\.\d+\] line \d+ Check that loop invariant is preserved: SUCCESS$
+\[main.assigns\.\d+\] line \d+ Check that i is assignable: SUCCESS$
+\[main.assigns\.\d+\] line \d+ Check that j is assignable: SUCCESS$
+\[main.assigns\.\d+\] line \d+ Check that k is assignable: SUCCESS$
+\[main.assigns\.\d+\] line \d+ Check that i is valid: SUCCESS$
+\[main.assigns\.\d+\] line \d+ Check that j is valid: SUCCESS$
+\[main.assigns\.\d+\] line \d+ Check that i is assignable: SUCCESS$
+\[main.overflow\.\d+\] line \d+ arithmetic overflow on unsigned \+ in i \+ 1u: SUCCESS
+\[main.assertion\.\d+\] line \d+ assertion i == k: SUCCESS$
+\[main.overflow\.\d+\] line \d+ arithmetic overflow on unsigned \+ in k \+ \(unsigned int\)1: SUCCESS
+\[main.assertion\.\d+\] line \d+ assertion j == k \+ 1: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This test demonstrates a case where the loop guard has side effects.
+The loop contracts must specify the state of all modified variables,
+including those in the loop guard.

regression/contracts/loop_guard_with_side_effects_fail/main.c

@@ -0,0 +1,26 @@
+#include <assert.h>
+#include <stdbool.h>
+
+bool check(unsigned *i, unsigned *j, unsigned *k)
+{
+  (*j)++;
+  return *i < *k;
+}
+
+int main()
+{
+  unsigned i, j, k;
+
+  i = j = 0;
+
+  while(check(&i, &j, &k))
+    // clang-format off
+    __CPROVER_assigns(i)
+    __CPROVER_loop_invariant(0 <= i && i <= k)
+    // clang-format on
+    {
+      i++;
+    }
+
+  assert(i == k);
+}

regression/contracts/loop_guard_with_side_effects_fail/test.desc

@@ -0,0 +1,20 @@
+CORE
+main.c
+--apply-loop-contracts _ --unsigned-overflow-check
+\[check.assigns\.\d+\] line \d+ Check that \*j is assignable: FAILURE$
+\[check.assigns\.\d+\] line \d+ Check that return_value_check is assignable: SUCCESS$
+\[main\.\d+\] line \d+ Check loop invariant before entry: SUCCESS$
+\[main\.\d+\] line \d+ Check that loop invariant is preserved: SUCCESS$
+\[main.assigns\.\d+\] line \d+ Check that i is assignable: SUCCESS$
+\[main.assigns\.\d+\] line \d+ Check that j is assignable: SUCCESS$
+\[main.assigns\.\d+\] line \d+ Check that k is assignable: SUCCESS$
+\[main.assigns\.\d+\] line \d+ Check that i is valid: SUCCESS$
+\[main.assigns\.\d+\] line \d+ Check that i is assignable: SUCCESS$
+\[main.assertion\.\d+\] line \d+ assertion i == k: SUCCESS$
+^EXIT=(6|10)$
+^SIGNAL=0$
+--
+--
+This test demonstrates a case where the loop guard has side effects.
+The writes performed in the guard must also be specified
+in the assigns clause of the loop.

regression/contracts/nonvacuous_loop_contracts/main.c

@@ -0,0 +1,33 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main()
+{
+  size_t size;
+
+  char *buf = malloc(size);
+  char c;
+
+  size_t start;
+  size_t end = start;
+
+  while(end < size)
+    // clang-format off
+    __CPROVER_loop_invariant(start <= end && end <= size)
+    __CPROVER_decreases(size - end)
+    // clang-format on
+    {
+      if(buf[end] != c)
+        break;
+      end++;
+    }
+
+  if(start > size)
+  {
+    assert(end == start);
+  }
+  else
+  {
+    assert(start <= end && end <= size);
+  }
+}

regression/contracts/nonvacuous_loop_contracts/test.desc

@@ -0,0 +1,25 @@
+CORE
+main.c
+--apply-loop-contracts _ --signed-overflow-check --unsigned-overflow-check
+\[main.\d+\] line \d+ Check loop invariant before entry: SUCCESS$
+\[main.\d+\] line \d+ Check that loop invariant is preserved: SUCCESS$
+\[main.assigns.\d+\] line \d+ Check that end is valid: SUCCESS$
+\[main.assigns.\d+\] line \d+ Check that end is assignable: SUCCESS$
+\[main.assertion.\d+\] line \d+ assertion end == start: SUCCESS$
+\[main.assertion.\d+\] line \d+ assertion start <= end && end <= size: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This test demonstrates a simplification that is now possible on loop contracts.
+
+Prior to this commit, loop contracts were unconditionally applied on loops,
+and thus had to also consider the case when the loop doesn't run even once.
+
+The contracts that were previously necessary were:
+  __CPROVER_loop_invariant(
+    (start > size && end == start) || (start <= end && end <= size)
+  )
+  __CPROVER_decreases(
+    max(start, size) - end
+  )

regression/contracts/variant_missing_invariant_warning/test.desc

@@ -2,7 +2,7 @@ CORE
 main.c
 --apply-loop-contracts
 activate-multi-line-match
-^The loop at file main.c line 4 function main does not have an invariant.*.\nHence, a default invariant \('true'\) is being used to prove those.$
+^The loop at file main.c line 4 function main does not have an invariant.*.\nHence, a default invariant \('true'\) is being used.*.$
 ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
 ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
 ^\[main\.\d+\] .* Check decreases clause on loop iteration: SUCCESS$

regression/contracts/variant_multi_instruction_loop_head/main.c

@@ -5,7 +5,7 @@ int main()
 
   while(*y <= 0 && *y < 10)
     // clang-format off
-    __CPROVER_loop_invariant(1 == 1)
+    __CPROVER_loop_invariant(0 <= *y && *y <= 10)
     __CPROVER_decreases(10 - x)
     // clang-format on
     {

regression/contracts/variant_multi_instruction_loop_head/test.desc

@@ -1,19 +1,16 @@
 CORE
 main.c
 --apply-loop-contracts
-^VERIFICATION FAILED$
-^EXIT=10$
+\[main\.\d+\] line \d+ Check loop invariant before entry: SUCCESS$
+\[main\.\d+\] line \d+ Check that loop invariant is preserved: SUCCESS$
+\[main\.\d+\] line \d+ Check decreases clause on loop iteration: SUCCESS$
+\[main\.\d+\] line \d+ Check that loop instrumentation was not truncated: SUCCESS$
+\[main\.assigns\.\d+\] line \d+ Check that x is valid: SUCCESS$
+\[main\.assigns\.\d+\] line \d+ Check that x is assignable: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
 ^SIGNAL=0$
 --
 --
-This test fails even without the fix proposed in the commit, so it should be improved.
-It is expected to fail because the proposed invariant isn't strong enough to help prove
-termination using the specified variant.
-
-The test highlights a case where a C loop guard is compiled to multiple GOTO instructions.
-Therefore the loop_head pointer needs to be advanced multiple times to get to the loop body,
-where the initial value of the loop variant (/ ranking function) must be recorded.
-
-The proposed fix advances the pointer until the source_location differs from the original
-loop_head's source_location. However, this might still not work if the loop guard in the
-original C code was split across multiple lines in the first place.
+This test checks that decreases clause is properly initialized
+when the loop head and loop invariant compilation emit several goto instructions.