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