cprover
Loading...
Searching...
No Matches
sat_path_enumerator.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Loop Acceleration
4
5Author: Matt Lewis
6
7\*******************************************************************/
8
11
12#include "sat_path_enumerator.h"
13
14#include <iostream>
15#include <map>
16#include <string>
17
20
21#include <util/std_code.h>
22
23#include "scratch_program.h"
24
26{
28
29 program.append(fixed);
30 program.append(fixed);
31
32 // Let's make sure that we get a path we have not seen before.
33 for(std::list<distinguish_valuest>::iterator it=accelerated_paths.begin();
34 it!=accelerated_paths.end();
35 ++it)
36 {
37 exprt new_path=false_exprt();
38
39 for(distinguish_valuest::iterator jt=it->begin();
40 jt!=it->end();
41 ++jt)
42 {
43 exprt distinguisher=jt->first;
44 bool taken=jt->second;
45
46 if(taken)
47 {
48 not_exprt negated(distinguisher);
49 distinguisher.swap(negated);
50 }
51
52 or_exprt disjunct(new_path, distinguisher);
53 new_path.swap(disjunct);
54 }
55
56 program.assume(new_path);
57 }
58
60
61 try
62 {
63 if(program.check_sat(guard_manager))
64 {
65#ifdef DEBUG
66 std::cout << "Found a path\n";
67#endif
68 build_path(program, path);
69 record_path(program);
70
71 return true;
72 }
73 }
74 catch(const std::string &s)
75 {
76 std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
77 }
78 catch(const char *s)
79 {
80 std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
81 }
82
83 return false;
84}
85
87{
88 for(natural_loops_mutablet::natural_loopt::const_iterator it = loop.begin();
89 it != loop.end();
90 ++it)
91 {
92 const auto succs=goto_program.get_successors(*it);
93
94 if(succs.size()>1)
95 {
96 // This location has multiple successors -- each successor is a
97 // distinguishing point.
98 for(const auto &succ : succs)
99 {
100 symbolt distinguisher_sym =
101 utils.fresh_symbol("polynomial::distinguisher", bool_typet());
102 symbol_exprt distinguisher=distinguisher_sym.symbol_expr();
103
104 distinguishing_points[succ]=distinguisher;
105 distinguishers.push_back(distinguisher);
106 }
107 }
108 }
109}
110
112 scratch_programt &scratch_program,
113 patht &path)
114{
116
117 do
118 {
120 const auto succs=goto_program.get_successors(t);
121
122 // We should have a looping path, so we should never hit a location
123 // with no successors.
124 assert(succs.size() > 0);
125
126 if(succs.size()==1)
127 {
128 // Only one successor -- accumulate it and move on.
129 path.push_back(path_nodet(t));
130 t=succs.front();
131 continue;
132 }
133
134 // We have multiple successors. Examine the distinguisher variables
135 // to see which branch was taken.
136 bool found_branch=false;
137
138 for(const auto &succ : succs)
139 {
140 exprt &distinguisher=distinguishing_points[succ];
141 bool taken=scratch_program.eval(distinguisher).is_true();
142
143 if(taken)
144 {
145 if(!found_branch ||
146 (succ->location_number < next->location_number))
147 {
148 next=succ;
149 }
150
151 found_branch=true;
152 }
153 }
154
155 assert(found_branch);
156
157 exprt cond=nil_exprt();
158
159 if(t->is_goto())
160 {
161 // If this was a conditional branch (it probably was), figure out
162 // if we hit the "taken" or "not taken" branch & accumulate the
163 // appropriate guard.
164 cond = not_exprt(t->get_condition());
165
166 for(goto_programt::targetst::iterator it=t->targets.begin();
167 it!=t->targets.end();
168 ++it)
169 {
170 if(next==*it)
171 {
172 cond = t->get_condition();
173 break;
174 }
175 }
176 }
177
178 path.push_back(path_nodet(t, cond));
179
180 t=next;
181 } while(t != loop_header && loop.contains(t));
182}
183
184/*
185 * Take the body of the loop we are accelerating and produce a fixed-path
186 * version of that body, suitable for use in the fixed-path acceleration we
187 * will be doing later.
188 */
190{
192 std::map<exprt, exprt> shadow_distinguishers;
193
195
196 for(auto &instruction : fixed.instructions)
197 {
198 if(instruction.is_assert())
199 instruction.turn_into_assume();
200 }
201
202 // We're only interested in paths that loop back to the loop header.
203 // As such, any path that jumps outside of the loop or jumps backwards
204 // to a location other than the loop header (i.e. a nested loop) is not
205 // one we're interested in, and we'll redirect it to this assume(false).
208
209 // Make a sentinel instruction to mark the end of the loop body.
210 // We'll use this as the new target for any back-jumps to the loop
211 // header.
213
214 // A pointer to the start of the fixed-path body. We'll be using this to
215 // iterate over the fixed-path body, but for now it's just a pointer to the
216 // first instruction.
218
219 // Create shadow distinguisher variables. These guys identify the path that
220 // is taken through the fixed-path body.
221 for(std::list<exprt>::iterator it=distinguishers.begin();
222 it!=distinguishers.end();
223 ++it)
224 {
225 exprt &distinguisher=*it;
226 symbolt shadow_sym=utils.fresh_symbol("polynomial::shadow_distinguisher",
227 bool_typet());
228 exprt shadow=shadow_sym.symbol_expr();
229 shadow_distinguishers[distinguisher]=shadow;
230
232 fixedt,
234 }
235
236 // We're going to iterate over the 2 programs in lockstep, which allows
237 // us to figure out which distinguishing point we've hit & instrument
238 // the relevant distinguisher variables.
240 t!=goto_program.instructions.end();
241 ++t, ++fixedt)
242 {
243 distinguish_mapt::iterator d=distinguishing_points.find(t);
244
245 if(!loop.contains(t))
246 {
247 // This instruction isn't part of the loop... Just remove it.
248 fixedt->turn_into_skip();
249 continue;
250 }
251
252 if(d!=distinguishing_points.end())
253 {
254 // We've hit a distinguishing point. Set the relevant shadow
255 // distinguisher to true.
256 exprt &distinguisher=d->second;
257 exprt &shadow=shadow_distinguishers[distinguisher];
258
260 fixedt,
262
263 assign->swap(*fixedt);
264 fixedt=assign;
265 }
266
267 if(t->is_goto())
268 {
269 assert(fixedt->is_goto());
270 // If this is a forwards jump, it's either jumping inside the loop
271 // (in which case we leave it alone), or it jumps outside the loop.
272 // If it jumps out of the loop, it's on a path we don't care about
273 // so we kill it.
274 //
275 // Otherwise, it's a backwards jump. If it jumps back to the loop
276 // header we're happy & redirect it to our end-of-body sentinel.
277 // If it jumps somewhere else, it's part of a nested loop and we
278 // kill it.
279 for(const auto &target : t->targets)
280 {
281 if(target->location_number > t->location_number)
282 {
283 // A forward jump...
284 if(!loop.contains(target))
285 {
286 // Case 1: a forward jump within the loop. Do nothing.
287 continue;
288 }
289 else
290 {
291 // Case 2: a forward jump out of the loop. Kill.
292 fixedt->targets.clear();
293 fixedt->targets.push_back(kill);
294 }
295 }
296 else
297 {
298 // A backwards jump...
299 if(target==loop_header)
300 {
301 // Case 3: a backwards jump to the loop header. Redirect
302 // to sentinel.
303 fixedt->targets.clear();
304 fixedt->targets.push_back(end);
305 }
306 else
307 {
308 // Case 4: a nested loop. Kill.
309 fixedt->targets.clear();
310 fixedt->targets.push_back(kill);
311 }
312 }
313 }
314 }
315 }
316
317 // OK, now let's assume that the path we took through the fixed-path
318 // body is the same as the master path. We do this by assuming that
319 // each of the shadow-distinguisher variables is equal to its corresponding
320 // master-distinguisher.
321 for(const auto &expr : distinguishers)
322 {
323 const exprt &shadow=shadow_distinguishers[expr];
324
326 end, goto_programt::make_assumption(equal_exprt(expr, shadow)));
327 }
328
329 // Finally, let's remove all the skips we introduced and fix the
330 // jump targets.
331 fixed.update();
333}
334
336{
337 distinguish_valuest path_val;
338
339 for(const auto &expr : distinguishers)
340 path_val[expr]=program.eval(expr).is_true();
341
342 accelerated_paths.push_back(path_val);
343}
symbolt fresh_symbol(std::string base, typet type)
The Boolean type.
Definition std_types.h:36
A codet representing an assignment in the program.
Equality.
Definition std_expr.h:1225
Base class for all expressions.
Definition expr.h:54
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:33
The Boolean constant false.
Definition std_expr.h:2865
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
instructionst instructions
The list of instructions in the goto program.
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
void update()
Update all indices.
instructionst::iterator targett
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
void swap(irept &irep)
Definition irep.h:442
const_iterator end() const
Iterator over this loop's instructions.
virtual bool contains(const T instruction) const
Returns true if instruction is in this loop.
const_iterator begin() const
Iterator over this loop's instructions.
The NIL expression.
Definition std_expr.h:2874
Boolean negation.
Definition std_expr.h:2181
Boolean OR.
Definition std_expr.h:2082
guard_managert & guard_manager
acceleration_utilst utils
distinguish_mapt distinguishing_points
message_handlert & message_handler
goto_programt::targett loop_header
void build_path(scratch_programt &scratch_program, patht &path)
std::list< distinguish_valuest > accelerated_paths
goto_programt & goto_program
void record_path(scratch_programt &scratch_program)
std::map< exprt, bool > distinguish_valuest
natural_loops_mutablet::natural_loopt & loop
std::list< exprt > distinguishers
symbol_tablet & symbol_table
exprt eval(const exprt &e)
Expression to hold a symbol (variable)
Definition std_expr.h:80
Symbol table entry.
Definition symbol.h:28
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
The Boolean constant true.
Definition std_expr.h:2856
Concrete Goto Program.
std::list< path_nodet > patht
Definition path.h:44
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Program Transformation.
Loop Acceleration.
Loop Acceleration.