From f7752cfb62e5a8bf5bfba313e88f67622e75fb40 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Thu, 16 Dec 2021 22:58:11 +0000 Subject: [PATCH] Function contracts: performance optimisation for assigns clause checking. - don't instrument assignments to locals and function parameters, - don't add function parameters and non-dirty locals to the write set, - remove from the local write set CARs that are provably not alive, - remove function parameters and locals from assigns clauses in tests. Sanity checks: - change GOTO instruction with false guards into SKIP instructions (removes artificial loops), - check loop-freeness before assigns clause instrumentation (required for soundness of assigns clause checking). The net effect of these changes is a better proof performance because of a reduction in the number of generated assertions and of their size, but otherwise the contract checking functionality remains unchanged. Rationale: Assigning to local variables or function parameter is always legal so we skip instrumenting these assignments. We avoid adding function parameters and local variables to the local write set, except when their address is taken at some point in the program and can later be assigned to indirectly via pointers. When generating inclusion checks for assignments, we remove from the local write set targets which are not possibly alive at the ASSIGN instruction that gets instrumented. --- .../contracts/assigns_enforce_04/test.desc | 6 - .../contracts/assigns_enforce_05/test.desc | 1 - .../contracts/assigns_enforce_18/test.desc | 3 - .../contracts/assigns_enforce_21/test.desc | 3 - .../assigns_enforce_arrays_01/main.c | 2 +- .../assigns_enforce_arrays_03/main.c | 2 +- .../assigns_enforce_arrays_03/test.desc | 5 +- .../assigns_enforce_arrays_04/main.c | 15 +- .../assigns_enforce_arrays_04/test.desc | 2 +- .../assigns_enforce_arrays_05/main.c | 15 +- .../assigns_enforce_arrays_05/test.desc | 11 +- .../test.desc | 9 +- .../assigns_enforce_free_dead/test.desc | 18 -- .../assigns_enforce_malloc_01/main.c | 9 +- .../assigns_enforce_malloc_01/test.desc | 7 +- .../assigns_enforce_malloc_02/test.desc | 6 +- .../assigns_enforce_multi_file_02/header.h | 2 +- .../assigns_enforce_multi_file_02/test.desc | 1 + .../assigns_enforce_statics/test.desc | 1 - .../assigns_enforce_structs_01/main.c | 9 +- .../assigns_enforce_structs_01/test.desc | 9 +- .../assigns_enforce_structs_02/main.c | 9 +- .../assigns_enforce_structs_02/test.desc | 11 +- .../assigns_enforce_structs_03/main.c | 11 +- .../assigns_enforce_structs_03/test.desc | 2 +- .../assigns_enforce_structs_04/test.desc | 1 - .../test.desc | 13 - .../contracts/assigns_function_pointer/main.c | 24 +- .../assigns_function_pointer/test.desc | 7 +- .../assigns_type_checking_valid_cases/main.c | 12 +- .../test.desc | 5 - .../assigns_validity_pointer_01/test.desc | 1 - .../assigns_validity_pointer_02/test.desc | 2 - regression/contracts/function_check_02/main.c | 14 +- .../history-pointer-enforce-10/main.c | 2 +- .../history-pointer-enforce-10/test.desc | 4 +- .../contracts/loop-freeness-check/main.c | 16 ++ .../contracts/loop-freeness-check/test.desc | 13 + .../quantifiers-exists-ensures-enforce/main.c | 28 ++- .../main.c | 28 ++- .../quantifiers-forall-ensures-enforce/main.c | 28 ++- .../test.desc | 3 +- .../main.c | 12 +- .../contracts/quantifiers-nested-01/main.c | 14 +- .../contracts/quantifiers-nested-03/main.c | 14 +- .../contracts/test_aliasing_ensure/main.c | 2 +- .../test_aliasing_ensure_indirect/main.c | 4 +- .../test_aliasing_ensure_indirect/test.desc | 1 - src/goto-instrument/contracts/assigns.cpp | 27 ++- src/goto-instrument/contracts/assigns.h | 9 +- src/goto-instrument/contracts/contracts.cpp | 224 ++++++++++++++---- src/goto-instrument/contracts/contracts.h | 68 ++++-- src/goto-instrument/contracts/utils.cpp | 65 +++++ src/goto-instrument/contracts/utils.h | 85 ++++++- 54 files changed, 642 insertions(+), 253 deletions(-) create mode 100644 regression/contracts/loop-freeness-check/main.c create mode 100644 regression/contracts/loop-freeness-check/test.desc diff --git a/regression/contracts/assigns_enforce_04/test.desc b/regression/contracts/assigns_enforce_04/test.desc index b1a24463b4d..2e1caa26893 100644 --- a/regression/contracts/assigns_enforce_04/test.desc +++ b/regression/contracts/assigns_enforce_04/test.desc @@ -3,12 +3,6 @@ main.c --enforce-contract f1 ^EXIT=0$ ^SIGNAL=0$ -^\[f1.\d+\] line \d+ Check that x2 is assignable: SUCCESS$ -^\[f1.\d+\] line \d+ Check that y2 is assignable: SUCCESS$ -^\[f1.\d+\] line \d+ Check that z2 is assignable: SUCCESS$ -^\[f2.\d+\] line \d+ Check that x3 is assignable: SUCCESS$ -^\[f2.\d+\] line \d+ Check that y3 is assignable: SUCCESS$ -^\[f2.\d+\] line \d+ Check that z3 is assignable: SUCCESS$ ^\[f3.\d+\] line \d+ Check that \*x3 is assignable: SUCCESS$ ^\[f3.\d+\] line \d+ Check that \*y3 is assignable: SUCCESS$ ^\[f3.\d+\] line \d+ Check that \*z3 is assignable: SUCCESS$ diff --git a/regression/contracts/assigns_enforce_05/test.desc b/regression/contracts/assigns_enforce_05/test.desc index 6c7363f88d0..97352a948f2 100644 --- a/regression/contracts/assigns_enforce_05/test.desc +++ b/regression/contracts/assigns_enforce_05/test.desc @@ -3,7 +3,6 @@ main.c --enforce-contract f1 --enforce-contract f2 --enforce-contract f3 ^EXIT=0$ ^SIGNAL=0$ -^\[f1.1\] line \d+ .*: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- -- diff --git a/regression/contracts/assigns_enforce_18/test.desc b/regression/contracts/assigns_enforce_18/test.desc index 011006f19c6..74c8ac7a49b 100644 --- a/regression/contracts/assigns_enforce_18/test.desc +++ b/regression/contracts/assigns_enforce_18/test.desc @@ -7,9 +7,6 @@ main.c ^\[bar.\d+\] line \d+ Check that \*b is assignable: SUCCESS$ ^\[baz.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)c\) is assignable: FAILURE$ ^\[baz.\d+\] line \d+ Check that \*a is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that a is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that yp is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$ ^\[foo.\d+\] line \d+ Check that \*xp is assignable: SUCCESS$ ^\[foo.\d+\] line \d+ Check that y is assignable: FAILURE$ ^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)yp\) is assignable: SUCCESS$ diff --git a/regression/contracts/assigns_enforce_21/test.desc b/regression/contracts/assigns_enforce_21/test.desc index 7b629e00d6f..7e2b828b342 100644 --- a/regression/contracts/assigns_enforce_21/test.desc +++ b/regression/contracts/assigns_enforce_21/test.desc @@ -6,9 +6,6 @@ main.c main.c function bar ^\[bar.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ ^\[bar.\d+\] line \d+ Check that x is assignable: FAILURE$ -^\[baz.\d+\] line \d+ Check that w is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that w is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/assigns_enforce_arrays_01/main.c b/regression/contracts/assigns_enforce_arrays_01/main.c index bf793de2da6..ee8405c3ce4 100644 --- a/regression/contracts/assigns_enforce_arrays_01/main.c +++ b/regression/contracts/assigns_enforce_arrays_01/main.c @@ -1,4 +1,4 @@ -void f1(int a[], int len) __CPROVER_assigns(a) +void f1(int a[], int len) __CPROVER_assigns() { int b[10]; a = b; diff --git a/regression/contracts/assigns_enforce_arrays_03/main.c b/regression/contracts/assigns_enforce_arrays_03/main.c index 9a51b358f75..2511fbe4103 100644 --- a/regression/contracts/assigns_enforce_arrays_03/main.c +++ b/regression/contracts/assigns_enforce_arrays_03/main.c @@ -1,4 +1,4 @@ -void assign_out_under(int a[], int len) __CPROVER_assigns(a) +void assign_out_under(int a[], int len) __CPROVER_assigns() { a[1] = 5; } diff --git a/regression/contracts/assigns_enforce_arrays_03/test.desc b/regression/contracts/assigns_enforce_arrays_03/test.desc index f8f7fe4b375..f6e98f0b4aa 100644 --- a/regression/contracts/assigns_enforce_arrays_03/test.desc +++ b/regression/contracts/assigns_enforce_arrays_03/test.desc @@ -6,5 +6,6 @@ main.c ^VERIFICATION FAILED$ -- -- -Checks whether verification fails when an assigns clause contains pointer, -but function only modifies its content. +Checks whether verification fails when a function has an array +as parameter, an empty assigns clause and attempts to modify the object +pointed to by the pointer. diff --git a/regression/contracts/assigns_enforce_arrays_04/main.c b/regression/contracts/assigns_enforce_arrays_04/main.c index 6e51934a449..bf4d22fa028 100644 --- a/regression/contracts/assigns_enforce_arrays_04/main.c +++ b/regression/contracts/assigns_enforce_arrays_04/main.c @@ -1,21 +1,20 @@ -void assigns_single(int a[], int len) __CPROVER_assigns(a) +void assigns_single(int a[], int len) { + int i; + __CPROVER_assume(0 <= i && i < len); + a[i] = 0; } -void assigns_range(int a[], int len) __CPROVER_assigns(a) -{ -} - -void assigns_big_range(int a[], int len) __CPROVER_assigns(a) +void uses_assigns(int a[], int len) + __CPROVER_assigns(__CPROVER_POINTER_OBJECT(a)) { assigns_single(a, len); - assigns_range(a, len); } int main() { int arr[10]; - assigns_big_range(arr, 10); + uses_assigns(arr, 10); return 0; } diff --git a/regression/contracts/assigns_enforce_arrays_04/test.desc b/regression/contracts/assigns_enforce_arrays_04/test.desc index e59988d65d7..e2dd274fa7d 100644 --- a/regression/contracts/assigns_enforce_arrays_04/test.desc +++ b/regression/contracts/assigns_enforce_arrays_04/test.desc @@ -1,6 +1,6 @@ CORE main.c ---enforce-contract assigns_single --enforce-contract assigns_range --enforce-contract assigns_big_range +--enforce-contract uses_assigns ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts/assigns_enforce_arrays_05/main.c b/regression/contracts/assigns_enforce_arrays_05/main.c index 4eade02f201..01ec9cf6b98 100644 --- a/regression/contracts/assigns_enforce_arrays_05/main.c +++ b/regression/contracts/assigns_enforce_arrays_05/main.c @@ -1,18 +1,23 @@ -void assigns_ptr(int *x) __CPROVER_assigns(*x) +void assigns_ptr(int *x) { *x = 200; } -void assigns_range(int a[], int len) __CPROVER_assigns(a) +void uses_assigns(int a[], int i, int len) + // clang-format off + __CPROVER_requires(0 <= i && i < len) + __CPROVER_assigns(*(&a[i])) +// clang-format on { - int *ptr = &(a[7]); + int *ptr = &(a[i]); assigns_ptr(ptr); } int main() { int arr[10]; - assigns_range(arr, 10); - + int i; + __CPROVER_assume(0 <= i && i < 10); + uses_assigns(arr, i, 10); return 0; } diff --git a/regression/contracts/assigns_enforce_arrays_05/test.desc b/regression/contracts/assigns_enforce_arrays_05/test.desc index 4fe133f4914..019d4770188 100644 --- a/regression/contracts/assigns_enforce_arrays_05/test.desc +++ b/regression/contracts/assigns_enforce_arrays_05/test.desc @@ -1,11 +1,10 @@ CORE main.c ---enforce-contract assigns_range -^EXIT=10$ +--enforce-contract uses_assigns +^EXIT=0$ ^SIGNAL=0$ -^VERIFICATION FAILED$ +^\[assigns_ptr\.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ +^VERIFICATION SUCCESSFUL$ -- -- -Checks whether verification fails when an assigns clause of a function -indicates the pointer might change, but one of its internal function only -modified its content. +Checks whether verification succeeds for array elements at a symbolic index. diff --git a/regression/contracts/assigns_enforce_detect_local_statics/test.desc b/regression/contracts/assigns_enforce_detect_local_statics/test.desc index 9b0ea3f8b69..e0309d9fc9d 100644 --- a/regression/contracts/assigns_enforce_detect_local_statics/test.desc +++ b/regression/contracts/assigns_enforce_detect_local_statics/test.desc @@ -1,13 +1,12 @@ CORE main.c --enforce-contract bar +^\[foo.\d+\] line 14 Check that foo\$\$1\$\$x is assignable: SUCCESS +^\[foo.\d+\] line 17 Check that \*y is assignable: SUCCESS +^\[foo.\d+\] line 20 Check that \*yy is assignable: FAILURE +^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ -^\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that foo\$\$1\$\$x is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that \*yy is assignable: FAILURE$ -^VERIFICATION FAILED$ -- -- Checks whether static local and global variables are correctly tracked diff --git a/regression/contracts/assigns_enforce_free_dead/test.desc b/regression/contracts/assigns_enforce_free_dead/test.desc index 616e2b670ab..b4cee3c92a3 100644 --- a/regression/contracts/assigns_enforce_free_dead/test.desc +++ b/regression/contracts/assigns_enforce_free_dead/test.desc @@ -7,12 +7,6 @@ main.c ^\[foo.\d+\] line \d+ Check that \*q is assignable: SUCCESS$ ^\[foo.\d+\] line \d+ Check that \*w is assignable: SUCCESS$ ^\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that a is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that q is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that w is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that x is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$ ^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)z\) is assignable: SUCCESS$ ^EXIT=10$ ^SIGNAL=0$ @@ -22,16 +16,7 @@ main.c ^\[foo.\d+\] line \d+ Check that \*q is assignable: FAILURE$ ^\[foo.\d+\] line \d+ Check that \*w is assignable: FAILURE$ ^\[foo.\d+\] line \d+ Check that \*x is assignable: FAILURE$ -^\[foo.\d+\] line \d+ Check that a is assignable: FAILURE$ -^\[foo.\d+\] line \d+ Check that q is assignable: FAILURE$ -^\[foo.\d+\] line \d+ Check that w is assignable: FAILURE$ -^\[foo.\d+\] line \d+ Check that x is assignable: FAILURE$ -^\[foo.\d+\] line \d+ Check that y is assignable: FAILURE$ -^\[foo.\d+\] line \d+ Check that z is assignable: FAILURE$ ^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)z\) is assignable: FAILURE$ -^.*__car_valid.*: FAILURE$ -^.*__car_lb.*: FAILURE$ -^.*__car_ub.*: FAILURE$ -- Checks that invalidated CARs are correctly tracked on `free` and `DEAD`. @@ -40,6 +25,3 @@ we rule out all failures using the negative regex matches above. We also check (using positive regex matches above) that `**p` should be assignable in one case and should not be assignable in the other. - -Finally, we check that there should be no "internal" assertion failures -on `__car_valid`, `__car_ub`, `__car_lb` variables used to track CARs. diff --git a/regression/contracts/assigns_enforce_malloc_01/main.c b/regression/contracts/assigns_enforce_malloc_01/main.c index c02eca20a2a..7896a93b158 100644 --- a/regression/contracts/assigns_enforce_malloc_01/main.c +++ b/regression/contracts/assigns_enforce_malloc_01/main.c @@ -1,16 +1,15 @@ #include -int f1(int *a, int *b) __CPROVER_assigns(*a, b) +int f(int *a) __CPROVER_assigns() { - b = (int *)malloc(sizeof(int)); - *b = 5; + a = (int *)malloc(sizeof(int)); + *a = 5; } int main() { int m = 4; - int n = 3; - f1(&m, &n); + f(&m); return 0; } diff --git a/regression/contracts/assigns_enforce_malloc_01/test.desc b/regression/contracts/assigns_enforce_malloc_01/test.desc index 7b71dc6b088..0ee889a7b2b 100644 --- a/regression/contracts/assigns_enforce_malloc_01/test.desc +++ b/regression/contracts/assigns_enforce_malloc_01/test.desc @@ -1,9 +1,12 @@ CORE main.c ---enforce-contract f1 +--enforce-contract f ^EXIT=0$ ^SIGNAL=0$ +^\[f\.\d+\] line \d+ Check that \*a is assignable: SUCCESS ^VERIFICATION SUCCESSFUL$ -- -- -This test checks that verification succeeds when a formal parameter pointer outside of the assigns clause is instead pointed as freshly allocated memory before being assigned. +This test checks that verification succeeds when a formal parameter +with a pointer type is first updated to point to a locally malloc'd object +before being assigned to. diff --git a/regression/contracts/assigns_enforce_malloc_02/test.desc b/regression/contracts/assigns_enforce_malloc_02/test.desc index 5cf7b48e5a7..49f5f99a59d 100644 --- a/regression/contracts/assigns_enforce_malloc_02/test.desc +++ b/regression/contracts/assigns_enforce_malloc_02/test.desc @@ -1,9 +1,11 @@ CORE main.c --enforce-contract f1 -^EXIT=6$ +^Invariant check failed$ +^Condition: is_loop_free +^Reason: Loops remain in function 'f1', assigns clause checking instrumentation cannot be applied\. +^EXIT=(127|134)$ ^SIGNAL=0$ -Unable to complete instrumentation, as this malloc may be in a loop.$ -- -- This test checks that an error is thrown when malloc is called within a loop. diff --git a/regression/contracts/assigns_enforce_multi_file_02/header.h b/regression/contracts/assigns_enforce_multi_file_02/header.h index e07691ac68a..267565a2ed5 100644 --- a/regression/contracts/assigns_enforce_multi_file_02/header.h +++ b/regression/contracts/assigns_enforce_multi_file_02/header.h @@ -14,7 +14,7 @@ struct pair_of_pairs int f1(int *a, struct pair *b); -int f1(int *a, struct pair *b) __CPROVER_assigns(*a, b) +int f1(int *a, struct pair *b) __CPROVER_assigns(*a) { struct pair_of_pairs *pop = (struct pair_of_pairs *)malloc(sizeof(struct pair_of_pairs)); diff --git a/regression/contracts/assigns_enforce_multi_file_02/test.desc b/regression/contracts/assigns_enforce_multi_file_02/test.desc index 6020c479abb..dd02559f652 100644 --- a/regression/contracts/assigns_enforce_multi_file_02/test.desc +++ b/regression/contracts/assigns_enforce_multi_file_02/test.desc @@ -3,6 +3,7 @@ main.c --enforce-contract f1 ^EXIT=0$ ^SIGNAL=0$ +^\[f1\.\d+\] line \d+ Check that b->y is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- -- diff --git a/regression/contracts/assigns_enforce_statics/test.desc b/regression/contracts/assigns_enforce_statics/test.desc index 269b088542b..fee67eaefaa 100644 --- a/regression/contracts/assigns_enforce_statics/test.desc +++ b/regression/contracts/assigns_enforce_statics/test.desc @@ -3,7 +3,6 @@ main.c --enforce-contract foo _ --pointer-primitive-check ^EXIT=0$ ^SIGNAL=0$ -^\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS$ ^\[foo.\d+\] line \d+ Check that foo\$\$1\$\$x is assignable: SUCCESS$ ^\[foo.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts/assigns_enforce_structs_01/main.c b/regression/contracts/assigns_enforce_structs_01/main.c index c44f786ef44..ee4a59c2b1f 100644 --- a/regression/contracts/assigns_enforce_structs_01/main.c +++ b/regression/contracts/assigns_enforce_structs_01/main.c @@ -6,18 +6,17 @@ struct pair int y; }; -int f1(int *a, int *b) __CPROVER_assigns(*a, b) +int f(int *a) __CPROVER_assigns() { struct pair *p = (struct pair *)malloc(sizeof(struct pair)); - b = &(p->y); - *b = 5; + a = &(p->y); + *a = 5; } int main() { int m = 4; - int n = 3; - f1(&m, &n); + f(&m); return 0; } diff --git a/regression/contracts/assigns_enforce_structs_01/test.desc b/regression/contracts/assigns_enforce_structs_01/test.desc index 00a255be860..0d77a423c99 100644 --- a/regression/contracts/assigns_enforce_structs_01/test.desc +++ b/regression/contracts/assigns_enforce_structs_01/test.desc @@ -1,11 +1,12 @@ CORE main.c ---enforce-contract f1 +--enforce-contract f ^EXIT=0$ ^SIGNAL=0$ +^\[f\.\d+\] line \d+ Check that \*a is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- -- -Checks whether verification succeeds when a formal parameter pointer outside -of the assigns clause is instead pointed at the location of a member of a -freshly allocated struct before being assigned. +Checks whether verification succeeds when a pointer deref that is not +specified in the assigns clause is first pointed at a member of a +locally malloc'd struct before being assigned. diff --git a/regression/contracts/assigns_enforce_structs_02/main.c b/regression/contracts/assigns_enforce_structs_02/main.c index 4d909f19131..fd544aa9148 100644 --- a/regression/contracts/assigns_enforce_structs_02/main.c +++ b/regression/contracts/assigns_enforce_structs_02/main.c @@ -12,19 +12,18 @@ struct pair_of_pairs struct pair p2; }; -int f1(int *a, int *b) __CPROVER_assigns(*a, b) +int f(int *a) __CPROVER_assigns() { struct pair_of_pairs *pop = (struct pair_of_pairs *)malloc(sizeof(struct pair_of_pairs)); - b = &(pop->p2.x); - *b = 5; + a = &(pop->p2.x); + *a = 5; } int main() { int m = 4; - int n = 3; - f1(&m, &n); + f(&m); return 0; } diff --git a/regression/contracts/assigns_enforce_structs_02/test.desc b/regression/contracts/assigns_enforce_structs_02/test.desc index 5d72b1c2f13..fc0948b1676 100644 --- a/regression/contracts/assigns_enforce_structs_02/test.desc +++ b/regression/contracts/assigns_enforce_structs_02/test.desc @@ -1,13 +1,12 @@ CORE main.c ---enforce-contract f1 +--enforce-contract f ^EXIT=0$ ^SIGNAL=0$ +^\[f\.\d+\] line \d+ Check that \*a is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- -- -Checks whether verification succeeds when a formal parameter pointer outside -of the assigns clause is assigned after being pointed at the location of a -member of a sub-struct of a freshly allocated struct before being assigned. -This is meant to show that all contained members (and their contained members) -of assignable structs are valid to assign. +Checks whether verification succeeds when a pointer deref that is not +specified in the assigns clause is first pointed at a member of a locally +malloc'd struct before being assigned (with extra nesting). diff --git a/regression/contracts/assigns_enforce_structs_03/main.c b/regression/contracts/assigns_enforce_structs_03/main.c index 2ecfd58997d..a4d282edc25 100644 --- a/regression/contracts/assigns_enforce_structs_03/main.c +++ b/regression/contracts/assigns_enforce_structs_03/main.c @@ -12,19 +12,18 @@ struct pair_of_pairs struct pair p2; }; -int f1(int *a, struct pair *b) __CPROVER_assigns(*a, b) +int f(struct pair *a) __CPROVER_assigns() { struct pair_of_pairs *pop = (struct pair_of_pairs *)malloc(sizeof(struct pair_of_pairs)); - b = &(pop->p2); - b->y = 5; + a = &(pop->p2); + a->y = 5; } int main() { - int m = 4; - struct pair n; - f1(&m, &n); + struct pair m; + f(&m); return 0; } diff --git a/regression/contracts/assigns_enforce_structs_03/test.desc b/regression/contracts/assigns_enforce_structs_03/test.desc index f8ab3d39c45..0d57241131b 100644 --- a/regression/contracts/assigns_enforce_structs_03/test.desc +++ b/regression/contracts/assigns_enforce_structs_03/test.desc @@ -1,6 +1,6 @@ CORE main.c ---enforce-contract f1 +--enforce-contract f ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts/assigns_enforce_structs_04/test.desc b/regression/contracts/assigns_enforce_structs_04/test.desc index 24300267705..3de0bffb9ca 100644 --- a/regression/contracts/assigns_enforce_structs_04/test.desc +++ b/regression/contracts/assigns_enforce_structs_04/test.desc @@ -6,7 +6,6 @@ main.c ^\[f1.\d+\] line \d+ Check that p->y is assignable: FAILURE$ ^\[f2.\d+\] line \d+ Check that p->x is assignable: FAILURE$ ^\[f3.\d+\] line \d+ Check that p->y is assignable: SUCCESS$ -^\[f4.\d+\] line \d+ Check that p is assignable: SUCCESS$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/assigns_enforce_subfunction_calls/test.desc b/regression/contracts/assigns_enforce_subfunction_calls/test.desc index c4ffcabe76d..9411d1e4536 100644 --- a/regression/contracts/assigns_enforce_subfunction_calls/test.desc +++ b/regression/contracts/assigns_enforce_subfunction_calls/test.desc @@ -3,28 +3,15 @@ main.c --enforce-contract foo ^EXIT=10$ ^SIGNAL=0$ -^main.c function bar$ -^\[bar.1\] line \d+ Check that x is assignable: SUCCESS$ -^\[bar.2\] line \d+ Check that y is assignable: SUCCESS$ -^\[bar.3\] line \d+ Check that x is assignable: SUCCESS$ -^\[bar.4\] line \d+ Check that y is assignable: SUCCESS$ ^main.c function baz$ ^\[baz.1\] line \d+ Check that \*x is assignable: SUCCESS$ ^\[baz.2\] line \d+ Check that \*x is assignable: SUCCESS$ ^\[baz.3\] line \d+ Check that \*x is assignable: FAILURE$ ^\[baz.4\] line \d+ Check that \*x is assignable: FAILURE$ ^main.c function foo$ -^\[foo.1\] line \d+ Check that x is assignable: SUCCESS$ -^\[foo.2\] line \d+ Check that y is assignable: SUCCESS$ ^\[foo.assertion.1\] line \d+ foo.x.set: SUCCESS$ -^\[foo.3\] line \d+ Check that x is assignable: SUCCESS$ -^\[foo.4\] line \d+ Check that y is assignable: SUCCESS$ ^\[foo.assertion.2\] line \d+ foo.local.set: SUCCESS$ -^\[foo.5\] line \d+ Check that x is assignable: SUCCESS$ -^\[foo.6\] line \d+ Check that y is assignable: SUCCESS$ ^\[foo.assertion.3\] line \d+ foo.y.set: SUCCESS$ -^\[foo.7\] line \d+ Check that x is assignable: SUCCESS$ -^\[foo.8\] line \d+ Check that y is assignable: SUCCESS$ ^\[foo.assertion.4\] line \d+ foo.z.set: SUCCESS$ ^VERIFICATION FAILED$ -- diff --git a/regression/contracts/assigns_function_pointer/main.c b/regression/contracts/assigns_function_pointer/main.c index 26bb484468a..f3d27e97713 100644 --- a/regression/contracts/assigns_function_pointer/main.c +++ b/regression/contracts/assigns_function_pointer/main.c @@ -3,22 +3,36 @@ int x = 0; +struct fptr_t +{ + void (*f)(); +}; + void foo() { x = 1; } -void bar(void (*fun_ptr)()) __CPROVER_assigns(fun_ptr) +void foofoo() +{ + x = 2; +} + +void bar(struct fptr_t *s, void (**f)()) __CPROVER_assigns(s->f, *f) { - fun_ptr = &foo; + s->f = &foo; + *f = &foofoo; } int main() { assert(x == 0); - void (*fun_ptr)() = NULL; - bar(fun_ptr); - fun_ptr(); + struct fptr_t s; + void (*f)(); + bar(&s, &f); + s.f(); assert(x == 1); + f(); + assert(x == 2); return 0; } diff --git a/regression/contracts/assigns_function_pointer/test.desc b/regression/contracts/assigns_function_pointer/test.desc index 4795e9d620b..f5d4a7d36b8 100644 --- a/regression/contracts/assigns_function_pointer/test.desc +++ b/regression/contracts/assigns_function_pointer/test.desc @@ -3,9 +3,12 @@ main.c --enforce-contract bar ^EXIT=0$ ^SIGNAL=0$ -^\[bar.1\] line \d+ Check that fun\_ptr is assignable: SUCCESS$ ^\[main.assertion.\d+\] line \d+ assertion x \=\= 0: SUCCESS$ +^\[bar\.\d+\] line \d+ Check that s->f is assignable: SUCCESS$ +^\[bar\.\d+\] line \d+ Check that \*f is assignable: SUCCESS$ ^\[main.assertion.\d+\] line \d+ assertion x \=\= 1: SUCCESS$ +^\[main.assertion.\d+\] line \d+ assertion x \=\= 2: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- -Checks whether assigns clause accepts function pointers. +Checks whether assigns clause accepts function pointers +and pointers to function pointers. diff --git a/regression/contracts/assigns_type_checking_valid_cases/main.c b/regression/contracts/assigns_type_checking_valid_cases/main.c index 69062b90dc4..f1381d555e4 100644 --- a/regression/contracts/assigns_type_checking_valid_cases/main.c +++ b/regression/contracts/assigns_type_checking_valid_cases/main.c @@ -14,17 +14,17 @@ struct buf struct blob aux; }; -void foo1(int a) __CPROVER_assigns(a) +void foo1(int a) __CPROVER_assigns() { a = 0; } -void foo2(int *b) __CPROVER_assigns(b) +void foo2(int *b) __CPROVER_assigns() { b = NULL; } -void foo3(int a, int *b) __CPROVER_assigns(b, x, y) +void foo3(int a, int *b) __CPROVER_assigns(x, y) { b = NULL; x = malloc(sizeof(*x)); @@ -32,14 +32,14 @@ void foo3(int a, int *b) __CPROVER_assigns(b, x, y) } void foo4(int a, int *b, int *c) __CPROVER_requires(c != NULL) - __CPROVER_requires(x != NULL) __CPROVER_assigns(b, *c, *x) + __CPROVER_requires(x != NULL) __CPROVER_assigns(*c, *x) { b = NULL; *c = 0; *x = 0; } -void foo5(struct buf buffer) __CPROVER_assigns(buffer) +void foo5(struct buf buffer) __CPROVER_assigns() { buffer.data = NULL; buffer.len = 0; @@ -73,7 +73,7 @@ void foo8(int array[]) __CPROVER_assigns(__CPROVER_POINTER_OBJECT(array)) array[9] = 1; } -void foo9(int array[]) __CPROVER_assigns(array) +void foo9(int array[]) __CPROVER_assigns() { int *new_array = NULL; array = new_array; diff --git a/regression/contracts/assigns_type_checking_valid_cases/test.desc b/regression/contracts/assigns_type_checking_valid_cases/test.desc index e7c22c65b59..1592a4973c2 100644 --- a/regression/contracts/assigns_type_checking_valid_cases/test.desc +++ b/regression/contracts/assigns_type_checking_valid_cases/test.desc @@ -3,13 +3,9 @@ main.c --enforce-contract foo1 --enforce-contract foo2 --enforce-contract foo3 --enforce-contract foo4 --enforce-contract foo5 --enforce-contract foo6 --enforce-contract foo7 --enforce-contract foo8 --enforce-contract foo9 --enforce-contract foo10 _ --pointer-primitive-check ^EXIT=0$ ^SIGNAL=0$ -^\[foo1.\d+\] line \d+ Check that a is assignable: SUCCESS$ ^\[foo10.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$ ^\[foo10.\d+\] line \d+ Check that buffer->aux\.allocated is assignable: SUCCESS$ -^\[foo2.\d+\] line \d+ Check that b is assignable: SUCCESS$ -^\[foo3.\d+\] line \d+ Check that b is assignable: SUCCESS$ ^\[foo3.\d+\] line \d+ Check that y is assignable: SUCCESS$ -^\[foo4.\d+\] line \d+ Check that b is assignable: SUCCESS$ ^\[foo4.\d+\] line \d+ Check that \*c is assignable: SUCCESS$ ^\[foo4.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ ^\[foo5.\d+\] line \d+ Check that buffer.data is assignable: SUCCESS$ @@ -28,7 +24,6 @@ main.c ^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)7\] is assignable: SUCCESS$ ^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)8\] is assignable: SUCCESS$ ^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)9\] is assignable: SUCCESS$ -^\[foo9.\d+\] line \d+ Check that array is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- Checks whether CBMC parses correctly all standard cases for assigns clauses. diff --git a/regression/contracts/assigns_validity_pointer_01/test.desc b/regression/contracts/assigns_validity_pointer_01/test.desc index 149013fd7a7..905c8e2e27a 100644 --- a/regression/contracts/assigns_validity_pointer_01/test.desc +++ b/regression/contracts/assigns_validity_pointer_01/test.desc @@ -8,7 +8,6 @@ SUCCESS // bar ASSERT \*foo::x > 0 IF ¬\(\*foo::x = 3\) THEN GOTO \d -IF ¬\(.*0.* = NULL\) THEN GOTO \d ASSIGN .*::tmp_if_expr := \(\*\(.*0.*\) = 5 \? true : false\) ASSIGN .*::tmp_if_expr\$\d := .*::tmp_if_expr \? true : false ASSUME .*::tmp_if_expr\$\d diff --git a/regression/contracts/assigns_validity_pointer_02/test.desc b/regression/contracts/assigns_validity_pointer_02/test.desc index c8730036836..4035fc12118 100644 --- a/regression/contracts/assigns_validity_pointer_02/test.desc +++ b/regression/contracts/assigns_validity_pointer_02/test.desc @@ -7,8 +7,6 @@ main.c ^\[bar.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ ^\[bar.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ ^\[baz.\d+\] line \d+ Check that \*z is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that x is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS$ ^\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/function_check_02/main.c b/regression/contracts/function_check_02/main.c index 7960696b6d1..18be2525d8e 100644 --- a/regression/contracts/function_check_02/main.c +++ b/regression/contracts/function_check_02/main.c @@ -15,10 +15,16 @@ int initialize(int *arr) ) // clang-format on { - for(int i = 0; i < 10; i++) - { - arr[i] = i; - } + arr[0] = 0; + arr[1] = 1; + arr[2] = 2; + arr[3] = 3; + arr[4] = 4; + arr[5] = 5; + arr[6] = 6; + arr[7] = 7; + arr[8] = 8; + arr[9] = 9; return 0; } diff --git a/regression/contracts/history-pointer-enforce-10/main.c b/regression/contracts/history-pointer-enforce-10/main.c index 5421773d9bb..475bc47b411 100644 --- a/regression/contracts/history-pointer-enforce-10/main.c +++ b/regression/contracts/history-pointer-enforce-10/main.c @@ -23,7 +23,7 @@ void bar(struct pair *p) __CPROVER_assigns(p->y) p->y = (p->y + 5); } -void baz(struct pair p) __CPROVER_assigns(p) +void baz(struct pair p) __CPROVER_assigns() __CPROVER_ensures(p == __CPROVER_old(p)) { struct pair pp = p; diff --git a/regression/contracts/history-pointer-enforce-10/test.desc b/regression/contracts/history-pointer-enforce-10/test.desc index a3ad4b4cb9c..e8359a34c9e 100644 --- a/regression/contracts/history-pointer-enforce-10/test.desc +++ b/regression/contracts/history-pointer-enforce-10/test.desc @@ -7,8 +7,6 @@ main.c ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$ ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$ ^\[bar.\d+\] line \d+ Check that p->y is assignable: SUCCESS$ -^\[baz.\d+\] line \d+ Check that p is assignable: SUCCESS$ -^\[baz.\d+\] line \d+ Check that p is assignable: SUCCESS$ ^\[foo.\d+\] line \d+ Check that \*p->y is assignable: SUCCESS$ ^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$ ^\[main.assertion.\d+\] line \d+ assertion \*\(p->y\) == 7: SUCCESS$ @@ -19,3 +17,5 @@ main.c This test checks that history variables are supported for structs, symbols, and struct members. By using the --enforce-contract flag, the postcondition (with history variable) is asserted. In this case, this assertion should pass. +Note: A function is always authorized to assign the variables that store +its arguments, there is no need to mention them in the assigns clause. diff --git a/regression/contracts/loop-freeness-check/main.c b/regression/contracts/loop-freeness-check/main.c new file mode 100644 index 00000000000..3840c6dcaec --- /dev/null +++ b/regression/contracts/loop-freeness-check/main.c @@ -0,0 +1,16 @@ +int foo(int *arr) + // clang-format off + __CPROVER_assigns(__CPROVER_POINTER_OBJECT(arr)) +// clang-format off +{ + for(int i = 0; i < 10; i++) + arr[i] = i; + + return 0; +} + +int main() +{ + int arr[10]; + foo(arr); +} diff --git a/regression/contracts/loop-freeness-check/test.desc b/regression/contracts/loop-freeness-check/test.desc new file mode 100644 index 00000000000..a1dc7477d0c --- /dev/null +++ b/regression/contracts/loop-freeness-check/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--enforce-contract foo +^--- begin invariant violation report ---$ +^Invariant check failed$ +^Condition: is_loop_free\(.*\) +^Reason: Loops remain in function 'foo', assigns clause checking instrumentation cannot be applied\.$ +^EXIT=(127|134)$ +^SIGNAL=0$ +-- +-- +This test checks that loops that remain in the program when attempting to +instrument assigns clauses are detected and trigger an INVARIANT. diff --git a/regression/contracts/quantifiers-exists-ensures-enforce/main.c b/regression/contracts/quantifiers-exists-ensures-enforce/main.c index 1194c2968de..bfdc2e43d77 100644 --- a/regression/contracts/quantifiers-exists-ensures-enforce/main.c +++ b/regression/contracts/quantifiers-exists-ensures-enforce/main.c @@ -7,10 +7,16 @@ int f1(int *arr) }) // clang-format on { - for(int i = 0; i < 10; i++) - { - arr[i] = i; - } + arr[0] = 0; + arr[1] = 1; + arr[2] = 2; + arr[3] = 3; + arr[4] = 4; + arr[5] = 5; + arr[6] = 6; + arr[7] = 7; + arr[8] = 8; + arr[9] = 9; return 0; } @@ -24,10 +30,16 @@ int f2(int *arr) }) // clang-format on { - for(int i = 0; i < 10; i++) - { - arr[i] = 0; - } + arr[0] = 0; + arr[1] = 1; + arr[2] = 2; + arr[3] = 3; + arr[4] = 4; + arr[5] = 5; + arr[6] = 6; + arr[7] = 7; + arr[8] = 8; + arr[9] = 9; return 0; } diff --git a/regression/contracts/quantifiers-exists-requires-enforce/main.c b/regression/contracts/quantifiers-exists-requires-enforce/main.c index 7985f57de3b..c74bbfbb009 100644 --- a/regression/contracts/quantifiers-exists-requires-enforce/main.c +++ b/regression/contracts/quantifiers-exists-requires-enforce/main.c @@ -1,7 +1,7 @@ #include #include -#define MAX_LEN 64 +#define MAX_LEN 10 // clang-format off bool f1(int *arr, int len) @@ -18,11 +18,27 @@ bool f1(int *arr, int len) // clang-format on { bool found_four = false; - for(int i = 0; i <= MAX_LEN; i++) - { - if(i < len) - found_four |= (arr[i] == 4); - } + if(0 < len) + found_four |= (arr[0] == 4); + if(1 < len) + found_four |= (arr[1] == 4); + if(2 < len) + found_four |= (arr[2] == 4); + if(3 < len) + found_four |= (arr[3] == 4); + if(4 < len) + found_four |= (arr[4] == 4); + if(5 < len) + found_four |= (arr[5] == 4); + if(6 < len) + found_four |= (arr[6] == 4); + if(7 < len) + found_four |= (arr[7] == 4); + if(8 < len) + found_four |= (arr[8] == 4); + + if(9 < len) + found_four |= (arr[9] == 4); // clang-format off return (len > 0 ==> found_four); diff --git a/regression/contracts/quantifiers-forall-ensures-enforce/main.c b/regression/contracts/quantifiers-forall-ensures-enforce/main.c index cceba46be58..3e6335ab1f3 100644 --- a/regression/contracts/quantifiers-forall-ensures-enforce/main.c +++ b/regression/contracts/quantifiers-forall-ensures-enforce/main.c @@ -1,6 +1,6 @@ #include -#define MAX_LEN 16 +#define MAX_LEN 10 // clang-format off int f1(int *arr, int len) @@ -12,11 +12,27 @@ int f1(int *arr, int len) }) // clang-format on { - for(int i = 0; i < MAX_LEN; i++) - { - if(i < len) - arr[i] = 0; - } + if(0 < len) + arr[0] = 0; + if(1 < len) + arr[1] = 0; + if(2 < len) + arr[2] = 0; + if(3 < len) + arr[3] = 0; + if(4 < len) + arr[4] = 0; + if(5 < len) + arr[5] = 0; + if(6 < len) + arr[6] = 0; + if(7 < len) + arr[7] = 0; + if(8 < len) + arr[8] = 0; + if(9 < len) + arr[9] = 0; + return 0; } diff --git a/regression/contracts/quantifiers-forall-ensures-enforce/test.desc b/regression/contracts/quantifiers-forall-ensures-enforce/test.desc index 87a1b4d333e..b5a17935c58 100644 --- a/regression/contracts/quantifiers-forall-ensures-enforce/test.desc +++ b/regression/contracts/quantifiers-forall-ensures-enforce/test.desc @@ -4,10 +4,11 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$ -^\[f1.\d+\] line \d+ Check that arr\[\(.*\)i\] is assignable: SUCCESS$ +^\[f1.\d+\] line \d+ Check that arr\[\(.*\)\d\] is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring +^\[f1.\d+\] line \d+ Check that arr\[\(.*\)\d\] is assignable: FAILURE$ -- The purpose of this test is to ensure that we can safely use __CPROVER_forall within positive contexts (enforced ENSURES clauses). diff --git a/regression/contracts/quantifiers-forall-requires-enforce/main.c b/regression/contracts/quantifiers-forall-requires-enforce/main.c index fe0da19e0ca..2040549f0f4 100644 --- a/regression/contracts/quantifiers-forall-requires-enforce/main.c +++ b/regression/contracts/quantifiers-forall-requires-enforce/main.c @@ -12,8 +12,16 @@ bool f1(int *arr) // clang-format on { bool is_identity = true; - for(int i = 0; i < 10; ++i) - is_identity &= (arr[i] == i); + is_identity &= (arr[0] == 0); + is_identity &= (arr[1] == 1); + is_identity &= (arr[2] == 2); + is_identity &= (arr[3] == 3); + is_identity &= (arr[4] == 4); + is_identity &= (arr[5] == 5); + is_identity &= (arr[6] == 6); + is_identity &= (arr[7] == 7); + is_identity &= (arr[8] == 8); + is_identity &= (arr[9] == 9); return is_identity; } diff --git a/regression/contracts/quantifiers-nested-01/main.c b/regression/contracts/quantifiers-nested-01/main.c index 2e1d0667115..f44da69dd13 100644 --- a/regression/contracts/quantifiers-nested-01/main.c +++ b/regression/contracts/quantifiers-nested-01/main.c @@ -11,10 +11,16 @@ int f1(int *arr) }) // clang-format on { - for(int i = 0; i < 10; i++) - { - arr[i] = i; - } + arr[0] = 0; + arr[1] = 1; + arr[2] = 2; + arr[3] = 3; + arr[4] = 4; + arr[5] = 5; + arr[6] = 6; + arr[7] = 7; + arr[8] = 8; + arr[9] = 9; return 0; } diff --git a/regression/contracts/quantifiers-nested-03/main.c b/regression/contracts/quantifiers-nested-03/main.c index e7bf048ddcf..ca586ae9f3e 100644 --- a/regression/contracts/quantifiers-nested-03/main.c +++ b/regression/contracts/quantifiers-nested-03/main.c @@ -10,10 +10,16 @@ __CPROVER_assigns(__CPROVER_POINTER_OBJECT(arr)) ) // clang-format on { - for(int i = 0; i < 10; i++) - { - arr[i] = i; - } + arr[0] = 0; + arr[1] = 1; + arr[2] = 2; + arr[3] = 3; + arr[4] = 4; + arr[5] = 5; + arr[6] = 6; + arr[7] = 7; + arr[8] = 8; + arr[9] = 9; return 0; } diff --git a/regression/contracts/test_aliasing_ensure/main.c b/regression/contracts/test_aliasing_ensure/main.c index 3c4f94e863d..f68c823dc5a 100644 --- a/regression/contracts/test_aliasing_ensure/main.c +++ b/regression/contracts/test_aliasing_ensure/main.c @@ -6,7 +6,7 @@ int z; // clang-format off int foo(int *x, int *y) - __CPROVER_assigns(z, *x, y) + __CPROVER_assigns(z, *x) __CPROVER_requires( __CPROVER_is_fresh(x, sizeof(int)) && *x > 0 && diff --git a/regression/contracts/test_aliasing_ensure_indirect/main.c b/regression/contracts/test_aliasing_ensure_indirect/main.c index bac705ee9e3..125da5a16ac 100644 --- a/regression/contracts/test_aliasing_ensure_indirect/main.c +++ b/regression/contracts/test_aliasing_ensure_indirect/main.c @@ -2,7 +2,7 @@ #include #include -void bar(int *z) __CPROVER_assigns(z) +void bar(int *z) __CPROVER_assigns() __CPROVER_ensures(__CPROVER_is_fresh(z, sizeof(int))) { z = malloc(sizeof(*z)); @@ -11,7 +11,7 @@ void bar(int *z) __CPROVER_assigns(z) // clang-format off int foo(int *x, int *y) - __CPROVER_assigns(*x, y) + __CPROVER_assigns(*x) __CPROVER_requires( __CPROVER_is_fresh(x, sizeof(int)) && *x > 0 && diff --git a/regression/contracts/test_aliasing_ensure_indirect/test.desc b/regression/contracts/test_aliasing_ensure_indirect/test.desc index 69df6b6065c..4c9575dddb9 100644 --- a/regression/contracts/test_aliasing_ensure_indirect/test.desc +++ b/regression/contracts/test_aliasing_ensure_indirect/test.desc @@ -4,7 +4,6 @@ main.c ^EXIT=0$ ^SIGNAL=0$ \[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS -\[bar.\d+\] line \d+ Check that z is assignable: SUCCESS \[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS \[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS ^VERIFICATION SUCCESSFUL$ diff --git a/src/goto-instrument/contracts/assigns.cpp b/src/goto-instrument/contracts/assigns.cpp index bd612a25ff1..6e17935a63e 100644 --- a/src/goto-instrument/contracts/assigns.cpp +++ b/src/goto-instrument/contracts/assigns.cpp @@ -159,6 +159,15 @@ assigns_clauset::conditional_address_ranget::generate_unsafe_inclusion_check( pointer_offset(upper_bound_address_var)}}); } +bool assigns_clauset::conditional_address_ranget::maybe_alive( + cfg_infot &cfg_info) const +{ + if(can_cast_expr(source_expr)) + return cfg_info.is_maybe_alive(to_symbol_expr(source_expr)); + + return true; +} + assigns_clauset::assigns_clauset( const exprt::operandst &assigns, const messaget &log, @@ -192,14 +201,26 @@ void assigns_clauset::remove_from_write_set(const exprt &target_expr) } exprt assigns_clauset::generate_inclusion_check( - const conditional_address_ranget &lhs) const + const conditional_address_ranget &lhs, + optionalt &cfg_info_opt) const { if(write_set.empty()) return not_exprt{lhs.validity_condition_var}; exprt::operandst conditions{not_exprt{lhs.validity_condition_var}}; - for(const auto &target : write_set) - conditions.push_back(target.generate_unsafe_inclusion_check(lhs)); + + if(cfg_info_opt.has_value()) + { + auto &cfg_info = cfg_info_opt.value(); + for(const auto &target : write_set) + if(target.maybe_alive(cfg_info)) + conditions.push_back(target.generate_unsafe_inclusion_check(lhs)); + } + else + { + for(const auto &target : write_set) + conditions.push_back(target.generate_unsafe_inclusion_check(lhs)); + } return disjunction(conditions); } diff --git a/src/goto-instrument/contracts/assigns.h b/src/goto-instrument/contracts/assigns.h index 3059c9e882c..f43251347de 100644 --- a/src/goto-instrument/contracts/assigns.h +++ b/src/goto-instrument/contracts/assigns.h @@ -47,6 +47,11 @@ class assigns_clauset } }; + /// Returns true whenever this CAR's `source_expr` and associated address + /// range may be alive at the instruction currently pointed to by + /// `cfg_info.target`. + bool maybe_alive(cfg_infot &cfg_info) const; + const exprt source_expr; const source_locationt &location; const assigns_clauset &parent; @@ -82,7 +87,9 @@ class assigns_clauset write_sett::const_iterator add_to_write_set(const exprt &); void remove_from_write_set(const exprt &); - exprt generate_inclusion_check(const conditional_address_ranget &) const; + exprt generate_inclusion_check( + const conditional_address_ranget &lhs, + optionalt &cfg_info_opt) const; const write_sett &get_write_set() const { diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 325ed89226a..6c74c51d0c5 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -16,6 +16,7 @@ Date: February 2016 #include #include +#include #include #include @@ -307,9 +308,19 @@ void code_contractst::check_apply_loop_contracts( goto_function.body, loop_head, snapshot_instructions); }; + optionalt cfg_empty_info; + // Perform write set instrumentation on the entire loop. check_frame_conditions( - function_name, goto_function.body, loop_head, loop_end, loop_assigns); + function_name, + goto_function.body, + loop_head, + loop_end, + loop_assigns, + // do not skip checks on function parameter assignments + skipt::DontSkip, + // do not use CFG info for now + cfg_empty_info); havoc_assigns_targetst havoc_gen(to_havoc, ns); havoc_gen.append_full_havoc_code( @@ -908,23 +919,25 @@ goto_functionst &code_contractst::get_goto_functions() } void code_contractst::instrument_assign_statement( - goto_programt::instructionst::iterator &instruction_it, + goto_programt::targett &instruction_it, goto_programt &program, - assigns_clauset &assigns_clause) + assigns_clauset &assigns_clause, + optionalt &cfg_info_opt) { - INVARIANT( - instruction_it->is_assign(), - "The first instruction of instrument_assign_statement should always be" - " an assignment"); add_inclusion_check( - program, assigns_clause, instruction_it, instruction_it->assign_lhs()); + program, + assigns_clause, + instruction_it, + instruction_it->assign_lhs(), + cfg_info_opt); } void code_contractst::instrument_call_statement( - goto_programt::instructionst::iterator &instruction_it, + goto_programt::targett &instruction_it, const irep_idt &function, goto_programt &body, - assigns_clauset &assigns) + assigns_clauset &assigns, + optionalt &cfg_info_opt) { INVARIANT( instruction_it->is_function_call(), @@ -962,7 +975,8 @@ void code_contractst::instrument_call_statement( body, assigns, instruction_it, - pointer_object(instruction_it->call_arguments().front())); + pointer_object(instruction_it->call_arguments().front()), + cfg_info_opt); // skip all invalidation business if we're freeing invalid memory goto_programt alias_checking_instructions, skip_program; @@ -1122,10 +1136,8 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function) return true; } - if(check_for_looped_mallocs(function_obj->second.body)) - { - return true; - } + const auto &goto_function = function_obj->second; + auto &function_body = function_obj->second.body; // Get assigns clause for function const symbolt &target = ns.lookup(function); @@ -1136,21 +1148,9 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function) function, symbol_table); - // detect and add static local variables + // Detect and add static local variables assigns.add_static_locals_to_write_set(goto_functions, function); - // Add formal parameters to write set - for(const auto ¶m : to_code_type(target.type).parameters()) - assigns.add_to_write_set(ns.lookup(param.get_identifier()).symbol_expr()); - - auto instruction_it = function_obj->second.body.instructions.begin(); - for(const auto &car : assigns.get_write_set()) - { - auto snapshot_instructions = car.generate_snapshot_instructions(); - insert_before_swap_and_advance( - function_obj->second.body, instruction_it, snapshot_instructions); - }; - // Full inlining of the function body // Inlining is performed so that function calls to a same function // occurring under different write sets get instrumented specifically @@ -1162,38 +1162,147 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function) decorated.get_recursive_function_warnings_count() == 0, "Recursive functions found during inlining"); - // restore internal invariants + // Clean up possible fake loops that are due to `IF 0!=0 GOTO i` instructions + simplify_gotos(function_body, ns); + + // Restore internal coherence in the programs + goto_functions.update(); + + INVARIANT( + is_loop_free(function_body, ns, log), + "Loops remain in function '" + id2string(function) + + "', assigns clause checking instrumentation cannot be applied."); + + // Create a deep copy of the original goto_function object + // and compute static control flow graph information on it + goto_functiont goto_function_orig; + goto_function_orig.copy_from(goto_function); + cfg_infot cfg_info(ns, goto_function_orig); + optionalt cfg_info_opt{cfg_info}; + + // Add formal parameters to write set + for(const auto ¶m : to_code_type(target.type).parameters()) + assigns.add_to_write_set(ns.lookup(param.get_identifier()).symbol_expr()); + + auto instruction_it = function_body.instructions.begin(); + for(const auto &car : assigns.get_write_set()) + { + auto snapshot_instructions = car.generate_snapshot_instructions(); + insert_before_swap_and_advance( + function_body, instruction_it, snapshot_instructions); + }; + + // Restore internal coherence in the programs goto_functions.update(); // Insert write set inclusion checks. check_frame_conditions( - function_obj->first, - function_obj->second.body, + function, + function_body, instruction_it, - function_obj->second.body.instructions.end(), - assigns); + function_body.instructions.end(), + assigns, + // skip checks on function parameter assignments + skipt::Skip, + cfg_info_opt); return false; } +/// Returns true iff the target instruction is tagged with a +/// 'CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK' pragma. +bool has_disable_assigns_check_pragma( + const goto_programt::const_targett &target) +{ + const auto &pragmas = target->source_location().get_pragmas(); + return pragmas.find(CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK) != pragmas.end(); +} + +/// Returns true iff an `ASSIGN lhs := rhs` instruction must be instrumented. +bool must_check_assign( + const goto_programt::const_targett &target, + code_contractst::skipt skip_parameter_assigns, + const namespacet ns, + const optionalt cfg_info_opt) +{ + if( + const auto &symbol_expr = + expr_try_dynamic_cast(target->assign_lhs())) + { + if( + skip_parameter_assigns == code_contractst::skipt::DontSkip && + ns.lookup(symbol_expr->get_identifier()).is_parameter) + return true; + + if(cfg_info_opt.has_value()) + return !cfg_info_opt.value().is_local(symbol_expr->get_identifier()); + } + + return true; +} + +/// Returns true iff a `DECL x` must be added to the local write set. +/// +/// A variable is called 'dirty' if its address gets taken at some point in +/// the program. +/// +/// Assuming the goto program is obtained from a structured C program that +/// passed C compiler checks, non-dirty variables can only be assigned to +/// directly by name, cannot escape their lexical scope, and are always safe +/// to assign. Hence, we only track dirty variables in the write set. +bool must_track_decl( + const goto_programt::const_targett &target, + const optionalt &cfg_info_opt) +{ + if(cfg_info_opt.has_value()) + return cfg_info_opt.value().is_not_local_or_dirty_local( + target->decl_symbol().get_identifier()); + + // Unless proved non-dirty by the CFG analysis we assume it is dirty. + return true; +} + +/// Returns true iff a `DEAD x` must be processed to upate the local write set. +/// The conditions are the same than for tracking a `DECL x` instruction. +bool must_track_dead( + const goto_programt::const_targett &target, + const optionalt &cfg_info_opt) +{ + // Unless proved non-dirty by the CFG analysis we assume it is dirty. + if(!cfg_info_opt.has_value()) + return true; + + return cfg_info_opt.value().is_not_local_or_dirty_local( + target->dead_symbol().get_identifier()); +} + void code_contractst::check_frame_conditions( const irep_idt &function, goto_programt &body, goto_programt::targett instruction_it, const goto_programt::targett &instruction_end, - assigns_clauset &assigns) + assigns_clauset &assigns, + skipt skip_parameter_assigns, + optionalt &cfg_info_opt) { - for(; instruction_it != instruction_end; ++instruction_it) + while(instruction_it != instruction_end) { - const auto &pragmas = instruction_it->source_location().get_pragmas(); - if(pragmas.find(CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK) != pragmas.end()) + // Skip instructions marked as disabled for assigns clause checking + if(has_disable_assigns_check_pragma(instruction_it)) + { + instruction_it++; + if(cfg_info_opt.has_value()) + cfg_info_opt.value().step(); continue; + } // Do not instrument this instruction again in the future, // since we are going to instrument it now below. add_pragma_disable_assigns_check(*instruction_it); - if(instruction_it->is_decl()) + if( + instruction_it->is_decl() && + must_track_decl(instruction_it, cfg_info_opt)) { // grab the declared symbol const auto &decl_symbol = instruction_it->decl_symbol(); @@ -1205,18 +1314,24 @@ void code_contractst::check_frame_conditions( body, instruction_it, snapshot_instructions); // since CAR was inserted *after* the DECL instruction, // move the instruction pointer backward, - // because the `for` loop takes care of the increment + // because the loop step takes care of the increment instruction_it--; } - else if(instruction_it->is_assign()) + else if( + instruction_it->is_assign() && + must_check_assign( + instruction_it, skip_parameter_assigns, ns, cfg_info_opt)) { - instrument_assign_statement(instruction_it, body, assigns); + instrument_assign_statement(instruction_it, body, assigns, cfg_info_opt); } else if(instruction_it->is_function_call()) { - instrument_call_statement(instruction_it, function, body, assigns); + instrument_call_statement( + instruction_it, function, body, assigns, cfg_info_opt); } - else if(instruction_it->is_dead()) + else if( + instruction_it->is_dead() && + must_track_dead(instruction_it, cfg_info_opt)) { const auto &symbol = instruction_it->dead_symbol(); source_locationt location_no_checks = instruction_it->source_location(); @@ -1232,10 +1347,10 @@ void code_contractst::check_frame_conditions( symbol_car->validity_condition_var, false_exprt{}, instruction_it->source_location()); - // note that the CAR must be invalidated _after_ the DEAD instruction - body.insert_after( + body.insert_before_swap( instruction_it, add_pragma_disable_assigns_check(invalidation_assignment)); + instruction_it++; } else { @@ -1257,8 +1372,14 @@ void code_contractst::check_frame_conditions( { const auto havoc_argument = pointer_object(instruction_it->get_other().operands().front()); - add_inclusion_check(body, assigns, instruction_it, havoc_argument); + add_inclusion_check( + body, assigns, instruction_it, havoc_argument, cfg_info_opt); } + + // Move to the next instruction + instruction_it++; + if(cfg_info_opt.has_value()) + cfg_info_opt.value().step(); } } @@ -1266,10 +1387,11 @@ const assigns_clauset::conditional_address_ranget code_contractst::add_inclusion_check( goto_programt &program, const assigns_clauset &assigns, - goto_programt::instructionst::iterator &instruction_it, - const exprt &expr) + goto_programt::targett &instruction_it, + const exprt &lhs, + optionalt &cfg_info_opt) { - const assigns_clauset::conditional_address_ranget car{assigns, expr}; + const assigns_clauset::conditional_address_ranget car{assigns, lhs}; auto snapshot_instructions = car.generate_snapshot_instructions(); insert_before_swap_and_advance( program, instruction_it, snapshot_instructions); @@ -1279,9 +1401,9 @@ code_contractst::add_inclusion_check( instruction_it->source_location_nonconst(); disable_pointer_checks(location_no_checks); location_no_checks.set_comment( - "Check that " + from_expr(ns, expr.id(), expr) + " is assignable"); + "Check that " + from_expr(ns, lhs.id(), lhs) + " is assignable"); assertion.add(goto_programt::make_assertion( - assigns.generate_inclusion_check(car), location_no_checks)); + assigns.generate_inclusion_check(car, cfg_info_opt), location_no_checks)); insert_before_swap_and_advance(program, instruction_it, assertion); return car; diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index 6514aada79e..bc0313c9595 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -28,6 +28,7 @@ Date: February 2016 #include #include +#include #include #include "assigns.h" @@ -110,6 +111,13 @@ class code_contractst namespacet ns; + /// Tells wether to skip or not skip an action + enum class skipt + { + DontSkip, + Skip + }; + protected: symbol_tablet &symbol_table; goto_functionst &goto_functions; @@ -125,22 +133,38 @@ class code_contractst /// Instrument functions to check frame conditions. bool check_frame_conditions_function(const irep_idt &function); - /// Insert assertion statements into the goto program to ensure that + /// \brief Insert assertion statements into the goto program to ensure that /// assigned memory is within the assignable memory frame. + /// + /// \param function Name of the function getting instrumented. + /// \param body Body of the function getting instrumented. + /// \param instruction_it Iterator to the instruction from which to start + /// instrumentation (inclusive). + /// \param instruction_end Iterator to the instruction at which to stop + /// instrumentation (exclusive). + /// \param assigns Assigns clause of the function (its write set attribute + /// gets extended during the instrumentation). + /// \param skip_parameter_assigns If true, will cause assignments to symbol + /// marked as is_parameter to not be instrumented. + /// \param cfg_info_opt Control flow graph information can will be used + /// for write set optimisation if available. void check_frame_conditions( - const irep_idt &, - goto_programt &, - goto_programt::targett, - const goto_programt::targett &, - assigns_clauset &); + const irep_idt &function, + goto_programt &body, + goto_programt::targett instruction_it, + const goto_programt::targett &instruction_end, + assigns_clauset &assigns, + skipt skip_parameter_assigns, + optionalt &cfg_info_opt); /// Inserts an assertion into the goto program to ensure that /// an expression is within the assignable memory frame. const assigns_clauset::conditional_address_ranget add_inclusion_check( - goto_programt &, - const assigns_clauset &, - goto_programt::instructionst::iterator &, - const exprt &); + goto_programt &program, + const assigns_clauset &assigns, + goto_programt::targett &instruction_it, + const exprt &lhs, + optionalt &cfg_info_opt); /// Check if there are any malloc statements which may be repeated because of /// a goto statement that jumps back. @@ -150,18 +174,20 @@ class code_contractst /// instruction_it, to ensure that the left-hand-side of the assignment /// is "included" in the (conditional address ranges in the) write set. void instrument_assign_statement( - goto_programt::instructionst::iterator &, - goto_programt &, - assigns_clauset &); + goto_programt::targett &instruction_it, + goto_programt &program, + assigns_clauset &assigns_clause, + optionalt &cfg_info_opt); /// Inserts an assertion into program immediately before the function call at /// instruction_it, to ensure that all memory locations written to by the // callee are "included" in the (conditional address ranges in the) write set. void instrument_call_statement( - goto_programt::instructionst::iterator &, - const irep_idt &, - goto_programt &, - assigns_clauset &); + goto_programt::targett &instruction_it, + const irep_idt &function, + goto_programt &body, + assigns_clauset &assigns, + optionalt &cfg_info_opt); /// Apply loop contracts, whenever available, to all loops in `function`. /// Loop invariants, loop variants, and loop assigns clauses. @@ -173,10 +199,10 @@ class code_contractst /// non-deterministic assignments for the write set, and assumptions /// based on ensures clauses. bool apply_function_contract( - const irep_idt &, - const source_locationt &, - goto_programt &, - goto_programt::targett &); + const irep_idt &function, + const source_locationt &location, + goto_programt &function_body, + goto_programt::targett &target); /// Instruments `wrapper_function` adding assumptions based on requires /// clauses and assertions based on ensures clauses. diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index 95185dd4dd1..607038d9e87 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -10,9 +10,13 @@ Date: September 2021 #include "utils.h" +#include #include +#include +#include #include #include +#include goto_programt::instructiont & add_pragma_disable_assigns_check(goto_programt::instructiont &instr) @@ -163,3 +167,64 @@ void disable_pointer_checks(source_locationt &source_location) source_location.add_pragma("disable:pointer-primitive-check"); source_location.add_pragma("disable:pointer-overflow-check"); } + +void simplify_gotos(goto_programt &goto_program, namespacet &ns) +{ + for(auto &instruction : goto_program.instructions) + { + if( + instruction.is_goto() && + simplify_expr(instruction.get_condition(), ns).is_false()) + instruction.turn_into_skip(); + } +} + +bool is_loop_free( + const goto_programt &goto_program, + namespacet &ns, + messaget &log) +{ + // create cfg from instruction list + cfg_baset cfg; + cfg(goto_program); + + // check that all nodes are there + INVARIANT( + goto_program.instructions.size() == cfg.size(), + "Instruction list vs CFG size mismatch."); + + // compute SCCs + using idxt = graph_nodet::node_indext; + std::vector node_to_scc(cfg.size(), -1); + auto nof_sccs = cfg.SCCs(node_to_scc); + + // compute size of each SCC + std::vector scc_size(nof_sccs, 0); + for(auto scc : node_to_scc) + { + INVARIANT( + 0 <= scc && scc < nof_sccs, "Could not determine SCC for instruction"); + scc_size[scc]++; + } + + // check they are all of size 1 + for(size_t scc_id = 0; scc_id < nof_sccs; scc_id++) + { + auto size = scc_size[scc_id]; + if(size > 1) + { + log.error() << "Found CFG SCC with size " << size << messaget::eom; + for(const auto &node_id : node_to_scc) + { + if(node_to_scc[node_id] == scc_id) + { + const auto &pc = cfg[node_id].PC; + goto_program.output_instruction(ns, "", log.error(), *pc); + log.error() << messaget::eom; + } + } + return false; + } + } + return true; +} diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h index 1614ce023a3..3ff656953a9 100644 --- a/src/goto-instrument/contracts/utils.h +++ b/src/goto-instrument/contracts/utils.h @@ -13,10 +13,16 @@ Date: September 2021 #include +#include +#include + #include #include +#include +#include + #define CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK "contracts:disable:assigns-check" /// \brief A class that overrides the low-level havocing functions in the base @@ -112,7 +118,7 @@ void insert_before_swap_and_advance( /// \param mode: The mode for the new symbol, e.g. ID_C, ID_java. /// \param symtab: The symbol table to which the new symbol is to be added. /// \param suffix: Suffix to use to generate the unique name -/// \param is_auxiliary: Do not print symbol in traces if true (default = false) +/// \param is_auxiliary: Do not print symbol in traces if true (default = true) /// \return The new symbolt object. const symbolt &new_tmp_symbol( const typet &type, @@ -120,9 +126,84 @@ const symbolt &new_tmp_symbol( const irep_idt &mode, symbol_table_baset &symtab, std::string suffix = "tmp_cc", - bool is_auxiliary = false); + bool is_auxiliary = true); /// Add disable pragmas for all pointer checks on the given location void disable_pointer_checks(source_locationt &source_location); +/// Turns goto instructions `IF cond GOTO label` where the condition +/// statically simplifies to `false` into SKIP instructions. +void simplify_gotos(goto_programt &goto_program, namespacet &ns); + +/// Returns true iff the given program is loop-free, +/// i.e. if each SCC of its CFG contains a single element. +bool is_loop_free( + const goto_programt &goto_program, + namespacet &ns, + messaget &log); + +/// Stores information about a goto function computed from its CFG, +/// together with a `target` iterator into the instructions of the function. +/// +/// The methods of this class provide information about identifiers at +/// the current `target` instruction to allow simplifying assigns +/// clause checking assertions. +class cfg_infot +{ +public: + cfg_infot(const namespacet &_ns, goto_functiont &_goto_function) + : ns(_ns), + goto_function(_goto_function), + target(goto_function.body.instructions.begin()), + dirty_analysis(goto_function), + locals(goto_function) + { + } + + /// Steps the `target` iterator forward. + void step() + { + target++; + } + + /// Returns true iff the given `ident` is either not a `goto_function` local + /// or is a local that is dirty. + bool is_not_local_or_dirty_local(irep_idt ident) const + { + if(is_local(ident)) + return dirty_analysis.get_dirty_ids().find(ident) != + dirty_analysis.get_dirty_ids().end(); + else + return true; + } + + /// Returns true whenever the given `symbol_expr` might be alive + /// at the current `target` instruction. + bool is_maybe_alive(const symbol_exprt &symbol_expr) + { + // TODO query the static analysis when available + return true; + } + + /// Returns true iff `ident` is a local (or parameter) of `goto_function`. + bool is_local(irep_idt ident) const + { + const auto &symbol = ns.lookup(ident); + return locals.is_local(ident) || symbol.is_parameter; + } + + /// returns the current target instruction + const goto_programt::targett &get_current_target() const + { + return target; + } + +private: + const namespacet &ns; + goto_functiont &goto_function; + goto_programt::targett target; + const dirtyt dirty_analysis; + const localst locals; +}; + #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H