Merge pull request #6025 from ArenBabikian/ghost-variables

feliperodri · web-flow · commit e645434d1fa4 · 2021-05-13T12:28:34.000-04:00
Supports history variables in function contracts
diff --git a/regression/contracts/history-pointer-both-01/main.c b/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;
+}
diff --git a/regression/contracts/history-pointer-both-01/test.desc b/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.
diff --git a/regression/contracts/history-pointer-enforce-01/main.c b/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;
+}
diff --git a/regression/contracts/history-pointer-enforce-01/test.desc b/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.
diff --git a/regression/contracts/history-pointer-enforce-02/main.c b/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;
+}
diff --git a/regression/contracts/history-pointer-enforce-02/test.desc b/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.
diff --git a/regression/contracts/history-pointer-enforce-03/main.c b/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;
+}
diff --git a/regression/contracts/history-pointer-enforce-03/test.desc b/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.
diff --git a/regression/contracts/history-pointer-enforce-04/main.c b/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;
+}
diff --git a/regression/contracts/history-pointer-enforce-04/test.desc b/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.
diff --git a/regression/contracts/history-pointer-enforce-05/main.c b/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;
+}
diff --git a/regression/contracts/history-pointer-enforce-05/test.desc b/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.
diff --git a/regression/contracts/history-pointer-enforce-06/main.c b/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;
+}
diff --git a/regression/contracts/history-pointer-enforce-06/test.desc b/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.
diff --git a/regression/contracts/history-pointer-enforce-07/main.c b/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;
+}
diff --git a/regression/contracts/history-pointer-enforce-07/test.desc b/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.
diff --git a/regression/contracts/history-pointer-enforce-08/main.c b/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;
+}
diff --git a/regression/contracts/history-pointer-enforce-08/test.desc b/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.
diff --git a/regression/contracts/history-pointer-replace-01/main.c b/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;
+}
diff --git a/regression/contracts/history-pointer-replace-01/test.desc b/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.
diff --git a/regression/contracts/history-pointer-replace-02/main.c b/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;
+}
diff --git a/regression/contracts/history-pointer-replace-02/test.desc b/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.
diff --git a/regression/contracts/history-pointer-replace-03/main.c b/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;
+}
diff --git a/regression/contracts/history-pointer-replace-03/test.desc b/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.
diff --git a/src/ansi-c/c_expr.h b/src/ansi-c/c_expr.h
diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp
diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h
diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h
diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp
diff --git a/src/goto-instrument/code_contracts.h b/src/goto-instrument/code_contracts.h
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
