From d3d58a071becebe1f1c4a47cd0beefa56d0c62aa Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 4 Apr 2019 17:47:44 +0000 Subject: [PATCH 1/3] Always evaluate __CPROVER_{r,w}_ok and add a test We did not have an explicit test of __CPROVER_{r,w}_ok, only implicit ones as we use these predicates in our model of the C library. While preparing a test it became apparent that the predicates are only evaluated when --pointer-check is set. This caused surprising behaviour as a negated predicate would result in failing assertions. Instead, make sure the expression is always evaluated, independent of --pointer-check. This requires always performing a local alias analysis, even when no pointer checks are enabled. --- regression/cbmc/r_w_ok1/main.c | 26 ++++++++++++++++++++++++++ regression/cbmc/r_w_ok1/test.desc | 10 ++++++++++ src/analyses/goto_check.cpp | 9 +++------ 3 files changed, 39 insertions(+), 6 deletions(-) create mode 100644 regression/cbmc/r_w_ok1/main.c create mode 100644 regression/cbmc/r_w_ok1/test.desc diff --git a/regression/cbmc/r_w_ok1/main.c b/regression/cbmc/r_w_ok1/main.c new file mode 100644 index 00000000000..0a24178df9c --- /dev/null +++ b/regression/cbmc/r_w_ok1/main.c @@ -0,0 +1,26 @@ +#include +#include + +int main() +{ + int *p = NULL; + + assert(!__CPROVER_r_ok(p, sizeof(int))); + assert(!__CPROVER_w_ok(p, sizeof(int))); + + p = malloc(sizeof(int)); + + assert(__CPROVER_r_ok(p, 1)); + assert(__CPROVER_w_ok(p, 1)); + assert(__CPROVER_r_ok(p, sizeof(int))); + assert(__CPROVER_w_ok(p, sizeof(int))); + + size_t n; + char *arbitrary_size = malloc(n); + + assert(__CPROVER_r_ok(arbitrary_size, n)); + assert(__CPROVER_w_ok(arbitrary_size, n)); + + assert(__CPROVER_r_ok(arbitrary_size, n + 1)); + assert(__CPROVER_w_ok(arbitrary_size, n + 1)); +} diff --git a/regression/cbmc/r_w_ok1/test.desc b/regression/cbmc/r_w_ok1/test.desc new file mode 100644 index 00000000000..e50051dc10b --- /dev/null +++ b/regression/cbmc/r_w_ok1/test.desc @@ -0,0 +1,10 @@ +CORE +main.c + +__CPROVER_[rw]_ok\(arbitrary_size, n \+ 1\): FAILURE$ +^\*\* 2 of 10 failed +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 9f1fc15813f..da3d59a6cb9 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -1076,9 +1076,7 @@ void goto_checkt::pointer_validity_check( goto_checkt::conditionst goto_checkt::address_check(const exprt &address, const exprt &size) { - if(!enable_pointer_check) - return {}; - + PRECONDITION(local_bitvector_analysis); PRECONDITION(address.type().id() == ID_pointer); const auto &pointer_type = to_pointer_type(address.type()); @@ -1700,9 +1698,8 @@ void goto_checkt::goto_check( bool did_something = false; - if(enable_pointer_check) - local_bitvector_analysis = - util_make_unique(goto_function, ns); + local_bitvector_analysis = + util_make_unique(goto_function, ns); goto_programt &goto_program=goto_function.body; From 52264662c69f358a9f8b89de6e3570cb6bb07cd3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 5 Apr 2019 07:26:03 +0000 Subject: [PATCH 2/3] Support __CPROVER_{r,w}_ok in assignments, assumptions, gotos, returns We previously only evaluated __CPROVER_{r,w}_ok in assertions (without telling anyone that was the case). Instead, evaluate it in all contexts where it might reasonably appear. --- regression/cbmc/r_w_ok2/main.c | 12 ++++++++++ regression/cbmc/r_w_ok2/test.desc | 8 +++++++ src/analyses/goto_check.cpp | 40 ++++++++++++++++++++++++++----- 3 files changed, 54 insertions(+), 6 deletions(-) create mode 100644 regression/cbmc/r_w_ok2/main.c create mode 100644 regression/cbmc/r_w_ok2/test.desc diff --git a/regression/cbmc/r_w_ok2/main.c b/regression/cbmc/r_w_ok2/main.c new file mode 100644 index 00000000000..50f42c16884 --- /dev/null +++ b/regression/cbmc/r_w_ok2/main.c @@ -0,0 +1,12 @@ +#include + +int main() +{ + int *p = (int *)0; + + _Bool not_ok = !__CPROVER_r_ok(p, sizeof(int)); + assert(not_ok); + + if(__CPROVER_w_ok(p, sizeof(int))) + assert(0); +} diff --git a/regression/cbmc/r_w_ok2/test.desc b/regression/cbmc/r_w_ok2/test.desc new file mode 100644 index 00000000000..278f468e130 --- /dev/null +++ b/regression/cbmc/r_w_ok2/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index da3d59a6cb9..b092e2b41f3 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -1718,8 +1718,19 @@ void goto_checkt::goto_check( assertions.clear(); if(i.has_condition()) + { check(i.get_condition()); + if(has_subexpr(i.get_condition(), [](const exprt &expr) { + return expr.id() == ID_r_ok || expr.id() == ID_w_ok; + })) + { + auto rw_ok_cond = rw_ok_check(i.get_condition()); + if(rw_ok_cond.has_value()) + i.set_condition(*rw_ok_cond); + } + } + // magic ERROR label? for(const auto &label : error_labels) { @@ -1762,6 +1773,16 @@ void goto_checkt::goto_check( // the LHS might invalidate any assertion invalidate(code_assign.lhs()); + + if(has_subexpr(code_assign.rhs(), [](const exprt &expr) { + return expr.id() == ID_r_ok || expr.id() == ID_w_ok; + })) + { + exprt &rhs = to_code_assign(i.code).rhs(); + auto rw_ok_cond = rw_ok_check(rhs); + if(rw_ok_cond.has_value()) + rhs = *rw_ok_cond; + } } else if(i.is_function_call()) { @@ -1807,9 +1828,20 @@ void goto_checkt::goto_check( { if(i.code.operands().size()==1) { - check(i.code.op0()); + const code_returnt &code_return = to_code_return(i.code); + check(code_return.return_value()); // the return value invalidate any assertion - invalidate(i.code.op0()); + invalidate(code_return.return_value()); + + if(has_subexpr(code_return.return_value(), [](const exprt &expr) { + return expr.id() == ID_r_ok || expr.id() == ID_w_ok; + })) + { + exprt &return_value = to_code_return(i.code).return_value(); + auto rw_ok_cond = rw_ok_check(return_value); + if(rw_ok_cond.has_value()) + return_value = *rw_ok_cond; + } } } else if(i.is_throw()) @@ -1841,10 +1873,6 @@ void goto_checkt::goto_check( { bool is_user_provided=i.source_location.get_bool("user-provided"); - auto rw_ok_cond = rw_ok_check(i.get_condition()); - if(rw_ok_cond.has_value()) - i.set_condition(*rw_ok_cond); - if((is_user_provided && !enable_assertions && i.source_location.get_property_class()!="error label") || (!is_user_provided && !enable_built_in_assertions)) From 7ecf1f69e859f76b5aa5ae86c2ff2ba9ccae62ef Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 4 Apr 2019 18:51:41 +0000 Subject: [PATCH 3/3] Add test showing limitations of __CPROVER_w_ok We do not currently have a good way of distinguishing lvalues from rvalues, and thus actually treat __CPROVER_w_ok and __CPROVER_r_ok the same. The test shows that this shouldn't always be done. --- regression/cbmc/r_w_ok3/main.c | 8 ++++++++ regression/cbmc/r_w_ok3/test.desc | 12 ++++++++++++ 2 files changed, 20 insertions(+) create mode 100644 regression/cbmc/r_w_ok3/main.c create mode 100644 regression/cbmc/r_w_ok3/test.desc diff --git a/regression/cbmc/r_w_ok3/main.c b/regression/cbmc/r_w_ok3/main.c new file mode 100644 index 00000000000..10944dcd2cd --- /dev/null +++ b/regression/cbmc/r_w_ok3/main.c @@ -0,0 +1,8 @@ +#include + +int main() +{ + const char *str = "foobar"; + assert(!__CPROVER_w_ok(str, 6)); + assert(__CPROVER_r_ok(str, 6)); +} diff --git a/regression/cbmc/r_w_ok3/test.desc b/regression/cbmc/r_w_ok3/test.desc new file mode 100644 index 00000000000..41d4263864c --- /dev/null +++ b/regression/cbmc/r_w_ok3/test.desc @@ -0,0 +1,12 @@ +KNOWNBUG +main.c + +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +We currently do not distinguish __CPROVER_r_ok and __CPROVER_w_ok at the +implementation level. To make a meaningful distinction we would need to have +predicates about lvalues vs rvalues.