cprover
ai_baset Class Referenceabstract

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

#include <ai.h>

Inheritance diagram for ai_baset:
[legend]

Public Types

typedef ai_domain_baset statet
 
typedef goto_programt::const_targett locationt
 

Public Member Functions

 ai_baset ()
 
virtual ~ai_baset ()
 
void operator() (const goto_programt &goto_program, const namespacet &ns)
 Running the interpreter. More...
 
void operator() (const goto_functionst &goto_functions, const namespacet &ns)
 
void operator() (const goto_modelt &goto_model)
 
void operator() (const goto_functionst::goto_functiont &goto_function, const namespacet &ns)
 
virtual std::unique_ptr< statetabstract_state_before (locationt l) const =0
 Accessing individual domains at particular locations (without needing to know what kind of domain or history is used) A pointer to a copy as the method should be const and there are some non-trivial cases including merging domains, etc. More...
 
virtual std::unique_ptr< statetabstract_state_after (locationt l) const
 Returns the abstract state after the given instruction. More...
 
virtual void clear ()
 Resets the domain. More...
 
virtual void output (const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
 
void output (const goto_modelt &goto_model, std::ostream &out) const
 
void output (const namespacet &ns, const goto_programt &goto_program, std::ostream &out) const
 
void output (const namespacet &ns, const goto_functionst::goto_functiont &goto_function, std::ostream &out) const
 
virtual jsont output_json (const namespacet &ns, const goto_functionst &goto_functions) const
 Output the domains for the whole program as JSON. More...
 
jsont output_json (const goto_modelt &goto_model) const
 
jsont output_json (const namespacet &ns, const goto_programt &goto_program) const
 
jsont output_json (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
 
virtual xmlt output_xml (const namespacet &ns, const goto_functionst &goto_functions) const
 Output the domains for the whole program as XML. More...
 
xmlt output_xml (const goto_modelt &goto_model) const
 
xmlt output_xml (const namespacet &ns, const goto_programt &goto_program) const
 
xmlt output_xml (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
 

Protected Types

typedef std::map< unsigned, locationtworking_sett
 

Protected Member Functions

virtual void initialize (const goto_programt &)
 
virtual void initialize (const goto_functionst::goto_functiont &)
 
virtual void initialize (const goto_functionst &)
 
virtual void finalize ()
 
void entry_state (const goto_programt &)
 
void entry_state (const goto_functionst &)
 
virtual void output (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier, std::ostream &out) const
 
virtual jsont output_json (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier) const
 Output the domains 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 domains for a single function as XML. More...
 
locationt get_next (working_sett &working_set)
 
void put_in_working_set (working_sett &working_set, locationt l)
 
bool fixedpoint (const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
 
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 (locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
 
bool do_function_call_rec (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 (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
 
virtual const statetfind_state (locationt l) const =0
 
virtual std::unique_ptr< statetmake_temporary_state (const statet &s)=0
 

Detailed Description

The basic interface of an abstract interpreter.

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

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

Definition at line 223 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

Returns the abstract state after the given instruction.

PRECONDITION(l is dereferenceable && std::next(l) is dereferenceable) Check relies on a DATA_INVARIANT of goto_programs

Definition at line 99 of file ai.h.

References abstract_state_before(), and INVARIANT.

◆ abstract_state_before()

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

Accessing individual domains at particular locations (without needing to know what kind of domain or history is used) A pointer to a copy as the method should be const and there are some non-trivial cases including merging domains, etc.

Intended for users of the abstract interpreter; don't use internally. Returns the abstract state before the given instruction PRECONDITION(l is dereferenceable)

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

Referenced by abstract_state_after(), build_dead_map_from_ai(), compute_called_functions_from_ai(), output(), output_json(), output_xml(), static_simplifier(), and static_verifier().

◆ clear()

◆ concurrent_fixedpoint()

◆ do_function_call()

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

◆ do_function_call_rec()

bool ai_baset::do_function_call_rec ( locationt  l_call,
locationt  l_return,
const exprt function,
const exprt::operandst arguments,
const goto_functionst goto_functions,
const namespacet ns 
)
protected

◆ entry_state() [1/2]

void ai_baset::entry_state ( const goto_programt goto_program)
protected

Definition at line 191 of file ai.cpp.

References get_state(), goto_program, and goto_programt::instructions.

Referenced by entry_state(), and operator()().

◆ entry_state() [2/2]

void ai_baset::entry_state ( const goto_functionst goto_functions)
protected

◆ finalize()

void ai_baset::finalize ( )
protectedvirtual

Reimplemented in dependence_grapht.

Definition at line 216 of file ai.cpp.

Referenced by operator()().

◆ find_state()

◆ fixedpoint() [1/2]

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

◆ fixedpoint() [2/2]

◆ get_next()

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

Definition at line 221 of file ai.cpp.

References PRECONDITION.

Referenced by concurrent_fixedpoint(), and fixedpoint().

◆ get_state()

◆ initialize() [1/3]

◆ initialize() [2/3]

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

Definition at line 197 of file ai.cpp.

References initialize().

◆ initialize() [3/3]

void ai_baset::initialize ( const goto_functionst goto_functions)
protectedvirtual

◆ make_temporary_state()

◆ merge()

◆ merge_shared()

◆ operator()() [1/4]

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

Running the interpreter.

Definition at line 47 of file ai.h.

References entry_state(), finalize(), fixedpoint(), goto_program, and initialize().

Referenced by constant_propagator_ait::constant_propagator_ait().

◆ operator()() [2/4]

void ai_baset::operator() ( const goto_functionst goto_functions,
const namespacet ns 
)
inline

Definition at line 58 of file ai.h.

References entry_state(), finalize(), fixedpoint(), and initialize().

◆ operator()() [3/4]

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

◆ operator()() [4/4]

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

Definition at line 77 of file ai.h.

References entry_state(), finalize(), fixedpoint(), and initialize().

◆ output() [1/5]

void ai_baset::output ( const namespacet ns,
const goto_functionst goto_functions,
std::ostream &  out 
) const
virtual

◆ output() [2/5]

void ai_baset::output ( const goto_modelt goto_model,
std::ostream &  out 
) const
inline

Definition at line 117 of file ai.h.

References goto_modelt::goto_functions, output(), and goto_modelt::symbol_table.

◆ output() [3/5]

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

Definition at line 125 of file ai.h.

References goto_program, and output().

◆ output() [4/5]

void ai_baset::output ( const namespacet ns,
const goto_functionst::goto_functiont goto_function,
std::ostream &  out 
) const
inline

Definition at line 133 of file ai.h.

References output().

◆ 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_json() [1/5]

jsont ai_baset::output_json ( const namespacet ns,
const goto_functionst goto_functions 
) const
virtual

Output the domains for the whole program as JSON.

parameters: The namespace and goto_functions
Returns
The JSON object

Definition at line 66 of file ai.cpp.

References forall_goto_functions, and id2string().

Referenced by output_json(), and static_show_domain().

◆ output_json() [2/5]

jsont ai_baset::output_json ( const goto_modelt goto_model) const
inline

Definition at line 146 of file ai.h.

References goto_modelt::goto_functions, output_json(), and goto_modelt::symbol_table.

◆ output_json() [3/5]

jsont ai_baset::output_json ( const namespacet ns,
const goto_programt goto_program 
) const
inline

Definition at line 153 of file ai.h.

References goto_program, and output_json().

◆ output_json() [4/5]

jsont ai_baset::output_json ( const namespacet ns,
const goto_functionst::goto_functiont goto_function 
) const
inline

Definition at line 160 of file ai.h.

References output_json().

◆ 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 domains for a single function as JSON.

parameters: The namespace, goto_program and it's identifier
Returns
The JSON object

Definition at line 91 of file ai.cpp.

References abstract_state_before(), forall_goto_program_instructions, goto_program, goto_programt::output_instruction(), json_arrayt::push_back(), and to_string().

◆ output_xml() [1/5]

xmlt ai_baset::output_xml ( const namespacet ns,
const goto_functionst goto_functions 
) const
virtual

Output the domains for the whole program as XML.

parameters: The namespace and goto_functions
Returns
The XML object

Definition at line 122 of file ai.cpp.

References forall_goto_functions, id2string(), xmlt::new_element(), and xmlt::set_attribute().

Referenced by output_xml(), and static_show_domain().

◆ output_xml() [2/5]

xmlt ai_baset::output_xml ( const goto_modelt goto_model) const
inline

Definition at line 172 of file ai.h.

References goto_modelt::goto_functions, output_xml(), and goto_modelt::symbol_table.

◆ output_xml() [3/5]

xmlt ai_baset::output_xml ( const namespacet ns,
const goto_programt goto_program 
) const
inline

Definition at line 179 of file ai.h.

References goto_program, and output_xml().

◆ output_xml() [4/5]

xmlt ai_baset::output_xml ( const namespacet ns,
const goto_functionst::goto_functiont goto_function 
) const
inline

Definition at line 186 of file ai.h.

References output_xml().

◆ 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 domains for a single function as XML.

parameters: The namespace, goto_program and it's identifier
Returns
The XML object

Definition at line 150 of file ai.cpp.

References abstract_state_before(), forall_goto_program_instructions, goto_program, xmlt::new_element(), goto_programt::output_instruction(), output_xml(), xmlt::set_attribute(), and to_string().

◆ put_in_working_set()

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

Definition at line 227 of file ai.h.

Referenced by concurrent_fixedpoint(), fixedpoint(), and visit().

◆ sequential_fixedpoint()

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

◆ visit()


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