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 std::list<exprt> &exprs)
37 {
38  // collect dependencies
39  for(const auto &expr : exprs)
40  get_symbols(expr);
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 
108  UNREACHABLE;
109  }
110 }
111 
113 {
114  PRECONDITION(SSA_step.ssa_lhs.id() == ID_symbol);
115  const irep_idt &id=SSA_step.ssa_lhs.get_identifier();
116 
117  if(depends.find(id)==depends.end())
118  {
119  // we don't really need it
120  SSA_step.ignore=true;
121  }
122  else
123  get_symbols(SSA_step.ssa_rhs);
124 }
125 
127 {
128  const irep_idt &id = to_symbol_expr(SSA_step.ssa_lhs).get_identifier();
129 
130  if(depends.find(id)==depends.end())
131  {
132  // we don't really need it
133  SSA_step.ignore=true;
134  }
135 }
136 
143  const symex_target_equationt &equation,
144  symbol_sett &open_variables)
145 {
146  symbol_sett lhs;
147 
148  for(symex_target_equationt::SSA_stepst::const_iterator
149  it=equation.SSA_steps.begin();
150  it!=equation.SSA_steps.end();
151  it++)
152  {
153  const SSA_stept &SSA_step = *it;
154 
155  get_symbols(SSA_step.guard);
156 
157  switch(SSA_step.type)
158  {
160  get_symbols(SSA_step.cond_expr);
161  break;
162 
164  get_symbols(SSA_step.cond_expr);
165  break;
166 
168  // ignore
169  break;
170 
172  get_symbols(SSA_step.ssa_rhs);
173  lhs.insert(SSA_step.ssa_lhs.get_identifier());
174  break;
175 
180  break;
181 
192  // ignore for now
193  break;
194 
196  UNREACHABLE;
197  }
198  }
199 
200  open_variables=depends;
201 
202  // remove the ones that are defined
203  open_variables.erase(lhs.begin(), lhs.end());
204 }
205 
207 {
208  symex_slicet symex_slice;
209  symex_slice.slice(equation);
210 }
211 
218  const symex_target_equationt &equation,
219  symbol_sett &open_variables)
220 {
221  symex_slicet symex_slice;
222  symex_slice.collect_open_variables(equation, open_variables);
223 }
224 
229 void slice(
230  symex_target_equationt &equation,
231  const std::list<exprt> &expressions)
232 {
233  symex_slicet symex_slice;
234  symex_slice.slice(equation, expressions);
235 }
236 
238 {
239  // just find the last assertion
240  symex_target_equationt::SSA_stepst::iterator
241  last_assertion=equation.SSA_steps.end();
242 
243  for(symex_target_equationt::SSA_stepst::iterator
244  it=equation.SSA_steps.begin();
245  it!=equation.SSA_steps.end();
246  it++)
247  if(it->is_assert())
248  last_assertion=it;
249 
250  // slice away anything after it
251 
252  symex_target_equationt::SSA_stepst::iterator s_it=
253  last_assertion;
254 
255  if(s_it!=equation.SSA_steps.end())
256  {
257  for(s_it++;
258  s_it!=equation.SSA_steps.end();
259  s_it++)
260  s_it->ignore=true;
261  }
262 }
263 
265 {
266  // set ignore to false
267  for(auto &step : equation.SSA_steps)
268  {
269  step.ignore = false;
270  }
271 }
Single SSA step in the equation.
Definition: ssa_step.h:45
bool ignore
Definition: ssa_step.h:172
exprt cond_expr
Definition: ssa_step.h:147
goto_trace_stept::typet type
Definition: ssa_step.h:48
exprt guard
Definition: ssa_step.h:137
exprt ssa_rhs
Definition: ssa_step.h:143
ssa_exprt ssa_lhs
Definition: ssa_step.h:141
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
const irep_idt & id() const
Definition: irep.h:407
const irep_idt & get_identifier() const
Definition: std_expr.h:110
void get_symbols(const exprt &expr)
Definition: slice.cpp:18
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:142
symbol_sett depends
void slice(symex_target_equationt &equation)
Definition: slice.cpp:45
void slice_decl(SSA_stept &SSA_step)
Definition: slice.cpp:126
void slice_assignment(SSA_stept &SSA_step)
Definition: slice.cpp:112
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
The type of an expression, extends irept.
Definition: type.h:28
#define forall_operands(it, expr)
Definition: expr.h:18
void revert_slice(symex_target_equationt &equation)
Undo whatever has been done by slice
Definition: slice.cpp:264
void slice(symex_target_equationt &equation)
Definition: slice.cpp:206
void simple_slice(symex_target_equationt &equation)
Definition: slice.cpp:237
void collect_open_variables(const symex_target_equationt &equation, symbol_sett &open_variables)
Collect the open variables, i.e.
Definition: slice.cpp:217
Slicer for symex traces.
std::unordered_set< irep_idt > symbol_sett
Definition: slice.h:35
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
Slicer for symex traces.