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 }
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:29
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:53
simple_slice
void simple_slice(symex_target_equationt &equation)
Definition: slice.cpp:237
SSA_stept::guard
exprt guard
Definition: ssa_step.h:137
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
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:111
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:264
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:177
irept::id
const irep_idt & id() const
Definition: irep.h:418
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:142
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:217
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:206