cprover
goto_symex.h
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 #ifndef CPROVER_GOTO_SYMEX_GOTO_SYMEX_H
13 #define CPROVER_GOTO_SYMEX_GOTO_SYMEX_H
14 
16 
17 #include <util/options.h>
18 #include <util/message.h>
19 
21 
22 #include "goto_symex_state.h"
23 #include "path_storage.h"
24 #include "symex_target_equation.h"
25 
26 class byte_extract_exprt;
27 class typet;
28 class code_typet;
29 class symbol_tablet;
30 class code_assignt;
32 class exprt;
33 class goto_symex_statet;
34 class guardt;
35 class if_exprt;
36 class index_exprt;
37 class symbol_exprt;
38 class member_exprt;
39 class namespacet;
40 class side_effect_exprt;
41 class typecast_exprt;
42 
49 {
50 public:
52 
54  message_handlert &mh,
56  symex_target_equationt &_target,
57  const optionst &options,
59  : should_pause_symex(false),
61  max_depth(options.get_unsigned_int_option("depth")),
62  doing_path_exploration(options.is_set("paths")),
64  options.get_bool_option("allow-pointer-unsoundness")),
65  total_vccs(0),
66  remaining_vccs(0),
69  language_mode(),
72  target(_target),
74  log(mh),
75  guard_identifier("goto_symex::\\guard"),
77  {
78  }
79 
80  virtual ~goto_symext()
81  {
82  }
83 
84  typedef
85  std::function<const goto_functionst::goto_functiont &(const irep_idt &)>
87 
94  virtual void symex_from_entry_point_of(
95  const goto_functionst &goto_functions,
96  symbol_tablet &new_symbol_table);
97 
104  virtual void symex_from_entry_point_of(
105  const get_goto_functiont &get_goto_function,
106  symbol_tablet &new_symbol_table);
107 
112  virtual void resume_symex_from_saved_state(
113  const get_goto_functiont &get_goto_function,
114  const statet &saved_state,
115  symex_target_equationt *const saved_equation,
116  symbol_tablet &new_symbol_table);
117 
125  virtual void symex_with_state(
126  statet &,
127  const goto_functionst &,
128  symbol_tablet &);
129 
137  virtual void symex_with_state(
138  statet &,
139  const get_goto_functiont &,
140  symbol_tablet &);
141 
150  virtual void symex_instruction_range(
151  statet &,
152  const goto_functionst &,
155 
164  virtual void symex_instruction_range(
165  statet &state,
166  const get_goto_functiont &get_goto_function,
169 
178 
179 protected:
188  statet &state,
189  const get_goto_functiont &get_goto_function,
192 
197  void symex_threaded_step(
198  statet &, const get_goto_functiont &);
199 
200  virtual void symex_step(
201  const get_goto_functiont &,
202  statet &);
203 
205 
206  const unsigned max_depth;
209 
210 public:
211  // these bypass the target maps
212  virtual void symex_step_goto(statet &, bool taken);
213 
214  // statistics
216 
219 
223 
224 protected:
231 
242 
243  mutable messaget log;
244 
246 
247  // this does the following:
248  // a) rename non-det choices
249  // b) remove pointer dereferencing
250  // c) clean up byte_extract on the lhs of an assignment
251  void clean_expr(
252  exprt &, statet &, bool write);
253 
254  void trigger_auto_object(const exprt &, statet &);
255  void initialize_auto_object(const exprt &, statet &);
256  void process_array_expr(exprt &);
257  exprt make_auto_object(const typet &, statet &);
258  virtual void dereference(exprt &, statet &, const bool write);
259 
260  void dereference_rec(
261  exprt &,
262  statet &,
263  guardt &,
264  const bool write);
265 
267  exprt &,
268  statet &,
269  guardt &);
270 
271  static bool is_index_member_symbol_if(const exprt &expr);
272 
274  const exprt &,
275  statet &,
276  guardt &,
277  bool keep_array);
278 
279  // guards
280 
282 
283  // symex
284  virtual void symex_transition(
285  statet &,
287  bool is_backwards_goto=false);
288 
290  {
292  ++next;
293  symex_transition(state, next);
294  }
295 
296  virtual void symex_goto(statet &);
297  virtual void symex_start_thread(statet &);
298  virtual void symex_atomic_begin(statet &);
299  virtual void symex_atomic_end(statet &);
300  virtual void symex_decl(statet &);
301  virtual void symex_decl(statet &, const symbol_exprt &expr);
302  virtual void symex_dead(statet &);
303  virtual void symex_other(statet &);
304 
305  virtual void vcc(
306  const exprt &,
307  const std::string &msg,
308  statet &);
309 
310  virtual void symex_assume(statet &, const exprt &cond);
311 
312  // gotos
313  void merge_gotos(statet &);
314 
315  virtual void merge_goto(
316  const statet::goto_statet &goto_state,
317  statet &);
318 
319  void merge_value_sets(
320  const statet::goto_statet &goto_state,
321  statet &dest);
322 
323  void phi_function(
324  const statet::goto_statet &goto_state,
325  statet &);
326 
327  // determine whether to unwind a loop -- true indicates abort,
328  // with false we continue.
329  virtual bool get_unwind(
330  const symex_targett::sourcet &source,
331  const goto_symex_statet::call_stackt &context,
332  unsigned unwind);
333 
334  virtual void loop_bound_exceeded(statet &, const exprt &guard);
335 
336  // function calls
337 
338  void pop_frame(statet &);
339  void return_assignment(statet &);
340 
341  virtual void no_body(const irep_idt &)
342  {
343  }
344 
345  virtual void symex_function_call(
346  const get_goto_functiont &,
347  statet &,
348  const code_function_callt &);
349 
350  virtual void symex_end_of_function(statet &);
351 
352  virtual void symex_function_call_symbol(
353  const get_goto_functiont &,
354  statet &,
355  const code_function_callt &);
356 
357  virtual void symex_function_call_code(
358  const get_goto_functiont &,
359  statet &,
360  const code_function_callt &);
361 
362  virtual bool get_unwind_recursion(
363  const irep_idt &identifier,
364  const unsigned thread_nr,
365  unsigned unwind);
366 
368  const irep_idt function_identifier,
370  statet &,
371  const exprt::operandst &arguments);
372 
373  void locality(
374  const irep_idt function_identifier,
375  statet &,
377 
378  void add_end_of_function(
379  exprt &code,
380  const irep_idt &identifier);
381 
383 
384  // exceptions
385  void symex_throw(statet &);
386  void symex_catch(statet &);
387 
388  virtual void do_simplify(exprt &);
389 
390  void symex_assign(statet &, const code_assignt &);
391 
392  // havocs the given object
393  void havoc_rec(statet &, const guardt &, const exprt &);
394 
396 
397  void symex_assign_rec(
398  statet &,
399  const exprt &lhs,
400  const exprt &full_lhs,
401  const exprt &rhs,
402  guardt &,
404  void symex_assign_symbol(
405  statet &,
406  const ssa_exprt &lhs,
407  const exprt &full_lhs,
408  const exprt &rhs,
409  guardt &,
412  statet &,
413  const typecast_exprt &lhs,
414  const exprt &full_lhs,
415  const exprt &rhs,
416  guardt &,
418  void symex_assign_array(
419  statet &,
420  const index_exprt &lhs,
421  const exprt &full_lhs,
422  const exprt &rhs,
423  guardt &,
426  statet &,
427  const member_exprt &lhs,
428  const exprt &full_lhs,
429  const exprt &rhs,
430  guardt &,
432  void symex_assign_if(
433  statet &,
434  const if_exprt &lhs,
435  const exprt &full_lhs,
436  const exprt &rhs,
437  guardt &,
440  statet &,
441  const byte_extract_exprt &lhs,
442  const exprt &full_lhs,
443  const exprt &rhs,
444  guardt &,
446 
447  static exprt add_to_lhs(const exprt &lhs, const exprt &what);
448 
449  virtual void symex_gcc_builtin_va_arg_next(
450  statet &, const exprt &lhs, const side_effect_exprt &);
451  virtual void symex_allocate(
452  statet &, const exprt &lhs, const side_effect_exprt &);
453  virtual void symex_cpp_delete(statet &, const codet &);
454  virtual void symex_cpp_new(
455  statet &, const exprt &lhs, const side_effect_exprt &);
456  virtual void symex_fkt(statet &, const code_function_callt &);
457  virtual void symex_macro(statet &, const code_function_callt &);
458  virtual void symex_trace(statet &, const code_function_callt &);
459  virtual void symex_printf(statet &, const exprt &rhs);
460  virtual void symex_input(statet &, const codet &);
461  virtual void symex_output(statet &, const codet &);
462 
463  static unsigned nondet_count;
464  static unsigned dynamic_counter;
465 
466  void read(exprt &);
467  void replace_nondet(exprt &);
468  void rewrite_quantifiers(exprt &, statet &);
469 
471 
472  std::unordered_map<irep_idt, local_safe_pointerst> safe_pointers;
473 };
474 
475 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_H
The type of an expression.
Definition: type.h:22
virtual void symex_gcc_builtin_va_arg_next(statet &, const exprt &lhs, const side_effect_exprt &)
semantic type conversion
Definition: std_expr.h:2111
const bool allow_pointer_unsoundness
Definition: goto_symex.h:208
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 &)
Base type of functions.
Definition: std_types.h:764
irep_idt guard_identifier
Definition: goto_symex.h:281
Generate Equation using Symbolic Execution.
void read(exprt &)
virtual void no_body(const irep_idt &)
Definition: goto_symex.h:341
virtual bool get_unwind_recursion(const irep_idt &identifier, const unsigned thread_nr, unsigned unwind)
goto_programt::const_targett pc
Definition: symex_target.h:32
virtual void symex_goto(statet &)
Definition: symex_goto.cpp:22
virtual void symex_fkt(statet &, const code_function_callt &)
virtual void symex_transition(statet &, goto_programt::const_targett to, bool is_backwards_goto=false)
Definition: symex_main.cpp:24
void replace_nondet(exprt &)
Definition: goto_symex.cpp:32
Goto Programs with Functions.
static bool is_index_member_symbol_if(const exprt &expr)
bool constant_propagation
Definition: goto_symex.h:217
void symex_assign_byte_extract(statet &, const byte_extract_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
Symbolic Execution.
virtual bool get_unwind(const symex_targett::sourcet &source, const goto_symex_statet::call_stackt &context, unsigned unwind)
Definition: symex_goto.cpp:541
virtual void merge_goto(const statet::goto_statet &goto_state, statet &)
Definition: symex_goto.cpp:343
virtual void symex_step_goto(statet &, bool taken)
Definition: symex_goto.cpp:302
The trinary if-then-else operator.
Definition: std_expr.h:3359
virtual void symex_macro(statet &, const code_function_callt &)
Definition: guard.h:19
const unsigned max_depth
Definition: goto_symex.h:206
virtual void symex_function_call_symbol(const get_goto_functiont &, statet &, const code_function_callt &)
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
goto_symext(message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage)
Definition: goto_symex.h:53
void symex_assign_rec(statet &, const exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
virtual void symex_step(const get_goto_functiont &, statet &)
do just one step
Definition: symex_main.cpp:302
Extract member of struct or union.
Definition: std_expr.h:3869
virtual void symex_end_of_function(statet &)
do function call by inlining
void symex_catch(statet &)
Definition: symex_catch.cpp:14
virtual void symex_atomic_end(statet &)
virtual void dereference(exprt &, statet &, const bool write)
symex_targett::assignment_typet assignment_typet
Definition: goto_symex.h:395
void symex_throw(statet &)
Definition: symex_throw.cpp:14
static exprt add_to_lhs(const exprt &lhs, const exprt &what)
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:239
bool self_loops_to_assumptions
Definition: goto_symex.h:218
virtual void symex_atomic_begin(statet &)
void symex_assign_typecast(statet &, const typecast_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
virtual void symex_allocate(statet &, const exprt &lhs, const side_effect_exprt &)
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
static unsigned nondet_count
Definition: goto_symex.h:463
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
virtual void symex_cpp_new(statet &, const exprt &lhs, const side_effect_exprt &)
Handles side effects of type &#39;new&#39; for C++ and &#39;new array&#39; for C++ and Java language modes...
virtual void symex_with_state(statet &, const goto_functionst &, symbol_tablet &)
symex entire program starting from entry point
Definition: symex_main.cpp:177
static unsigned dynamic_counter
Definition: goto_symex.h:464
const symbol_tablet & outer_symbol_table
The symbol table associated with the goto-program that we&#39;re executing.
Definition: goto_symex.h:230
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
exprt address_arithmetic(const exprt &, statet &, guardt &, bool keep_array)
Evaluate an ID_address_of expression.
virtual void symex_assume(statet &, const exprt &cond)
Definition: symex_main.cpp:75
virtual ~goto_symext()
Definition: goto_symex.h:80
messaget log
Definition: goto_symex.h:243
virtual void symex_decl(statet &)
Definition: symex_decl.cpp:22
symex_target_equationt & target
Definition: goto_symex.h:240
void merge_value_sets(const statet::goto_statet &goto_state, statet &dest)
Definition: symex_goto.cpp:363
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
unsigned remaining_vccs
Definition: goto_symex.h:215
A function call.
Definition: std_code.h:858
path_storaget & path_storage
Definition: goto_symex.h:470
void locality(const irep_idt function_identifier, statet &, const goto_functionst::goto_functiont &)
preserves locality of local variables of a given function by applying L1 renaming to the local identi...
void dereference_rec(exprt &, statet &, guardt &, const bool write)
exprt make_auto_object(const typet &, statet &)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
goto_symex_statet statet
Definition: goto_symex.h:51
virtual void symex_trace(statet &, const code_function_callt &)
virtual void loop_bound_exceeded(statet &, const exprt &guard)
Definition: symex_goto.cpp:502
void pop_frame(statet &)
pop one call frame
void symex_assign_if(statet &, const if_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
Storage for symbolic execution paths to be resumed later.
Definition: path_storage.h:24
void add_end_of_function(exprt &code, const irep_idt &identifier)
std::vector< exprt > operandst
Definition: expr.h:45
void parameter_assignments(const irep_idt function_identifier, const goto_functionst::goto_functiont &, statet &, const exprt::operandst &arguments)
unsigned atomic_section_counter
Definition: goto_symex.h:241
virtual void symex_input(statet &, const codet &)
void phi_function(const statet::goto_statet &goto_state, statet &)
Definition: symex_goto.cpp:376
virtual void symex_transition(statet &state)
Definition: goto_symex.h:289
const optionst & options
Definition: goto_symex.h:204
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
The main class for the forward symbolic simulator.
Definition: goto_symex.h: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
std::vector< framet > call_stackt
void process_array_expr(exprt &)
Given an expression, find the root object and the offset into it.
void clean_expr(exprt &, statet &, bool write)
Expression to hold a nondeterministic choice.
Definition: std_expr.h:239
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use...
Definition: goto_symex.h:222
void dereference_rec_address_of(exprt &, statet &, guardt &)
bool should_pause_symex
Have states been pushed onto the workqueue?
Definition: goto_symex.h:177
Base class for all expressions.
Definition: expr.h:42
virtual void symex_function_call_code(const get_goto_functiont &, statet &, const code_function_callt &)
do function call by inlining
void trigger_auto_object(const exprt &, statet &)
virtual void symex_output(statet &, const codet &)
void symex_assign_struct_member(statet &, const member_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
void initialize_auto_object(const exprt &, statet &)
virtual void symex_dead(statet &)
Definition: symex_dead.cpp:20
Local safe pointer analysis.
virtual void symex_start_thread(statet &)
void merge_gotos(statet &)
Definition: symex_goto.cpp:319
virtual void symex_printf(statet &, const exprt &rhs)
Expression to hold a symbol (variable)
Definition: std_expr.h:90
void symex_assign_array(statet &, const index_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
Options.
A statement in a programming language.
Definition: std_code.h:21
An expression containing a side effect.
Definition: std_code.h:1271
virtual void symex_function_call(const get_goto_functiont &, statet &, const code_function_callt &)
const bool doing_path_exploration
Definition: goto_symex.h:207
unsigned total_vccs
Definition: goto_symex.h:215
TO_BE_DOCUMENTED.
unsigned int statet
virtual void symex_cpp_delete(statet &, const codet &)
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
Storage of symbolic execution paths to resume.
Assignment.
Definition: std_code.h:196
nondet_symbol_exprt build_symex_nondet(typet &type)
Definition: goto_symex.cpp:25
void havoc_rec(statet &, const guardt &, const exprt &)
Definition: symex_other.cpp:20
array index operator
Definition: std_expr.h:1462
symex_targett::sourcet source
void symex_assign_symbol(statet &, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)