diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index 1de892e76d7..cd0899fd79b 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -23,6 +23,7 @@ Date: September 2021 #include +#include #include #include @@ -610,3 +611,130 @@ unsigned get_suffix_unsigned(const std::string &str, const std::string &prefix) std::string result = str.substr(first_index, last_index - first_index); return std::stol(result); } + +goto_programt::const_targett get_loop_end_from_loop_head_and_content( + const goto_programt::const_targett &loop_head, + const loop_templatet< + goto_programt::const_targett, + goto_programt::target_less_than> &loop) +{ + goto_programt::const_targett loop_end = loop_head; + for(const auto &t : loop) + { + // an instruction is the loop end if it is a goto instruction + // and it jumps backward to the loop head + if( + t->is_goto() && t->get_target() == loop_head && + t->location_number > loop_end->location_number) + loop_end = t; + } + INVARIANT( + loop_head != loop_end, + "Could not find end of the loop starting at: " + + loop_head->source_location().as_string()); + + return loop_end; +} + +goto_programt::targett get_loop_end_from_loop_head_and_content_mutable( + const goto_programt::targett &loop_head, + const loop_templatet + &loop) +{ + goto_programt::targett loop_end = loop_head; + for(const auto &t : loop) + { + // an instruction is the loop end if it is a goto instruction + // and it jumps backward to the loop head + if( + t->is_goto() && t->get_target() == loop_head && + t->location_number > loop_end->location_number) + loop_end = t; + } + INVARIANT( + loop_head != loop_end, + "Could not find end of the loop starting at: " + + loop_head->source_location().as_string()); + + return loop_end; +} + +goto_programt::targett get_loop_head_or_end( + const unsigned int target_loop_number, + goto_functiont &function, + bool finding_head) +{ + natural_loops_mutablet natural_loops(function.body); + + // iterate over all natural loops to find the loop with `target_loop_number` + for(const auto &loop_p : natural_loops.loop_map) + { + const goto_programt::targett loop_head = loop_p.first; + goto_programt::targett loop_end = + get_loop_end_from_loop_head_and_content_mutable(loop_head, loop_p.second); + // check if the current loop is the target loop by comparing loop number + if(loop_end->loop_number == target_loop_number) + { + if(finding_head) + return loop_head; + else + return loop_end; + } + } + + UNREACHABLE; +} + +goto_programt::targett +get_loop_end(const unsigned int target_loop_number, goto_functiont &function) +{ + return get_loop_head_or_end(target_loop_number, function, false); +} + +goto_programt::targett +get_loop_head(const unsigned int target_loop_number, goto_functiont &function) +{ + return get_loop_head_or_end(target_loop_number, function, true); +} + +void annotate_invariants( + const invariant_mapt &invariant_map, + goto_modelt &goto_model) +{ + for(const auto &invariant_map_entry : invariant_map) + { + loop_idt loop_id = invariant_map_entry.first; + irep_idt function_id = loop_id.function_id; + unsigned int loop_number = loop_id.loop_number; + + // get the last instruction of the target loop + auto &function = goto_model.goto_functions.function_map[function_id]; + goto_programt::targett loop_end = get_loop_end(loop_number, function); + + // annotate the invariant to the condition of `loop_end` + loop_end->condition_nonconst().add(ID_C_spec_loop_invariant) = + invariant_map_entry.second; + } +} + +void annotate_assigns( + const std::map> &assigns_map, + goto_modelt &goto_model) +{ + for(const auto &assigns_map_entry : assigns_map) + { + loop_idt loop_id = assigns_map_entry.first; + irep_idt function_id = loop_id.function_id; + unsigned int loop_number = loop_id.loop_number; + + // get the last instruction of the target loop + auto &function = goto_model.goto_functions.function_map[function_id]; + goto_programt::targett loop_end = get_loop_end(loop_number, function); + + exprt &condition = loop_end->condition_nonconst(); + auto assigns = exprt(ID_target_list); + for(const auto &e : assigns_map_entry.second) + assigns.add_to_operands(e); + condition.add(ID_C_spec_assigns) = assigns; + } +} diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h index 1d3ab53f8cc..81173aed8fc 100644 --- a/src/goto-instrument/contracts/utils.h +++ b/src/goto-instrument/contracts/utils.h @@ -14,6 +14,7 @@ Date: September 2021 #include #include +#include #include @@ -24,6 +25,10 @@ Date: September 2021 #define IN_LOOP_HAVOC_BLOCK "__in_loop_havoc_block" #define INIT_INVARIANT "__init_invariant" +template +class loop_templatet; +typedef std::map invariant_mapt; + /// Class that allows to clean expressions of side effects and to generate /// havoc_slice expressions. class cleanert : public goto_convertt @@ -271,4 +276,45 @@ bool is_assignment_to_instrumented_variable( /// Convert the suffix digits right after `prefix` of `str` into unsigned. unsigned get_suffix_unsigned(const std::string &str, const std::string &prefix); +/// Find the goto instruction of `loop` that jumps to `loop_head` +goto_programt::targett get_loop_end_from_loop_head_and_content_mutable( + const goto_programt::targett &loop_head, + const loop_templatet + &loop); + +goto_programt::const_targett get_loop_end_from_loop_head_and_content( + const goto_programt::const_targett &loop_head, + const loop_templatet< + goto_programt::const_targett, + goto_programt::target_less_than> &loop); + +/// Return loop head if `finding_head` is true, +/// Otherwise return loop end. +goto_programt::targett get_loop_head_or_end( + const unsigned int loop_number, + goto_functiont &function, + bool finding_head); + +/// Find and return the last instruction of the natural loop with +/// `loop_number` in `function`. loop_end -> loop_head +goto_programt::targett +get_loop_end(const unsigned int loop_number, goto_functiont &function); + +/// Find and return the first instruction of the natural loop with +/// `loop_number` in `function`. loop_end -> loop_head +goto_programt::targett +get_loop_head(const unsigned int loop_number, goto_functiont &function); + +/// Annotate the invariants in `invariant_map` to their corresponding +/// loops. Corresponding loops are specified by keys of `invariant_map` +void annotate_invariants( + const invariant_mapt &invariant_map, + goto_modelt &goto_model); + +/// Annotate the assigns in `assigns_map` to their corresponding +/// loops. Corresponding loops are specified by keys of `assigns_map` +void annotate_assigns( + const std::map> &assigns_map, + goto_modelt &goto_model); + #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H diff --git a/src/goto-synthesizer/synthesizer_utils.cpp b/src/goto-synthesizer/synthesizer_utils.cpp index f86d9e46316..8ea4aec6f5a 100644 --- a/src/goto-synthesizer/synthesizer_utils.cpp +++ b/src/goto-synthesizer/synthesizer_utils.cpp @@ -8,139 +8,6 @@ Author: Qinheping Hu #include "synthesizer_utils.h" -#include - -#include -#include -#include - -goto_programt::const_targett get_loop_end_from_loop_head_and_content( - const goto_programt::const_targett &loop_head, - const loop_templatet< - goto_programt::const_targett, - goto_programt::target_less_than> &loop) -{ - goto_programt::const_targett loop_end = loop_head; - for(const auto &t : loop) - { - // an instruction is the loop end if it is a goto instruction - // and it jumps backward to the loop head - if( - t->is_goto() && t->get_target() == loop_head && - t->location_number > loop_end->location_number) - loop_end = t; - } - INVARIANT( - loop_head != loop_end, - "Could not find end of the loop starting at: " + - loop_head->source_location().as_string()); - - return loop_end; -} - -goto_programt::targett get_loop_end_from_loop_head_and_content_mutable( - const goto_programt::targett &loop_head, - const loop_templatet - &loop) -{ - goto_programt::targett loop_end = loop_head; - for(const auto &t : loop) - { - // an instruction is the loop end if it is a goto instruction - // and it jumps backward to the loop head - if( - t->is_goto() && t->get_target() == loop_head && - t->location_number > loop_end->location_number) - loop_end = t; - } - INVARIANT( - loop_head != loop_end, - "Could not find end of the loop starting at: " + - loop_head->source_location().as_string()); - - return loop_end; -} - -goto_programt::targett get_loop_head_or_end( - const unsigned int target_loop_number, - goto_functiont &function, - bool finding_head) -{ - natural_loops_mutablet natural_loops(function.body); - - // iterate over all natural loops to find the loop with `target_loop_number` - for(const auto &loop_p : natural_loops.loop_map) - { - const goto_programt::targett loop_head = loop_p.first; - goto_programt::targett loop_end = - get_loop_end_from_loop_head_and_content_mutable(loop_head, loop_p.second); - // check if the current loop is the target loop by comparing loop number - if(loop_end->loop_number == target_loop_number) - { - if(finding_head) - return loop_head; - else - return loop_end; - } - } - - UNREACHABLE; -} - -goto_programt::targett -get_loop_end(const unsigned int target_loop_number, goto_functiont &function) -{ - return get_loop_head_or_end(target_loop_number, function, false); -} - -goto_programt::targett -get_loop_head(const unsigned int target_loop_number, goto_functiont &function) -{ - return get_loop_head_or_end(target_loop_number, function, true); -} - -void annotate_invariants( - const invariant_mapt &invariant_map, - goto_modelt &goto_model) -{ - for(const auto &invariant_map_entry : invariant_map) - { - loop_idt loop_id = invariant_map_entry.first; - irep_idt function_id = loop_id.function_id; - unsigned int loop_number = loop_id.loop_number; - - // get the last instruction of the target loop - auto &function = goto_model.goto_functions.function_map[function_id]; - goto_programt::targett loop_end = get_loop_end(loop_number, function); - - // annotate the invariant to the condition of `loop_end` - loop_end->condition_nonconst().add(ID_C_spec_loop_invariant) = - invariant_map_entry.second; - } -} - -void annotate_assigns( - const std::map> &assigns_map, - goto_modelt &goto_model) -{ - for(const auto &assigns_map_entry : assigns_map) - { - loop_idt loop_id = assigns_map_entry.first; - irep_idt function_id = loop_id.function_id; - unsigned int loop_number = loop_id.loop_number; - - // get the last instruction of the target loop - auto &function = goto_model.goto_functions.function_map[function_id]; - goto_programt::targett loop_end = get_loop_end(loop_number, function); - - exprt &condition = loop_end->condition_nonconst(); - auto assigns = exprt(ID_target_list); - for(const auto &e : assigns_map_entry.second) - assigns.add_to_operands(e); - condition.add(ID_C_spec_assigns) = assigns; - } -} - invariant_mapt combine_in_and_post_invariant_clauses( const invariant_mapt &in_clauses, const invariant_mapt &post_clauses, diff --git a/src/goto-synthesizer/synthesizer_utils.h b/src/goto-synthesizer/synthesizer_utils.h index 5c130c42752..38f52f30e7d 100644 --- a/src/goto-synthesizer/synthesizer_utils.h +++ b/src/goto-synthesizer/synthesizer_utils.h @@ -9,56 +9,7 @@ Author: Qinheping Hu #ifndef CPROVER_GOTO_SYNTHESIZER_SYNTHESIZER_UTILS_H #define CPROVER_GOTO_SYNTHESIZER_SYNTHESIZER_UTILS_H -#include -#include -#include - -class goto_functiont; -class messaget; -template -class loop_templatet; - -typedef std::map invariant_mapt; - -/// Find the goto instruction of `loop` that jumps to `loop_head` -goto_programt::targett get_loop_end_from_loop_head_and_content_mutable( - const goto_programt::targett &loop_head, - const loop_templatet - &loop); -goto_programt::const_targett get_loop_end_from_loop_head_and_content( - const goto_programt::const_targett &loop_head, - const loop_templatet< - goto_programt::const_targett, - goto_programt::target_less_than> &loop); - -/// Return loop head if `finding_head` is true, -/// Otherwise return loop end. -goto_programt::targett get_loop_head_or_end( - const unsigned int loop_number, - goto_functiont &function, - bool finding_head); - -/// Find and return the last instruction of the natural loop with -/// `loop_number` in `function`. loop_end -> loop_head -goto_programt::targett -get_loop_end(const unsigned int loop_number, goto_functiont &function); - -/// Find and return the first instruction of the natural loop with -/// `loop_number` in `function`. loop_end -> loop_head -goto_programt::targett -get_loop_head(const unsigned int loop_number, goto_functiont &function); - -/// Annotate the invariants in `invariant_map` to their corresponding -/// loops. Corresponding loops are specified by keys of `invariant_map` -void annotate_invariants( - const invariant_mapt &invariant_map, - goto_modelt &goto_model); - -/// Annotate the assigns in `assigns_map` to their corresponding -/// loops. Corresponding loops are specified by keys of `assigns_map` -void annotate_assigns( - const std::map> &assigns_map, - goto_modelt &goto_model); +#include /// Combine invariant of form /// (in_inv || !guard) && (!guard -> pos_inv)