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#include <util/cprover_prefix.h>
17
20
22 const cfgt::nodet &node,
23 queuet &queue,
26{
28 dep_graph[dep_graph[node.PC].get_node_id()];
29
30 for(dependence_grapht::edgest::const_iterator
31 it=d_node.in.begin();
32 it!=d_node.in.end();
33 ++it)
34 add_to_queue(queue, dep_node_to_cfg[it->first], node.PC);
35}
36
38 const cfgt::nodet &node,
39 queuet &queue,
40 const goto_functionst &goto_functions)
41{
42 goto_functionst::function_mapt::const_iterator f_it =
43 goto_functions.function_map.find(node.function_id);
44 assert(f_it!=goto_functions.function_map.end());
45
46 assert(!f_it->second.body.instructions.empty());
48 f_it->second.body.instructions.begin();
49
50 const auto &entry = cfg.get_node(begin_function);
51 for(const auto &in_edge : entry.in)
52 add_to_queue(queue, in_edge.first, node.PC);
53}
54
56 const cfgt::nodet &node,
57 queuet &queue,
59{
60 if(decl_dead.empty())
61 return;
62
64
65 node.PC->apply([&syms](const exprt &e) { find_symbols_or_nexts(e, syms); });
66
67 for(find_symbols_sett::const_iterator
68 it=syms.begin();
69 it!=syms.end();
70 ++it)
71 {
72 decl_deadt::iterator entry=decl_dead.find(*it);
73 if(entry==decl_dead.end())
74 continue;
75
76 while(!entry->second.empty())
77 {
78 add_to_queue(queue, entry->second.top(), node.PC);
79 entry->second.pop();
80 }
81
82 decl_dead.erase(entry);
83 }
84}
85
87 queuet &queue,
89 const dependence_grapht::post_dominators_mapt &post_dominators)
90{
91 // Based on:
92 // On slicing programs with jump statements
93 // Hiralal Agrawal, PLDI'94
94 // Figure 7:
95 // Slice = the slice obtained using the conventional slicing algorithm;
96 // do {
97 // Traverse the postdominator tree using the preorder traversal,
98 // and for each jump statement, J, encountered that is
99 // (i) not in Slice and
100 // (ii) whose nearest postdominator in Slice is different from
101 // the nearest lexical successor in Slice) do {
102 // Add J to Slice;
103 // Add the transitive closure of the dependences of J to Slice;
104 // }
105 // } until no new jump statements may be added to Slice;
106 // For each goto statement, Goto L, in Slice, if the statement
107 // labeled L is not in Slice then associate the label L with its
108 // nearest postdominator in Slice;
109 // return (Slice);
110
111 for(jumpst::iterator
112 it=jumps.begin();
113 it!=jumps.end();
114 ) // no ++it
115 {
116 jumpst::iterator next=it;
117 ++next;
118
119 const cfgt::nodet &j=cfg[*it];
120
121 // is j in the slice already?
122 if(j.node_required)
123 {
124 jumps.erase(it);
125 it=next;
126 continue;
127 }
128
129 // check nearest lexical successor in slice
131 for( ; !lex_succ->is_end_function(); ++lex_succ)
132 {
133 if(cfg.get_node(lex_succ).node_required)
134 break;
135 }
136 if(lex_succ->is_end_function())
137 {
138 it=next;
139 continue;
140 }
141
142 const irep_idt &id = j.function_id;
143 const cfg_post_dominatorst &pd=post_dominators.at(id);
144
145 const auto &j_PC_node = pd.get_node(j.PC);
146
147 // find the nearest post-dominator in slice
148 if(!pd.dominates(lex_succ, j_PC_node))
149 {
150 add_to_queue(queue, *it, lex_succ);
151 jumps.erase(it);
152 }
153 else
154 {
155 // check whether the nearest post-dominator is different from
156 // lex_succ
158 std::size_t post_dom_size=0;
159 for(cfg_dominatorst::target_sett::const_iterator d_it =
160 j_PC_node.dominators.begin();
161 d_it != j_PC_node.dominators.end();
162 ++d_it)
163 {
164 const auto &node = cfg.get_node(*d_it);
165 if(node.node_required)
166 {
167 const irep_idt &id2 = node.function_id;
168 INVARIANT(id==id2,
169 "goto/jump expected to be within a single function");
170
171 const auto &postdom_node = pd.get_node(*d_it);
172
173 if(postdom_node.dominators.size() > post_dom_size)
174 {
175 nearest=*d_it;
176 post_dom_size = postdom_node.dominators.size();
177 }
178 }
179 }
180 if(nearest!=lex_succ)
181 {
182 add_to_queue(queue, *it, nearest);
183 jumps.erase(it);
184 }
185 }
186
187 it=next;
188 }
189}
190
192 goto_functionst &goto_functions,
193 queuet &queue,
194 jumpst &jumps,
197{
198 std::vector<cfgt::entryt> dep_node_to_cfg;
199 dep_node_to_cfg.reserve(dep_graph.size());
200
201 for(dependence_grapht::node_indext i = 0; i < dep_graph.size(); ++i)
203
204 // process queue until empty
205 while(!queue.empty())
206 {
207 while(!queue.empty())
208 {
209 cfgt::entryt e=queue.top();
210 cfgt::nodet &node=cfg[e];
211 queue.pop();
212
213 // already done by some earlier iteration?
214 if(node.node_required)
215 continue;
216
217 // node is required
218 node.node_required=true;
219
220 // add data and control dependencies of node
222
223 // retain all calls of the containing function
224 add_function_calls(node, queue, goto_functions);
225
226 // find all the symbols it uses to add declarations
227 add_decl_dead(node, queue, decl_dead);
228 }
229
230 // add any required jumps
231 add_jumps(queue, jumps, dep_graph.cfg_post_dominators());
232 }
233}
234
236{
237 // some variables are used during symbolic execution only
238
239 const irep_idt &statement = target->get_code().get_statement();
240 if(statement==ID_array_copy)
241 return true;
242
243 if(!target->is_assign())
244 return false;
245
246 const exprt &a_lhs = target->assign_lhs();
247 if(a_lhs.id() != ID_symbol)
248 return false;
249
251
253}
254
256 goto_functionst &goto_functions,
257 const namespacet &ns,
259{
260 // build the CFG data structure
261 cfg(goto_functions);
262 for(const auto &gf_entry : goto_functions.function_map)
263 {
265 cfg.get_node(i_it).function_id = gf_entry.first;
266 }
267
268 // fill queue with according to slicing criterion
269 queuet queue;
270 // gather all unconditional jumps as they may need to be included
272 // declarations or dead instructions may be necessary as well
274
275 for(const auto &instruction_and_index : cfg.entries())
276 {
277 const auto &instruction = instruction_and_index.first;
279 if(criterion(cfg[instruction_node_index].function_id, instruction))
280 add_to_queue(queue, instruction_node_index, instruction);
281 else if(implicit(instruction))
282 add_to_queue(queue, instruction_node_index, instruction);
283 else if(
284 (instruction->is_goto() && instruction->get_condition().is_true()) ||
285 instruction->is_throw())
286 jumps.push_back(instruction_node_index);
287 else if(instruction->is_decl())
288 {
289 const auto &s = instruction->decl_symbol();
290 decl_dead[s.get_identifier()].push(instruction_node_index);
291 }
292 else if(instruction->is_dead())
293 {
294 const auto &s = instruction->dead_symbol();
295 decl_dead[s.get_identifier()].push(instruction_node_index);
296 }
297 }
298
299 // compute program dependence graph (and post-dominators)
301 dep_graph(goto_functions, ns);
302
303 // compute the fixedpoint
304 fixedpoint(goto_functions, queue, jumps, decl_dead, dep_graph);
305
306 // now replace those instructions that are not needed
307 // by skips
308
309 for(auto &gf_entry : goto_functions.function_map)
310 {
311 if(gf_entry.second.body_available())
312 {
314 {
315 const auto &cfg_node = cfg.get_node(i_it);
316 if(
317 !i_it->is_end_function() && // always retained
318 !cfg_node.node_required)
319 {
320 i_it->turn_into_skip();
321 }
322#ifdef DEBUG_FULL_SLICERT
323 else
324 {
325 std::string c="ins:"+std::to_string(i_it->location_number);
326 c+=" req by:";
327 for(std::set<unsigned>::const_iterator req_it =
328 cfg_node.required_by.begin();
329 req_it != cfg_node.required_by.end();
330 ++req_it)
331 {
332 if(req_it != cfg_node.required_by.begin())
333 c+=",";
334 c+=std::to_string(*req_it);
335 }
336 i_it->source_location.set_column(c); // for show-goto-functions
337 i_it->source_location.set_comment(c); // for dump-c
338 }
339#endif
340 }
341 }
342 }
343
344 // remove the skips
345 remove_skip(goto_functions);
346}
347
349 goto_functionst &goto_functions,
350 const namespacet &ns,
352{
353 full_slicert()(goto_functions, ns, criterion);
354}
355
357 goto_functionst &goto_functions,
358 const namespacet &ns)
359{
361 full_slicert()(goto_functions, ns, a);
362}
363
364void full_slicer(goto_modelt &goto_model)
365{
367 const namespacet ns(goto_model.symbol_table);
368 full_slicert()(goto_model.goto_functions, ns, a);
369}
370
372 goto_functionst &goto_functions,
373 const namespacet &ns,
374 const std::list<std::string> &properties)
375{
376 properties_criteriont p(properties);
377 full_slicert()(goto_functions, ns, p);
378}
379
381 goto_modelt &goto_model,
382 const std::list<std::string> &properties)
383{
384 const namespacet ns(goto_model.symbol_table);
385 property_slicer(goto_model.goto_functions, ns, properties);
386}
387
irep_idt rounding_mode_identifier()
Return the identifier of the program symbol used to store the current rounding mode.
Symbolic Execution.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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
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
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:37
Base class for all expressions.
Definition expr.h:54
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:30
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:33
instructionst::const_iterator const_targett
nodet::node_indext node_indext
Definition graph.h:173
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:80
const irep_idt & get_identifier() const
Definition std_expr.h:109
void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest)
Add to the set dest the sub-expressions of src with id ID_symbol or ID_next_symbol.
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 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:189