Adds support for pointer history variables in function contracts

This adds support for history variables in function contracts.
History variables are (1) declared and (2) assigned to the
value that their corresponding variable has at function call time.
Currently, only pointers are supported.

Author: ArenBabikian

regression/contracts/history-pointer-enforce-01/main.c

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

regression/contracts/history-pointer-enforce-01/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test checks that history variables are supported for parameters of the
+the function under test. By using the --enforce-all-contracts flag,
+the post-condition (which contains the history variable) is asserted.
+In this case, this assertion should pass.

regression/contracts/history-pointer-enforce-02/main.c

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

regression/contracts/history-pointer-enforce-02/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Verification:
+This test checks that history variables are supported for parameters of the
+the function under test. By using the --enforce-all-contracts flag,
+the post-condition (which contains the history variable) is asserted.
+In this case, this assertion should fail.

regression/contracts/history-pointer-enforce-03/main.c

@@ -0,0 +1,14 @@
+void foo(int *x) __CPROVER_assigns(*x)
+  __CPROVER_requires(*x > 0 && *x < __INT_MAX__ - 5) __CPROVER_ensures(
+    *x >= __CPROVER_old(*x) + 4 && *x <= __CPROVER_old(*x) + 6)
+{
+  *x = *x + 5;
+}
+
+int main()
+{
+  int n;
+  foo(&n);
+
+  return 0;
+}

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

@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-all-contracts _ --trace
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test checks that history variables are supported in the case where a
+history variable is referred to multiple times within an ensures clause.
+By using the --enforce-all-contracts flag, the post-condition (which contains
+the history variable) is asserted. In this case, this assertion should pass.

regression/contracts/history-pointer-enforce-04/main.c

@@ -0,0 +1,15 @@
+void foo(int *x, int *y) __CPROVER_assigns(*x, *y)
+  __CPROVER_ensures(*x == __CPROVER_old(*y) + 1 && *y == __CPROVER_old(*x) + 2)
+{
+  int x_initial = *x;
+  *x = *y + 1;
+  *y = x_initial + 2;
+}
+
+int main()
+{
+  int x, y;
+  foo(&x, &y);
+
+  return 0;
+}

regression/contracts/history-pointer-enforce-04/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test checks that history variables are supported in the case where the
+function under test has multiple parameters. By using the
+--enforce-all-contracts flag, the post-condition (which contains the history
+variables) is asserted. In this case, this assertion should pass.

regression/contracts/history-pointer-enforce-05/main.c

@@ -0,0 +1,14 @@
+void foo(int *x, int *y) __CPROVER_assigns(*x, *y)
+  __CPROVER_ensures(*x == __CPROVER_old(*x) + 2 || *y == __CPROVER_old(*y) + 3)
+{
+  *x = *x + 1;
+  *y = *y + 2;
+}
+
+int main()
+{
+  int x, y;
+  foo(&x, &y);
+
+  return 0;
+}

regression/contracts/history-pointer-enforce-05/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Verification:
+This test checks that history variables are supported in the case where the
+function under test has multiple parameters. By using the
+--enforce-all-contracts flag, the post-condition (which contains the history
+variables) is asserted. In this case, this assertion should fail.

regression/contracts/history-pointer-enforce-06/main.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+void foo(int *x) __CPROVER_assigns(*x)
+  __CPROVER_ensures(*x == __CPROVER_old(*x) + 5)
+{
+  assert(__CPROVER_old(*x) == *x);
+  *x = *x + 5;
+}
+
+int main()
+{
+  int n;
+  foo(&n);
+
+  return 0;
+}

regression/contracts/history-pointer-enforce-06/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Verification:
+This test checks that history variables are not supported when referred to from
+a function body. In such a case, verification should fail.

regression/contracts/history-pointer-enforce-07/main.c

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

regression/contracts/history-pointer-enforce-07/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=1$
+^SIGNAL=0$
+^CONVERSION ERROR$
+--
+--
+Verification:
+This test checks that history variables may only be used with existing
+symbols. In other words, including a new symbol as part of __CPROVER_old()
+is not alowed. In such a case, the program should not parse and there
+should be a conversion error.

