cprover
path_search.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Path-based Symbolic Execution
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "path_search.h"
13 
14 #include <util/simplify_expr.h>
15 #include <util/time_stopping.h>
16 
18 #include <solvers/sat/satcheck.h>
19 
20 #include <path-symex/path_symex.h>
22 
24  const goto_functionst &goto_functions)
25 {
26  locst locs(ns);
27  var_mapt var_map(ns);
28 
29  locs.build(goto_functions);
30 
31  // this is the container for the history-forest
32  path_symex_historyt history;
33 
34  queue.push_back(initial_state(var_map, locs, history));
35 
36  // set up the statistics
45  number_of_locs=locs.size();
46 
47  // stop the time
49 
50  initialize_property_map(goto_functions);
51 
52  while(!queue.empty())
53  {
55 
56  // Pick a state from the queue,
57  // according to some heuristic.
58  // The state moves to the head of the queue.
59  pick_state();
60 
61  // move into temporary queue
62  queuet tmp_queue;
63  tmp_queue.splice(
64  tmp_queue.begin(), queue, queue.begin(), ++queue.begin());
65 
66  try
67  {
68  statet &state=tmp_queue.front();
69 
70  // record we have seen it
71  loc_data[state.pc().loc_number].visited=true;
72 
73  debug() << "Loc: #" << state.pc().loc_number
74  << ", queue: " << queue.size()
75  << ", depth: " << state.get_depth();
76  for(const auto &s : queue)
77  debug() << ' ' << s.get_depth();
78 
79  debug() << eom;
80 
81  if(drop_state(state))
82  {
85  continue;
86  }
87 
88  if(!state.is_executable())
89  {
91  continue;
92  }
93 
95  state.last_was_branch() &&
96  !is_feasible(state))
97  {
100  continue;
101  }
102 
103  if(number_of_steps%1000==0)
104  {
105  time_periodt running_time=current_time()-start_time;
106  status() << "Queue " << queue.size()
107  << " thread " << state.get_current_thread()+1
108  << '/' << state.threads.size()
109  << " PC " << state.pc()
110  << " [" << number_of_steps << " steps, "
111  << running_time << "s]" << messaget::eom;
112  }
113 
114  // an error, possibly?
115  if(state.get_instruction()->is_assert())
116  {
117  if(show_vcc)
118  do_show_vcc(state);
119  else
120  {
121  check_assertion(state);
122 
123  // all assertions failed?
125  break;
126  }
127  }
128 
129  // execute
130  path_symex(state, tmp_queue);
131 
132  // put at head of main queue
133  queue.splice(queue.begin(), tmp_queue);
134  }
135  catch(const std::string &e)
136  {
137  error() << e << eom;
139  }
140  catch(const char *e)
141  {
142  error() << e << eom;
144  }
145  catch(int)
146  {
148  }
149  }
150 
152 
154 }
155 
157 {
158  std::size_t number_of_visited_locations=0;
159  for(const auto &l : loc_data)
160  if(l.visited)
161  number_of_visited_locations++;
162 
163  #if 0
164  for(unsigned l=0; l<loc_data.size(); l++)
165  if(!loc_data[l].visited)
166  status() << "NV: " << l << eom;
167  #endif
168 
169  // report a bit
170  status() << "Number of visited locations: "
171  << number_of_visited_locations << " (out of "
172  << number_of_locs << ')' << messaget::eom;
173 
174  status() << "Number of dropped states: "
176 
177  status() << "Number of paths: "
179 
180  status() << "Number of infeasible paths: "
182 
183  status() << "Generated " << number_of_VCCs << " VCC(s), "
185  << " remaining after simplification"
186  << messaget::eom;
187 
188  time_periodt total_time=current_time()-start_time;
189  status() << "Runtime: " << total_time << "s total, "
190  << sat_time << "s SAT" << messaget::eom;
191 }
192 
194 {
195  switch(search_heuristic)
196  {
198  // Picking the first one (most recently added) is a DFS.
199  return;
200 
202  // Picking the last one is a BFS.
203  if(queue.size()>=2)
204  // move last to first position
205  queue.splice(queue.begin(), queue, --queue.end(), queue.end());
206  return;
207 
209  return;
210  }
211 }
212 
214 {
215  // keep statistics
216  number_of_VCCs++;
217 
218  const goto_programt::instructiont &instruction=
219  *state.get_instruction();
220 
221  mstreamt &out=result();
222 
223  if(instruction.source_location.is_not_nil())
224  out << instruction.source_location << '\n';
225 
226  if(instruction.source_location.get_comment()!="")
227  out << instruction.source_location.get_comment() << '\n';
228 
229  unsigned count=1;
230 
231  std::vector<path_symex_step_reft> steps;
232  state.history.build_history(steps);
233 
234  for(const auto &step_ref : steps)
235  {
236  if(step_ref->guard.is_not_nil())
237  {
238  std::string string_value=from_expr(ns, "", step_ref->guard);
239  out << "{-" << count << "} " << string_value << '\n';
240  count++;
241  }
242 
243  if(step_ref->ssa_rhs.is_not_nil())
244  {
245  equal_exprt equality(step_ref->ssa_lhs, step_ref->ssa_rhs);
246  std::string string_value=from_expr(ns, "", equality);
247  out << "{-" << count << "} " << string_value << '\n';
248  count++;
249  }
250  }
251 
252  out << "|--------------------------" << '\n';
253 
254  exprt assertion=state.read(instruction.guard);
255 
256  out << "{" << 1 << "} "
257  << from_expr(ns, "", assertion) << '\n';
258 
259  if(!assertion.is_true())
261 
262  out << eom;
263 }
264 
267 {
269 
270  const source_locationt &source_location=pc->source_location;
271 
272  if(!source_location.is_nil() &&
273  last_source_location!=source_location)
274  {
275  debug() << "SYMEX at file " << source_location.get_file()
276  << " line " << source_location.get_line()
277  << " function " << source_location.get_function()
278  << eom;
279 
280  last_source_location=source_location;
281  }
282 
283  // depth limit
284  if(state.get_depth()>=depth_limit)
285  return true;
286 
287  // context bound
289  return true;
290 
291  // branch bound
292  if(state.get_no_branches()>=branch_bound)
293  return true;
294 
295  // unwinding limit -- loops
296  if(unwind_limit!=std::numeric_limits<unsigned>::max() &&
297  pc->is_backwards_goto())
298  {
299  bool stop=false;
300 
301  for(const auto &loop_info : state.unwinding_map)
302  if(loop_info.second>=unwind_limit)
303  {
304  stop=true;
305  break;
306  }
307 
308  const irep_idt id=goto_programt::loop_id(pc);
309  path_symex_statet::unwinding_mapt::const_iterator entry=
310  state.unwinding_map.find(state.pc());
311  debug() << (stop?"Not unwinding":"Unwinding")
312  << " loop " << id << " iteration "
313  << (entry==state.unwinding_map.end()?-1:entry->second)
314  << " (" << unwind_limit << " max)"
315  << " " << source_location
316  << " thread " << state.get_current_thread() << eom;
317 
318  if(stop)
319  return true;
320  }
321 
322  // unwinding limit -- recursion
323  if(unwind_limit!=std::numeric_limits<unsigned>::max() &&
324  pc->is_function_call())
325  {
326  bool stop=false;
327 
328  for(const auto &rec_info : state.recursion_map)
329  if(rec_info.second>=unwind_limit)
330  {
331  stop=true;
332  break;
333  }
334 
335  exprt function=to_code_function_call(pc->code).function();
336  const irep_idt id=function.get(ID_identifier); // could be nil
337  path_symex_statet::recursion_mapt::const_iterator entry=
338  state.recursion_map.find(id);
339  if(entry!=state.recursion_map.end())
340  debug() << (stop?"Not unwinding":"Unwinding")
341  << " recursion " << id << " iteration "
342  << entry->second
343  << " (" << unwind_limit << " max)"
344  << " " << source_location
345  << " thread " << state.get_current_thread() << eom;
346 
347  if(stop)
348  return true;
349  }
350 
351  // search time limit (--max-search-time)
352  if(time_limit!=std::numeric_limits<unsigned>::max() &&
353  current_time().get_t()>start_time.get_t()+time_limit*1000)
354  return true;
355 
356  if(pc->is_assume() &&
357  simplify_expr(pc->guard, ns).is_false())
358  {
359  debug() << "aborting path on assume(false) at "
360  << pc->source_location
361  << " thread " << state.get_current_thread();
362 
363  const irep_idt &c=pc->source_location.get_comment();
364  if(!c.empty())
365  debug() << ": " << c;
366 
367  debug() << eom;
368 
369  return true;
370  }
371 
372  return false;
373 }
374 
376 {
377  // keep statistics
378  number_of_VCCs++;
379 
380  const goto_programt::instructiont &instruction=
381  *state.get_instruction();
382 
383  irep_idt property_name=instruction.source_location.get_property_id();
384  property_entryt &property_entry=property_map[property_name];
385 
386  if(property_entry.status==FAILURE)
387  return; // already failed
388  else if(property_entry.status==NOT_REACHED)
389  property_entry.status=SUCCESS; // well, for now!
390 
391  // the assertion in SSA
392  exprt assertion=
393  state.read(instruction.guard);
394 
395  if(assertion.is_true())
396  return; // no error, trivially
397 
398  // keep statistics
400 
401  status() << "Checking property " << property_name << eom;
402 
403  // take the time
404  absolute_timet sat_start_time=current_time();
405 
406  satcheckt satcheck;
407  bv_pointerst bv_pointers(ns, satcheck);
408 
411 
412  if(!state.check_assertion(bv_pointers))
413  {
414  build_goto_trace(state, bv_pointers, property_entry.error_trace);
415  property_entry.status=FAILURE;
417  }
418 
419  sat_time+=current_time()-sat_start_time;
420 }
421 
423 {
424  status() << "Feasibility check" << eom;
425 
426  // take the time
427  absolute_timet sat_start_time=current_time();
428 
429  satcheckt satcheck;
430  bv_pointerst bv_pointers(ns, satcheck);
431 
434 
435  bool result=state.is_feasible(bv_pointers);
436 
437  sat_time+=current_time()-sat_start_time;
438 
439  return result;
440 }
441 
443  const goto_functionst &goto_functions)
444 {
445  forall_goto_functions(it, goto_functions)
446  if(!it->second.is_inlined())
447  {
448  const goto_programt &goto_program=it->second.body;
449 
450  forall_goto_program_instructions(i_it, goto_program)
451  {
452  if(!i_it->is_assert())
453  continue;
454 
455  const source_locationt &source_location=i_it->source_location;
456 
457  irep_idt property_name=source_location.get_property_id();
458 
459  property_entryt &property_entry=property_map[property_name];
460  property_entry.status=NOT_REACHED;
461  property_entry.description=source_location.get_comment();
462  property_entry.source_location=source_location;
463  }
464  }
465 }
mstreamt & result()
Definition: message.h:233
std::size_t number_of_infeasible_paths
Definition: path_search.h:76
static irep_idt loop_id(const_targett target)
Human-readable loop name.
bool is_nil() const
Definition: irep.h:103
void build_history(std::vector< path_symex_step_reft > &dest) const
property_mapt property_map
Definition: path_search.h:103
unsigned context_bound
Definition: path_search.h:138
exprt simplify_expr(const exprt &src, const namespacet &ns)
std::size_t number_of_locs
Definition: path_search.h:80
mstreamt & status()
Definition: message.h:238
unsigned loc_number
Definition: loc_ref.h:20
const irep_idt & get_function() const
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
virtual resultt operator()(const goto_functionst &goto_functions)
Definition: path_search.cpp:23
bool is_false() const
Definition: expr.cpp:140
source_locationt source_location
Definition: path_search.h:91
std::size_t number_of_dropped_states
Definition: path_search.h:72
bool is_true() const
Definition: expr.cpp:133
std::size_t number_of_paths
Definition: path_search.h:73
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
void initialize_property_map(const goto_functionst &goto_functions)
unsigned time_limit
Definition: path_search.h:141
void report_statistics()
unwinding_mapt unwinding_map
std::size_t number_of_feasible_paths
Definition: path_search.h:75
equality
Definition: std_expr.h:1082
bool last_was_branch() const
bool drop_state(const statet &state)
decide whether to drop a state
instructionst::const_iterator const_targett
void pick_state()
const irep_idt & get_line() const
const namespacet & ns
exprt read(const exprt &src)
time_periodt sat_time
Definition: path_search.h:82
void path_symex(path_symex_statet &state, std::list< path_symex_statet > &further_states)
source_locationt last_source_location
Definition: path_search.h:145
unsigned depth_limit
Definition: path_search.h:137
source_locationt source_location
Definition: message.h:175
Build Goto Trace from Path Symex History.
std::size_t number_of_steps
Definition: path_search.h:74
bool is_feasible(class decision_proceduret &) const
unsigned long long get_t() const
Definition: time_stopping.h:31
Time Stopping.
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:122
bool is_feasible(statet &state)
bool eager_infeasibility
Definition: path_search.h:69
unsigned get_current_thread() const
unsigned unwind_limit
Definition: path_search.h:140
unsigned get_no_thread_interleavings() const
std::list< statet > queuet
Definition: path_search.h:110
std::size_t number_of_VCCs_after_simplification
Definition: path_search.h:78
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
std::size_t number_of_failed_properties
Definition: path_search.h:79
mstreamt & debug()
Definition: message.h:253
bool check_assertion(class decision_proceduret &)
const irep_idt & get_file() const
message_handlert & get_message_handler()
Definition: message.h:127
recursion_mapt recursion_map
absolute_timet current_time()
goto_programt::const_targett get_instruction() const
exprt & function()
Definition: std_code.h:677
Definition: locs.h:39
void do_show_vcc(statet &state)
Base class for all expressions.
Definition: expr.h:46
std::size_t size() const
Definition: locs.h:86
bool is_executable() const
queuet queue
Definition: path_search.h:111
Path-based Symbolic Execution.
unsigned branch_bound
Definition: path_search.h:139
unsigned get_no_branches() const
Concrete Symbolic Transformer.
absolute_timet start_time
Definition: path_search.h:81
enum path_searcht::search_heuristict search_heuristic
mstreamt & error()
Definition: message.h:223
const irep_idt & get_comment() const
void check_assertion(statet &state)
path_symex_statet initial_state(var_mapt &var_map, const locst &locs, path_symex_historyt &path_symex_history)
#define forall_goto_functions(it, functions)
const irep_idt & get_property_id() const
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
loc_reft pc() const
bool empty() const
Definition: dstring.h:61
path_symex_step_reft history
expanding_vectort< loc_datat > loc_data
Definition: path_search.h:122
std::size_t number_of_VCCs
Definition: path_search.h:77
unsigned get_depth() const
void build(const goto_functionst &goto_functions)
Definition: locs.cpp:20
void build_goto_trace(const symex_target_equationt &target, symex_target_equationt::SSA_stepst::const_iterator end_step, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace)
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700