From c9a22ab57d7a455cc9c4e9665bf23b1f0c7ca55c Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 25 Sep 2021 17:23:04 +0100 Subject: [PATCH] is_invalid_pointer is now defined as a bi-implication The previous encoding of is_invalid_pointer is an implication, which means that constraints that a pointer is not an invalid pointer have no meaning. This commit changes the encoding to be a bi-implication, using the numerical range of the valid pointers. --- .../cbmc-primitives/r_w_ok_bug/test.desc | 7 +-- .../test-no-cp.desc | 3 +- .../r_w_ok_inconsistent_integer/test.desc | 3 +- .../test-no-cp.desc | 3 +- .../r_w_ok_inconsistent_nondet/test.desc | 3 +- .../cbmc-primitives/same-object-01/main.c | 6 +-- src/solvers/flattening/bv_pointers.cpp | 54 ++++++++----------- src/solvers/flattening/pointer_logic.cpp | 3 -- src/solvers/flattening/pointer_logic.h | 6 --- src/solvers/smt2/smt2_conv.cpp | 33 ++++++++++-- src/solvers/smt2/smt2_conv.h | 4 ++ src/solvers/smt2/smt2_dec.cpp | 2 + 12 files changed, 66 insertions(+), 61 deletions(-) diff --git a/regression/cbmc-primitives/r_w_ok_bug/test.desc b/regression/cbmc-primitives/r_w_ok_bug/test.desc index e47b34c18b2..b04f084c0aa 100644 --- a/regression/cbmc-primitives/r_w_ok_bug/test.desc +++ b/regression/cbmc-primitives/r_w_ok_bug/test.desc @@ -1,10 +1,7 @@ CORE main.c --pointer-check --no-simplify --no-propagation -^\[main.pointer_dereference.\d+\] line 8 dereference failure: pointer outside object bounds in \*p1: FAILURE$ -^\*\* 1 of \d+ failed -^VERIFICATION FAILED$ -^EXIT=10$ +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ ^SIGNAL=0$ -- -^warning: ignoring diff --git a/regression/cbmc-primitives/r_w_ok_inconsistent_integer/test-no-cp.desc b/regression/cbmc-primitives/r_w_ok_inconsistent_integer/test-no-cp.desc index 98ce59cbf3e..8733961bde6 100644 --- a/regression/cbmc-primitives/r_w_ok_inconsistent_integer/test-no-cp.desc +++ b/regression/cbmc-primitives/r_w_ok_inconsistent_integer/test-no-cp.desc @@ -1,11 +1,10 @@ -FUTURE +CORE main.c --pointer-check --no-simplify --no-propagation ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -^warning: ignoring -- Tests that an inconsistent assumption involving a pointer initialized to an integer address not pointing to memory and __CPROVER_r_ok() can be detected via diff --git a/regression/cbmc-primitives/r_w_ok_inconsistent_integer/test.desc b/regression/cbmc-primitives/r_w_ok_inconsistent_integer/test.desc index 041ac2e31d9..400351aaed7 100644 --- a/regression/cbmc-primitives/r_w_ok_inconsistent_integer/test.desc +++ b/regression/cbmc-primitives/r_w_ok_inconsistent_integer/test.desc @@ -1,11 +1,10 @@ -FUTURE +CORE main.c --pointer-check ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -^warning: ignoring -- Tests that an inconsistent assumption involving a pointer initialized to an integer address not pointing to memory and __CPROVER_r_ok() can be detected via diff --git a/regression/cbmc-primitives/r_w_ok_inconsistent_nondet/test-no-cp.desc b/regression/cbmc-primitives/r_w_ok_inconsistent_nondet/test-no-cp.desc index 2f9ebc57929..c86457b7162 100644 --- a/regression/cbmc-primitives/r_w_ok_inconsistent_nondet/test-no-cp.desc +++ b/regression/cbmc-primitives/r_w_ok_inconsistent_nondet/test-no-cp.desc @@ -1,11 +1,10 @@ -FUTURE +CORE main.c --pointer-check --no-simplify --no-propagation ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -^warning: ignoring -- Tests that an inconsistent assumption involving a nondet pointer and __CPROVER_r_ok() can be detected via assert(0). We use --no-simplify and diff --git a/regression/cbmc-primitives/r_w_ok_inconsistent_nondet/test.desc b/regression/cbmc-primitives/r_w_ok_inconsistent_nondet/test.desc index 34641ac0acf..9991b71a596 100644 --- a/regression/cbmc-primitives/r_w_ok_inconsistent_nondet/test.desc +++ b/regression/cbmc-primitives/r_w_ok_inconsistent_nondet/test.desc @@ -1,11 +1,10 @@ -FUTURE +CORE main.c --pointer-check ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -^warning: ignoring -- Tests that an inconsistent assumption involving a nondet pointer and __CPROVER_r_ok() can be detected via assert(0). diff --git a/regression/cbmc-primitives/same-object-01/main.c b/regression/cbmc-primitives/same-object-01/main.c index 363c1dd4c1c..dfa0f7f120f 100644 --- a/regression/cbmc-primitives/same-object-01/main.c +++ b/regression/cbmc-primitives/same-object-01/main.c @@ -4,10 +4,10 @@ void main() { char *p = malloc(1); - assert(__CPROVER_POINTER_OBJECT(p) == 2); + assert(__CPROVER_POINTER_OBJECT(p) == 1); assert( - __CPROVER_same_object(p, (char *)((size_t)2 << (sizeof(char *) * 8 - 8)))); + __CPROVER_same_object(p, (char *)((size_t)1 << (sizeof(char *) * 8 - 8)))); assert( - !__CPROVER_same_object(p, (char *)((size_t)3 << (sizeof(char *) * 8 - 8)))); + !__CPROVER_same_object(p, (char *)((size_t)2 << (sizeof(char *) * 8 - 8)))); } diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index 0290ccae0f7..3bce94519c8 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -119,37 +119,7 @@ literalt bv_pointerst::convert_rest(const exprt &expr) const exprt::operandst &operands=expr.operands(); - if(expr.id() == ID_is_invalid_pointer) - { - if(operands.size()==1 && - operands[0].type().id()==ID_pointer) - { - const bvt &bv=convert_bv(operands[0]); - - if(!bv.empty()) - { - const pointer_typet &type = to_pointer_type(operands[0].type()); - bvt object_bv = object_literals(bv, type); - - bvt invalid_bv = object_literals( - encode(pointer_logic.get_invalid_object(), type), type); - - const std::size_t object_bits = - bv_pointers_width.get_object_width(type); - - bvt equal_invalid_bv; - equal_invalid_bv.reserve(object_bits); - - for(std::size_t i=0; i &objects) const; diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index fd700efe1e2..9d6d457d6e0 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -270,6 +270,7 @@ void smt2_convt::define_object_size( decision_proceduret::resultt smt2_convt::dec_solve() { + post_process(); write_footer(); out.flush(); return decision_proceduret::resultt::D_ERROR; @@ -1615,14 +1616,14 @@ void smt2_convt::convert_expr(const exprt &expr) } else if(expr.id() == ID_is_invalid_pointer) { + // we don't know the number of objects until conversion + // is finished const auto &op = to_unary_expr(expr).op(); std::size_t pointer_width = boolbv_width(op.type()); - out << "(= ((_ extract " - << pointer_width-1 << " " - << pointer_width-config.bv_encoding.object_bits << ") "; + out << "(bvuge ((_ extract " << pointer_width - 1 << " " + << pointer_width - config.bv_encoding.object_bits << ") "; convert_expr(op); - out << ") (_ bv" << pointer_logic.get_invalid_object() - << " " << config.bv_encoding.object_bits << "))"; + out << ") number-of-objects)"; } else if(expr.id()==ID_string_constant) { @@ -2133,6 +2134,17 @@ void smt2_convt::convert_expr(const exprt &expr) expr.id_string()); } +void smt2_convt::post_process() +{ + // we now know how many objects there are + if(number_of_objects_declared) + { + out << "; fix number of objects\n"; + out << "(assert (= number-of-objects (_ bv" << pointer_logic.objects.size() + << ' ' << config.bv_encoding.object_bits << ")))\n"; + } +} + void smt2_convt::convert_typecast(const typecast_exprt &expr) { const exprt &src = expr.op(); @@ -4723,6 +4735,17 @@ void smt2_convt::find_symbols(const exprt &expr) defined_expressions[expr]=id; } } + else if(expr.id() == ID_is_invalid_pointer) + { + if(!number_of_objects_declared) + { + out << "; the following is for is_invalid_pointer\n"; + out << "(declare-fun number-of-objects () "; + out << "(_ BitVec " << config.bv_encoding.object_bits << ')'; + out << ")\n"; + number_of_objects_declared = true; + } + } else if(expr.id() == ID_object_size) { const exprt &op = to_unary_expr(expr).op(); diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index ef6cffe1be0..41e69554f69 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -93,6 +93,10 @@ class smt2_convt : public stack_decision_proceduret std::vector assumptions; boolbv_widtht boolbv_width; + // post-processing for number-of-objects + bool number_of_objects_declared = false; + void post_process(); + std::size_t number_of_solver_calls = 0; resultt dec_solve() override; diff --git a/src/solvers/smt2/smt2_dec.cpp b/src/solvers/smt2/smt2_dec.cpp index 79a55b4bd0d..879c829041a 100644 --- a/src/solvers/smt2/smt2_dec.cpp +++ b/src/solvers/smt2/smt2_dec.cpp @@ -33,6 +33,8 @@ std::string smt2_dect::decision_procedure_text() const decision_proceduret::resultt smt2_dect::dec_solve() { + post_process(); + ++number_of_solver_calls; temporary_filet temp_file_problem("smt2_dec_problem_", ""),