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,14 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+ASSERT \*tmp_cc\$\d == tmp_cc\$\d \+ 5
+--
+--
+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,14 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+ASSERT \*tmp_cc\$\d < tmp_cc\$\d \+ 5
+--
+--
+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,16 @@
+#include <limits.h>
+
+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,14 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+ASSERT tmp_if_expr\$\d
+--
+--
+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,14 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+ASSERT tmp_if_expr
+--
+--
+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,14 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+ASSERT tmp_if_expr
+--
+--
+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,12 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+warning: ignoring old
+--
+--
+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,14 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=(1|64)$
+^SIGNAL=0$
+^CONVERSION ERROR$
+error: failed to find symbol 'y'
+--
+--
+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,19 @@
+#include <assert.h>
+#include <limits.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,15 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+ASSERT \*\(&n\) > 0
+ASSUME \*\(&n\) == tmp_cc\$\d \+ 2
+--
+--
+Verification:
+This test checks that history variables are supported with the use of the
+--replace-all-calls-with-contracts flag. In this case, the pre-condition
+becomes an assertion and the post-condition (which contains the history
+variable) becomes an assumption.

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,15 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+ASSERT \*\(&n\) == 0
+ASSUME \*\(&n\) >= tmp_cc\$\d \+ 2
+--
+--
+Verification:
+This test checks that history variables are supported with the use of the
+--replace-all-calls-with-contracts flag. In this case, the pre-condition
+becomes an assertion and the post-condition (which contains the history
+variable) becomes an assumption.

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,12 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^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.

src/ansi-c/c_typecheck_base.cpp

@@ -729,6 +729,7 @@ void c_typecheck_baset::typecheck_declaration(
         if(as_const(code_type).requires().is_not_nil())
         {
           auto &requires = code_type.requires();
+          disallow_history_variables(requires);
           typecheck_expr(requires);
           implicit_typecast_bool(requires);
         }

src/ansi-c/c_typecheck_base.h

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

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" ||
@@ -3797,3 +3811,26 @@ void c_typecheck_baset::make_constant_index(exprt &expr)
     throw 0;
   }
 }
+
+void c_typecheck_baset::disallow_history_variables(exprt &expr)
+{
+  for(auto &op : expr.operands())
+  {
+    disallow_history_variables(op);
+  }
+
+  if(expr.id() == ID_side_effect && expr.get(ID_statement) == ID_function_call)
+  {
+    const auto &func_call_expr = to_side_effect_expr_function_call(expr);
+    const exprt &f_op = func_call_expr.function();
+    const irep_idt &identifier = to_symbol_expr(f_op).get_identifier();
+    if(identifier == CPROVER_PREFIX "old")
+    {
+      error().source_location = f_op.source_location();
+      error() << CPROVER_PREFIX
+        "old expressions are not allowed in " CPROVER_PREFIX "requires clauses"
+              << eom;
+      throw 0;
+    }
+  }
+}

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();