CBMC
Loading...
Searching...
No Matches
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#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
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,
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
196 }
197 }
198
200
201 // remove the ones that are defined
202 open_variables.erase(lhs.begin(), lhs.end());
203}
204
206{
208 symex_slice.slice(equation);
209}
210
216 const symex_target_equationt &equation,
218{
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{
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())
246
247 // slice away anything after it
248
249 symex_target_equationt::SSA_stepst::iterator s_it=
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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.