cprover
Loading...
Searching...
No Matches
full_slicer.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Slicing
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "full_slicer.h"
13#include "full_slicer_class.h"
14
15#include <util/find_symbols.h>
16
19
21 const cfgt::nodet &node,
22 queuet &queue,
23 const dependence_grapht &dep_graph,
24 const dep_node_to_cfgt &dep_node_to_cfg)
25{
26 const dependence_grapht::nodet &d_node=
27 dep_graph[dep_graph[node.PC].get_node_id()];
28
29 for(dependence_grapht::edgest::const_iterator
30 it=d_node.in.begin();
31 it!=d_node.in.end();
32 ++it)
33 add_to_queue(queue, dep_node_to_cfg[it->first], node.PC);
34}
35
37 const cfgt::nodet &node,
38 queuet &queue,
39 const goto_functionst &goto_functions)
40{
41 goto_functionst::function_mapt::const_iterator f_it =
42 goto_functions.function_map.find(node.function_id);
43 CHECK_RETURN(f_it != goto_functions.function_map.end());
44
45 CHECK_RETURN(!f_it->second.body.instructions.empty());
46 goto_programt::const_targett begin_function=
47 f_it->second.body.instructions.begin();
48
49 const auto &entry = cfg.get_node(begin_function);
50 for(const auto &in_edge : entry.in)
51 add_to_queue(queue, in_edge.first, node.PC);
52}
53
55 const cfgt::nodet &node,
56 queuet &queue,
57 decl_deadt &decl_dead)
58{
59 if(decl_dead.empty())
60 return;
61
63
64 node.PC->apply([&syms](const exprt &e) { find_symbols(e, syms); });
65
66 for(find_symbols_sett::const_iterator
67 it=syms.begin();
68 it!=syms.end();
69 ++it)
70 {
71 decl_deadt::iterator entry=decl_dead.find(*it);
72 if(entry==decl_dead.end())
73 continue;
74
75 while(!entry->second.empty())
76 {
77 add_to_queue(queue, entry->second.top(), node.PC);
78 entry->second.pop();
79 }
80
81 decl_dead.erase(entry);
82 }
83}
84
86 queuet &queue,
87 jumpst &jumps,
88 const dependence_grapht::post_dominators_mapt &post_dominators)
89{
90 // Based on:
91 // On slicing programs with jump statements
92 // Hiralal Agrawal, PLDI'94
93 // Figure 7:
94 // Slice = the slice obtained using the conventional slicing algorithm;
95 // do {
96 // Traverse the postdominator tree using the preorder traversal,
97 // and for each jump statement, J, encountered that is
98 // (i) not in Slice and
99 // (ii) whose nearest postdominator in Slice is different from
100 // the nearest lexical successor in Slice) do {
101 // Add J to Slice;
102 // Add the transitive closure of the dependences of J to Slice;
103 // }
104 // } until no new jump statements may be added to Slice;
105 // For each goto statement, Goto L, in Slice, if the statement
106 // labeled L is not in Slice then associate the label L with its
107 // nearest postdominator in Slice;
108 // return (Slice);
109
110 for(jumpst::iterator
111 it=jumps.begin();
112 it!=jumps.end();
113 ) // no ++it
114 {
115 jumpst::iterator next=it;
116 ++next;
117
118 const cfgt::nodet &j=cfg[*it];
119
120 // is j in the slice already?
121 if(j.node_required)
122 {
123 jumps.erase(it);
124 it=next;
125 continue;
126 }
127
128 // check nearest lexical successor in slice
129 goto_programt::const_targett lex_succ=j.PC;
130 for( ; !lex_succ->is_end_function(); ++lex_succ)
131 {
132 if(cfg.get_node(lex_succ).node_required)
133 break;
134 }
135 if(lex_succ->is_end_function())
136 {
137 it=next;
138 continue;
139 }
140
141 const irep_idt &id = j.function_id;
142 const cfg_post_dominatorst &pd=post_dominators.at(id);
143
144 const auto &j_PC_node = pd.get_node(j.PC);
145
146 // find the nearest post-dominator in slice
147 if(!pd.dominates(lex_succ, j_PC_node))
148 {
149 add_to_queue(queue, *it, lex_succ);
150 jumps.erase(it);
151 }
152 else
153 {
154 // check whether the nearest post-dominator is different from
155 // lex_succ
156 goto_programt::const_targett nearest=lex_succ;
157 std::size_t post_dom_size=0;
158 for(cfg_dominatorst::target_sett::const_iterator d_it =
159 j_PC_node.dominators.begin();
160 d_it != j_PC_node.dominators.end();
161 ++d_it)
162 {
163 const auto &node = cfg.get_node(*d_it);
164 if(node.node_required)
165 {
166 const irep_idt &id2 = node.function_id;
167 INVARIANT(id==id2,
168 "goto/jump expected to be within a single function");
169
170 const auto &postdom_node = pd.get_node(*d_it);
171
172 if(postdom_node.dominators.size() > post_dom_size)
173 {
174 nearest=*d_it;
175 post_dom_size = postdom_node.dominators.size();
176 }
177 }
178 }
179 if(nearest!=lex_succ)
180 {
181 add_to_queue(queue, *it, nearest);
182 jumps.erase(it);
183 }
184 }
185
186 it=next;
187 }
188}
189
191 goto_functionst &goto_functions,
192 queuet &queue,
193 jumpst &jumps,
194 decl_deadt &decl_dead,
195 const dependence_grapht &dep_graph)
196{
197 std::vector<cfgt::entryt> dep_node_to_cfg;
198 dep_node_to_cfg.reserve(dep_graph.size());
199
200 for(dependence_grapht::node_indext i = 0; i < dep_graph.size(); ++i)
201 dep_node_to_cfg.push_back(cfg.get_node_index(dep_graph[i].PC));
202
203 // process queue until empty
204 while(!queue.empty())
205 {
206 while(!queue.empty())
207 {
208 cfgt::entryt e=queue.top();
209 cfgt::nodet &node=cfg[e];
210 queue.pop();
211
212 // already done by some earlier iteration?
213 if(node.node_required)
214 continue;
215
216 // node is required
217 node.node_required=true;
218
219 // add data and control dependencies of node
220 add_dependencies(node, queue, dep_graph, dep_node_to_cfg);
221
222 // retain all calls of the containing function
223 add_function_calls(node, queue, goto_functions);
224
225 // find all the symbols it uses to add declarations
226 add_decl_dead(node, queue, decl_dead);
227 }
228
229 // add any required jumps
230 add_jumps(queue, jumps, dep_graph.cfg_post_dominators());
231 }
232}
233
235{
236 // some variables are used during symbolic execution only
237
238 const irep_idt &statement = target->code().get_statement();
239 if(statement==ID_array_copy)
240 return true;
241
242 if(!target->is_assign())
243 return false;
244
245 const exprt &a_lhs = target->assign_lhs();
246 if(a_lhs.id() != ID_symbol)
247 return false;
248
249 const symbol_exprt &s = to_symbol_expr(a_lhs);
250
252}
253
255 goto_functionst &goto_functions,
256 const namespacet &ns,
257 const slicing_criteriont &criterion)
258{
259 // build the CFG data structure
260 cfg(goto_functions);
261 for(const auto &gf_entry : goto_functions.function_map)
262 {
263 forall_goto_program_instructions(i_it, gf_entry.second.body)
264 cfg.get_node(i_it).function_id = gf_entry.first;
265 }
266
267 // fill queue with according to slicing criterion
268 queuet queue;
269 // gather all unconditional jumps as they may need to be included
270 jumpst jumps;
271 // declarations or dead instructions may be necessary as well
272 decl_deadt decl_dead;
273
274 for(const auto &instruction_and_index : cfg.entries())
275 {
276 const auto &instruction = instruction_and_index.first;
277 const auto instruction_node_index = instruction_and_index.second;
278 if(criterion(cfg[instruction_node_index].function_id, instruction))
279 add_to_queue(queue, instruction_node_index, instruction);
280 else if(implicit(instruction))
281 add_to_queue(queue, instruction_node_index, instruction);
282 else if(
283 (instruction->is_goto() && instruction->condition().is_true()) ||
284 instruction->is_throw())
285 jumps.push_back(instruction_node_index);
286 else if(instruction->is_decl())
287 {
288 const auto &s = instruction->decl_symbol();
289 decl_dead[s.get_identifier()].push(instruction_node_index);
290 }
291 else if(instruction->is_dead())
292 {
293 const auto &s = instruction->dead_symbol();
294 decl_dead[s.get_identifier()].push(instruction_node_index);
295 }
296 }
297
298 // compute program dependence graph (and post-dominators)
299 dependence_grapht dep_graph(ns);
300 dep_graph(goto_functions, ns);
301
302 // compute the fixedpoint
303 fixedpoint(goto_functions, queue, jumps, decl_dead, dep_graph);
304
305 // now replace those instructions that are not needed
306 // by skips
307
308 for(auto &gf_entry : goto_functions.function_map)
309 {
310 if(gf_entry.second.body_available())
311 {
312 Forall_goto_program_instructions(i_it, gf_entry.second.body)
313 {
314 const auto &cfg_node = cfg.get_node(i_it);
315 if(
316 !i_it->is_end_function() && // always retained
317 !cfg_node.node_required)
318 {
319 i_it->turn_into_skip();
320 }
321#ifdef DEBUG_FULL_SLICERT
322 else
323 {
324 std::string c="ins:"+std::to_string(i_it->location_number);
325 c+=" req by:";
326 for(std::set<unsigned>::const_iterator req_it =
327 cfg_node.required_by.begin();
328 req_it != cfg_node.required_by.end();
329 ++req_it)
330 {
331 if(req_it != cfg_node.required_by.begin())
332 c+=",";
333 c+=std::to_string(*req_it);
334 }
335 i_it->source_location.set_column(c); // for show-goto-functions
336 i_it->source_location.set_comment(c); // for dump-c
337 }
338#endif
339 }
340 }
341 }
342
343 // remove the skips
344 remove_skip(goto_functions);
345}
346
348 goto_functionst &goto_functions,
349 const namespacet &ns,
350 const slicing_criteriont &criterion)
351{
352 full_slicert()(goto_functions, ns, criterion);
353}
354
356 goto_functionst &goto_functions,
357 const namespacet &ns)
358{
360 full_slicert()(goto_functions, ns, a);
361}
362
363void full_slicer(goto_modelt &goto_model)
364{
366 const namespacet ns(goto_model.symbol_table);
367 full_slicert()(goto_model.goto_functions, ns, a);
368}
369
371 goto_functionst &goto_functions,
372 const namespacet &ns,
373 const std::list<std::string> &properties)
374{
375 properties_criteriont p(properties);
376 full_slicert()(goto_functions, ns, p);
377}
378
380 goto_modelt &goto_model,
381 const std::list<std::string> &properties)
382{
383 const namespacet ns(goto_model.symbol_table);
384 property_slicer(goto_model.goto_functions, ns, properties);
385}
386
irep_idt rounding_mode_identifier()
Return the identifier of the program symbol used to store the current rounding mode.
Symbolic Execution.
const entry_mapt & entries() const
Get a map from program points to their corresponding node indices.
Definition cfg.h:259
base_grapht::node_indext entryt
Definition cfg.h:91
base_grapht::nodet nodet
Definition cfg.h:92
nodet & get_node(const goto_programt::const_targett &program_point)
Get the CFG graph node relating to program_point.
Definition cfg.h:245
entryt get_node_index(const goto_programt::const_targett &program_point) const
Get the graph node index for program_point.
Definition cfg.h:239
const cfgt::nodet & get_node(const T &program_point) const
Get the graph node (which gives dominators, predecessors and successors) for program_point.
bool dominates(T lhs, const nodet &rhs_node) const
Returns true if the program point corresponding to rhs_node is dominated by program point lhs.
const post_dominators_mapt & cfg_post_dominators() const
std::map< irep_idt, cfg_post_dominatorst > post_dominators_mapt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
void add_function_calls(const cfgt::nodet &node, queuet &queue, const goto_functionst &goto_functions)
std::list< cfgt::entryt > jumpst
void add_to_queue(queuet &queue, const cfgt::entryt &entry, goto_programt::const_targett reason)
std::unordered_map< irep_idt, queuet > decl_deadt
void add_dependencies(const cfgt::nodet &node, queuet &queue, const dependence_grapht &dep_graph, const dep_node_to_cfgt &dep_node_to_cfg)
void fixedpoint(goto_functionst &goto_functions, queuet &queue, jumpst &jumps, decl_deadt &decl_dead, const dependence_grapht &dep_graph)
void add_decl_dead(const cfgt::nodet &node, queuet &queue, decl_deadt &decl_dead)
void operator()(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
std::stack< cfgt::entryt > queuet
std::vector< cfgt::entryt > dep_node_to_cfgt
void add_jumps(queuet &queue, jumpst &jumps, const dependence_grapht::post_dominators_mapt &post_dominators)
A collection of goto functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
instructionst::const_iterator const_targett
edgest in
Definition graph.h:42
nodet::node_indext node_indext
Definition graph.h:173
std::size_t size() const
Definition graph.h:212
const irep_idt & id() const
Definition irep.h:396
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
virtual ~slicing_criteriont()
Expression to hold a symbol (variable)
Definition std_expr.h:113
const irep_idt & get_identifier() const
Definition std_expr.h:142
static bool find_symbols(symbol_kindt, const typet &, std::function< bool(const symbol_exprt &)>, std::unordered_set< irep_idt > &bindings)
std::unordered_set< irep_idt > find_symbols_sett
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
static bool implicit(goto_programt::const_targett target)
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
Goto Program Slicing.
#define forall_goto_program_instructions(it, program)
#define Forall_goto_program_instructions(it, program)
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Program Transformation.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222