|
| | concurrency_aware_ait () |
| |
| | concurrency_aware_ait (std::unique_ptr< ai_domain_factory_baset > &&df) |
| |
| virtual bool | merge_shared (const statet &src, locationt from, locationt to, const namespacet &ns) |
| |
| | ait () |
| |
| | ait (std::unique_ptr< ai_domain_factory_baset > &&df) |
| |
| const domainT & | operator[] (locationt l) const |
| | Find the analysis result for a given location. More...
|
| |
| | ai_recursive_interproceduralt (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) |
| |
| | 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 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...
|
| |
| 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...
|
| |
|
| void | fixedpoint (ai_baset::trace_ptrt start_trace, const goto_functionst &goto_functions, const namespacet &ns) override |
| |
| virtual statet & | get_state (locationt l) |
| |
| 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...
|
| |
| 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) override |
| |
| 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...
|
| |
| 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 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 | 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...
|
| |
template<typename domainT>
class concurrency_aware_ait< domainT >
Base class for concurrency-aware abstract interpretation.
See ait for details. The only difference is that after the sequential fixed point construction, as done by ait, another step is added to account for concurrently-executed instructions. Basically, it makes the analysis flow-insensitive by feeding results of a sequential execution back into the entry point, thereby accounting for any values computed by different threads. Compare [Martin Rinard, "Analysis of Multi-Threaded Programs", SAS 2001]( http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.28.4747& rep=rep1&type=pdf).
- Template Parameters
-
| domainT | A type derived from ai_domain_baset that represents the values in the AI domain |
It is important to note that the domains used by this need an extra merge method, but, far more critically, they need the property that it is not possible to "undo" changes to the domain. Tracking last modified location has this property, numerical domains such as constants and intervals do not and using this kind of concurrent analysis for these domains may miss significant behaviours.
Definition at line 650 of file ai.h.
Inheritance diagram for concurrency_aware_ait< domainT >: