CBMC
dfcc_loop_nesting_graph.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Dynamic frame condition checking
4 
5 Author: Qinheping Hu, qinhh@amazon.com
6 
7 Author: Remi Delmas, delmasrd@amazon.com
8 
9 Date: March 2023
10 
11 \*******************************************************************/
12 
14 
15 #include <analyses/natural_loops.h>
16 
18  const goto_programt::targett &head,
19  const goto_programt::targett &latch,
21  &instructions)
22  : head(head), latch(latch), instructions(instructions)
23 {
24 }
25 
28 {
29  natural_loops_mutablet natural_loops(goto_program);
30  dfcc_loop_nesting_grapht loop_nesting_graph;
31  // Add a node per natural loop
32  for(auto &loop : natural_loops.loop_map)
33  {
34  auto loop_head = loop.first;
35  auto &loop_instructions = loop.second;
36 
37  if(loop_instructions.size() <= 1)
38  {
39  // ignore single instruction loops of the form
40  // LOOP: goto LOOP;
41  continue;
42  }
43 
44  // Find the instruction that jumps back to `loop_head` and has the
45  // highest GOTO location number, define it as the latch.
46  auto loop_latch = loop_head;
47  for(const auto &t : loop_instructions)
48  {
49  if(
50  t->is_goto() && t->get_target() == loop_head &&
51  t->location_number > loop_latch->location_number)
52  loop_latch = t;
53  }
54 
55  DATA_INVARIANT(loop_latch != loop_head, "Natural loop latch is found");
56 
57  loop_nesting_graph.add_node(loop_head, loop_latch, loop_instructions);
58  }
59 
60  // Add edges to the graph, pointing from inner loop to outer loops.
61  // An `inner` will be considered nested in `outer` iff both its head
62  // and latch instructions are instructions of `outer`.
63  for(size_t outer = 0; outer < loop_nesting_graph.size(); ++outer)
64  {
65  const auto &outer_instructions = loop_nesting_graph[outer].instructions;
66 
67  for(size_t inner = 0; inner < loop_nesting_graph.size(); ++inner)
68  {
69  if(inner == outer)
70  continue;
71 
72  if(outer_instructions.contains(loop_nesting_graph[inner].head))
73  {
74  loop_nesting_graph.add_edge(inner, outer);
75  }
76  }
77  }
78 
79  auto topsorted_size = loop_nesting_graph.topsort().size();
80  INVARIANT(
81  topsorted_size == loop_nesting_graph.size(),
82  "loop_nesting_graph must be acyclic");
83 
84  return loop_nesting_graph;
85 }
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::iterator targett
Definition: goto_program.h:614
A generic directed graph with a parametric node type.
Definition: graph.h:167
node_indext add_node(arguments &&... values)
Definition: graph.h:180
void add_edge(node_indext a, node_indext b)
Definition: graph.h:232
std::size_t size() const
Definition: graph.h:212
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.
Definition: graph.h:879
loop_mapt loop_map
Definition: loop_analysis.h:88
A loop, specified as a set of instructions.
Definition: loop_analysis.h:24
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,...
Definition: invariant.h:534
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
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)