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