CBMC
Loading...
Searching...
No Matches
Public Types | Public Member Functions | Protected Member Functions | Protected Attributes | Friends | List of all members
variable_sensitivity_dependence_grapht Class Reference

#include <variable_sensitivity_dependence_graph.h>

+ Inheritance diagram for variable_sensitivity_dependence_grapht:
[フレーム]
[legend]
+ Collaboration diagram for variable_sensitivity_dependence_grapht:
[フレーム]
[legend]

Public Types

typedef std::map< irep_idt, cfg_post_dominatorst >  post_dominators_mapt
 
- Public Types inherited from ai_baset
typedef ai_domain_baset  statet
 
typedef ai_storage_baset::cstate_ptrt  cstate_ptrt
 
typedef ai_history_baset::trace_ptrt  trace_ptrt
 
typedef ai_history_baset::trace_sett  trace_sett
 
typedef ai_storage_baset::ctrace_set_ptrt  ctrace_set_ptrt
 
typedef goto_programt::const_targett  locationt
 
- Public Types inherited from grapht< vs_dep_nodet >
typedef vs_dep_nodet  nodet
 
typedef nodet::edgest  edgest
 
typedef std::vector< nodet >  nodest
 
typedef nodet::edget  edget
 
typedef nodet::node_indext  node_indext
 
typedef std::list< node_indext >  patht
 

Public Member Functions

  variable_sensitivity_dependence_grapht (const goto_functionst &goto_functions, const namespacet &_ns, variable_sensitivity_object_factory_ptrt object_factory, const vsd_configt &_configuration, message_handlert &message_handler)
 
void  initialize (const irep_idt &function_id, const goto_programt &goto_program)
  Initialize all the abstract states for a single function.
 
void  finalize ()
  Override this to add a cleanup or post-processing step after fixedpoint has run.
 
void  add_dep (vs_dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to)
 
post_dominators_mapt &  cfg_post_dominators ()
 
- Public Member Functions inherited from ai_three_way_merget
  ai_three_way_merget (std::unique_ptr< ai_history_factory_baset > &&hf, std::unique_ptr< ai_domain_factory_baset > &&df, std::unique_ptr< ai_storage_baset > &&st, message_handlert &mh)
 
- Public Member Functions inherited from ai_recursive_interproceduralt
  ai_recursive_interproceduralt (std::unique_ptr< ai_history_factory_baset > &&hf, std::unique_ptr< ai_domain_factory_baset > &&df, std::unique_ptr< ai_storage_baset > &&st, message_handlert &mh)
 
- Public Member Functions inherited from ai_baset
  ai_baset (std::unique_ptr< ai_history_factory_baset > &&hf, std::unique_ptr< ai_domain_factory_baset > &&df, std::unique_ptr< ai_storage_baset > &&st, message_handlert &mh)
 
virtual  ~ai_baset ()
 
void  operator() (const irep_idt &function_id, const goto_programt &goto_program, const namespacet &ns)
  Run abstract interpretation on a single function.
 
void  operator() (const goto_functionst &goto_functions, const namespacet &ns)
  Run abstract interpretation on a whole program.
 
void  operator() (const abstract_goto_modelt &goto_model)
  Run abstract interpretation on a whole program.
 
void  operator() (const irep_idt &function_id, const goto_functionst::goto_functiont &goto_function, const namespacet &ns)
  Run abstract interpretation on a single function.
 
virtual ctrace_set_ptrt  abstract_traces_before (locationt l) const
  Returns all of the histories that have reached the start of the instruction.
 
virtual ctrace_set_ptrt  abstract_traces_after (locationt l) const
  Returns all of the histories that have reached the end of the instruction.
 
virtual cstate_ptrt  abstract_state_before (locationt l) const
  Get a copy of the abstract state before the given instruction, without needing to know what kind of domain or history is used.
 
virtual cstate_ptrt  abstract_state_after (locationt l) const
  Get a copy of the abstract state after the given instruction, without needing to know what kind of domain or history is used.
 
virtual cstate_ptrt  abstract_state_before (const trace_ptrt &p) const
  The same interfaces but with histories.
 
virtual cstate_ptrt  abstract_state_after (const trace_ptrt &p) const
 
virtual void  clear ()
  Reset the abstract state.
 
