14 template <
bool track_forward_jumps,
bool track_backward_jumps>
26 track_backward_jumps>>
31 current_loc->is_goto() &&
32 (current_loc->is_backwards_goto() ? track_backward_jumps
33 : track_forward_jumps))
35 bool branch_taken = (current_loc->get_target() == to) &&
36 !(current_loc->get_target() == std::next(current_loc));
42 auto decision = std::make_shared<local_control_flow_decisiont>(
43 current_loc, branch_taken, control_flow_decision_history);
44 next_step = std::make_shared<
46 to, decision, max_histories_per_location);
49 current_loc->is_function_call() &&
50 std::next(this->current_loc)->location_number != to->location_number)
55 if(others.size() == 0)
57 next_step = std::make_shared<
59 to,
nullptr, max_histories_per_location);
66 "Function start should have at most one merged history");
68 to_local_control_flow_history(*(others.begin()))
69 ->is_path_merge_history(),
70 "The one history must be a merge point");
72 return std::make_pair(
76 else if(current_loc->is_end_function())
82 next_step = std::make_shared<
85 to_local_control_flow_history(caller_hist)->control_flow_decision_history,
86 max_histories_per_location);
92 next_step = std::make_shared<
94 to, control_flow_decision_history, max_histories_per_location);
97 next_step !=
nullptr,
"All branches should create a candidate history");
100 auto it = others.find(next_step);
101 if(it == others.end())
103 if(has_histories_per_location_limit())
105 auto number_of_histories = others.size();
107 if(number_of_histories < max_histories_per_location - 1)
112 else if(number_of_histories == max_histories_per_location - 1)
117 track_backward_jumps>>(to,
nullptr, max_histories_per_location);
120 else if(others.size() == max_histories_per_location)
125 auto last_history_pointer = std::prev(others.end());
128 to_local_control_flow_history(*last_history_pointer)
129 ->is_path_merge_history(),
130 "The last history must be the merged one");
132 return std::make_pair(
138 others.size() <= max_histories_per_location,
139 "Histories-per-location limit should be enforced");
156 template <
bool track_forward_jumps,
bool track_backward_jumps>
160 auto other =
dynamic_cast<
167 if(this->current_loc->location_number < other.current_loc->location_number)
172 this->current_loc->location_number > other.current_loc->location_number)
179 this->control_flow_decision_history ==
180 other.control_flow_decision_history)
185 else if(other.control_flow_decision_history ==
nullptr)
192 else if(this->control_flow_decision_history ==
nullptr)
200 *(this->control_flow_decision_history) <
201 *(other.control_flow_decision_history));
207 template <
bool track_forward_jumps,
bool track_backward_jumps>
211 auto other =
dynamic_cast<
216 if(this->current_loc->location_number == other.current_loc->location_number)
219 this->control_flow_decision_history ==
220 other.control_flow_decision_history)
225 this->control_flow_decision_history ==
nullptr ||
226 other.control_flow_decision_history ==
nullptr)
237 *(this->control_flow_decision_history) ==
238 *(other.control_flow_decision_history));
248 template <
bool track_forward_jumps,
bool track_backward_jumps>
250 output(std::ostream &out)
const
252 out <<
"local_control_flow_history : location "
253 << current_loc->location_number;
254 lcfd_ptrt working = control_flow_decision_history;
255 while(working !=
nullptr)
257 out <<
" after " << working->branch_location->location_number;
258 if(working->branch_taken)
266 working = working->previous;
292 "Implied by if-then-else");
363 const trace_sett &others,
364 trace_ptrt caller_hist)
const;
369 const trace_sett &others,
370 trace_ptrt caller_hist)
const;
375 const trace_sett &others,
376 trace_ptrt caller_hist)
const;
381 const trace_sett &others,
382 trace_ptrt caller_hist)
const;
A history object is an abstraction / representation of the control-flow part of a set of traces.
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.
std::pair< step_statust, trace_ptrt > step_returnt
static const trace_ptrt no_caller_history
goto_programt::const_targett locationt
std::set< trace_ptrt, compare_historyt > trace_sett
Records all local control-flow decisions up to a limit of number of histories per location.
bool operator<(const local_control_flow_decisiont &op) const
bool operator==(const local_control_flow_decisiont &op) const
locationt branch_location
Whether we track forwards and / or backwards jumps is compile-time fixed as it does not need to be va...
bool operator<(const ai_history_baset &op) const override
The order for history_sett.
void output(std::ostream &out) const override
bool operator==(const ai_history_baset &op) const override
History objects should be comparable.
local_control_flow_decisiont::lcfd_ptrt lcfd_ptrt
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 o...
Track function-local control flow for loop unwinding and path senstivity.
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.