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 
142  const symex_target_equationt &equation,
143  symbol_sett &open_variables)
144 {
145  symbol_sett lhs;
146 
147  for(symex_target_equationt::SSA_stepst::const_iterator
148  it=equation.SSA_steps.begin();
149  it!=equation.SSA_steps.end();
150  it++)
151  {
152  const SSA_stept &SSA_step = *it;
153 
154  get_symbols(SSA_step.guard);
155 
156  switch(SSA_step.type)
157  {
159  get_symbols(SSA_step.cond_expr);
160  break;
161 
163  get_symbols(SSA_step.cond_expr);
164  break;
165 
167  // ignore
168  break;
169 
171  get_symbols(SSA_step.ssa_rhs);
172  lhs.insert(SSA_step.ssa_lhs.get_identifier());
173  break;
174 
179  break;
180 
191  // ignore for now
192  break;
193 
195  UNREACHABLE;
196  }
197  }
198 
199  open_variables=depends;
200 
201  // remove the ones that are defined
202  open_variables.erase(lhs.begin(), lhs.end());
203 }
204 
206 {
207  symex_slicet symex_slice;
208  symex_slice.slice(equation);
209 }
210 
216  const symex_target_equationt &equation,
217  symbol_sett &open_variables)
218 {
219  symex_slicet symex_slice;
220  symex_slice.collect_open_variables(equation, open_variables);
221 }
222 
226 void slice(
227  symex_target_equationt &equation,
228  const std::list<exprt> &expressions)
229 {
230  symex_slicet symex_slice;
231  symex_slice.slice(equation, expressions);
232 }
233 
235 {
236  // just find the last assertion
237  symex_target_equationt::SSA_stepst::iterator
238  last_assertion=equation.SSA_steps.end();
239 
240  for(symex_target_equationt::SSA_stepst::iterator
241  it=equation.SSA_steps.begin();
242  it!=equation.SSA_steps.end();
243  it++)
244  if(it->is_assert())
245  last_assertion=it;
246 
247  // slice away anything after it
248 
249  symex_target_equationt::SSA_stepst::iterator s_it=
250  last_assertion;
251 
252  if(s_it!=equation.SSA_steps.end())
253  {
254  for(s_it++;
255  s_it!=equation.SSA_steps.end();
256  s_it++)
257  s_it->ignore=true;
258  }
259 }
260 
262 {
263  // set ignore to false
264  for(auto &step : equation.SSA_steps)
265  {
266  step.ignore = false;
267  }
268 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symex_slice_class.h
Slicer for symex traces.
goto_trace_stept::typet::LOCATION
@ LOCATION
goto_trace_stept::typet::ASSUME
@ ASSUME
symex_slicet::slice_decl
void slice_decl(SSA_stept &SSA_step)
Definition: slice.cpp:126
typet
The type of an expression, extends irept.
Definition: type.h:28
SSA_stept
Single SSA step in the equation.
Definition: ssa_step.h:45
symex_slicet
Definition: symex_slice_class.h:19
exprt
Base class for all expressions.
Definition: expr.h:54
simple_slice
void simple_slice(symex_target_equationt &equation)
Definition: slice.cpp:234
SSA_stept::guard
exprt guard
Definition: ssa_step.h:137
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
goto_trace_stept::typet::OUTPUT
@ OUTPUT
goto_trace_stept::typet::FUNCTION_RETURN
@ FUNCTION_RETURN
goto_trace_stept::typet::DECL
@ DECL
SSA_stept::ssa_lhs
ssa_exprt ssa_lhs
Definition: ssa_step.h:141
goto_trace_stept::typet::ASSERT
@ ASSERT
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
goto_trace_stept::typet::NONE
@ NONE
SSA_stept::cond_expr
exprt cond_expr
Definition: ssa_step.h:147
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
symex_slicet::slice
void slice(symex_target_equationt &equation)
Definition: slice.cpp:45
revert_slice
void revert_slice(symex_target_equationt &equation)
Undo whatever has been done by slice
Definition: slice.cpp:261
goto_trace_stept::typet::ASSIGNMENT
@ ASSIGNMENT
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
irept::id
const irep_idt & id() const
Definition: irep.h:407
goto_trace_stept::typet::INPUT
@ INPUT
goto_trace_stept::typet::ATOMIC_END
@ ATOMIC_END
SSA_stept::ignore
bool ignore
Definition: ssa_step.h:172
goto_trace_stept::typet::SPAWN
@ SPAWN
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: symex_target_equation.h:41
symex_slicet::collect_open_variables
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:141
goto_trace_stept::typet::MEMORY_BARRIER
@ MEMORY_BARRIER
goto_trace_stept::typet::SHARED_WRITE
@ SHARED_WRITE
symbol_sett
std::unordered_set< irep_idt > symbol_sett
Definition: slice.h:35
goto_trace_stept::typet::GOTO
@ GOTO
symex_slicet::depends
symbol_sett depends
Definition: symex_slice_class.h:30
collect_open_variables
void collect_open_variables(const symex_target_equationt &equation, symbol_sett &open_variables)
Collect the open variables, i.e.
Definition: slice.cpp:215
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:257
SSA_stept::type
goto_trace_stept::typet type
Definition: ssa_step.h:48
SSA_stept::ssa_rhs
exprt ssa_rhs
Definition: ssa_step.h:143
goto_trace_stept::typet::ATOMIC_BEGIN
@ ATOMIC_BEGIN
goto_trace_stept::typet::SHARED_READ
@ SHARED_READ
goto_trace_stept::typet::FUNCTION_CALL
@ FUNCTION_CALL
symex_slicet::get_symbols
void get_symbols(const exprt &expr)
Definition: slice.cpp:18
slice.h
Slicer for symex traces.
std_expr.h
API to expression classes.
symex_slicet::slice_assignment
void slice_assignment(SSA_stept &SSA_step)
Definition: slice.cpp:112
goto_trace_stept::typet::DEAD
@ DEAD
goto_trace_stept::typet::CONSTRAINT
@ CONSTRAINT
slice
void slice(symex_target_equationt &equation)
Definition: slice.cpp:205