CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
dfcc_loop_nesting_graph.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dynamic frame condition checking
4
5Author: Qinheping Hu, qinhh@amazon.com
6
7Author: Remi Delmas, delmasrd@amazon.com
8
9Date: March 2023
10
11\*******************************************************************/
12
14
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);
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
73 {
75 }
76 }
77 }
78
79 auto topsorted_size = loop_nesting_graph.topsort().size();
82 "loop_nesting_graph must be acyclic");
83
84 return loop_nesting_graph;
85}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
loop_mapt loop_map
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)