CONTRACTS: Several fixes for loop contracts

+ Disabled loop contract instrumentation along program paths that result in vacuous loops,
  i.e., when the loop guard doesn't hold initially and the loop never runs.
  This allows for significantly simpler loop contracts in some cases.
+ Fixed the instrumentation for decreases clauses.
  It no longer requires the `source_location` hack to find the beginning of loop "body".
+ Added some regression tests for loops that have side effects within guards

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_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.