CONTRACTS: several fixes for loop contracts

+ disabled loop contract instrumentation along program paths that result in vacuous loop (i.e., the loop guard doesn't hold initially and the loop never runs)
  - this allows for significantly simpler loop contracts
+ also fixed the instrumentation for decreases clauses; no longer need 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/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,36 @@
+#include <assert.h>
+#include <stdlib.h>
+
+#define MAX_SIZE 1000000
+
+int main()
+{
+  size_t size;
+  __CPROVER_assume(size <= MAX_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$