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

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.

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 Attributes

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

This is the basic interface of the abstract interpreter with default implementations of the core functionality.

Users of abstract interpreters should use the interface given by this class. It breaks into three categories:

Running an analysis, via operator()(const irep_idt&,const goto_programt&, const namespacet&), ai_baset::operator()(const goto_functionst&,const namespacet&) and ai_baset::operator()(const abstract_goto_modelt&)
Accessing the results of an analysis, by looking up the history objects for a given location l using ai_baset::abstract_traces_before(locationt)const or the domains using ai_baset::abstract_state_before(locationt)const
Outputting the results of the analysis; see ai_baset::output(const namespacet&, const irep_idt&, const goto_programt&, std::ostream&)const et cetera.

Where possible, uses should be agnostic of the particular configuration of the abstract interpreter. The "tasks" that goto-analyze uses are good examples of how to do this.

From a development point of view, there are several directions in which this can be extended by inheriting from ai_baset or one of its children:

A. To change how single edges are computed ait::visit_edge and ait::visit_edge_function_call ai_recursive_interproceduralt uses this to recurse to evaluate function calls rather than approximating them as ai_baset does.

B. To change how individual instructions are handled ait::visit() and related functions.

C. To change the way that the fixed point is computed ait::fixedpoint() concurrency_aware_ait does this to compute a fixed point over threads.

D. For pre-analysis initialization ait::initialize(const irep_idt&, const goto_programt&), ait::initialize(const irep_idt&, const goto_functionst::goto_functiont&) and ait::initialize(const goto_functionst&),

E. For post-analysis cleanup ait::finalize(),

Historically, uses of abstract interpretation inherited from ait<domainT> and added the necessary functionality. This works (although care must be taken to respect the APIs of the various components – there are some hacks to support older analyses that didn't) but is discouraged in favour of having an object for the abstract interpreter and using its public API.

Definition at line 116 of file ai.h.

Member Typedef Documentation

◆ cstate_ptrt

typedef ai_storage_baset::cstate_ptrt ai_baset::cstate_ptrt

Definition at line 120 of file ai.h.

◆ ctrace_set_ptrt

typedef ai_storage_baset::ctrace_set_ptrt ai_baset::ctrace_set_ptrt

Definition at line 123 of file ai.h.

◆ locationt

typedef goto_programt::const_targett ai_baset::locationt

Definition at line 124 of file ai.h.

◆ statet

typedef ai_domain_baset ai_baset::statet

Definition at line 119 of file ai.h.

◆ trace_ptrt

typedef ai_history_baset::trace_ptrt ai_baset::trace_ptrt

Definition at line 121 of file ai.h.

◆ trace_sett

typedef ai_history_baset::trace_sett ai_baset::trace_sett

Definition at line 122 of file ai.h.

◆ working_sett

typedef trace_sett ai_baset::working_sett

protected

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

Definition at line 418 of file ai.h.

Constructor & Destructor Documentation

◆ ai_baset()

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

)

inline

Definition at line 126 of file ai.h.

◆ ~ai_baset()

virtual ai_baset::~ai_baset ( )

inlinevirtual

Definition at line 138 of file ai.h.

Member Function Documentation

◆ abstract_state_after() [1/2]

virtual cstate_ptrt ai_baset::abstract_state_after ( const trace_ptrt & p ) const

inlinevirtual

Definition at line 252 of file ai.h.

◆ abstract_state_after() [2/2]

virtual cstate_ptrt ai_baset::abstract_state_after ( locationt l ) const

inlinevirtual

Get a copy of the abstract state after the given instruction, without needing to know what kind of domain or history is used.

Note: intended for users of the abstract interpreter; derived classes should use get_state to access the actual underlying state.

Parameters: l The location before which we want the abstract state

Returns: The abstract state after l. We return a pointer to a copy as the method should be const and there are some non-trivial cases including merging abstract states, etc.

PRECONDITION(l is dereferenceable && std::next(l) is dereferenceable) Check relies on a DATA_INVARIANT of goto_programs

