function contracts: allow history variables for typecast and constant expressions.

Author: Remi Delmas

regression/contracts/assigns-replace-ignored-return-value/main.c

@@ -0,0 +1,37 @@
+#include <stdbool.h>
+#include <stdlib.h>
+
+int bar(int l, int r) __CPROVER_requires(0 <= l && l <= 10)
+  __CPROVER_requires(0 <= r && r <= 10) __CPROVER_assigns() __CPROVER_ensures(
+    __CPROVER_return_value == __CPROVER_old(l) + __CPROVER_old(r))
+{
+  return l + r;
+}
+
+int *baz(int l, int r) __CPROVER_requires(0 <= l && l <= 10)
+  __CPROVER_requires(0 <= r && r <= 10) __CPROVER_assigns() __CPROVER_ensures(
+    *__CPROVER_return_value == __CPROVER_old(l) + __CPROVER_old(r))
+{
+  int *res = malloc(sizeof(int));
+  *res = l + r;
+  return res;
+}
+
+int foo(int l, int r) __CPROVER_requires(0 <= l && l <= 10)
+  __CPROVER_requires(0 <= r && r <= 10) __CPROVER_assigns() __CPROVER_ensures(
+    __CPROVER_return_value == __CPROVER_old(l) + __CPROVER_old(r))
+{
+  bar(l, r);
+  bar(l, r);
+  baz(l, r);
+  baz(l, r);
+  return l + r;
+}
+
+int main()
+{
+  int l;
+  int r;
+  foo(l, r);
+  return 0;
+}

regression/contracts/assigns-replace-ignored-return-value/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--replace-call-with-contract bar --replace-call-with-contract baz --enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^[.*] Check that .*ignored_return_value.* is assignable: FAILURE
+--
+This test checks that when replacing a call by a contract for a call that
+ignores the return value of the function, the temporary introduced to 
+receive the call result does not trigger errors with assigns clause Checking
+in the function under verification.

regression/contracts/assigns_enforce_21/test.desc

