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

@@ -4,7 +4,7 @@ main.c
 ^EXIT=(1|64)$
 ^SIGNAL=0$
 ^CONVERSION ERROR$
-error: __CPROVER_old expressions are not allowed in __CPROVER_requires clauses
+error: __CPROVER_old expressions are not allowed
 --
 --
 Verification:

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

@@ -0,0 +1,48 @@
+#include <assert.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,9 @@
+CORE
+main.c
+--apply-loop-contracts
+^CONVERSION ERROR$
+^EXIT=1$
+^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,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^CONVERSION ERROR$
+^EXIT=1$
+^SIGNAL=0$
+--
+--
+This test ensures that __CPROVER_loop_entry cannot be
+used for function contracts.

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;
 }

src/ansi-c/c_typecheck_base.cpp

@@ -731,6 +731,7 @@ void c_typecheck_baset::typecheck_declaration(
             typecheck_expr(requires);
             implicit_typecast_bool(requires);
             disallow_history_variables(requires);
+            disallow_loop_history_variables(requires);
           }
         }
 
@@ -751,6 +752,7 @@ void c_typecheck_baset::typecheck_declaration(
           {
             typecheck_expr(ensures);
             implicit_typecast_bool(ensures);
+            disallow_loop_history_variables(ensures);
           }
 
           if(return_type.id() != ID_empty)

src/ansi-c/c_typecheck_base.h

@@ -207,6 +207,7 @@ class c_typecheck_baset:
   virtual exprt
   typecheck_shuffle_vector(const side_effect_expr_function_callt &expr);
   void disallow_history_variables(const exprt &) const;
+  void disallow_loop_history_variables(const exprt &) const;
 
   virtual void make_index_type(exprt &expr);
   virtual void make_constant(exprt &expr);