From 2d416e1b437f7ce7d7039927b6852ac4043cca95 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Mon, 22 Jul 2024 02:37:40 -0500 Subject: [PATCH] Check side effect of loop contracts during instrumentation --- doc/man/goto-instrument.1 | 8 ++- .../main.c | 16 +++++ .../test.desc | 10 +++ .../variant_function_call_fail/test.desc | 4 +- .../variant_side_effects_fail/test.desc | 4 +- .../main.c | 16 +++++ .../test.desc | 10 +++ src/ansi-c/goto-conversion/goto_convert.cpp | 13 ---- src/cprover/instrument_given_invariants.cpp | 11 +++ src/goto-instrument/contracts/contracts.cpp | 11 ++- src/goto-instrument/contracts/contracts.h | 5 ++ .../dynamic-frames/dfcc_cfg_info.cpp | 68 ++++++++----------- src/goto-instrument/contracts/utils.cpp | 60 ++++++++++++++++ src/goto-instrument/contracts/utils.h | 17 +++++ .../goto_instrument_parse_options.cpp | 4 +- .../goto_instrument_parse_options.h | 1 + 16 files changed, 193 insertions(+), 65 deletions(-) create mode 100644 regression/contracts-dfcc/loop_contracts_statement_expression/main.c create mode 100644 regression/contracts-dfcc/loop_contracts_statement_expression/test.desc create mode 100644 regression/contracts/loop_contracts_statement_expression/main.c create mode 100644 regression/contracts/loop_contracts_statement_expression/test.desc diff --git a/doc/man/goto-instrument.1 b/doc/man/goto-instrument.1 index 92342ceb482..960a2ec0354 100644 --- a/doc/man/goto-instrument.1 +++ b/doc/man/goto-instrument.1 @@ -1015,7 +1015,13 @@ force aggressive slicer to preserve all direct paths .SS "Code contracts:" .TP \fB\-\-apply\-loop\-contracts\fR -check and use loop contracts when provided +.TP +\fB\-disable\-loop\-contracts\-side\-effect\-check\fR +UNSOUND OPTION. Disable checking the absence of side effects in loop +contract clauses. In absence of such checking, loop contracts clauses will +accept more expressions, such as pure functions and statement expressions. +But user have to make sure the loop contracts are side-effect free by them self +to get a sound result. .TP \fB\-loop\-contracts\-no\-unwind\fR do not unwind transformed loops diff --git a/regression/contracts-dfcc/loop_contracts_statement_expression/main.c b/regression/contracts-dfcc/loop_contracts_statement_expression/main.c new file mode 100644 index 00000000000..e314d366cb4 --- /dev/null +++ b/regression/contracts-dfcc/loop_contracts_statement_expression/main.c @@ -0,0 +1,16 @@ +int main() +{ + unsigned i; + + while(i > 1) + __CPROVER_loop_invariant(({ + unsigned b = i >= 1; + goto label; + b = i < 1; + label: + b; + })) + { + i--; + } +} diff --git a/regression/contracts-dfcc/loop_contracts_statement_expression/test.desc b/regression/contracts-dfcc/loop_contracts_statement_expression/test.desc new file mode 100644 index 00000000000..f502fbb0673 --- /dev/null +++ b/regression/contracts-dfcc/loop_contracts_statement_expression/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--dfcc main --apply-loop-contracts --disable-loop-contracts-side-effect-check +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test demonstrates a case where the loop invariant +is a side-effect free statement expression. diff --git a/regression/contracts-dfcc/variant_function_call_fail/test.desc b/regression/contracts-dfcc/variant_function_call_fail/test.desc index d1bff78a41a..884263a801f 100644 --- a/regression/contracts-dfcc/variant_function_call_fail/test.desc +++ b/regression/contracts-dfcc/variant_function_call_fail/test.desc @@ -1,8 +1,8 @@ CORE main.c --dfcc main --apply-loop-contracts -^Decreases clause is not side-effect free. \(at: file main.c line .* function main\)$ -^EXIT=70$ +^Decreases clause is not side-effect free.$ +^EXIT=6$ ^SIGNAL=0$ -- -- diff --git a/regression/contracts-dfcc/variant_side_effects_fail/test.desc b/regression/contracts-dfcc/variant_side_effects_fail/test.desc index 7ce5cab0ce1..546e0c5e7c8 100644 --- a/regression/contracts-dfcc/variant_side_effects_fail/test.desc +++ b/regression/contracts-dfcc/variant_side_effects_fail/test.desc @@ -1,8 +1,8 @@ CORE main.c --dfcc main --apply-loop-contracts -^Decreases clause is not side-effect free. \(at: file main.c line .* function main\)$ -^EXIT=70$ +^Decreases clause is not side-effect free.$ +^EXIT=6$ ^SIGNAL=0$ -- -- diff --git a/regression/contracts/loop_contracts_statement_expression/main.c b/regression/contracts/loop_contracts_statement_expression/main.c new file mode 100644 index 00000000000..e314d366cb4 --- /dev/null +++ b/regression/contracts/loop_contracts_statement_expression/main.c @@ -0,0 +1,16 @@ +int main() +{ + unsigned i; + + while(i > 1) + __CPROVER_loop_invariant(({ + unsigned b = i >= 1; + goto label; + b = i < 1; + label: + b; + })) + { + i--; + } +} diff --git a/regression/contracts/loop_contracts_statement_expression/test.desc b/regression/contracts/loop_contracts_statement_expression/test.desc new file mode 100644 index 00000000000..7bf3ba98beb --- /dev/null +++ b/regression/contracts/loop_contracts_statement_expression/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--apply-loop-contracts --disable-loop-contracts-side-effect-check +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test demonstrates a case where the loop invariant +is a side-effect free statement expression. diff --git a/src/ansi-c/goto-conversion/goto_convert.cpp b/src/ansi-c/goto-conversion/goto_convert.cpp index 4c2f8960ed8..809783d2fba 100644 --- a/src/ansi-c/goto-conversion/goto_convert.cpp +++ b/src/ansi-c/goto-conversion/goto_convert.cpp @@ -1036,12 +1036,6 @@ void goto_convertt::convert_loop_contracts( static_cast(code.find(ID_C_spec_loop_invariant)); if(!invariant.is_nil()) { - if(has_subexpr(invariant, ID_side_effect)) - { - throw incorrect_goto_program_exceptiont( - "Loop invariant is not side-effect free.", code.find_source_location()); - } - PRECONDITION(loop->is_goto() || loop->is_incomplete_goto()); loop->condition_nonconst().add(ID_C_spec_loop_invariant).swap(invariant); } @@ -1050,13 +1044,6 @@ void goto_convertt::convert_loop_contracts( static_cast(code.find(ID_C_spec_decreases)); if(!decreases_clause.is_nil()) { - if(has_subexpr(decreases_clause, ID_side_effect)) - { - throw incorrect_goto_program_exceptiont( - "Decreases clause is not side-effect free.", - code.find_source_location()); - } - PRECONDITION(loop->is_goto() || loop->is_incomplete_goto()); loop->condition_nonconst().add(ID_C_spec_decreases).swap(decreases_clause); } diff --git a/src/cprover/instrument_given_invariants.cpp b/src/cprover/instrument_given_invariants.cpp index 9cd5bdc4186..1093daea568 100644 --- a/src/cprover/instrument_given_invariants.cpp +++ b/src/cprover/instrument_given_invariants.cpp @@ -11,6 +11,8 @@ Author: Daniel Kroening, dkr@amazon.com #include "instrument_given_invariants.h" +#include + #include void instrument_given_invariants(goto_functionst::function_mapt::value_type &f) @@ -25,6 +27,15 @@ void instrument_given_invariants(goto_functionst::function_mapt::value_type &f) { const auto &invariants = static_cast( it->condition().find(ID_C_spec_loop_invariant)); + if(!invariants.is_nil()) + { + if(has_subexpr(invariants, ID_side_effect)) + { + throw incorrect_goto_program_exceptiont( + "Loop invariant is not side-effect free.", + it->condition().find_source_location()); + } + } for(const auto &invariant : invariants.operands()) { diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 36eff629528..ed84145237d 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -983,12 +983,11 @@ void code_contractst::apply_loop_contract( goto_function.body, loop_head, goto_programt::make_skip()); loop_end->set_target(loop_head); - exprt assigns_clause = - static_cast(loop_end->condition().find(ID_C_spec_assigns)); - exprt invariant = static_cast( - loop_end->condition().find(ID_C_spec_loop_invariant)); - exprt decreases_clause = static_cast( - loop_end->condition().find(ID_C_spec_decreases)); + exprt assigns_clause = get_loop_assigns(loop_end); + exprt invariant = + get_loop_invariants(loop_end, loop_contract_config.check_side_effect); + exprt decreases_clause = + get_loop_decreases(loop_end, loop_contract_config.check_side_effect); if(invariant.is_nil()) { diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index 8e6fe670dd3..56cedd05baa 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -33,6 +33,11 @@ Date: February 2016 #define HELP_LOOP_CONTRACTS \ " {y--apply-loop-contracts} \t check and use loop contracts when provided\n" +#define FLAG_DISABLE_SIDE_EFFECT_CHECK \ + "disable-loop-contracts-side-effect-check" +#define HELP_DISABLE_SIDE_EFFECT_CHECK \ + " {y--disable-loop-contracts-side-effect-check} \t UNSOUND OPTION.\t " \ + " disable the check of side-effect of loop contracts\n" #define FLAG_LOOP_CONTRACTS_NO_UNWIND "loop-contracts-no-unwind" #define HELP_LOOP_CONTRACTS_NO_UNWIND \ " {y--loop-contracts-no-unwind} \t do not unwind transformed loops\n" diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp index 2aa5953ef38..97b632cbb70 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp @@ -29,40 +29,15 @@ Date: March 2023 #include "dfcc_root_object.h" #include "dfcc_utils.h" -/// Extracts the assigns clause expression from the latch condition -static const exprt::operandst & -get_assigns(const goto_programt::const_targett &latch_target) -{ - return static_cast( - latch_target->condition().find(ID_C_spec_assigns)) - .operands(); -} - -/// Extracts the invariant clause expression from the latch condition -static const exprt::operandst & -get_invariants(const goto_programt::const_targett &latch_target) -{ - return static_cast( - latch_target->condition().find(ID_C_spec_loop_invariant)) - .operands(); -} - -/// Extracts the decreases clause expression from the latch condition -static const exprt::operandst & -get_decreases(const goto_programt::const_targett &latch_target) -{ - return static_cast( - latch_target->condition().find(ID_C_spec_decreases)) - .operands(); -} - /// Returns true iff some contract clause expression is attached /// to the latch condition of this loop -static bool has_contract(const goto_programt::const_targett &latch_target) +static bool has_contract( + const goto_programt::const_targett &latch_target, + const bool check_side_effect) { - return !get_assigns(latch_target).empty() || - !get_invariants(latch_target).empty() || - !get_decreases(latch_target).empty(); + return get_loop_assigns(latch_target).is_not_nil() || + get_loop_invariants(latch_target, check_side_effect).is_not_nil() || + get_loop_decreases(latch_target, check_side_effect).is_not_nil(); } void dfcc_loop_infot::output(std::ostream &out) const @@ -155,16 +130,20 @@ dfcc_loop_infot::find_latch(goto_programt &goto_program) const static std::optional check_has_contract_rec( const dfcc_loop_nesting_grapht &loop_nesting_graph, const std::size_t loop_idx, - const bool must_have_contract) + const bool must_have_contract, + const bool check_side_effect) { const auto &node = loop_nesting_graph[loop_idx]; - if(must_have_contract && !has_contract(node.latch)) + if(must_have_contract && !has_contract(node.latch, check_side_effect)) return node.head; for(const auto pred_idx : loop_nesting_graph.get_predecessors(loop_idx)) { auto result = check_has_contract_rec( - loop_nesting_graph, pred_idx, has_contract(node.latch)); + loop_nesting_graph, + pred_idx, + has_contract(node.latch, check_side_effect), + check_side_effect); if(result.has_value()) return result; } @@ -175,13 +154,15 @@ static std::optional check_has_contract_rec( /// loops nested in loops that have contracts also have contracts. /// Return the head of the first offending loop if it exists, nothing otherwise. static std::optional check_inner_loops_have_contracts( - const dfcc_loop_nesting_grapht &loop_nesting_graph) + const dfcc_loop_nesting_grapht &loop_nesting_graph, + const bool check_side_effect) { for(std::size_t idx = 0; idx < loop_nesting_graph.size(); idx++) { if(loop_nesting_graph.get_successors(idx).empty()) { - auto result = check_has_contract_rec(loop_nesting_graph, idx, false); + auto result = check_has_contract_rec( + loop_nesting_graph, idx, false, check_side_effect); if(result.has_value()) return result; } @@ -349,6 +330,7 @@ static struct contract_clausest default_loop_contract_clauses( const std::size_t loop_id, const irep_idt &function_id, local_may_aliast &local_may_alias, + const bool check_side_effect, message_handlert &message_handler, const namespacet &ns) { @@ -356,11 +338,13 @@ static struct contract_clausest default_loop_contract_clauses( const auto &loop = loop_nesting_graph[loop_id]; // Process loop contract clauses - exprt::operandst invariant_clauses = get_invariants(loop.latch); - exprt::operandst assigns_clauses = get_assigns(loop.latch); + exprt::operandst invariant_clauses = + get_loop_invariants(loop.latch, check_side_effect).operands(); + exprt::operandst assigns_clauses = get_loop_assigns(loop.latch).operands(); // Initialise defaults - struct contract_clausest result(get_decreases(loop.latch)); + struct contract_clausest result( + get_loop_decreases(loop.latch, check_side_effect).operands()); // Generate defaults for all clauses if at least one type of clause is defined if( @@ -435,6 +419,7 @@ static dfcc_loop_infot gen_dfcc_loop_info( const std::map &loop_info_map, dirtyt &dirty, local_may_aliast &local_may_alias, + const bool check_side_effect, message_handlert &message_handler, dfcc_libraryt &library, symbol_table_baset &symbol_table) @@ -454,6 +439,7 @@ static dfcc_loop_infot gen_dfcc_loop_info( loop_id, function_id, local_may_alias, + check_side_effect, message_handler, ns); @@ -523,7 +509,8 @@ dfcc_cfg_infot::dfcc_cfg_infot( dfcc_check_loop_normal_form(goto_program, log); loop_nesting_graph = build_loop_nesting_graph(goto_program); - const auto head = check_inner_loops_have_contracts(loop_nesting_graph); + const auto head = check_inner_loops_have_contracts( + loop_nesting_graph, loop_contract_config.check_side_effect); if(head.has_value()) { throw invalid_source_file_exceptiont( @@ -571,6 +558,7 @@ dfcc_cfg_infot::dfcc_cfg_infot( loop_info_map, dirty, local_may_alias, + loop_contract_config.check_side_effect, message_handler, library, symbol_table)}); diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index 8b86a1c6ea9..803cf47eb6a 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -682,6 +682,66 @@ get_loop_head(const unsigned int target_loop_number, goto_functiont &function) return get_loop_head_or_end(target_loop_number, function, true); } +/// Extract loop invariants from loop end without any checks. +static exprt +extract_loop_invariants(const goto_programt::const_targett &loop_end) +{ + return static_cast( + loop_end->condition().find(ID_C_spec_loop_invariant)); +} + +static exprt extract_loop_assigns(const goto_programt::const_targett &loop_end) +{ + return static_cast( + loop_end->condition().find(ID_C_spec_assigns)); +} + +static exprt +extract_loop_decreases(const goto_programt::const_targett &loop_end) +{ + return static_cast( + loop_end->condition().find(ID_C_spec_decreases)); +} + +exprt get_loop_invariants( + const goto_programt::const_targett &loop_end, + const bool check_side_effect) +{ + auto invariant = extract_loop_invariants(loop_end); + if(!invariant.is_nil() && check_side_effect) + { + if(has_subexpr(invariant, ID_side_effect)) + { + throw incorrect_goto_program_exceptiont( + "Loop invariant is not side-effect free.", + loop_end->condition().find_source_location()); + } + } + return invariant; +} + +exprt get_loop_assigns(const goto_programt::const_targett &loop_end) +{ + return extract_loop_assigns(loop_end); +} + +exprt get_loop_decreases( + const goto_programt::const_targett &loop_end, + const bool check_side_effect) +{ + auto decreases_clause = extract_loop_decreases(loop_end); + if(!decreases_clause.is_nil() && check_side_effect) + { + if(has_subexpr(decreases_clause, ID_side_effect)) + { + throw incorrect_goto_program_exceptiont( + "Decreases clause is not side-effect free.", + loop_end->condition().find_source_location()); + } + } + return decreases_clause; +} + void annotate_invariants( const invariant_mapt &invariant_map, goto_modelt &goto_model) diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h index 0dd802bab18..607dc2fccfa 100644 --- a/src/goto-instrument/contracts/utils.h +++ b/src/goto-instrument/contracts/utils.h @@ -313,6 +313,23 @@ get_loop_end(const unsigned int loop_number, goto_functiont &function); goto_programt::targett get_loop_head(const unsigned int loop_number, goto_functiont &function); +/// Extract loop invariants from annotated loop end. +/// Will check if the loop invariant is side-effect free if +/// \p check_side_effect` is set. +exprt get_loop_invariants( + const goto_programt::const_targett &loop_end, + const bool check_side_effect = true); + +/// Extract loop assigns from annotated loop end. +exprt get_loop_assigns(const goto_programt::const_targett &loop_end); + +/// Extract loop decreases from annotated loop end. +/// Will check if the loop decreases is side-effect free if +/// \p check_side_effect` is set. +exprt get_loop_decreases( + const goto_programt::const_targett &loop_end, + const bool check_side_effect = true); + /// Annotate the invariants in `invariant_map` to their corresponding /// loops. Corresponding loops are specified by keys of `invariant_map` void annotate_invariants( diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index dc613b102f4..6f65e04c567 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1169,7 +1169,8 @@ void goto_instrument_parse_optionst::instrument_goto_program() // Initialize loop contract config from cmdline. loop_contract_configt loop_contract_config = { cmdline.isset(FLAG_LOOP_CONTRACTS), - !cmdline.isset(FLAG_LOOP_CONTRACTS_NO_UNWIND)}; + !cmdline.isset(FLAG_LOOP_CONTRACTS_NO_UNWIND), + !cmdline.isset(FLAG_DISABLE_SIDE_EFFECT_CHECK)}; if( cmdline.isset(FLAG_LOOP_CONTRACTS) && @@ -2029,6 +2030,7 @@ void goto_instrument_parse_optionst::help() "Code contracts:\n" HELP_DFCC HELP_LOOP_CONTRACTS + HELP_DISABLE_SIDE_EFFECT_CHECK HELP_LOOP_CONTRACTS_NO_UNWIND HELP_LOOP_CONTRACTS_FILE HELP_REPLACE_CALL diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 7ceeb29ede6..5258481c270 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -102,6 +102,7 @@ Author: Daniel Kroening, kroening@kroening.com "(horn)(skip-loops):(model-argc-argv):" \ OPT_DFCC \ "(" FLAG_LOOP_CONTRACTS ")" \ + "(" FLAG_DISABLE_SIDE_EFFECT_CHECK ")" \ "(" FLAG_LOOP_CONTRACTS_NO_UNWIND ")" \ "(" FLAG_LOOP_CONTRACTS_FILE "):" \ "(" FLAG_REPLACE_CALL "):" \