From a465b986b4a406f92188bcc416476b81e19fa030 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Thu, 8 Dec 2022 15:01:46 +0000 Subject: [PATCH 1/2] CONTRACTS: support bounded user-defined memory predicates Users can now write their own pointer predicates in terms of: - __CPROVER_is_fresh(ptr, size) - __CPROVER_obeys_contract(ptr, target) A rewriting pass lifts these user-defined pointer predicates into predicates that take pointers by reference and can make the predicates hold in assumption contexts using side-effects, and check the predicates in assertion contexts. Limitiations: User-defined predicates can be self-recursive but not mutually recursive, and their evaluation needs to be terminate, i.e. they can only describe bounded data structures. --- .../assigns-enforce-malloc-zero/main.c | 33 +- .../assigns-enforce-malloc-zero/test.desc | 13 +- .../assigns-replace-malloc-zero/main.c | 54 +-- .../assigns-replace-malloc-zero/test.desc | 4 +- .../is_unique_01_replace/main.c | 84 +--- .../is_unique_01_replace/test.desc | 7 +- .../main.c | 22 + .../test.desc | 12 + .../main.c | 101 +++++ .../test.desc | 10 + .../main.c | 124 ++++++ .../test.desc | 10 + .../main.c | 44 ++ .../test.desc | 9 + .../main.c | 36 ++ .../test.desc | 10 + .../main.c | 76 ++++ .../test.desc | 10 + .../main.c | 94 ++++ .../test.desc | 11 + .../test_array_memory_enforce/main.c | 18 +- .../test_array_memory_replace/main.c | 32 +- .../test_array_memory_replace/test.desc | 7 +- .../main.c | 33 +- .../test.desc | 7 +- .../test_scalar_memory_replace/main.c | 31 +- .../test_scalar_memory_replace/test.desc | 6 +- .../test_array_memory_replace/test.desc | 2 +- .../test.desc | 2 +- src/ansi-c/library/cprover_contracts.c | 33 +- src/goto-instrument/Makefile | 1 + .../doc/developer/contracts-dev-arch.md | 1 + .../contracts-dev-spec-dfcc-instrument.md | 10 +- ...ts-dev-spec-memory-predicates-rewriting.md | 192 ++++++++ .../contracts-dev-spec-spec-rewriting.md | 2 +- .../doc/developer/contracts-dev-spec.md | 1 + .../doc/user/contracts-memory-predicates.md | 88 ++++ .../contracts/doc/user/contracts-user.md | 1 + .../contracts/dynamic-frames/dfcc.cpp | 17 + .../contracts/dynamic-frames/dfcc.h | 3 + .../dynamic-frames/dfcc_contract_handler.cpp | 6 +- .../dynamic-frames/dfcc_contract_handler.h | 3 + .../dfcc_lift_memory_predicates.cpp | 419 ++++++++++++++++++ .../dfcc_lift_memory_predicates.h | 113 +++++ .../dynamic-frames/dfcc_spec_functions.cpp | 67 --- .../dynamic-frames/dfcc_spec_functions.h | 29 -- .../dynamic-frames/dfcc_wrapper_program.cpp | 11 +- .../dynamic-frames/dfcc_wrapper_program.h | 8 +- 48 files changed, 1585 insertions(+), 322 deletions(-) create mode 100644 regression/contracts-dfcc/memory-predicates-is-fresh-requires-max-malloc-size/main.c create mode 100644 regression/contracts-dfcc/memory-predicates-is-fresh-requires-max-malloc-size/test.desc create mode 100644 regression/contracts-dfcc/memory-predicates-user-defined-ensures-enforce/main.c create mode 100644 regression/contracts-dfcc/memory-predicates-user-defined-ensures-enforce/test.desc create mode 100644 regression/contracts-dfcc/memory-predicates-user-defined-ensures-replace/main.c create mode 100644 regression/contracts-dfcc/memory-predicates-user-defined-ensures-replace/test.desc create mode 100644 regression/contracts-dfcc/memory-predicates-user-defined-mutually-recursive-fail/main.c create mode 100644 regression/contracts-dfcc/memory-predicates-user-defined-mutually-recursive-fail/test.desc create mode 100644 regression/contracts-dfcc/memory-predicates-user-defined-recursive-alternation/main.c create mode 100644 regression/contracts-dfcc/memory-predicates-user-defined-recursive-alternation/test.desc create mode 100644 regression/contracts-dfcc/memory-predicates-user-defined-requires-enforce/main.c create mode 100644 regression/contracts-dfcc/memory-predicates-user-defined-requires-enforce/test.desc create mode 100644 regression/contracts-dfcc/memory-predicates-user-defined-requires-replace/main.c create mode 100644 regression/contracts-dfcc/memory-predicates-user-defined-requires-replace/test.desc create mode 100644 src/goto-instrument/contracts/doc/developer/contracts-dev-spec-memory-predicates-rewriting.md create mode 100644 src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp create mode 100644 src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.h diff --git a/regression/contracts-dfcc/assigns-enforce-malloc-zero/main.c b/regression/contracts-dfcc/assigns-enforce-malloc-zero/main.c index 61f105f8a43..e2026c00273 100644 --- a/regression/contracts-dfcc/assigns-enforce-malloc-zero/main.c +++ b/regression/contracts-dfcc/assigns-enforce-malloc-zero/main.c @@ -1,31 +1,32 @@ +#include #include -// returns the index at which the write was performed if any -// -1 otherwise -int foo(char *a, int size) +bool foo(char *a, size_t size, size_t *out) // clang-format off - __CPROVER_requires(0 <= size && size <= __CPROVER_max_malloc_size) __CPROVER_requires(a == NULL || __CPROVER_is_fresh(a, size)) - __CPROVER_assigns(a: __CPROVER_object_whole(a)) + __CPROVER_requires(__CPROVER_is_fresh(out, sizeof(*out))) + __CPROVER_assigns(a: __CPROVER_object_from(a), *out) __CPROVER_ensures( - a && __CPROVER_return_value >= 0 ==> a[__CPROVER_return_value] == 0) + a && __CPROVER_return_value ==> + (0 <= *out && *out < size && + a[*out] == 0) + ) // clang-format on { - if(!a) - return -1; - int i; - if(0 <= i && i < size) + size_t i; + if(a && 0 <= i && i < size) { a[i] = 0; - return i; + *out = i; + return true; } - return -1; + return false; } -int main() +void main() { - size_t size; char *a; - foo(a, size); - return 0; + size_t size; + size_t *out; + foo(a, size, out); } diff --git a/regression/contracts-dfcc/assigns-enforce-malloc-zero/test.desc b/regression/contracts-dfcc/assigns-enforce-malloc-zero/test.desc index 7d82f4cf938..caf6e623c0a 100644 --- a/regression/contracts-dfcc/assigns-enforce-malloc-zero/test.desc +++ b/regression/contracts-dfcc/assigns-enforce-malloc-zero/test.desc @@ -1,11 +1,14 @@ CORE main.c ---dfcc main --enforce-contract foo _ --malloc-may-fail --malloc-fail-null -^\[foo.assigns.\d+\] line 19 Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ +--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo +^\[foo.assigns.\d+\] line \d+ Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that \*out is assignable: SUCCESS$ ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -This test checks that objects of size zero or __CPROVER_max_malloc_size -do not cause spurious falsifications in assigns clause instrumentation -in contract enforcement mode. +This test checks assuming is_fresh(ptr, size) with a non-deterministic size +does not result in spurious falsifications when checking assigns clauses. +An implicit strict upper bound of __CPROVER_max_malloc_size is imposed on the size by +__CPROVER_is_fresh which guarantees the absence of pointer overflow when computing +the address `ptr + size`. diff --git a/regression/contracts-dfcc/assigns-replace-malloc-zero/main.c b/regression/contracts-dfcc/assigns-replace-malloc-zero/main.c index 444b33ce29f..6bbea93e2c2 100644 --- a/regression/contracts-dfcc/assigns-replace-malloc-zero/main.c +++ b/regression/contracts-dfcc/assigns-replace-malloc-zero/main.c @@ -1,37 +1,41 @@ +#include #include -// returns the index at which the write was performed if any -// -1 otherwise -int foo(char *a, int size) +bool foo(char *a, size_t size, size_t *out) // clang-format off -__CPROVER_requires(0 <= size && size <= __CPROVER_max_malloc_size) -__CPROVER_requires(a == NULL || __CPROVER_rw_ok(a, size)) -__CPROVER_assigns(__CPROVER_object_whole(a)) -__CPROVER_ensures( - a && __CPROVER_return_value >= 0 ==> a[__CPROVER_return_value] == 0) + __CPROVER_requires(a == NULL || __CPROVER_is_fresh(a, size)) + __CPROVER_requires(__CPROVER_is_fresh(out, sizeof(*out))) + __CPROVER_assigns(a: __CPROVER_object_from(a), *out) + __CPROVER_ensures( + a && __CPROVER_return_value ==> + (0 <= *out && *out < size && + a[*out] == 0) + ) // clang-format on { - if(!a) - return -1; - int i; - if(0 <= i && i < size) + size_t i; + if(a && 0 <= i && i < size) { a[i] = 0; - return i; + *out = i; + return true; } - return -1; + return false; } -int main() +int nondet_int(); + +void bar(int size) +{ + size_t out; + char *a = malloc(size); + bool res = foo(a, size, &out); + if(a && res) + __CPROVER_assert(a[out] == 0, "expecting SUCCESS"); +} + +void main() { - int size; - if(size < 0) - size = 0; - if(size > __CPROVER_max_malloc_size) - size = __CPROVER_max_malloc_size; - char *a = malloc(size * sizeof(*a)); - int res = foo(a, size); - if(a && res >= 0) - __CPROVER_assert(a[res] == 0, "expecting SUCCESS"); - return 0; + size_t size; + bar(size); } diff --git a/regression/contracts-dfcc/assigns-replace-malloc-zero/test.desc b/regression/contracts-dfcc/assigns-replace-malloc-zero/test.desc index 2e410cec503..66adacca708 100644 --- a/regression/contracts-dfcc/assigns-replace-malloc-zero/test.desc +++ b/regression/contracts-dfcc/assigns-replace-malloc-zero/test.desc @@ -1,9 +1,9 @@ CORE main.c ---dfcc main --replace-call-with-contract foo _ --malloc-may-fail --malloc-fail-null +--dfcc main --replace-call-with-contract foo --malloc-may-fail --malloc-fail-null ^EXIT=0$ ^SIGNAL=0$ -\[main\.assertion\.1\] line 35 expecting SUCCESS: SUCCESS$ +\[bar\.assertion\.\d+\] line \d+ expecting SUCCESS: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- This test checks that objects of size zero or of __CPROVER_max_malloc_size diff --git a/regression/contracts-dfcc/is_unique_01_replace/main.c b/regression/contracts-dfcc/is_unique_01_replace/main.c index b81f917e90c..cc9d9e2bff4 100644 --- a/regression/contracts-dfcc/is_unique_01_replace/main.c +++ b/regression/contracts-dfcc/is_unique_01_replace/main.c @@ -1,84 +1,38 @@ #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; + return 0 < *x && *x < 5; } -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; + 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)) +int foo(int *x) + // clang-format off +__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int))) +__CPROVER_requires(ptr_ok(x)) +__CPROVER_assigns(*x) +__CPROVER_ensures(!ptr_ok(x)) +__CPROVER_ensures(return_ok(__CPROVER_return_value, x)) +// clang-format on { *x = *x + 4; - int y = *x + 5; return *x + 5; } -int main() +void 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; + int x; + int *_x = &x; + if(ptr_ok(_x)) + { + int ret_val = foo(_x); + assert(!ptr_ok(_x)); + assert(return_ok(ret_val, _x)); + } } diff --git a/regression/contracts-dfcc/is_unique_01_replace/test.desc b/regression/contracts-dfcc/is_unique_01_replace/test.desc index eb56439d295..34b59785f6a 100644 --- a/regression/contracts-dfcc/is_unique_01_replace/test.desc +++ b/regression/contracts-dfcc/is_unique_01_replace/test.desc @@ -6,8 +6,5 @@ main.c ^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. +This test shows that replacing a call by a contract establishes the +postconditions of the contracts. diff --git a/regression/contracts-dfcc/memory-predicates-is-fresh-requires-max-malloc-size/main.c b/regression/contracts-dfcc/memory-predicates-is-fresh-requires-max-malloc-size/main.c new file mode 100644 index 00000000000..6d3c2bfb9c1 --- /dev/null +++ b/regression/contracts-dfcc/memory-predicates-is-fresh-requires-max-malloc-size/main.c @@ -0,0 +1,22 @@ +#include + +void foo(char *arr, size_t size) + // clang-format off +__CPROVER_requires(__CPROVER_is_fresh(arr, size)) +__CPROVER_assigns(__CPROVER_object_from(arr)) +// clang-format on +{ + assert(__CPROVER_same_object(arr, arr + size)); + if(size > 0) + { + arr[0] = 0; + arr[size - 1] = 0; + } +} + +int main() +{ + char *arr; + size_t size; + foo(arr, size); +} diff --git a/regression/contracts-dfcc/memory-predicates-is-fresh-requires-max-malloc-size/test.desc b/regression/contracts-dfcc/memory-predicates-is-fresh-requires-max-malloc-size/test.desc new file mode 100644 index 00000000000..f0a7357d53a --- /dev/null +++ b/regression/contracts-dfcc/memory-predicates-is-fresh-requires-max-malloc-size/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check --pointer-overflow-check +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This tests shows how assuming that a pointer is fresh with a nondeterministic +size implicitly assumes that the size is strictly less than the max malloc +size. This is in order to ensure that the internal representation used for +assignable address ranges cannot suffer pointer overflows. diff --git a/regression/contracts-dfcc/memory-predicates-user-defined-ensures-enforce/main.c b/regression/contracts-dfcc/memory-predicates-user-defined-ensures-enforce/main.c new file mode 100644 index 00000000000..aa9e55daa3e --- /dev/null +++ b/regression/contracts-dfcc/memory-predicates-user-defined-ensures-enforce/main.c @@ -0,0 +1,101 @@ +#include +#include + +typedef struct list_t +{ + int value; + struct list_t *next; +} list_t; + +#define MIN_VALUE -10 +#define MAX_VALUE 10 + +bool is_list(list_t *l, size_t len) +{ + if(len == 0) + return l == NULL; + else + return __CPROVER_is_fresh(l, sizeof(*l)) && + (MIN_VALUE <= l->value && l->value <= MAX_VALUE) && + is_list(l->next, len - 1); +} + +typedef struct buffer_t +{ + size_t size; + char *arr; +} buffer_t; + +typedef struct double_buffer_t +{ + buffer_t *first; + buffer_t *second; +} double_buffer_t; + +#define MIN_BUFFER_SIZE 1 +#define MAX_BUFFER_SIZE 10 + +bool is_sized_array(char *arr, size_t size) +{ + return (MIN_BUFFER_SIZE <= size && size <= MAX_BUFFER_SIZE) && + __CPROVER_is_fresh(arr, size); +} + +bool is_buffer(buffer_t *b) +{ + return __CPROVER_is_fresh(b, sizeof(*b)) && is_sized_array(b->arr, b->size); +} + +bool is_double_buffer(double_buffer_t *b) +{ + return __CPROVER_is_fresh(b, sizeof(*b)) && is_buffer(b->first) && + is_buffer(b->second); +} + +#define LIST_LEN 3 + +list_t *create_node(int value, list_t *next) +{ + assert(MIN_VALUE <= value && value <= MAX_VALUE); + list_t *result = malloc(sizeof(list_t)); + result->value = value; + result->next = next; + return result; +} + +buffer_t *create_buffer(size_t size) +{ + assert(MIN_BUFFER_SIZE <= size && size <= MAX_BUFFER_SIZE); + buffer_t *result = malloc(sizeof(buffer_t)); + result->arr = malloc(size); + result->size = size; + return result; +} + +double_buffer_t *create_double_buffer(size_t first_size, size_t second_size) +{ + double_buffer_t *result = malloc(sizeof(double_buffer_t)); + result->first = create_buffer(first_size); + result->second = create_buffer(second_size); + return result; +} + +void foo(list_t **l, double_buffer_t **b) + // clang-format off +__CPROVER_requires(__CPROVER_is_fresh(l, sizeof(*l))) +__CPROVER_requires(__CPROVER_is_fresh(b, sizeof(*b))) +__CPROVER_assigns(*l, *b) +__CPROVER_ensures(is_list(*l, LIST_LEN)) +__CPROVER_ensures(is_double_buffer(*b)) +// clang-format on +{ + *l = create_node(1, create_node(2, create_node(3, NULL))); + *b = create_double_buffer(1, 10); +} + +int main() +{ + list_t *l; + double_buffer_t *b; + foo(&l, &b); +} diff --git a/regression/contracts-dfcc/memory-predicates-user-defined-ensures-enforce/test.desc b/regression/contracts-dfcc/memory-predicates-user-defined-ensures-enforce/test.desc new file mode 100644 index 00000000000..1ab0b27e0cc --- /dev/null +++ b/regression/contracts-dfcc/memory-predicates-user-defined-ensures-enforce/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks if user defined predicates in ensures clauses are successfully asserted +when enforcing contracts. diff --git a/regression/contracts-dfcc/memory-predicates-user-defined-ensures-replace/main.c b/regression/contracts-dfcc/memory-predicates-user-defined-ensures-replace/main.c new file mode 100644 index 00000000000..cd4b9ac8591 --- /dev/null +++ b/regression/contracts-dfcc/memory-predicates-user-defined-ensures-replace/main.c @@ -0,0 +1,124 @@ +#include +#include + +typedef struct list_t +{ + int value; + struct list_t *next; +} list_t; + +#define MIN_VALUE -10 +#define MAX_VALUE 10 + +bool is_list(list_t *l, size_t len) +{ + if(len == 0) + return l == NULL; + else + return __CPROVER_is_fresh(l, sizeof(*l)) && + (MIN_VALUE <= l->value && l->value <= MAX_VALUE) && + is_list(l->next, len - 1); +} + +typedef struct buffer_t +{ + size_t size; + char *arr; +} buffer_t; + +typedef struct double_buffer_t +{ + buffer_t *first; + buffer_t *second; +} double_buffer_t; + +#define MIN_BUFFER_SIZE 1 +#define MAX_BUFFER_SIZE 10 + +bool is_sized_array(char *arr, size_t size) +{ + return (MIN_BUFFER_SIZE <= size && size <= MAX_BUFFER_SIZE) && + __CPROVER_is_fresh(arr, size); +} + +bool is_buffer(buffer_t *b) +{ + return __CPROVER_is_fresh(b, sizeof(*b)) && is_sized_array(b->arr, b->size); +} + +bool is_double_buffer(double_buffer_t *b) +{ + return __CPROVER_is_fresh(b, sizeof(*b)) && is_buffer(b->first) && + is_buffer(b->second); +} + +#define LIST_LEN 3 + +list_t *create_node(int value, list_t *next) +{ + assert(MIN_VALUE <= value && value <= MAX_VALUE); + list_t *result = malloc(sizeof(list_t)); + result->value = value; + result->next = next; + return result; +} + +buffer_t *create_buffer(size_t size) +{ + assert(MIN_BUFFER_SIZE <= size && size <= MAX_BUFFER_SIZE); + buffer_t *result = malloc(sizeof(buffer_t)); + result->arr = malloc(size); + result->size = size; + return result; +} + +double_buffer_t *create_double_buffer(size_t first_size, size_t second_size) +{ + double_buffer_t *result = malloc(sizeof(double_buffer_t)); + result->first = create_buffer(first_size); + result->second = create_buffer(second_size); + return result; +} + +void foo(list_t **l, double_buffer_t **b) + // clang-format off +__CPROVER_requires(__CPROVER_is_fresh(l, sizeof(*l))) +__CPROVER_requires(__CPROVER_is_fresh(b, sizeof(*b))) +__CPROVER_assigns(*l, *b) __CPROVER_ensures(is_list(*l, LIST_LEN)) +__CPROVER_ensures(is_double_buffer(*b)) +// clang-format on +{ + *l = create_node(1, create_node(2, create_node(3, NULL))); + *b = create_double_buffer(1, 10); +} + +void bar() +{ + list_t *l = NULL; + double_buffer_t *b = NULL; + + foo(&l, &b); + + assert(__CPROVER_r_ok(l, sizeof(list_t))); + assert(__CPROVER_r_ok(l->next, sizeof(list_t))); + assert(__CPROVER_r_ok(l->next->next, sizeof(list_t))); + assert(l->next->next->next == NULL); + assert(MIN_VALUE <= l->value && l->value <= MAX_VALUE); + assert(MIN_VALUE <= l->next->value && l->next->value <= MAX_VALUE); + assert( + MIN_VALUE <= l->next->next->value && l->next->next->value <= MAX_VALUE); + assert(__CPROVER_r_ok(b, sizeof(double_buffer_t))); + assert(__CPROVER_r_ok(b->first, sizeof(buffer_t))); + assert(__CPROVER_r_ok(b->first->arr, b->first->size)); + assert( + MIN_BUFFER_SIZE <= b->first->size && b->first->size <= MAX_BUFFER_SIZE); + assert(__CPROVER_r_ok(b->second, sizeof(buffer_t))); + assert(__CPROVER_r_ok(b->second->arr, b->second->size)); + assert( + MIN_BUFFER_SIZE <= b->second->size && b->second->size <= MAX_BUFFER_SIZE); +} + +int main() +{ + bar(); +} diff --git a/regression/contracts-dfcc/memory-predicates-user-defined-ensures-replace/test.desc b/regression/contracts-dfcc/memory-predicates-user-defined-ensures-replace/test.desc new file mode 100644 index 00000000000..224938be523 --- /dev/null +++ b/regression/contracts-dfcc/memory-predicates-user-defined-ensures-replace/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--dfcc main --enforce-contract bar --replace-call-with-contract foo _ --pointer-check --pointer-primitive-check +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks that user defined predicates assumed in ensures clauses for replaced +contracts build a state such that the predicates holds. diff --git a/regression/contracts-dfcc/memory-predicates-user-defined-mutually-recursive-fail/main.c b/regression/contracts-dfcc/memory-predicates-user-defined-mutually-recursive-fail/main.c new file mode 100644 index 00000000000..304e273b62d --- /dev/null +++ b/regression/contracts-dfcc/memory-predicates-user-defined-mutually-recursive-fail/main.c @@ -0,0 +1,44 @@ +#include +#include + +typedef struct list_t +{ + int value; + struct list_t *next; +} list_t; + +bool is_positive_list(list_t *l, size_t len) +{ + if(len == 0) + return l == NULL; + else + return __CPROVER_is_fresh(l, sizeof(*l)) && (l->value >= 0) && + is_negative_list(l->next, len - 1); +} + +bool is_negative_list(list_t *l, size_t len) +{ + if(len == 0) + return l == NULL; + else + return __CPROVER_is_fresh(l, sizeof(*l)) && (l->value <= 0) && + is_positive_list(l->next, len - 1); +} + +#define LIST_LEN 3 + +void foo(list_t *l) + // clang-format off + __CPROVER_requires(is_positive_list(l, LIST_LEN)) +// clang-format on +{ + assert(l->value >= 0); + assert(l->next->value <= 0); + assert(l->next->next->value >= 0); +} + +int main() +{ + list_t *l; + foo(l); +} diff --git a/regression/contracts-dfcc/memory-predicates-user-defined-mutually-recursive-fail/test.desc b/regression/contracts-dfcc/memory-predicates-user-defined-mutually-recursive-fail/test.desc new file mode 100644 index 00000000000..0daf2567c3d --- /dev/null +++ b/regression/contracts-dfcc/memory-predicates-user-defined-mutually-recursive-fail/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check +^could not determine instrumentation order for memory predicates, most likely due to mutual recursion$ +^EXIT=(0|127|134|137)$ +^SIGNAL=0$ +-- +-- +Checks that mutually recursive memory predicates are detected and rejected. diff --git a/regression/contracts-dfcc/memory-predicates-user-defined-recursive-alternation/main.c b/regression/contracts-dfcc/memory-predicates-user-defined-recursive-alternation/main.c new file mode 100644 index 00000000000..48652b5384b --- /dev/null +++ b/regression/contracts-dfcc/memory-predicates-user-defined-recursive-alternation/main.c @@ -0,0 +1,36 @@ +#include +#include + +typedef struct list_t +{ + int value; + struct list_t *next; +} list_t; + +bool is_alternating_list(list_t *l, size_t len, bool pos) +{ + if(len == 0) + return l == NULL; + else + return __CPROVER_is_fresh(l, sizeof(*l)) && + (pos ? (l->value >= 0) : (l->value <= 0)) && + is_alternating_list(l->next, len - 1, !pos); +} + +#define LIST_LEN 3 + +void foo(list_t *l) + // clang-format off + __CPROVER_requires(is_alternating_list(l, LIST_LEN, true)) +// clang-format on +{ + assert(l->value >= 0); + assert(l->next->value <= 0); + assert(l->next->next->value >= 0); +} + +int main() +{ + list_t *l; + foo(l); +} diff --git a/regression/contracts-dfcc/memory-predicates-user-defined-recursive-alternation/test.desc b/regression/contracts-dfcc/memory-predicates-user-defined-recursive-alternation/test.desc new file mode 100644 index 00000000000..9daba594bd4 --- /dev/null +++ b/regression/contracts-dfcc/memory-predicates-user-defined-recursive-alternation/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +Checks that recursive memory predicates that specify alternating patterns on +values can be assumed and checked. diff --git a/regression/contracts-dfcc/memory-predicates-user-defined-requires-enforce/main.c b/regression/contracts-dfcc/memory-predicates-user-defined-requires-enforce/main.c new file mode 100644 index 00000000000..ee0b412f96d --- /dev/null +++ b/regression/contracts-dfcc/memory-predicates-user-defined-requires-enforce/main.c @@ -0,0 +1,76 @@ +#include +#include + +typedef struct list_t +{ + int value; + struct list_t *next; +} list_t; + +#define MIN_VALUE -10 +#define MAX_VALUE 10 + +bool is_list(list_t *l, size_t len) +{ + if(len == 0) + return l == NULL; + else + return __CPROVER_is_fresh(l, sizeof(*l)) && + (MIN_VALUE <= l->value && l->value <= MAX_VALUE) && + is_list(l->next, len - 1); +} + +typedef struct buffer_t +{ + size_t size; + char *arr; +} buffer_t; + +typedef struct double_buffer_t +{ + buffer_t *first; + buffer_t *second; +} double_buffer_t; + +#define MIN_BUFFER_SIZE 1 +#define MAX_BUFFER_SIZE 10 + +bool is_sized_array(char *arr, size_t size) +{ + return (MIN_BUFFER_SIZE <= size && size <= MAX_BUFFER_SIZE) && + __CPROVER_is_fresh(arr, size); +} + +bool is_buffer(buffer_t *b) +{ + return __CPROVER_is_fresh(b, sizeof(*b)) && is_sized_array(b->arr, b->size); +} + +bool is_double_buffer(double_buffer_t *b) +{ + return __CPROVER_is_fresh(b, sizeof(*b)) && is_buffer(b->first) && + is_buffer(b->second); +} + +#define LIST_LEN 3 + +int foo(list_t *l, double_buffer_t *b) + // clang-format off + __CPROVER_requires(is_list(l, LIST_LEN)) + __CPROVER_requires(is_double_buffer(b)) + __CPROVER_ensures( + (2 * MIN_BUFFER_SIZE + LIST_LEN * MIN_VALUE) <= __CPROVER_return_value && + __CPROVER_return_value <= (2 * MAX_BUFFER_SIZE + LIST_LEN * MAX_VALUE)) +// clang-format on +{ + // access the assumed data structure + return l->value + l->next->value + l->next->next->value + b->first->size + + b->second->size; +} + +int main() +{ + list_t *l; + double_buffer_t *b; + int return_value = foo(l, b); +} diff --git a/regression/contracts-dfcc/memory-predicates-user-defined-requires-enforce/test.desc b/regression/contracts-dfcc/memory-predicates-user-defined-requires-enforce/test.desc new file mode 100644 index 00000000000..29de400a9ac --- /dev/null +++ b/regression/contracts-dfcc/memory-predicates-user-defined-requires-enforce/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks if user-defined memory predicates in requires clauses are succesfully +assumed when enforcing a contract. diff --git a/regression/contracts-dfcc/memory-predicates-user-defined-requires-replace/main.c b/regression/contracts-dfcc/memory-predicates-user-defined-requires-replace/main.c new file mode 100644 index 00000000000..ecdfa2a7bd4 --- /dev/null +++ b/regression/contracts-dfcc/memory-predicates-user-defined-requires-replace/main.c @@ -0,0 +1,94 @@ +#include +#include + +typedef struct list_t +{ + int value; + struct list_t *next; +} list_t; + +#define MIN_VALUE -10 +#define MAX_VALUE 10 + +bool is_list(list_t *l, size_t len) +{ + if(len == 0) + return l == NULL; + else + return __CPROVER_is_fresh(l, sizeof(*l)) && + (MIN_VALUE <= l->value && l->value <= MAX_VALUE) && + is_list(l->next, len - 1); +} + +typedef struct buffer_t +{ + size_t size; + char *arr; +} buffer_t; + +typedef struct double_buffer_t +{ + buffer_t *first; + buffer_t *second; +} double_buffer_t; + +#define MIN_BUFFER_SIZE 1 +#define MAX_BUFFER_SIZE 10 + +bool is_sized_array(char *arr, size_t size) +{ + return (MIN_BUFFER_SIZE <= size && size <= MAX_BUFFER_SIZE) && + __CPROVER_is_fresh(arr, size); +} + +bool is_buffer(buffer_t *b) +{ + return __CPROVER_is_fresh(b, sizeof(*b)) && is_sized_array(b->arr, b->size); +} + +bool is_double_buffer(double_buffer_t *b) +{ + return __CPROVER_is_fresh(b, sizeof(*b)) && is_buffer(b->first) && + is_buffer(b->second); +} + +#define LIST_LEN 3 + +int bar(list_t *l) + // clang-format off + __CPROVER_requires(is_list(l, LIST_LEN)) + __CPROVER_ensures(LIST_LEN * MIN_VALUE <= __CPROVER_return_value && + __CPROVER_return_value <= LIST_LEN * MAX_VALUE) +// clang-format on +{ + return l->value + l->next->value + l->next->next->value; +} + +int baz(double_buffer_t *b) + // clang-format off + __CPROVER_requires(is_double_buffer(b)) + __CPROVER_ensures(2 * MIN_BUFFER_SIZE <= __CPROVER_return_value && + __CPROVER_return_value <= 2 * MAX_BUFFER_SIZE) +// clang-format on +{ + return b->first->size + b->second->size; +} + +int foo(list_t *l, double_buffer_t *b) + // clang-format off + __CPROVER_requires(is_list(l, LIST_LEN)) + __CPROVER_requires(is_double_buffer(b)) + __CPROVER_ensures( + (2 * MIN_BUFFER_SIZE + LIST_LEN * MIN_VALUE) <= __CPROVER_return_value && + __CPROVER_return_value <= (2 * MAX_BUFFER_SIZE + LIST_LEN * MAX_VALUE)) +// clang-format on +{ + return bar(l) + baz(b); +} + +int main() +{ + list_t *l; + double_buffer_t *b; + int return_value = foo(l, b); +} diff --git a/regression/contracts-dfcc/memory-predicates-user-defined-requires-replace/test.desc b/regression/contracts-dfcc/memory-predicates-user-defined-requires-replace/test.desc new file mode 100644 index 00000000000..9a0a17f5855 --- /dev/null +++ b/regression/contracts-dfcc/memory-predicates-user-defined-requires-replace/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--dfcc main --enforce-contract foo --replace-call-with-contract bar --replace-call-with-contract baz _ --pointer-check +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks that user defined predicates assumed in requires clauses for checked +contracts build a state such that the same predicates used in requires clauses +for function calls replaced by their contracts hold. diff --git a/regression/contracts-dfcc/test_array_memory_enforce/main.c b/regression/contracts-dfcc/test_array_memory_enforce/main.c index 937456af0e5..1a550dd6065 100644 --- a/regression/contracts-dfcc/test_array_memory_enforce/main.c +++ b/regression/contracts-dfcc/test_array_memory_enforce/main.c @@ -2,27 +2,20 @@ bool ptr_ok(int *x) { - return (*x < 5); + return (0 < *x && *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(__CPROVER_object_from(x)) - __CPROVER_requires( - __CPROVER_is_fresh(x, sizeof(int) * 10) && - x[0] > 0 && - ptr_ok(x)) - __CPROVER_ensures( + // clang-format off +__CPROVER_assigns(__CPROVER_object_from(x)) +__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int) * 10) && ptr_ok(x)) +__CPROVER_ensures( !ptr_ok(x) && - /* x is not fresh because it was seen by the preconditions. */ - !__CPROVER_is_fresh(x, sizeof(int) * 10) && x[9] == 113 && return_ok(__CPROVER_return_value, x)) // clang-format on @@ -30,7 +23,6 @@ int foo(int *x) *x = *x + 4; x[5] = 12; x[9] = 113; - int y = *x + 5; return *x + 5; } diff --git a/regression/contracts-dfcc/test_array_memory_replace/main.c b/regression/contracts-dfcc/test_array_memory_replace/main.c index 76a7d7063ca..3097959ff5e 100644 --- a/regression/contracts-dfcc/test_array_memory_replace/main.c +++ b/regression/contracts-dfcc/test_array_memory_replace/main.c @@ -4,26 +4,20 @@ bool ptr_ok(int *x) { - return (*x < 5); + return (0 < *x && *x < 5); } bool return_ok(int ret_value, int *x) { - int a; - a = *x; - return (ret_value == (*x + 5)); + 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( + // clang-format off +__CPROVER_assigns(__CPROVER_object_from(x)) +__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int) * 10) && 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 @@ -31,16 +25,18 @@ int foo(int *x) *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); + int *x = malloc(sizeof(int) * 10); + if(ptr_ok(x)) + { + int o = foo(x); + assert(!ptr_ok(x)); + assert(x[9] == 113); + assert(return_ok(o, x)); + } return 0; } diff --git a/regression/contracts-dfcc/test_array_memory_replace/test.desc b/regression/contracts-dfcc/test_array_memory_replace/test.desc index eaa05296653..26cb949cb17 100644 --- a/regression/contracts-dfcc/test_array_memory_replace/test.desc +++ b/regression/contracts-dfcc/test_array_memory_replace/test.desc @@ -1,12 +1,9 @@ CORE main.c --dfcc main --replace-call-with-contract foo +^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ -^\[foo.precondition.\d+\] line \d+ Check requires clause of contract contract::foo for function foo: 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. +Checks whether CBMC successfully asserts __CPROVER_is_fresh for arrays. diff --git a/regression/contracts-dfcc/test_array_memory_too_small_replace/main.c b/regression/contracts-dfcc/test_array_memory_too_small_replace/main.c index 4c8cd24452e..1764fd5f345 100644 --- a/regression/contracts-dfcc/test_array_memory_too_small_replace/main.c +++ b/regression/contracts-dfcc/test_array_memory_too_small_replace/main.c @@ -4,26 +4,20 @@ bool ptr_ok(int *x) { - return (*x < 5); + return (0 < *x && *x < 5); } bool return_ok(int ret_value, int *x) { - int a; - a = *x; - return (ret_value == (*x + 5)); + 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( + // clang-format off +__CPROVER_assigns(__CPROVER_object_from(x)) +__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int) * 10) && 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 @@ -31,15 +25,18 @@ int foo(int *x) *x = *x + 4; x[5] = 12; x[9] = 113; - int y = *x + 5; - return (*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); + int *x = malloc(sizeof(int) * 9); + if(ptr_ok(x)) + { + int o = foo(x); + assert(!ptr_ok(x)); + assert(x[9] == 113); + assert(return_ok(o, x)); + } return 0; } diff --git a/regression/contracts-dfcc/test_array_memory_too_small_replace/test.desc b/regression/contracts-dfcc/test_array_memory_too_small_replace/test.desc index 69cfcf98108..01569bcc9b9 100644 --- a/regression/contracts-dfcc/test_array_memory_too_small_replace/test.desc +++ b/regression/contracts-dfcc/test_array_memory_too_small_replace/test.desc @@ -1,13 +1,12 @@ CORE main.c --dfcc main --replace-call-with-contract foo -^EXIT=10$ -^SIGNAL=0$ ^\[foo.precondition.\d+\] line \d+ Check requires clause of contract contract::foo for function foo: FAILURE$ -^\[main.assertion.\d+\] line \d+ assertion o >\= 10 \&\& o \=\= \*n \+ 5: SUCCESS$ ^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ -- -- -Checks whether CBMC successfuly assert __CPROVER_is_fresh for arrays. +Checks whether CBMC successfully 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-dfcc/test_scalar_memory_replace/main.c b/regression/contracts-dfcc/test_scalar_memory_replace/main.c index 888731fb375..87904c40bb1 100644 --- a/regression/contracts-dfcc/test_scalar_memory_replace/main.c +++ b/regression/contracts-dfcc/test_scalar_memory_replace/main.c @@ -4,38 +4,31 @@ bool ptr_ok(int *x) { - return (*x < 5); + return (0 < *x && *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 off +__CPROVER_assigns(*x) +__CPROVER_requires( __CPROVER_is_fresh(x, sizeof(int)) && ptr_ok(x)) +__CPROVER_ensures(!ptr_ok(x) && return_ok(__CPROVER_return_value, x)) // clang-format on { *x = *x + 4; return (*x + 5); } -int main() +void 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; + int *x = malloc(sizeof(int)); + assert(__CPROVER_r_ok(x, sizeof(int))); + *x = 3; + int o = foo(x); + assert(!ptr_ok(x)); + assert(return_ok(o, x)); } diff --git a/regression/contracts-dfcc/test_scalar_memory_replace/test.desc b/regression/contracts-dfcc/test_scalar_memory_replace/test.desc index 7458eeed320..dd4c533b248 100644 --- a/regression/contracts-dfcc/test_scalar_memory_replace/test.desc +++ b/regression/contracts-dfcc/test_scalar_memory_replace/test.desc @@ -1,13 +1,9 @@ CORE main.c --dfcc main --replace-call-with-contract foo +^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ -^\[foo.precondition.\d+\] line \d+ Check requires clause of contract contract::foo for function foo: 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_array_memory_replace/test.desc b/regression/contracts/test_array_memory_replace/test.desc index 8d0a65dd8df..b6c5d13435b 100644 --- a/regression/contracts/test_array_memory_replace/test.desc +++ b/regression/contracts/test_array_memory_replace/test.desc @@ -9,4 +9,4 @@ main.c ^VERIFICATION SUCCESSFUL$ -- -- -Checks whether CBMC successfuly assert __CPROVER_is_fresh for arrays. +Checks whether CBMC successfully assert __CPROVER_is_fresh for arrays. diff --git a/regression/contracts/test_array_memory_too_small_replace/test.desc b/regression/contracts/test_array_memory_too_small_replace/test.desc index c6605a85e23..fb30f3ebf7c 100644 --- a/regression/contracts/test_array_memory_too_small_replace/test.desc +++ b/regression/contracts/test_array_memory_too_small_replace/test.desc @@ -8,6 +8,6 @@ main.c ^VERIFICATION FAILED$ -- -- -Checks whether CBMC successfuly assert __CPROVER_is_fresh for arrays. +Checks whether CBMC successfully assert __CPROVER_is_fresh for arrays. Test fails because allocated array was smaller then the one required in the contract. diff --git a/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c index b8bcc009efb..cb7ad870c30 100644 --- a/src/ansi-c/library/cprover_contracts.c +++ b/src/ansi-c/library/cprover_contracts.c @@ -13,7 +13,8 @@ extern const void *__CPROVER_deallocated; extern const void *__CPROVER_new_object; extern __CPROVER_bool __CPROVER_malloc_is_new_array; int __builtin_clzll(unsigned long long); -__CPROVER_bool __VERIFIER_nondet_CPROVER_bool(); +__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); +__CPROVER_size_t __VERIFIER_nondet_size(); /// \brief A conditionally writable range of bytes. typedef struct @@ -1052,7 +1053,7 @@ __CPROVER_HIDE:; // and we attempt to free again one of the already freed pointers, // the r_ok condition above will fail, preventing us to deallocate // the same pointer twice - if((ptr != 0) & preconditions & __VERIFIER_nondet_CPROVER_bool()) + if((ptr != 0) & preconditions & __VERIFIER_nondet___CPROVER_bool()) { __CPROVER_contracts_free(ptr, 0); __CPROVER_contracts_write_set_record_deallocated(set, ptr); @@ -1190,9 +1191,14 @@ __CPROVER_HIDE:; (write_set->assert_ensures_ctx == 0), "only one context flag at a time"); #endif + // fail if size is too big + if(size >= __CPROVER_max_malloc_size) + return 0; + // pass a null write set pointer to the instrumented malloc void *ptr = __CPROVER_contracts_malloc(size, 0); *elem = ptr; + // malloc can also return a NULL pointer if failure modes are active if(!ptr) return 0; // record fresh object in the object set @@ -1219,6 +1225,9 @@ __CPROVER_HIDE:; (write_set->assert_ensures_ctx == 0), "only one context flag at a time"); #endif + // fail if size is too big + if(size >= __CPROVER_max_malloc_size) + return 0; void *ptr = __CPROVER_contracts_malloc(size, 0); *elem = ptr; if(!ptr) @@ -1446,21 +1455,13 @@ __CPROVER_HIDE:; "__CPROVER_obeys_contract is used only in requires or ensures clauses"); if((set->assume_requires_ctx == 1) | (set->assume_ensures_ctx == 1)) { - // In assumption contexts, flip a coin to decide wehter the predicate - // shall hold or not - if(__VERIFIER_nondet_CPROVER_bool()) - { - // if it must hold, assign the function pointer to the contract function - *function_pointer = contract; - return 1; - } - else - { - // if it must not hold do not modify the pointer value - // function_pointer will keep whatever bit pattern and value set it had - // before evaluating the predicate + // decide if predicate must hold + if(__VERIFIER_nondet___CPROVER_bool()) return 0; - } + + // must hold, assign the function pointer to the contract function + *function_pointer = contract; + return 1; } else { diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index 640a1a2e3e1..bdc1bbdcc05 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -22,6 +22,7 @@ SRC = accelerate/accelerate.cpp \ contracts/dynamic-frames/dfcc_is_fresh.cpp \ contracts/dynamic-frames/dfcc_is_freeable.cpp \ contracts/dynamic-frames/dfcc_obeys_contract.cpp \ + contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp \ contracts/dynamic-frames/dfcc_instrument.cpp \ contracts/dynamic-frames/dfcc_spec_functions.cpp \ contracts/dynamic-frames/dfcc_contract_functions.cpp \ diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md index aa4eb074557..0b05529d44b 100644 --- a/src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md +++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md @@ -28,6 +28,7 @@ Each of these translation passes is implemented in a specific class: :-------------------------------|:--------------------------------------- @ref dfcc_instrumentt | Implements @ref contracts-dev-spec-dfcc for @ref goto_functiont, @ref goto_programt, or subsequences of instructions of @ref goto_programt @ref dfcc_is_fresht | Implements @ref contracts-dev-spec-is-fresh + @ref dfcc_lift_memory_predicatest | Implements @ref contracts-dev-spec-memory-predicates-rewriting @ref dfcc_is_freeablet | Implements @ref contracts-dev-spec-is-freeable @ref dfcc_obeys_contractt | Implements @ref contracts-dev-spec-obeys-contract @ref dfcc_spec_functionst | Implements @ref contracts-dev-spec-spec-rewriting diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-instrument.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-instrument.md index 333b954ce6d..578b4d7bd7d 100644 --- a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-instrument.md +++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-instrument.md @@ -162,10 +162,14 @@ skip_target: SKIP; CALL __CPROVER_deallocate(ptr); ``` -Calls to `__CPROVER_was_freed` or `__CPROVER_is_freeable` are rewritten as described -in @subpage contracts-dev-spec-is-freeable +Calls to `__CPROVER_was_freed` or `__CPROVER_is_freeable` are rewritten as +described in @subpage contracts-dev-spec-is-freeable -Calls to `__CPROVER_is_fresh` are rewritten as described in @subpage contracts-dev-spec-is-fresh +Calls to `__CPROVER_is_fresh` are rewritten as described in +@subpage contracts-dev-spec-is-fresh + +Calls to `__CPROVER_obeys_contract` are rewritten as described in +@subpage contracts-dev-spec-obeys-contract Calls to `__CPROVER_obeys_contract` are rewritten as described in @subpage contracts-dev-spec-obeys-contract diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-memory-predicates-rewriting.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-memory-predicates-rewriting.md new file mode 100644 index 00000000000..2d570183901 --- /dev/null +++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-memory-predicates-rewriting.md @@ -0,0 +1,192 @@ +# Rewriting User-Defined Memory Predicates {#contracts-dev-spec-memory-predicates-rewriting} + +Back to top @ref contracts-dev-spec + +@tableofcontents + +The C extensions for contract specification provide three pointer-related memory +predicates: + +```c +// Holds iff ptr is pointing to an object distinct to all objects pointed to by +// other __CPROVER_is_fresh occurrences in the contract's pre and post conditions +__CPROVER_bool __CPROVER_is_fresh(void *ptr, size_t size); + +// Holds iff the function pointer \p fptr points to a function satisfying +// \p contract. +__CPROVER_bool __CPROVER_obeys_contract(void (*fptr)(void), void (*contract)(void)); +``` + +Users are free to call these predicates from requires and ensures clauses. +Users can also define their own functions in terms of these predicates, and call +them from requires and ensures clauses, but not from the program under analysis. + +For instance, one could write a predicate defining linked lists of at most `len` +elements as follows: + +```c +typedef struct list_t +{ + int value; + struct list_t *next; +} list_t; + +// true iff list of len nodes with values in [-10,10] +bool is_list(list_t *l, size_t len) +{ + if(len == 0) + return l == NULL; + else + return __CPROVER_is_fresh(l, sizeof(*l)) && -10 <= l->value && + l->value <= 10 && is_list(l->next, len - 1); +} +``` + +One can also simply describe finite nested structures: + +```c +typedef struct buffer_t +{ + size_t size; + char *arr; + char *cursor; +} buffer_t; + +typedef struct double_buffer_t +{ + buffer_t *first; + buffer_t *second; +} double_buffer_t; + +bool is_sized_array(char *arr, size_t size) +{ + return __CPROVER_is_fresh(arr, size); +} + +bool is_buffer(buffer_t *b) +{ + return __CPROVER_is_fresh(b, sizeof(*b)) && (0 < b->size && b->size <= 10) && + is_sized_array(b->arr, b->size); +} + +bool is_double_buffer(double_buffer_t *b) +{ + return __CPROVER_is_fresh(b, sizeof(*b)) && is_buffer(b->first) && + is_buffer(b->second); +} +``` + +By rewriting such user-defined predicate we achieve two things: +1. in assumption contexts, evaluating the predicate allocates the data stucture + specified by the predicate; +2. in assertion contexts, evaluating the predicate checks that a given pointer + satisfies the predicate definition; + +To achieve point 1., we apply an instrumentation pass to transform the +user-defined functions into functions that take their pointer arguments by +reference instead of by value, so that enforcing the assumption described by the +predicate can be done by updating the pointer in place using a side effect. + +## Collecting user-defined memory predicates {#contracts-dev-spec-memory-predicate-collect} + +We first run a pass that collects all user-defined functions that are defined +in terms of one of the three core memory predicates using this fixpoint +algorithm: + +``` +predicates = {}; +updated = true; +while(updated) +{ + updated = false; + for(function : goto_model.goto_functions.function_map) + { + if(!predicates.contains(function) && + (calls_core_predicate(function) || + calls_one_of(function, predicates))) + { + predicates.insert(function); + updated = true; + } + } +} +``` + +## Rewriting user-defined memory predicates {#contracts-dev-spec-memory-predicate-rewrite} + +We only support sets of predicates that are non-recursive or self-recursive +(i.e. predicates that call themselves directly). +We build a graph representing the P-calls-Q relation, omitting edges for +self-recursion, and try to sort it topologically. If the sort succeeds we +rewrite the predicates in topological order, so that when instrumenting P any +other predicate Q it calls is already instrumented and we know which parameters +of Q have been lifted. If the topological sort fails, then it means the predicate +are mutually recursive and we abort instrumentation. + +Rewriting a user-defined memory predicate P consists in: +- Identifying the subset of parameters of P which get passed to a core predicate + or a user-defined predicate in a lifted position; +- In the signature of P, lift all such parameters to pointer-to-pointer types; +- In the body of P, rewrite all occurences of a lifted parameter `p` into `*p` + (this brings back type coherence in the body of P); +- For calls to memory predicates Q, add an `address_of` operator to arguments + passed on a lifted parameter of Q; + +Once these transformations are applied, the body of the predicate is well typed +and the predicate now takes the pointers on which it operates by reference +instead of by value. By doing so, the P gains the capability to update in place +the memory location hold the pointer value subject to the predicate definition. + +The last step of the rewriting is to apply the normal DFCC instrumentation +which adds a write set parameter to the function, instruments it for side +effect checking, and maps core memory predicates to their implementations. + +On our previous list example, this yields the following result: + +```c +bool is_list(list_t **l, size_t len, + __CPROVER_contracts_write_set_ptr_t write_set) +{ + if(len == 0) + return (*l) == NULL; + else + return __CPROVER_contracts_is_fresh(&(*l), sizeof(*(*l)), write_set) && + -10 <= (*l)->value && (*l)->value <= 10 && + is_list(&((*l)->next), len-1, write_set); +} +``` + +On the nested structs example, it gives the following result: + +```c +bool is_sized_array(char **arr, size_t size, + __CPROVER_contracts_write_set_ptr_t write_set) +{ + return __CPROVER_contracts_is_fresh(&(*arr), size, write_set); +} + +bool is_buffer(buffer_t **b, + __CPROVER_contracts_write_set_ptr_t write_set) +{ + return __CPROVER_contracts_is_fresh(&(*b), sizeof(*(*b)), write_set) && + (0 < (*b)->size && (*b)->size <= 10) && + is_sized_array(&(*b)->arr, (*b)->size, write_set); +} + +bool is_double_buffer(double_buffer_t **b, + __CPROVER_contracts_write_set_ptr_t write_set) +{ + return __CPROVER_contracts_is_fresh(&(*b), sizeof(*(*b)), write_set) && + is_buffer(&((*b)->first), write_set) && + is_buffer(&((*b)->second), write_set); +} +``` + +The write_set parameter carries assumption/assertion context flags, so that the +implementation of the core-predicates know when to update the pointers in place +using malloc and assignments to make the predicates hold. + +--- + Prev | Next +:-----|:------ + @ref contracts-dev-spec-spec-rewriting | @ref contracts-dev-spec-dfcc \ No newline at end of file diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-spec-rewriting.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-spec-rewriting.md index afc11386e11..92e429b33b3 100644 --- a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-spec-rewriting.md +++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-spec-rewriting.md @@ -215,4 +215,4 @@ void foo( --- Prev | Next :-----|:------ - @ref contracts-dev-spec-spec-rewriting | @ref contracts-dev-spec-dfcc \ No newline at end of file + @ref contracts-dev-spec-codegen | @ref contracts-dev-spec-memory-predicates-rewriting \ No newline at end of file diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec.md index f70e74221ee..2d0c321f09a 100644 --- a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec.md +++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec.md @@ -9,6 +9,7 @@ sections: 2. @subpage contracts-dev-spec-transform-params 3. @subpage contracts-dev-spec-codegen 4. @subpage contracts-dev-spec-spec-rewriting +4. @subpage contracts-dev-spec-memory-predicates-rewriting 5. @subpage contracts-dev-spec-dfcc 6. @subpage contracts-dev-spec-harness 7. @subpage contracts-dev-spec-contract-checking diff --git a/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md b/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md index 0cce76ee7fd..b04dccb3e5f 100644 --- a/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md +++ b/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md @@ -120,6 +120,94 @@ int foo() } ``` +## User defined memory predicates + +Users can write their own memory predicates based on the core predicates described above. +`__CPROVER_is_fresh` allows to specify pointer validity and separation. +For instance, one could write a predicate defining linked lists of at most `len` +elements as follows: + +```c +typedef struct list_t +{ + int value; + struct list_t *next; +} list_t; + +// true iff list of len nodes with values in [-10,10] +bool is_list(list_t *l, size_t len) +{ + if(len == 0) + return l == NULL; + else + return __CPROVER_is_fresh(l, sizeof(*l)) && -10 <= l->value && + l->value <= 10 && is_list(l->next, len - 1); +} +``` + +One can also simply describe finite nested structures: + +```c +typedef struct buffer_t +{ + size_t size; + char *arr; + char *cursor; +} buffer_t; + +typedef struct double_buffer_t +{ + buffer_t *first; + buffer_t *second; +} double_buffer_t; + +bool is_sized_array(char *arr, size_t size) +{ + return __CPROVER_is_fresh(arr, size); +} + +bool is_buffer(buffer_t *b) +{ + return __CPROVER_is_fresh(b, sizeof(*b)) && (0 < b->size && b->size <= 10) && + is_sized_array(b->arr, b->size) && +} + +bool is_double_buffer(double_buffer_t *b) +{ + return __CPROVER_is_fresh(b, sizeof(*b)) && is_buffer(b->first) && + is_buffer(b->second); +} +``` + +And one can then use these predicates in requires or ensures clauses for function +contracts. + +```c +int foo(list_t *l, double_buffer_t *b) + // clang-format off + __CPROVER_requires(is_list(l, 3)) + __CPROVER_requires(is_double_buffer(b)) + __CPROVER_ensures(-28 <= __CPROVER_return_value && + __CPROVER_return_value <= 50) +// clang-format on +{ + // access the assumed data structure + return l->value + l->next->value + l->next->next->value + b->first->size + + b->second->size; +} +``` + +### Limitations + +The main limitation with user defined predicates are: +- their evaluation must terminate; +- self-recursive predicates are supported, but mutually recursive predicates are + not supported for the moment. + +For instance, in the `is_list` example above, recursion is bounded by the use of +the explicit `len` parameter. The `is_double_buffer` predicate also describes +a bounded structure. + ## Additional Resources - @ref contracts-functions diff --git a/src/goto-instrument/contracts/doc/user/contracts-user.md b/src/goto-instrument/contracts/doc/user/contracts-user.md index 7c335835274..041a660b69b 100644 --- a/src/goto-instrument/contracts/doc/user/contracts-user.md +++ b/src/goto-instrument/contracts/doc/user/contracts-user.md @@ -11,6 +11,7 @@ The individual types of clauses for contracts are documented here: - @subpage contracts-loop-invariants - @subpage contracts-decreases - @subpage contracts-memory-predicates +- @subpage contracts-function-pointer-predicates - @subpage contracts-history-variables - @subpage contracts-quantifiers - @subpage contracts-user-cli diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp index 99c0b2e4872..4a2307809bf 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp @@ -45,6 +45,8 @@ Author: Remi Delmas, delmarsd@amazon.com #include #include +#include "dfcc_lift_memory_predicates.h" + void dfcc( const optionst &options, goto_modelt &goto_model, @@ -122,6 +124,7 @@ dfcct::dfcct( library(goto_model, utils, message_handler), ns(goto_model.symbol_table), instrument(goto_model, message_handler, utils, library), + memory_predicates(goto_model, utils, library, instrument, message_handler), spec_functions(goto_model, message_handler, utils, library, instrument), contract_handler( goto_model, @@ -129,6 +132,7 @@ dfcct::dfcct( utils, library, instrument, + memory_predicates, spec_functions), swap_and_wrap( goto_model, @@ -269,6 +273,18 @@ void dfcct::instrument_harness_function() other_symbols.erase(harness_id); } +void dfcct::lift_memory_predicates() +{ + std::set predicates = + memory_predicates.lift_predicates(function_pointer_contracts); + for(const auto &predicate : predicates) + { + log.debug() << "Memory predicate" << predicate << messaget::eom; + if(other_symbols.find(predicate) != other_symbols.end()) + other_symbols.erase(predicate); + } +} + void dfcct::wrap_checked_function() { // swap-and-wrap checked functions with contracts @@ -415,6 +431,7 @@ void dfcct::transform_goto_model() { check_transform_goto_model_preconditions(); link_model_and_load_dfcc_library(); + lift_memory_predicates(); instrument_harness_function(); wrap_checked_function(); wrap_replaced_functions(); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc.h b/src/goto-instrument/contracts/dynamic-frames/dfcc.h index 2e8521de6dc..fa0d04f67e4 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc.h @@ -35,6 +35,7 @@ Author: Remi Delmas, delmasrd@amazon.com #include "dfcc_contract_handler.h" #include "dfcc_instrument.h" #include "dfcc_library.h" +#include "dfcc_lift_memory_predicates.h" #include "dfcc_spec_functions.h" #include "dfcc_swap_and_wrap.h" #include "dfcc_utils.h" @@ -198,6 +199,7 @@ class dfcct dfcc_libraryt library; namespacet ns; dfcc_instrumentt instrument; + dfcc_lift_memory_predicatest memory_predicates; dfcc_spec_functionst spec_functions; dfcc_contract_handlert contract_handler; dfcc_swap_and_wrapt swap_and_wrap; @@ -235,6 +237,7 @@ class dfcct void link_model_and_load_dfcc_library(); void instrument_harness_function(); + void lift_memory_predicates(); void wrap_checked_function(); void wrap_replaced_functions(); void wrap_discovered_function_pointer_contracts(); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp index 1ff9513847d..9d45026fcc2 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp @@ -12,7 +12,6 @@ Date: August 2022 #include #include #include -// #include #include #include #include @@ -44,6 +43,7 @@ dfcc_contract_handlert::dfcc_contract_handlert( dfcc_utilst &utils, dfcc_libraryt &library, dfcc_instrumentt &instrument, + dfcc_lift_memory_predicatest &memory_predicates, dfcc_spec_functionst &spec_functions) : goto_model(goto_model), message_handler(message_handler), @@ -51,6 +51,7 @@ dfcc_contract_handlert::dfcc_contract_handlert( utils(utils), library(library), instrument(instrument), + memory_predicates(memory_predicates), spec_functions(spec_functions), ns(goto_model.symbol_table) { @@ -104,7 +105,8 @@ void dfcc_contract_handlert::add_contract_instructions( message_handler, utils, library, - instrument) + instrument, + memory_predicates) .add_to_dest(dest, function_pointer_contracts); } diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h index 11bcae93fe3..2cfdc28aabf 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h @@ -29,6 +29,7 @@ class message_handlert; class dfcc_libraryt; class dfcc_utilst; class dfcc_instrumentt; +class dfcc_lift_memory_predicatest; class dfcc_spec_functionst; class code_with_contract_typet; class conditional_target_group_exprt; @@ -70,6 +71,7 @@ class dfcc_contract_handlert dfcc_utilst &utils, dfcc_libraryt &library, dfcc_instrumentt &instrument, + dfcc_lift_memory_predicatest &memory_predicates, dfcc_spec_functionst &spec_functions); /// Adds instructions in `dest` modeling contract checking, assuming @@ -119,6 +121,7 @@ class dfcc_contract_handlert dfcc_utilst &utils; dfcc_libraryt &library; dfcc_instrumentt &instrument; + dfcc_lift_memory_predicatest &memory_predicates; dfcc_spec_functionst &spec_functions; namespacet ns; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp new file mode 100644 index 00000000000..8a3f8ea1486 --- /dev/null +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp @@ -0,0 +1,419 @@ +/*******************************************************************\ + +Module: Dynamic frame condition checking for function contracts + +Author: Remi Delmas, delmasrd@amazon.com +Date: August 2022 + +\*******************************************************************/ + +#include "dfcc_lift_memory_predicates.h" + +#include +#include +#include +#include +#include +#include + +#include + +#include "dfcc_instrument.h" +#include "dfcc_library.h" +#include "dfcc_utils.h" + +dfcc_lift_memory_predicatest::dfcc_lift_memory_predicatest( + goto_modelt &goto_model, + dfcc_utilst &utils, + dfcc_libraryt &library, + dfcc_instrumentt &instrument, + message_handlert &message_handler) + : goto_model(goto_model), + utils(utils), + library(library), + instrument(instrument), + log(message_handler) +{ +} + +/// True if a function had at least one of its parameters lifted +bool dfcc_lift_memory_predicatest::is_lifted_function( + const irep_idt &function_id) +{ + return lifted_parameters.find(function_id) != lifted_parameters.end(); +} + +/// True iff function_id is a core memory predicate +static bool is_core_memory_predicate(const irep_idt &function_id) +{ + return (function_id == CPROVER_PREFIX "is_fresh") || + (function_id == CPROVER_PREFIX "obeys_contract"); +} + +bool dfcc_lift_memory_predicatest::calls_memory_predicates( + const goto_programt &goto_program, + const std::set &predicates) +{ + for(const auto &instruction : goto_program.instructions) + { + if( + instruction.is_function_call() && + instruction.call_function().id() == ID_symbol) + { + const auto &callee_id = + to_symbol_expr(instruction.call_function()).get_identifier(); + + if( + is_core_memory_predicate(callee_id) || + predicates.find(callee_id) != predicates.end()) + { + return true; + } + } + } + return false; +} + +std::set dfcc_lift_memory_predicatest::lift_predicates( + std::set &discovered_function_pointer_contracts) +{ + std::set candidates; + for(const auto &pair : goto_model.symbol_table) + { + if( + pair.second.type.id() == ID_code && + !instrument.do_not_instrument(pair.first)) + { + const auto &iter = + goto_model.goto_functions.function_map.find(pair.first); + if( + iter != goto_model.goto_functions.function_map.end() && + iter->second.body_available()) + { + candidates.insert(pair.first); + } + } + } + + std::set predicates; + + // iterate until no new predicate is found + bool new_predicates_found = true; + while(new_predicates_found) + { + new_predicates_found = false; + for(const auto &function_id : candidates) + { + if( + predicates.find(function_id) == predicates.end() && + calls_memory_predicates( + goto_model.goto_functions.function_map[function_id].body, predicates)) + { + predicates.insert(function_id); + new_predicates_found = true; + } + } + } + + if(predicates.empty()) + return predicates; + + // some predicates were found, build dependency graph + struct dep_graph_nodet : public graph_nodet + { + const irep_idt &function_id; + explicit dep_graph_nodet(const irep_idt &function_id) + : function_id(function_id) + { + } + }; + + grapht dep_graph; + + // inverse mapping from names to dep_graph_nodet identifiers + std::map id_to_node_map; + // create all nodes + for(auto &predicate : predicates) + { + id_to_node_map.insert({predicate, dep_graph.add_node(predicate)}); + } + + // create all edges + for(auto &caller : predicates) + { + const auto caller_id = id_to_node_map[caller]; + for(const auto &instruction : + goto_model.goto_functions.function_map[caller].body.instructions) + { + if( + instruction.is_function_call() && + instruction.call_function().id() == ID_symbol) + { + const auto &callee = + to_symbol_expr(instruction.call_function()).get_identifier(); + if(predicates.find(callee) != predicates.end()) + { + log.conditional_output(log.debug(), [&](messaget::mstreamt &mstream) { + mstream << "Memory predicate dependency " << caller << " -> " + << callee << messaget::eom; + }); + const auto callee_id = id_to_node_map[callee]; + if(callee != caller) // do not add edges for self-recursive functions + dep_graph.add_edge(callee_id, caller_id); + } + } + } + } + + // lift in dependency order + auto sorted = dep_graph.topsort(); + PRECONDITION_WITH_DIAGNOSTICS( + !sorted.empty(), + "could not determine instrumentation order for memory predicates, most " + "likely due to mutual recursion"); + for(const auto &idx : sorted) + { + lift_predicate( + dep_graph[idx].function_id, discovered_function_pointer_contracts); + } + + return predicates; +} + +// returns an optional rank +static optionalt is_param_expr( + const exprt &expr, + const std::map ¶meter_rank) +{ + if(expr.id() == ID_typecast) + { + // ignore typecasts + return is_param_expr(to_typecast_expr(expr).op(), parameter_rank); + } + else if(expr.id() == ID_symbol) + { + const irep_idt &ident = to_symbol_expr(expr).get_identifier(); + const auto found = parameter_rank.find(ident); + if(found != parameter_rank.end()) + { + return {found->second}; + } + else + { + return {}; + } + } + else + { + // bail on anything else + return {}; + } +} + +void dfcc_lift_memory_predicatest::collect_parameters_to_lift( + const irep_idt &function_id) +{ + const symbolt &function_symbol = utils.get_function_symbol(function_id); + // map of parameter name to its rank in the signature + std::map parameter_rank; + const auto ¶meters = to_code_type(function_symbol.type).parameters(); + for(std::size_t rank = 0; rank < parameters.size(); rank++) + { + parameter_rank[parameters[rank].get_identifier()] = rank; + } + const goto_programt &body = + goto_model.goto_functions.function_map[function_id].body; + for(const auto &it : body.instructions) + { + // for all function calls, if a parameter of function_id is passed + // in a lifted position, add its rank to the set of lifted parameters + if(it.is_function_call() && it.call_function().id() == ID_symbol) + { + const irep_idt &callee_id = + to_symbol_expr(it.call_function()).get_identifier(); + if(callee_id == CPROVER_PREFIX "is_fresh") + { + auto opt_rank = is_param_expr(it.call_arguments()[0], parameter_rank); + if(opt_rank.has_value()) + { + lifted_parameters[function_id].insert(opt_rank.value()); + } + } + else if(callee_id == CPROVER_PREFIX "obeys_contract") + { + auto opt_rank = is_param_expr(it.call_arguments()[0], parameter_rank); + if(opt_rank.has_value()) + { + lifted_parameters[function_id].insert(opt_rank.value()); + } + } + else if(is_lifted_function(callee_id)) + { + // search wether a parameter of function_id is passed to a lifted + // parameter of callee_id + for(const std::size_t callee_rank : lifted_parameters[callee_id]) + { + auto opt_rank = + is_param_expr(it.call_arguments()[callee_rank], parameter_rank); + if(opt_rank.has_value()) + { + lifted_parameters[function_id].insert(opt_rank.value()); + } + } + } + } + } +} + +void dfcc_lift_memory_predicatest::add_pointer_type( + const irep_idt &function_id, + const std::size_t parameter_rank, + replace_symbolt &replace_lifted_param) +{ + symbolt &function_symbol = utils.get_function_symbol(function_id); + code_typet &code_type = to_code_type(function_symbol.type); + auto ¶meters = code_type.parameters(); + auto ¶meter_id = parameters[parameter_rank].get_identifier(); + auto entry = goto_model.symbol_table.symbols.find(parameter_id); + log.conditional_output(log.debug(), [&](messaget::mstreamt &mstream) { + mstream << "adding pointer type to " << function_id << " " << parameter_id + << messaget::eom; + }); + const symbolt &old_symbol = entry->second; + const auto &old_symbol_expr = old_symbol.symbol_expr(); + // create new parameter symbol, same everything except type + symbolt new_symbol( + old_symbol.name, pointer_type(old_symbol.type), old_symbol.mode); + new_symbol.base_name = old_symbol.base_name; + new_symbol.location = old_symbol.location; + new_symbol.module = old_symbol.module; + new_symbol.is_lvalue = old_symbol.is_lvalue; + new_symbol.is_state_var = old_symbol.is_state_var; + new_symbol.is_thread_local = old_symbol.is_thread_local; + new_symbol.is_file_local = old_symbol.is_file_local; + new_symbol.is_auxiliary = old_symbol.is_auxiliary; + new_symbol.is_parameter = old_symbol.is_parameter; + goto_model.symbol_table.erase(entry); + std::pair res = + goto_model.symbol_table.insert(std::move(new_symbol)); + CHECK_RETURN(res.second); + replace_lifted_param.insert( + old_symbol_expr, dereference_exprt(res.first.symbol_expr())); + code_typet::parametert parameter(res.first.type); + parameter.set_base_name(res.first.base_name); + parameter.set_identifier(res.first.name); + parameters[parameter_rank] = parameter; +} + +void dfcc_lift_memory_predicatest::lift_parameters_and_update_body( + const irep_idt &function_id, + std::set &discovered_function_pointer_contracts) +{ + replace_symbolt replace_lifted_params; + // add pointer types to all parameters that require it + for(const auto rank : lifted_parameters[function_id]) + { + add_pointer_type(function_id, rank, replace_lifted_params); + } + auto &body = goto_model.goto_functions.function_map[function_id].body; + // update the function body + for(auto &instruction : body.instructions) + { + // rewrite all occurrences of lifted parameters + instruction.transform([&replace_lifted_params](exprt expr) { + const bool changed = !replace_lifted_params.replace(expr); + return changed ? optionalt{expr} : nullopt; + }); + + // add address-of to all arguments expressions passed in lifted position to + // another memory predicate + if( + instruction.is_function_call() && + instruction.call_function().id() == ID_symbol) + { + // add address-of to arguments that are passed in lifted position + auto &callee_id = + to_symbol_expr(instruction.call_function()).get_identifier(); + if(is_lifted_function(callee_id)) + { + for(const auto &rank : lifted_parameters[callee_id]) + { + const auto arg = instruction.call_arguments()[rank]; + log.conditional_output(log.debug(), [&](messaget::mstreamt &mstream) { + mstream << "Adding address_of to call " << callee_id + << ", argument " << format(arg) << messaget::eom; + }); + instruction.call_arguments()[rank] = address_of_exprt(arg); + } + } + } + } + for(auto instruction : body.instructions) + { + instruction.output(log.debug()); + } +} + +void dfcc_lift_memory_predicatest::lift_predicate( + const irep_idt &function_id, + std::set &discovered_function_pointer_contracts) +{ + // when this function_id gets processed, any memory predicate it calls has + // already been processed (except itself if it is recursive); + + log.status() << "Instrumenting memory predicate '" << function_id << "'" + << messaget::eom; + + // first step: identify which parameters are passed directly to core + // predicates of lifted positions in user-defined memory predicates and mark + // them as lifted + collect_parameters_to_lift(function_id); + lift_parameters_and_update_body( + function_id, discovered_function_pointer_contracts); + + log.conditional_output(log.debug(), [&](messaget::mstreamt &mstream) { + mstream << "Ranks of lifted parameters for " << function_id << ": "; + for(const auto rank : lifted_parameters[function_id]) + mstream << rank << ", "; + mstream << messaget::eom; + }); + + // instrument the function for side effects: adds the write_set parameter, + // adds checks for side effects, maps core predicates to their implementation. + instrument.instrument_function( + function_id, discovered_function_pointer_contracts); +} + +void dfcc_lift_memory_predicatest::fix_calls(goto_programt &program) +{ + fix_calls(program, program.instructions.begin(), program.instructions.end()); +} + +void dfcc_lift_memory_predicatest::fix_calls( + goto_programt &program, + goto_programt::targett first_instruction, + const goto_programt::targett &last_instruction) +{ + for(auto target = first_instruction; target != last_instruction; target++) + { + if(target->is_function_call()) + { + const auto &function = target->call_function(); + + if(function.id() == ID_symbol) + { + const irep_idt &fun_name = to_symbol_expr(function).get_identifier(); + + if(is_lifted_function(fun_name)) + { + // add address-of on all lifted argumnents + for(const auto rank : lifted_parameters[fun_name]) + { + target->call_arguments()[rank] = + address_of_exprt(target->call_arguments()[rank]); + } + } + } + } + } +} diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.h new file mode 100644 index 00000000000..e18cfab729a --- /dev/null +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.h @@ -0,0 +1,113 @@ +/*******************************************************************\ + +Module: Dynamic frame condition checking for function contracts + +Author: Remi Delmas, delmasrd@amazon.com +Date: November 2022 + +\*******************************************************************/ + +/// \file +/// Collects all user-defined predicates that call functions +/// is_fresh, pointer_in_range, obeys_contract and lifts them to function taking +/// pointers by reference. When called in assumption contexts, +/// These user-defined predicates update the pointers using side effect in order +/// to make the assumptions described by the predicate hold. +/// In assertion contexts, they behave like the original user-defined predicate +/// i.e. without side effects. + +#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LIFT_MEMORY_PREDICATES_H +#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LIFT_MEMORY_PREDICATES_H + +#include + +#include + +#include +#include + +class dfcc_utilst; +class dfcc_libraryt; +class dfcc_instrumentt; +class message_handlert; +class goto_modelt; +class exprt; +class replace_symbolt; + +class dfcc_lift_memory_predicatest +{ +public: + /// \param goto_model The goto model to process + /// \param utils Utility methods + /// \param library The contracts instrumentation library + /// \param instrument The DFCC instrumenter object + /// \param message_handler Used for messages + dfcc_lift_memory_predicatest( + goto_modelt &goto_model, + dfcc_utilst &utils, + dfcc_libraryt &library, + dfcc_instrumentt &instrument, + message_handlert &message_handler); + + /// \brief Collects and lifts all user-defined memory predicates. + /// \param[out] discovered_function_pointer_contracts Set of function pointer + /// contracts discovered during instrumentation + /// \return The set of predicates that were lifted + std::set + lift_predicates(std::set &discovered_function_pointer_contracts); + + /// Fixes calls to user-defined memory predicates in the given program, + /// by adding an address-of to arguments passed in lifted position. + void fix_calls(goto_programt &program); + + /// Fixes calls to user-defined memory predicates in the given program, + /// by adding an address-of to arguments passed in lifted position, between + /// first_instruction (included) and last_instruction (excluded). + void fix_calls( + goto_programt &program, + goto_programt::targett first_instruction, + const goto_programt::targett &last_instruction); + +protected: + goto_modelt &goto_model; + dfcc_utilst &utils; + dfcc_libraryt &library; + dfcc_instrumentt &instrument; + messaget log; + // index of lifted parameters for lifted functions + std::map> lifted_parameters; + + /// \brief Returns true iff \p goto_program calls core memory predicates. + /// or one of the functions found in \p predicates . + bool calls_memory_predicates( + const goto_programt &goto_program, + const std::set &predicates); + + void lift_predicate( + const irep_idt &function_id, + std::set &discovered_function_pointer_contracts); + + void lift_parameters_and_update_body( + const irep_idt &function_id, + std::set &discovered_function_pointer_contracts); + + /// \brief adds a pointer_type to the parameter of a function + /// \param function_id The function to update + /// \param parameter_rank The parameter to update + /// \param replace_lifted_param Symbol replacer (receives `p ~> *p` mappings) + /// The parameter symbol gets updated in the symbol table and the function + /// signature gets updated with the new type. + void add_pointer_type( + const irep_idt &function_id, + const std::size_t parameter_rank, + replace_symbolt &replace_lifted_param); + + /// \brief Computes the subset of function parameters of function_id + /// that are passed directly to core predicates and must be lifted. + void collect_parameters_to_lift(const irep_idt &function_id); + + /// \brief True if a function at least had one of its parameters lifted + bool is_lifted_function(const irep_idt &function_id); +}; + +#endif diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp index 6f832be6ccf..ea6288a162a 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp @@ -35,73 +35,6 @@ dfcc_spec_functionst::dfcc_spec_functionst( { } -std::set dfcc_spec_functionst::collect_spec_assigns_functions( - const std::vector &candidates) -{ - const std::set functions = { - CPROVER_PREFIX "assignable", - CPROVER_PREFIX "object_whole", - CPROVER_PREFIX "object_from", - CPROVER_PREFIX "object_upto"}; - std::set dest; - collect_functions_that_call(candidates, functions, dest); - return dest; -} - -std::set dfcc_spec_functionst::collect_spec_frees_functions( - const std::vector &candidates) -{ - std::set dest; - const std::set functions = {CPROVER_PREFIX "freeable"}; - collect_functions_that_call(candidates, functions, dest); - return dest; -} - -void dfcc_spec_functionst::collect_functions_that_call( - const std::vector &candidates, - const std::set &functions, - std::set &dest) -{ - bool changed = true; - while(changed) - { - changed = false; - for(const auto &function_id : candidates) - { - const auto &it = goto_model.goto_functions.function_map.find(function_id); - if(dest.find(function_id) == dest.end() && it->second.body_available()) - { - changed |= - insert_if_calls(function_id, it->second.body, functions, dest); - } - } - } -} - -bool dfcc_spec_functionst::insert_if_calls( - const irep_idt &function_id, - const goto_programt &goto_program, - const std::set &functions, - std::set &dest) -{ - PRECONDITION(dest.find(function_id) == dest.end()); - bool insert = false; - for(const auto &it : goto_program.instructions) - { - if(it.is_function_call() && it.call_function().id() == ID_symbol) - { - const irep_idt &called_function = - to_symbol_expr(it.call_function()).get_identifier(); - - insert = functions.find(called_function) != functions.end() || - dest.find(called_function) != dest.end(); - } - } - if(insert) - dest.insert(function_id); - return insert; -} - const typet &dfcc_spec_functionst::get_target_type(const exprt &expr) { INVARIANT( diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h index beccd8723d7..3bb843859cb 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h @@ -133,17 +133,6 @@ class dfcc_spec_functionst void to_spec_frees_function(const irep_idt &function_id, std::size_t &nof_targets); - /// \brief Returns the subset of \p candidates that call built-ins - /// `assignable`, `object_from`, `object_upto`, `object_whole` directly or - /// indirectly. - std::set - collect_spec_assigns_functions(const std::vector &candidates); - - /// \brief Returns the subset of \p candidates that call the built-in - /// `freeable` directly or indirectly. - std::set - collect_spec_frees_functions(const std::vector &candidates); - protected: goto_modelt &goto_model; message_handlert &message_handler; @@ -157,24 +146,6 @@ class dfcc_spec_functionst /// The expression must be of the form: /// `expr = cast(address_of(target), empty*)` const typet &get_target_type(const exprt &expr); - - /// \brief Collect functions that call one of the given \p functions directly - /// or indirectly into \p dest. May miss functions if function pointers - /// calls are not already removed. - void collect_functions_that_call( - const std::vector &candidates, - const std::set &functions, - std::set &dest); - - /// \brief Adds \p function_id to \p dest if a call to a function that's - /// either in \p functions or in \p dest is found in \p goto_program. - /// \return true if \p function_id was added to \p dest, false otherwise. - /// \pre dest does not already contain \p function_id - bool insert_if_calls( - const irep_idt &function_id, - const goto_programt &goto_program, - const std::set &functions, - std::set &dest); }; #endif diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp index 46aa0654c3c..ef258745758 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp @@ -27,6 +27,7 @@ Author: Remi Delmas, delmasrd@amazon.com #include "dfcc_contract_functions.h" #include "dfcc_instrument.h" #include "dfcc_library.h" +#include "dfcc_lift_memory_predicates.h" #include "dfcc_utils.h" /// Generate the contract write set @@ -183,7 +184,8 @@ dfcc_wrapper_programt::dfcc_wrapper_programt( message_handlert &message_handler, dfcc_utilst &utils, dfcc_libraryt &library, - dfcc_instrumentt &instrument) + dfcc_instrumentt &instrument, + dfcc_lift_memory_predicatest &memory_predicates) : contract_mode(contract_mode), wrapper_symbol(wrapper_symbol), wrapped_symbol(wrapped_symbol), @@ -214,6 +216,7 @@ dfcc_wrapper_programt::dfcc_wrapper_programt( utils(utils), library(library), instrument(instrument), + memory_predicates(memory_predicates), ns(goto_model.symbol_table), converter(goto_model.symbol_table, log.get_message_handler()) { @@ -700,6 +703,9 @@ void dfcc_wrapper_programt::encode_requires_clauses() } const auto address_of_requires_write_set = addr_of_requires_write_set; + // fix calls to user-defined memory predicates + memory_predicates.fix_calls(requires_program); + // instrument for side effects instrument.instrument_goto_program( wrapper_id, @@ -766,6 +772,9 @@ void dfcc_wrapper_programt::encode_ensures_clauses() link_deallocated_contract.add( goto_programt::make_function_call(call, wrapper_sl)); + // fix calls to user-defined user-defined memory predicates + memory_predicates.fix_calls(ensures_program); + // instrument for side effects instrument.instrument_goto_program( wrapper_id, diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h index f253fc4cf34..004366dee66 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h @@ -30,6 +30,7 @@ class messaget; class message_handlert; class dfcc_instrumentt; class dfcc_libraryt; +class dfcc_lift_memory_predicatest; class dfcc_utilst; class code_with_contract_typet; class conditional_target_group_exprt; @@ -108,6 +109,9 @@ class dfcc_wrapper_programt /// \param utils utility functions for contracts transformation /// \param library the contracts instrumentation library /// \param instrument the instrumenter class for goto functions/goto programs + /// \param memory_predicates handler for user-defed memory predicates, used to + /// adjust call parameters for user defined predicates used in requires and + /// ensures clauses. dfcc_wrapper_programt( const dfcc_contract_modet contract_mode, const symbolt &wrapper_symbol, @@ -118,7 +122,8 @@ class dfcc_wrapper_programt message_handlert &message_handler, dfcc_utilst &utils, dfcc_libraryt &library, - dfcc_instrumentt &instrument); + dfcc_instrumentt &instrument, + dfcc_lift_memory_predicatest &memory_predicates); /// Adds the whole program to `dest` and the discovered function pointer /// contracts `dest_fp_contracts`. @@ -173,6 +178,7 @@ class dfcc_wrapper_programt dfcc_utilst &utils; dfcc_libraryt &library; dfcc_instrumentt &instrument; + dfcc_lift_memory_predicatest &memory_predicates; namespacet ns; goto_convertt converter; From c144993e406df1d2a143643b9c3699ec0fc3ed98 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Thu, 8 Dec 2022 15:58:26 +0000 Subject: [PATCH 2/2] CONTRACTS: support pointer_in_range_dfcc predicate Adds support for pointer_in_range_dfcc in ensures and requires clauses and user-defined predicates. This is a temporary workaround to the fact that pointer_in_range is lowered by the front-end. --- .../main.c | 42 +++++++++++ .../test.desc | 10 +++ .../main.c | 24 ++++++ .../test.desc | 10 +++ .../main.c | 25 +++++++ .../test.desc | 10 +++ .../main.c | 25 +++++++ .../test.desc | 10 +++ src/ansi-c/c_typecheck_expr.cpp | 23 ++++++ src/ansi-c/cprover_builtin_headers.h | 2 + src/ansi-c/library/cprover_contracts.c | 45 ++++++++++++ src/goto-instrument/Makefile | 1 + .../doc/developer/contracts-dev-arch.md | 1 + .../contracts-dev-spec-dfcc-instrument.md | 3 +- ...ts-dev-spec-memory-predicates-rewriting.md | 4 + .../contracts-dev-spec-pointer-in-range.md | 26 +++++++ .../doc/user/contracts-memory-predicates.md | 47 +++++++++--- .../dynamic-frames/dfcc_instrument.cpp | 10 +++ .../contracts/dynamic-frames/dfcc_library.cpp | 2 + .../contracts/dynamic-frames/dfcc_library.h | 2 + .../dfcc_lift_memory_predicates.cpp | 9 +++ .../dynamic-frames/dfcc_pointer_in_range.cpp | 73 +++++++++++++++++++ .../dynamic-frames/dfcc_pointer_in_range.h | 58 +++++++++++++++ 23 files changed, 451 insertions(+), 11 deletions(-) create mode 100644 regression/contracts-dfcc/memory-predicates-pointer-in-range-nondet/main.c create mode 100644 regression/contracts-dfcc/memory-predicates-pointer-in-range-nondet/test.desc create mode 100644 regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/main.c create mode 100644 regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/test.desc create mode 100644 regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-01/main.c create mode 100644 regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-01/test.desc create mode 100644 regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-02/main.c create mode 100644 regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-02/test.desc create mode 100644 src/goto-instrument/contracts/doc/developer/contracts-dev-spec-pointer-in-range.md create mode 100644 src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.cpp create mode 100644 src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.h diff --git a/regression/contracts-dfcc/memory-predicates-pointer-in-range-nondet/main.c b/regression/contracts-dfcc/memory-predicates-pointer-in-range-nondet/main.c new file mode 100644 index 00000000000..db7d4a60e1e --- /dev/null +++ b/regression/contracts-dfcc/memory-predicates-pointer-in-range-nondet/main.c @@ -0,0 +1,42 @@ +#include +#include + +// A vtable is a struct containing function pointers +typedef struct vtable_s +{ + int (*f)(void); +} vtable_t; + +int return_0() +{ + return 0; +} + +int return_1() +{ + return 1; +} + +// we have two possible vtables +vtable_t vtable_0 = {.f = &return_0}; +vtable_t vtable_1 = {.f = &return_1}; + +// foo takes a vtable and calls f +int foo(vtable_t *vtable) + // clang-format off +__CPROVER_requires( + // vtable is nondeterministic pointer to one of two objects + __CPROVER_pointer_in_range_dfcc(&vtable_0, vtable, &vtable_0) || + __CPROVER_pointer_in_range_dfcc(&vtable_1, vtable, &vtable_1)) +__CPROVER_ensures(__CPROVER_return_value == 0 || __CPROVER_return_value == 1) +// clang-format on +{ +CALL: + return vtable->f(); +} + +int main() +{ + vtable_t *vtable; + foo(vtable); +} diff --git a/regression/contracts-dfcc/memory-predicates-pointer-in-range-nondet/test.desc b/regression/contracts-dfcc/memory-predicates-pointer-in-range-nondet/test.desc new file mode 100644 index 00000000000..693a0ed85ea --- /dev/null +++ b/regression/contracts-dfcc/memory-predicates-pointer-in-range-nondet/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--restrict-function-pointer foo.CALL/return_0,return_1 --nondet-static-exclude vtable_0 --nondet-static-exclude vtable_1 --dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Demonstrates the use of __CPROVER_pointer_in_range_dfcc to define nondeterministic +pointers to one or more targets. diff --git a/regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/main.c b/regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/main.c new file mode 100644 index 00000000000..5acb55bedca --- /dev/null +++ b/regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/main.c @@ -0,0 +1,24 @@ +#include +#include + +void foo(char *arr, size_t size, char *cur) + // clang-format off +__CPROVER_requires( + (0 < size && size < __CPROVER_max_malloc_size) && + __CPROVER_is_fresh(arr, size) && + __CPROVER_pointer_in_range_dfcc(arr, cur, arr + size)) +__CPROVER_ensures(__CPROVER_pointer_in_range_dfcc(arr, cur, arr + size)) +// clang-format on +{ + assert(__CPROVER_r_ok(arr, size)); + assert(__CPROVER_same_object(arr, cur)); + assert(arr <= cur && cur <= arr + size); +} + +int main() +{ + char *arr; + size_t size; + char *cur; + foo(arr, size, cur); +} diff --git a/regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/test.desc b/regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/test.desc new file mode 100644 index 00000000000..a96c3616508 --- /dev/null +++ b/regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks that assuming pointer-in-range as preconditions establishes a state +in which the definition of the predicate holds. diff --git a/regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-01/main.c b/regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-01/main.c new file mode 100644 index 00000000000..8eb18cc76eb --- /dev/null +++ b/regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-01/main.c @@ -0,0 +1,25 @@ +#include +#include + +void foo(char *arr, size_t size, char *cur) + // clang-format off +__CPROVER_requires( + (0 < size && size < __CPROVER_max_malloc_size) && + __CPROVER_is_fresh(arr, size) && + __CPROVER_pointer_in_range_dfcc(arr, cur, arr + size)) +__CPROVER_ensures(__CPROVER_pointer_in_range_dfcc( + arr, cur /*, arr + size missing arg */)) +// clang-format on +{ + assert(__CPROVER_r_ok(arr, size)); + assert(__CPROVER_same_object(arr, cur)); + assert(arr <= cur && cur <= arr + size); +} + +int main() +{ + char *arr; + size_t size; + char *cur; + foo(arr, size, cur); +} diff --git a/regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-01/test.desc b/regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-01/test.desc new file mode 100644 index 00000000000..f6e9098f119 --- /dev/null +++ b/regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-01/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check +^.*error: __CPROVER_pointer_in_range_dfcc expects three arguments$ +^EXIT=(1|64)$ +^SIGNAL=0$ +^CONVERSION ERROR$ +-- +-- +Checks that badly typed occurrences of __CPROVER_pointer_in_range_dfcc are detected. diff --git a/regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-02/main.c b/regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-02/main.c new file mode 100644 index 00000000000..126f296d545 --- /dev/null +++ b/regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-02/main.c @@ -0,0 +1,25 @@ +#include +#include + +void foo(char *arr, size_t size, char *cur) + // clang-format off +__CPROVER_requires( + (0 < size && size < __CPROVER_max_malloc_size) && + __CPROVER_is_fresh(arr, size) && + __CPROVER_pointer_in_range_dfcc(arr, cur, arr + size)) +__CPROVER_ensures(__CPROVER_pointer_in_range_dfcc( + arr, cur, 2 /* wrong type arg */)) +// clang-format on +{ + assert(__CPROVER_r_ok(arr, size)); + assert(__CPROVER_same_object(arr, cur)); + assert(arr <= cur && cur <= arr + size); +} + +int main() +{ + char *arr; + size_t size; + char *cur; + foo(arr, size, cur); +} diff --git a/regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-02/test.desc b/regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-02/test.desc new file mode 100644 index 00000000000..860036ca9cd --- /dev/null +++ b/regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-02/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check +^.*error: __CPROVER_pointer_in_range_dfcc expects pointer-typed arguments$ +^EXIT=(1|64)$ +^SIGNAL=0$ +^CONVERSION ERROR$ +-- +-- +Checks that badly typed occurrences of __CPROVER_pointer_in_range_dfcc are detected. diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index f1f3e3e4253..647b6817f58 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2334,6 +2334,29 @@ exprt c_typecheck_baset::do_special_functions( // returning nil leaves the call expression in place return nil_exprt(); } + else if(identifier == CPROVER_PREFIX "pointer_in_range_dfcc") + { + // same as pointer_in_range with experimental support for DFCC contracts + // -- do not use + if(expr.arguments().size() != 3) + { + throw invalid_source_file_exceptiont{ + CPROVER_PREFIX "pointer_in_range_dfcc expects three arguments", + expr.source_location()}; + } + + for(const auto &arg : expr.arguments()) + { + if(arg.type().id() != ID_pointer) + { + throw invalid_source_file_exceptiont{ + CPROVER_PREFIX + "pointer_in_range_dfcc expects pointer-typed arguments", + arg.source_location()}; + } + } + 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 fc500a79148..184db687496 100644 --- a/src/ansi-c/cprover_builtin_headers.h +++ b/src/ansi-c/cprover_builtin_headers.h @@ -50,6 +50,8 @@ __CPROVER_bool __CPROVER_is_freeable(const void *mem); __CPROVER_bool __CPROVER_was_freed(const void *mem); __CPROVER_bool __CPROVER_is_fresh(const void *mem, __CPROVER_size_t size); __CPROVER_bool __CPROVER_obeys_contract(void (*)(void), void (*)(void)); +// same as pointer_in_range with experimental support in contracts +__CPROVER_bool __CPROVER_pointer_in_range_dfcc(void *lb, void *ptr, void *ub); void __CPROVER_old(const void *); void __CPROVER_loop_entry(const void *); diff --git a/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c index cb7ad870c30..0a8459df020 100644 --- a/src/ansi-c/library/cprover_contracts.c +++ b/src/ansi-c/library/cprover_contracts.c @@ -1292,6 +1292,51 @@ __CPROVER_HIDE:; } } +__CPROVER_bool __CPROVER_contracts_pointer_in_range_dfcc( + void *lb, + void **ptr, + void *ub, + __CPROVER_contracts_write_set_ptr_t write_set) +{ +__CPROVER_HIDE:; + __CPROVER_assert( + (write_set != 0) & ((write_set->assume_requires_ctx == 1) | + (write_set->assert_requires_ctx == 1) | + (write_set->assume_ensures_ctx == 1) | + (write_set->assert_ensures_ctx == 1)), + "__CPROVER_pointer_in_range_dfcc is used only in requires or ensures " + "clauses"); + __CPROVER_assert(__CPROVER_r_ok(lb, 0), "lb pointer must be valid"); + __CPROVER_assert(__CPROVER_r_ok(ub, 0), "ub pointer must be valid"); + __CPROVER_assert( + __CPROVER_same_object(lb, ub), + "lb and ub pointers must have the same object"); + __CPROVER_ssize_t lb_offset = __CPROVER_POINTER_OFFSET(lb); + __CPROVER_ssize_t ub_offset = __CPROVER_POINTER_OFFSET(ub); + __CPROVER_assert( + lb_offset <= ub_offset, "lb and ub pointers must be ordered"); + if(write_set->assume_requires_ctx | write_set->assume_ensures_ctx) + { + if(__VERIFIER_nondet___CPROVER_bool()) + return 0; + + // add nondet offset + __CPROVER_size_t offset = __VERIFIER_nondet_size(); + + // this cast is safe because we prove that ub and lb are ordered + __CPROVER_size_t max_offset = (__CPROVER_size_t)(ub_offset - lb_offset); + __CPROVER_assume(offset <= max_offset); + *ptr = (char *)lb + offset; + return 1; + } + else /* write_set->assert_requires_ctx | write_set->assert_ensures_ctx */ + { + __CPROVER_ssize_t offset = __CPROVER_POINTER_OFFSET(*ptr); + return __CPROVER_same_object(lb, *ptr) && lb_offset <= offset && + offset <= ub_offset; + } +} + /// \brief Returns the start address of the conditional address range found at /// index \p idx in \p set->contract_assigns. void *__CPROVER_contracts_write_set_havoc_get_assignable_target( diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index bdc1bbdcc05..bfa8ae84975 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -20,6 +20,7 @@ SRC = accelerate/accelerate.cpp \ contracts/dynamic-frames/dfcc_utils.cpp \ contracts/dynamic-frames/dfcc_library.cpp \ contracts/dynamic-frames/dfcc_is_fresh.cpp \ + contracts/dynamic-frames/dfcc_pointer_in_range.cpp \ contracts/dynamic-frames/dfcc_is_freeable.cpp \ contracts/dynamic-frames/dfcc_obeys_contract.cpp \ contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp \ diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md index 0b05529d44b..b1b5230962e 100644 --- a/src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md +++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md @@ -28,6 +28,7 @@ Each of these translation passes is implemented in a specific class: :-------------------------------|:--------------------------------------- @ref dfcc_instrumentt | Implements @ref contracts-dev-spec-dfcc for @ref goto_functiont, @ref goto_programt, or subsequences of instructions of @ref goto_programt @ref dfcc_is_fresht | Implements @ref contracts-dev-spec-is-fresh + @ref dfcc_pointer_in_ranget | Implements @ref contracts-dev-spec-pointer-in-range @ref dfcc_lift_memory_predicatest | Implements @ref contracts-dev-spec-memory-predicates-rewriting @ref dfcc_is_freeablet | Implements @ref contracts-dev-spec-is-freeable @ref dfcc_obeys_contractt | Implements @ref contracts-dev-spec-obeys-contract diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-instrument.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-instrument.md index 578b4d7bd7d..22c64d14402 100644 --- a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-instrument.md +++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-instrument.md @@ -171,7 +171,8 @@ Calls to `__CPROVER_is_fresh` are rewritten as described in Calls to `__CPROVER_obeys_contract` are rewritten as described in @subpage contracts-dev-spec-obeys-contract -Calls to `__CPROVER_obeys_contract` are rewritten as described in @subpage contracts-dev-spec-obeys-contract +Calls to `__CPROVER_pointer_in_range_dfcc` are rewritten as described in +@subpage contracts-dev-spec-pointer-in-range For all other function or function pointer calls, we proceed as follows. diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-memory-predicates-rewriting.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-memory-predicates-rewriting.md index 2d570183901..56f23746c0b 100644 --- a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-memory-predicates-rewriting.md +++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-memory-predicates-rewriting.md @@ -12,6 +12,10 @@ predicates: // other __CPROVER_is_fresh occurrences in the contract's pre and post conditions __CPROVER_bool __CPROVER_is_fresh(void *ptr, size_t size); +// Holds iff ptr is a valid pointer pointing between lb and ub pointers. +// \pre lb and ub must be valid pointers pointing in the same object. +__CPROVER_bool __CPROVER_pointer_in_range_dfcc(void *lb, void *ptr, void *ub); + // Holds iff the function pointer \p fptr points to a function satisfying // \p contract. __CPROVER_bool __CPROVER_obeys_contract(void (*fptr)(void), void (*contract)(void)); diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-pointer-in-range.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-pointer-in-range.md new file mode 100644 index 00000000000..c8f06d4a174 --- /dev/null +++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-pointer-in-range.md @@ -0,0 +1,26 @@ +# Rewriting Calls to the __CPROVER_pointer_in_range_dfcc Predicate {#contracts-dev-spec-pointer-in-range} + +Back to top @ref contracts-dev-spec + +@tableofcontents + +In goto programs encoding pre or post conditions (generated from the contract +clauses) and in all user-defined functions, we simply replace calls to +`__CPROVER_pointer_in_range_dfcc` with calls to the library implementation. + +```c +__CPROVER_pointer_in_range_dfcc( + void *lb, + void **ptr, + void *ub, + __CPROVER_contracts_write_set_ptr_t write_set); +``` + +This function implements the `__CPROVER_pointer_in_range_dfcc` behaviour in all +possible contexts (contract checking vs replacement, requires vs ensures clause +context, as described by the flags carried by the write set parameter). + +--- + Prev | Next +:-----|:------ + @ref contracts-dev | @ref contracts-dev-spec-reminder \ No newline at end of file diff --git a/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md b/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md index b04dccb3e5f..13219022147 100644 --- a/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md +++ b/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md @@ -4,29 +4,38 @@ Back to @ref contracts-user @tableofcontents -## Syntax +The built-in and user-defined predicates discussed in this section are meant to +let users describe the shape of the memory accessed through pointers in +_requires clauses_ and _ensures clauses_. Attempting to call these predicates +outside of a requires or ensures clause context will result in a verification +error. +## The __CPROVER_is_fresh predicate +### Syntax ```c bool __CPROVER_is_fresh(void *p, size_t size); ``` -To specify memory footprint we use a special function called `__CPROVER_is_fresh `. The meaning of `__CPROVER_is_fresh` is that we are borrowing a pointer from the -external environment (in a precondition), or returning it to the calling context (in a postcondition). +To specify memory footprint we use a special function called `__CPROVER_is_fresh `. +The meaning of `__CPROVER_is_fresh` is that we are borrowing a pointer from the +external environment (in a precondition), or returning it to the calling context +(in a postcondition). -### Parameters +#### Parameters `__CPROVER_is_fresh` takes two arguments: a pointer and an allocation size. The first argument is the pointer to be checked for "freshness" (i.e., not previously allocated), and the second is the expected size in bytes for the memory -available at the pointer. +available at the pointer. -### Return Value +#### Return Value It returns a `bool` value, indicating whether the pointer is fresh. -## Semantics +### Semantics -To illustrate the semantics for `__CPROVER_is_fresh`, consider the following implementation of `sum` function. +To illustrate the semantics for `__CPROVER_is_fresh`, consider the following +implementation of `sum` function. ```c int *err_signal; // Global variable @@ -45,7 +54,7 @@ __CPROVER_assigns(*out, err_signal) } ``` -### Enforcement +#### Enforcement When checking the contract abstracts a function a `__CPROVER_is_fresh` in a _requires_ clause will cause fresh memory to be allocated. @@ -74,7 +83,7 @@ int sum(const uint32_t a, const uint32_t b, uint32_t* out) } ``` -### Replacement +#### Replacement In our example, consider that a function `foo` may call `sum`. @@ -120,10 +129,28 @@ int foo() } ``` +## The __CPROVER_pointer_in_range_dfcc predicate +### Syntax + +```c +bool __CPROVER_pointer_in_range_dfcc(void *lb, void *p, void *ub); +``` + +This predicate holds if `lb`, `p` and `ub` are valid pointers within the same +object and the pointers are ordered such that `lb <= p && p <= ub` holds. + +### Semantics +In assertion contexts, the predicate checks the conditions described above. +In assumption contexts, the predicate checks that `lb` and `ub` are valid pointers +into the same object, and updates `p` using a side effect to be a non-deterministic +pointer ranging between `lb` and `ub`. + ## User defined memory predicates Users can write their own memory predicates based on the core predicates described above. `__CPROVER_is_fresh` allows to specify pointer validity and separation. +`__CPROVER_pointer_in_range` allows to specify aliasing constraints. + For instance, one could write a predicate defining linked lists of at most `len` elements as follows: diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp index 0baa04785ea..762ed33df88 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp @@ -33,6 +33,7 @@ Author: Remi Delmas, delmarsd@amazon.com #include "dfcc_is_fresh.h" #include "dfcc_library.h" #include "dfcc_obeys_contract.h" +#include "dfcc_pointer_in_range.h" #include "dfcc_utils.h" #include @@ -239,6 +240,10 @@ void dfcc_instrumentt::instrument_harness_function( auto &goto_function = goto_model.goto_functions.function_map.at(function_id); auto &body = goto_function.body; + // rewrite pointer_in_range calls + dfcc_pointer_in_ranget pointer_in_range(library, message_handler); + pointer_in_range.rewrite_calls(body, null_expr); + // rewrite is_fresh_calls dfcc_is_fresht is_fresh(library, message_handler); is_fresh.rewrite_calls(body, null_expr); @@ -425,6 +430,11 @@ void dfcc_instrumentt::instrument_instructions( const std::function &pred, std::set &function_pointer_contracts) { + // rewrite pointer_in_range calls + dfcc_pointer_in_ranget pointer_in_range(library, message_handler); + pointer_in_range.rewrite_calls( + goto_program, first_instruction, last_instruction, write_set); + // rewrite is_fresh calls dfcc_is_fresht is_fresh(library, message_handler); is_fresh.rewrite_calls( diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp index b622bcd8173..bc30d1ef9ff 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp @@ -125,6 +125,8 @@ const std::map create_dfcc_fun_to_name() {dfcc_funt::LINK_ALLOCATED, CONTRACTS_PREFIX "link_allocated"}, {dfcc_funt::LINK_DEALLOCATED, CONTRACTS_PREFIX "link_deallocated"}, {dfcc_funt::IS_FRESH, CONTRACTS_PREFIX "is_fresh"}, + {dfcc_funt::POINTER_IN_RANGE_DFCC, + CONTRACTS_PREFIX "pointer_in_range_dfcc"}, {dfcc_funt::IS_FREEABLE, CONTRACTS_PREFIX "is_freeable"}, {dfcc_funt::WAS_FREED, CONTRACTS_PREFIX "was_freed"}, {dfcc_funt::REPLACE_ENSURES_WAS_FREED_PRECONDITIONS, diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h index 0d2de64a7c4..b8ff5e5b361 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h @@ -125,6 +125,8 @@ enum class dfcc_funt LINK_DEALLOCATED, /// \see __CPROVER_contracts_is_fresh IS_FRESH, + /// \see __CPROVER_contracts_pointer_in_range_dfcc + POINTER_IN_RANGE_DFCC, /// \see __CPROVER_contracts_is_freeable IS_FREEABLE, /// \see __CPROVER_contracts_was_freed diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp index 8a3f8ea1486..0f5e05a7f9b 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp @@ -47,6 +47,7 @@ bool dfcc_lift_memory_predicatest::is_lifted_function( static bool is_core_memory_predicate(const irep_idt &function_id) { return (function_id == CPROVER_PREFIX "is_fresh") || + (function_id == CPROVER_PREFIX "pointer_in_range_dfcc") || (function_id == CPROVER_PREFIX "obeys_contract"); } @@ -239,6 +240,14 @@ void dfcc_lift_memory_predicatest::collect_parameters_to_lift( lifted_parameters[function_id].insert(opt_rank.value()); } } + else if(callee_id == CPROVER_PREFIX "pointer_in_range_dfcc") + { + auto opt_rank = is_param_expr(it.call_arguments()[1], parameter_rank); + if(opt_rank.has_value()) + { + lifted_parameters[function_id].insert(opt_rank.value()); + } + } else if(callee_id == CPROVER_PREFIX "obeys_contract") { auto opt_rank = is_param_expr(it.call_arguments()[0], parameter_rank); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.cpp new file mode 100644 index 00000000000..00d4579f5a4 --- /dev/null +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.cpp @@ -0,0 +1,73 @@ +/*******************************************************************\ + +Module: Dynamic frame condition checking for function contracts + +Author: Remi Delmas, delmasrd@amazon.com +Date: August 2022 + +\*******************************************************************/ + +#include "dfcc_pointer_in_range.h" + +#include +#include +#include +#include +#include + +#include "dfcc_library.h" + +dfcc_pointer_in_ranget::dfcc_pointer_in_ranget( + dfcc_libraryt &library, + message_handlert &message_handler) + : library(library), message_handler(message_handler), log(message_handler) +{ +} + +void dfcc_pointer_in_ranget::rewrite_calls( + goto_programt &program, + const exprt &write_set) +{ + rewrite_calls( + program, + program.instructions.begin(), + program.instructions.end(), + write_set); +} + +void dfcc_pointer_in_ranget::rewrite_calls( + goto_programt &program, + goto_programt::targett first_instruction, + const goto_programt::targett &last_instruction, + const exprt &write_set) +{ + auto &target = first_instruction; + while(target != last_instruction) + { + if(target->is_function_call()) + { + const auto &function = target->call_function(); + + if(function.id() == ID_symbol) + { + const irep_idt &fun_name = to_symbol_expr(function).get_identifier(); + + if(fun_name == CPROVER_PREFIX "pointer_in_range_dfcc") + { + // add address on second operand + target->call_arguments()[1] = + address_of_exprt(target->call_arguments()[1]); + + // fix the function name. + to_symbol_expr(target->call_function()) + .set_identifier( + library.dfcc_fun_symbol[dfcc_funt::POINTER_IN_RANGE_DFCC].name); + + // pass the write_set + target->call_arguments().push_back(write_set); + } + } + } + target++; + } +} diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.h new file mode 100644 index 00000000000..0a368f8cc9a --- /dev/null +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.h @@ -0,0 +1,58 @@ +/*******************************************************************\ + +Module: Dynamic frame condition checking for function contracts + +Author: Remi Delmas, delmasrd@amazon.com +Date: August 2022 + +\*******************************************************************/ + +/// \file +/// Instruments occurrences of pointer_in_range predicates in programs +/// encoding requires and ensures clauses of contracts. + +#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_POINTER_IN_RANGE_H +#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_POINTER_IN_RANGE_H + +#include + +#include + +class goto_modelt; +class message_handlert; +class dfcc_libraryt; +class exprt; + +/// Rewrites calls to pointer_in_range predicates into calls +/// to the library implementation. +class dfcc_pointer_in_ranget +{ +public: + /// \param library The contracts instrumentation library + /// \param message_handler Used for messages + dfcc_pointer_in_ranget( + dfcc_libraryt &library, + message_handlert &message_handler); + + /// Rewrites calls to pointer_in_range predicates into calls + /// to the library implementation in the given program, passing the + /// given write_set expression as parameter to the library function. + void rewrite_calls(goto_programt &program, const exprt &write_set); + + /// Rewrites calls to pointer_in_range predicates into calls + /// to the library implementation in the given program between + /// first_instruction (included) and last_instruction (excluded), passing the + /// given write_set expression as parameter to the library function. + void rewrite_calls( + goto_programt &program, + goto_programt::targett first_instruction, + const goto_programt::targett &last_instruction, + const exprt &write_set); + +protected: + dfcc_libraryt &library; + message_handlert &message_handler; + messaget log; +}; + +#endif