Loading...

Searching...

No Matches

ait< domainT > Class Template Reference

ait supplies three of the four components needed: an abstract interpreter (in this case handling function calls via recursion), a history factory (using the simplest possible history objects) and storage (one domain per location). More...

#include <ai.h>

+ Inheritance diagram for ait< domainT >:

[フレーム]

[legend]

+ Collaboration diagram for ait< domainT >:

[フレーム]

[legend]

Public Types

typedef goto_programt::const_targett locationt

- 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 Member Functions

ait ()

ait (std::unique_ptr< ai_domain_factory_baset > &&df)

const domainT & operator[] (locationt l) const

Find the analysis result for a given location.

- 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.

Protected Member Functions

virtual statet & get_state (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_recursive_interproceduralt

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_programt &goto_program)

Initialize all the abstract states for a single function.

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.

virtual void finalize ()

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

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.

Private Member Functions

void dummy (const domainT &s)

This function exists to enforce that domainT is derived from ai_domain_baset.

Private Attributes

null_message_handlert no_logging

Additional Inherited Members

- Protected Types inherited from ai_baset

typedef trace_sett working_sett

The work queue, sorted using the history's ordering operator.

- 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

Detailed Description

template<typename domainT>
class ait< domainT >

ait supplies three of the four components needed: an abstract interpreter (in this case handling function calls via recursion), a history factory (using the simplest possible history objects) and storage (one domain per location).

The fourth component, the domain, is provided by the template parameter. This is gives a "classical" abstract interpreter and is backwards compatible with older code.