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-both-01/main.c

@@ -0,0 +1,20 @@
+#include <stdio.h>
+
+void bar(int *l) __CPROVER_assigns(*l) __CPROVER_requires(l != NULL)
+  __CPROVER_ensures(__CPROVER_old(*l) == *l)
+{
+}
+
+void foo(int *n) __CPROVER_assigns(*n) __CPROVER_requires(n != NULL)
+  __CPROVER_ensures(__CPROVER_old(*n) == *n)
+{
+  bar(n);
+}
+
+int main()
+{
+  int m;
+  foo(&m);
+
+  return 0;
+}

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

@@ -0,0 +1,17 @@
+CORE
+main.c
+--enforce-contract foo --replace-call-with-contract bar
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+ASSUME tmp_cc\$\d != \(\(signed int \*\)NULL\)
+ASSERT n != \(\(signed int \*\)NULL\)
+ASSUME tmp_cc == \*n
+ASSERT tmp_cc\$\d == \*tmp_cc\$\d
+--
+--
+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-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-enforce-08/main.c

@@ -0,0 +1,24 @@
+#include <stdlib.h>
+
+struct pair
+{
+  int *x;
+  int *y;
+};
+
+void foo(struct pair p) __CPROVER_assigns(*(p.y))
+  __CPROVER_ensures(*(p.y) == __CPROVER_old(*(p.y)) + 5)
+{
+  *(p.y) = *(p.y) + 5;
+}
+
+int main()
+{
+  struct pair p;
+  p.x = malloc(sizeof(int));
+  p.y = malloc(sizeof(int));
+
+  foo(p);
+
+  return 0;
+}

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

@@ -0,0 +1,14 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+ASSERT \*tmp_cc\$\d\.y == tmp_cc\$\d \+ 5
+--
+--
+Verification:
+This test checks that history variables are supported for dereferences over
+pointers to struct members. 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-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.

scripts/expected_doxygen_warnings.txt

@@ -35,6 +35,6 @@ warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (1
 warning: Included by graph for 'prefix.h' not generated, too many nodes (85), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (79), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_code.h' not generated, too many nodes (79), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'std_expr.h' not generated, too many nodes (241), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'std_expr.h' not generated, too many nodes (242), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_types.h' not generated, too many nodes (96), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'symbol_table.h' not generated, too many nodes (95), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.