Added support for loop_entry history variable.

1. Created a new predicate __CPROVER_loop_entry which can be used in the loop invariant
   to keep track of the value of a variable at the start of the loop.
2. Modified the code contract to support this history variable.

Author: Aalok Thakkar

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

@@ -3,8 +3,8 @@ main.c
 --replace-all-calls-with-contracts
 ^EXIT=(1|64)$
 ^SIGNAL=0$
+^main.c.* error: __CPROVER_old expressions are not allowed in this context$
 ^CONVERSION ERROR$
-error: __CPROVER_old expressions are not allowed in __CPROVER_requires clauses
 --
 --
 Verification:

regression/contracts/loop-history-variables-01/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 == __CPROVER_loop_entry(*s1))
+    {
+      --y3;
+      s1->n = s1->n + 1;
+      s1->n = s1->n - 1;
+    }
+
+  assert(s1->n == s2->n);
+}

regression/contracts/loop-history-variables-01/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/loop-history-variables-02/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/loop-history-variables-02/test.desc

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

regression/contracts/loop-history-variables-03/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/loop-history-variables-03/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^main.c.* error: __CPROVER_loop_entry expressions are not allowed in this context$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test ensures that __CPROVER_loop_entry cannot be
+used for function contracts.

regression/contracts/loop-history-variables-04/main.c

@@ -0,0 +1,16 @@
+#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;
+    }
+  assert(x == z);
+}

regression/contracts/loop-history-variables-04/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--apply-loop-contracts
+^EXIT=(10|6)$
+^SIGNAL=0$
+^\[main.1\] .* Check loop invariant before entry: SUCCESS$
+^\[main.2\] .* Check that loop invariant is preserved: FAILURE$
+^\[main.assertion.1\] .* assertion x == z: SUCCESS$
+^VERIFICATION FAILED$
+--
+--
+This test checks that __CPROVER_loop_entry is sound.

src/ansi-c/c_expr.h

@@ -202,10 +202,11 @@ inline side_effect_expr_overflowt &to_side_effect_expr_overflow(exprt &expr)
 
 /// \brief A class for an expression that indicates the pre-function-call
 /// value of an expression passed as a parameter to a function
-class old_exprt : public unary_exprt
+class history_exprt : public unary_exprt
 {
 public:
-  explicit old_exprt(exprt variable) : unary_exprt(ID_old, std::move(variable))
+  explicit history_exprt(exprt variable, const irep_idt &id)
+    : unary_exprt(id, std::move(variable))
   {
   }
 
@@ -215,10 +216,12 @@ class old_exprt : public unary_exprt
   }
 };
 
-inline const old_exprt &to_old_expr(const exprt &expr)
+inline const history_exprt &
+to_history_expr(const exprt &expr, const irep_idt &id)
 {
-  PRECONDITION(expr.id() == ID_old);
-  auto &ret = static_cast<const old_exprt &>(expr);
+  PRECONDITION(id == ID_old || id == ID_loop_entry);
+  PRECONDITION(expr.id() == id);
+  auto &ret = static_cast<const history_exprt &>(expr);
   validate_expr(ret);
   return ret;
 }