cprover
slice.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Slicer for symex traces
4
5Author: 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)
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
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
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
226void 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:174
exprt cond_expr
Definition: ssa_step.h:149
goto_trace_stept::typet type
Definition: ssa_step.h:50
exprt guard
Definition: ssa_step.h:139
exprt ssa_rhs
Definition: ssa_step.h:145
ssa_exprt ssa_lhs
Definition: ssa_step.h:143
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:396
const irep_idt & get_identifier() const
Definition: std_expr.h:109
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:141
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:29
#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: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
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#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:189
Slicer for symex traces.