cprover
ait< domainT > Class Template Reference

Base class for abstract interpretation. More...

#include <ai.h>

+ Inheritance diagram for ait< domainT >:
+ Collaboration diagram for ait< domainT >:

Public Types

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

 ait ()
 
domainT & operator[] (locationt l)
 Find the analysis result for a given location. More...
 
const domainT & operator[] (locationt l) const
 Find the analysis result for a given location. More...
 
std::unique_ptr< statetabstract_state_before (locationt t) const override
 Used internally by the analysis. More...
 
void clear () override
 Remove all analysis results. More...
 
- Public Member Functions inherited from ai_baset
 ai_baset ()
 
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 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 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 irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
 Output the abstract states for a single function. 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

typedef std::unordered_map< locationt, domainT, const_target_hash, pointee_address_equaltstate_mapt
 Map from locations to domain elements, for the results of a static analysis. More...
 
- Protected Types inherited from ai_baset
typedef std::map< unsigned, locationtworking_sett
 The work queue, sorted by location number. More...
 

Protected Member Functions

virtual statetget_state (locationt l) override
 Look up the analysis state for a given location, instantiating a new state if required. More...
 
const statetfind_state (locationt l) const override
 Look up the analysis state for a given location, throwing an exception if no state is known. More...
 
bool merge (const statet &src, locationt from, locationt to) override
 Merge the state src, flowing from location from to location to, into the state currently stored for location to. More...
 
std::unique_ptr< statetmake_temporary_state (const statet &s) override
 Make a copy of s. More...
 
void fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) override
 Internal: implementation of the fixed point function using ai_baset::sequential_fixedpoint(const goto_functionst&, const namespacet&). More...
 
- 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...
 
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 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...
 
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_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...
 
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_id, 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_id, 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_id, 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

state_mapt state_map
 

Private Member Functions

void dummy (const domainT &s)
 This function exists to enforce that domainT is derived from ai_domain_baset. More...
 
bool merge_shared (const statet &, locationt, locationt, const namespacet &) override
 This function should not be implemented in sequential analyses. More...
 

Detailed Description

template<typename domainT>
class ait< domainT >

Base class for abstract interpretation.

An actual analysis must (a) inherit from this class and (b) provide a domain class as a type argument, which must, in turn, inherit from ai_domain_baset.

From a user's perspective, this class provides three main groups of functions:

  1. Running an analysis, via ai_baset::operator()(const irep_idt&,const goto_programt&, const namespacet&), ai_baset::operator()(const goto_functionst&,const namespacet&) and ai_baset::operator()(const goto_modelt&)
  2. Accessing the results of an analysis, by looking up the result for a given location l using ait::operator[](goto_programt::const_targett).
  3. Outputting the results of the analysis; see ai_baset::output(const namespacet&, const irep_idt&, const goto_programt&, std::ostream&)const et cetera.

A typical usage pattern would be to call the analysis first, and use operator[] afterwards to retrieve the results. The fixed point algorithm used is a standard worklist algorithm; the current implementation is flow- and path-sensitive, but not context-sensitive.

From an analysis developer's perspective, an analysis is implemented by inheriting from this class (or, if a concurrency-sensitive analysis is required, from concurrency_aware_ait), providing a class implementing the abstract domain as the type for the domainT parameter. Most of the actual analysis functions (in particular, the minimal element, the lattice join, and the state transformer) are supplied using domainT.

To control the analysis in more detail, you can also override the following methods:

Definition at line 398 of file ai.h.

Member Typedef Documentation

◆ locationt

template<typename domainT>
typedef goto_programt::const_targett ait< domainT >::locationt

Definition at line 406 of file ai.h.

◆ state_mapt

template<typename domainT>
typedef std:: unordered_map<locationt, domainT, const_target_hash, pointee_address_equalt> ait< domainT >::state_mapt
protected

Map from locations to domain elements, for the results of a static analysis.

Definition at line 454 of file ai.h.

Constructor & Destructor Documentation

◆ ait()

template<typename domainT>
ait< domainT >::ait ( )
inline

Definition at line 402 of file ai.h.

Member Function Documentation

◆ abstract_state_before()

template<typename domainT>
std::unique_ptr<statet> ait< domainT >::abstract_state_before ( locationt  t) const
inlineoverridevirtual

Used internally by the analysis.

Implements ai_baset.

Definition at line 429 of file ai.h.

◆ clear()

template<typename domainT>
void ait< domainT >::clear ( )
inlineoverridevirtual

Remove all analysis results.

Reimplemented from ai_baset.

Definition at line 443 of file ai.h.

◆ dummy()

template<typename domainT>
void ait< domainT >::dummy ( const domainT &  s)
inlineprivate

This function exists to enforce that domainT is derived from ai_domain_baset.

Definition at line 504 of file ai.h.

◆ find_state()

template<typename domainT>
const statet& ait< domainT >::find_state ( locationt  l) const
inlineoverrideprotectedvirtual

Look up the analysis state for a given location, throwing an exception if no state is known.

Used internally by the analysis.

Implements ai_baset.

Definition at line 467 of file ai.h.

◆ fixedpoint()

template<typename domainT>
void ait< domainT >::fixedpoint ( const goto_functionst goto_functions,
const namespacet ns 
)
inlineoverrideprotectedvirtual

Internal: implementation of the fixed point function using ai_baset::sequential_fixedpoint(const goto_functionst&, const namespacet&).

Implements ai_baset.

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

Definition at line 494 of file ai.h.

◆ get_state()

template<typename domainT>
virtual statet& ait< domainT >::get_state ( locationt  l)
inlineoverrideprotectedvirtual

Look up the analysis state for a given location, instantiating a new state if required.

Used internally by the analysis.

Implements ai_baset.

Reimplemented in reaching_definitions_analysist, and dependence_grapht.

Definition at line 459 of file ai.h.

◆ make_temporary_state()

template<typename domainT>
std::unique_ptr<statet> ait< domainT >::make_temporary_state ( const statet s)
inlineoverrideprotectedvirtual

Make a copy of s.

Implements ai_baset.

Definition at line 486 of file ai.h.

◆ merge()

template<typename domainT>
bool ait< domainT >::merge ( const statet src,
locationt  from,
locationt  to 
)
inlineoverrideprotectedvirtual

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

Implements ai_baset.

Definition at line 478 of file ai.h.

◆ merge_shared()

template<typename domainT>
bool ait< domainT >::merge_shared ( const statet ,
locationt  ,
locationt  ,
const namespacet  
)
inlineoverrideprivatevirtual

This function should not be implemented in sequential analyses.

Implements ai_baset.

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

Definition at line 507 of file ai.h.

◆ operator[]() [1/2]

template<typename domainT>
domainT& ait< domainT >::operator[] ( locationt  l)
inline

Find the analysis result for a given location.

Definition at line 409 of file ai.h.

◆ operator[]() [2/2]

template<typename domainT>
const domainT& ait< domainT >::operator[] ( locationt  l) const
inline

Find the analysis result for a given location.

Definition at line 419 of file ai.h.

Member Data Documentation

◆ state_map

template<typename domainT>
state_mapt ait< domainT >::state_map
protected

Definition at line 455 of file ai.h.


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