21 const cfgt::nodet &node,
27 dep_graph[dep_graph[node.PC].get_node_id()];
29 for(dependence_grapht::edgest::const_iterator
33 add_to_queue(queue, dep_node_to_cfg[it->first], node.PC);
37 const cfgt::nodet &node,
41 goto_functionst::function_mapt::const_iterator f_it =
47 f_it->second.body.instructions.begin();
50 for(
const auto &in_edge : entry.in)
55 const cfgt::nodet &node,
66 for(find_symbols_sett::const_iterator
71 decl_deadt::iterator entry=decl_dead.find(*it);
72 if(entry==decl_dead.end())
75 while(!entry->second.empty())
81 decl_dead.erase(entry);
115 jumpst::iterator next=it;
130 for( ; !lex_succ->is_end_function(); ++lex_succ)
135 if(lex_succ->is_end_function())
144 const auto &j_PC_node = pd.
get_node(j.PC);
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();
164 if(node.node_required)
166 const irep_idt &id2 = node.function_id;
168 "goto/jump expected to be within a single function");
170 const auto &postdom_node = pd.
get_node(*d_it);
172 if(postdom_node.dominators.size() > post_dom_size)
175 post_dom_size = postdom_node.dominators.size();
179 if(nearest!=lex_succ)
197 std::vector<cfgt::entryt> dep_node_to_cfg;
198 dep_node_to_cfg.reserve(dep_graph.
size());
204 while(!queue.empty())
206 while(!queue.empty())
213 if(node.node_required)
217 node.node_required=
true;
238 const irep_idt &statement = target->code().get_statement();
239 if(statement==ID_array_copy)
242 if(!target->is_assign())
245 const exprt &a_lhs = target->assign_lhs();
246 if(a_lhs.
id() != ID_symbol)
275 for(
const auto &instruction_and_index :
cfg.
entries())
277 const auto &instruction = instruction_and_index.first;
278 const auto instruction_node_index = instruction_and_index.second;
279 if(criterion(
cfg[instruction_node_index].function_id, instruction))
280 add_to_queue(queue, instruction_node_index, instruction);
282 add_to_queue(queue, instruction_node_index, instruction);
284 (instruction->is_goto() && instruction->condition().is_true()) ||
285 instruction->is_throw())
286 jumps.push_back(instruction_node_index);
287 else if(instruction->is_decl())
289 const auto &s = instruction->decl_symbol();
290 decl_dead[s.get_identifier()].push(instruction_node_index);
292 else if(instruction->is_dead())
294 const auto &s = instruction->dead_symbol();
295 decl_dead[s.get_identifier()].push(instruction_node_index);
301 dep_graph(goto_functions, ns);
304 fixedpoint(goto_functions, queue, jumps, decl_dead, dep_graph);
311 if(gf_entry.second.body_available())
317 !i_it->is_end_function() &&
318 !cfg_node.node_required)
320 i_it->turn_into_skip();
322 #ifdef DEBUG_FULL_SLICERT
327 for(std::set<unsigned>::const_iterator req_it =
328 cfg_node.required_by.begin();
329 req_it != cfg_node.required_by.end();
332 if(req_it != cfg_node.required_by.begin())
336 i_it->source_location.set_column(c);
337 i_it->source_location.set_comment(c);
354 full_slicert()(goto_functions, ns, criterion, message_handler);
376 const std::list<std::string> &properties,
385 const std::list<std::string> &properties,
irep_idt rounding_mode_identifier()
Return the identifier of the program symbol used to store the current rounding mode.
base_grapht::node_indext entryt
const entry_mapt & entries() const
Get a map from program points to their corresponding node indices.
entryt get_node_index(const goto_programt::const_targett &program_point) const
Get the graph node index for program_point.
nodet & get_node(const goto_programt::const_targett &program_point)
Get the CFG graph node relating to 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 cfgt::nodet & get_node(const T &program_point) const
Get the graph node (which gives dominators, predecessors and successors) for program_point.
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.
Base class for all expressions.
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, 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)
A collection of goto functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
instructionst::const_iterator const_targett
nodet::node_indext node_indext
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
virtual ~slicing_criteriont()
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
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
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)
#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
#define CHECK_RETURN(CONDITION)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.