cprover
slice.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Slicer for symex traces
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "slice.h"
13 
14 #include <util/std_expr.h>
15 
16 #include "symex_slice_class.h"
17 
19 {
20  get_symbols(expr.type());
21 
22  forall_operands(it, expr)
23  get_symbols(*it);
24 
25  if(expr.id()==ID_symbol)
26  depends.insert(to_symbol_expr(expr).get_identifier());
27 }
28 
30 {
31  // TODO
32 }
33 
35  symex_target_equationt &equation,
36  const expr_listt &exprs)
37 {
38  // collect dependencies
39  forall_expr_list(expr_it, exprs)
40  get_symbols(*expr_it);
41 
42  slice(equation);
43 }
44 
46 {
47  for(symex_target_equationt::SSA_stepst::reverse_iterator
48  it=equation.SSA_steps.rbegin();
49  it!=equation.SSA_steps.rend();
50  it++)
51  slice(*it);
52 }
53 
55 {
56  get_symbols(SSA_step.guard);
57 
58  switch(SSA_step.type)
59  {
61  get_symbols(SSA_step.cond_expr);
62  break;
63 
65  get_symbols(SSA_step.cond_expr);
66  break;
67 
69  get_symbols(SSA_step.cond_expr);
70  break;
71 
73  // ignore
74  break;
75 
77  slice_assignment(SSA_step);
78  break;
79 
81  slice_decl(SSA_step);
82  break;
83 
86  break;
87 
89  // ignore for now
90  break;
91 
99  // ignore for now
100  break;
101 
104  // ignore for now
105  break;
106 
107  default:
108  assert(false);
109  }
110 }
111 
114 {
115  assert(SSA_step.ssa_lhs.id()==ID_symbol);
116  const irep_idt &id=SSA_step.ssa_lhs.get_identifier();
117 
118  if(depends.find(id)==depends.end())
119  {
120  // we don't really need it
121  SSA_step.ignore=true;
122  }
123  else
124  get_symbols(SSA_step.ssa_rhs);
125 }
126 
129 {
130  assert(SSA_step.ssa_lhs.id()==ID_symbol);
131  const irep_idt &id=SSA_step.ssa_lhs.get_identifier();
132 
133  if(depends.find(id)==depends.end())
134  {
135  // we don't really need it
136  SSA_step.ignore=true;
137  }
138 }
139 
146  const symex_target_equationt &equation,
147  symbol_sett &open_variables)
148 {
149  symbol_sett lhs;
150 
151  for(symex_target_equationt::SSA_stepst::const_iterator
152  it=equation.SSA_steps.begin();
153  it!=equation.SSA_steps.end();
154  it++)
155  {
156  const symex_target_equationt::SSA_stept &SSA_step=*it;
157 
158  get_symbols(SSA_step.guard);
159 
160  switch(SSA_step.type)
161  {
163  get_symbols(SSA_step.cond_expr);
164  break;
165 
167  get_symbols(SSA_step.cond_expr);
168  break;
169 
171  // ignore
172  break;
173 
175  get_symbols(SSA_step.ssa_rhs);
176  lhs.insert(SSA_step.ssa_lhs.get_identifier());
177  break;
178 
183  break;
184 
195  // ignore for now
196  break;
197 
198  default:
199  assert(false);
200  }
201  }
202 
203  open_variables=depends;
204 
205  // remove the ones that are defined
206  open_variables.erase(lhs.begin(), lhs.end());
207 }
208 
210 {
211  symex_slicet symex_slice;
212  symex_slice.slice(equation);
213 }
214 
221  const symex_target_equationt &equation,
222  symbol_sett &open_variables)
223 {
224  symex_slicet symex_slice;
225  symex_slice.collect_open_variables(equation, open_variables);
226 }
227 
233  const expr_listt &expressions)
234 {
235  symex_slicet symex_slice;
236  symex_slice.slice(equation, expressions);
237 }
238 
240 {
241  // just find the last assertion
242  symex_target_equationt::SSA_stepst::iterator
243  last_assertion=equation.SSA_steps.end();
244 
245  for(symex_target_equationt::SSA_stepst::iterator
246  it=equation.SSA_steps.begin();
247  it!=equation.SSA_steps.end();
248  it++)
249  if(it->is_assert())
250  last_assertion=it;
251 
252  // slice away anything after it
253 
254  symex_target_equationt::SSA_stepst::iterator s_it=
255  last_assertion;
256 
257  if(s_it!=equation.SSA_steps.end())
258  {
259  for(s_it++;
260  s_it!=equation.SSA_steps.end();
261  s_it++)
262  s_it->ignore=true;
263  }
264 }
The type of an expression.
Definition: type.h:20
void slice(symex_target_equationt &equation)
Definition: slice.cpp:209
void simple_slice(symex_target_equationt &equation)
Definition: slice.cpp:239
const irep_idt & get_identifier() const
Definition: std_expr.h:120
typet & type()
Definition: expr.h:60
symbol_sett depends
const irep_idt & id() const
Definition: irep.h:189
void slice_assignment(symex_target_equationt::SSA_stept &SSA_step)
Definition: slice.cpp:112
std::unordered_set< irep_idt, irep_id_hash > symbol_sett
Definition: slice.h:29
void get_symbols(const exprt &expr)
Definition: slice.cpp:18
API to expression classes.
#define forall_operands(it, expr)
Definition: expr.h:17
std::list< exprt > expr_listt
Definition: expr.h:166
#define forall_expr_list(it, expr)
Definition: expr.h:36
void collect_open_variables(const symex_target_equationt &equation, symbol_sett &open_variables)
Collect the open variables, i.e., variables that are used in RHS but never written in LHS...
Definition: slice.cpp:145
Base class for all expressions.
Definition: expr.h:46
Slicer for symex traces.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
void slice(symex_target_equationt &equation)
Definition: slice.cpp:45
void collect_open_variables(const symex_target_equationt &equation, symbol_sett &open_variables)
Collect the open variables, i.e.
Definition: slice.cpp:220
void slice_decl(symex_target_equationt::SSA_stept &SSA_step)
Definition: slice.cpp:127
Slicer for symex traces.