Base class for concurrency-aware abstract interpretation. More...

#include <ai.h>

Inheritance diagram for concurrency_aware_ait< domainT >:

Collaboration diagram for concurrency_aware_ait< domainT >:

Public Types
using	statet = typename ait< domainT >::statet

using	locationt = typename statet::locationt

Public Types inherited from ait< domainT >
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
	concurrency_aware_ait ()

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

virtual bool	merge_shared (const statet &src, locationt from, locationt to, const namespacet &ns)

Public Member Functions inherited from ait< domainT >
	ait ()

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

const domainT &	operator[] (locationt l) const
	Find the analysis result for a given location. More...

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

void	operator() (const goto_functionst &goto_functions, const namespacet &ns)
	Run abstract interpretation on a whole program. More...

void	operator() (const abstract_goto_modelt &goto_model)
	Run abstract interpretation on a whole program. More...

void	operator() (const irep_idt &function_id, const goto_functionst::goto_functiont &goto_function, const namespacet &ns)
	Run abstract interpretation on a single function. More...

virtual ctrace_set_ptrt	abstract_traces_before (locationt l) const
	Returns all of the histories that have reached the start of the instruction. More...

virtual ctrace_set_ptrt	abstract_traces_after (locationt l) const
	Returns all of the histories that have reached the end of the instruction. More...

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

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

virtual cstate_ptrt	abstract_state_before (const trace_ptrt &p) const
	The same interfaces but with histories. More...

virtual cstate_ptrt	abstract_state_after (const trace_ptrt &p) const

virtual void	clear ()
	Reset the abstract state. More...

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

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

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

virtual void	output (const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
	Output the abstract states for a whole program. More...

void	output (const goto_modelt &goto_model, std::ostream &out) const
	Output the abstract states for a whole program. More...

void	output (const namespacet &ns, const goto_functionst::goto_functiont &goto_function, std::ostream &out) const
	Output the abstract states for a function. More...

virtual jsont	output_json (const namespacet &ns, const goto_functionst &goto_functions) const
	Output the abstract states for the whole program as JSON. More...

jsont	output_json (const goto_modelt &goto_model) const
	Output the abstract states for a whole program as JSON. More...

jsont	output_json (const namespacet &ns, const goto_programt &goto_program) const
	Output the abstract states for a single function as JSON. More...

jsont	output_json (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
	Output the abstract states for a single function as JSON. More...

virtual xmlt	output_xml (const namespacet &ns, const goto_functionst &goto_functions) const
	Output the abstract states for the whole program as XML. More...

xmlt	output_xml (const goto_modelt &goto_model) const
	Output the abstract states for the whole program as XML. More...

xmlt	output_xml (const namespacet &ns, const goto_programt &goto_program) const
	Output the abstract states for a single function as XML. More...

xmlt	output_xml (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
	Output the abstract states for a single function as XML. More...

Protected Types
using	working_sett = ai_baset::working_sett

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

Protected Member Functions
void	fixedpoint (ai_baset::trace_ptrt start_trace, const goto_functionst &goto_functions, const namespacet &ns) override

Protected Member Functions inherited from ait< domainT >
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. More...

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

virtual void	initialize (const irep_idt &function_id, const goto_functionst::goto_functiont &goto_function)
	Initialize all the abstract states for a single function. More...

virtual void	initialize (const goto_functionst &goto_functions)
	Initialize all the abstract states for a whole program. More...

virtual void	finalize ()
	Override this to add a cleanup or post-processing step after fixedpoint has run. More...

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

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

trace_ptrt	get_next (working_sett &working_set)
	Get the next location from the work queue. More...

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

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

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

virtual std::unique_ptr< statet >	make_temporary_state (const statet &s)
	Make a copy of a state. More...

virtual statet &	get_state (trace_ptrt p)
	Get the state for the given history, creating it with the factory if it doesn't exist. More...

Additional Inherited Members
Protected Attributes inherited from ai_baset
std::unique_ptr< ai_history_factory_baset >	history_factory
	For creating history objects. More...

std::unique_ptr< ai_domain_factory_baset >	domain_factory
	For creating domain objects. More...

std::unique_ptr< ai_storage_baset >	storage

message_handlert &	message_handler

Detailed Description

template<typename domainT>
class concurrency_aware_ait< domainT >

Base class for concurrency-aware abstract interpretation.

See ait for details. The only difference is that after the sequential fixed point construction, as done by ait, another step is added to account for concurrently-executed instructions. Basically, it makes the analysis flow-insensitive by feeding results of a sequential execution back into the entry point, thereby accounting for any values computed by different threads. Compare [Martin Rinard, "Analysis of Multi-Threaded Programs", SAS 2001]( http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.28.4747& rep=rep1&type=pdf).

Template Parameters

domainT A type derived from ai_domain_baset that represents the values in the AI domain

It is important to note that the domains used by this need an extra merge method, but, far more critically, they need the property that it is not possible to "undo" changes to the domain. Tracking last modified location has this property, numerical domains such as constants and intervals do not and using this kind of concurrent analysis for these domains may miss significant behaviours.

Definition at line 650 of file ai.h.

Member Typedef Documentation

◆ locationt

template<typename domainT >

using concurrency_aware_ait< domainT >::locationt = typename statet::locationt

Definition at line 654 of file ai.h.

◆ statet

template<typename domainT >

using concurrency_aware_ait< domainT >::statet = typename ait<domainT>::statet

Definition at line 653 of file ai.h.

◆ working_sett

template<typename domainT >

using concurrency_aware_ait< domainT >::working_sett = ai_baset::working_sett

protected

Definition at line 677 of file ai.h.

Constructor & Destructor Documentation

◆ concurrency_aware_ait() [1/2]

template<typename domainT >

concurrency_aware_ait< domainT >::concurrency_aware_ait ( )

inline

Definition at line 657 of file ai.h.

◆ concurrency_aware_ait() [2/2]

template<typename domainT >

concurrency_aware_ait< domainT >::concurrency_aware_ait ( std::unique_ptr< ai_domain_factory_baset > && df )

inlineexplicit

Definition at line 660 of file ai.h.

Member Function Documentation

◆ fixedpoint()

template<typename domainT >

void concurrency_aware_ait< domainT >::fixedpoint	(	ai_baset::trace_ptrt	start_trace,
		const goto_functionst &	goto_functions,
		const namespacet &	ns
	)

inlineoverrideprotectedvirtual

Reimplemented from ai_baset.

Definition at line 679 of file ai.h.

◆ merge_shared()

template<typename domainT >

virtual bool concurrency_aware_ait< domainT >::merge_shared	(	const statet &	src,
		locationt	from,
		locationt	to,
		const namespacet &	ns
	)

inlinevirtual

Definition at line 665 of file ai.h.

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

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

Public Types

Public Member Functions

Protected Types

Protected Member Functions

Additional Inherited Members

Detailed Description

template<typename domainT> class concurrency_aware_ait< domainT >

Member Typedef Documentation

◆ locationt

◆ statet

◆ working_sett

Constructor & Destructor Documentation

◆ concurrency_aware_ait() [1/2]

◆ concurrency_aware_ait() [2/2]

Member Function Documentation

◆ fixedpoint()

◆ merge_shared()

template<typename domainT>
class concurrency_aware_ait< domainT >