cprover
invariant_propagationt Class Reference

#include <invariant_propagation.h>

+ Inheritance diagram for invariant_propagationt:
+ Collaboration diagram for invariant_propagationt:

Public Types

typedef ait< invariant_set_domaintbaset
 
- 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 goto_programt::const_targett locationt
 

Public Member Functions

 invariant_propagationt (const namespacet &_ns, value_setst &_value_sets)
 
const invariant_settlookup (locationt l) const
 
virtual void initialize (const goto_programt &goto_program)
 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...
 
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 ()
 
invariant_set_domaintoperator[] (locationt l)
 
const invariant_set_domaintoperator[] (locationt l) const
 
std::unique_ptr< statetabstract_state_before (locationt t) const override
 Get a copy of the abstract state before the given instruction, without needing to know what kind of domain or history is used. More...
 
void clear () override
 Reset the abstract state. More...
 
- Public Member Functions inherited from ai_baset
 ai_baset ()
 
virtual ~ai_baset ()
 
void operator() (const irep_idt &function_identifier, 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 goto_modelt &goto_model)
 Run abstract interpretation on a whole program. More...
 
void operator() (const irep_idt &function_identifier, const goto_functionst::goto_functiont &goto_function, const namespacet &ns)
 Run abstract interpretation on a single function. More...
 
virtual std::unique_ptr< statetabstract_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 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_programt &goto_program, std::ostream &out) const
 Output the abstract states for a function. 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

typedef std::list< unsigned > object_listt
 
- Protected Types inherited from ait< invariant_set_domaint >
typedef std::unordered_map< locationt, invariant_set_domaint, const_target_hash, pointee_address_equaltstate_mapt
 
- Protected Types inherited from ai_baset
typedef std::map< unsigned, locationtworking_sett
 The work queue, sorted by location number. More...
 

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 statetget_state (locationt l) override
 Get the state for the given location, creating it in a default way if it doesn't exist. More...
 
const statetfind_state (locationt l) const override
 Get the state for the given location if it already exists; throw an exception if it doesn't. More...
 
bool merge (const statet &src, locationt from, locationt to) override
 
std::unique_ptr< statetmake_temporary_state (const statet &s) override
 Make a copy of a state. More...
 
void fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) override
 
- Protected Member Functions inherited from ai_baset
virtual void initialize (const goto_functionst::goto_functiont &goto_function)
 Initialize all the abstract states for a single function. More...
 
virtual void finalize ()
 Override this to add a cleanup or post-processing step after fixedpoint has run. More...
 
void 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...
 
void 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...
 
virtual void output (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier, std::ostream &out) const
 Output the abstract states for a single function. More...
 
virtual jsont output_json (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier) const
 Output the abstract states for a single function as JSON. More...
 
virtual xmlt output_xml (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier) const
 Output the abstract states for a single function as XML. More...
 
locationt get_next (working_sett &working_set)
 Get the next location from the work queue. More...
 
void put_in_working_set (working_sett &working_set, locationt l)
 
bool fixedpoint (const irep_idt &function_identifier, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
 Run the fixedpoint algorithm until it reaches a fixed point. More...
 
void sequential_fixedpoint (const goto_functionst &goto_functions, const namespacet &ns)
 
void concurrent_fixedpoint (const goto_functionst &goto_functions, const namespacet &ns)
 
bool visit (const irep_idt &function_identifier, locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
 Perform one step of abstract interpretation from location l Depending on the instruction type it may compute a number of "edges" or applications of the abstract transformer. More...
 
bool do_function_call_rec (const irep_idt &calling_function_identifier, locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, const goto_functionst &goto_functions, const namespacet &ns)
 
bool do_function_call (const irep_idt &calling_function_identifier, locationt l_call, locationt l_return, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, const namespacet &ns)
 

Protected Attributes

const namespacetns
 
value_setstvalue_sets
 
inv_object_storet object_store
 
- Protected Attributes inherited from ait< invariant_set_domaint >
state_mapt state_map
 

Detailed Description

Definition at line 20 of file invariant_propagation.h.

Member Typedef Documentation

◆ baset

◆ object_listt

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

Definition at line 56 of file invariant_propagation.h.

Constructor & Destructor Documentation

◆ invariant_propagationt()

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

Definition at line 24 of file invariant_propagation.h.

Member Function Documentation

◆ add_objects() [1/2]

void invariant_propagationt::add_objects ( const goto_programt goto_program)
protected

Definition at line 31 of file invariant_propagation.cpp.

◆ add_objects() [2/2]

void invariant_propagationt::add_objects ( const goto_functionst goto_functions)
protected

Definition at line 119 of file invariant_propagation.cpp.

◆ check_type()

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

Definition at line 183 of file invariant_propagation.cpp.

◆ get_globals()

void invariant_propagationt::get_globals ( object_listt globals)
protected

Definition at line 170 of file invariant_propagation.cpp.

◆ get_objects()

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

Definition at line 77 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 89 of file invariant_propagation.cpp.

◆ initialize() [1/2]

void invariant_propagationt::initialize ( const goto_programt goto_program)
virtual

Initialize all the abstract states for a single function.

Override this to do custom per-domain initialization.

Reimplemented from ai_baset.

Definition at line 203 of file invariant_propagation.cpp.

◆ initialize() [2/2]

void invariant_propagationt::initialize ( const goto_functionst goto_functions)
virtual

Initialize all the abstract states for a whole program.

Override this to do custom per-analysis initialization.

Reimplemented from ai_baset.

Definition at line 224 of file invariant_propagation.cpp.

◆ lookup()

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

Definition at line 34 of file invariant_propagation.h.

◆ make_all_false()

void invariant_propagationt::make_all_false ( )

Definition at line 25 of file invariant_propagation.cpp.

◆ make_all_true()

void invariant_propagationt::make_all_true ( )

Definition at line 19 of file invariant_propagation.cpp.

◆ simplify() [1/2]

void invariant_propagationt::simplify ( goto_programt goto_program)

Definition at line 238 of file invariant_propagation.cpp.

◆ simplify() [2/2]

void invariant_propagationt::simplify ( goto_functionst goto_functions)

Definition at line 232 of file invariant_propagation.cpp.

Member Data Documentation

◆ ns

const namespacet& invariant_propagationt::ns
protected

Definition at line 51 of file invariant_propagation.h.

◆ object_store

inv_object_storet invariant_propagationt::object_store
protected

Definition at line 54 of file invariant_propagation.h.

◆ value_sets

value_setst& invariant_propagationt::value_sets
protected

Definition at line 52 of file invariant_propagation.h.


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