Definition at line 238 of file ai.h.

◆ abstract_state_before() [1/2]

virtual cstate_ptrt ai_baset::abstract_state_before ( const trace_ptrt & p ) const

inlinevirtual

The same interfaces but with histories.

Definition at line 247 of file ai.h.

◆ abstract_state_before() [2/2]

virtual cstate_ptrt ai_baset::abstract_state_before ( locationt l ) const

inlinevirtual

Get a copy of the abstract state before the given instruction, without needing to know what kind of domain or history is used.

Note: intended for users of the abstract interpreter; derived classes should use get_state to access the actual underlying state. PRECONDITION(l is dereferenceable)

Parameters: l The location before which we want the abstract state

Returns: The abstract state before l. We return a pointer to a copy as the method should be const and there are some non-trivial cases including merging abstract states, etc.

Definition at line 225 of file ai.h.

◆ abstract_traces_after()

virtual ctrace_set_ptrt ai_baset::abstract_traces_after ( locationt l ) const

inlinevirtual

Returns all of the histories that have reached the end of the instruction.

PRECONDITION(l is dereferenceable)

Parameters: l The location before which we want the set of histories

Returns: The set of histories before l.

PRECONDITION(l is dereferenceable && std::next(l) is dereferenceable) Check relies on a DATA_INVARIANT of goto_programs

Definition at line 208 of file ai.h.

◆ abstract_traces_before()

virtual ctrace_set_ptrt ai_baset::abstract_traces_before ( locationt l ) const

inlinevirtual

Returns all of the histories that have reached the start of the instruction.

PRECONDITION(l is dereferenceable)

Parameters: l The location before which we want the set of histories

Returns: The set of histories before l.

Definition at line 198 of file ai.h.

◆ clear()

virtual void ai_baset::clear ( )

inlinevirtual

Reset the abstract state.

Definition at line 269 of file ai.h.

◆ entry_state() [1/2]

ai_baset::trace_ptrt ai_baset::entry_state ( const goto_functionst & goto_functions )

protected

Set the abstract state of the entry location of a whole program to the entry state required by the analysis.

Definition at line 165 of file ai.cpp.

◆ entry_state() [2/2]

ai_baset::trace_ptrt ai_baset::entry_state ( const goto_programt & goto_program )

protected

Set the abstract state of the entry location of a single function to the entry state required by the analysis.

Definition at line 179 of file ai.cpp.

◆ finalize()

void ai_baset::finalize ( )

protectedvirtual

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

Reimplemented in dependence_grapht, and variable_sensitivity_dependence_grapht.

Definition at line 209 of file ai.cpp.

◆ fixedpoint() [1/2]

void ai_baset::fixedpoint ( trace_ptrt starting_trace,

const goto_functionst & goto_functions,

const namespacet & ns

)

protectedvirtual

Reimplemented in concurrency_aware_ait< domainT >, and concurrency_aware_ait< rd_range_domaint >.

Definition at line 258 of file ai.cpp.

◆ fixedpoint() [2/2]

bool ai_baset::fixedpoint ( trace_ptrt starting_trace,

const irep_idt & function_id,

const goto_programt & goto_program,

const goto_functionst & goto_functions,

const namespacet & ns

)

protectedvirtual

Run the fixedpoint algorithm until it reaches a fixed point.

Returns: True if we found something new

Definition at line 232 of file ai.cpp.

◆ get_next()

ai_baset::trace_ptrt ai_baset::get_next ( working_sett & working_set )

protected

Get the next location from the work queue.

Definition at line 214 of file ai.cpp.

◆ get_state()

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 in ait< domainT >, ait< constant_propagator_domaint >, ait< custom_bitvector_domaint >, ait< dep_graph_domaint >, ait< escape_domaint >, ait< global_may_alias_domaint >, ait< invariant_set_domaint >, ait< rd_range_domaint >, ait< uninitialized_domaint >, ait< VSDT >, and variable_sensitivity_dependence_grapht.

