15 #ifndef CPROVER_ANALYSES_DEPENDENCE_GRAPH_H
16 #define CPROVER_ANALYSES_DEPENDENCE_GRAPH_H
101 "node_id must not be valid");
112 "node_id must be valid");
125 node_id != std::numeric_limits<node_indext>::max(),
126 "node_id must not be valid");
139 "node_id must be valid");
145 "If the domain is top, it must have no dependencies");
153 "node_id must be valid");
159 "If the domain is bottom, it must have no dependencies");
179 set<goto_programt::const_targett, goto_programt::target_less_than>
219 public ait<dep_graph_domaint>,
233 rd(goto_functions,
ns);
238 if(!goto_program.
empty())
241 entry.first, std::prev(goto_program.
instructions.end()));
254 if(!goto_program.
empty())
266 for(
const auto &location_state :
269 std::static_pointer_cast<dep_graph_domaint>(location_state.second)
270 ->populate_dep_graph(*
this, location_state.first);
Compute dominators for CFG of goto_function.
This is the basic interface of the abstract interpreter with default implementations of the core func...
virtual void initialize(const irep_idt &function_id, const goto_programt &goto_program)
Initialize all the abstract states for a single function.
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
virtual void make_bottom()=0
no states
ai_history_baset::trace_ptrt trace_ptrt
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
virtual statet & get_state(trace_ptrt p)
Get the state for the given history, creating it with the factory if it doesn't exist.
This ensures that all domains are constructed with the node ID that links them to the graph part of t...
bool is_top() const final override
friend const depst & dependence_graph_test_get_control_deps(const dep_graph_domaint &)
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
node_indext get_node_id() const
bool merge(const dep_graph_domaint &src, trace_ptrt from, trace_ptrt to)
bool is_bottom() const final override
void make_bottom() final override
no states
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...
friend const depst & dependence_graph_test_get_data_deps(const dep_graph_domaint &)
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 make_top() final override
all states – the analysis doesn't use this directly (see make_entry) and domains may refuse to implem...
void make_entry() final override
Make this domain a reasonable entry-point state For most domains top is sufficient.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
message_handlert & message_handler
grapht< dep_nodet >::node_indext node_indext
void add_dep(dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to)
dependence_grapht(const namespacet &_ns, message_handlert &)
friend dep_graph_domain_factoryt
const reaching_definitions_analysist & reaching_definitions() const
const post_dominators_mapt & cfg_post_dominators() const
reaching_definitions_analysist rd
std::map< irep_idt, cfg_post_dominatorst > post_dominators_mapt
void initialize(const goto_functionst &goto_functions)
Initialize all the abstract states for a whole program.
void finalize()
Override this to add a cleanup or post-processing step after fixedpoint has run.
std::map< irep_idt, goto_programt::const_targett > end_function_map
void initialize(const irep_idt &function, const goto_programt &goto_program)
Initialize all the abstract states for a single function.
post_dominators_mapt post_dominators
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A collection of goto functions.
function_mapt function_map
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
bool empty() const
Is the program empty?
This class represents a node in a directed graph.
A generic directed graph with a parametric node type.
The most conventional storage; one domain per location.
state_mapt & internal(void)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
#define forall_goto_program_instructions(it, program)
A Template Class for Graphs.
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis,...
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
graph_nodet< dep_edget >::edget edget
graph_nodet< dep_edget >::edgest edgest
goto_programt::const_targett PC