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 
16 #include <util/std_expr.h>
17 #include <util/rename.h>
18 #include <util/symbol_table.h>
19 #include <util/replace_symbol.h>
20 
21 #include <analyses/dirty.h>
22 
24  statet &state,
26  bool is_backwards_goto)
27 {
28  if(!state.call_stack().empty())
29  {
30  // initialize the loop counter of any loop we are newly entering
31  // upon this transition; we are entering a loop if
32  // 1. the transition from state.source.pc to "to" is not a backwards goto
33  // or
34  // 2. we are arriving from an outer loop
35  statet::framet &frame=state.top();
36  const goto_programt::instructiont &instruction=*to;
37  for(const auto &i_e : instruction.incoming_edges)
38  if(i_e->is_goto() && i_e->is_backwards_goto() &&
39  (!is_backwards_goto ||
40  state.source.pc->location_number>i_e->location_number))
41  frame.loop_iterations[goto_programt::loop_id(i_e)].count=0;
42  }
43 
44  state.source.pc=to;
45 }
46 
48 {
49  get_new_name(symbol, ns);
50  new_symbol_table.add(symbol);
51 }
52 
54  const exprt &vcc_expr,
55  const std::string &msg,
56  statet &state)
57 {
58  total_vccs++;
59 
60  exprt expr=vcc_expr;
61 
62  // we are willing to re-write some quantified expressions
63  rewrite_quantifiers(expr, state);
64 
65  // now rename, enables propagation
66  state.rename(expr, ns);
67 
68  // now try simplifier on it
69  do_simplify(expr);
70 
71  if(expr.is_true())
72  return;
73 
74  state.guard.guard_expr(expr);
75 
77  target.assertion(state.guard.as_expr(), expr, msg, state.source);
78 }
79 
80 void goto_symext::symex_assume(statet &state, const exprt &cond)
81 {
82  exprt simplified_cond=cond;
83 
84  do_simplify(simplified_cond);
85 
86  if(simplified_cond.is_true())
87  return;
88 
89  if(state.threads.size()==1)
90  {
91  exprt tmp=simplified_cond;
92  state.guard.guard_expr(tmp);
93  target.assumption(state.guard.as_expr(), tmp, state.source);
94  }
95  // symex_target_equationt::convert_assertions would fail to
96  // consider assumptions of threads that have a thread-id above that
97  // of the thread containing the assertion:
98  // T0 T1
99  // x=0; assume(x==1);
100  // assert(x!=42); x=42;
101  else
102  state.guard.add(simplified_cond);
103 
104  if(state.atomic_section_id!=0 &&
105  state.guard.is_false())
106  symex_atomic_end(state);
107 }
108 
110 {
111  if(expr.id()==ID_forall)
112  {
113  // forall X. P -> P
114  // we keep the quantified variable unique by means of L2 renaming
115  assert(expr.operands().size()==2);
116  assert(expr.op0().id()==ID_symbol);
117  symbol_exprt tmp0=
118  to_symbol_expr(to_ssa_expr(expr.op0()).get_original_expr());
119  symex_decl(state, tmp0);
120  exprt tmp=expr.op1();
121  expr.swap(tmp);
122  }
123 }
124 
127  statet &state,
128  const goto_functionst &goto_functions,
129  const goto_programt &goto_program)
130 {
131  assert(!goto_program.instructions.empty());
132 
133  state.source=symex_targett::sourcet(goto_program);
134  assert(!state.threads.empty());
135  assert(!state.call_stack().empty());
136  state.top().end_of_function=--goto_program.instructions.end();
137  state.top().calling_location.pc=state.top().end_of_function;
138  state.symex_target=&target;
139  state.dirty=new dirtyt(goto_functions);
140 
141  symex_transition(state, state.source.pc);
142 
143  assert(state.top().end_of_function->is_end_function());
144 
145  while(!state.call_stack().empty())
146  {
147  symex_step(goto_functions, state);
148 
149  // is there another thread to execute?
150  if(state.call_stack().empty() &&
151  state.source.thread_nr+1<state.threads.size())
152  {
153  unsigned t=state.source.thread_nr+1;
154  // std::cout << "********* Now executing thread " << t << '\n';
155  state.switch_to_thread(t);
156  symex_transition(state, state.source.pc);
157  }
158  }
159 
160  delete state.dirty;
161  state.dirty=nullptr;
162 }
163 
166  const goto_functionst &goto_functions,
167  const goto_programt &goto_program)
168 {
169  statet state;
170  operator() (state, goto_functions, goto_program);
171 }
172 
174 void goto_symext::operator()(const goto_functionst &goto_functions)
175 {
176  goto_functionst::function_mapt::const_iterator it=
177  goto_functions.function_map.find(goto_functionst::entry_point());
178 
179  if(it==goto_functions.function_map.end())
180  throw "the program has no entry point";
181 
182  const goto_programt &body=it->second.body;
183 
184  operator()(goto_functions, body);
185 }
186 
189  const goto_functionst &goto_functions,
190  statet &state)
191 {
192  #if 0
193  std::cout << "\ninstruction type is " << state.source.pc->type << '\n';
194  std::cout << "Location: " << state.source.pc->source_location << '\n';
195  std::cout << "Guard: " << from_expr(ns, "", state.guard.as_expr()) << '\n';
196  std::cout << "Code: " << from_expr(ns, "", state.source.pc->code) << '\n';
197  #endif
198 
199  assert(!state.threads.empty());
200  assert(!state.call_stack().empty());
201 
202  const goto_programt::instructiont &instruction=*state.source.pc;
203 
204  merge_gotos(state);
205 
206  // depth exceeded?
207  {
208  unsigned max_depth=options.get_unsigned_int_option("depth");
209  if(max_depth!=0 && state.depth>max_depth)
210  state.guard.add(false_exprt());
211  state.depth++;
212  }
213 
214  // actually do instruction
215  switch(instruction.type)
216  {
217  case SKIP:
218  if(!state.guard.is_false())
219  target.location(state.guard.as_expr(), state.source);
220  symex_transition(state);
221  break;
222 
223  case END_FUNCTION:
224  // do even if state.guard.is_false() to clear out frame created
225  // in symex_start_thread
226  symex_end_of_function(state);
227  symex_transition(state);
228  break;
229 
230  case LOCATION:
231  if(!state.guard.is_false())
232  target.location(state.guard.as_expr(), state.source);
233  symex_transition(state);
234  break;
235 
236  case GOTO:
237  symex_goto(state);
238  break;
239 
240  case ASSUME:
241  if(!state.guard.is_false())
242  {
243  exprt tmp=instruction.guard;
244  clean_expr(tmp, state, false);
245  state.rename(tmp, ns);
246  symex_assume(state, tmp);
247  }
248 
249  symex_transition(state);
250  break;
251 
252  case ASSERT:
253  if(!state.guard.is_false())
254  {
255  std::string msg=id2string(state.source.pc->source_location.get_comment());
256  if(msg=="")
257  msg="assertion";
258  exprt tmp(instruction.guard);
259  clean_expr(tmp, state, false);
260  vcc(tmp, msg, state);
261  }
262 
263  symex_transition(state);
264  break;
265 
266  case RETURN:
267  if(!state.guard.is_false())
268  return_assignment(state);
269 
270  symex_transition(state);
271  break;
272 
273  case ASSIGN:
274  if(!state.guard.is_false())
275  symex_assign_rec(state, to_code_assign(instruction.code));
276 
277  symex_transition(state);
278  break;
279 
280  case FUNCTION_CALL:
281  if(!state.guard.is_false())
282  {
283  code_function_callt deref_code=
284  to_code_function_call(instruction.code);
285 
286  if(deref_code.lhs().is_not_nil())
287  clean_expr(deref_code.lhs(), state, true);
288 
289  clean_expr(deref_code.function(), state, false);
290 
291  Forall_expr(it, deref_code.arguments())
292  clean_expr(*it, state, false);
293 
294  symex_function_call(goto_functions, state, deref_code);
295  }
296  else
297  symex_transition(state);
298  break;
299 
300  case OTHER:
301  if(!state.guard.is_false())
302  symex_other(goto_functions, state);
303 
304  symex_transition(state);
305  break;
306 
307  case DECL:
308  if(!state.guard.is_false())
309  symex_decl(state);
310 
311  symex_transition(state);
312  break;
313 
314  case DEAD:
315  symex_dead(state);
316  symex_transition(state);
317  break;
318 
319  case START_THREAD:
320  symex_start_thread(state);
321  symex_transition(state);
322  break;
323 
324  case END_THREAD:
325  // behaves like assume(0);
326  if(!state.guard.is_false())
327  state.guard.add(false_exprt());
328  symex_transition(state);
329  break;
330 
331  case ATOMIC_BEGIN:
332  symex_atomic_begin(state);
333  symex_transition(state);
334  break;
335 
336  case ATOMIC_END:
337  symex_atomic_end(state);
338  symex_transition(state);
339  break;
340 
341  case CATCH:
342  symex_catch(state);
343  symex_transition(state);
344  break;
345 
346  case THROW:
347  symex_throw(state);
348  symex_transition(state);
349  break;
350 
351  case NO_INSTRUCTION_TYPE:
352  throw "symex got NO_INSTRUCTION";
353 
354  default:
355  throw "symex got unexpected instruction";
356  }
357 }
virtual void do_simplify(exprt &expr)
Definition: goto_symex.cpp:19
exprt as_expr() const
Definition: guard.h:43
virtual void symex_atomic_begin(statet &state)
symex_targett & target
Definition: goto_symex.h:105
static irep_idt loop_id(const_targett target)
Human-readable loop name.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
virtual void location(const exprt &guard, const sourcet &source)=0
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 guard_expr(exprt &dest) const
Definition: guard.cpp:19
void new_name(symbolt &symbol)
Definition: symex_main.cpp:47
exprt & op0()
Definition: expr.h:84
unsigned int get_unsigned_int_option(const std::string &option) const
Definition: options.cpp:54
Variables whose address is taken.
instructionst instructions
The list of instructions in the goto program.
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
virtual void symex_decl(statet &state)
Definition: symex_decl.cpp:23
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
bool is_false() const
Definition: expr.cpp:140
symex_targett * symex_target
bool is_true() const
Definition: expr.cpp:133
optionst options
Definition: goto_symex.h:96
loop_iterationst loop_iterations
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
void switch_to_thread(unsigned t)
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:178
const irep_idt & id() const
Definition: irep.h:189
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
argumentst & arguments()
Definition: std_code.h:689
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:150
#define Forall_expr(it, expr)
Definition: expr.h:32
Symbolic Execution.
virtual void symex_transition(statet &state, goto_programt::const_targett to, bool is_backwards_goto=false)
Definition: symex_main.cpp:23
API to expression classes.
virtual void symex_start_thread(statet &state)
exprt & op1()
Definition: expr.h:87
virtual void symex_function_call(const goto_functionst &goto_functions, statet &state, const code_function_callt &call)
virtual void assertion(const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)=0
unsigned remaining_vccs
Definition: goto_symex.h:92
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
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
void clean_expr(exprt &expr, statet &state, bool write)
Symbol table.
void merge_gotos(statet &state)
Definition: symex_goto.cpp:210
virtual void symex_dead(statet &state)
Definition: symex_dead.cpp:21
The boolean constant false.
Definition: std_expr.h:3753
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)=0
void symex_assign_rec(statet &state, const code_assignt &code)
const dirtyt * dirty
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
symbol_tablet & new_symbol_table
Definition: goto_symex.h:97
virtual void symex_goto(statet &state)
Definition: symex_goto.cpp:21
exprt & function()
Definition: std_code.h:677
Base class for all expressions.
Definition: expr.h:46
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
call_stackt & call_stack()
virtual void symex_atomic_end(statet &state)
Definition: dirty.h:22
virtual void vcc(const exprt &expr, const std::string &msg, statet &state)
Definition: symex_main.cpp:53
void swap(irept &irep)
Definition: irep.h:231
symex_targett::sourcet calling_location
Expression to hold a symbol (variable)
Definition: std_expr.h:82
void symex_catch(statet &state)
Definition: symex_catch.cpp:14
void symex_throw(statet &state)
Definition: symex_throw.cpp:14
void rewrite_quantifiers(exprt &expr, statet &state)
Definition: symex_main.cpp:109
operandst & operands()
Definition: expr.h:70
unsigned total_vccs
Definition: goto_symex.h:92
void get_new_name(symbolt &symbol, const namespacet &ns)
automated variable renaming
Definition: rename.cpp:20
const namespacet & ns
Definition: goto_symex.h:104
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:700
symex_targett::sourcet source