diff --git a/regression/contracts/assigns_replace_03/test.desc b/regression/contracts/assigns_replace_03/test.desc index 93cd2e13787..9cf224b7c34 100644 --- a/regression/contracts/assigns_replace_03/test.desc +++ b/regression/contracts/assigns_replace_03/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --replace-all-calls-with-contracts ^EXIT=0$ @@ -7,3 +7,7 @@ main.c -- -- This test checks that a havocked variable can be constrained by a function post-condition. + +Known Bug: +Currently, there is a bug when char variables are being passed to +__CPROVER_w_ok(). See GitHub issue #6106 for further details. diff --git a/regression/contracts/assigns_validity_pointer_01/main.c b/regression/contracts/assigns_validity_pointer_01/main.c new file mode 100644 index 00000000000..9bd875890bc --- /dev/null +++ b/regression/contracts/assigns_validity_pointer_01/main.c @@ -0,0 +1,36 @@ +#include +#include + +int *z; + +void bar(int *x, int *y) __CPROVER_assigns(*x, *y) __CPROVER_requires(*x > 0) + __CPROVER_ensures(*x == 3 && (y == NULL || *y == 5)) +{ + *x = 3; + if(y != NULL) + *y = 5; +} + +void baz() __CPROVER_assigns(*z) __CPROVER_ensures(z == NULL || *z == 7) +{ + if(z != NULL) + *z = 7; +} + +void foo(int *x) __CPROVER_assigns(*x) __CPROVER_requires(*x > 0) + __CPROVER_ensures(*x == 3) +{ + bar(x, NULL); + z == NULL; + baz(); +} + +int main() +{ + int n; + foo(&n); + + assert(n == 3); + assert(z == NULL || *z == 7); + return 0; +} diff --git a/regression/contracts/assigns_validity_pointer_01/test.desc b/regression/contracts/assigns_validity_pointer_01/test.desc new file mode 100644 index 00000000000..345bde8483c --- /dev/null +++ b/regression/contracts/assigns_validity_pointer_01/test.desc @@ -0,0 +1,29 @@ +CORE +main.c +--enforce-contract foo --replace-call-with-contract bar --replace-call-with-contract baz +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +SUCCESS +// bar +ASSERT \*x > 0 +IF !\(\*x == 3\) THEN GOTO \d +IF !\(\(signed int \*\)\(void \*\)0 == \(\(signed int \*\)NULL\)\) THEN GOTO \d +tmp_if_expr = \*\(\(signed int \*\)\(void \*\)0\) == 5 \? TRUE \: FALSE; +tmp_if_expr\$\d = tmp_if_expr \? TRUE : FALSE; +ASSUME tmp_if_expr\$\d +// baz +IF !\(z == \(\(signed int \*\)NULL\)\) THEN GOTO \d +tmp_if_expr\$\d = \*z == 7 \? TRUE : FALSE; +ASSUME tmp_if_expr\$\d +// foo +ASSUME \*tmp_cc\$\d > 0 +ASSERT \*tmp_cc\$\d == 3 +-- +\[3\] file main\.c line 6 assertion: FAILURE +-- +Verification: +This test checks support for a NULL pointer that is assigned to by +a function (bar and baz). Both functions bar and baz are being replaced by +their function contracts, while the calling function foo is being checked +(by enforcing it's function contracts). diff --git a/regression/contracts/assigns_validity_pointer_02/main.c b/regression/contracts/assigns_validity_pointer_02/main.c new file mode 100644 index 00000000000..c1315797495 --- /dev/null +++ b/regression/contracts/assigns_validity_pointer_02/main.c @@ -0,0 +1,36 @@ +#include +#include + +int *z; + +void bar(int *x, int *y) __CPROVER_assigns(*x, *y) __CPROVER_requires(*x > 0) + __CPROVER_ensures(*x == 3 && (y == NULL || *y == 5)) +{ + *x = 3; + if(y != NULL) + *y = 5; +} + +void baz() __CPROVER_assigns(*z) __CPROVER_ensures(z == NULL || *z == 7) +{ + if(z != NULL) + *z = 7; +} + +void foo(int *x) __CPROVER_assigns(*x) __CPROVER_requires(*x > 0) + __CPROVER_ensures(*x == 3) +{ + bar(x, NULL); + *x = 3; + z == NULL; + baz(); +} + +int main() +{ + int n; + foo(&n); + + assert(n == 3); + return 0; +} diff --git a/regression/contracts/assigns_validity_pointer_02/test.desc b/regression/contracts/assigns_validity_pointer_02/test.desc new file mode 100644 index 00000000000..038910fa7bf --- /dev/null +++ b/regression/contracts/assigns_validity_pointer_02/test.desc @@ -0,0 +1,19 @@ +CORE +main.c +--enforce-contract foo +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +//^([foo\.1] line 15 assertion: FAILURE) +// foo +ASSUME \*tmp_cc\$\d > 0 +ASSERT \*tmp_cc\$\d == 3 +-- +\[foo\.1\] line 24 assertion: FAILURE +\[foo\.3\] line 27 assertion: FAILURE +-- +Verification: +This test checks support for a NULL pointer that is assigned to by +a function (bar and baz). The calling function foo is being checked +(by enforcing it's function contracts). As for bar and baz, their +function contracts are ot being considered for this test. diff --git a/regression/contracts/assigns_validity_pointer_03/main.c b/regression/contracts/assigns_validity_pointer_03/main.c new file mode 100644 index 00000000000..a3e68c4f79e --- /dev/null +++ b/regression/contracts/assigns_validity_pointer_03/main.c @@ -0,0 +1,33 @@ +#include +#include + +int *z; + +void bar(int *x, int *y) __CPROVER_assigns(*x, *y) __CPROVER_requires(*x > 0) + __CPROVER_ensures(*x == 3 && *y == 5) +{ +} + +void baz() __CPROVER_assigns(*z) __CPROVER_ensures(*z == 7) +{ +} + +void foo(int *x) __CPROVER_assigns(*x) __CPROVER_requires(*x > 0) + __CPROVER_ensures(*x == 3) +{ + int *y; + bar(x, y); + assert(*y == 5); + + baz(); + assert(*z == 7); +} + +int main() +{ + int n; + foo(&n); + + assert(n == 3); + return 0; +} diff --git a/regression/contracts/assigns_validity_pointer_03/test.desc b/regression/contracts/assigns_validity_pointer_03/test.desc new file mode 100644 index 00000000000..988ad466d7c --- /dev/null +++ b/regression/contracts/assigns_validity_pointer_03/test.desc @@ -0,0 +1,28 @@ +KNOWNBUG +main.c +--enforce-contract foo --replace-call-with-contract bar --replace-call-with-contract baz +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +// bar +ASSERT \*x > 0 +IF !\(\*x == 3\) THEN GOTO \d +tmp_if_expr = \*y == 5 \? TRUE \: FALSE; +ASSUME tmp_if_expr +// baz +ASSUME \*z == 7 +// foo +ASSUME \*tmp_cc\$\d > 0 +ASSERT \*tmp_cc\$\d == 3 +-- +-- +Verification: +This test checks support for an uninitialized pointer that is assigned to by +a function (bar and baz). Both functions bar and baz are being replaced by +their function contracts, while the calling function foo is being checked +(by enforcing it's function contracts). + +Known Bug: +Currently, there is a known issue with __CPROVER_w_ok(ptr, 0) such that it +returns true if ptr is uninitialized. This is not the expected behavior, +therefore, the outcome of this test case is currently incorrect. diff --git a/regression/contracts/assigns_validity_pointer_04/main.c b/regression/contracts/assigns_validity_pointer_04/main.c new file mode 100644 index 00000000000..1042131e090 --- /dev/null +++ b/regression/contracts/assigns_validity_pointer_04/main.c @@ -0,0 +1,34 @@ +#include +#include + +int *z; + +void bar(int *x, int *y) __CPROVER_assigns(*x, *y) __CPROVER_requires(*x > 0) + __CPROVER_ensures(*x == 3 && *y == 5) +{ +} + +void baz() __CPROVER_assigns(*z) __CPROVER_ensures(*z == 7) +{ +} + +void foo(int *x) __CPROVER_assigns(*x) __CPROVER_requires(*x > 0) + __CPROVER_ensures(*x == 3) +{ + int *y = malloc(sizeof(int)); + bar(x, y); + assert(*y == 5); + + z = malloc(sizeof(int)); + baz(); + assert(*z == 7); +} + +int main() +{ + int n; + foo(&n); + + assert(n == 3); + return 0; +} diff --git a/regression/contracts/assigns_validity_pointer_04/test.desc b/regression/contracts/assigns_validity_pointer_04/test.desc new file mode 100644 index 00000000000..f6cee72a7b6 --- /dev/null +++ b/regression/contracts/assigns_validity_pointer_04/test.desc @@ -0,0 +1,23 @@ +CORE +main.c +--enforce-contract foo --replace-call-with-contract bar --replace-call-with-contract baz +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +// bar +ASSERT \*x > 0 +IF !\(\*x == 3\) THEN GOTO \d +tmp_if_expr = \*y == 5 \? TRUE \: FALSE; +ASSUME tmp_if_expr +// baz +ASSUME \*z == 7 +// foo +ASSUME \*tmp_cc\$\d > 0 +ASSERT \*tmp_cc\$\d == 3 +-- +-- +Verification: +This test checks support for a malloced pointer that is assigned to by +a function (bar and baz). Both functions bar and baz are being replaced by +their function contracts, while the calling function foo is being checked +(by enforcing it's function contracts). diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 90b23b9866a..e460dd0431c 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -1524,11 +1524,40 @@ goto_programt assigns_clauset::havoc_code( goto_programt havoc_statements; for(assigns_clause_targett *target : targets) { + // (1) If the assigned target is not a dereference, + // only include the havoc_statement + + // (2) If the assigned target is a dereference, do the following: + + // if(!__CPROVER_w_ok(target, 0)) goto z; + // havoc_statements + // z: skip + + // create the z label + goto_programt tmp_z; + goto_programt::targett z = tmp_z.add(goto_programt::make_skip(location)); + + const auto &target_ptr = target->get_direct_pointer(); + if(to_address_of_expr(target_ptr).object().id() == ID_dereference) + { + // create the condition + exprt condition = + not_exprt(w_ok_exprt(target_ptr, from_integer(0, integer_typet()))); + havoc_statements.add(goto_programt::make_goto(z, condition, location)); + } + + // create havoc_statements for(goto_programt::instructiont instruction : target->havoc_code(location).instructions) { havoc_statements.add(std::move(instruction)); } + + if(to_address_of_expr(target_ptr).object().id() == ID_dereference) + { + // add the z label instruction + havoc_statements.destructive_append(tmp_z); + } } return havoc_statements; } @@ -1577,8 +1606,28 @@ exprt assigns_clauset::compatible_expression( { if(first_iter) { - current_target_compatible = - target->compatible_expression(*called_target); + // TODO: Optimize the validation below and remove code duplication + // See GitHub issue #6105 for further details + + // Validating the called target through __CPROVER_w_ok() is + // only useful when the called target is a dereference + const auto &called_target_ptr = called_target->get_direct_pointer(); + if( + to_address_of_expr(called_target_ptr).object().id() == ID_dereference) + { + // or_exprt is short-circuited, therefore + // target->compatible_expression(*called_target) would not be + // checked on invalid called_targets. + current_target_compatible = or_exprt( + not_exprt( + w_ok_exprt(called_target_ptr, from_integer(0, integer_typet()))), + target->compatible_expression(*called_target)); + } + else + { + current_target_compatible = + target->compatible_expression(*called_target); + } first_iter = false; } else