20 std::vector<std::pair<goto_programt::targett, goto_programt::targett>> spans;
22 for(
auto &loop : natural_loops.
loop_map)
24 auto head = loop.first;
25 auto &loop_instructions = loop.second;
27 if(loop_instructions.size() <= 1)
35 bool latch_found =
false;
38 for(
const auto &t : loop_instructions)
40 if(t->is_goto() && t->get_target() == head)
44 log.
error() <<
"Loop starting at:"
46 <<
"\nhas more than one latch instruction:"
47 <<
"\n- latch1: " << latch->source_location()
48 <<
"\n- latch2: " << t->source_location()
51 "Found loop with more than one latch instruction");
58 INVARIANT(latch_found,
"Natural loop latch found");
61 for(
const auto &span : spans)
64 span.first->location_number <= head->location_number &&
65 head->location_number <= span.second->location_number;
68 span.first->location_number <= latch->location_number &&
69 latch->location_number <= span.second->location_number;
71 if(head_in_span != latch_in_span)
73 log.
error() <<
"Loop spanning:"
75 <<
"\n- latch: " << latch->source_location()
76 <<
"\noverlaps loop spanning:"
77 <<
"\n- head: " << span.first->source_location()
78 <<
"\n- latch: " << span.second->source_location()
81 "Found loops with overlapping instruction spans");
85 spans.push_back({head, latch});
91 for(
const auto &i : loop_instructions)
94 i->location_number < head->location_number ||
95 i->location_number > latch->location_number)
97 log.
error() <<
"Loop body instruction at:"
99 <<
"\n- head: " << head->source_location()
100 <<
"\n- latch: " << latch->source_location()
103 "Found loop body instruction outside of the [head, latch] "
107 for(
const auto &from : i->incoming_edges)
109 if(i != head && !loop_instructions.contains(from))
111 log.
error() <<
"Loop body instruction at:"
113 <<
"\n has incoming edge from outside the loop at:"
117 "Found loop body instruction with incoming edge from outside the "
125 for(
auto &other_loop : natural_loops.
loop_map)
127 auto &other_loop_instructions = other_loop.second;
128 bool contains_head = other_loop_instructions.contains(head);
129 bool contains_latch = other_loop_instructions.contains(latch);
131 contains_head == contains_latch,
132 "nested loop head and latch are in outer loop");
145 if(latch->has_condition() && !latch->condition().is_true())
161 exprt latch_condition = latch->condition();
162 latch_condition.
set(ID_value, ID_true);
172 latch->set_target(head);
void insert_before_and_update_jumps(goto_programt &destination, goto_programt::targett &target, const goto_programt::instructiont &i)
Insert a goto instruction before a target instruction iterator and update targets of all jumps that p...