From 9e8e5c2e0ae05bb99582aaf1ba9685570cda9fd2 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Thu, 23 Jan 2025 16:52:26 -0500 Subject: [PATCH] CONTRATCS: force success for unit pointer predicates Force success for pointer predicates that appear as top level units in requires or ensures clauses. For example `__CPROVER_ensures(__CPROVER_is_fresh(p,size))` is a unit. This ensures that the value set of `p` after assuming the clause contains a unique valid target. It solves a performance issue with z3. All predicates in the `cprover_contracts.c` library now have an extra input `may_fail` controlling the failure behaviour, instrumentation detects units in contracts and sets the `may_fail` parameter accordingly. --- .../test.desc | 7 +--- src/ansi-c/library/cprover_contracts.c | 26 ++++++++----- .../dynamic-frames/dfcc_is_cprover_symbol.cpp | 8 ++++ .../dynamic-frames/dfcc_is_cprover_symbol.h | 3 ++ .../dynamic-frames/dfcc_is_fresh.cpp | 13 +++++-- .../dynamic-frames/dfcc_obeys_contract.cpp | 7 ++++ .../dynamic-frames/dfcc_pointer_equals.cpp | 13 ++++++- .../dynamic-frames/dfcc_pointer_in_range.cpp | 12 +++++- .../dynamic-frames/dfcc_wrapper_program.cpp | 38 +++++++++++++++++++ 9 files changed, 106 insertions(+), 21 deletions(-) diff --git a/regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test.desc b/regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test.desc index 0bc2a52f471..5f7b38654d0 100644 --- a/regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test.desc +++ b/regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test.desc @@ -1,4 +1,4 @@ -FUTURE dfcc-only smt-backend broken-cprover-smt-backend +CORE dfcc-only smt-backend broken-cprover-smt-backend main.c --dfcc main --apply-loop-contracts --enforce-contract foo --malloc-may-fail --malloc-fail-null _ --z3 --slice-formula --no-standard-checks ^EXIT=0$ @@ -8,11 +8,6 @@ main.c ^warning: ignoring -- -Marked as FUTURE because: -- z3 >v4.12 and up can solve the problem with `--dfcc-simple-invalid-pointer-model`, - but the CI uses older versions; -- bitwuzla >v0.6 can solve the problem but we don't run bitwuzla in CI. - Tests support for quantifiers in loop contracts with the SMT backend. When quantified loop invariants are used, they are inserted three times in the transformed program (base case assertion, step case assumption, diff --git a/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c index 5a64466659e..03c9abb1b3f 100644 --- a/src/ansi-c/library/cprover_contracts.c +++ b/src/ansi-c/library/cprover_contracts.c @@ -1166,6 +1166,7 @@ void __CPROVER_contracts_make_invalid_pointer(void **ptr) /// /// \param ptr1 First argument of the `pointer_equals` predicate /// \param ptr2 Second argument of the `pointer_equals` predicate +/// \param may_fail Allow predicate to fail in assume mode /// \param write_set Write set which conveys the invocation context /// (requires/ensures clause, assert/assume context); /// @@ -1179,6 +1180,7 @@ void __CPROVER_contracts_make_invalid_pointer(void **ptr) __CPROVER_bool __CPROVER_contracts_pointer_equals( void **ptr1, void *ptr2, + __CPROVER_bool may_fail, __CPROVER_contracts_write_set_ptr_t write_set) { __CPROVER_HIDE:; @@ -1195,7 +1197,8 @@ __CPROVER_HIDE:; #endif if(write_set->assume_requires_ctx | write_set->assume_ensures_ctx) { - if(__VERIFIER_nondet___CPROVER_bool()) + // SOUNDNESS: allow predicate to fail + if(may_fail && __VERIFIER_nondet___CPROVER_bool()) { __CPROVER_contracts_make_invalid_pointer(ptr1); return 0; @@ -1224,8 +1227,9 @@ __CPROVER_HIDE:; /// The behaviour depends on the boolean flags carried by \p write_set /// which reflect the invocation context: checking vs. replacing a contract, /// in a requires or an ensures clause context. -/// \param elem First argument of the `is_fresh` predicate -/// \param size Second argument of the `is_fresh` predicate +/// \param elem Pointer to the target pointer of the check +/// \param size Size to check for +/// \param may_fail Allow predicate to fail in assume mode /// \param write_set Write set in which seen/allocated objects are recorded; /// /// \details The behaviour is as follows: @@ -1242,6 +1246,7 @@ __CPROVER_HIDE:; __CPROVER_bool __CPROVER_contracts_is_fresh( void **elem, __CPROVER_size_t size, + __CPROVER_bool may_fail, __CPROVER_contracts_write_set_ptr_t write_set) { __CPROVER_HIDE:; @@ -1289,7 +1294,7 @@ __CPROVER_HIDE:; } // SOUNDNESS: allow predicate to fail - if(__VERIFIER_nondet___CPROVER_bool()) + if(may_fail && __VERIFIER_nondet___CPROVER_bool()) { __CPROVER_contracts_make_invalid_pointer(elem); return 0; @@ -1349,7 +1354,7 @@ __CPROVER_HIDE:; } // SOUNDNESS: allow predicate to fail - if(__VERIFIER_nondet___CPROVER_bool()) + if(may_fail && __VERIFIER_nondet___CPROVER_bool()) { __CPROVER_contracts_make_invalid_pointer(elem); return 0; @@ -1436,6 +1441,7 @@ __CPROVER_HIDE:; /// \param lb Lower bound pointer /// \param ptr Target pointer of the predicate /// \param ub Upper bound pointer +/// \param may_fail Allow predicate to fail in assume mode /// \param write_set Write set in which seen/allocated objects are recorded; /// /// \details The behaviour is as follows: @@ -1449,6 +1455,7 @@ __CPROVER_bool __CPROVER_contracts_pointer_in_range_dfcc( void *lb, void **ptr, void *ub, + __CPROVER_bool may_fail, __CPROVER_contracts_write_set_ptr_t write_set) { __CPROVER_HIDE:; @@ -1470,9 +1477,9 @@ __CPROVER_HIDE:; lb_offset <= ub_offset, "lb and ub pointers must be ordered"); if(write_set->assume_requires_ctx | write_set->assume_ensures_ctx) { - if(__VERIFIER_nondet___CPROVER_bool()) + // SOUNDNESS: allow predicate to fail + if(may_fail && __VERIFIER_nondet___CPROVER_bool()) { - // SOUNDNESS: allow predicate to fail __CPROVER_contracts_make_invalid_pointer(ptr); return 0; } @@ -1647,6 +1654,7 @@ __CPROVER_HIDE:; __CPROVER_bool __CPROVER_contracts_obeys_contract( void (**function_pointer)(void), void (*contract)(void), + __CPROVER_bool may_fail, __CPROVER_contracts_write_set_ptr_t set) { __CPROVER_HIDE:; @@ -1657,8 +1665,8 @@ __CPROVER_HIDE:; "__CPROVER_obeys_contract is used only in requires or ensures clauses"); if((set->assume_requires_ctx == 1) | (set->assume_ensures_ctx == 1)) { - // decide if predicate must hold - if(__VERIFIER_nondet___CPROVER_bool()) + // SOUDNESS: allow predicate to fail + if(may_fail && __VERIFIER_nondet___CPROVER_bool()) return 0; // must hold, assign the function pointer to the contract function diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp index 2c945eb8acd..649e3e0cee9 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp @@ -156,3 +156,11 @@ bool dfcc_is_cprover_static_symbol(const irep_idt &id) // going_to variables converted from goto statements has_prefix(id2string(id), CPROVER_PREFIX "going_to"); } + +bool dfcc_is_cprover_pointer_predicate(const irep_idt &id) +{ + return id == CPROVER_PREFIX "pointer_equals" || + id == CPROVER_PREFIX "is_fresh" || + id == CPROVER_PREFIX "pointer_in_range_dfcc" || + id == CPROVER_PREFIX "obeys_contract"; +} diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.h index ce2b3eeb37a..e6848cecf4a 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.h @@ -24,4 +24,7 @@ bool dfcc_is_cprover_function_symbol(const irep_idt &id); /// auto-generated object following a pointer dereference. bool dfcc_is_cprover_static_symbol(const irep_idt &id); +/// Returns `true` iff the symbol is one of the CPROVER pointer predicates +bool dfcc_is_cprover_pointer_predicate(const irep_idt &id); + #endif diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_fresh.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_fresh.cpp index 10a8ee97f95..f29cbe85b3c 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_fresh.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_fresh.cpp @@ -11,6 +11,8 @@ Date: August 2022 #include #include +#include +#include #include #include "dfcc_cfg_info.h" @@ -33,7 +35,7 @@ void dfcc_is_fresht::rewrite_calls( program.instructions.end(), cfg_info); } - +#include void dfcc_is_fresht::rewrite_calls( goto_programt &program, goto_programt::targett first_instruction, @@ -50,8 +52,7 @@ void dfcc_is_fresht::rewrite_calls( if(function.id() == ID_symbol) { const irep_idt &fun_name = to_symbol_expr(function).get_identifier(); - - if(fun_name == CPROVER_PREFIX "is_fresh") + if(has_prefix(id2string(fun_name), CPROVER_PREFIX "is_fresh")) { // add address on first operand target->call_arguments()[0] = @@ -61,6 +62,12 @@ void dfcc_is_fresht::rewrite_calls( to_symbol_expr(target->call_function()) .set_identifier(library.dfcc_fun_symbol[dfcc_funt::IS_FRESH].name); + // pass the may_fail flag + if(function.source_location().get_bool("no_fail")) + target->call_arguments().push_back(false_exprt()); + else + target->call_arguments().push_back(true_exprt()); + // pass the write_set target->call_arguments().push_back(cfg_info.get_write_set(target)); } diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.cpp index da69a217332..44503a0a5fa 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.cpp @@ -12,6 +12,7 @@ Date: August 2022 #include #include #include +#include #include #include @@ -87,6 +88,12 @@ void dfcc_obeys_contractt::rewrite_calls( .set_identifier( library.dfcc_fun_symbol[dfcc_funt::OBEYS_CONTRACT].name); + // pass the may_fail flag + if(function.source_location().get_bool("no_fail")) + target->call_arguments().push_back(false_exprt()); + else + target->call_arguments().push_back(true_exprt()); + // pass the write_set target->call_arguments().push_back(cfg_info.get_write_set(target)); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.cpp index a5fbfea3fa7..5e81637b8cc 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.cpp @@ -13,9 +13,11 @@ Date: Jan 2025 #include #include #include +#include #include #include #include +#include #include #include "dfcc_cfg_info.h" @@ -56,7 +58,7 @@ void dfcc_pointer_equalst::rewrite_calls( { const irep_idt &fun_name = to_symbol_expr(function).get_identifier(); - if(fun_name == CPROVER_PREFIX "pointer_equals") + if(has_prefix(id2string(fun_name), CPROVER_PREFIX "pointer_equals")) { // add address on first operand target->call_arguments()[0] = @@ -67,6 +69,12 @@ void dfcc_pointer_equalst::rewrite_calls( .set_identifier( library.dfcc_fun_symbol[dfcc_funt::POINTER_EQUALS].name); + // pass the may_fail flag + if(function.source_location().get_bool("no_fail")) + target->call_arguments().push_back(false_exprt()); + else + target->call_arguments().push_back(true_exprt()); + // pass the write_set target->call_arguments().push_back(cfg_info.get_write_set(target)); } @@ -106,7 +114,8 @@ class pointer_equality_visitort : public expr_visitort code_typet::parametert(pointer_type(void_type()))}, bool_typet()); - symbol_exprt pointer_equals("ID_pointer_equals", pointer_equals_type); + symbol_exprt pointer_equals( + CPROVER_PREFIX "pointer_equals", pointer_equals_type); for(exprt *expr_ptr : equality_exprs_to_transform) { diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.cpp index 76cb565fd67..d0637d393de 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.cpp @@ -11,8 +11,10 @@ Date: August 2022 #include #include +#include #include #include +#include #include #include "dfcc_cfg_info.h" @@ -53,7 +55,8 @@ void dfcc_pointer_in_ranget::rewrite_calls( { const irep_idt &fun_name = to_symbol_expr(function).get_identifier(); - if(fun_name == CPROVER_PREFIX "pointer_in_range_dfcc") + if(has_prefix( + id2string(fun_name), CPROVER_PREFIX "pointer_in_range_dfcc")) { // add address on second operand target->call_arguments()[1] = @@ -64,6 +67,13 @@ void dfcc_pointer_in_ranget::rewrite_calls( .set_identifier( library.dfcc_fun_symbol[dfcc_funt::POINTER_IN_RANGE_DFCC].name); + // pass the may_fail flag + // pass the may_fail flag + if(function.source_location().get_bool("no_fail")) + target->call_arguments().push_back(false_exprt()); + else + target->call_arguments().push_back(true_exprt()); + // pass the write_set target->call_arguments().push_back(cfg_info.get_write_set(target)); } diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp index a625383f182..182b4b036c6 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp @@ -25,6 +25,7 @@ Author: Remi Delmas, delmasrd@amazon.com #include "dfcc_contract_functions.h" #include "dfcc_instrument.h" +#include "dfcc_is_cprover_symbol.h" #include "dfcc_library.h" #include "dfcc_lift_memory_predicates.h" #include "dfcc_pointer_equals.h" @@ -535,6 +536,37 @@ void dfcc_wrapper_programt::encode_is_fresh_set() postamble.add(goto_programt::make_dead(is_fresh_set, wrapper_sl)); } +#include + +/// If the expression is a function call to one of the pointer predicates, +/// adds a "_no_fail" prefix to the function name. This is later picked up +/// by fix_calls to synthesize the value of the `may_fail` parameter for +/// pointer predicates. +bool disable_may_fail(exprt &expr) +{ + if(expr.id() != ID_side_effect) + return false; + + side_effect_exprt &side_effect = to_side_effect_expr(expr); + if(side_effect.get_statement() != ID_function_call) + return false; + + exprt &function = side_effect.operands()[0]; + if(function.id() != ID_symbol) + return false; + + const irep_idt &func_name = to_symbol_expr(function).get_identifier(); + + if(dfcc_is_cprover_pointer_predicate(func_name)) + { + // tag call as no_fail + function.add_source_location().set("no_fail", true); + return true; + } + + return false; +} + void dfcc_wrapper_programt::encode_requires_clauses() { // we use this empty requires write set to check for the absence of side @@ -556,6 +588,9 @@ void dfcc_wrapper_programt::encode_requires_clauses() { exprt requires_lmbd = to_lambda_expr(r).application(contract_lambda_parameters); + + // add "no_fail" suffix to predicates required as units + disable_may_fail(requires_lmbd); source_locationt sl(r.source_location()); if(statement_type == ID_assert) { @@ -605,6 +640,9 @@ void dfcc_wrapper_programt::encode_ensures_clauses() .application(contract_lambda_parameters) .with_source_location(e); + // add "no_fail" suffix to unit pointer predicates + disable_may_fail(ensures); + // this also rewrites ID_old expressions to fresh variables generate_history_variables_initialization( goto_model.symbol_table, ensures, language_mode, history);