22 : head(head), latch(latch), instructions(instructions)
32 for(
auto &loop : natural_loops.
loop_map)
34 auto loop_head = loop.first;
35 auto &loop_instructions = loop.second;
37 if(loop_instructions.size() <= 1)
46 auto loop_latch = loop_head;
47 for(
const auto &t : loop_instructions)
50 t->is_goto() && t->get_target() == loop_head &&
51 t->location_number > loop_latch->location_number)
55 DATA_INVARIANT(loop_latch != loop_head,
"Natural loop latch is found");
57 loop_nesting_graph.
add_node(loop_head, loop_latch, loop_instructions);
63 for(
size_t outer = 0; outer < loop_nesting_graph.
size(); ++outer)
65 const auto &outer_instructions = loop_nesting_graph[outer].instructions;
67 for(
size_t inner = 0; inner < loop_nesting_graph.
size(); ++inner)
72 if(outer_instructions.contains(loop_nesting_graph[inner].head))
74 loop_nesting_graph.
add_edge(inner, outer);
79 auto topsorted_size = loop_nesting_graph.
topsort().size();
81 topsorted_size == loop_nesting_graph.
size(),
82 "loop_nesting_graph must be acyclic");
84 return loop_nesting_graph;
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
A generic directed graph with a parametric node type.
node_indext add_node(arguments &&... values)
void add_edge(node_indext a, node_indext b)
std::list< node_indext > topsort() const
Find a topological order of the nodes if graph is DAG, return empty list for non-DAG or empty graph.
A loop, specified as a set of instructions.
dfcc_loop_nesting_grapht build_loop_nesting_graph(goto_programt &goto_program)
Builds a graph instance describing the nesting structure of natural loops in the given goto_program.
Builds a graph describing how loops are nested in a GOTO program.
Compute natural loops in a goto_function.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
dfcc_loop_nesting_graph_nodet(const goto_programt::targett &head, const goto_programt::targett &latch, const loop_templatet< goto_programt::targett, goto_programt::target_less_than > &instructions)