Definition at line 519 of file ai.h.

◆ initialize() [1/3]

void ai_baset::initialize ( const goto_functionst & goto_functions )

protectedvirtual

Initialize all the abstract states for a whole program.

Override this to do custom per-analysis initialization.

Reimplemented in escape_analysist, global_may_alias_analysist, custom_bitvector_analysist, dependence_grapht, and reaching_definitions_analysist.

Definition at line 203 of file ai.cpp.

◆ initialize() [2/3]

void ai_baset::initialize ( const irep_idt & function_id,

const goto_functionst::goto_functiont & goto_function

)

protectedvirtual

Initialize all the abstract states for a single function.

Definition at line 190 of file ai.cpp.

◆ initialize() [3/3]

void ai_baset::initialize ( const irep_idt & function_id,

const goto_programt & goto_program

)

protectedvirtual

Initialize all the abstract states for a single function.

Override this to do custom per-domain initialization.

Reimplemented in dependence_grapht, invariant_propagationt, and variable_sensitivity_dependence_grapht.

Definition at line 197 of file ai.cpp.

◆ make_temporary_state()

virtual std::unique_ptr< statet > ai_baset::make_temporary_state ( const statet & s )

inlineprotectedvirtual

Make a copy of a state.

Definition at line 509 of file ai.h.

◆ merge()

virtual bool ai_baset::merge ( const statet & src,

trace_ptrt from,

trace_ptrt to

)

inlineprotectedvirtual

Merge the state src, flowing from tracet from to tracet to, into the state currently stored for tracet to.

Definition at line 502 of file ai.h.

◆ operator()() [1/4]

void ai_baset::operator() ( const abstract_goto_modelt & goto_model )

inline

Run abstract interpretation on a whole program.

Definition at line 169 of file ai.h.

◆ operator()() [2/4]

void ai_baset::operator() ( const goto_functionst & goto_functions,

const namespacet & ns

)

inline

Run abstract interpretation on a whole program.

Definition at line 157 of file ai.h.

◆ operator()() [3/4]

void ai_baset::operator() ( const irep_idt & function_id,

const goto_functionst::goto_functiont & goto_function,

const namespacet & ns

)

inline

Run abstract interpretation on a single function.

Definition at line 180 of file ai.h.

◆ operator()() [4/4]

void ai_baset::operator() ( const irep_idt & function_id,

const goto_programt & goto_program,

const namespacet & ns

)

inline

Run abstract interpretation on a single function.

Definition at line 143 of file ai.h.

◆ output() [1/4]

void ai_baset::output ( const goto_modelt & goto_model,

std::ostream & out

) const

inline

Output the abstract states for a whole program.

Definition at line 315 of file ai.h.

◆ output() [2/4]

void ai_baset::output ( const namespacet & ns,

const goto_functionst & goto_functions,

std::ostream & out

) const

virtual

Output the abstract states for a whole program.

Definition at line 20 of file ai.cpp.

◆ output() [3/4]

void ai_baset::output ( const namespacet & ns,

const goto_functionst::goto_functiont & goto_function,

std::ostream & out

) const

inline

Output the abstract states for a function.

Definition at line 324 of file ai.h.

◆ output() [4/4]

void ai_baset::output ( const namespacet & ns,

const irep_idt & function_id,

const goto_programt & goto_program,

std::ostream & out

) const

virtual

Output the abstract states for a single function.

Parameters: ns The namespace

function_id The identifier used to find a symbol to identify the goto_program's source language

goto_program The goto program

out The ostream to direct output to

Definition at line 39 of file ai.cpp.

◆ output_json() [1/5]

jsont ai_baset::output_json ( const goto_modelt & goto_model ) const

inline

Output the abstract states for a whole program as JSON.

Definition at line 338 of file ai.h.

◆ output_json() [2/5]

jsont ai_baset::output_json ( const namespacet & ns,

const goto_functionst & goto_functions

) const