virtual void  output (const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
  Output the abstract states for a single function.
 
virtual jsont  output_json (const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program) const
  Output the abstract states for a single function as JSON.
 
virtual xmlt  output_xml (const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program) const
  Output the abstract states for a single function as XML.
 
virtual void  output (const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
  Output the abstract states for a whole program.
 
void  output (const goto_modelt &goto_model, std::ostream &out) const
  Output the abstract states for a whole program.
 
void  output (const namespacet &ns, const goto_functionst::goto_functiont &goto_function, std::ostream &out) const
  Output the abstract states for a function.
 
virtual jsont  output_json (const namespacet &ns, const goto_functionst &goto_functions) const
  Output the abstract states for the whole program as JSON.
 
jsont  output_json (const goto_modelt &goto_model) const
  Output the abstract states for a whole program as JSON.
 
jsont  output_json (const namespacet &ns, const goto_programt &goto_program) const
  Output the abstract states for a single function as JSON.
 
jsont  output_json (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
  Output the abstract states for a single function as JSON.
 
virtual xmlt  output_xml (const namespacet &ns, const goto_functionst &goto_functions) const
  Output the abstract states for the whole program as XML.
 
xmlt  output_xml (const goto_modelt &goto_model) const
  Output the abstract states for the whole program as XML.
 
xmlt  output_xml (const namespacet &ns, const goto_programt &goto_program) const
  Output the abstract states for a single function as XML.
 
xmlt  output_xml (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
  Output the abstract states for a single function as XML.
 
- Public Member Functions inherited from grapht< vs_dep_nodet >
node_indext  add_node (arguments &&... values)
 
void  swap (grapht &other)
 
bool  has_edge (node_indext i, node_indext j) const
 
const nodet &  operator[] (node_indext n) const
 
nodet &  operator[] (node_indext n)
 
void  resize (node_indext s)
 
std::size_t  size () const
 
bool  empty () const
 
const edgest &  in (node_indext n) const
 
const edgest &  out (node_indext n) const
 
void  add_edge (node_indext a, node_indext b)
 
void  remove_edge (node_indext a, node_indext b)
 
edget &  edge (node_indext a, node_indext b)
 
void  add_undirected_edge (node_indext a, node_indext b)
 
void  remove_undirected_edge (node_indext a, node_indext b)
 
void  remove_in_edges (node_indext n)
 
void  remove_out_edges (node_indext n)
 
void  remove_edges (node_indext n)
 
void  clear ()
 
void  shortest_path (node_indext src, node_indext dest, patht &path) const
 
void  shortest_loop (node_indext node, patht &path) const
 
void  visit_reachable (node_indext src)
 
std::vector< node_indext >  get_reachable (node_indext src, bool forwards) const
  Run depth-first search on the graph, starting from a single source node.
 
std::vector< node_indext >  get_reachable (const std::vector< node_indext > &src, bool forwards) const
  Run depth-first search on the graph, starting from multiple source nodes.
 
void  disconnect_unreachable (node_indext src)
  Removes any edges between nodes in a graph that are unreachable from a given start node.
 
void  disconnect_unreachable (const std::vector< node_indext > &src)
  Removes any edges between nodes in a graph that are unreachable from a vector of start nodes.
 
std::vector< typename N::node_indext >  depth_limited_search (typename N::node_indext src, std::size_t limit) const
  Run recursive depth-limited search on the graph, starting from multiple source nodes, to find the nodes reachable within n steps.
 
std::vector< typename N::node_indext >  depth_limited_search (std::vector< typename N::node_indext > &src, std::size_t limit) const
  Run recursive depth-limited search on the graph, starting from multiple source nodes, to find the nodes reachable within n steps.
 
void  make_chordal ()
  Ensure a graph is chordal (contains no 4+-cycles without an edge crossing the cycle) by adding extra edges.
 
std::size_t  connected_subgraphs (std::vector< node_indext > &subgraph_nr)
  Find connected subgraphs in an undirected graph.
 
std::size_t  SCCs (std::vector< node_indext > &subgraph_nr) const
  Computes strongly-connected components of a graph and yields a vector expressing a mapping from nodes to components indices.
 
bool  is_dag () const
 
std::list< node_indext >  topsort () const
  Find a topological order of the nodes if graph is DAG, return empty list for non-DAG or empty graph.
 
std::vector< node_indext >  get_predecessors (const node_indext &n) const
 
std::vector< node_indext >  get_successors (const node_indext &n) const
 
void  output_dot (std::ostream &out) const
 
void  for_each_predecessor (const node_indext &n, std::function< void(const node_indext &)> f) const
 
void  for_each_successor (const node_indext &n, std::function< void(const node_indext &)> f) const
 

Protected Member Functions

virtual statet &  get_state (locationt l)
 
variable_sensitivity_dependence_domaint &  operator[] (locationt l)
 
virtual statet &  get_state (trace_ptrt p)
  Get the state for the given history, creating it with the factory if it doesn't exist.
 
- Protected Member Functions inherited from ai_three_way_merget
bool  visit_edge_function_call (const irep_idt &calling_function_id, trace_ptrt p_call, locationt l_return, const irep_idt &callee_function_id, working_sett &working_set, const goto_programt &callee, const goto_functionst &goto_functions, const namespacet &ns) override
 
- Protected Member Functions inherited from ai_baset
virtual void  initialize (const irep_idt &function_id, const goto_functionst::goto_functiont &goto_function)
  Initialize all the abstract states for a single function.
 
virtual void  initialize (const goto_functionst &goto_functions)
  Initialize all the abstract states for a whole program.
 
trace_ptrt  entry_state (const goto_programt &goto_program)
  Set the abstract state of the entry location of a single function to the entry state required by the analysis.
 
trace_ptrt  entry_state (const goto_functionst &goto_functions)
  Set the abstract state of the entry location of a whole program to the entry state required by the analysis.
 
trace_ptrt  get_next (working_sett &working_set)
  Get the next location from the work queue.
 
void  put_in_working_set (working_sett &working_set, trace_ptrt t)
 
virtual bool  fixedpoint (trace_ptrt starting_trace, const irep_idt &function_id, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
  Run the fixedpoint algorithm until it reaches a fixed point.
 
virtual void  fixedpoint (trace_ptrt starting_trace, const goto_functionst &goto_functions, const namespacet &ns)
 
virtual bool  visit (const irep_idt &function_id, trace_ptrt p, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
  Perform one step of abstract interpretation from trace t Depending on the instruction type it may compute a number of "edges" or applications of the abstract transformer.
 
virtual bool  visit_function_call (const irep_idt &function_id, trace_ptrt p_call, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
 
virtual bool  visit_end_function (const irep_idt &function_id, trace_ptrt p, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
 
bool  visit_edge (const irep_idt &function_id, trace_ptrt p, const irep_idt &to_function_id, locationt to_l, trace_ptrt caller_history, const namespacet &ns, working_sett &working_set)
 
virtual bool  merge (const statet &src, trace_ptrt from, trace_ptrt to)
  Merge the state src, flowing from tracet from to tracet to, into the state currently stored for tracet to.
 
virtual std::unique_ptr< statet >  make_temporary_state (const statet &s)
  Make a copy of a state.
 
- Protected Member Functions inherited from grapht< vs_dep_nodet >
void  shortest_path (node_indext src, node_indext dest, patht &path, bool non_trivial) const
 
std::vector< typename N::node_indext >  depth_limited_search (std::vector< typename N::node_indext > &src, std::size_t limit, std::vector< bool > &visited) const
  Run recursive depth-limited search on the graph, starting from multiple source nodes, to find the nodes reachable within n steps.
 
void  tarjan (class tarjant &t, node_indext v) const
 

Protected Attributes

friend  variable_sensitivity_dependence_domain_factoryt
 
friend  variable_sensitivity_dependence_domaint
 
const goto_functionst &  goto_functions
 
const namespacet &  ns
 
post_dominators_mapt  post_dominators
 
- Protected Attributes inherited from ai_baset
std::unique_ptr< ai_history_factory_baset >  history_factory
  For creating history objects.
 
std::unique_ptr< ai_domain_factory_baset >  domain_factory
  For creating domain objects.
 
std::unique_ptr< ai_storage_baset >  storage
 
message_handlert &  message_handler
 
- Protected Attributes inherited from grapht< vs_dep_nodet >
nodest  nodes
 

Friends

class  variable_sensitivity_dependence_domaint
 

Additional Inherited Members

- Protected Types inherited from ai_baset
typedef trace_sett  working_sett
  The work queue, sorted using the history's ordering operator.
 

Detailed Description

Definition at line 217 of file variable_sensitivity_dependence_graph.h.

Member Typedef Documentation

◆  post_dominators_mapt

typedef std::map<irep_idt, cfg_post_dominatorst> variable_sensitivity_dependence_grapht::post_dominators_mapt

Definition at line 241 of file variable_sensitivity_dependence_graph.h.

Constructor & Destructor Documentation

◆  variable_sensitivity_dependence_grapht()

variable_sensitivity_dependence_grapht::variable_sensitivity_dependence_grapht ( const goto_functionst &  goto_functions,
const namespacet &  _ns,
variable_sensitivity_object_factory_ptrt  object_factory,
const vsd_configt &  _configuration,
message_handlert &  message_handler 
)
explicit

Definition at line 633 of file variable_sensitivity_dependence_graph.cpp.

Member Function Documentation

◆  add_dep()

void variable_sensitivity_dependence_grapht::add_dep ( vs_dep_edget::kindt  kind,
goto_programt::const_targett  from,
goto_programt::const_targett  to 
)

Definition at line 652 of file variable_sensitivity_dependence_graph.cpp.

◆  cfg_post_dominators()

post_dominators_mapt & variable_sensitivity_dependence_grapht::cfg_post_dominators ( )
inline

Definition at line 272 of file variable_sensitivity_dependence_graph.h.

◆  finalize()

void variable_sensitivity_dependence_grapht::finalize ( )
inlinevirtual

Override this to add a cleanup or post-processing step after fixedpoint has run.

Reimplemented from ai_baset.

Definition at line 256 of file variable_sensitivity_dependence_graph.h.

◆  get_state() [1/2]

virtual statet & variable_sensitivity_dependence_grapht::get_state ( locationt  l )
inlineprotectedvirtual

Definition at line 224 of file variable_sensitivity_dependence_graph.h.

◆  get_state() [2/2]

virtual statet & ai_baset::get_state ( trace_ptrt  p )
inlineprotectedvirtual

Get the state for the given history, creating it with the factory if it doesn't exist.

Reimplemented from ai_baset.

Definition at line 519 of file ai.h.

◆  initialize()

void variable_sensitivity_dependence_grapht::initialize ( const irep_idt &  function_id,
const goto_programt &  goto_program 
)
inlinevirtual

Initialize all the abstract states for a single function.

Override this to do custom per-domain initialization.

Reimplemented from ai_baset.

Definition at line 251 of file variable_sensitivity_dependence_graph.h.

◆  operator[]()

variable_sensitivity_dependence_domaint & variable_sensitivity_dependence_grapht::operator[] ( locationt  l )
inlineprotected

Definition at line 230 of file variable_sensitivity_dependence_graph.h.

Friends And Related Symbol Documentation

◆  variable_sensitivity_dependence_domaint

friend class variable_sensitivity_dependence_domaint
friend

Definition at line 239 of file variable_sensitivity_dependence_graph.h.

Member Data Documentation

◆  goto_functions

const goto_functionst& variable_sensitivity_dependence_grapht::goto_functions
protected

Definition at line 280 of file variable_sensitivity_dependence_graph.h.

◆  ns

const namespacet& variable_sensitivity_dependence_grapht::ns
protected

Definition at line 281 of file variable_sensitivity_dependence_graph.h.

◆  post_dominators

post_dominators_mapt variable_sensitivity_dependence_grapht::post_dominators
protected

Definition at line 283 of file variable_sensitivity_dependence_graph.h.

◆  variable_sensitivity_dependence_domain_factoryt

friend variable_sensitivity_dependence_grapht::variable_sensitivity_dependence_domain_factoryt
protected

Definition at line 278 of file variable_sensitivity_dependence_graph.h.

◆  variable_sensitivity_dependence_domaint

friend variable_sensitivity_dependence_grapht::variable_sensitivity_dependence_domaint
protected

Definition at line 279 of file variable_sensitivity_dependence_graph.h.

The documentation for this class was generated from the following files:

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