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/byte_operators.h>
17 
19 
20 #include "goto_symex_state.h"
21 
22 class typet;
23 class code_typet;
24 class symbol_tablet;
25 class code_assignt;
27 class exprt;
28 class goto_symex_statet;
29 class guardt;
30 class if_exprt;
31 class index_exprt;
32 class symbol_exprt;
33 class member_exprt;
34 class namespacet;
35 class side_effect_exprt;
36 class symex_targett;
37 class typecast_exprt;
38 
42 {
43 public:
45  const namespacet &_ns,
46  symbol_tablet &_new_symbol_table,
47  symex_targett &_target):
48  total_vccs(0),
49  remaining_vccs(0),
51  new_symbol_table(_new_symbol_table),
52  language_mode(),
53  ns(_ns),
54  target(_target),
56  guard_identifier("goto_symex::\\guard")
57  {
58  options.set_option("simplify", true);
59  options.set_option("assertions", true);
60  }
61 
62  virtual ~goto_symext()
63  {
64  }
65 
67 
69  virtual void operator()(
70  const goto_functionst &goto_functions);
71 
73  virtual void operator()(
74  const goto_functionst &goto_functions,
75  const goto_programt &goto_program);
76 
78  virtual void operator()(
79  statet &state,
80  const goto_functionst &goto_functions,
81  const goto_programt &goto_program);
82 
84  virtual void symex_step(
85  const goto_functionst &goto_functions,
86  statet &state);
87 
88  // these bypass the target maps
89  virtual void symex_step_goto(statet &state, bool taken);
90 
91  // statistics
93 
95 
98 
102 
103 protected:
104  const namespacet &ns;
107 
109 
110  void new_name(symbolt &symbol);
111 
112  // this does the following:
113  // a) rename non-det choices
114  // b) remove pointer dereferencing
115  // c) rewrite array_equal expression into equality
116  void clean_expr(
117  exprt &expr, statet &state, bool write);
118 
119  void replace_array_equal(exprt &expr);
120  void trigger_auto_object(const exprt &expr, statet &state);
121  void initialize_auto_object(const exprt &expr, statet &state);
122  void process_array_expr(exprt &expr);
123  void process_array_expr_rec(exprt &expr, const typet &type) const;
124  exprt make_auto_object(const typet &type);
125 
126  virtual void dereference(
127  exprt &expr,
128  statet &state,
129  const bool write);
130 
131  void dereference_rec(
132  exprt &expr,
133  statet &state,
134  guardt &guard,
135  const bool write);
136 
138  exprt &expr,
139  statet &state,
140  guardt &guard);
141 
142  static bool is_index_member_symbol_if(const exprt &expr);
143 
145  const exprt &expr,
146  statet &state,
147  guardt &guard,
148  bool keep_array);
149 
150  // guards
151 
153 
154  // symex
155  virtual void symex_transition(
156  statet &state,
158  bool is_backwards_goto=false);
160  {
162  ++next;
163  symex_transition(state, next);
164  }
165 
166  virtual void symex_goto(statet &state);
167  virtual void symex_start_thread(statet &state);
168  virtual void symex_atomic_begin(statet &state);
169  virtual void symex_atomic_end(statet &state);
170  virtual void symex_decl(statet &state);
171  virtual void symex_decl(statet &state, const symbol_exprt &expr);
172  virtual void symex_dead(statet &state);
173 
174  virtual void symex_other(
175  const goto_functionst &goto_functions,
176  statet &state);
177 
178  virtual void vcc(
179  const exprt &expr,
180  const std::string &msg,
181  statet &state);
182 
183  virtual void symex_assume(statet &state, const exprt &cond);
184 
185  // gotos
186  void merge_gotos(statet &state);
187 
188  virtual void merge_goto(
189  const statet::goto_statet &goto_state,
190  statet &state);
191 
192  void merge_value_sets(
193  const statet::goto_statet &goto_state,
194  statet &dest);
195 
196  void phi_function(
197  const statet::goto_statet &goto_state,
198  statet &state);
199 
200  // determine whether to unwind a loop -- true indicates abort,
201  // with false we continue.
202  virtual bool get_unwind(
203  const symex_targett::sourcet &source,
204  unsigned unwind);
205 
206  virtual void loop_bound_exceeded(statet &state, const exprt &guard);
207 
208  // function calls
209 
210  void pop_frame(statet &state);
212 
213  virtual void no_body(const irep_idt &identifier)
214  {
215  }
216 
217  virtual void symex_function_call(
218  const goto_functionst &goto_functions,
219  statet &state,
220  const code_function_callt &call);
221 
222  virtual void symex_end_of_function(statet &state);
223 
224  virtual void symex_function_call_symbol(
225  const goto_functionst &goto_functions,
226  statet &state,
227  const code_function_callt &call);
228 
229  virtual void symex_function_call_code(
230  const goto_functionst &goto_functions,
231  statet &state,
232  const code_function_callt &call);
233 
234  virtual bool get_unwind_recursion(
235  const irep_idt &identifier,
236  const unsigned thread_nr,
237  unsigned unwind);
238 
240  const irep_idt function_identifier,
241  const goto_functionst::goto_functiont &goto_function,
242  statet &state,
243  const exprt::operandst &arguments);
244 
245  void locality(
246  const irep_idt function_identifier,
247  statet &state,
248  const goto_functionst::goto_functiont &goto_function);
249 
250  void add_end_of_function(
251  exprt &code,
252  const irep_idt &identifier);
253 
254  // exceptions
255 
256  void symex_throw(statet &state);
257  void symex_catch(statet &state);
258 
259  virtual void do_simplify(exprt &expr);
260 
261  // virtual void symex_block(statet &state, const codet &code);
262  void symex_assign_rec(statet &state, const code_assignt &code);
263  virtual void symex_assign(statet &state, const code_assignt &code);
264 
266 
267  void symex_assign_rec(
268  statet &state,
269  const exprt &lhs,
270  const exprt &full_lhs,
271  const exprt &rhs,
272  guardt &guard,
273  assignment_typet assignment_type);
274  void symex_assign_symbol(
275  statet &state,
276  const ssa_exprt &lhs,
277  const exprt &full_lhs,
278  const exprt &rhs,
279  guardt &guard,
280  assignment_typet assignment_type);
282  statet &state,
283  const typecast_exprt &lhs,
284  const exprt &full_lhs,
285  const exprt &rhs,
286  guardt &guard,
287  assignment_typet assignment_type);
288  void symex_assign_array(
289  statet &state,
290  const index_exprt &lhs,
291  const exprt &full_lhs,
292  const exprt &rhs,
293  guardt &guard,
294  assignment_typet assignment_type);
296  statet &state,
297  const member_exprt &lhs,
298  const exprt &full_lhs,
299  const exprt &rhs,
300  guardt &guard,
301  assignment_typet assignment_type);
302  void symex_assign_if(
303  statet &state,
304  const if_exprt &lhs,
305  const exprt &full_lhs,
306  const exprt &rhs,
307  guardt &guard,
308  assignment_typet assignment_type);
310  statet &state,
311  const byte_extract_exprt &lhs,
312  const exprt &full_lhs,
313  const exprt &rhs,
314  guardt &guard,
315  assignment_typet assignment_type);
316 
317  static exprt add_to_lhs(const exprt &lhs, const exprt &what);
318 
319  virtual void symex_gcc_builtin_va_arg_next(
320  statet &state, const exprt &lhs, const side_effect_exprt &code);
321  virtual void symex_malloc(
322  statet &state, const exprt &lhs, const side_effect_exprt &code);
323  virtual void symex_cpp_delete(statet &state, const codet &code);
324  virtual void symex_cpp_new(
325  statet &state, const exprt &lhs, const side_effect_exprt &code);
326  virtual void symex_fkt(statet &state, const code_function_callt &code);
327  virtual void symex_macro(statet &state, const code_function_callt &code);
328  virtual void symex_trace(statet &state, const code_function_callt &code);
329  virtual void symex_printf(statet &state, const exprt &lhs, const exprt &rhs);
330  virtual void symex_input(statet &state, const codet &code);
331  virtual void symex_output(statet &state, const codet &code);
332 
333  static unsigned nondet_count;
334  static unsigned dynamic_counter;
335 
336  void read(exprt &expr);
337  void replace_nondet(exprt &expr);
338  void rewrite_quantifiers(exprt &expr, statet &state);
339 };
340 
341 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_H
virtual void do_simplify(exprt &expr)
Definition: goto_symex.cpp:19
The type of an expression.
Definition: type.h:20
virtual void symex_atomic_begin(statet &state)
semantic type conversion
Definition: std_expr.h:1725
virtual void symex_step_goto(statet &state, bool taken)
Definition: symex_goto.cpp:193
symex_targett & target
Definition: goto_symex.h:105
Base type of functions.
Definition: std_types.h:734
irep_idt guard_identifier
Definition: goto_symex.h:152
virtual bool get_unwind_recursion(const irep_idt &identifier, const unsigned thread_nr, unsigned unwind)
virtual void symex_assign(statet &state, const code_assignt &code)
goto_programt::const_targett pc
Definition: symex_target.h:32
virtual void symex_assume(statet &state, const exprt &cond)
Definition: symex_main.cpp:80
void new_name(symbolt &symbol)
Definition: symex_main.cpp:47
virtual void merge_goto(const statet::goto_statet &goto_state, statet &state)
Definition: symex_goto.cpp:234
void dereference_rec(exprt &expr, statet &state, guardt &guard, const bool write)
virtual void dereference(exprt &expr, statet &state, const bool write)
virtual void symex_function_call_symbol(const goto_functionst &goto_functions, statet &state, const code_function_callt &call)
virtual void symex_decl(statet &state)
Definition: symex_decl.cpp:23
void symex_assign_byte_extract(statet &state, const byte_extract_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
Goto Programs with Functions.
static bool is_index_member_symbol_if(const exprt &expr)
virtual void symex_gcc_builtin_va_arg_next(statet &state, const exprt &lhs, const side_effect_exprt &code)
void symex_assign_if(statet &state, const if_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
virtual void symex_trace(statet &state, const code_function_callt &code)
bool constant_propagation
Definition: goto_symex.h:94
Symbolic Execution.
exprt make_auto_object(const typet &type)
void process_array_expr_rec(exprt &expr, const typet &type) const
void replace_array_equal(exprt &expr)
The trinary if-then-else operator.
Definition: std_expr.h:2771
void parameter_assignments(const irep_idt function_identifier, const goto_functionst::goto_functiont &goto_function, statet &state, const exprt::operandst &arguments)
optionst options
Definition: goto_symex.h:96
Definition: guard.h:19
void read(exprt &expr)
void return_assignment(statet &state)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
virtual void symex_step(const goto_functionst &goto_functions, statet &state)
execute just one step
Definition: symex_main.cpp:188
virtual void symex_macro(statet &state, const code_function_callt &code)
void locality(const irep_idt function_identifier, statet &state, const goto_functionst::goto_functiont &goto_function)
preserves locality of local variables of a given function by applying L1 renaming to the local identi...
void replace_nondet(exprt &expr)
Definition: goto_symex.cpp:25
Extract member of struct or union.
Definition: std_expr.h:3214
symex_targett::assignment_typet assignment_typet
Definition: goto_symex.h:265
void symex_assign_symbol(statet &state, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
static exprt add_to_lhs(const exprt &lhs, const exprt &what)
virtual void symex_printf(statet &state, const exprt &lhs, const exprt &rhs)
virtual void operator()(const goto_functionst &goto_functions)
symex all at once, starting from entry point
Definition: symex_main.cpp:174
instructionst::const_iterator const_targett
Expression classes for byte-level operators.
static unsigned nondet_count
Definition: goto_symex.h:333
static unsigned dynamic_counter
Definition: goto_symex.h:334
virtual bool get_unwind(const symex_targett::sourcet &source, unsigned unwind)
Definition: symex_goto.cpp:412
void trigger_auto_object(const exprt &expr, statet &state)
virtual ~goto_symext()
Definition: goto_symex.h:62
virtual void symex_transition(statet &state, goto_programt::const_targett to, bool is_backwards_goto=false)
Definition: symex_main.cpp:23
virtual void symex_start_thread(statet &state)
void merge_value_sets(const statet::goto_statet &goto_state, statet &dest)
Definition: symex_goto.cpp:254
The symbol table.
Definition: symbol_table.h:52
virtual void symex_function_call(const goto_functionst &goto_functions, statet &state, const code_function_callt &call)
TO_BE_DOCUMENTED.
Definition: namespace.h:62
unsigned remaining_vccs
Definition: goto_symex.h:92
virtual void symex_input(statet &state, const codet &code)
A function call.
Definition: std_code.h:657
virtual void symex_end_of_function(statet &state)
do function call by inlining
virtual void symex_other(const goto_functionst &goto_functions, statet &state)
Definition: symex_other.cpp:24
void clean_expr(exprt &expr, statet &state, bool write)
goto_function_templatet< goto_programt > goto_functiont
void symex_assign_struct_member(statet &state, const member_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
goto_symex_statet statet
Definition: goto_symex.h:66
void merge_gotos(statet &state)
Definition: symex_goto.cpp:210
virtual void symex_dead(statet &state)
Definition: symex_dead.cpp:21
virtual void symex_fkt(statet &state, const code_function_callt &code)
void dereference_rec_address_of(exprt &expr, statet &state, guardt &guard)
void initialize_auto_object(const exprt &expr, statet &state)
void symex_assign_rec(statet &state, const code_assignt &code)
void add_end_of_function(exprt &code, const irep_idt &identifier)
std::vector< exprt > operandst
Definition: expr.h:49
virtual void symex_cpp_new(statet &state, const exprt &lhs, const side_effect_exprt &code)
unsigned atomic_section_counter
Definition: goto_symex.h:106
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
virtual void symex_transition(statet &state)
Definition: goto_symex.h:159
symbol_tablet & new_symbol_table
Definition: goto_symex.h:97
The main class for the forward symbolic simulator.
Definition: goto_symex.h:41
virtual void symex_function_call_code(const goto_functionst &goto_functions, statet &state, const code_function_callt &call)
do function call by inlining
virtual void symex_malloc(statet &state, const exprt &lhs, const side_effect_exprt &code)
virtual void symex_goto(statet &state)
Definition: symex_goto.cpp:21
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:101
Base class for all expressions.
Definition: expr.h:46
virtual void symex_atomic_end(statet &state)
void phi_function(const statet::goto_statet &goto_state, statet &state)
Definition: symex_goto.cpp:267
virtual void vcc(const exprt &expr, const std::string &msg, statet &state)
Definition: symex_main.cpp:53
void process_array_expr(exprt &expr)
virtual void loop_bound_exceeded(statet &state, const exprt &guard)
Definition: symex_goto.cpp:373
virtual void symex_cpp_delete(statet &state, const codet &code)
Expression to hold a symbol (variable)
Definition: std_expr.h:82
Options.
void symex_catch(statet &state)
Definition: symex_catch.cpp:14
void set_option(const std::string &option, const bool value)
Definition: options.cpp:24
A statement in a programming language.
Definition: std_code.h:19
virtual void no_body(const irep_idt &identifier)
Definition: goto_symex.h:213
virtual void symex_output(statet &state, const codet &code)
An expression containing a side effect.
Definition: std_code.h:997
void symex_throw(statet &state)
Definition: symex_throw.cpp:14
void rewrite_quantifiers(exprt &expr, statet &state)
Definition: symex_main.cpp:109
exprt address_arithmetic(const exprt &expr, statet &state, guardt &guard, bool keep_array)
Evaluate an ID_address_of expression.
unsigned total_vccs
Definition: goto_symex.h:92
TO_BE_DOCUMENTED.
goto_symext(const namespacet &_ns, symbol_tablet &_new_symbol_table, symex_targett &_target)
Definition: goto_symex.h:44
unsigned int statet
const namespacet & ns
Definition: goto_symex.h:104
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
void symex_assign_typecast(statet &state, const typecast_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
Assignment.
Definition: std_code.h:144
void pop_frame(statet &state)
pop one call frame
void symex_assign_array(statet &state, const index_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
array index operator
Definition: std_expr.h:1170
symex_targett::sourcet source