From 8788466d90b6ec24e733cda2525b8f87683160ff Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Wed, 28 Jun 2023 16:35:44 -0400 Subject: [PATCH] CONTRACTS: fix fresh symbols for quantified vars --- .../main.c | 32 +++++++++++++++++++ .../test.desc | 15 +++++++++ .../dynamic-frames/dfcc_instrument_loop.cpp | 22 +++++++------ .../dynamic-frames/dfcc_instrument_loop.h | 6 ++-- 4 files changed, 63 insertions(+), 12 deletions(-) create mode 100644 regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/main.c create mode 100644 regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test.desc diff --git a/regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/main.c b/regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/main.c new file mode 100644 index 00000000000..5f7b9a26fb4 --- /dev/null +++ b/regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/main.c @@ -0,0 +1,32 @@ +#include +void foo(char *dst, const char *src, size_t n) + // clang-format off + __CPROVER_requires(__CPROVER_is_fresh(src, n)) + __CPROVER_requires(__CPROVER_is_fresh(dst, n)) + __CPROVER_assigns(__CPROVER_object_from(dst)) + __CPROVER_ensures(__CPROVER_forall { + size_t j; + j < n ==> dst[j] == src[j] + }) +// clang-format on +{ + for(size_t i = 0; i < n; i++) + // clang-format off + __CPROVER_assigns(i, __CPROVER_object_from(dst)) + __CPROVER_loop_invariant(i <= n) + __CPROVER_loop_invariant( + __CPROVER_forall { size_t j; j < i ==> dst[j] == src[j] }) + // clang-format on + { + dst[i] = src[i]; + } +} + +int main() +{ + char *dst; + char *src; + size_t n; + foo(dst, src, n); + return 0; +} 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 new file mode 100644 index 00000000000..c7692c036dc --- /dev/null +++ b/regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test.desc @@ -0,0 +1,15 @@ +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 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +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, +step case assertion), and each occurrence needs to be rewritten with fresh +symbols for the quantified variables. The SMT solver would with an error +whenever this renaming is not properly done. diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp index b8bf3d7c4f4..f2d864b7c69 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp @@ -129,15 +129,10 @@ void dfcc_instrument_loopt::operator()( write_set_populate_instrs, nof_targets); - // Replace bound variables by fresh instances in quantified formulas. - exprt invariant = loop.invariant; - if(has_subexpr(invariant, ID_exists) || has_subexpr(invariant, ID_forall)) - add_quantified_variable(symbol_table, invariant, language_mode); - // ---------- Add instrumented instructions ---------- goto_programt::targett loop_latch = loop.find_latch(goto_function.body).value(); - + exprt invariant(loop.invariant); const auto history_var_map = add_prehead_instructions( loop_id, goto_function, @@ -240,7 +235,9 @@ dfcc_instrument_loopt::add_prehead_instructions( // GOTO HEAD; // ``` - + // Replace bound variables by fresh instances in quantified formulas. + if(has_subexpr(invariant, ID_exists) || has_subexpr(invariant, ID_forall)) + add_quantified_variable(symbol_table, invariant, language_mode); // initialize loop_entry history vars; auto replace_history_result = replace_history_loop_entry( symbol_table, invariant, loop_head_location, language_mode); @@ -329,7 +326,7 @@ dfcc_instrument_loopt::add_step_instructions( goto_programt::targett loop_head, goto_programt::targett loop_latch, goto_programt &havoc_instrs, - const exprt &invariant, + exprt &invariant, const exprt::operandst &decreases_clauses, const symbol_exprt &addr_of_loop_write_set, const exprt &outer_write_set, @@ -432,6 +429,9 @@ dfcc_instrument_loopt::add_step_instructions( dfcc_utilst::get_function_symbol(symbol_table, function_id).mode; { // Assume the loop invariant after havocing the state. + // Replace bound variables by fresh instances in quantified formulas. + if(has_subexpr(invariant, ID_exists) || has_subexpr(invariant, ID_forall)) + add_quantified_variable(symbol_table, invariant, language_mode); code_assumet assumption{invariant}; assumption.add_source_location() = loop_head_location; converter.goto_convert(assumption, step_instrs, language_mode); @@ -461,7 +461,7 @@ void dfcc_instrument_loopt::add_body_instructions( symbol_table_baset &symbol_table, goto_programt::targett loop_head, goto_programt::targett loop_latch, - const exprt &invariant, + exprt &invariant, const exprt::operandst &decreases_clauses, const symbol_exprt &entered_loop, const symbol_exprt &in_base_case, @@ -512,6 +512,10 @@ void dfcc_instrument_loopt::add_body_instructions( "Check invariant after step for loop " + id2string(check_location.get_function()) + "." + std::to_string(cbmc_loop_id)); + // Assume the loop invariant after havocing the state. + // Replace bound variables by fresh instances in quantified formulas. + if(has_subexpr(invariant, ID_exists) || has_subexpr(invariant, ID_forall)) + add_quantified_variable(symbol_table, invariant, language_mode); code_assertt assertion{invariant}; assertion.add_source_location() = check_location; converter.goto_convert(assertion, pre_loop_latch_instrs, language_mode); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.h index 523aeb1fdca..8e624e016ae 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.h @@ -184,7 +184,7 @@ class dfcc_instrument_loopt /// \param[inout] loop_latch Latch node of the loop. /// \param[out] assigns_instrs `goto_programt` that contains instructions of /// populating assigns into the loop write set. - /// \param[out] invariant Loop invariants. + /// \param[in] invariant Loop invariants. /// \param[in] assigns Assigns targets of the loop. /// \param[in] loop_write_set Stack allocated loop write set variable. /// \param[in] addr_of_loop_write_set Loop write set pointer variable. @@ -250,7 +250,7 @@ class dfcc_instrument_loopt goto_programt::targett loop_head, goto_programt::targett loop_latch, goto_programt &havoc_instrs, - const exprt &invariant, + exprt &invariant, const exprt::operandst &decreases_clauses, const symbol_exprt &loop_write_set, const exprt &outer_write_set, @@ -296,7 +296,7 @@ class dfcc_instrument_loopt symbol_table_baset &symbol_table, goto_programt::targett loop_head, goto_programt::targett loop_latch, - const exprt &invariant, + exprt &invariant, const exprt::operandst &decreases_clauses, const symbol_exprt &entered_loop, const symbol_exprt &in_base_case,