This is the basic interface of the abstract interpreter with default implementations of the core functionality.
More...
|
| | ai_baset (std::unique_ptr< ai_history_factory_baset > &&hf, std::unique_ptr< ai_domain_factory_baset > &&df, std::unique_ptr< ai_storage_baset > &&st, message_handlert &mh) |
| |
| 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 abstract_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 ctrace_set_ptrt | abstract_traces_before (locationt l) const |
| | Returns all of the histories that have reached the start of the instruction. More...
|
| |
| virtual ctrace_set_ptrt | abstract_traces_after (locationt l) const |
| | Returns all of the histories that have reached the end of the instruction. More...
|
| |
| virtual cstate_ptrt | abstract_state_before (locationt l) const |
| | 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 cstate_ptrt | abstract_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 cstate_ptrt | abstract_state_before (const trace_ptrt &p) const |
| | The same interfaces but with histories. More...
|
| |
| virtual cstate_ptrt | abstract_state_after (const trace_ptrt &p) const |
| |
| virtual void | clear () |
| | Reset the abstract state. 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...
|
| |
|
| 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...
|
| |
| trace_ptrt | 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...
|
| |
| trace_ptrt | 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...
|
| |
| trace_ptrt | get_next (working_sett &working_set) |
| | Get the next location from the work queue. More...
|
| |
| void | put_in_working_set (working_sett &working_set, trace_ptrt t) |
| |
| virtual bool | fixedpoint (trace_ptrt starting_trace, 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...
|
| |
| virtual void | fixedpoint (trace_ptrt starting_trace, const goto_functionst &goto_functions, const namespacet &ns) |
| |
| virtual bool | visit (const irep_idt &function_id, trace_ptrt p, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) |
| | Perform one step of abstract interpretation from trace t Depending on the instruction type it may compute a number of "edges" or applications of the abstract transformer. More...
|
| |
| virtual bool | visit_function_call (const irep_idt &function_id, trace_ptrt p_call, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) |
| |
| virtual bool | visit_end_function (const irep_idt &function_id, trace_ptrt p, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) |
| |
| bool | visit_edge (const irep_idt &function_id, trace_ptrt p, const irep_idt &to_function_id, locationt to_l, trace_ptrt caller_history, const namespacet &ns, working_sett &working_set) |
| |
| virtual bool | visit_edge_function_call (const irep_idt &calling_function_id, trace_ptrt p_call, locationt l_return, const irep_idt &callee_function_id, working_sett &working_set, const goto_programt &callee, const goto_functionst &goto_functions, const namespacet &ns) |
| |
| virtual bool | merge (const statet &src, trace_ptrt from, trace_ptrt to) |
| | Merge the state src, flowing from tracet from to tracet to, into the state currently stored for tracet to. More...
|
| |
| virtual std::unique_ptr< statet > | make_temporary_state (const statet &s) |
| | Make a copy of a state. More...
|
| |
| virtual statet & | get_state (trace_ptrt p) |
| | Get the state for the given history, creating it with the factory if it doesn't exist. More...
|
| |
This is the basic interface of the abstract interpreter with default implementations of the core functionality.
Users of abstract interpreters should use the interface given by this class. It breaks into three categories:
- 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 abstract_goto_modelt&)
- Accessing the results of an analysis, by looking up the history objects for a given location
l using ai_baset::abstract_traces_before(locationt)const or the domains using ai_baset::abstract_state_before(locationt)const
- Outputting the results of the analysis; see ai_baset::output(const namespacet&, const irep_idt&, const goto_programt&, std::ostream&)const et cetera.
Where possible, uses should be agnostic of the particular configuration of the abstract interpreter. The "tasks" that goto-analyze uses are good examples of how to do this.
From a development point of view, there are several directions in which this can be extended by inheriting from ai_baset or one of its children:
A. To change how single edges are computed ait::visit_edge and ait::visit_edge_function_call ai_recursive_interproceduralt uses this to recurse to evaluate function calls rather than approximating them as ai_baset does.
B. To change how individual instructions are handled ait::visit() and related functions.
C. To change the way that the fixed point is computed ait::fixedpoint() concurrency_aware_ait does this to compute a fixed point over threads.
D. For pre-analysis initialization ait::initialize(const irep_idt&, const goto_programt&), ait::initialize(const irep_idt&, const goto_functionst::goto_functiont&) and ait::initialize(const goto_functionst&),
E. For post-analysis cleanup ait::finalize(),
Historically, uses of abstract interpretation inherited from ait<domainT> and added the necessary functionality. This works (although care must be taken to respect the APIs of the various components – there are some hacks to support older analyses that didn't) but is discouraged in favour of having an object for the abstract interpreter and using its public API.
Definition at line 118 of file ai.h.
Inheritance diagram for ai_baset: