71 if(from->is_goto() || from->is_assume())
73 else if(from->is_end_function())
93 bool post_dom_all = !control_dep_candidate->is_assume();
94 bool post_dom_one=
false;
98 const cfg_post_dominatorst::cfgt::nodet &m =
102 for(
const auto &edge : m.out)
107 const cfg_post_dominatorst::cfgt::nodet &m_s=
110 if(m_s.dominators.find(to)!=m_s.dominators.end())
116 if(post_dom_all || !post_dom_one)
142 else if(w_start >= r_start)
168 goto_rw(function_to, to, rw_set);
170 for(
const auto &read_object_entry : rw_set.
get_r_set())
176 for(
const auto &w_range : w_ranges)
179 for(
const auto &wr : w_range.second)
181 for(
const auto &r_range : r_ranges)
185 r_range.first, r_range.second))
198 if(to->is_set_return_value())
233 depst filtered_control_deps;
237 std::inserter(filtered_control_deps, filtered_control_deps.end()),
242 if(from->is_function_call() && function_from != function_to)
279 out <<
"Control dependencies: ";
280 for(depst::const_iterator
287 out << (*it)->location_number;
294 out <<
"Data dependencies: ";
295 for(depst::const_iterator
302 out << (*it)->location_number;
320 {
"locationNumber",
json_numbert(std::to_string(cd->location_number))},
321 {
"sourceLocation",
json(cd->source_location())},
329 {
"locationNumber",
json_numbert(std::to_string(dd->location_number))},
330 {
"sourceLocation",
json(dd->source_location())},
335 return std::move(graph);
353 auto node_id =
dg.add_node();
354 dg.nodes[node_id].PC = l;
355 auto p = std::make_unique<dep_graph_domaint>(node_id,
message_handler);
358 return std::unique_ptr<statet>(p.release());
381 const node_indext n_from = (*this)[from].get_node_id();
383 const node_indext n_to = (*this)[to].get_node_id();
389 nodes[n_from].out[n_to].add(kind);
390 nodes[n_to].in[n_from].add(kind);
cfg_dominators_templatet< const goto_programt, goto_programt::const_targett, true > cfg_post_dominatorst
This is the basic interface of the abstract interpreter with default implementations of the core func...
message_handlert & message_handler
ai_history_baset::trace_ptrt trace_ptrt
goto_programt::const_targett locationt
ai_domain_factory_baset::locationt locationt
virtual const locationt & current_location(void) const =0
The current location in the history, used to compute the transformer POSTCONDITION(return value is de...
virtual statet & get_state(trace_ptrt p)
Get the state for the given history, creating it with the factory if it doesn't exist.
const cfgt::nodet & get_node(const T &program_point) const
Get the graph node (which gives dominators, predecessors and successors) for program_point.
std::unique_ptr< statet > make(locationt l) const override
dep_graph_domain_factoryt(dependence_grapht &_dg, message_handlert &message_handler)
message_handlert & message_handler
dep_graph_domaint(node_indext id, message_handlert &message_handler)
void control_dependencies(const irep_idt &function_id, goto_programt::const_targett from, goto_programt::const_targett to, dependence_grapht &dep_graph)
std::set< goto_programt::const_targett, goto_programt::target_less_than > depst
bool merge(const dep_graph_domaint &src, trace_ptrt from, trace_ptrt to)
bool is_bottom() const final override
void populate_dep_graph(dependence_grapht &, goto_programt::const_targett) const
jsont output_json(const ai_baset &ai, const namespacet &ns) const override
Outputs the current value of the domain.
void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) final override
how function calls are treated: a) there is an edge from each call site to the function head b) there...
depst control_dep_candidates
void data_dependencies(goto_programt::const_targett from, const irep_idt &function_to, goto_programt::const_targett to, dependence_grapht &dep_graph, const namespacet &ns)
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
message_handlert & message_handler
void add_dep(dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to)
dependence_grapht(const namespacet &_ns, message_handlert &)
const post_dominators_mapt & cfg_post_dominators() const
friend dep_graph_domain_factoryt
const reaching_definitions_analysist & reaching_definitions() const
reaching_definitions_analysist rd
std::map< irep_idt, goto_programt::const_targett > end_function_map
instructionst::const_iterator const_targett
nodet::node_indext node_indext
jsont & push_back(const jsont &json)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Data type to describe upper and lower bounds of the range of bits that a read or write access may aff...
std::map< locationt, rangest, goto_programt::target_less_than > ranges_at_loct
value_setst & get_value_sets() const
const objectst & get_r_set() const
const range_domaint & get_ranges(const std::unique_ptr< range_domain_baset > &ranges) const
const V & get(const std::size_t value_index) const
bool util_inplace_set_union(std::set< T, Compare, Alloc > &target, const std::set< T, Compare, Alloc > &source)
Compute union of two sets.
static bool may_be_def_use_pair(const range_spect &w_start, const range_spect &w_end, const range_spect &r_start, const range_spect &r_end)
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
static void goto_rw(const irep_idt &function, goto_programt::const_targett target, const exprt &lhs, const exprt &function_expr, const exprt::operandst &arguments, rw_range_sett &rw_set)
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
#define CHECK_RETURN(CONDITION)
#define PRECONDITION(CONDITION)