20 std::vector<std::pair<goto_programt::targett, goto_programt::targett>> spans;
28 for(
auto &loop : natural_loops.
loop_map)
30 auto head = loop.first;
31 auto &loop_instructions = loop.second;
33 if(loop_instructions.size() <= 1)
41 bool latch_found =
false;
44 for(
const auto &t : loop_instructions)
46 if(t->is_goto() && t->get_target() == head)
50 log.
error() <<
"Loop starting at:"
52 <<
"\nhas more than one latch instruction:"
53 <<
"\n- latch1: " << latch->source_location()
54 <<
"\n- latch2: " << t->source_location()
57 "Found loop with more than one latch instruction");
64 INVARIANT(latch_found,
"Natural loop latch found");
67 for(
const auto &span : spans)
70 span.first->location_number <= head->location_number &&
71 head->location_number <= span.second->location_number;
74 span.first->location_number <= latch->location_number &&
75 latch->location_number <= span.second->location_number;
77 if(head_in_span != latch_in_span)
79 log.
error() <<
"Loop spanning:"
81 <<
"\n- latch: " << latch->source_location()
82 <<
"\noverlaps loop spanning:"
83 <<
"\n- head: " << span.first->source_location()
84 <<
"\n- latch: " << span.second->source_location()
87 "Found loops with overlapping instruction spans");
91 spans.push_back({head, latch});
97 for(
const auto &i : loop_instructions)
100 i->location_number < head->location_number ||
101 i->location_number > latch->location_number)
103 log.
error() <<
"Loop body instruction at:"
105 <<
"\n- head: " << head->source_location()
106 <<
"\n- latch: " << latch->source_location()
109 "Found loop body instruction outside of the [head, latch] "
113 for(
const auto &from : i->incoming_edges)
115 if(i != head && !loop_instructions.contains(from))
117 log.
error() <<
"Loop body instruction at:"
119 <<
"\n has incoming edge from outside the loop at:"
123 "Found loop body instruction with incoming edge from outside the "
131 for(
auto &other_loop : natural_loops.
loop_map)
133 auto &other_loop_instructions = other_loop.second;
134 bool contains_head = other_loop_instructions.contains(head);
135 bool contains_latch = other_loop_instructions.contains(latch);
137 contains_head == contains_latch,
138 "nested loop head and latch are in outer loop");
141 if(!latch_head_pairs.emplace(latch, head).second)
146 for(
auto &entry_pair : latch_head_pairs)
148 auto latch = entry_pair.first;
149 auto head = entry_pair.second;
159 if(latch->has_condition() && !latch->condition().is_true())
178 const exprt &latch_condition = latch->condition();
179 irept latch_assigns = latch_condition.
find(ID_C_spec_assigns);
181 new_condition.
add(ID_C_spec_assigns).
swap(latch_assigns);
183 irept latch_loop_invariant =
184 latch_condition.
find(ID_C_spec_loop_invariant);
186 new_condition.
add(ID_C_spec_loop_invariant).
swap(latch_loop_invariant);
188 irept latch_decreases = latch_condition.
find(ID_C_spec_decreases);
190 new_condition.
add(ID_C_spec_decreases).
swap(latch_decreases);
192 latch->condition_nonconst() = new_condition;
200 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...