cprover
symex_goto.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 #include <algorithm>
16 
17 #include <util/std_expr.h>
18 
19 #include <analyses/dirty.h>
20 
22 {
23  const goto_programt::instructiont &instruction=*state.source.pc;
24  statet::framet &frame=state.top();
25 
26  exprt old_guard=instruction.guard;
27  clean_expr(old_guard, state, false);
28 
29  exprt new_guard=old_guard;
30  state.rename(new_guard, ns);
31  do_simplify(new_guard);
32 
33  if(new_guard.is_false() ||
34  state.guard.is_false())
35  {
36  if(!state.guard.is_false())
37  target.location(state.guard.as_expr(), state.source);
38 
39  // next instruction
40  symex_transition(state);
41  return; // nothing to do
42  }
43 
44  target.goto_instruction(state.guard.as_expr(), new_guard, state.source);
45 
46  assert(!instruction.targets.empty());
47 
48  // we only do deterministic gotos for now
49  if(instruction.targets.size()!=1)
50  throw "no support for non-deterministic gotos";
51 
52  goto_programt::const_targett goto_target=
53  instruction.get_target();
54 
55  bool forward=!instruction.is_backwards_goto();
56 
57  if(!forward) // backwards?
58  {
59  // is it label: goto label; or while(cond); - popular in SV-COMP
60  if(goto_target==state.source.pc ||
61  (instruction.incoming_edges.size()==1 &&
62  *instruction.incoming_edges.begin()==goto_target))
63  {
64  // generate assume(false) or a suitable negation if this
65  // instruction is a conditional goto
66  exprt negated_cond;
67 
68  if(new_guard.is_true())
69  negated_cond=false_exprt();
70  else
71  negated_cond=not_exprt(new_guard);
72 
73  symex_assume(state, negated_cond);
74 
75  // next instruction
76  symex_transition(state);
77  return;
78  }
79 
80  unsigned &unwind=
81  frame.loop_iterations[goto_programt::loop_id(state.source.pc)].count;
82  unwind++;
83 
84  // continue unwinding?
85  if(get_unwind(state.source, unwind))
86  {
87  // no!
88  loop_bound_exceeded(state, new_guard);
89 
90  // next instruction
91  symex_transition(state);
92  return;
93  }
94 
95  if(new_guard.is_true())
96  {
97  symex_transition(state, goto_target, true);
98  return; // nothing else to do
99  }
100  }
101 
102  goto_programt::const_targett new_state_pc, state_pc;
103  symex_targett::sourcet original_source=state.source;
104 
105  if(forward)
106  {
107  new_state_pc=goto_target;
108  state_pc=state.source.pc;
109  state_pc++;
110 
111  // skip dead instructions
112  if(new_guard.is_true())
113  while(state_pc!=goto_target && !state_pc->is_target())
114  ++state_pc;
115 
116  if(state_pc==goto_target)
117  {
118  symex_transition(state, goto_target);
119  return; // nothing else to do
120  }
121  }
122  else
123  {
124  new_state_pc=state.source.pc;
125  new_state_pc++;
126  state_pc=goto_target;
127  }
128 
129  // put into state-queue
130  statet::goto_state_listt &goto_state_list=
131  state.top().goto_state_map[new_state_pc];
132 
133  goto_state_list.push_back(statet::goto_statet(state));
134  statet::goto_statet &new_state=goto_state_list.back();
135 
136  symex_transition(state, state_pc, !forward);
137 
138  // adjust guards
139  if(new_guard.is_true())
140  {
141  state.guard.make_false();
142  }
143  else
144  {
145  // produce new guard symbol
146  exprt guard_expr;
147 
148  if(new_guard.id()==ID_symbol ||
149  (new_guard.id()==ID_not &&
150  new_guard.operands().size()==1 &&
151  new_guard.op0().id()==ID_symbol))
152  guard_expr=new_guard;
153  else
154  {
155  symbol_exprt guard_symbol_expr=
157  exprt new_rhs=new_guard;
158  new_rhs.make_not();
159 
160  ssa_exprt new_lhs(guard_symbol_expr);
161  state.rename(new_lhs, ns, goto_symex_statet::L1);
162  state.assignment(new_lhs, new_rhs, ns, true, false);
163 
164  guardt guard;
165 
167  guard.as_expr(),
168  new_lhs, new_lhs, guard_symbol_expr,
169  new_rhs,
170  original_source,
172 
173  guard_expr=guard_symbol_expr;
174  guard_expr.make_not();
175  state.rename(guard_expr, ns);
176  }
177 
178  if(forward)
179  {
180  new_state.guard.add(guard_expr);
181  guard_expr.make_not();
182  state.guard.add(guard_expr);
183  }
184  else
185  {
186  state.guard.add(guard_expr);
187  guard_expr.make_not();
188  new_state.guard.add(guard_expr);
189  }
190  }
191 }
192 
193 void goto_symext::symex_step_goto(statet &state, bool taken)
194 {
195  const goto_programt::instructiont &instruction=*state.source.pc;
196 
197  exprt guard(instruction.guard);
198  dereference(guard, state, false);
199  state.rename(guard, ns);
200 
201  if(!taken)
202  guard.make_not();
203 
204  state.guard.guard_expr(guard);
205  do_simplify(guard);
206 
207  target.assumption(state.guard.as_expr(), guard, state.source);
208 }
209 
211 {
212  statet::framet &frame=state.top();
213 
214  // first, see if this is a target at all
215  statet::goto_state_mapt::iterator state_map_it=
216  frame.goto_state_map.find(state.source.pc);
217 
218  if(state_map_it==frame.goto_state_map.end())
219  return; // nothing to do
220 
221  // we need to merge
222  statet::goto_state_listt &state_list=state_map_it->second;
223 
224  for(statet::goto_state_listt::reverse_iterator
225  list_it=state_list.rbegin();
226  list_it!=state_list.rend();
227  list_it++)
228  merge_goto(*list_it, state);
229 
230  // clean up to save some memory
231  frame.goto_state_map.erase(state_map_it);
232 }
233 
235  const statet::goto_statet &goto_state,
236  statet &state)
237 {
238  // check atomic section
239  if(state.atomic_section_id!=goto_state.atomic_section_id)
240  throw "atomic sections differ across branches";
241 
242  // do SSA phi functions
243  phi_function(goto_state, state);
244 
245  merge_value_sets(goto_state, state);
246 
247  // adjust guard
248  state.guard|=goto_state.guard;
249 
250  // adjust depth
251  state.depth=std::min(state.depth, goto_state.depth);
252 }
253 
255  const statet::goto_statet &src,
256  statet &dest)
257 {
258  if(dest.guard.is_false())
259  {
260  dest.value_set=src.value_set;
261  return;
262  }
263 
264  dest.value_set.make_union(src.value_set);
265 }
266 
268  const statet::goto_statet &goto_state,
269  statet &dest_state)
270 {
271  // go over all variables to see what changed
272  std::unordered_set<ssa_exprt, irep_hash> variables;
273 
274  goto_state.level2_get_variables(variables);
275  dest_state.level2.get_variables(variables);
276 
277  guardt diff_guard;
278 
279  if(!variables.empty())
280  {
281  diff_guard=goto_state.guard;
282 
283  // this gets the diff between the guards
284  diff_guard-=dest_state.guard;
285  }
286 
287  for(std::unordered_set<ssa_exprt, irep_hash>::const_iterator
288  it=variables.begin();
289  it!=variables.end();
290  it++)
291  {
292  const irep_idt l1_identifier=it->get_identifier();
293  const irep_idt &obj_identifier=it->get_object_name();
294 
295  if(obj_identifier==guard_identifier)
296  continue; // just a guard, don't bother
297 
298  if(goto_state.level2_current_count(l1_identifier)==
299  dest_state.level2.current_count(l1_identifier))
300  continue; // not at all changed
301 
302  // changed!
303 
304  // shared variables are renamed on every access anyway, we don't need to
305  // merge anything
306  const symbolt &symbol=ns.lookup(obj_identifier);
307 
308  // shared?
309  if(dest_state.atomic_section_id==0 &&
310  dest_state.threads.size()>=2 &&
311  (symbol.is_shared() || (*dest_state.dirty)(symbol.name)))
312  continue; // no phi nodes for shared stuff
313 
314  // don't merge (thread-)locals across different threads, which
315  // may have been introduced by symex_start_thread (and will
316  // only later be removed from level2.current_names by pop_frame
317  // once the thread is executed)
318  if(!it->get_level_0().empty() &&
319  it->get_level_0()!=std::to_string(dest_state.source.thread_nr))
320  continue;
321 
322  exprt goto_state_rhs=*it, dest_state_rhs=*it;
323 
324  {
325  goto_symex_statet::propagationt::valuest::const_iterator p_it=
326  goto_state.propagation.values.find(l1_identifier);
327 
328  if(p_it!=goto_state.propagation.values.end())
329  goto_state_rhs=p_it->second;
330  else
331  to_ssa_expr(goto_state_rhs).set_level_2(
332  goto_state.level2_current_count(l1_identifier));
333  }
334 
335  {
336  goto_symex_statet::propagationt::valuest::const_iterator p_it=
337  dest_state.propagation.values.find(l1_identifier);
338 
339  if(p_it!=dest_state.propagation.values.end())
340  dest_state_rhs=p_it->second;
341  else
342  to_ssa_expr(dest_state_rhs).set_level_2(
343  dest_state.level2.current_count(l1_identifier));
344  }
345 
346  exprt rhs;
347 
348  if(dest_state.guard.is_false())
349  rhs=goto_state_rhs;
350  else if(goto_state.guard.is_false())
351  rhs=dest_state_rhs;
352  else
353  {
354  rhs=if_exprt(diff_guard.as_expr(), goto_state_rhs, dest_state_rhs);
355  do_simplify(rhs);
356  }
357 
358  ssa_exprt new_lhs=*it;
359  const bool record_events=dest_state.record_events;
360  dest_state.record_events=false;
361  dest_state.assignment(new_lhs, rhs, ns, true, true);
362  dest_state.record_events=record_events;
363 
365  true_exprt(),
366  new_lhs, new_lhs, new_lhs.get_original_expr(),
367  rhs,
368  dest_state.source,
370  }
371 }
372 
374  statet &state,
375  const exprt &guard)
376 {
377  const unsigned loop_number=state.source.pc->loop_number;
378 
379  exprt negated_cond;
380 
381  if(guard.is_true())
382  negated_cond=false_exprt();
383  else
384  negated_cond=not_exprt(guard);
385 
386  bool unwinding_assertions=
387  options.get_bool_option("unwinding-assertions");
388 
389  bool partial_loops=
390  options.get_bool_option("partial-loops");
391 
392  if(!partial_loops)
393  {
394  if(unwinding_assertions)
395  {
396  // Generate VCC for unwinding assertion.
397  vcc(negated_cond,
398  "unwinding assertion loop "+std::to_string(loop_number),
399  state);
400 
401  // add to state guard to prevent further assignments
402  state.guard.add(negated_cond);
403  }
404  else
405  {
406  // generate unwinding assumption, unless we permit partial loops
407  symex_assume(state, negated_cond);
408  }
409  }
410 }
411 
413  const symex_targett::sourcet &source,
414  unsigned unwind)
415 {
416  // by default, we keep going
417  return false;
418 }
virtual void do_simplify(exprt &expr)
Definition: goto_symex.cpp:19
irep_idt name
The unique identifier.
Definition: symbol.h:46
exprt as_expr() const
Definition: guard.h:43
Boolean negation.
Definition: std_expr.h:2648
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
virtual void symex_step_goto(statet &state, bool taken)
Definition: symex_goto.cpp:193
symex_targett & target
Definition: goto_symex.h:105
bool is_shared() const
Definition: symbol.h:103
irep_idt guard_identifier
Definition: goto_symex.h:152
static irep_idt loop_id(const_targett target)
Human-readable loop name.
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 level2_get_variables(std::unordered_set< ssa_exprt, irep_hash > &vars) const
class goto_symex_statet::propagationt propagation
virtual void merge_goto(const statet::goto_statet &goto_state, statet &state)
Definition: symex_goto.cpp:234
exprt & op0()
Definition: expr.h:84
Variables whose address is taken.
virtual void dereference(exprt &expr, statet &state, const bool write)
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
bool make_union(object_mapt &dest, const object_mapt &src) const
Definition: value_set.cpp:246
bool is_false() const
Definition: expr.cpp:140
The trinary if-then-else operator.
Definition: std_expr.h:2771
bool is_true() const
Definition: expr.cpp:133
optionst options
Definition: goto_symex.h:96
Definition: guard.h:19
loop_iterationst loop_iterations
The proper Booleans.
Definition: std_types.h:33
void set_level_2(unsigned i)
Definition: ssa_expr.h:95
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
void get_variables(std::unordered_set< ssa_exprt, irep_hash > &vars) const
unsigned level2_current_count(const irep_idt &identifier) const
goto_symex_statet::level2t level2
const irep_idt & id() const
Definition: irep.h:189
instructionst::const_iterator const_targett
The boolean constant true.
Definition: std_expr.h:3742
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:150
Symbolic Execution.
virtual bool get_unwind(const symex_targett::sourcet &source, unsigned unwind)
Definition: symex_goto.cpp:412
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.
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
void merge_value_sets(const statet::goto_statet &goto_state, statet &dest)
Definition: symex_goto.cpp:254
goto_state_mapt goto_state_map
void clean_expr(exprt &expr, statet &state, bool write)
void merge_gotos(statet &state)
Definition: symex_goto.cpp:210
The boolean constant false.
Definition: std_expr.h:3753
virtual void goto_instruction(const exprt &guard, const exprt &cond, const sourcet &source)=0
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)=0
const dirtyt * dirty
virtual void assignment(const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &ssa_full_lhs, const exprt &original_full_lhs, const exprt &ssa_rhs, const sourcet &source, assignment_typet assignment_type)=0
void make_not()
Definition: expr.cpp:100
virtual void symex_goto(statet &state)
Definition: symex_goto.cpp:21
unsigned current_count(const irep_idt &identifier) const
Base class for all expressions.
Definition: expr.h:46
void make_false()
Definition: expr.cpp:159
void assignment(ssa_exprt &lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value)
const exprt & get_original_expr() const
Definition: ssa_expr.h:41
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
virtual void loop_bound_exceeded(statet &state, const exprt &guard)
Definition: symex_goto.cpp:373
Expression to hold a symbol (variable)
Definition: std_expr.h:82
std::list< goto_statet > goto_state_listt
operandst & operands()
Definition: expr.h:70
const namespacet & ns
Definition: goto_symex.h:104
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
void add(const exprt &expr)
Definition: guard.cpp:64
symex_targett::sourcet source