cprover
ai_baset Class Referenceabstract

The basic interface of an abstract interpreter. More...

#include <ai.h>

+ Inheritance diagram for ai_baset:

Public Types

typedef ai_domain_baset statet
 
typedef goto_programt::const_targett locationt
 

Public Member Functions

 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_before (locationt l) const =0
 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 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 clear ()
 Reset the abstract state. 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::map< unsigned, locationtworking_sett
 The work queue, sorted by location number. More...
 

Protected Member Functions

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_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...
 
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...
 
virtual void fixedpoint (const goto_functionst &goto_functions, const namespacet &ns)=0
 
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)
 
virtual bool merge (const statet &src, locationt from, locationt to)=0
 
virtual bool merge_shared (const statet &src, locationt from, locationt to, const namespacet &ns)=0
 
virtual statetget_state (locationt l)=0
 Get the state for the given location, creating it in a default way if it doesn't exist. More...
 
virtual const statetfind_state (locationt l) const =0
 Get the state for the given location if it already exists; throw an exception if it doesn't. More...
 
virtual std::unique_ptr< statetmake_temporary_state (const statet &s)=0
 Make a copy of a state. More...
 

Detailed Description

The basic interface of an abstract interpreter.

This should be enough to create, run and query an abstract interpreter.

Note: this is just a base class. ait should be used instead.

Definition at line 32 of file ai.h.

Member Typedef Documentation

◆ locationt

Definition at line 36 of file ai.h.

◆ statet

Definition at line 35 of file ai.h.

◆ working_sett

typedef std::map<unsigned, locationt> ai_baset::working_sett
protected

The work queue, sorted by location number.

Definition at line 277 of file ai.h.

Constructor & Destructor Documentation

◆ ai_baset()

ai_baset::ai_baset ( )
inline

Definition at line 38 of file ai.h.

◆ ~ai_baset()

virtual ai_baset::~ai_baset ( )
inlinevirtual

Definition at line 42 of file ai.h.

Member Function Documentation

◆ abstract_state_after()

virtual std::unique_ptr<statet> 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 or find_state to access the actual underlying state.

Parameters
lThe 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 114 of file ai.h.

◆ abstract_state_before()

virtual std::unique_ptr<statet> ai_baset::abstract_state_before ( locationt  l) const
pure virtual

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 or find_state to access the actual underlying state. PRECONDITION(l is dereferenceable)

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

Implemented in ait< domainT >, ait< escape_domaint >, ait< invariant_set_domaint >, ait< global_may_alias_domaint >, ait< rd_range_domaint >, ait< constant_propagator_domaint >, ait< uninitialized_domaint >, ait< custom_bitvector_domaint >, and ait< dep_graph_domaint >.

◆ clear()

◆ concurrent_fixedpoint()

void ai_baset::concurrent_fixedpoint ( const goto_functionst goto_functions,
const namespacet ns 
)
protected

Definition at line 456 of file ai.cpp.

◆ do_function_call()

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

Definition at line 325 of file ai.cpp.

◆ do_function_call_rec()

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

Definition at line 405 of file ai.cpp.

◆ entry_state() [1/2]

void 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 191 of file ai.cpp.

◆ entry_state() [2/2]

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

Definition at line 216 of file ai.cpp.

◆ find_state()

virtual const statet& ai_baset::find_state ( locationt  l) const
protectedpure virtual

◆ fixedpoint() [1/2]

bool ai_baset::fixedpoint ( const irep_idt function_identifier,
const goto_programt goto_program,
const goto_functionst goto_functions,
const namespacet ns 
)
protected

Run the fixedpoint algorithm until it reaches a fixed point.

Returns
True if we found something new

Definition at line 233 of file ai.cpp.

◆ fixedpoint() [2/2]

◆ get_next()

ai_baset::locationt ai_baset::get_next ( working_sett working_set)
protected

Get the next location from the work queue.

Definition at line 221 of file ai.cpp.

◆ get_state()

◆ initialize() [1/3]