regression/contracts/history-pointer-replace-01/main.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+
+void foo(int *x) __CPROVER_assigns(*x) __CPROVER_requires(*x > 0)
+  __CPROVER_ensures(*x == __CPROVER_old(*x) + 2)
+{
+  *x = *x + 2;
+}
+
+int main()
+{
+  int n;
+  __CPROVER_assume(n > 0 && n < __INT_MAX__ - 2);
+  foo(&n);
+
+  assert(n > 2);
+
+  return 0;
+}

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

@@ -0,0 +1,13 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test checks that history variables are supported with the use of the
+--replace-all-calls-with-contracts flag. In this case, the post-condition
+(which contains the history variable) becomes an assumption. We then manually
+assert this assumption. For this test, the assertion should succeed.

regression/contracts/history-pointer-replace-02/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+void foo(int *x) __CPROVER_assigns(*x) __CPROVER_requires(*x == 0)
+  __CPROVER_ensures(*x > __CPROVER_old(*x) + 2)
+{
+  *x = *x + 2;
+}
+
+int main()
+{
+  int n = 0;
+  foo(&n);
+
+  assert(n > 2);
+
+  return 0;
+}

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

@@ -0,0 +1,13 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test checks that history variables are supported with the use of the
+--replace-all-calls-with-contracts flag. In this case, the post-condition
+(which contains the history variable) becomes an assumption. We then manually
+assert this assumption. For this test, the assertion should succeed.

regression/contracts/history-pointer-replace-03/main.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+
+void foo(int *x) __CPROVER_assigns(*x)
+  __CPROVER_requires(*x == __CPROVER_old(*x))
+    __CPROVER_ensures(*x == __CPROVER_old(*x) + 2)
+{
+  *x = *x + 2;
+}
+
+int main()
+{
+  int n = 0;
+  foo(&n);
+
+  assert(n == 2);
+
+  return 0;
+}

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

@@ -0,0 +1,11 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Verification:
+This test checks that history variables cannot be used as part of the
+pre-condition contract. In this case, verification should fail.

src/ansi-c/c_typecheck_expr.cpp

@@ -2575,6 +2575,20 @@ exprt c_typecheck_baset::do_special_functions(
 
     return std::move(ok_expr);
   }
+  else if(identifier == CPROVER_PREFIX "old")
+  {
+    if(expr.arguments().size() != 1)
+    {
+      error().source_location = f_op.source_location();
+      error() << identifier << " expects one operands" << eom;
+      throw 0;
+    }
+
+    old_exprt old_expr(ID_old, expr.arguments()[0]);
+    old_expr.add_source_location() = source_location;
+
+    return std::move(old_expr);
+  }
   else if(identifier==CPROVER_PREFIX "isinff" ||
           identifier==CPROVER_PREFIX "isinfd" ||
           identifier==CPROVER_PREFIX "isinfld" ||

src/ansi-c/cprover_builtin_headers.h

@@ -12,6 +12,7 @@ __CPROVER_size_t __CPROVER_zero_string_length(const void *);
 __CPROVER_size_t __CPROVER_buffer_size(const void *);
 __CPROVER_bool __CPROVER_r_ok(const void *, __CPROVER_size_t);
 __CPROVER_bool __CPROVER_w_ok(const void *, __CPROVER_size_t);
+void __CPROVER_old(const void *);
 
 // bitvector analysis
 __CPROVER_bool __CPROVER_get_flag(const void *, const char *);

src/ansi-c/library/cprover.h

@@ -35,6 +35,7 @@ __CPROVER_size_t __CPROVER_zero_string_length(const void *);
 __CPROVER_size_t __CPROVER_buffer_size(const void *);
 __CPROVER_bool __CPROVER_r_ok(const void *, __CPROVER_size_t);
 __CPROVER_bool __CPROVER_w_ok(const void *, __CPROVER_size_t);
+void __CPROVER_old(const void *);
 
 #if 0
 __CPROVER_bool __CPROVER_equal();