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..0432df1b9e9 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" @@ -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..17b2f07d195 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,103 @@ void dfcc_wrapper_programt::encode_is_fresh_set() postamble.add(goto_programt::make_dead(is_fresh_set, wrapper_sl)); } +/// Recursively traverses expression, adding "no_fail" attributes to pointer +/// predicates that we know cannot fail when invoked in an assume context: +/// Starting from the root with "no_fail" true, we recurse over the boolean +/// structure, setting the "no_fail" false for all but the last operand +/// disjunctive operators like `||` and `==>`, and distributing the current +/// "no_fail" status over disjunctions. +/// +/// For instance: +/// ``` +/// (len > 0):no_fail=false ==> is_fresh(p, len):no_fail=true +/// ``` +/// +/// ``` +/// is_fresh(p, len):no_fail=true && is_fresh(q, len):no_fail=true +/// ``` +/// +/// ``` +/// is_fresh(p, len):no_fail=false || +/// is_fresh(q, len):no_fail=false || +/// is_fresh(r, len):no_fail=true +/// ``` +/// +/// ``` +/// is_fresh(p, len):no_fail=false || +/// ( +/// is_fresh(q, len):no_fail=true && +/// ( +/// (len>0):no_fail=true ==> is_fresh(r, len):no_fail=true +/// ) +/// ) +/// ``` +/// \param expr The expression to traverse +/// \param no_fail The current no_fail value based on logical context +void disable_may_fail_rec(exprt &expr, bool no_fail) +{ + if(expr.id() == ID_side_effect) + { + // Base case: pointer predicate function call + side_effect_exprt &side_effect = to_side_effect_expr(expr); + if(side_effect.get_statement() == ID_function_call) + { + exprt &function = side_effect.operands()[0]; + if(function.id() == ID_symbol) + { + const irep_idt &func_name = to_symbol_expr(function).get_identifier(); + if(dfcc_is_cprover_pointer_predicate(func_name)) + { + function.add_source_location().set("no_fail", no_fail); + } + } + } + return; + } + else if(expr.id() == ID_and) + { + // Shortcutting AND: propagate current no_fail value to all operands + for(auto &op : expr.operands()) + { + disable_may_fail_rec(op, no_fail); + } + } + else if(expr.id() == ID_or) + { + // Shortcutting OR: set no_fail=false for all but last operand + auto &ops = expr.operands(); + // Process all operands except the last one with no_fail=false + for(std::size_t i = 0; i < ops.size() - 1; ++i) + { + disable_may_fail_rec(ops[i], false); + } + // Process last operand with current no_fail value + if(!ops.empty()) + { + disable_may_fail_rec(ops.back(), no_fail); + } + } + else if(expr.id() == ID_implies) + { + // Shortcutting implies: false for antecedent, current value for consequent + INVARIANT( + expr.operands().size() == 2, + "Implication expression must have two operands"); + disable_may_fail_rec(expr.operands()[0], false); + disable_may_fail_rec(expr.operands()[1], no_fail); + } + else + { + // bail on other types of expressions + return; + } +} + +void disable_may_fail(exprt &expr) +{ + disable_may_fail_rec(expr, true); +} + void dfcc_wrapper_programt::encode_requires_clauses() { // we use this empty requires write set to check for the absence of side @@ -556,6 +654,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 +706,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);