void ai_baset::initialize ( 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, and invariant_propagationt.

Definition at line 202 of file ai.cpp.

◆ initialize() [2/3]

void ai_baset::initialize ( const goto_functionst::goto_functiont goto_function)
protectedvirtual

Initialize all the abstract states for a single function.

Definition at line 197 of file ai.cpp.

◆ initialize() [3/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 reaching_definitions_analysist, dependence_grapht, custom_bitvector_analysist, escape_analysist, global_may_alias_analysist, and invariant_propagationt.

Definition at line 210 of file ai.cpp.

◆ make_temporary_state()

◆ merge()

◆ merge_shared()

◆ operator()() [1/4]

void ai_baset::operator() ( const irep_idt function_identifier,
const goto_programt goto_program,
const namespacet ns 
)
inline

Run abstract interpretation on a single function.

Definition at line 47 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 60 of file ai.h.

◆ operator()() [3/4]

void ai_baset::operator() ( const goto_modelt goto_model)
inline

Run abstract interpretation on a whole program.

Definition at line 71 of file ai.h.

◆ operator()() [4/4]

void ai_baset::operator() ( const irep_idt function_identifier,
const goto_functionst::goto_functiont goto_function,
const namespacet ns 
)
inline

Run abstract interpretation on a single function.

Definition at line 81 of file ai.h.

◆ output() [1/5]

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 24 of file ai.cpp.

◆ output() [2/5]

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 134 of file ai.h.

◆ output() [3/5]

void ai_baset::output ( const namespacet ns,
const goto_programt goto_program,
std::ostream &  out 
) const
inline

Output the abstract states for a function.

Definition at line 143 of file ai.h.

◆ output() [4/5]

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 152 of file ai.h.

◆ output() [5/5]

void ai_baset::output ( const namespacet ns,
const goto_programt goto_program,
const irep_idt identifier,
std::ostream &  out 
) const
protectedvirtual

Output the abstract states for a single function.

Parameters
nsThe namespace
goto_programThe goto program
identifierThe identifier used to find a symbol to identify the source language
outThe ostream to direct output to

Definition at line 43 of file ai.cpp.

◆ output_json() [1/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 63 of file ai.cpp.

◆ output_json() [2/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 166 of file ai.h.

◆ output_json() [3/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 174 of file ai.h.

◆ output_json() [4/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 182 of file ai.h.

◆ output_json() [5/5]

jsont ai_baset::output_json ( const namespacet ns,
const goto_programt goto_program,
const irep_idt identifier 
) const
protectedvirtual

Output the abstract states for a single function as JSON.

Output the domains for a single function as JSON.

Parameters
nsThe namespace
goto_programThe goto program
identifierThe identifier used to find a symbol to identify the source language
Returns
The JSON object

Definition at line 91 of file ai.cpp.

◆ output_xml() [1/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 119 of file ai.cpp.

◆ output_xml() [2/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 195 of file ai.h.

◆ output_xml() [3/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 203 of file ai.h.

◆ output_xml() [4/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 211 of file ai.h.

◆ output_xml() [5/5]

xmlt ai_baset::output_xml ( const namespacet ns,
const goto_programt goto_program,
const irep_idt identifier 
) const
protectedvirtual

Output the abstract states for a single function as XML.

Output the domains for a single function as XML.

Parameters
nsThe namespace
goto_programThe goto program
identifierThe identifier used to find a symbol to identify the source language
Returns
The XML object

Definition at line 150 of file ai.cpp.

◆ put_in_working_set()

void ai_baset::put_in_working_set ( working_sett working_set,
locationt  l 
)
inlineprotected

Definition at line 282 of file ai.h.

◆ sequential_fixedpoint()

void ai_baset::sequential_fixedpoint ( const goto_functionst goto_functions,
const namespacet ns 
)
protected

Definition at line 445 of file ai.cpp.

◆ visit()

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

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.

Returns
True if the state was changed

Definition at line 262 of file ai.cpp.


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