cprover
symex_main.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_symex.h"
13 
14 #include <cassert>
15 #include <memory>
16 
17 #include <util/std_expr.h>
18 #include <util/symbol_table.h>
19 #include <util/replace_symbol.h>
20 #include <util/make_unique.h>
21 
22 #include <analyses/dirty.h>
23 
25  statet &state,
27  bool is_backwards_goto)
28 {
29  if(!state.call_stack().empty())
30  {
31  // initialize the loop counter of any loop we are newly entering
32  // upon this transition; we are entering a loop if
33  // 1. the transition from state.source.pc to "to" is not a backwards goto
34  // or
35  // 2. we are arriving from an outer loop
36  statet::framet &frame=state.top();
37  const goto_programt::instructiont &instruction=*to;
38  for(const auto &i_e : instruction.incoming_edges)
39  if(i_e->is_goto() && i_e->is_backwards_goto() &&
40  (!is_backwards_goto ||
41  state.source.pc->location_number>i_e->location_number))
42  frame.loop_iterations[goto_programt::loop_id(*i_e)].count=0;
43  }
44 
45  state.source.pc=to;
46 }
47 
49  const exprt &vcc_expr,
50  const std::string &msg,
51  statet &state)
52 {
53  total_vccs++;
54 
55  exprt expr=vcc_expr;
56 
57  // we are willing to re-write some quantified expressions
58  rewrite_quantifiers(expr, state);
59 
60  // now rename, enables propagation
61  state.rename(expr, ns);
62 
63  // now try simplifier on it
64  do_simplify(expr);
65 
66  if(expr.is_true())
67  return;
68 
69  state.guard.guard_expr(expr);
70 
72  target.assertion(state.guard.as_expr(), expr, msg, state.source);
73 }
74 
75 void goto_symext::symex_assume(statet &state, const exprt &cond)
76 {
77  exprt simplified_cond=cond;
78 
79  do_simplify(simplified_cond);
80 
81  if(simplified_cond.is_true())
82  return;
83 
84  if(state.threads.size()==1)
85  {
86  exprt tmp=simplified_cond;
87  state.guard.guard_expr(tmp);
88  target.assumption(state.guard.as_expr(), tmp, state.source);
89  }
90  // symex_target_equationt::convert_assertions would fail to
91  // consider assumptions of threads that have a thread-id above that
92  // of the thread containing the assertion:
93  // T0 T1
94  // x=0; assume(x==1);
95  // assert(x!=42); x=42;
96  else
97  state.guard.add(simplified_cond);
98 
99  if(state.atomic_section_id!=0 &&
100  state.guard.is_false())
101  symex_atomic_end(state);
102 }
103 
105 {
106  if(expr.id()==ID_forall)
107  {
108  // forall X. P -> P
109  // we keep the quantified variable unique by means of L2 renaming
110  PRECONDITION(expr.operands().size()==2);
111  PRECONDITION(expr.op0().id()==ID_symbol);
112  symbol_exprt tmp0=
113  to_symbol_expr(to_ssa_expr(expr.op0()).get_original_expr());
114  symex_decl(state, tmp0);
115  exprt tmp=expr.op1();
116  expr.swap(tmp);
117  }
118 }
119 
121  statet &state,
122  const get_goto_functiont &get_goto_function,
124  const goto_programt::const_targett limit)
125 {
126  PRECONDITION(!state.threads.empty());
127  PRECONDITION(!state.call_stack().empty());
128  state.source=symex_targett::sourcet(pc);
129  state.top().end_of_function=limit;
130  state.top().calling_location.pc=state.top().end_of_function;
131  state.symex_target=&target;
132 
133  INVARIANT(
134  !pc->function.empty(), "all symexed instructions should have a function");
136  pc->function, get_goto_function(pc->function));
137 
138  symex_transition(state, state.source.pc);
139 }
140 
142  statet &state, const get_goto_functiont &get_goto_function)
143 {
144  symex_step(get_goto_function, state);
146  return;
147 
148  // is there another thread to execute?
149  if(state.call_stack().empty() &&
150  state.source.thread_nr+1<state.threads.size())
151  {
152  unsigned t=state.source.thread_nr+1;
153 #if 0
154  std::cout << "********* Now executing thread " << t << '\n';
155 #endif
156  state.switch_to_thread(t);
157  symex_transition(state, state.source.pc);
158  }
159 }
160 
162  const goto_functionst &goto_functions)
163 {
164  return [&goto_functions](
165  const irep_idt &key) -> const goto_functionst::goto_functiont & {
166  return goto_functions.function_map.at(key);
167  };
168 }
169 
171  statet &state,
172  const goto_functionst &goto_functions,
173  symbol_tablet &new_symbol_table)
174 {
176  state,
177  get_function_from_goto_functions(goto_functions),
178  new_symbol_table);
179 }
180 
182  statet &state,
183  const get_goto_functiont &get_goto_function,
184  symbol_tablet &new_symbol_table)
185 {
186  // We'll be using ns during symbolic execution and it needs to know
187  // about the names minted in `state`, so make it point both to
188  // `state`'s symbol table and the symbol table of the original
189  // goto-program.
191 
192  PRECONDITION(state.top().end_of_function->is_end_function());
193 
194  symex_threaded_step(state, get_goto_function);
196  return;
197  while(!state.call_stack().empty())
198  {
199  state.has_saved_jump_target = false;
200  state.has_saved_next_instruction = false;
201  symex_threaded_step(state, get_goto_function);
203  return;
204  }
205 
206  // Clients may need to construct a namespace with both the names in
207  // the original goto-program and the names generated during symbolic
208  // execution, so return the names generated through symbolic execution
209  // through `new_symbol_table`.
210  new_symbol_table = state.symbol_table;
211  // reset the namespace back to a sane state as state.symbol_table might go out
212  // of scope
214 }
215 
217  const get_goto_functiont &get_goto_function,
218  const statet &saved_state,
219  symex_target_equationt *const saved_equation,
220  symbol_tablet &new_symbol_table)
221 {
222  // saved_state contains a pointer to a symex_target_equationt that is
223  // almost certainly stale. This is because equations are owned by bmcts,
224  // and we construct a new bmct for every path that we execute. We're on a
225  // new path now, so the old bmct and the equation that it owned have now
226  // been deallocated. So, construct a new state from the old one, and make
227  // its equation member point to the (valid) equation passed as an argument.
228  statet state(saved_state, saved_equation);
229 
230  // Do NOT do the same initialization that `symex_with_state` does for a
231  // fresh state, as that would clobber the saved state's program counter
233  state,
234  get_goto_function,
235  new_symbol_table);
236 }
237 
239  statet &state,
240  const goto_functionst &goto_functions,
241  const goto_programt::const_targett first,
242  const goto_programt::const_targett limit)
243 {
245  state, get_function_from_goto_functions(goto_functions), first, limit);
246 }
247 
249  statet &state,
250  const get_goto_functiont &get_goto_function,
251  const goto_programt::const_targett first,
252  const goto_programt::const_targett limit)
253 {
254  initialize_entry_point(state, get_goto_function, first, limit);
256  while(state.source.pc->function!=limit->function || state.source.pc!=limit)
257  symex_threaded_step(state, get_goto_function);
258 }
259 
261  const goto_functionst &goto_functions,
262  symbol_tablet &new_symbol_table)
263 {
265  get_function_from_goto_functions(goto_functions), new_symbol_table);
266 }
267 
269  const get_goto_functiont &get_goto_function,
270  symbol_tablet &new_symbol_table)
271 {
272  const goto_functionst::goto_functiont *start_function;
273  try
274  {
275  start_function = &get_goto_function(goto_functionst::entry_point());
276  }
277  catch(const std::out_of_range &error)
278  {
279  throw "the program has no entry point";
280  }
281 
282  statet state;
283 
285  state,
286  get_goto_function,
287  start_function->body.instructions.begin(),
288  prev(start_function->body.instructions.end()));
289 
291  state, get_goto_function, new_symbol_table);
292 }
293 
296  const get_goto_functiont &get_goto_function,
297  statet &state)
298 {
299  #if 0
300  std::cout << "\ninstruction type is " << state.source.pc->type << '\n';
301  std::cout << "Location: " << state.source.pc->source_location << '\n';
302  std::cout << "Guard: " << format(state.guard.as_expr()) << '\n';
303  std::cout << "Code: " << format(state.source.pc->code) << '\n';
304  #endif
305 
306  PRECONDITION(!state.threads.empty());
307  PRECONDITION(!state.call_stack().empty());
308 
309  const goto_programt::instructiont &instruction=*state.source.pc;
310 
312  merge_gotos(state);
313 
314  // depth exceeded?
315  if(max_depth != 0 && state.depth > max_depth)
316  state.guard.add(false_exprt());
317  state.depth++;
318 
319  // actually do instruction
320  switch(instruction.type)
321  {
322  case SKIP:
323  if(!state.guard.is_false())
324  target.location(state.guard.as_expr(), state.source);
325  symex_transition(state);
326  break;
327 
328  case END_FUNCTION:
329  // do even if state.guard.is_false() to clear out frame created
330  // in symex_start_thread
331  symex_end_of_function(state);
332  symex_transition(state);
333  break;
334 
335  case LOCATION:
336  if(!state.guard.is_false())
337  target.location(state.guard.as_expr(), state.source);
338  symex_transition(state);
339  break;
340 
341  case GOTO:
342  symex_goto(state);
343  break;
344 
345  case ASSUME:
346  if(!state.guard.is_false())
347  {
348  exprt tmp=instruction.guard;
349  clean_expr(tmp, state, false);
350  state.rename(tmp, ns);
351  symex_assume(state, tmp);
352  }
353 
354  symex_transition(state);
355  break;
356 
357  case ASSERT:
358  if(!state.guard.is_false())
359  {
360  std::string msg=id2string(state.source.pc->source_location.get_comment());
361  if(msg=="")
362  msg="assertion";
363  exprt tmp(instruction.guard);
364  clean_expr(tmp, state, false);
365  vcc(tmp, msg, state);
366  }
367 
368  symex_transition(state);
369  break;
370 
371  case RETURN:
372  if(!state.guard.is_false())
373  return_assignment(state);
374 
375  symex_transition(state);
376  break;
377 
378  case ASSIGN:
379  if(!state.guard.is_false())
380  symex_assign(state, to_code_assign(instruction.code));
381 
382  symex_transition(state);
383  break;
384 
385  case FUNCTION_CALL:
386  if(!state.guard.is_false())
387  {
388  code_function_callt deref_code=
389  to_code_function_call(instruction.code);
390 
391  if(deref_code.lhs().is_not_nil())
392  clean_expr(deref_code.lhs(), state, true);
393 
394  clean_expr(deref_code.function(), state, false);
395 
396  Forall_expr(it, deref_code.arguments())
397  clean_expr(*it, state, false);
398 
399  symex_function_call(get_goto_function, state, deref_code);
400  }
401  else
402  symex_transition(state);
403  break;
404 
405  case OTHER:
406  if(!state.guard.is_false())
407  symex_other(state);
408 
409  symex_transition(state);
410  break;
411 
412  case DECL:
413  if(!state.guard.is_false())
414  symex_decl(state);
415 
416  symex_transition(state);
417  break;
418 
419  case DEAD:
420  symex_dead(state);
421  symex_transition(state);
422  break;
423 
424  case START_THREAD:
425  symex_start_thread(state);
426  symex_transition(state);
427  break;
428 
429  case END_THREAD:
430  // behaves like assume(0);
431  if(!state.guard.is_false())
432  state.guard.add(false_exprt());
433  symex_transition(state);
434  break;
435 
436  case ATOMIC_BEGIN:
437  symex_atomic_begin(state);
438  symex_transition(state);
439  break;
440 
441  case ATOMIC_END:
442  symex_atomic_end(state);
443  symex_transition(state);
444  break;
445 
446  case CATCH:
447  symex_catch(state);
448  symex_transition(state);
449  break;
450 
451  case THROW:
452  symex_throw(state);
453  symex_transition(state);
454  break;
455 
456  case NO_INSTRUCTION_TYPE:
457  throw "symex got NO_INSTRUCTION";
458 
459  default:
460  throw "symex got unexpected instruction";
461  }
462 }
exprt as_expr() const
Definition: guard.h:43
virtual void symex_instruction_range(statet &, const goto_functionst &, goto_programt::const_targett first, goto_programt::const_targett limit)
Symexes from the first instruction and the given state, terminating as soon as the last instruction i...
Definition: symex_main.cpp:238
void return_assignment(statet &)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
bool is_not_nil() const
Definition: irep.h:103
goto_programt::const_targett pc
Definition: symex_target.h:32
void guard_expr(exprt &dest) const
Definition: guard.cpp:19
virtual void symex_goto(statet &)
Definition: symex_goto.cpp:22
std::set< targett > incoming_edges
Definition: goto_program.h:226
exprt & op0()
Definition: expr.h:72
Variables whose address is taken.
virtual void symex_transition(statet &, goto_programt::const_targett to, bool is_backwards_goto=false)
Definition: symex_main.cpp:24
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)
record an assumption
bool is_false() const
Definition: expr.cpp:131
symex_target_equationt * symex_target
bool is_true() const
Definition: expr.cpp:124
function_mapt function_map
const unsigned max_depth
Definition: goto_symex.h:204
loop_iterationst loop_iterations
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
Definition: goto_symex.h:84
virtual void do_simplify(exprt &)
Definition: goto_symex.cpp:19
void switch_to_thread(unsigned t)
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
virtual void symex_step(const get_goto_functiont &, statet &)
do just one step
Definition: symex_main.cpp:295
virtual void symex_end_of_function(statet &)
do function call by inlining
unsigned depth
distance from entry
void symex_catch(statet &)
Definition: symex_catch.cpp:14
virtual void symex_atomic_end(statet &)
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
void symex_throw(statet &)
Definition: symex_throw.cpp:14
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:237
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:239
const irep_idt & id() const
Definition: irep.h:189
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:154
virtual void symex_atomic_begin(statet &)
void initialize_entry_point(statet &state, const get_goto_functiont &get_goto_function, goto_programt::const_targett pc, goto_programt::const_targett limit)
Initialise the symbolic execution and the given state with pc as entry point.
Definition: symex_main.cpp:120
argumentst & arguments()
Definition: std_code.h:860
virtual void symex_from_entry_point_of(const goto_functionst &goto_functions, symbol_tablet &new_symbol_table)
symex entire program starting from entry point
Definition: symex_main.cpp:260
virtual void symex_other(statet &)
Definition: symex_other.cpp:76
#define Forall_expr(it, expr)
Definition: expr.h:32
static goto_symext::get_goto_functiont get_function_from_goto_functions(const goto_functionst &goto_functions)
Definition: symex_main.cpp:161
virtual void symex_with_state(statet &, const goto_functionst &, symbol_tablet &)
symex entire program starting from entry point
Definition: symex_main.cpp:170
const symbol_tablet & outer_symbol_table
The symbol table associated with the goto-program that we&#39;re executing.
Definition: goto_symex.h:228
Symbolic Execution.
virtual void resume_symex_from_saved_state(const get_goto_functiont &get_goto_function, const statet &saved_state, symex_target_equationt *const saved_equation, symbol_tablet &new_symbol_table)
Performs symbolic execution using a state and equation that have already been used to symex part of t...
Definition: symex_main.cpp:216
virtual void symex_assume(statet &, const exprt &cond)
Definition: symex_main.cpp:75
virtual void symex_decl(statet &)
Definition: symex_decl.cpp:22
API to expression classes.
symex_target_equationt & target
Definition: goto_symex.h:238
exprt & op1()
Definition: expr.h:75
The symbol table.
Definition: symbol_table.h:19
instructionst::const_iterator const_targett
Definition: goto_program.h:398
TO_BE_DOCUMENTED.
Definition: namespace.h:74
::goto_functiont goto_functiont
static irep_idt loop_id(const instructiont &instruction)
Human-readable loop name.
Definition: goto_program.h:583
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
unsigned remaining_vccs
Definition: goto_symex.h:213
A function call.
Definition: std_code.h:828
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
incremental_dirtyt dirty
void populate_dirty_for_function(const irep_idt &id, const goto_functionst::goto_functiont &function)
Analyse the given function with dirtyt if it hasn&#39;t been seen before.
Definition: dirty.cpp:80
bool has_saved_next_instruction
This state is saved, with the PC pointing to the next instruction of a GOTO.
Author: Diffblue Ltd.
The boolean constant false.
Definition: std_expr.h:4499
void rewrite_quantifiers(exprt &, statet &)
Definition: symex_main.cpp:104
void symex_assign(statet &, const code_assignt &)
virtual void vcc(const exprt &, const std::string &msg, statet &)
Definition: symex_main.cpp:48
void symex_threaded_step(statet &, const get_goto_functiont &)
Invokes symex_step and verifies whether additional threads can be executed.
Definition: symex_main.cpp:141
virtual void assertion(const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)
record an assertion
static irep_idt entry_point()
void clean_expr(exprt &, statet &, bool write)
bool should_pause_symex
Have states been pushed onto the workqueue?
Definition: goto_symex.h:175
exprt & function()
Definition: std_code.h:848
Base class for all expressions.
Definition: expr.h:42
call_stackt & call_stack()
virtual void symex_dead(statet &)
Definition: symex_dead.cpp:20
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc...
virtual void location(const exprt &guard, const sourcet &source)
just record a location
virtual void symex_start_thread(statet &)
bool has_saved_jump_target
This state is saved, with the PC pointing to the target of a GOTO.
void merge_gotos(statet &)
Definition: symex_goto.cpp:319
void swap(irept &irep)
Definition: irep.h:231
symex_targett::sourcet calling_location
Expression to hold a symbol (variable)
Definition: std_expr.h:90
virtual void symex_function_call(const get_goto_functiont &, statet &, const code_function_callt &)
operandst & operands()
Definition: expr.h:66
const bool doing_path_exploration
Definition: goto_symex.h:205
unsigned total_vccs
Definition: goto_symex.h:213
goto_programt::const_targett end_of_function
void add(const exprt &expr)
Definition: guard.cpp:64
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:879
symex_targett::sourcet source
static format_containert< T > format(const T &o)
Definition: format.h:35