Added loop_entry history variables for invariants

In this commit we introduce a new expression, `__CPROVER_loop_entry`,
which can be used within loop invariants to track history of variables.
`__CPROVER_loop_entry(x)` returns the initial value of a variable just
before the very first iteration of a loop.

Co-authored-by: Aalok Thakkar <[email protected]>

Author: SaswatPadhi

regression/contracts/function_loop_history_ensures_fail/main.c

@@ -0,0 +1,13 @@
+void foo(int *x) __CPROVER_assigns(*x)
+  __CPROVER_ensures(*x == __CPROVER_loop_entry(*x) + 5)
+{
+  *x = *x + 5;
+}
+
+int main()
+{
+  int n;
+  foo(&n);
+
+  return 0;
+}

regression/contracts/function_loop_history_ensures_fail/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^main.c.* error: __CPROVER_loop_entry is not allowed within postconditions.$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test ensures that __CPROVER_loop_entry cannot be used within ensures clause.

regression/contracts/function_loop_history_requires_fail/main.c

@@ -0,0 +1,13 @@
+void bar(int *x) __CPROVER_assigns(*x)
+  __CPROVER_requires(*x == __CPROVER_loop_entry(*x) + 5)
+{
+  *x = *x + 5;
+}
+
+int main()
+{
+  int n;
+  foo(&n);
+
+  return 0;
+}

regression/contracts/function_loop_history_requires_fail/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^main.c.* error: __CPROVER_loop_entry is not allowed within preconditions.$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test ensures that __CPROVER_loop_entry cannot be used within requires clause.

regression/contracts/history-pointer-replace-03/test.desc

@@ -1,12 +1,11 @@
 CORE
 main.c
 --replace-all-calls-with-contracts
+^main.c.* error: __CPROVER_old is not allowed within preconditions.$
+^CONVERSION ERROR$
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^CONVERSION ERROR$
-error: __CPROVER_old expressions are not allowed in __CPROVER_requires clauses
 --
 --
-Verification:
 This test checks that history variables cannot be used as part of the
-pre-condition contract. In this case, verification should fail.
+pre-condition (requires) contract.

regression/contracts/invar_function-old_fail/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+void main()
+{
+  int *x, y, z;
+
+  x = &z;
+
+  while(y > 0)
+    __CPROVER_loop_invariant(*x == __CPROVER_old(*x))
+    {
+      --y;
+      *x = *x + 1;
+      *x = *x - 1;
+    }
+  assert(*x == z);
+}

regression/contracts/invar_function-old_fail/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--apply-loop-contracts
+^main.c.* error: __CPROVER_old is not allowed within loop invariants.$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test ensures that __CPROVER_old cannot be used within loop contracts. 

regression/contracts/invar_loop-entry_check/main.c

@@ -0,0 +1,49 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct
+{
+  int *n;
+} s;
+
+void main()
+{
+  int *x1, y1, z1;
+  x1 = &z1;
+
+  while(y1 > 0)
+    __CPROVER_loop_invariant(*x1 == __CPROVER_loop_entry(*x1))
+    {
+      --y1;
+      *x1 = *x1 + 1;
+      *x1 = *x1 - 1;
+    }
+  assert(*x1 == z1);
+
+  int x2, y2, z2;
+  x2 = z2;
+
+  while(y2 > 0)
+    __CPROVER_loop_invariant(x2 == __CPROVER_loop_entry(x2))
+    {
+      --y2;
+      x2 = x2 + 1;
+      x2 = x2 - 1;
+    }
+  assert(x2 == z2);
+
+  int y3;
+  s *s1, *s2;
+  s2->n = malloc(sizeof(int));
+  s1->n = s2->n;
+
+  while(y3 > 0)
+    __CPROVER_loop_invariant(s1->n == __CPROVER_loop_entry(s1->n))
+    {
+      --y3;
+      s1->n = s1->n + 1;
+      s1->n = s1->n - 1;
+    }
+
+  assert(*(s1->n) == *(s2->n));
+}

regression/contracts/invar_loop-entry_check/test.desc

@@ -0,0 +1,18 @@
+CORE
+main.c
+--apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[main.1\] .* Check loop invariant before entry: SUCCESS$
+^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assertion.1\] .* assertion \*x1 == z1: SUCCESS$
+^\[main.3\] .* Check loop invariant before entry: SUCCESS$
+^\[main.4\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assertion.2\] .* assertion x2 == z2: SUCCESS$
+^\[main.5\] .* Check loop invariant before entry: SUCCESS$
+^\[main.6\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assertion.3\] .* assertion \*\(s1->n\) == \*\(s2->n\): SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that __CPROVER_loop_entry is supported.

regression/contracts/invar_loop-entry_fail/main.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+
+void main()
+{
+  int x, y, z;
+  x = z;
+
+  while(y > 0)
+    __CPROVER_loop_invariant(x == __CPROVER_loop_entry(x))
+    {
+      --y;
+      x = x + 1;
+      x = x - 2;
+    }
+}