Whether we track forwards and / or backwards jumps is compile-time fixed as it does not need to be variable and because there may be a lot of history objects created. More...
#include <local_control_flow_history.h>
Inheritance diagram for local_control_flow_historyt< track_forward_jumps, track_backward_jumps >: Collaboration diagram for local_control_flow_historyt< track_forward_jumps, track_backward_jumps >:Public Member Functions | |
| bool | is_path_merge_history (void) const |
| bool | has_histories_per_location_limit (void) const |
| local_control_flow_historyt (locationt loc) | |
| local_control_flow_historyt (locationt loc, lcfd_ptrt hist, size_t max_hist) | |
| local_control_flow_historyt (locationt loc, size_t max_hist) | |
| local_control_flow_historyt (const local_control_flow_historyt< track_forward_jumps, track_backward_jumps > &old) | |
| step_returnt | step (locationt to, const trace_sett &others, trace_ptrt caller_hist) const override |
| 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... | |
| bool | operator< (const ai_history_baset &op) const override |
| The order for history_sett. More... | |
| bool | operator== (const ai_history_baset &op) const override |
| History objects should be comparable. More... | |
| const locationt & | current_location (void) const override |
| The current location in the history, used to compute the transformer POSTCONDITION(return value is dereferenceable) More... | |
| bool | should_widen (const ai_history_baset &other) const override |
| 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... | |
| void | output (std::ostream &out) const override |
| Public Member Functions inherited from ai_history_baset | |
| virtual | ~ai_history_baset () |
| virtual jsont | output_json (void) const |
| virtual xmlt | output_xml (void) const |
Protected Types | |
| typedef local_control_flow_decisiont::lcfd_ptrt | lcfd_ptrt |
Protected Member Functions | |
| std::shared_ptr< const local_control_flow_historyt< track_forward_jumps, track_backward_jumps > > | to_local_control_flow_history (trace_ptrt in) const |
| Protected Member Functions inherited from ai_history_baset | |
| 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 &) | |
Protected Attributes | |
| locationt | current_loc |
| lcfd_ptrt | control_flow_decision_history |
| size_t | max_histories_per_location |
Additional Inherited Members | |
| Public Types inherited from ai_history_baset | |
| 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 |
| Static Public Attributes inherited from ai_history_baset | |
| static const trace_ptrt | no_caller_history |
Detailed Description
template<bool track_forward_jumps, bool track_backward_jumps>
class local_control_flow_historyt< track_forward_jumps, track_backward_jumps >
Whether we track forwards and / or backwards jumps is compile-time fixed as it does not need to be variable and because there may be a lot of history objects created.
Definition at line 45 of file local_control_flow_history.h.
Member Typedef Documentation
◆ lcfd_ptrt
|
protected |
Definition at line 48 of file local_control_flow_history.h.
Constructor & Destructor Documentation
◆ local_control_flow_historyt() [1/4]
|
inlineexplicit |
Definition at line 83 of file local_control_flow_history.h.
◆ local_control_flow_historyt() [2/4]
|
inline |
Definition at line 92 of file local_control_flow_history.h.
◆ local_control_flow_historyt() [3/4]
|
inline |
Definition at line 100 of file local_control_flow_history.h.
◆ local_control_flow_historyt() [4/4]
|
inline |
Definition at line 109 of file local_control_flow_history.h.
Member Function Documentation
◆ current_location()
|
inlineoverridevirtual |
The current location in the history, used to compute the transformer POSTCONDITION(return value is dereferenceable)
Implements ai_history_baset.
Definition at line 127 of file local_control_flow_history.h.
◆ has_histories_per_location_limit()
|
inline |
Definition at line 78 of file local_control_flow_history.h.
◆ is_path_merge_history()
|
inline |
Definition at line 71 of file local_control_flow_history.h.
◆ operator<()
|
overridevirtual |
The order for history_sett.
Implements ai_history_baset.
Definition at line 157 of file local_control_flow_history.cpp.
◆ operator==()
|
overridevirtual |
History objects should be comparable.
Implements ai_history_baset.
Definition at line 208 of file local_control_flow_history.cpp.
◆ output()
|
overridevirtual |
Reimplemented from ai_history_baset.
Definition at line 249 of file local_control_flow_history.cpp.
◆ should_widen()
|
inlineoverridevirtual |
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 from ai_history_baset.
Definition at line 135 of file local_control_flow_history.h.
◆ step()
|
overridevirtual |
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()));
Implements ai_history_baset.
Definition at line 16 of file local_control_flow_history.cpp.
◆ to_local_control_flow_history()
|
inlineprotected |
Definition at line 59 of file local_control_flow_history.h.
Member Data Documentation
◆ control_flow_decision_history
|
protected |
Definition at line 51 of file local_control_flow_history.h.
◆ current_loc
|
protected |
Definition at line 50 of file local_control_flow_history.h.
◆ max_histories_per_location
|
protected |
Definition at line 52 of file local_control_flow_history.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/analyses/local_control_flow_history.h
- /home/runner/work/cbmc/cbmc/src/analyses/local_control_flow_history.cpp
