cprover
all_paths_enumerator.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Loop Acceleration
4 
5 Author: Matt Lewis
6 
7 \*******************************************************************/
8 
11 
12 #include "all_paths_enumerator.h"
13 
14 #include <iostream>
15 
17 {
18  if(last_path.empty())
19  {
20  // This is the first time we've been called -- build an initial
21  // path.
22  last_path.push_back(path_nodet(loop_header));
23 
24  // This shouldn't be able to fail.
26 
28  {
29  // If this was a loop path, we're good. If it wasn't,
30  // we'll keep enumerating paths until we hit a looping one.
31  // This case is exactly the same as if someone just called
32  // next() on us.
33  path.clear();
34  path.insert(path.begin(), last_path.begin(), last_path.end());
35  return true;
36  }
37  }
38 
39  do
40  {
41 #ifdef DEBUG
42  std::cout << "Enumerating next path...\n";
43 #endif
44 
45  int decision=backtrack(last_path);
46  complete_path(last_path, decision);
47 
49  {
50  path.clear();
51  path.insert(path.begin(), last_path.begin(), last_path.end());
52  return true;
53  }
54  }
55  while(!last_path.empty());
56 
57  // We've enumerated all the paths.
58  return false;
59 }
60 
62 {
63  // If we have a path of length 1 or 0, we can't backtrack any further.
64  // That means we're done enumerating paths!
65  if(path.size()<2)
66  {
67  path.clear();
68  return 0;
69  }
70 
71  goto_programt::targett node_loc=path.back().loc;
72  path.pop_back();
73 
74  goto_programt::targett parent_loc=path.back().loc;
75  const auto succs=goto_program.get_successors(parent_loc);
76 
77  unsigned int ret=0;
78 
79  for(const auto &succ : succs)
80  {
81  if(succ==node_loc)
82  break;
83 
84  ret++;
85  }
86 
87  if((ret+1)<succs.size())
88  {
89  // We can take the next branch here...
90 
91 #ifdef DEBUG
92  std::cout << "Backtracked to a path of size " << path.size() << '\n';
93 #endif
94 
95  return ret+1;
96  }
97 
98  // Recurse.
99  return backtrack(path);
100 }
101 
103 {
104  if(path.empty())
105  return;
106 
107  goto_programt::targett node_loc=path.back().loc;
108  extend_path(path, node_loc, succ);
109 
110  goto_programt::targett end=path.back().loc;
111 
112  if(end == loop_header || !loop.contains(end))
113  return;
114 
115  complete_path(path, 0);
116 }
117 
119  patht &path,
121  int succ)
122 {
124  exprt guard=true_exprt();
125 
126  for(const auto &s : goto_program.get_successors(t))
127  {
128  if(succ==0)
129  {
130  next=s;
131  break;
132  }
133 
134  succ--;
135  }
136 
137  if(t->is_goto())
138  {
139  guard = not_exprt(t->get_condition());
140 
141  for(goto_programt::targetst::iterator it=t->targets.begin();
142  it != t->targets.end();
143  ++it)
144  {
145  if(next == *it)
146  {
147  guard = t->get_condition();
148  break;
149  }
150  }
151  }
152 
153  path.push_back(path_nodet(next, guard));
154 }
155 
157 {
158  return path.size()>1 && path.back().loc==loop_header;
159 }
all_paths_enumeratort::extend_path
void extend_path(patht &path, goto_programt::targett t, int succ)
Definition: all_paths_enumerator.cpp:118
exprt
Base class for all expressions.
Definition: expr.h:53
path_nodet
Definition: path.h:24
all_paths_enumeratort::loop
natural_loops_mutablet::natural_loopt & loop
Definition: all_paths_enumerator.h:44
goto_programt::get_successors
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
Definition: goto_program.h:1084
all_paths_enumeratort::goto_program
goto_programt & goto_program
Definition: all_paths_enumerator.h:43
all_paths_enumeratort::loop_header
goto_programt::targett loop_header
Definition: all_paths_enumerator.h:45
all_paths_enumeratort::last_path
patht last_path
Definition: all_paths_enumerator.h:47
all_paths_enumeratort::is_looping
bool is_looping(patht &path)
Definition: all_paths_enumerator.cpp:156
all_paths_enumeratort::backtrack
int backtrack(patht &path)
Definition: all_paths_enumerator.cpp:61
all_paths_enumeratort::complete_path
void complete_path(patht &path, int succ)
Definition: all_paths_enumerator.cpp:102
patht
std::list< path_nodet > patht
Definition: path.h:45
all_paths_enumeratort::next
virtual bool next(patht &path)
Definition: all_paths_enumerator.cpp:16
all_paths_enumerator.h
Loop Acceleration.
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
loop_templatet::contains
virtual bool contains(const T instruction) const
Returns true if instruction is in this loop.
Definition: loop_analysis.h:40
not_exprt
Boolean negation.
Definition: std_expr.h:2843