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 
43 {
44 public:
46 
47 private:
48  unsigned nondet_count = 0;
49 };
50 
52 struct symex_configt final
53 {
54  unsigned max_depth;
63 
69 
70  explicit symex_configt(const optionst &options);
71 };
72 
79 {
80 public:
82 
84  message_handlert &mh,
86  symex_target_equationt &_target,
87  const optionst &options,
89  : should_pause_symex(false),
90  symex_config(options),
91  language_mode(),
94  target(_target),
96  log(mh),
97  guard_identifier("goto_symex::\\guard"),
100  _total_vccs(std::numeric_limits<unsigned>::max()),
101  _remaining_vccs(std::numeric_limits<unsigned>::max())
102  {
103  }
104 
105  virtual ~goto_symext() = default;
106 
107  typedef
108  std::function<const goto_functionst::goto_functiont &(const irep_idt &)>
110 
117  virtual void symex_from_entry_point_of(
118  const get_goto_functiont &get_goto_function,
119  symbol_tablet &new_symbol_table);
120 
125  virtual void resume_symex_from_saved_state(
126  const get_goto_functiont &get_goto_function,
127  const statet &saved_state,
128  symex_target_equationt *saved_equation,
129  symbol_tablet &new_symbol_table);
130 
138  virtual void symex_with_state(
139  statet &,
140  const goto_functionst &,
141  symbol_tablet &);
142 
150  virtual void symex_with_state(
151  statet &,
152  const get_goto_functiont &,
153  symbol_tablet &);
154 
163 
164 protected:
166 
176  statet &state,
177  const get_goto_functiont &get_goto_function,
178  const irep_idt &function_identifier,
181 
186  void symex_threaded_step(
187  statet &, const get_goto_functiont &);
188 
189  virtual void symex_step(
190  const get_goto_functiont &,
191  statet &);
192 
193 public:
194 
198 
199 protected:
200 
207 
218 
219  mutable messaget log;
220 
222 
223  // this does the following:
224  // a) rename non-det choices
225  // b) remove pointer dereferencing
226  // c) clean up byte_extract on the lhs of an assignment
227  void clean_expr(
228  exprt &, statet &, bool write);
229 
230  void trigger_auto_object(const exprt &, statet &);
231  void initialize_auto_object(const exprt &, statet &);
232  void process_array_expr(exprt &);
233  exprt make_auto_object(const typet &, statet &);
234  virtual void dereference(exprt &, statet &, bool write);
235 
236  void dereference_rec(exprt &, statet &, guardt &, bool write);
237 
239  exprt &,
240  statet &,
241  guardt &);
242 
243  static bool is_index_member_symbol_if(const exprt &expr);
244 
246  const exprt &,
247  statet &,
248  guardt &,
249  bool keep_array);
250 
251  // guards
252 
254 
255  virtual void symex_goto(statet &);
256  virtual void symex_start_thread(statet &);
257  virtual void symex_atomic_begin(statet &);
258  virtual void symex_atomic_end(statet &);
259  virtual void symex_decl(statet &);
260  virtual void symex_decl(statet &, const symbol_exprt &expr);
261  virtual void symex_dead(statet &);
262  virtual void symex_other(statet &);
263 
264  virtual void vcc(
265  const exprt &,
266  const std::string &msg,
267  statet &);
268 
269  virtual void symex_assume(statet &, const exprt &cond);
270 
271  // gotos
272  void merge_gotos(statet &);
273 
274  virtual void merge_goto(
275  const statet::goto_statet &goto_state,
276  statet &);
277 
278  void merge_value_sets(
279  const statet::goto_statet &goto_state,
280  statet &dest);
281 
282  void phi_function(
283  const statet::goto_statet &goto_state,
284  statet &);
285 
286  // determine whether to unwind a loop -- true indicates abort,
287  // with false we continue.
288  virtual bool should_stop_unwind(
289  const symex_targett::sourcet &source,
290  const goto_symex_statet::call_stackt &context,
291  unsigned unwind);
292 
293  virtual void loop_bound_exceeded(statet &, const exprt &guard);
294 
295  // function calls
296 
297  void pop_frame(statet &);
298  void return_assignment(statet &);
299 
300  virtual void no_body(const irep_idt &)
301  {
302  }
303 
304  virtual void symex_function_call(
305  const get_goto_functiont &,
306  statet &,
307  const code_function_callt &);
308 
309  virtual void symex_end_of_function(statet &);
310 
311  virtual void symex_function_call_symbol(
312  const get_goto_functiont &,
313  statet &,
314  const code_function_callt &);
315 
316  virtual void symex_function_call_code(
317  const get_goto_functiont &,
318  statet &,
319  const code_function_callt &);
320 
321  virtual bool get_unwind_recursion(
322  const irep_idt &identifier,
323  unsigned thread_nr,
324  unsigned unwind);
325 
327  const irep_idt &function_identifier,
329  statet &,
330  const exprt::operandst &arguments);
331 
332  void locality(
333  const irep_idt &function_identifier,
334  statet &,
336 
337  // exceptions
338  void symex_throw(statet &);
339  void symex_catch(statet &);
340 
341  virtual void do_simplify(exprt &);
342 
343  void symex_assign(statet &, const code_assignt &);
344 
345  // havocs the given object
346  void havoc_rec(statet &, const guardt &, const exprt &);
347 
349 
350  void symex_assign_rec(
351  statet &,
352  const exprt &lhs,
353  const exprt &full_lhs,
354  const exprt &rhs,
355  guardt &,
357  void symex_assign_symbol(
358  statet &,
359  const ssa_exprt &lhs,
360  const exprt &full_lhs,
361  const exprt &rhs,
362  guardt &,
365  statet &,
366  const typecast_exprt &lhs,
367  const exprt &full_lhs,
368  const exprt &rhs,
369  guardt &,
371  void symex_assign_array(
372  statet &,
373  const index_exprt &lhs,
374  const exprt &full_lhs,
375  const exprt &rhs,
376  guardt &,
379  statet &,
380  const member_exprt &lhs,
381  const exprt &full_lhs,
382  const exprt &rhs,
383  guardt &,
385  void symex_assign_if(
386  statet &,
387  const if_exprt &lhs,
388  const exprt &full_lhs,
389  const exprt &rhs,
390  guardt &,
393  statet &,
394  const byte_extract_exprt &lhs,
395  const exprt &full_lhs,
396  const exprt &rhs,
397  guardt &,
399 
406  static exprt add_to_lhs(const exprt &lhs, const exprt &what);
407 
408  virtual void symex_gcc_builtin_va_arg_next(
409  statet &, const exprt &lhs, const side_effect_exprt &);
410  virtual void symex_allocate(
411  statet &, const exprt &lhs, const side_effect_exprt &);
412  virtual void symex_cpp_delete(statet &, const codet &);
413  virtual void symex_cpp_new(
414  statet &, const exprt &lhs, const side_effect_exprt &);
415  virtual void symex_fkt(statet &, const code_function_callt &);
416  virtual void symex_macro(statet &, const code_function_callt &);
417  virtual void symex_trace(statet &, const code_function_callt &);
418  virtual void symex_printf(statet &, const exprt &rhs);
419  virtual void symex_input(statet &, const codet &);
420  virtual void symex_output(statet &, const codet &);
421 
423  static unsigned dynamic_counter;
424 
425  void rewrite_quantifiers(exprt &, statet &);
426 
428 
429 public:
439  std::size_t path_segment_vccs;
440 
441 protected:
448 
451 
452 public:
453  unsigned get_total_vccs()
454  {
455  INVARIANT(
456  _total_vccs != std::numeric_limits<unsigned>::max(),
457  "symex_threaded_step should have been executed at least once before "
458  "attempting to read total_vccs");
459  return _total_vccs;
460  }
461 
463  {
464  INVARIANT(
465  _remaining_vccs != std::numeric_limits<unsigned>::max(),
466  "symex_threaded_step should have been executed at least once before "
467  "attempting to read remaining_vccs");
468  return _remaining_vccs;
469  }
470 
471  void validate(const namespacet &ns, const validation_modet vm) const
472  {
473  target.validate(ns, vm);
474  }
475 };
476 
478 
479 void symex_transition(
482  bool is_backwards_goto);
483 
484 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_H
The type of an expression, extends irept.
Definition: type.h:27
bool constant_propagation
Definition: goto_symex.h:57
virtual void symex_gcc_builtin_va_arg_next(statet &, const exprt &lhs, const side_effect_exprt &)
Semantic type conversion.
Definition: std_expr.h:2277
BigInt mp_integer
Definition: mp_arith.h:22
void return_assignment(statet &)
Base type of functions.
Definition: std_types.h:751
Generate Equation using Symbolic Execution.
virtual void no_body(const irep_idt &)
Definition: goto_symex.h:300
virtual void symex_from_entry_point_of(const get_goto_functiont &get_goto_function, symbol_tablet &new_symbol_table)
symex entire program starting from entry point
Definition: symex_main.cpp:295
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...
virtual void symex_goto(statet &)
Definition: symex_goto.cpp:25
unsigned _remaining_vccs
Definition: goto_symex.h:449
virtual void symex_fkt(statet &, const code_function_callt &)
Goto Programs with Functions.
static bool is_index_member_symbol_if(const exprt &expr)
void symex_assign_byte_extract(statet &, const byte_extract_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Symbolic Execution.
unsigned max_depth
Definition: goto_symex.h:54
virtual void merge_goto(const statet::goto_statet &goto_state, statet &)
Definition: symex_goto.cpp:321
The trinary if-then-else operator.
Definition: std_expr.h:3427
virtual void symex_macro(statet &, const code_function_callt &)
Definition: guard.h:19
virtual void symex_function_call_symbol(const get_goto_functiont &, statet &, const code_function_callt &)
STL namespace.
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
Definition: goto_symex.h:109
virtual void resume_symex_from_saved_state(const get_goto_functiont &get_goto_function, const statet &saved_state, symex_target_equationt *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:273
virtual void do_simplify(exprt &)
Definition: goto_symex.cpp:18
void validate(const namespacet &ns, const validation_modet vm) const
void validate(const namespacet &ns, const validation_modet vm) const
Definition: goto_symex.h:471
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:83
void symex_assign_rec(statet &, const exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
mp_integer debug_level
Definition: goto_symex.h:62
virtual void symex_step(const get_goto_functiont &, statet &)
do just one step
Definition: symex_main.cpp:325
Extract member of struct or union.
Definition: std_expr.h:3890
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 &)
void initialize_entry_point(statet &state, const get_goto_functiont &get_goto_function, const irep_idt &function_identifier, 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:145
symex_targett::assignment_typet assignment_typet
Definition: goto_symex.h:348
void symex_throw(statet &)
Definition: symex_throw.cpp:14
void parameter_assignments(const irep_idt &function_identifier, const goto_functionst::goto_functiont &, statet &, const exprt::operandst &arguments)
static exprt add_to_lhs(const exprt &lhs, const exprt &what)
Store the what expression by recursively descending into the operands of lhs until the first operand ...
Configuration of the symbolic execution.
Definition: goto_symex.h:52
symex_nondet_generatort build_symex_nondet
Definition: goto_symex.h:422
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:215
bool simplify_opt
Definition: goto_symex.h:59
virtual ~goto_symext()=default
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 &)
virtual void symex_other(statet &)
Definition: symex_other.cpp:77
Identifies source in the context of symbolic execution.
Definition: symex_target.h:35
bool doing_path_exploration
Definition: goto_symex.h:55
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:227
static unsigned dynamic_counter
Definition: goto_symex.h:423
const symbol_tablet & outer_symbol_table
The symbol table associated with the goto-program that we&#39;re executing.
Definition: goto_symex.h:206
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:101
messaget log
Definition: goto_symex.h:219
virtual void symex_decl(statet &)
Definition: symex_decl.cpp:22
symex_target_equationt & target
Definition: goto_symex.h:216
void merge_value_sets(const statet::goto_statet &goto_state, statet &dest)
Definition: symex_goto.cpp:343
The symbol table.
Definition: symbol_table.h:19
instructionst::const_iterator const_targett
Definition: goto_program.h:415
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
::goto_functiont goto_functiont
std::size_t path_segment_vccs
Number of VCCs generated during the run of this goto_symext object.
Definition: goto_symex.h:439
void symex_transition(goto_symext::statet &state)
Definition: symex_main.cpp:66
void dereference_rec(exprt &, statet &, guardt &, bool write)
bool run_validation_checks
Should the additional validation checks be run?
Definition: goto_symex.h:68
codet representation of a function call statement.
Definition: std_code.h:1036
A collection of goto functions.
path_storaget & path_storage
Definition: goto_symex.h:427
exprt make_auto_object(const typet &, statet &)
virtual void dereference(exprt &, statet &, bool write)
Class that provides messages with a built-in verbosity &#39;level&#39;.
Definition: message.h:144
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
goto_symex_statet statet
Definition: goto_symex.h:81
virtual bool should_stop_unwind(const symex_targett::sourcet &source, const goto_symex_statet::call_stackt &context, unsigned unwind)
Definition: symex_goto.cpp:579
virtual void symex_trace(statet &, const code_function_callt &)
virtual void loop_bound_exceeded(statet &, const exprt &guard)
Definition: symex_goto.cpp:546
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
std::vector< exprt > operandst
Definition: expr.h:57
unsigned atomic_section_counter
Definition: goto_symex.h:217
virtual void symex_input(statet &, const codet &)
void phi_function(const statet::goto_statet &goto_state, statet &)
Definition: symex_goto.cpp:514
void rewrite_quantifiers(exprt &, statet &)
Definition: symex_main.cpp:130
void symex_assign(statet &, const code_assignt &)
virtual void vcc(const exprt &, const std::string &msg, statet &)
Definition: symex_main.cpp:73
The main class for the forward symbolic simulator.
Definition: goto_symex.h:78
void symex_threaded_step(statet &, const get_goto_functiont &)
Invokes symex_step and verifies whether additional threads can be executed.
Definition: symex_main.cpp:194
std::vector< framet > call_stackt
bool self_loops_to_assumptions
Definition: goto_symex.h:58
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:277
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:197
void dereference_rec_address_of(exprt &, statet &, guardt &)
bool should_pause_symex
Have states been pushed onto the workqueue?
Definition: goto_symex.h:162
const symex_configt symex_config
Definition: goto_symex.h:165
Base class for all expressions.
Definition: expr.h:54
symex_configt(const optionst &options)
Definition: symex_main.cpp:26
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 &)
bool allow_pointer_unsoundness
Definition: goto_symex.h:56
virtual void symex_dead(statet &)
Definition: symex_dead.cpp:20
virtual void symex_start_thread(statet &)
const irep_idt guard_identifier
Definition: goto_symex.h:253
void merge_gotos(statet &)
Definition: symex_goto.cpp:297
unsigned get_total_vccs()
Definition: goto_symex.h:453
validation_modet
virtual void symex_printf(statet &, const exprt &rhs)
Expression to hold a symbol (variable)
Definition: std_expr.h:143
void symex_assign_array(statet &, const index_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
Options.
nondet_symbol_exprt operator()(typet &type)
Definition: goto_symex.cpp:24
bool unwinding_assertions
Definition: goto_symex.h:60
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
An expression containing a side effect.
Definition: std_code.h:1560
virtual void symex_function_call(const get_goto_functiont &, statet &, const code_function_callt &)
TO_BE_DOCUMENTED.
unsigned int statet
bool partial_loops
Definition: goto_symex.h:61
virtual void symex_cpp_delete(statet &, const codet &)
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
unsigned _total_vccs
Definition: goto_symex.h:449
Storage of symbolic execution paths to resume.
Functor generating fresh nondet symbols.
Definition: goto_symex.h:42
unsigned get_remaining_vccs()
Definition: goto_symex.h:462
A codet representing an assignment in the program.
Definition: std_code.h:256
virtual bool get_unwind_recursion(const irep_idt &identifier, unsigned thread_nr, unsigned unwind)
void havoc_rec(statet &, const guardt &, const exprt &)
Definition: symex_other.cpp:20
Array index operator.
Definition: std_expr.h:1595
void symex_assign_symbol(statet &, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)