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");
135 
136  const goto_functiont &entry_point_function = get_goto_function(pc->function);
137 
138  auto emplace_safe_pointers_result =
139  safe_pointers.emplace(pc->function, local_safe_pointerst{ns});
140  if(emplace_safe_pointers_result.second)
141  emplace_safe_pointers_result.first->second(entry_point_function.body);
142 
143  state.dirty.populate_dirty_for_function(pc->function, entry_point_function);
144 
145  symex_transition(state, state.source.pc);
146 }
147 
149  statet &state, const get_goto_functiont &get_goto_function)
150 {
151  symex_step(get_goto_function, state);
153  return;
154 
155  // is there another thread to execute?
156  if(state.call_stack().empty() &&
157  state.source.thread_nr+1<state.threads.size())
158  {
159  unsigned t=state.source.thread_nr+1;
160 #if 0
161  std::cout << "********* Now executing thread " << t << '\n';
162 #endif
163  state.switch_to_thread(t);
164  symex_transition(state, state.source.pc);
165  }
166 }
167 
169  const goto_functionst &goto_functions)
170 {
171  return [&goto_functions](
172  const irep_idt &key) -> const goto_functionst::goto_functiont & {
173  return goto_functions.function_map.at(key);
174  };
175 }
176 
178  statet &state,
179  const goto_functionst &goto_functions,
180  symbol_tablet &new_symbol_table)
181 {
183  state,
184  get_function_from_goto_functions(goto_functions),
185  new_symbol_table);
186 }
187 
189  statet &state,
190  const get_goto_functiont &get_goto_function,
191  symbol_tablet &new_symbol_table)
192 {
193  // We'll be using ns during symbolic execution and it needs to know
194  // about the names minted in `state`, so make it point both to
195  // `state`'s symbol table and the symbol table of the original
196  // goto-program.
198 
199  PRECONDITION(state.top().end_of_function->is_end_function());
200 
201  symex_threaded_step(state, get_goto_function);
203  return;
204  while(!state.call_stack().empty())
205  {
206  state.has_saved_jump_target = false;
207  state.has_saved_next_instruction = false;
208  symex_threaded_step(state, get_goto_function);
210  return;
211  }
212 
213  // Clients may need to construct a namespace with both the names in
214  // the original goto-program and the names generated during symbolic
215  // execution, so return the names generated through symbolic execution
216  // through `new_symbol_table`.
217  new_symbol_table = state.symbol_table;
218  // reset the namespace back to a sane state as state.symbol_table might go out
219  // of scope
221 }
222 
224  const get_goto_functiont &get_goto_function,
225  const statet &saved_state,
226  symex_target_equationt *const saved_equation,
227  symbol_tablet &new_symbol_table)
228 {
229  // saved_state contains a pointer to a symex_target_equationt that is
230  // almost certainly stale. This is because equations are owned by bmcts,
231  // and we construct a new bmct for every path that we execute. We're on a
232  // new path now, so the old bmct and the equation that it owned have now
233  // been deallocated. So, construct a new state from the old one, and make
234  // its equation member point to the (valid) equation passed as an argument.
235  statet state(saved_state, saved_equation);
236 
237  // Do NOT do the same initialization that `symex_with_state` does for a
238  // fresh state, as that would clobber the saved state's program counter
240  state,
241  get_goto_function,
242  new_symbol_table);
243 }
244 
246  statet &state,
247  const goto_functionst &goto_functions,
248  const goto_programt::const_targett first,
249  const goto_programt::const_targett limit)
250 {
252  state, get_function_from_goto_functions(goto_functions), first, limit);
253 }
254 
256  statet &state,
257  const get_goto_functiont &get_goto_function,
258  const goto_programt::const_targett first,
259  const goto_programt::const_targett limit)
260 {
261  initialize_entry_point(state, get_goto_function, first, limit);
263  while(state.source.pc->function!=limit->function || state.source.pc!=limit)
264  symex_threaded_step(state, get_goto_function);
265 }
266 
268  const goto_functionst &goto_functions,
269  symbol_tablet &new_symbol_table)
270 {
272  get_function_from_goto_functions(goto_functions), new_symbol_table);
273 }
274 
276  const get_goto_functiont &get_goto_function,
277  symbol_tablet &new_symbol_table)
278 {
279  const goto_functionst::goto_functiont *start_function;
280  try
281  {
282  start_function = &get_goto_function(goto_functionst::entry_point());
283  }
284  catch(const std::out_of_range &)
285  {
286  throw "the program has no entry point";
287  }
288 
289  statet state;
290 
292  state,
293  get_goto_function,
294  start_function->body.instructions.begin(),
295  prev(start_function->body.instructions.end()));
296 
298  state, get_goto_function, new_symbol_table);
299 }
300 
303  const get_goto_functiont &get_goto_function,
304  statet &state)
305 {
306  #if 0
307  std::cout << "\ninstruction type is " << state.source.pc->type << '\n';
308  std::cout << "Location: " << state.source.pc->source_location << '\n';
309  std::cout << "Guard: " << format(state.guard.as_expr()) << '\n';
310  std::cout << "Code: " << format(state.source.pc->code) << '\n';
311  #endif
312 
313  PRECONDITION(!state.threads.empty());
314  PRECONDITION(!state.call_stack().empty());
315 
316  const goto_programt::instructiont &instruction=*state.source.pc;
317 
319  merge_gotos(state);
320 
321  // depth exceeded?
322  if(max_depth != 0 && state.depth > max_depth)
323  state.guard.add(false_exprt());
324  state.depth++;
325 
326  // actually do instruction
327  switch(instruction.type)
328  {
329  case SKIP:
330  if(!state.guard.is_false())
331  target.location(state.guard.as_expr(), state.source);
332  symex_transition(state);
333  break;
334 
335  case END_FUNCTION:
336  // do even if state.guard.is_false() to clear out frame created
337  // in symex_start_thread
338  symex_end_of_function(state);
339  symex_transition(state);
340  break;
341 
342  case LOCATION:
343  if(!state.guard.is_false())
344  target.location(state.guard.as_expr(), state.source);
345  symex_transition(state);
346  break;
347 
348  case GOTO:
349  symex_goto(state);
350  break;
351 
352  case ASSUME:
353  if(!state.guard.is_false())
354  {
355  exprt tmp=instruction.guard;
356  clean_expr(tmp, state, false);
357  state.rename(tmp, ns);
358  symex_assume(state, tmp);
359  }
360 
361  symex_transition(state);
362  break;
363 
364  case ASSERT:
365  if(!state.guard.is_false())
366  {
367  std::string msg=id2string(state.source.pc->source_location.get_comment());
368  if(msg=="")
369  msg="assertion";
370  exprt tmp(instruction.guard);
371  clean_expr(tmp, state, false);
372  vcc(tmp, msg, state);
373  }
374 
375  symex_transition(state);
376  break;
377 
378  case RETURN:
379  if(!state.guard.is_false())
380  return_assignment(state);
381 
382  symex_transition(state);
383  break;
384 
385  case ASSIGN:
386  if(!state.guard.is_false())
387  symex_assign(state, to_code_assign(instruction.code));
388 
389  symex_transition(state);
390  break;
391 
392  case FUNCTION_CALL:
393  if(!state.guard.is_false())
394  {
395  code_function_callt deref_code=
396  to_code_function_call(instruction.code);
397 
398  if(deref_code.lhs().is_not_nil())
399  clean_expr(deref_code.lhs(), state, true);
400 
401  clean_expr(deref_code.function(), state, false);
402 
403  Forall_expr(it, deref_code.arguments())
404  clean_expr(*it, state, false);
405 
406  symex_function_call(get_goto_function, state, deref_code);
407  }
408  else
409  symex_transition(state);
410  break;
411 
412  case OTHER:
413  if(!state.guard.is_false())
414  symex_other(state);
415 
416  symex_transition(state);
417  break;
418 
419  case DECL:
420  if(!state.guard.is_false())
421  symex_decl(state);
422 
423  symex_transition(state);
424  break;
425 
426  case DEAD:
427  symex_dead(state);
428  symex_transition(state);
429  break;
430 
431  case START_THREAD:
432  symex_start_thread(state);
433  symex_transition(state);
434  break;
435 
436  case END_THREAD:
437  // behaves like assume(0);
438  if(!state.guard.is_false())
439  state.guard.add(false_exprt());
440  symex_transition(state);
441  break;
442 
443  case ATOMIC_BEGIN:
444  symex_atomic_begin(state);
445  symex_transition(state);
446  break;
447 
448  case ATOMIC_END:
449  symex_atomic_end(state);
450  symex_transition(state);
451  break;
452 
453  case CATCH:
454  symex_catch(state);
455  symex_transition(state);
456  break;
457 
458  case THROW:
459  symex_throw(state);
460  symex_transition(state);
461  break;
462 
463  case NO_INSTRUCTION_TYPE:
464  throw "symex got NO_INSTRUCTION";
465 
466  default:
467  throw "symex got unexpected instruction";
468  }
469 }
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:245
void return_assignment(statet &)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
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:206
loop_iterationst loop_iterations
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
Definition: goto_symex.h:86
virtual void do_simplify(exprt &)
Definition: goto_symex.cpp:19
void switch_to_thread(unsigned t)
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
virtual void symex_step(const get_goto_functiont &, statet &)
do just one step
Definition: symex_main.cpp:302
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:239
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:240
const irep_idt & id() const
Definition: irep.h:259
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:890
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:267
virtual void symex_other(statet &)
Definition: symex_other.cpp:77
std::unordered_map< irep_idt, local_safe_pointerst > safe_pointers
Definition: goto_symex.h:472
#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:168
virtual void symex_with_state(statet &, const goto_functionst &, symbol_tablet &)
symex entire program starting from entry point
Definition: symex_main.cpp:177
const symbol_tablet & outer_symbol_table
The symbol table associated with the goto-program that we&#39;re executing.
Definition: goto_symex.h:230
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:223
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:240
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:242
unsigned remaining_vccs
Definition: goto_symex.h:215
A function call.
Definition: std_code.h:858
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.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Author: Diffblue Ltd.
The boolean constant false.
Definition: std_expr.h:4497
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:148
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:177
exprt & function()
Definition: std_code.h:878
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
A very simple, cheap analysis to determine when dereference operations are trivially guarded by a che...
void swap(irept &irep)
Definition: irep.h:303
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:207
unsigned total_vccs
Definition: goto_symex.h:215
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:909
symex_targett::sourcet source
static format_containert< T > format(const T &o)
Definition: format.h:35