A history object is an abstraction / representation of the control-flow part of a set of traces. More...
#include <ai_history.h>
Inheritance diagram for ai_history_baset: Collaboration diagram for ai_history_baset:Classes | |
| struct | compare_historyt |
| In a number of places we need to work with sets of histories so that these (a) make use of the immutability and sharing and (b) ownership can be transfered if necessary, we use shared pointers rather than references. More... | |
Public Types | |
| enum class | step_statust { NEW , MERGED , BLOCKED } |
| typedef goto_programt::const_targett | locationt |
| typedef std::shared_ptr< const ai_history_baset > | trace_ptrt |
| History objects are intended to be immutable so they can be shared to reduce memory overhead. More... | |
| typedef std::set< trace_ptrt, compare_historyt > | trace_sett |
| typedef std::pair< step_statust, trace_ptrt > | step_returnt |
Public Member Functions | |
| virtual | ~ai_history_baset () |
| virtual step_returnt | step (locationt to, const trace_sett &others, trace_ptrt caller_hist) const =0 |
| Step creates a new history by advancing the current one to location "to" It is given the set of all other histories that have reached this point. More... | |
| virtual bool | operator< (const ai_history_baset &op) const =0 |
| The order for history_sett. More... | |
| virtual bool | operator== (const ai_history_baset &op) const =0 |
| History objects should be comparable. More... | |
| virtual const locationt & | current_location (void) const =0 |
| The current location in the history, used to compute the transformer POSTCONDITION(return value is dereferenceable) More... | |
| virtual bool | should_widen (const ai_history_baset &other) const |
| Domains with a substantial height may need to widen when merging this method allows the history to provide a hint on when to do this The suggested use of this is for domains merge operation to check this and then widen in a domain specific way. More... | |
| virtual void | output (std::ostream &out) const |
| virtual jsont | output_json (void) const |
| virtual xmlt | output_xml (void) const |
Static Public Attributes | |
| static const trace_ptrt | no_caller_history |
Protected Member Functions | |
| ai_history_baset (locationt) | |
| Create a new history starting from a given location This is used to start the analysis from scratch PRECONDITION(l.is_dereferenceable());. More... | |
| ai_history_baset (const ai_history_baset &) | |
Detailed Description
A history object is an abstraction / representation of the control-flow part of a set of traces.
The simplest example is a single location which represents "all traces that reach this location". More sophisticated history objects represent "all traces that reach this point after exactly N iterations of this loop", "all traces that follow a given pattern of branching to reach this point" or "all traces that have the following call stack and reach this location".
These are used to control the abstract interpreter; edges are computed per history. Depending on what storage is used, they may also control or influence the number of domains that are used, supporting delayed merging, loop unwinding, context dependent analysis, etc. This is the base interface; derive from this.
Definition at line 36 of file ai_history.h.
Member Typedef Documentation
◆ locationt
Definition at line 39 of file ai_history.h.
◆ step_returnt
| typedef std::pair<step_statust, trace_ptrt> ai_history_baset::step_returnt |
Definition at line 88 of file ai_history.h.
◆ trace_ptrt
| typedef std::shared_ptr<const ai_history_baset> ai_history_baset::trace_ptrt |
History objects are intended to be immutable so they can be shared to reduce memory overhead.
Definition at line 43 of file ai_history.h.
◆ trace_sett
| typedef std::set<trace_ptrt, compare_historyt> ai_history_baset::trace_sett |
Definition at line 79 of file ai_history.h.
Member Enumeration Documentation
◆ step_statust
|
strong |
| Enumerator | |
|---|---|
| NEW | |
| MERGED | |
| BLOCKED | |
Definition at line 81 of file ai_history.h.
Constructor & Destructor Documentation
◆ ai_history_baset() [1/2]
|
inlineexplicitprotected |
Create a new history starting from a given location This is used to start the analysis from scratch PRECONDITION(l.is_dereferenceable());.
Definition at line 49 of file ai_history.h.
◆ ai_history_baset() [2/2]
|
inlineprotected |
Definition at line 53 of file ai_history.h.
◆ ~ai_history_baset()
|
inlinevirtual |
Definition at line 58 of file ai_history.h.
Member Function Documentation
◆ current_location()
|
pure virtual |
The current location in the history, used to compute the transformer POSTCONDITION(return value is dereferenceable)
Implemented in local_control_flow_historyt< track_forward_jumps, track_backward_jumps >, call_stack_historyt, and ahistoricalt.
◆ operator<()
|
pure virtual |
The order for history_sett.
Implemented in local_control_flow_historyt< track_forward_jumps, track_backward_jumps >, call_stack_historyt, and ahistoricalt.
◆ operator==()
|
pure virtual |
History objects should be comparable.
Implemented in local_control_flow_historyt< track_forward_jumps, track_backward_jumps >, call_stack_historyt, and ahistoricalt.
◆ output()
|
inlinevirtual |
Reimplemented in local_control_flow_historyt< track_forward_jumps, track_backward_jumps >, call_stack_historyt, and ahistoricalt.
Definition at line 144 of file ai_history.h.
◆ output_json()
|
virtual |
Definition at line 14 of file ai_history.cpp.
◆ output_xml()
|
virtual |
Definition at line 22 of file ai_history.cpp.
◆ should_widen()
|
inlinevirtual |
Domains with a substantial height may need to widen when merging this method allows the history to provide a hint on when to do this The suggested use of this is for domains merge operation to check this and then widen in a domain specific way.
However it could be used in other ways (such as the transformer). The key idea is that the history tracks / should know when to widen and when to continue.
Reimplemented in local_control_flow_historyt< track_forward_jumps, track_backward_jumps >, call_stack_historyt, and ahistoricalt.
Definition at line 139 of file ai_history.h.
◆ step()
|
pure virtual |
Step creates a new history by advancing the current one to location "to" It is given the set of all other histories that have reached this point.
In the case of function call return it is also given the full history of the caller. This allows function-local histories as they can "pick up" the state from before the call when computing the return edge.
PRECONDITION(to.id_dereferenceable()); PRECONDITION(to in goto_program.get_successors(current_location()) || current_location()->is_function_call() || current_location()->is_end_function()); PRECONDITION(caller_hist == no_caller_history || current_location()->is_end_function);
Step may do one of three things :
- Create a new history object and return a pointer to it This will force the analyser to continue regardless of domain changes POSTCONDITION(IMPLIES(result.first == step_statust::NEW, result.second.use_count() == 1 ));
- Merge with an existing history This means the analyser will only continue if the domain is updated POSTCONDITION(IMPLIES(result.first == step_statust::MERGED, result.second is an element of others));
- Block this flow of execution This indicates the transition is impossible (returning to a location other than the call location) or undesireable (omitting some traces) POSTCONDITION(IMPLIES(result.first == BLOCKED, result.second == nullptr()));
Implemented in local_control_flow_historyt< track_forward_jumps, track_backward_jumps >, call_stack_historyt, and ahistoricalt.
Member Data Documentation
◆ no_caller_history
|
static |
Definition at line 121 of file ai_history.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/analyses/ai_history.h
- /home/runner/work/cbmc/cbmc/src/analyses/ai_history.cpp
