CBMC: /home/runner/work/cbmc/cbmc/src/goto-instrument/full_slicer.cpp Source File

CBMC
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
17#include <goto-programs/adjust_float_expressions.h>
18#include <goto-programs/remove_skip.h>
19
21 const cfgt::nodet &node,
22 queuet &queue,
25{
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());
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,
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,
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
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
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,
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)
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
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
250
251 return s.identifier() == rounding_mode_identifier();
252}
253
255 goto_functionst &goto_functions,
256 const namespacet &ns,
258 message_handlert &message_handler)
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->condition() == 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.identifier()].push(instruction_node_index);
291 }
292 else if(instruction->is_dead())
293 {
294 const auto &s = instruction->dead_symbol();
295 decl_dead[s.identifier()].push(instruction_node_index);
296 }
297 }
298
299 // compute program dependence graph (and post-dominators)
300 dependence_grapht dep_graph(ns, message_handler);
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 message_handlert &message_handler)
353{
354 full_slicert()(goto_functions, ns, criterion, message_handler);
355}
356
358 goto_functionst &goto_functions,
359 const namespacet &ns,
360 message_handlert &message_handler)
361{
363 full_slicert()(goto_functions, ns, a, message_handler);
364}
365
366 void full_slicer(goto_modelt &goto_model, message_handlert &message_handler)
367{
369 const namespacet ns(goto_model.symbol_table);
370 full_slicert()(goto_model.goto_functions, ns, a, message_handler);
371}
372
374 goto_functionst &goto_functions,
375 const namespacet &ns,
376 const std::list<std::string> &properties,
377 message_handlert &message_handler)
378{
379 properties_criteriont p(properties);
380 full_slicert()(goto_functions, ns, p, message_handler);
381}
382
384 goto_modelt &goto_model,
385 const std::list<std::string> &properties,
386 message_handlert &message_handler)
387{
388 const namespacet ns(goto_model.symbol_table);
389 property_slicer(goto_model.goto_functions, ns, properties, message_handler);
390}
391
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:566
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:38
Base class for all expressions.
Definition expr.h:57
void add_function_calls(const cfgt::nodet &node, queuet &queue, const goto_functionst &goto_functions)
Definition full_slicer.cpp:36
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)
Definition full_slicer.cpp:20
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)
Definition full_slicer.cpp:54
cfgt cfg
void operator()(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion, message_handlert &message_handler)
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)
Definition full_slicer.cpp:85
A collection of goto functions.
function_mapt function_map
Definition goto_model.h:27
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
Definition goto_program.h:614
N nodet
Definition graph.h:169
nodet::node_indext node_indext
Definition graph.h:173
Definition message.h:27
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Definition full_slicer.h:37
virtual ~slicing_criteriont()
Expression to hold a symbol (variable)
Definition std_expr.h:132
void identifier(const irep_idt &identifier)
Definition std_expr.h:160
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...
std::unordered_set< irep_idt > find_symbols_sett
Definition find_symbols.h:22
static bool implicit(goto_programt::const_targett target)
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties, message_handlert &message_handler)
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion, message_handlert &message_handler)
Slicing.
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
Definition remove_skip.cpp:87
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:221

AltStyle によって変換されたページ (->オリジナル) /