From fb583b45cb9335c0a577db15a656a58455cb3226 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 23 Jan 2024 11:47:52 +0000 Subject: [PATCH 1/3] Restrict function pointers: update goto program Maintain goto-program invariants when modifying a program via function-pointer restrictions. --- src/goto-programs/restrict_function_pointers.cpp | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/src/goto-programs/restrict_function_pointers.cpp b/src/goto-programs/restrict_function_pointers.cpp index e7ddab4fa06..070f7282c1d 100644 --- a/src/goto-programs/restrict_function_pointers.cpp +++ b/src/goto-programs/restrict_function_pointers.cpp @@ -35,7 +35,7 @@ void for_each_function_call(GotoFunctionT &&goto_function, Handler handler) handler); } -static void restrict_function_pointer( +[[nodiscard]] static bool restrict_function_pointer( message_handlert &message_handler, symbol_tablet &symbol_table, goto_programt &goto_program, @@ -54,7 +54,7 @@ static void restrict_function_pointer( const auto &original_function = location->call_function(); if(!can_cast_expr(original_function)) - return; + return false; // because we run the label function pointer calls transformation pass before // this stage a dereference can only dereference a symbol expression @@ -66,7 +66,7 @@ static void restrict_function_pointer( restrictions.restrictions.find(pointer_symbol.get_identifier()); if(restriction_iterator == restrictions.restrictions.end()) - return; + return false; const namespacet ns(symbol_table); std::unordered_set candidates; @@ -80,6 +80,8 @@ static void restrict_function_pointer( function_id, location, candidates); + + return true; } } // namespace @@ -180,8 +182,9 @@ void restrict_function_pointers( { goto_functiont &goto_function = function_item.second; + bool did_something = false; for_each_function_call(goto_function, [&](const goto_programt::targett it) { - restrict_function_pointer( + did_something |= restrict_function_pointer( message_handler, goto_model.symbol_table, goto_function.body, @@ -189,6 +192,9 @@ void restrict_function_pointers( restrictions, it); }); + + if(did_something) + goto_function.body.update(); } } From 5d9fe8280ec8e5c5b94c0c5a583a0c9d4ee32b4d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 5 Dec 2023 13:54:23 +0000 Subject: [PATCH 2/3] Code contracts: do not interleave checking and instrumenting Loop normalisation must first check that all loops described via `natural_loopst` are of the expected shape and then start inserting or transforming instructions. Else, and depending on loop shapes and loop nesting, the instruction iterators held in the `natural_loopst` may no longer be adequate descriptions of the loops. (The iterators weren't invalidated, but would no longer point to heads or loop ends.) --- .../loop_contracts_do_while/main.c | 10 +-- .../loop_contracts_do_while/nested.c | 16 +++++ .../loop_contracts_do_while/nested.desc | 9 +++ .../test.desc | 8 +-- src/goto-instrument/contracts/contracts.cpp | 68 ++++++++++++------- .../dfcc_check_loop_normal_form.cpp | 14 ++++ .../goto_instrument_parse_options.cpp | 12 ++-- 7 files changed, 99 insertions(+), 38 deletions(-) create mode 100644 regression/contracts-dfcc/loop_contracts_do_while/nested.c create mode 100644 regression/contracts-dfcc/loop_contracts_do_while/nested.desc diff --git a/regression/contracts-dfcc/loop_contracts_do_while/main.c b/regression/contracts-dfcc/loop_contracts_do_while/main.c index 88477df7fc2..8519d3953fb 100644 --- a/regression/contracts-dfcc/loop_contracts_do_while/main.c +++ b/regression/contracts-dfcc/loop_contracts_do_while/main.c @@ -5,9 +5,11 @@ int main() int x = 0; do - { - x++; - } while(x < 10) __CPROVER_loop_invariant(0 <= x && x <= 10); + __CPROVER_loop_invariant(0 <= x && x <= 10) + { + x++; + } + while(x < 10); - assert(x == 10); + assert(x <= 10); } diff --git a/regression/contracts-dfcc/loop_contracts_do_while/nested.c b/regression/contracts-dfcc/loop_contracts_do_while/nested.c new file mode 100644 index 00000000000..f926264b78f --- /dev/null +++ b/regression/contracts-dfcc/loop_contracts_do_while/nested.c @@ -0,0 +1,16 @@ +#include + +int main() +{ + int x = 0; + + do + { + do + { + x++; + } while(0); + } while(0); + + assert(x <= 10); +} diff --git a/regression/contracts-dfcc/loop_contracts_do_while/nested.desc b/regression/contracts-dfcc/loop_contracts_do_while/nested.desc new file mode 100644 index 00000000000..20cdc6fa135 --- /dev/null +++ b/regression/contracts-dfcc/loop_contracts_do_while/nested.desc @@ -0,0 +1,9 @@ +KNOWNBUG +nested.c +--dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +We spuriously report that x is not assignable. diff --git a/regression/contracts-dfcc/loop_contracts_reject_loops_two_latches/test.desc b/regression/contracts-dfcc/loop_contracts_reject_loops_two_latches/test.desc index 0c2a66a7b05..044656dbb72 100644 --- a/regression/contracts-dfcc/loop_contracts_reject_loops_two_latches/test.desc +++ b/regression/contracts-dfcc/loop_contracts_reject_loops_two_latches/test.desc @@ -1,10 +1,10 @@ CORE dfcc-only main.c --dfcc main --apply-loop-contracts -^Found loop with more than one latch instruction$ -^EXIT=(6|10)$ +^EXIT=10$ ^SIGNAL=0$ -- +^Found loop with more than one latch instruction$ -- -This test checks that our loop contract instrumentation verifies that loops -nested in loops with contracts also have contracts. +This test checks that our loop contract instrumentation first transforms loops +so as to only have a single loop latch. diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 8b9e9ee23e8..ecf6fc0adf5 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -888,6 +888,12 @@ void code_contractst::apply_loop_contract( std::list to_check_contracts_on_children; + std::map< + goto_programt::targett, + std::pair, + goto_programt::target_less_than> + loop_head_ends; + for(const auto &loop_head_and_content : natural_loops.loop_map) { const auto &loop_content = loop_head_and_content.second; @@ -914,6 +920,42 @@ void code_contractst::apply_loop_contract( throw 0; } + // By definition the `loop_content` is a set of instructions computed + // by `natural_loops` based on the CFG. + // Since we perform assigns clause instrumentation by sequentially + // traversing instructions from `loop_head` to `loop_end`, + // here we ensure that all instructions in `loop_content` belong within + // the [loop_head, loop_end] target range. + + // Check 1. (i \in loop_content) ==> loop_head <= i <= loop_end + for(const auto &i : loop_content) + { + if( + loop_head->location_number > i->location_number || + i->location_number > loop_end->location_number) + { + log.conditional_output( + log.error(), [&i, &loop_head](messaget::mstreamt &mstream) { + mstream << "Computed loop at " << loop_head->source_location() + << "contains an instruction beyond [loop_head, loop_end]:" + << messaget::eom; + i->output(mstream); + mstream << messaget::eom; + }); + throw 0; + } + } + + if(!loop_head_ends + .emplace(loop_head, std::make_pair(loop_end, loop_content)) + .second) + UNREACHABLE; + } + + for(auto &loop_head_end : loop_head_ends) + { + auto loop_head = loop_head_end.first; + auto loop_end = loop_head_end.second.first; // After loop-contract instrumentation, jumps to the `loop_head` will skip // some instrumented instructions. So we want to make sure that there is // only one jump targeting `loop_head` from `loop_end` before loop-contract @@ -961,7 +1003,7 @@ void code_contractst::apply_loop_contract( } const auto idx = loop_nesting_graph.add_node( - loop_content, + loop_head_end.second.second, loop_head, loop_end, assigns_clause, @@ -974,30 +1016,6 @@ void code_contractst::apply_loop_contract( continue; to_check_contracts_on_children.push_back(idx); - - // By definition the `loop_content` is a set of instructions computed - // by `natural_loops` based on the CFG. - // Since we perform assigns clause instrumentation by sequentially - // traversing instructions from `loop_head` to `loop_end`, - // here we ensure that all instructions in `loop_content` belong within - // the [loop_head, loop_end] target range - - // Check 1. (i \in loop_content) ==> loop_head <= i <= loop_end - for(const auto &i : loop_content) - { - if(std::distance(loop_head, i) < 0 || std::distance(i, loop_end) < 0) - { - log.conditional_output( - log.error(), [&i, &loop_head](messaget::mstreamt &mstream) { - mstream << "Computed loop at " << loop_head->source_location() - << "contains an instruction beyond [loop_head, loop_end]:" - << messaget::eom; - i->output(mstream); - mstream << messaget::eom; - }); - throw 0; - } - } } for(size_t outer = 0; outer < loop_nesting_graph.size(); ++outer) diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_check_loop_normal_form.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_check_loop_normal_form.cpp index 2c0e5d03619..38d86e9d5c8 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_check_loop_normal_form.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_check_loop_normal_form.cpp @@ -19,6 +19,12 @@ void dfcc_check_loop_normal_form(goto_programt &goto_program, messaget &log) // instruction span for each loop std::vector> spans; + std::map< + goto_programt::targett, + goto_programt::targett, + goto_programt::target_less_than> + latch_head_pairs; + for(auto &loop : natural_loops.loop_map) { auto head = loop.first; @@ -132,7 +138,15 @@ void dfcc_check_loop_normal_form(goto_programt &goto_program, messaget &log) "nested loop head and latch are in outer loop"); } + if(!latch_head_pairs.emplace(latch, head).second) + UNREACHABLE; + } + // all checks passed, now we perform some instruction rewriting + for(auto &entry_pair : latch_head_pairs) + { + auto latch = entry_pair.first; + auto head = entry_pair.second; // Convert conditional latch into exiting + unconditional latch. // ``` diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index cc78444fcd8..db030ac89b5 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1174,6 +1174,8 @@ void goto_instrument_parse_optionst::instrument_goto_program() } do_indirect_call_and_rtti_removal(); + log.status() << "Trying to force one backedge per target" << messaget::eom; + ensure_one_backedge_per_target(goto_model); const irep_idt harness_id(cmdline.get_value(FLAG_DFCC)); @@ -1232,13 +1234,13 @@ void goto_instrument_parse_optionst::instrument_goto_program() to_exclude_from_nondet_static, log.get_message_handler()); } - - if( - !use_dfcc && - (cmdline.isset(FLAG_LOOP_CONTRACTS) || cmdline.isset(FLAG_REPLACE_CALL) || - cmdline.isset(FLAG_ENFORCE_CONTRACT))) + else if((cmdline.isset(FLAG_LOOP_CONTRACTS) || + cmdline.isset(FLAG_REPLACE_CALL) || + cmdline.isset(FLAG_ENFORCE_CONTRACT))) { do_indirect_call_and_rtti_removal(); + log.status() << "Trying to force one backedge per target" << messaget::eom; + ensure_one_backedge_per_target(goto_model); code_contractst contracts(goto_model, log); std::set to_replace( From e2e3e0ecb50197850daf360f284095596f40a7f0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 23 Jan 2024 11:49:29 +0000 Subject: [PATCH 3/3] Rename loop_content to loop_body This is to use standard terminology. --- src/goto-instrument/contracts/contracts.cpp | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index ecf6fc0adf5..ca8189ff846 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -896,16 +896,16 @@ void code_contractst::apply_loop_contract( for(const auto &loop_head_and_content : natural_loops.loop_map) { - const auto &loop_content = loop_head_and_content.second; + const auto &loop_body = loop_head_and_content.second; // Skip empty loops and self-looped node. - if(loop_content.size() <= 1) + if(loop_body.size() <= 1) continue; auto loop_head = loop_head_and_content.first; auto loop_end = loop_head; // Find the last back edge to `loop_head` - for(const auto &t : loop_content) + for(const auto &t : loop_body) { if( t->is_goto() && t->get_target() == loop_head && @@ -920,15 +920,15 @@ void code_contractst::apply_loop_contract( throw 0; } - // By definition the `loop_content` is a set of instructions computed + // By definition the `loop_body` is a set of instructions computed // by `natural_loops` based on the CFG. // Since we perform assigns clause instrumentation by sequentially // traversing instructions from `loop_head` to `loop_end`, - // here we ensure that all instructions in `loop_content` belong within + // here we ensure that all instructions in `loop_body` belong within // the [loop_head, loop_end] target range. - // Check 1. (i \in loop_content) ==> loop_head <= i <= loop_end - for(const auto &i : loop_content) + // Check 1. (i \in loop_body) ==> loop_head <= i <= loop_end + for(const auto &i : loop_body) { if( loop_head->location_number > i->location_number || @@ -946,8 +946,7 @@ void code_contractst::apply_loop_contract( } } - if(!loop_head_ends - .emplace(loop_head, std::make_pair(loop_end, loop_content)) + if(!loop_head_ends.emplace(loop_head, std::make_pair(loop_end, loop_body)) .second) UNREACHABLE; }