CBMC
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 #include "symex_slice_class.h"
14 
15 #include <util/find_symbols.h>
16 #include <util/std_expr.h>
17 
19 {
20  find_symbols(expr, depends);
21 }
22 
24  symex_target_equationt &equation,
25  const std::list<exprt> &exprs)
26 {
27  // collect dependencies
28  for(const auto &expr : exprs)
29  get_symbols(expr);
30 
31  slice(equation);
32 }
33 
35 {
36  simple_slice(equation);
37 
38  for(symex_target_equationt::SSA_stepst::reverse_iterator
39  it=equation.SSA_steps.rbegin();
40  it!=equation.SSA_steps.rend();
41  it++)
42  {
43  if(!it->ignore)
44  slice(*it);
45  }
46 }
47 
49 {
50  switch(SSA_step.type)
51  {
53  get_symbols(SSA_step.cond_expr);
54  break;
55 
57  get_symbols(SSA_step.cond_expr);
58  break;
59 
61  // ignore
62  break;
63 
65  // ignore
66  break;
67 
69  slice_assignment(SSA_step);
70  break;
71 
73  slice_decl(SSA_step);
74  break;
75 
78  break;
79 
81  // ignore for now
82  break;
83 
91  // ignore for now
92  break;
93 
96  // ignore for now
97  break;
98 
100  UNREACHABLE;
101  }
102 }
103 
105 {
106  PRECONDITION(SSA_step.ssa_lhs.id() == ID_symbol);
107  const irep_idt &id=SSA_step.ssa_lhs.get_identifier();
108 
109  auto entry = depends.find(id);
110  if(entry == depends.end())
111  {
112  // we don't really need it
113  SSA_step.ignore=true;
114  }
115  else
116  {
117  // we have resolved this dependency
118  depends.erase(entry);
119  get_symbols(SSA_step.ssa_rhs);
120  }
121 }
122 
124 {
125  const irep_idt &id = to_symbol_expr(SSA_step.ssa_lhs).get_identifier();
126 
127  if(depends.find(id)==depends.end())
128  {
129  // we don't really need it
130  SSA_step.ignore=true;
131  }
132 }
133 
139  const symex_target_equationt &equation,
140  symbol_sett &open_variables)
141 {
142  symbol_sett lhs;
143 
144  for(symex_target_equationt::SSA_stepst::const_iterator
145  it=equation.SSA_steps.begin();
146  it!=equation.SSA_steps.end();
147  it++)
148  {
149  const SSA_stept &SSA_step = *it;
150 
151  get_symbols(SSA_step.guard);
152 
153  switch(SSA_step.type)
154  {
156  get_symbols(SSA_step.cond_expr);
157  break;
158 
160  get_symbols(SSA_step.cond_expr);
161  break;
162 
164  // ignore
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 
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 }
Single SSA step in the equation.
Definition: ssa_step.h:47
bool ignore
Definition: ssa_step.h:172
exprt cond_expr
Definition: ssa_step.h:145
goto_trace_stept::typet type
Definition: ssa_step.h:50
exprt guard
Definition: ssa_step.h:135
exprt ssa_rhs
Definition: ssa_step.h:141
ssa_exprt ssa_lhs
Definition: ssa_step.h:139
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
const irep_idt & id() const
Definition: irep.h:388
const irep_idt & get_identifier() const
Definition: std_expr.h:160
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:138
symbol_sett depends
void slice(symex_target_equationt &equation)
Definition: slice.cpp:34
void slice_decl(SSA_stept &SSA_step)
Definition: slice.cpp:123
void slice_assignment(SSA_stept &SSA_step)
Definition: slice.cpp:104
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
static bool find_symbols(symbol_kindt, const typet &, std::function< bool(const symbol_exprt &)>, std::unordered_set< irep_idt > &bindings, const std::vector< irep_idt > &subs_to_find)
Find identifiers with id ID_symbol of the sub expressions and the subs with ID in subs_to_find consid...
void revert_slice(symex_target_equationt &equation)
Undo whatever has been done by slice
Definition: slice.cpp:261
void slice(symex_target_equationt &equation)
Definition: slice.cpp:205
void simple_slice(symex_target_equationt &equation)
Definition: slice.cpp:234
void collect_open_variables(const symex_target_equationt &equation, symbol_sett &open_variables)
Collect the open variables, i.e.
Definition: slice.cpp:215
Slicer for symex traces.
std::unordered_set< irep_idt > symbol_sett
Definition: slice.h:39
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
Slicer for symex traces.