virtual

Output the abstract states for the whole program as JSON.

Definition at line 61 of file ai.cpp.

◆ output_json() [3/5]

jsont ai_baset::output_json ( const namespacet & ns,

const goto_functionst::goto_functiont & goto_function

) const

inline

Output the abstract states for a single function as JSON.

Definition at line 354 of file ai.h.

◆ output_json() [4/5]

jsont ai_baset::output_json ( const namespacet & ns,

const goto_programt & goto_program

) const

inline

Output the abstract states for a single function as JSON.

Definition at line 346 of file ai.h.

◆ output_json() [5/5]

jsont ai_baset::output_json ( const namespacet & ns,

const irep_idt & function_id,

const goto_programt & goto_program

) const

virtual

Output the abstract states for a single function as JSON.

Parameters: ns The namespace

goto_program The goto program

function_id The identifier used to find a symbol to identify the source language

Returns: The JSON object

Definition at line 83 of file ai.cpp.

◆ output_xml() [1/5]

xmlt ai_baset::output_xml ( const goto_modelt & goto_model ) const

inline

Output the abstract states for the whole program as XML.

Definition at line 367 of file ai.h.

◆ output_xml() [2/5]

xmlt ai_baset::output_xml ( const namespacet & ns,

const goto_functionst & goto_functions

) const

virtual

Output the abstract states for the whole program as XML.

Definition at line 110 of file ai.cpp.

◆ output_xml() [3/5]

xmlt ai_baset::output_xml ( const namespacet & ns,

const goto_functionst::goto_functiont & goto_function

) const

inline

Output the abstract states for a single function as XML.

Definition at line 383 of file ai.h.

◆ output_xml() [4/5]

xmlt ai_baset::output_xml ( const namespacet & ns,

const goto_programt & goto_program

) const

inline

Output the abstract states for a single function as XML.

Definition at line 375 of file ai.h.

◆ output_xml() [5/5]

xmlt ai_baset::output_xml ( const namespacet & ns,

const irep_idt & function_id,

const goto_programt & goto_program

) const

virtual

Output the abstract states for a single function as XML.

Parameters: ns The namespace

goto_program The goto program

function_id The identifier used to find a symbol to identify the source language

Returns: The XML object

Definition at line 136 of file ai.cpp.

◆ put_in_working_set()

void ai_baset::put_in_working_set ( working_sett & working_set,

trace_ptrt t

)

inlineprotected

Definition at line 423 of file ai.h.

◆ visit()

bool ai_baset::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

)

protectedvirtual

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.

Returns: True if the state was changed

Definition at line 270 of file ai.cpp.

◆ visit_edge()

bool ai_baset::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

)

protected

Definition at line 331 of file ai.cpp.

◆ visit_edge_function_call()

bool ai_baset::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

)

protectedvirtual

Reimplemented in ai_recursive_interproceduralt, and ai_three_way_merget.

Definition at line 416 of file ai.cpp.

◆ visit_end_function()

bool ai_baset::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

)

protectedvirtual

Definition at line 523 of file ai.cpp.

◆ visit_function_call()

bool ai_baset::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

)

protectedvirtual

Definition at line 444 of file ai.cpp.

Member Data Documentation

◆ domain_factory

std::unique_ptr<ai_domain_factory_baset> ai_baset::domain_factory

protected

For creating domain objects.

Definition at line 498 of file ai.h.

◆ history_factory

std::unique_ptr<ai_history_factory_baset> ai_baset::history_factory

protected

For creating history objects.

Definition at line 495 of file ai.h.

◆ message_handler

message_handlert& ai_baset::message_handler

protected

Definition at line 525 of file ai.h.

◆ storage

std::unique_ptr<ai_storage_baset> ai_baset::storage

protected

Definition at line 515 of file ai.h.

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

/home/runner/work/cbmc/cbmc/src/analyses/ai.h
/home/runner/work/cbmc/cbmc/src/analyses/ai.cpp