cprover
|
The basic interface of an abstract interpreter. More...
#include <ai.h>
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< statet > | abstract_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< statet > | abstract_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, locationt > | working_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 statet & | get_state (locationt l)=0 |
virtual const statet & | find_state (locationt l) const =0 |
virtual std::unique_ptr< statet > | make_temporary_state (const statet &s)=0 |
The basic interface of an abstract interpreter.
This should be enough to create, run and query an abstract interpreter.
typedef ai_domain_baset ai_baset::statet |
|
protected |
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.
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().
|
inlinevirtual |
Resets the domain.
Reimplemented 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 >.
Definition at line 108 of file ai.h.
Referenced by ait< dep_graph_domaint >::clear().
|
protected |
Definition at line 431 of file ai.cpp.
References goto_programt::add_instruction(), forall_goto_functions, forall_goto_program_instructions, get_next(), get_state(), goto_programt::instructions, merge(), merge_shared(), put_in_working_set(), sequential_fixedpoint(), and visit().
Referenced by concurrency_aware_ait< rd_range_domaint >::fixedpoint().
|
protected |
Definition at line 318 of file ai.cpp.
References fixedpoint(), get_state(), make_temporary_state(), merge(), PRECONDITION, and ai_domain_baset::transform().
Referenced by do_function_call_rec().
|
protected |
Definition at line 388 of file ai.cpp.
References DATA_INVARIANT, do_function_call(), goto_functionst::function_map, symbol_exprt::get_identifier(), id2string(), PRECONDITION, and to_symbol_expr().
Referenced by visit().
|
protected |
Definition at line 191 of file ai.cpp.
References get_state(), goto_program, and goto_programt::instructions.
Referenced by entry_state(), and operator()().
|
protected |
Definition at line 180 of file ai.cpp.
References goto_functionst::entry_point(), entry_state(), and goto_functionst::function_map.
|
protectedvirtual |
Reimplemented in dependence_grapht.
Definition at line 216 of file ai.cpp.
Referenced by operator()().
|
protected |
Definition at line 233 of file ai.cpp.
References goto_programt::empty(), get_next(), goto_program, goto_programt::instructions, put_in_working_set(), and visit().
Referenced by do_function_call(), operator()(), and sequential_fixedpoint().
|
protectedpure virtual |
Implemented in concurrency_aware_ait< domainT >, concurrency_aware_ait< rd_range_domaint >, 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 >.
|
protected |
Definition at line 221 of file ai.cpp.
References PRECONDITION.
Referenced by concurrent_fixedpoint(), and fixedpoint().
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 >, ait< dep_graph_domaint >, dependence_grapht, and reaching_definitions_analysist.
Referenced by concurrent_fixedpoint(), do_function_call(), entry_state(), initialize(), and visit().
|
protectedvirtual |
Reimplemented in dependence_grapht, and invariant_propagationt.
Definition at line 202 of file ai.cpp.
References forall_goto_program_instructions, get_state(), goto_program, and ai_domain_baset::make_bottom().
Referenced by invariant_propagationt::initialize(), custom_bitvector_analysist::initialize(), initialize(), dependence_grapht::initialize(), reaching_definitions_analysist::initialize(), and operator()().
|
protectedvirtual |
Definition at line 197 of file ai.cpp.
References initialize().
|
protectedvirtual |
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.
References forall_goto_functions, and initialize().
|
protectedpure virtual |
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 do_function_call(), and visit().
|
protectedpure virtual |
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 concurrent_fixedpoint(), do_function_call(), and visit().
|
protectedpure virtual |
Implemented in concurrency_aware_ait< domainT >, concurrency_aware_ait< rd_range_domaint >, 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 concurrent_fixedpoint().
|
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().
|
inline |
Definition at line 58 of file ai.h.
References entry_state(), finalize(), fixedpoint(), and initialize().
|
inline |
Definition at line 68 of file ai.h.
References entry_state(), finalize(), fixedpoint(), goto_modelt::goto_functions, initialize(), and goto_modelt::symbol_table.
|
inline |
Definition at line 77 of file ai.h.
References entry_state(), finalize(), fixedpoint(), and initialize().
|
virtual |
Definition at line 24 of file ai.cpp.
References forall_goto_functions.
Referenced by goto_instrument_parse_optionst::doit(), taint_analysist::operator()(), output(), show_uninitialized(), and static_show_domain().
|
inline |
Definition at line 117 of file ai.h.
References goto_modelt::goto_functions, output(), and goto_modelt::symbol_table.
|
inline |
Definition at line 125 of file ai.h.
References goto_program, and output().
|
inline |
|
protectedvirtual |
Definition at line 43 of file ai.cpp.
References abstract_state_before(), forall_goto_program_instructions, goto_program, and goto_programt::output_instruction().
|
virtual |
Output the domains for the whole program as JSON.
Definition at line 66 of file ai.cpp.
References forall_goto_functions, and id2string().
Referenced by output_json(), and static_show_domain().
|
inline |
Definition at line 146 of file ai.h.
References goto_modelt::goto_functions, output_json(), and goto_modelt::symbol_table.
|
inline |
Definition at line 153 of file ai.h.
References goto_program, and output_json().
|
inline |
Definition at line 160 of file ai.h.
References output_json().
|
protectedvirtual |
Output the domains for a single function as JSON.
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().
|
virtual |
Output the domains for the whole program as XML.
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().
|
inline |
Definition at line 172 of file ai.h.
References goto_modelt::goto_functions, output_xml(), and goto_modelt::symbol_table.
|
inline |
Definition at line 179 of file ai.h.
References goto_program, and output_xml().
|
inline |
Definition at line 186 of file ai.h.
References output_xml().
|
protectedvirtual |
Output the domains for a single function as XML.
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().
|
inlineprotected |
Definition at line 227 of file ai.h.
Referenced by concurrent_fixedpoint(), fixedpoint(), and visit().
|
protected |
Definition at line 420 of file ai.cpp.
References goto_functionst::entry_point(), fixedpoint(), and goto_functionst::function_map.
Referenced by concurrent_fixedpoint(), and ait< dep_graph_domaint >::fixedpoint().
|
protected |
Definition at line 260 of file ai.cpp.
References code_function_callt::arguments(), do_function_call_rec(), code_function_callt::function(), goto_functionst::function_map, get_state(), goto_programt::get_successors(), goto_program, goto_programt::instructions, make_temporary_state(), merge(), put_in_working_set(), to_code_function_call(), and ai_domain_baset::transform().
Referenced by concurrent_fixedpoint(), and fixedpoint().