#include <invariant_propagation.h>

Inheritance diagram for invariant_propagationt:

Collaboration diagram for invariant_propagationt:

Public Types
typedef ait< invariant_set_domaint >	baset

Public Types inherited from ait< invariant_set_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
	invariant_propagationt (const namespacet &_ns, value_setst &_value_sets)

const invariant_sett &	lookup (locationt l) const

void	initialize (const irep_idt &function, const goto_programt &goto_program) override
	Initialize all the abstract states for a single function.

void	make_all_true ()

void	make_all_false ()

void	simplify (goto_programt &goto_program)

void	simplify (goto_functionst &goto_functions)

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

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

const invariant_set_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 Types
typedef std::list< unsigned >	object_listt

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

Protected Member Functions
void	add_objects (const goto_programt &goto_program)

void	add_objects (const goto_functionst &goto_functions)

void	get_objects (const symbolt &symbol, object_listt &dest)

void	get_objects_rec (const exprt &src, std::list< exprt > &dest)

void	get_globals (object_listt &globals)

bool	check_type (const typet &type) const

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

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

Protected Attributes
friend	invariant_set_domain_factoryt

const namespacet &	ns

value_setst &	value_sets

inv_object_storet	object_store

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

Definition at line 21 of file invariant_propagation.h.

Member Typedef Documentation

◆ baset

typedef ait<invariant_set_domaint> invariant_propagationt::baset

Definition at line 41 of file invariant_propagation.h.

◆ object_listt

typedef std::list<unsigned> invariant_propagationt::object_listt

protected

Definition at line 57 of file invariant_propagation.h.

Constructor & Destructor Documentation

◆ invariant_propagationt()

invariant_propagationt::invariant_propagationt	(	const namespacet &	_ns,
		value_setst &	_value_sets
	)

Definition at line 39 of file invariant_propagation.cpp.

Member Function Documentation

◆ add_objects() [1/2]

void invariant_propagationt::add_objects ( const goto_functionst & goto_functions )

protected

Definition at line 158 of file invariant_propagation.cpp.

◆ add_objects() [2/2]

void invariant_propagationt::add_objects ( const goto_programt & goto_program )

protected

Definition at line 66 of file invariant_propagation.cpp.

◆ check_type()

bool invariant_propagationt::check_type ( const typet & type ) const

protected

Definition at line 222 of file invariant_propagation.cpp.

◆ get_globals()

void invariant_propagationt::get_globals ( object_listt & globals )

protected

Definition at line 209 of file invariant_propagation.cpp.

◆ get_objects()

void invariant_propagationt::get_objects	(	const symbolt &	symbol,
		object_listt &	dest
	)

protected

Definition at line 112 of file invariant_propagation.cpp.

◆ get_objects_rec()

void invariant_propagationt::get_objects_rec	(	const exprt &	src,
		std::list< exprt > &	dest
	)

protected

Definition at line 124 of file invariant_propagation.cpp.

◆ initialize()

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

overridevirtual

Initialize all the abstract states for a single function.

Override this to do custom per-domain initialization.

Reimplemented from ai_baset.

Definition at line 243 of file invariant_propagation.cpp.

◆ lookup()

const invariant_sett & invariant_propagationt::lookup ( locationt l ) const

inline

Definition at line 27 of file invariant_propagation.h.

◆ make_all_false()

void invariant_propagationt::make_all_false ( )

Definition at line 58 of file invariant_propagation.cpp.

◆ make_all_true()

void invariant_propagationt::make_all_true ( )

Definition at line 50 of file invariant_propagation.cpp.

◆ simplify() [1/2]

void invariant_propagationt::simplify ( goto_functionst & goto_functions )

Definition at line 252 of file invariant_propagation.cpp.

◆ simplify() [2/2]

void invariant_propagationt::simplify ( goto_programt & goto_program )

Definition at line 258 of file invariant_propagation.cpp.

Member Data Documentation

◆ invariant_set_domain_factoryt

friend invariant_propagationt::invariant_set_domain_factoryt

protected

Definition at line 50 of file invariant_propagation.h.

◆ ns

const namespacet& invariant_propagationt::ns

protected

Definition at line 52 of file invariant_propagation.h.

◆ object_store

inv_object_storet invariant_propagationt::object_store

protected

Definition at line 55 of file invariant_propagation.h.

◆ value_sets

value_setst& invariant_propagationt::value_sets

protected

Definition at line 53 of file invariant_propagation.h.

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

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

Public Types

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ baset

◆ object_listt

Constructor & Destructor Documentation

◆ invariant_propagationt()

Member Function Documentation

◆ add_objects() [1/2]

◆ add_objects() [2/2]

◆ check_type()

◆ get_globals()

◆ get_objects()

◆ get_objects_rec()

◆ initialize()

◆ lookup()

◆ make_all_false()

◆ make_all_true()

◆ simplify() [1/2]

◆ simplify() [2/2]

Member Data Documentation

◆ invariant_set_domain_factoryt

◆ ns

◆ object_store

◆ value_sets