diff --git a/regression/contracts/is_unique_01_replace/main.c b/regression/contracts/is_unique_01_replace/main.c new file mode 100644 index 00000000000..b81f917e90c --- /dev/null +++ b/regression/contracts/is_unique_01_replace/main.c @@ -0,0 +1,84 @@ +#include +#include +#include +#include +#include + +bool dummy_for_definitions(int *n) +{ + assert(__CPROVER_is_fresh(&n, sizeof(int))); + int *x = malloc(sizeof(int)); +} + +bool ptr_ok(int *x) +{ + return *x < 5; +} + +/* + Here are the meanings of the predicates: + +static _Bool __foo_memory_map[__CPROVER_constant_infinity_uint]; + +bool __foo_requires_is_fresh(void **elem, size_t size) { + *elem = malloc(size); + if (!*elem || (__foo_memory_map[__CPROVER_POINTER_OBJECT(*elem)] != 0)) return false; + + __foo_memory_map[__CPROVER_POINTER_OBJECT(*elem)] = 1; + return true; +} + +bool __foo_ensures_is_fresh(void *elem, size_t size) { + bool ok = (__foo_memory_map[__CPROVER_POINTER_OBJECT(elem)] == 0 && + __CPROVER_r_ok(elem, size)); + __foo_memory_map[__CPROVER_POINTER_OBJECT(elem)] = 1; + return ok; +} + + +_Bool __call_foo_requires_is_fresh(void *elem, size_t size) { + _Bool r_ok = __CPROVER_r_ok(elem, size); + if (!__CPROVER_r_ok(elem, size) || + __foo_memory_map[__CPROVER_POINTER_OBJECT(elem)]) return 0; + __foo_memory_map[__CPROVER_POINTER_OBJECT(elem)] = 1; + return 1; +} + +// In the calling context, we assume freshness means new +// allocation from within the function. +bool __call_foo_ensures_is_fresh(void **elem, size_t size) { + *elem = malloc(size); + return (*elem != NULL); +} +*/ + +bool return_ok(int ret_value, int *x) +{ + int a; + a = *x; + return ret_value == *x + 5; +} + +// The 'ensures' __CPROVER_is_fresh test is unnecessary, but left in just to test the function is working correctly. +// If you remove the negation, the program will fail, because 'x' is not fresh. + +int foo(int *x, int y) __CPROVER_assigns(*x) + __CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)) && *x > 0 && ptr_ok(x)) + __CPROVER_ensures( + !ptr_ok(x) && !__CPROVER_is_fresh(x, sizeof(int)) && + return_ok(__CPROVER_return_value, x)) +{ + *x = *x + 4; + int y = *x + 5; + return *x + 5; +} + +int main() +{ + int *n = malloc(sizeof(int)); + assert(__CPROVER_r_ok(n, sizeof(int))); + *n = 3; + int o = foo(n, 10); + assert(o >= 10 && o == *n + 5); + return 0; +} diff --git a/regression/contracts/is_unique_01_replace/test.desc b/regression/contracts/is_unique_01_replace/test.desc new file mode 100644 index 00000000000..40382c3c652 --- /dev/null +++ b/regression/contracts/is_unique_01_replace/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--replace-all-calls-with-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that verification succeeds if only expressions inside the assigns clause are assigned within the function. + +Note: For all 'enforce' tests, nothing can be assumed about the return value of the function (as the function call is not replaced at this point). + +To make such assumptions would cause verification to fail. diff --git a/regression/contracts/quantifiers-loop-02/test.desc b/regression/contracts/quantifiers-loop-02/test.desc index d5367bac034..1e28824258d 100644 --- a/regression/contracts/quantifiers-loop-02/test.desc +++ b/regression/contracts/quantifiers-loop-02/test.desc @@ -3,9 +3,9 @@ main.c --enforce-all-contracts _ --z3 ^EXIT=0$ ^SIGNAL=0$ -^\[main.1\] line .* Check loop invariant before entry: SUCCESS -^\[main.2\] line .* Check that loop invariant is preserved: SUCCESS -^\[main.assertion.1\] line .* assertion .*: SUCCESS +^\[main.\d+\] line .* Check loop invariant before entry: SUCCESS +^\[main.\d+\] line .* Check that loop invariant is preserved: SUCCESS +^\[main.assertion.\d+\] line .* assertion .*: SUCCESS ^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring diff --git a/regression/contracts/test_aliasing_enforce/main.c b/regression/contracts/test_aliasing_enforce/main.c new file mode 100644 index 00000000000..e79ef71fce3 --- /dev/null +++ b/regression/contracts/test_aliasing_enforce/main.c @@ -0,0 +1,34 @@ +#include +#include +#include + +int z; + +// clang-format off +int foo(int *x, int *y) + __CPROVER_assigns(z, *x, *y) + __CPROVER_requires( + __CPROVER_is_fresh(x, sizeof(int)) && + __CPROVER_is_fresh(y, sizeof(int)) && + *x > 0 && + *x < 4) + __CPROVER_ensures( + x != NULL && + y != NULL && + x != y && + __CPROVER_return_value == *x + 5) +// clang-format on +{ + *x = *x + 4; + *y = *x; + z = *y; + return (*x + 5); +} + +int main() +{ + int n = 4; + n = foo(&n, &n); + assert(!(n < 4)); + return 0; +} diff --git a/regression/contracts/test_aliasing_enforce/test.desc b/regression/contracts/test_aliasing_enforce/test.desc new file mode 100644 index 00000000000..e5f49a3ee51 --- /dev/null +++ b/regression/contracts/test_aliasing_enforce/test.desc @@ -0,0 +1,15 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS +\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS +\[foo.\d+\] line \d+ Check that \*y is assignable: SUCCESS +\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS +\[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks whether assuming __CPROVER_is_fresh will guarantee a new freshly +allocated pointer (no aliasing) for structs. diff --git a/regression/contracts/test_aliasing_ensure/main.c b/regression/contracts/test_aliasing_ensure/main.c new file mode 100644 index 00000000000..3c4f94e863d --- /dev/null +++ b/regression/contracts/test_aliasing_ensure/main.c @@ -0,0 +1,35 @@ +#include +#include +#include + +int z; + +// clang-format off +int foo(int *x, int *y) + __CPROVER_assigns(z, *x, y) + __CPROVER_requires( + __CPROVER_is_fresh(x, sizeof(int)) && + *x > 0 && + *x < 4) + __CPROVER_ensures( + x != NULL && + !__CPROVER_is_fresh(x, sizeof(int)) && + __CPROVER_is_fresh(y, sizeof(int)) && + x != y && + __CPROVER_return_value == *x + 5) +// clang-format on +{ + *x = *x + 4; + y = malloc(sizeof(*y)); + *y = *x; + z = *y; + return (*x + 5); +} + +int main() +{ + int n = 4; + n = foo(&n, &n); + assert(!(n < 4)); + return 0; +} diff --git a/regression/contracts/test_aliasing_ensure/test.desc b/regression/contracts/test_aliasing_ensure/test.desc new file mode 100644 index 00000000000..8355f437a08 --- /dev/null +++ b/regression/contracts/test_aliasing_ensure/test.desc @@ -0,0 +1,15 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS +\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS +\[foo.\d+\] line \d+ Check that \*y is assignable: SUCCESS +\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS +\[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks whether ensures(is_fresh()) pass on functions that perform allocation +directly and return a new object. diff --git a/regression/contracts/test_aliasing_ensure_indirect/main.c b/regression/contracts/test_aliasing_ensure_indirect/main.c new file mode 100644 index 00000000000..bac705ee9e3 --- /dev/null +++ b/regression/contracts/test_aliasing_ensure_indirect/main.c @@ -0,0 +1,38 @@ +#include +#include +#include + +void bar(int *z) __CPROVER_assigns(z) + __CPROVER_ensures(__CPROVER_is_fresh(z, sizeof(int))) +{ + z = malloc(sizeof(*z)); + z = 10; +} + +// clang-format off +int foo(int *x, int *y) + __CPROVER_assigns(*x, y) + __CPROVER_requires( + __CPROVER_is_fresh(x, sizeof(int)) && + *x > 0 && + *x < 4) + __CPROVER_ensures( + x != NULL && + !__CPROVER_is_fresh(x, sizeof(int)) && + __CPROVER_is_fresh(y, sizeof(int)) && + x != y && + __CPROVER_return_value == *x + 5) +// clang-format on +{ + *x = *x + 4; + bar(y); + return (*x + 5); +} + +int main() +{ + int n = 4; + n = foo(&n, &n); + assert(!(n < 4)); + return 0; +} diff --git a/regression/contracts/test_aliasing_ensure_indirect/test.desc b/regression/contracts/test_aliasing_ensure_indirect/test.desc new file mode 100644 index 00000000000..67f44e427c6 --- /dev/null +++ b/regression/contracts/test_aliasing_ensure_indirect/test.desc @@ -0,0 +1,15 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS +\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS +\[bar.\d+\] line \d+ Check that z is assignable: SUCCESS +\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS +\[foo.\d+\] line \d+ Check compatibility of assigns clause with the called function: SUCCESS +\[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks whether CBMC propagates freshness correctly across contracts. diff --git a/regression/contracts/test_aliasing_replace/main.c b/regression/contracts/test_aliasing_replace/main.c new file mode 100644 index 00000000000..f77721d1a2a --- /dev/null +++ b/regression/contracts/test_aliasing_replace/main.c @@ -0,0 +1,32 @@ +#include +#include +#include + +int z; + +// clang-format off +int foo(int *x, int *y) + __CPROVER_assigns(z, *x, *y) + __CPROVER_requires( + __CPROVER_is_fresh(x, sizeof(int)) && + __CPROVER_is_fresh(y, sizeof(int)) && + *x > 0 + && *x <= 4) + __CPROVER_ensures( + x != NULL && + y != NULL && + x != y && + __CPROVER_return_value == *x + 5) +// clang-format on +{ + *x = *x + 4; + return (*x + 5); +} + +int main() +{ + int n = 4; + n = foo(&n, &n); + assert(!(n < 4)); + return 0; +} diff --git a/regression/contracts/test_aliasing_replace/test.desc b/regression/contracts/test_aliasing_replace/test.desc new file mode 100644 index 00000000000..9c9a3c85936 --- /dev/null +++ b/regression/contracts/test_aliasing_replace/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--replace-all-calls-with-contracts +^EXIT=10$ +^SIGNAL=0$ +\[precondition.\d+\] file main.c line \d+ Check requires clause: FAILURE +\[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS +^VERIFICATION FAILED$ +-- +-- +Checks whether asserting __CPROVER_is_fresh will guarantee that objects +mapped to distinct objetcs. diff --git a/regression/contracts/test_array_memory_enforce/main.c b/regression/contracts/test_array_memory_enforce/main.c new file mode 100644 index 00000000000..0abfeefd0a3 --- /dev/null +++ b/regression/contracts/test_array_memory_enforce/main.c @@ -0,0 +1,41 @@ +#include + +bool ptr_ok(int *x) +{ + return (*x < 5); +} + +bool return_ok(int ret_value, int *x) +{ + int a; + a = *x; + return (ret_value == *x + 5); +} + +// clang-format off +int foo(int *x) + __CPROVER_assigns(*x) + __CPROVER_requires( + __CPROVER_is_fresh(x, sizeof(int) * 10) && + x[0] > 0 && + ptr_ok(x)) + __CPROVER_ensures( + !ptr_ok(x) && + !__CPROVER_is_fresh(x, sizeof(int) * 10) && /* `x` is not fresh anymore. */ + x[9] == 113 && + return_ok(__CPROVER_return_value, x)) +// clang-format on +{ + *x = *x + 4; + x[5] = 12; + x[9] = 113; + int y = *x + 5; + return *x + 5; +} + +int main() +{ + int *n; + int o = foo(n); + return 0; +} diff --git a/regression/contracts/test_array_memory_enforce/test.desc b/regression/contracts/test_array_memory_enforce/test.desc new file mode 100644 index 00000000000..64dc6849502 --- /dev/null +++ b/regression/contracts/test_array_memory_enforce/test.desc @@ -0,0 +1,17 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS +\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS +\[foo.\d+\] line \d+ Check that x\[\(.* int\)5\] is assignable: SUCCESS +\[foo.\d+\] line \d+ Check that x\[\(.* int\)9\] is assignable: SUCCESS +\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks whether __CPROVER_is_fresh behaves correctly for arrays both in +requires and ensures clauses. In the ensures clause, the __CPROVER_is_fresh +is unnecessary. By negating the predicate in the ensures clause, the test +proves that `x` is not fresh at end of the function. diff --git a/regression/contracts/test_array_memory_replace/main.c b/regression/contracts/test_array_memory_replace/main.c new file mode 100644 index 00000000000..76a7d7063ca --- /dev/null +++ b/regression/contracts/test_array_memory_replace/main.c @@ -0,0 +1,46 @@ +#include +#include +#include + +bool ptr_ok(int *x) +{ + return (*x < 5); +} + +bool return_ok(int ret_value, int *x) +{ + int a; + a = *x; + return (ret_value == (*x + 5)); +} + +// clang-format off +int foo(int *x) + __CPROVER_assigns(*x) + __CPROVER_requires( + __CPROVER_is_fresh(x, sizeof(int) * 10) && + x[0] > 0 && + ptr_ok(x)) + __CPROVER_ensures( + !ptr_ok(x) && + !__CPROVER_is_fresh(x, sizeof(int) * 10) && + x[9] == 113 && + return_ok(__CPROVER_return_value, x)) +// clang-format on +{ + *x = *x + 4; + x[5] = 12; + x[9] = 113; + int y = *x + 5; + return *x + 5; +} + +int main() +{ + int *n = malloc(sizeof(int) * 10); + n[0] = 3; + int o = foo(n); + assert(o >= 10 && o == *n + 5); + assert(n[9] == 113); + return 0; +} diff --git a/regression/contracts/test_array_memory_replace/test.desc b/regression/contracts/test_array_memory_replace/test.desc new file mode 100644 index 00000000000..5c5b0494a33 --- /dev/null +++ b/regression/contracts/test_array_memory_replace/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--replace-all-calls-with-contracts +^EXIT=0$ +^SIGNAL=0$ +\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS +\[main.assertion.\d+\] line \d+ assertion o \>\= 10 \&\& o \=\= \*n \+ 5: SUCCESS +\[main.assertion.\d+\] line \d+ assertion n\[9\] == 113: SUCCESS +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks whether CBMC successfuly assert __CPROVER_is_fresh for arrays. diff --git a/regression/contracts/test_array_memory_too_small_replace/main.c b/regression/contracts/test_array_memory_too_small_replace/main.c new file mode 100644 index 00000000000..4c8cd24452e --- /dev/null +++ b/regression/contracts/test_array_memory_too_small_replace/main.c @@ -0,0 +1,45 @@ +#include +#include +#include + +bool ptr_ok(int *x) +{ + return (*x < 5); +} + +bool return_ok(int ret_value, int *x) +{ + int a; + a = *x; + return (ret_value == (*x + 5)); +} + +// clang-format off +int foo(int *x) + __CPROVER_assigns(*x) + __CPROVER_requires( + __CPROVER_is_fresh(x, sizeof(int) * 10) && + x[0] > 0 && + ptr_ok(x)) + __CPROVER_ensures( + !ptr_ok(x) && + !__CPROVER_is_fresh(x, sizeof(int) * 10) && + x[9] == 113 && + return_ok(__CPROVER_return_value, x)) +// clang-format on +{ + *x = *x + 4; + x[5] = 12; + x[9] = 113; + int y = *x + 5; + return (*x + 5); +} + +int main() +{ + int *n = malloc(sizeof(int) * 9); + n[0] = 3; + int o = foo(n); + assert(o >= 10 && o == *n + 5); + return 0; +} diff --git a/regression/contracts/test_array_memory_too_small_replace/test.desc b/regression/contracts/test_array_memory_too_small_replace/test.desc new file mode 100644 index 00000000000..9d20386dcca --- /dev/null +++ b/regression/contracts/test_array_memory_too_small_replace/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--replace-all-calls-with-contracts +^EXIT=10$ +^SIGNAL=0$ +\[precondition.\d+\] file main.c line \d+ Check requires clause: FAILURE +\[main.assertion.\d+\] line \d+ assertion o \>\= 10 \&\& o \=\= \*n \+ 5: SUCCESS +^VERIFICATION FAILED$ +-- +-- +Checks whether CBMC successfuly assert __CPROVER_is_fresh for arrays. +Test fails because allocated array was smaller then the one required +in the contract. diff --git a/regression/contracts/test_possibly_aliased_arguments/main.c b/regression/contracts/test_possibly_aliased_arguments/main.c new file mode 100644 index 00000000000..6f168a148d9 --- /dev/null +++ b/regression/contracts/test_possibly_aliased_arguments/main.c @@ -0,0 +1,26 @@ +#include +#include +#include + +// When enforced, this contract should pass + +// clang-format off +bool sub_ptr_values(int *x, int *y) + __CPROVER_requires( + __CPROVER_is_fresh(x, sizeof(int)) && + (y == x || __CPROVER_is_fresh(y, sizeof(int))) + ) + __CPROVER_ensures( + __CPROVER_return_value == (*x - *y) + ) +// clang-format on +{ + return (*x - *y); +} + +// A function that uses `sub_ptr_values` +void main() +{ + int *n = malloc(sizeof(int)); + int diff = sub_ptr_values(n, n); +} diff --git a/regression/contracts/test_possibly_aliased_arguments/test.desc b/regression/contracts/test_possibly_aliased_arguments/test.desc new file mode 100644 index 00000000000..ade5330c5cf --- /dev/null +++ b/regression/contracts/test_possibly_aliased_arguments/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--replace-all-calls-with-contracts +^EXIT=0$ +^SIGNAL=0$ +\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks whether __CPROVER_is_fresh can be used conditionally, +in order to allow possibly-aliased arguments. diff --git a/regression/contracts/test_scalar_memory_enforce/main.c b/regression/contracts/test_scalar_memory_enforce/main.c new file mode 100644 index 00000000000..b22c93fe00f --- /dev/null +++ b/regression/contracts/test_scalar_memory_enforce/main.c @@ -0,0 +1,37 @@ +#include +#include + +bool ptr_ok(int *x) +{ + return (*x < 5); +} + +bool return_ok(int ret_value, int *x) +{ + int a = *x; + return (ret_value == (*x + 5)); +} + +// clang-format off +int foo(int *x) + __CPROVER_assigns(*x) + __CPROVER_requires( + __CPROVER_is_fresh(x, sizeof(int)) && + *x > 0 && + ptr_ok(x)) + __CPROVER_ensures( + !ptr_ok(x) && + !__CPROVER_is_fresh(x, sizeof(int)) && + return_ok(__CPROVER_return_value, x)) +// clang-format on +{ + *x = *x + 4; + return (*x + 5); +} + +int main() +{ + int *n; + int o = foo(n); + return 0; +} diff --git a/regression/contracts/test_scalar_memory_enforce/test.desc b/regression/contracts/test_scalar_memory_enforce/test.desc new file mode 100644 index 00000000000..2e29a7d7c5a --- /dev/null +++ b/regression/contracts/test_scalar_memory_enforce/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS +\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks whether __CPROVER_is_fresh works properly for scalars (enforce context). +It tests both positive and negative cases for __CPROVER_is_fresh. diff --git a/regression/contracts/test_scalar_memory_replace/main.c b/regression/contracts/test_scalar_memory_replace/main.c new file mode 100644 index 00000000000..888731fb375 --- /dev/null +++ b/regression/contracts/test_scalar_memory_replace/main.c @@ -0,0 +1,41 @@ +#include +#include +#include + +bool ptr_ok(int *x) +{ + return (*x < 5); +} + +bool return_ok(int ret_value, int *x) +{ + int a = *x; + return (ret_value == (*x + 5)); +} + +// clang-format off +int foo(int *x) + __CPROVER_assigns(*x) + __CPROVER_requires( + __CPROVER_is_fresh(x, sizeof(int)) && + *x > 0 && + ptr_ok(x)) + __CPROVER_ensures( + !ptr_ok(x) && + !__CPROVER_is_fresh(x, sizeof(int)) && + return_ok(__CPROVER_return_value, x)) +// clang-format on +{ + *x = *x + 4; + return (*x + 5); +} + +int main() +{ + int *n = malloc(sizeof(int)); + assert(__CPROVER_r_ok(n, sizeof(int))); + *n = 3; + int o = foo(n); + assert(o >= 10 && o == *n + 5); + return 0; +} diff --git a/regression/contracts/test_scalar_memory_replace/test.desc b/regression/contracts/test_scalar_memory_replace/test.desc new file mode 100644 index 00000000000..5a00ec342ff --- /dev/null +++ b/regression/contracts/test_scalar_memory_replace/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--replace-all-calls-with-contracts +^EXIT=0$ +^SIGNAL=0$ +\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS +\[main.assertion.\d+\] line \d+ assertion \_\_CPROVER\_r\_ok\(n, sizeof\(int\)\): SUCCESS +\[main.assertion.\d+\] line \d+ assertion o \>\= 10 \&\& o \=\= \*n \+ 5: SUCCESS +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks whether __CPROVER_is_fresh works properly for scalars (replace context). +It tests both positive and negative cases for __CPROVER_is_fresh. diff --git a/regression/contracts/test_struct_enforce/main.c b/regression/contracts/test_struct_enforce/main.c new file mode 100644 index 00000000000..7ea407d7af0 --- /dev/null +++ b/regression/contracts/test_struct_enforce/main.c @@ -0,0 +1,30 @@ +#include +#include + +struct bar +{ + int baz; + unsigned int qux; +}; + +// clang-format off +int foo(struct bar *x) + __CPROVER_assigns(*x) + __CPROVER_requires( + __CPROVER_is_fresh(x, sizeof(struct bar))) + __CPROVER_ensures( + __CPROVER_return_value == (x->baz + x->qux)) +// clang-format on +{ + x->baz = 5; + x->qux = 5; + return (x->baz + x->qux); +} + +int main() +{ + struct bar *x; + int rval = foo(x); + assert(rval == 10); + return 0; +} diff --git a/regression/contracts/test_struct_enforce/test.desc b/regression/contracts/test_struct_enforce/test.desc new file mode 100644 index 00000000000..077284e4885 --- /dev/null +++ b/regression/contracts/test_struct_enforce/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS +\[foo.\d+\] line \d+ Check that x-\>baz is assignable: SUCCESS +\[foo.\d+\] line \d+ Check that x-\>qux is assignable: SUCCESS +\[main.assertion.\d+\] line \d+ assertion rval \=\= 10: SUCCESS +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks whether assuming __CPROVER_is_fresh will guarantee a new freshly +allocated pointer (no aliasing) for structs. diff --git a/regression/contracts/test_struct_member_enforce/main.c b/regression/contracts/test_struct_member_enforce/main.c new file mode 100644 index 00000000000..54bf409fdfa --- /dev/null +++ b/regression/contracts/test_struct_member_enforce/main.c @@ -0,0 +1,30 @@ +#include + +struct string +{ + int len; + char *str; +}; + +// clang-format off +int foo(struct string *x) + __CPROVER_assigns(*(x->str)) + __CPROVER_requires( + x->len == 128 && + __CPROVER_is_fresh(x->str, x->len * sizeof(char))) + __CPROVER_ensures( + __CPROVER_return_value == 128 && + x->str[x->len - 1] == '\0') +// clang-format on +{ + x->str[x->len - 1] = '\0'; + return x->len; +} + +int main() +{ + struct string x; + int rval = foo(&x); + assert(rval == 128); + return 0; +} diff --git a/regression/contracts/test_struct_member_enforce/test.desc b/regression/contracts/test_struct_member_enforce/test.desc new file mode 100644 index 00000000000..439136d614d --- /dev/null +++ b/regression/contracts/test_struct_member_enforce/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS +\[foo.\d+\] line \d+ Check that x-\>str\[\(.*\)\(x-\>len - 1\)\] is assignable: SUCCESS +\[main.assertion.\d+\] line \d+ assertion rval \=\= 128: SUCCESS +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks whether assuming __CPROVER_is_fresh will guarantee a new freshly +allocated pointer (no aliasing) for struct members. diff --git a/regression/contracts/test_struct_replace/main.c b/regression/contracts/test_struct_replace/main.c new file mode 100644 index 00000000000..b5e1a50df1a --- /dev/null +++ b/regression/contracts/test_struct_replace/main.c @@ -0,0 +1,35 @@ +#include +#include + +struct bar +{ + int baz; + unsigned int qux; +}; + +// clang-format off +int foo(struct bar *x, struct bar *y) + __CPROVER_assigns(*x, *y) + __CPROVER_requires( + __CPROVER_is_fresh(x, sizeof(struct bar)) && + __CPROVER_is_fresh(y, sizeof(struct bar))) + __CPROVER_ensures( + __CPROVER_return_value == (x->baz + x->qux) && + *x == *y) +// clang-format on +{ + x->baz = 5; + x->qux = 5; + *y = *x; + return (x->baz + x->qux); +} + +int main() +{ + struct bar *x = malloc(sizeof(*x)); + struct bar *y = malloc(sizeof(*y)); + int rval = foo(x, y); + assert(rval == x->baz + x->qux); + assert(*x == *y); + return 0; +} diff --git a/regression/contracts/test_struct_replace/test.desc b/regression/contracts/test_struct_replace/test.desc new file mode 100644 index 00000000000..ee71de5385d --- /dev/null +++ b/regression/contracts/test_struct_replace/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--replace-all-calls-with-contracts +^EXIT=0$ +^SIGNAL=0$ +\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS +\[main.assertion.\d+\] line \d+ assertion rval \=\= x-\>baz \+ x-\>qux: SUCCESS +\[main.assertion.\d+\] line \d+ assertion \*x \=\= \*y: SUCCESS +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks whether asserting __CPROVER_is_fresh will guarantee that objects +mapped to distinct objetcs (for structs). diff --git a/scripts/expected_doxygen_warnings.txt b/scripts/expected_doxygen_warnings.txt index cb512d21ff6..cb643b52373 100644 --- a/scripts/expected_doxygen_warnings.txt +++ b/scripts/expected_doxygen_warnings.txt @@ -2,13 +2,13 @@ warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, to warning: Included by graph for 'goto_model.h' not generated, too many nodes (95), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'arith_tools.h' not generated, too many nodes (167), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'c_types.h' not generated, too many nodes (128), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. -warning: Included by graph for 'config.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. +warning: Included by graph for 'config.h' not generated, too many nodes (79), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'invariant.h' not generated, too many nodes (172), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'irep.h' not generated, too many nodes (80), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'message.h' not generated, too many nodes (97), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'namespace.h' not generated, too many nodes (88), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (122), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. -warning: Included by graph for 'prefix.h' not generated, too many nodes (62), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. +warning: Included by graph for 'prefix.h' not generated, too many nodes (63), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (67), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'std_code.h' not generated, too many nodes (71), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'std_expr.h' not generated, too many nodes (178), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 20c1d063ccd..3dab4f2a856 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2161,7 +2161,19 @@ exprt c_typecheck_baset::do_special_functions( const irep_idt &identifier=to_symbol_expr(f_op).get_identifier(); - if(identifier==CPROVER_PREFIX "same_object") + if(identifier == CPROVER_PREFIX "is_fresh") + { + if(expr.arguments().size() != 2) + { + error().source_location = f_op.source_location(); + error() << CPROVER_PREFIX "is_fresh expects two operands; " + << expr.arguments().size() << "provided." << eom; + throw 0; + } + typecheck_function_call_arguments(expr); + return nil_exprt(); + } + else if(identifier == CPROVER_PREFIX "same_object") { if(expr.arguments().size()!=2) { diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h index 250b5ba06c0..72e5e05a6bb 100644 --- a/src/ansi-c/cprover_builtin_headers.h +++ b/src/ansi-c/cprover_builtin_headers.h @@ -13,7 +13,6 @@ __CPROVER_size_t __CPROVER_buffer_size(const void *); __CPROVER_bool __CPROVER_r_ok(); __CPROVER_bool __CPROVER_w_ok(); __CPROVER_bool __CPROVER_rw_ok(); -void __CPROVER_old(const void *); // bitvector analysis __CPROVER_bool __CPROVER_get_flag(const void *, const char *); @@ -35,6 +34,10 @@ void __CPROVER_atomic_begin(); void __CPROVER_atomic_end(); void __CPROVER_fence(const char *kind, ...); +// contract-related functions +__CPROVER_bool __CPROVER_is_fresh(const void *mem, __CPROVER_size_t size); +void __CPROVER_old(const void *); + // pointers __CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *); __CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *); diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h index c4e3427393a..f646f55e8ee 100644 --- a/src/ansi-c/library/cprover.h +++ b/src/ansi-c/library/cprover.h @@ -36,7 +36,6 @@ __CPROVER_size_t __CPROVER_buffer_size(const void *); __CPROVER_bool __CPROVER_r_ok(); __CPROVER_bool __CPROVER_w_ok(); __CPROVER_bool __CPROVER_rw_ok(); -void __CPROVER_old(); #if 0 __CPROVER_bool __CPROVER_equal(); diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index b7ef438ff25..b398c231a1b 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -18,12 +18,17 @@ Date: February 2016 #include +#include #include +#include #include +#include + #include #include +#include #include #include #include @@ -31,36 +36,72 @@ Date: February 2016 #include #include #include +#include #include -/// Predicate to be used with the exprt::visit() function. The function -/// found_return_value() will return `true` iff this predicate is called on an -/// expr that contains `__CPROVER_return_value`. -class return_value_visitort : public const_expr_visitort +bool return_value_visitort::found_return_value() { -public: - return_value_visitort() : const_expr_visitort(), found(false) - { - } + return found; +} - // \brief Has this object been passed to exprt::visit() on an exprt whose - // descendants contain __CPROVER_return_value? - bool found_return_value() - { - return found; - } +void return_value_visitort::operator()(const exprt &exp) +{ + if(exp.id() != ID_symbol) + return; + const symbol_exprt &sym = to_symbol_expr(exp); + found |= sym.get_identifier() == CPROVER_PREFIX "return_value"; +} + +std::set &functions_in_scope_visitort::function_calls() +{ + return function_set; +} - void operator()(const exprt &exp) override +void functions_in_scope_visitort::operator()(const goto_programt &prog) +{ + forall_goto_program_instructions(ins, prog) { - if(exp.id() != ID_symbol) - return; - const symbol_exprt &sym = to_symbol_expr(exp); - found |= sym.get_identifier() == CPROVER_PREFIX "return_value"; - } + if(ins->is_function_call()) + { + const code_function_callt &call = ins->get_function_call(); -protected: - bool found; -}; + if(call.function().id() != ID_symbol) + { + log.error().source_location = call.find_source_location(); + log.error() << "Function pointer used in function invoked by " + "function contract: " + << messaget::eom; + throw 0; + } + else + { + const irep_idt &fun_name = + to_symbol_expr(call.function()).get_identifier(); + if(function_set.find(fun_name) == function_set.end()) + { + function_set.insert(fun_name); + auto called_fun = goto_functions.function_map.find(fun_name); + if(called_fun == goto_functions.function_map.end()) + { + log.warning() << "Could not find function '" << fun_name + << "' in goto-program." << messaget::eom; + throw 0; + } + if(called_fun->second.body_available()) + { + const goto_programt &program = called_fun->second.body; + (*this)(program); + } + else + { + log.warning() << "No body for function: " << fun_name + << "invoked from function contract." << messaget::eom; + } + } + } + } + } +} exprt get_size(const typet &type, const namespacet &ns, messaget &log) { @@ -429,6 +470,9 @@ bool code_contractst::apply_function_contract( const auto &mode = symbol_table.lookup_ref(function).mode; + is_fresh_replacet is_fresh(*this, log, function); + is_fresh.create_declarations(); + // Insert assertion of the precondition immediately before the call site. if(requires.is_not_nil()) { @@ -441,11 +485,12 @@ bool code_contractst::apply_function_contract( code_assertt(requires), assertion, symbol_table.lookup_ref(function).mode); - assertion.instructions.front().source_location = requires.source_location(); + assertion.instructions.back().source_location = requires.source_location(); assertion.instructions.back().source_location.set_comment( "Check requires clause"); - assertion.instructions.front().source_location.set_property_class( + assertion.instructions.back().source_location.set_property_class( ID_precondition); + is_fresh.update_requires(assertion); auto lines_to_iterate = assertion.instructions.size(); goto_program.insert_before_swap(target, assertion); std::advance(target, lines_to_iterate); @@ -488,11 +533,11 @@ bool code_contractst::apply_function_contract( std::advance(target, lines_to_iterate); } - // To remove the function call, replace it with an assumption statement - // assuming the postcondition, if there is one. Otherwise, replace the - // function call with a SKIP statement. + // To remove the function call, insert statements related to the assumption. + // Then, replace the function call with a SKIP statement. if(ensures.is_not_nil()) { + is_fresh.update_ensures(ensures_pair.first); auto lines_to_iterate = ensures_pair.first.instructions.size(); goto_program.insert_before_swap(target, ensures_pair.first); std::advance(target, lines_to_iterate); @@ -537,6 +582,21 @@ const symbolt &code_contractst::new_tmp_symbol( symbol_table); } +const namespacet &code_contractst::get_namespace() const +{ + return ns; +} + +symbol_tablet &code_contractst::get_symbol_table() +{ + return symbol_table; +} + +goto_functionst &code_contractst::get_goto_functions() +{ + return goto_functions; +} + exprt code_contractst::create_alias_expression( const exprt &lhs, std::vector &aliasable_references) @@ -892,6 +952,7 @@ bool code_contractst::enforce_contract(const std::string &fun_to_enforce) wrapper.parameter_identifiers = mangled_fun->second.parameter_identifiers; wrapper.body.add(goto_programt::make_end_function(sl)); add_contract_check(original, mangled, wrapper.body); + return false; } @@ -983,6 +1044,9 @@ void code_contractst::add_contract_check( common_replace.insert(parameter_symbol.symbol_expr(), p); } + is_fresh_enforcet visitor(*this, log, wrapper_fun); + visitor.create_declarations(); + // Generate: assume(requires) if(requires.is_not_nil()) { @@ -996,6 +1060,7 @@ void code_contractst::add_contract_check( goto_programt assumption; converter.goto_convert( code_assumet(requires), assumption, function_symbol.mode); + visitor.update_requires(assumption); check.destructive_append(assumption); } @@ -1019,10 +1084,11 @@ void code_contractst::add_contract_check( assertion, ensures.source_location(), wrapper_fun, function_symbol.mode); ensures_pair.first.instructions.back().source_location.set_comment( "Check ensures clause"); - ensures_pair.first.instructions.front().source_location.set_property_class( + ensures_pair.first.instructions.back().source_location.set_property_class( ID_postcondition); // add all the history variable initializations + visitor.update_ensures(ensures_pair.first); check.destructive_append(ensures_pair.second); } @@ -1809,3 +1875,277 @@ exprt assigns_clauset::compatible_expression( return result; } + +std::set &find_is_fresh_calls_visitort::is_fresh_calls() +{ + return function_set; +} + +void find_is_fresh_calls_visitort::clear_set() +{ + function_set.clear(); +} + +void find_is_fresh_calls_visitort::operator()(goto_programt &prog) +{ + Forall_goto_program_instructions(ins, prog) + { + if(ins->is_function_call()) + { + const code_function_callt &call = ins->get_function_call(); + + if(call.function().id() == ID_symbol) + { + const irep_idt &fun_name = + to_symbol_expr(call.function()).get_identifier(); + + if(fun_name == (CPROVER_PREFIX + std::string("is_fresh"))) + { + function_set.insert(ins); + } + } + } + } +} + +void is_fresh_baset::update_requires(goto_programt &requires) +{ + find_is_fresh_calls_visitort requires_visitor; + requires_visitor(requires); + for(auto it : requires_visitor.is_fresh_calls()) + { + create_requires_fn_call(it); + } +} + +void is_fresh_baset::update_ensures(goto_programt &ensures) +{ + find_is_fresh_calls_visitort ensures_visitor; + ensures_visitor(ensures); + for(auto it : ensures_visitor.is_fresh_calls()) + { + create_ensures_fn_call(it); + } +} + +// +// +// Code largely copied from model_argc_argv.cpp +// +// + +void is_fresh_baset::add_declarations(const std::string &decl_string) +{ + log.debug() << "Creating declarations: \n" << decl_string << "\n"; + + std::istringstream iss(decl_string); + + ansi_c_languaget ansi_c_language; + ansi_c_language.set_message_handler(log.get_message_handler()); + configt::ansi_ct::preprocessort pp = config.ansi_c.preprocessor; + config.ansi_c.preprocessor = configt::ansi_ct::preprocessort::NONE; + ansi_c_language.parse(iss, ""); + config.ansi_c.preprocessor = pp; + + symbol_tablet tmp_symbol_table; + ansi_c_language.typecheck(tmp_symbol_table, ""); + exprt value = nil_exprt(); + + goto_functionst tmp_functions; + + // Add the new functions into the goto functions table. + parent.get_goto_functions().function_map[ensures_fn_name].copy_from( + tmp_functions.function_map[ensures_fn_name]); + + parent.get_goto_functions().function_map[requires_fn_name].copy_from( + tmp_functions.function_map[requires_fn_name]); + + for(const auto &symbol_pair : tmp_symbol_table.symbols) + { + if( + symbol_pair.first == memmap_name || + symbol_pair.first == ensures_fn_name || + symbol_pair.first == requires_fn_name || symbol_pair.first == "malloc") + { + this->parent.get_symbol_table().insert(symbol_pair.second); + } + // Parameters are stored as scoped names in the symbol table. + else if( + (has_prefix( + id2string(symbol_pair.first), id2string(ensures_fn_name) + "::") || + has_prefix( + id2string(symbol_pair.first), id2string(requires_fn_name) + "::")) && + parent.get_symbol_table().add(symbol_pair.second)) + { + UNREACHABLE; + } + } + + // We have to set the global memory map array to + // all zeros for this to work properly + const array_typet ty = + to_array_type(tmp_symbol_table.lookup_ref(memmap_name).type); + constant_exprt initial_value(irep_idt(dstringt("0")), ty.subtype()); + array_of_exprt memmap_init(initial_value, ty); + goto_programt::instructiont a = + goto_programt::make_assignment(symbol_exprt(memmap_name, ty), memmap_init); + + // insert the assignment into the initialize function. + auto called_func = + parent.get_goto_functions().function_map.find(INITIALIZE_FUNCTION); + goto_programt &body = called_func->second.body; + auto target = body.get_end_function(); + body.insert_before(target, a); +} + +void is_fresh_baset::update_fn_call( + goto_programt::targett &ins, + const std::string &fn_name, + bool add_address_of) +{ + const code_function_callt &const_call = ins->get_function_call(); + code_function_callt call( + exprt(const_call.lhs()), + exprt(const_call.function()), + code_function_callt::argumentst(const_call.arguments())); + + // adjusting the expression for the first argument, if required + if(add_address_of) + { + INVARIANT(call.arguments().size() > 0, "Function must have arguments"); + call.arguments()[0] = address_of_exprt(call.arguments()[0]); + } + + // fixing the function name. + to_symbol_expr(call.function()).set_identifier(fn_name); + log.debug() << "printing updated call expression: " + << expr2c(call, parent.get_namespace()) << "\n"; + + ins->set_function_call(call); +} + +/* Declarations for contract enforcement */ + +is_fresh_enforcet::is_fresh_enforcet( + code_contractst &_parent, + messaget _log, + irep_idt _fun_id) + : is_fresh_baset(_parent, _log, _fun_id) +{ + std::stringstream ssreq, ssensure, ssmemmap; + ssreq << CPROVER_PREFIX << fun_id << "_requires_is_fresh"; + this->requires_fn_name = ssreq.str(); + + ssensure << CPROVER_PREFIX << fun_id << "_ensures_is_fresh"; + this->ensures_fn_name = ssensure.str(); + + ssmemmap << CPROVER_PREFIX << fun_id << "_memory_map"; + this->memmap_name = ssmemmap.str(); +} + +void is_fresh_enforcet::create_declarations() +{ + std::ostringstream oss; + std::string cprover_prefix(CPROVER_PREFIX); + oss << "static _Bool " << memmap_name + << "[" + cprover_prefix + "constant_infinity_uint]; \n" + << "\n" + << "_Bool " << requires_fn_name + << "(void **elem, " + cprover_prefix + "size_t size) { \n" + << " *elem = malloc(size); \n" + << " if (!*elem || " << memmap_name + << "[" + cprover_prefix + "POINTER_OBJECT(*elem)]) return 0; \n" + << " " << memmap_name << "[" + cprover_prefix + << "POINTER_OBJECT(*elem)] = 1; \n" + << " return 1; \n" + << "} \n" + << "\n" + << "_Bool " << ensures_fn_name + << "(void *elem, " + cprover_prefix + "size_t size) { \n" + << " _Bool ok = (!" << memmap_name + << "[" + cprover_prefix + "POINTER_OBJECT(elem)] && " + << cprover_prefix + "r_ok(elem, size)); \n" + << " " << memmap_name << "[" + cprover_prefix + << "POINTER_OBJECT(elem)] = 1; \n" + << " return ok; \n" + << "}"; + + add_declarations(oss.str()); +} + +void is_fresh_enforcet::create_requires_fn_call(goto_programt::targett &ins) +{ + update_fn_call(ins, requires_fn_name, true); +} + +void is_fresh_enforcet::create_ensures_fn_call(goto_programt::targett &ins) +{ + update_fn_call(ins, ensures_fn_name, false); +} + +/* Declarations for contract replacement: note that there may be several + instances of the same function called in a particular context, so care must be taken + that the 'call' functions and global data structure are unique for each instance. + This is why we check that the symbols are unique for each such declaration. */ + +std::string unique_symbol(const symbol_tablet &tbl, const std::string &original) +{ + auto size = tbl.next_unused_suffix(original); + return original + std::to_string(size); +} + +is_fresh_replacet::is_fresh_replacet( + code_contractst &_parent, + messaget _log, + irep_idt _fun_id) + : is_fresh_baset(_parent, _log, _fun_id) +{ + std::stringstream ssreq, ssensure, ssmemmap; + ssreq /* << CPROVER_PREFIX */ << fun_id << "_call_requires_is_fresh"; + this->requires_fn_name = + unique_symbol(parent.get_symbol_table(), ssreq.str()); + + ssensure /* << CPROVER_PREFIX */ << fun_id << "_call_ensures_is_fresh"; + this->ensures_fn_name = + unique_symbol(parent.get_symbol_table(), ssensure.str()); + + ssmemmap /* << CPROVER_PREFIX */ << fun_id << "_memory_map"; + this->memmap_name = unique_symbol(parent.get_symbol_table(), ssmemmap.str()); +} + +void is_fresh_replacet::create_declarations() +{ + std::ostringstream oss; + std::string cprover_prefix(CPROVER_PREFIX); + oss << "static _Bool " << memmap_name + << "[" + cprover_prefix + "constant_infinity_uint]; \n" + << "\n" + << "static _Bool " << requires_fn_name + << "(void *elem, " + cprover_prefix + "size_t size) { \n" + << " _Bool r_ok = " + cprover_prefix + "r_ok(elem, size); \n" + << " if (" << memmap_name + << "[" + cprover_prefix + "POINTER_OBJECT(elem)]" + << " != 0 || !r_ok) return 0; \n" + << " " << memmap_name << "[" + << cprover_prefix + "POINTER_OBJECT(elem)] = 1; \n" + << " return 1; \n" + << "} \n" + << " \n" + << "_Bool " << ensures_fn_name + << "(void **elem, " + cprover_prefix + "size_t size) { \n" + << " *elem = malloc(size); \n" + << " return (*elem != 0); \n" + << "} \n"; + + add_declarations(oss.str()); +} + +void is_fresh_replacet::create_requires_fn_call(goto_programt::targett &ins) +{ + update_fn_call(ins, requires_fn_name, false); +} + +void is_fresh_replacet::create_ensures_fn_call(goto_programt::targett &ins) +{ + update_fn_call(ins, ensures_fn_name, true); +} diff --git a/src/goto-instrument/code_contracts.h b/src/goto-instrument/code_contracts.h index f1ecd275276..f9da1d19360 100644 --- a/src/goto-instrument/code_contracts.h +++ b/src/goto-instrument/code_contracts.h @@ -102,6 +102,11 @@ class code_contractst const goto_programt::targett loop_head, const loopt &loop, const irep_idt &mode); + const namespacet &get_namespace() const; + + // for "helper" classes to update symbol table. + symbol_tablet &get_symbol_table(); + goto_functionst &get_goto_functions(); namespacet ns; @@ -393,4 +398,144 @@ class assigns_clauset messaget log; }; +class is_fresh_baset +{ +public: + is_fresh_baset( + code_contractst &_parent, + messaget _log, + const irep_idt _fun_id) + : parent(_parent), log(_log), fun_id(_fun_id) + { + } + + void update_requires(goto_programt &requires); + void update_ensures(goto_programt &ensures); + + virtual void create_declarations() = 0; + +protected: + void add_declarations(const std::string &decl_string); + void update_fn_call( + goto_programt::targett &target, + const std::string &name, + bool add_address_of); + + virtual void create_requires_fn_call(goto_programt::targett &target) = 0; + virtual void create_ensures_fn_call(goto_programt::targett &target) = 0; + + code_contractst &parent; + messaget log; + irep_idt fun_id; + + // written by the child classes. + std::string memmap_name; + std::string requires_fn_name; + std::string ensures_fn_name; +}; + +class is_fresh_enforcet : public is_fresh_baset +{ +public: + is_fresh_enforcet( + code_contractst &_parent, + messaget _log, + const irep_idt _fun_id); + + virtual void create_declarations(); + +protected: + virtual void create_requires_fn_call(goto_programt::targett &target); + virtual void create_ensures_fn_call(goto_programt::targett &target); +}; + +class is_fresh_replacet : public is_fresh_baset +{ +public: + is_fresh_replacet( + code_contractst &_parent, + messaget _log, + const irep_idt _fun_id); + + virtual void create_declarations(); + +protected: + virtual void create_requires_fn_call(goto_programt::targett &target); + virtual void create_ensures_fn_call(goto_programt::targett &target); +}; + +/// Predicate to be used with the exprt::visit() function. It +/// will return the set of function calls within a goto program. +class find_is_fresh_calls_visitort +{ +public: + find_is_fresh_calls_visitort() + { + } + + // \brief return the set of functions invoked by + // the call graph of this program. + std::set &is_fresh_calls(); + void clear_set(); + void operator()(goto_programt &prog); + +protected: + std::set function_set; +}; + +/// Predicate to be used with the exprt::visit() function. The function +/// found_return_value() will return `true` iff this predicate is called on an +/// expr that contains `__CPROVER_return_value`. +class return_value_visitort : public const_expr_visitort +{ +public: + return_value_visitort() : const_expr_visitort(), found(false) + { + } + + // \brief Has this object been passed to exprt::visit() on an exprt whose + // descendants contain __CPROVER_return_value? + bool found_return_value(); + void operator()(const exprt &exp) override; + +protected: + bool found; +}; + +/// Predicate to be used with the exprt::visit() function. The function +/// found_return_value() will return `true` iff this predicate is called on an +/// expr that contains `__CPROVER_return_value`. +class functions_in_scope_visitort +{ +public: + functions_in_scope_visitort( + const goto_functionst &goto_functions, + messaget &log) + : goto_functions(goto_functions), log(log) + { + } + + // \brief return the set of functions invoked by + // the call graph of this program. + std::set &function_calls(); + void operator()(const goto_programt &prog); + +protected: + const goto_functionst &goto_functions; + messaget &log; + std::set function_set; +}; + +class function_binding_visitort : const_expr_visitort +{ +public: + function_binding_visitort() : const_expr_visitort() + { + } + + void operator()(const exprt &exp) override + { + } +}; + #endif // CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H