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 
15 #include <util/options.h>
16 #include <util/message.h>
17 
19 
20 #include "goto_symex_state.h"
21 #include "path_storage.h"
22 #include "symex_target_equation.h"
23 
24 class byte_extract_exprt;
25 class typet;
26 class code_typet;
27 class symbol_tablet;
28 class code_assignt;
30 class exprt;
31 class goto_symex_statet;
32 class guardt;
33 class if_exprt;
34 class index_exprt;
35 class symbol_exprt;
36 class member_exprt;
37 class namespacet;
38 class side_effect_exprt;
39 class typecast_exprt;
40 
47 {
48 public:
50 
52  message_handlert &mh,
54  symex_target_equationt &_target,
55  const optionst &options,
57  : should_pause_symex(false),
59  max_depth(options.get_unsigned_int_option("depth")),
60  doing_path_exploration(options.is_set("paths")),
62  options.get_bool_option("allow-pointer-unsoundness")),
63  total_vccs(0),
64  remaining_vccs(0),
67  language_mode(),
70  target(_target),
72  log(mh),
73  guard_identifier("goto_symex::\\guard"),
75  {
76  }
77 
78  virtual ~goto_symext()
79  {
80  }
81 
82  typedef
83  std::function<const goto_functionst::goto_functiont &(const irep_idt &)>
85 
92  virtual void symex_from_entry_point_of(
93  const goto_functionst &goto_functions,
94  symbol_tablet &new_symbol_table);
95 
102  virtual void symex_from_entry_point_of(
103  const get_goto_functiont &get_goto_function,
104  symbol_tablet &new_symbol_table);
105 
110  virtual void resume_symex_from_saved_state(
111  const get_goto_functiont &get_goto_function,
112  const statet &saved_state,
113  symex_target_equationt *const saved_equation,
114  symbol_tablet &new_symbol_table);
115 
123  virtual void symex_with_state(
124  statet &,
125  const goto_functionst &,
126  symbol_tablet &);
127 
135  virtual void symex_with_state(
136  statet &,
137  const get_goto_functiont &,
138  symbol_tablet &);
139 
148  virtual void symex_instruction_range(
149  statet &,
150  const goto_functionst &,
153 
162  virtual void symex_instruction_range(
163  statet &state,
164  const get_goto_functiont &get_goto_function,
167 
176 
177 protected:
186  statet &state,
187  const get_goto_functiont &get_goto_function,
190 
195  void symex_threaded_step(
196  statet &, const get_goto_functiont &);
197 
198  virtual void symex_step(
199  const get_goto_functiont &,
200  statet &);
201 
203 
204  const unsigned max_depth;
207 
208 public:
209  // these bypass the target maps
210  virtual void symex_step_goto(statet &, bool taken);
211 
212  // statistics
214 
217 
221 
222 protected:
229 
240 
241  mutable messaget log;
242 
244 
245  // this does the following:
246  // a) rename non-det choices
247  // b) remove pointer dereferencing
248  // c) clean up byte_extract on the lhs of an assignment
249  void clean_expr(
250  exprt &, statet &, bool write);
251 
252  void trigger_auto_object(const exprt &, statet &);
253  void initialize_auto_object(const exprt &, statet &);
254  void process_array_expr(exprt &);
255  exprt make_auto_object(const typet &, statet &);
256  virtual void dereference(exprt &, statet &, const bool write);
257 
258  void dereference_rec(
259  exprt &,
260  statet &,
261  guardt &,
262  const bool write);
263 
265  exprt &,
266  statet &,
267  guardt &);
268 
269  static bool is_index_member_symbol_if(const exprt &expr);
270 
272  const exprt &,
273  statet &,
274  guardt &,
275  bool keep_array);
276 
277  // guards
278 
280 
281  // symex
282  virtual void symex_transition(
283  statet &,
285  bool is_backwards_goto=false);
286 
288  {
290  ++next;
291  symex_transition(state, next);
292  }
293 
294  virtual void symex_goto(statet &);
295  virtual void symex_start_thread(statet &);
296  virtual void symex_atomic_begin(statet &);
297  virtual void symex_atomic_end(statet &);
298  virtual void symex_decl(statet &);
299  virtual void symex_decl(statet &, const symbol_exprt &expr);
300  virtual void symex_dead(statet &);
301  virtual void symex_other(statet &);
302 
303  virtual void vcc(
304  const exprt &,
305  const std::string &msg,
306  statet &);
307 
308  virtual void symex_assume(statet &, const exprt &cond);
309 
310  // gotos
311  void merge_gotos(statet &);
312 
313  virtual void merge_goto(
314  const statet::goto_statet &goto_state,
315  statet &);
316 
317  void merge_value_sets(
318  const statet::goto_statet &goto_state,
319  statet &dest);
320 
321  void phi_function(
322  const statet::goto_statet &goto_state,
323  statet &);
324 
325  // determine whether to unwind a loop -- true indicates abort,
326  // with false we continue.
327  virtual bool get_unwind(
328  const symex_targett::sourcet &source,
329  unsigned unwind);
330 
331  virtual void loop_bound_exceeded(statet &, const exprt &guard);
332 
333  // function calls
334 
335  void pop_frame(statet &);
336  void return_assignment(statet &);
337 
338  virtual void no_body(const irep_idt &identifier)
339  {
340  }
341 
342  virtual void symex_function_call(
343  const get_goto_functiont &,
344  statet &,
345  const code_function_callt &);
346 
347  virtual void symex_end_of_function(statet &);
348 
349  virtual void symex_function_call_symbol(
350  const get_goto_functiont &,
351  statet &,
352  const code_function_callt &);
353 
354  virtual void symex_function_call_code(
355  const get_goto_functiont &,
356  statet &,
357  const code_function_callt &);
358 
359  virtual bool get_unwind_recursion(
360  const irep_idt &identifier,
361  const unsigned thread_nr,
362  unsigned unwind);
363 
365  const irep_idt function_identifier,
367  statet &,
368  const exprt::operandst &arguments);
369 
370  void locality(
371  const irep_idt function_identifier,
372  statet &,
374 
375  void add_end_of_function(
376  exprt &code,
377  const irep_idt &identifier);
378 
380 
381  // exceptions
382  void symex_throw(statet &);
383  void symex_catch(statet &);
384 
385  virtual void do_simplify(exprt &);
386 
387  void symex_assign(statet &, const code_assignt &);
388 
389  // havocs the given object
390  void havoc_rec(statet &, const guardt &, const exprt &);
391 
393 
394  void symex_assign_rec(
395  statet &,
396  const exprt &lhs,
397  const exprt &full_lhs,
398  const exprt &rhs,
399  guardt &,
401  void symex_assign_symbol(
402  statet &,
403  const ssa_exprt &lhs,
404  const exprt &full_lhs,
405  const exprt &rhs,
406  guardt &,
409  statet &,
410  const typecast_exprt &lhs,
411  const exprt &full_lhs,
412  const exprt &rhs,
413  guardt &,
415  void symex_assign_array(
416  statet &,
417  const index_exprt &lhs,
418  const exprt &full_lhs,
419  const exprt &rhs,
420  guardt &,
423  statet &,
424  const member_exprt &lhs,
425  const exprt &full_lhs,
426  const exprt &rhs,
427  guardt &,
429  void symex_assign_if(
430  statet &,
431  const if_exprt &lhs,
432  const exprt &full_lhs,
433  const exprt &rhs,
434  guardt &,
437  statet &,
438  const byte_extract_exprt &lhs,
439  const exprt &full_lhs,
440  const exprt &rhs,
441  guardt &,
443 
444  static exprt add_to_lhs(const exprt &lhs, const exprt &what);
445 
446  virtual void symex_gcc_builtin_va_arg_next(
447  statet &, const exprt &lhs, const side_effect_exprt &);
448  virtual void symex_allocate(
449  statet &, const exprt &lhs, const side_effect_exprt &);
450  virtual void symex_cpp_delete(statet &, const codet &);
451  virtual void symex_cpp_new(
452  statet &, const exprt &lhs, const side_effect_exprt &);
453  virtual void symex_fkt(statet &, const code_function_callt &);
454  virtual void symex_macro(statet &, const code_function_callt &);
455  virtual void symex_trace(statet &, const code_function_callt &);
456  virtual void symex_printf(statet &, const exprt &lhs, const exprt &rhs);
457  virtual void symex_input(statet &, const codet &);
458  virtual void symex_output(statet &, const codet &);
459 
460  static unsigned nondet_count;
461  static unsigned dynamic_counter;
462 
463  void read(exprt &);
464  void replace_nondet(exprt &);
465  void rewrite_quantifiers(exprt &, statet &);
466 
468 };
469 
470 #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:206
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 &)
Base type of functions.
Definition: std_types.h:764
irep_idt guard_identifier
Definition: goto_symex.h:279
Generate Equation using Symbolic Execution.
void read(exprt &)
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:215
void symex_assign_byte_extract(statet &, const byte_extract_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
Symbolic Execution.
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:3361
virtual void symex_macro(statet &, const code_function_callt &)
Definition: guard.h:19
const unsigned max_depth
Definition: goto_symex.h:204
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:84
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:51
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:295
Extract member of struct or union.
Definition: std_expr.h:3871
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:392
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:237
bool self_loops_to_assumptions
Definition: goto_symex.h:216
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:460
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
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:170
static unsigned dynamic_counter
Definition: goto_symex.h:461
const symbol_tablet & outer_symbol_table
The symbol table associated with the goto-program that we&#39;re executing.
Definition: goto_symex.h:228
virtual bool get_unwind(const symex_targett::sourcet &source, unsigned unwind)
Definition: symex_goto.cpp:541
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
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:78
messaget log
Definition: goto_symex.h:241
virtual void symex_decl(statet &)
Definition: symex_decl.cpp:22
symex_target_equationt & target
Definition: goto_symex.h:238
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:213
A function call.
Definition: std_code.h:828
path_storaget & path_storage
Definition: goto_symex.h:467
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 &)
goto_symex_statet statet
Definition: goto_symex.h:49
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:239
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:287
const optionst & options
Definition: goto_symex.h:202
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:46
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
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:220
void dereference_rec_address_of(exprt &, statet &, guardt &)
bool should_pause_symex
Have states been pushed onto the workqueue?
Definition: goto_symex.h:175
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
virtual void symex_start_thread(statet &)
void merge_gotos(statet &)
Definition: symex_goto.cpp:319
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.
virtual void symex_printf(statet &, const exprt &lhs, const exprt &rhs)
A statement in a programming language.
Definition: std_code.h:21
virtual void no_body(const irep_idt &identifier)
Definition: goto_symex.h:338
An expression containing a side effect.
Definition: std_code.h:1238
virtual void symex_function_call(const get_goto_functiont &, statet &, const code_function_callt &)
const bool doing_path_exploration
Definition: goto_symex.h:205
unsigned total_vccs
Definition: goto_symex.h:213
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:195
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)