CBMC
loop_analysis.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Loop analysis
4 
5 Author: Diffblue Ltd
6 
7 \*******************************************************************/
8 
12 
13 #ifndef CPROVER_ANALYSES_LOOP_ANALYSIS_H
14 #define CPROVER_ANALYSES_LOOP_ANALYSIS_H
15 
17 
18 template <class T, typename C>
19 class loop_analysist;
20 
22 template <class T, typename C>
24 {
25  typedef std::set<T, C> loop_instructionst;
27 
29 
30 public:
31  loop_templatet() = default;
32 
33  template <typename InstructionSet>
34  explicit loop_templatet(InstructionSet &&instructions)
35  : loop_instructions(std::forward<InstructionSet>(instructions))
36  {
37  }
38 
40  bool virtual contains(const T instruction) const
41  {
42  return !loop_instructions.empty() && loop_instructions.count(instruction);
43  }
44 
45  // NOLINTNEXTLINE(readability/identifiers)
46  typedef typename loop_instructionst::const_iterator const_iterator;
47 
50  {
51  return loop_instructions.begin();
52  }
53 
56  {
57  return loop_instructions.end();
58  }
59 
61  std::size_t size() const
62  {
63  return loop_instructions.size();
64  }
65 
67  bool empty() const
68  {
69  return loop_instructions.empty();
70  }
71 
74  bool insert_instruction(const T instruction)
75  {
76  return loop_instructions.insert(instruction).second;
77  }
78 };
79 
80 template <class T, typename C>
82 {
83 public:
85  // map loop headers to loops
86  typedef std::map<T, loopt, C> loop_mapt;
87 
89 
90  virtual void output(std::ostream &) const;
91 
93  bool is_loop_header(const T instruction) const
94  {
95  return loop_map.count(instruction);
96  }
97 
98  loop_analysist() = default;
99 };
100 
101 template <typename T, typename C>
103 {
105 
106 public:
109  {
110  }
111 
112  template <typename InstructionSet>
115  InstructionSet &&instructions)
116  : loop_templatet<T, C>(std::forward<InstructionSet>(instructions)),
118  {
119  }
120 
123  const typename loop_analysist<T, C>::loopt &loop,
124  const T instruction) const
125  {
126  return loop.loop_instructions.count(instruction);
127  }
128 
131  {
132  return loop_analysis;
133  }
136  {
137  return loop_analysis;
138  }
139 
140 private:
142 };
143 
144 template <class T, typename C>
146 {
147 public:
149 
152  const typename loop_analysist<T, C>::loopt &loop,
153  const T instruction) const
154  {
155  return loop.loop_instructions.count(instruction);
156  }
157 
158  // The loop structures stored in `loop_map` contain back-pointers to this
159  // class, so we forbid copying or moving the analysis struct. If this becomes
160  // necessary then either add a layer of indirection or update the loop_map
161  // back-pointers on copy/move.
166 };
167 
169 template <class T, typename C>
170 void loop_analysist<T, C>::output(std::ostream &out) const
171 {
172  for(const auto &loop : loop_map)
173  {
174  unsigned n = loop.first->location_number;
175 
176  std::unordered_set<std::size_t> backedge_location_numbers;
177  for(const auto &backedge : loop.first->incoming_edges)
178  backedge_location_numbers.insert(backedge->location_number);
179 
180  out << n << " is head of { ";
181 
182  std::vector<std::size_t> loop_location_numbers;
183  for(const auto &loop_instruction_it : loop.second)
184  loop_location_numbers.push_back(loop_instruction_it->location_number);
185  std::sort(loop_location_numbers.begin(), loop_location_numbers.end());
186 
187  for(const auto location_number : loop_location_numbers)
188  {
189  if(location_number != loop_location_numbers.at(0))
190  out << ", ";
191  out << location_number;
192  if(backedge_location_numbers.count(location_number))
193  out << " (backedge)";
194  }
195  out << " }\n";
196  }
197 }
198 
199 template <class LoopAnalysis>
200 void show_loops(const goto_modelt &goto_model, std::ostream &out)
201 {
202  for(const auto &gf_entry : goto_model.goto_functions.function_map)
203  {
204  out << "*** " << gf_entry.first << '\n';
205 
206  LoopAnalysis loop_analysis;
207  loop_analysis(gf_entry.second.body);
208  loop_analysis.output(out);
209 
210  out << '\n';
211  }
212 }
213 
214 #endif // CPROVER_ANALYSES_LOOP_ANALYSIS_H
function_mapt function_map
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
bool loop_contains(const typename loop_analysist< T, C >::loopt &loop, const T instruction) const
Returns true if instruction is in loop.
linked_loop_analysist & operator=(linked_loop_analysist &&)=delete
linked_loop_analysist(const linked_loop_analysist &)=delete
linked_loop_analysist(linked_loop_analysist &&)=delete
linked_loop_analysist & operator=(const linked_loop_analysist &)=delete
linked_loop_analysist()=default
std::map< T, loopt, C > loop_mapt
Definition: loop_analysis.h:86
loop_mapt loop_map
Definition: loop_analysis.h:88
loop_templatet< T, C > loopt
Definition: loop_analysis.h:84
bool is_loop_header(const T instruction) const
Returns true if instruction is the header of any loop.
Definition: loop_analysis.h:93
loop_analysist()=default
virtual void output(std::ostream &) const
Print all natural loops that were found.
A loop, specified as a set of instructions.
Definition: loop_analysis.h:24
loop_instructionst loop_instructions
Definition: loop_analysis.h:26
bool insert_instruction(const T instruction)
Adds instruction to this loop.
Definition: loop_analysis.h:74
const_iterator end() const
Iterator over this loop's instructions.
Definition: loop_analysis.h:55
const_iterator begin() const
Iterator over this loop's instructions.
Definition: loop_analysis.h:49
std::size_t size() const
Number of instructions in this loop.
Definition: loop_analysis.h:61
bool empty() const
Returns true if this loop contains no instructions.
Definition: loop_analysis.h:67
virtual bool contains(const T instruction) const
Returns true if instruction is in this loop.
Definition: loop_analysis.h:40
loop_templatet(InstructionSet &&instructions)
Definition: loop_analysis.h:34
loop_instructionst::const_iterator const_iterator
Definition: loop_analysis.h:46
loop_templatet()=default
std::set< T, C > loop_instructionst
Definition: loop_analysis.h:25
loop_with_parent_analysis_templatet(parent_analysist &loop_analysis, InstructionSet &&instructions)
bool loop_contains(const typename loop_analysist< T, C >::loopt &loop, const T instruction) const
Returns true if instruction is in loop.
loop_with_parent_analysis_templatet(parent_analysist &loop_analysis)
parent_analysist & get_loop_analysis()
Get the parent_analysist analysis this loop relates to.
const parent_analysist & get_loop_analysis() const
Get the parent_analysist analysis this loop relates to.
loop_analysist< T, C > parent_analysist
Symbol Table + CFG.
void show_loops(const goto_modelt &goto_model, std::ostream &out)