@@ -4,8 +4,8 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 main.c function bar
-^\[bar.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
-^\[bar.\d+\] line \d+ Check that x is assignable: FAILURE$
+^\[bar\.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
+^\[bar\.\d+\] line \d+ Check that x \(assigned by the contract of quz\) is assignable: FAILURE
 ^VERIFICATION FAILED$
 --
 --

regression/contracts/assigns_replace_08/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo --replace-call-with-contract bar _ --pointer-primitive-check
 ^EXIT=10$
 ^SIGNAL=0$
-\[foo.\d+\] line \d+ Check that \*z is assignable: FAILURE$
+\[foo.\d+\] line \d+ Check that \*z \(assigned by the contract of bar\) is assignable: FAILURE$
 ^.* 1 of \d+ failed \(\d+ iteration.*\)$
 ^VERIFICATION FAILED$
 --

regression/contracts/assigns_replace_09/test.desc

@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract bar --enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
-\[foo.\d+\] line \d+ Check that \*z is assignable: SUCCESS$
+\[foo.\d+\] line \d+ Check that \*z \(assigned by the contract of bar\) is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^Condition: \!not\_found$

regression/contracts/assigns_replace_havoc_dependent_targets_fail/enforce.desc

@@ -0,0 +1,9 @@
+CORE
+main_enforce.c
+--enforce-contract resize_vec _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Verifies the contract being replaced in `replace.desc`.

regression/contracts/assigns_replace_havoc_dependent_targets_fail/main_enforce.c

@@ -0,0 +1,9 @@
+#include "vect.h"
+
+int main()
+{
+  vect *v;
+  size_t incr;
+  resize_vec(v, incr);
+  return 0;
+}

regression/contracts/assigns_replace_havoc_dependent_targets_fail/main_replace.c

@@ -0,0 +1,8 @@
+#include "vect.h"
+
+int main()
+{
+  vect *v;
+  resize_vec_incr10(v);
+  return 0;
+}

regression/contracts/assigns_replace_havoc_dependent_targets_fail/replace.desc

@@ -0,0 +1,16 @@
+CORE
+main_replace.c
+--replace-call-with-contract resize_vec --enforce-contract resize_vec_incr10 _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check
+^\[.*\] .* Check that v->size \(assigned by the contract of resize_vec\) is assignable: SUCCESS
+^\[.*\] .* Check that v->arr \(assigned by the contract of resize_vec\) is assignable: FAILURE
+^\[.*\] .* Check that POINTER_OBJECT\(\(const void \*\)v->arr\) \(assigned by the contract of resize_vec\) is assignable: FAILURE
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Shows that when an assigns clause contains targets that are dependent, 
+in this case, a pointer variable `v->arr` and
+the object it points to `__CPROVER_POINTER_OBJECT(v->arr)`, we can correctly
+havoc them when replacing the call by the contract.
+In this version of the test the inclusion check must fail.

regression/contracts/assigns_replace_havoc_dependent_targets_fail/vect.h

@@ -0,0 +1,48 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct vect
+{
+  char *arr;
+  size_t size;
+} vect;
+
+void resize_vec(vect *v, size_t incr)
+  // clang-format off
+__CPROVER_requires(
+  __CPROVER_is_fresh(v, sizeof(vect)) &&
+  0 < v->size && v->size <= __CPROVER_max_malloc_size &&
+  0 < incr && incr < __CPROVER_max_malloc_size - v->size &&
+  __CPROVER_is_fresh(v->arr, v->size)
+)
+__CPROVER_assigns(v->size, v->arr, __CPROVER_POINTER_OBJECT(v->arr))
+__CPROVER_ensures(
+  v->size == __CPROVER_old(v->size) + __CPROVER_old(incr) &&
+  __CPROVER_is_fresh(v->arr, v->size)
+)
+// clang-format on
+{
+  free(v->arr);
+  v->size += incr;
+  v->arr = malloc(v->size);
+  return;
+}
+
+void resize_vec_incr10(vect *v)
+  // clang-format off
+__CPROVER_requires(
+  __CPROVER_is_fresh(v, sizeof(vect)) &&
+  0 < v->size && v->size <= __CPROVER_max_malloc_size &&
+  v->size + 10 < __CPROVER_max_malloc_size &&
+  __CPROVER_is_fresh(v->arr, v->size)
+)
+__CPROVER_assigns(v->size)
+__CPROVER_ensures(
+  v->size == __CPROVER_old(v->size) + 10 &&
+  __CPROVER_is_fresh(v->arr, v->size)
+)
+// clang-format on
+{
+  resize_vec(v, 10);
+  return;
+}

regression/contracts/assigns_replace_havoc_dependent_targets_pass/enforce.desc

@@ -0,0 +1,9 @@
+CORE
+main_enforce.c
+--enforce-contract resize_vec _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Verifies the contract being replaced in `replace.desc`.

regression/contracts/assigns_replace_havoc_dependent_targets_pass/main_enforce.c

@@ -0,0 +1,9 @@
+#include "vect.h"
+
+int main()
+{
+  vect *v;
+  size_t incr;
+  resize_vec(v, incr);
+  return 0;
+}

regression/contracts/assigns_replace_havoc_dependent_targets_pass/main_replace.c

@@ -0,0 +1,8 @@
+#include "vect.h"
+
+int main()
+{
+  vect *v;
+  resize_vec_incr10(v);
+  return 0;
+}

regression/contracts/assigns_replace_havoc_dependent_targets_pass/replace.desc

@@ -0,0 +1,16 @@
+CORE
+main_replace.c
+--replace-call-with-contract resize_vec --enforce-contract resize_vec_incr10 _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check
+^VERIFICATION SUCCESSFUL$
+^\[.*\] .* Check that v->size \(assigned by the contract of resize_vec\) is assignable: SUCCESS
+^\[.*\] .* Check that v->arr \(assigned by the contract of resize_vec\) is assignable: SUCCESS
+^\[.*\] .* Check that POINTER_OBJECT\(\(const void \*\)v->arr\) \(assigned by the contract of resize_vec\) is assignable: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Shows that when an assigns clause contains targets that are dependent, 
+in this case, a pointer variable `v->arr` and
+the object it points to `__CPROVER_POINTER_OBJECT(v->arr)`, we can correctly
+havoc them when replacing the call by the contract.
+In this version of the test the inclusion check must pass.

regression/contracts/assigns_replace_havoc_dependent_targets_pass/vect.h

@@ -0,0 +1,48 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct vect
+{
+  char *arr;
+  size_t size;
+} vect;
+
+void resize_vec(vect *v, size_t incr)
+  // clang-format off
+__CPROVER_requires(
+  __CPROVER_is_fresh(v, sizeof(vect)) &&
+  0 < v->size && v->size <= __CPROVER_max_malloc_size &&
+  0 < incr && incr < __CPROVER_max_malloc_size - v->size &&
+  __CPROVER_is_fresh(v->arr, v->size)
+)
+__CPROVER_assigns(v->size, v->arr, __CPROVER_POINTER_OBJECT(v->arr))
+__CPROVER_ensures(
+  v->size == __CPROVER_old(v->size) + __CPROVER_old(incr) &&
+  __CPROVER_is_fresh(v->arr, v->size)
+)
+// clang-format on
+{
+  free(v->arr);
+  v->size += incr;
+  v->arr = malloc(v->size);
+  return;
+}
+
+void resize_vec_incr10(vect *v)
+  // clang-format off
+__CPROVER_requires(
+  __CPROVER_is_fresh(v, sizeof(vect)) &&
+  0 < v->size && v->size <= __CPROVER_max_malloc_size &&
+  v->size + 10 < __CPROVER_max_malloc_size &&
+  __CPROVER_is_fresh(v->arr, v->size)
+)
+__CPROVER_assigns(*v, __CPROVER_POINTER_OBJECT(v->arr))
+__CPROVER_ensures(
+  v->size == __CPROVER_old(v->size) + 10 &&
+  __CPROVER_is_fresh(v->arr, v->size)
+)
+// clang-format on
+{
+  resize_vec(v, 10);
+  return;
+}

regression/contracts/history-constant/main.c

@@ -0,0 +1,15 @@
+#include <stdio.h>
+
+int foo(int l) __CPROVER_requires(-10 <= l && l <= 10) __CPROVER_ensures(
+  __CPROVER_return_value == __CPROVER_old(l) + __CPROVER_old(10))
+{
+  return l + 10;
+}
+
+int main()
+{
+  int l;
+  __CPROVER_assume(-10 <= l && l <= 10);
+  foo(l);
+  return 0;
+}

regression/contracts/history-constant/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^Tracking history of constant expressions is not supported yet
+--
+This test checks that history variables are supported for constant expressions.

regression/contracts/history-typecast/main.c

@@ -0,0 +1,23 @@
+#include <stdio.h>
+
+long bar(long l, long r) __CPROVER_requires(-10 <= l && l <= 10)
+  __CPROVER_requires(-10 <= r && r <= 10) __CPROVER_ensures(
+    __CPROVER_return_value == __CPROVER_old(l) + __CPROVER_old(r))
+{
+  return l + r;
+}
+
+int foo(int l, int r) __CPROVER_requires(-10 <= l && l <= 10)
+  __CPROVER_requires(-10 <= r && r <= 10) __CPROVER_ensures(
+    __CPROVER_return_value == __CPROVER_old(l) + __CPROVER_old(r))
+{
+  return bar((long)l, (long)r);
+}
+
+int main()
+{
+  int n;
+  __CPROVER_assume(-10 <= n && n <= 10);
+  foo(n, n);
+  return 0;
+}

regression/contracts/history-typecast/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--replace-call-with-contract bar --enforce-contract foo 
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^Tracking history of typecast expressions is not supported yet
+--
+This test checks that history variables are supported for typecast expressions.

src/goto-instrument/Makefile

@@ -18,6 +18,7 @@ SRC = accelerate/accelerate.cpp \
       call_sequences.cpp \
       contracts/assigns.cpp \
       contracts/contracts.cpp \
+      contracts/havoc_assigns_clause_targets.cpp \
       contracts/memory_predicates.cpp \
       contracts/utils.cpp \
       concurrency.cpp \