36 locationt l_call_site = p_call->current_location();
43 l_callee_end->is_end_function(),
44 "The last instruction of a goto_program must be END_FUNCTION");
47 log.progress() <<
"ai_three_way_merget::visit_edge_function_call"
48 <<
" from " << l_call_site->location_number <<
" to "
54 auto next = p_call_site->step(
56 *(
storage->abstract_traces_before(l_callee_start)),
83 log.progress() <<
"Handle " << callee_function_id <<
" recursively"
100 auto traces =
storage->abstract_traces_before(l_callee_end);
102 bool new_data =
false;
107 for(
auto p_callee_end : *traces)
109 log.progress() <<
"ai_three_way_merget::visit_edge_function_call edge from "
110 << l_callee_end->location_number <<
" to "
111 << l_return_site->location_number <<
"... ";
123 auto return_step = p_callee_end->step(
125 *(
storage->abstract_traces_before(l_return_site)),
134 log.progress() <<
"gives a new history... ";
138 log.progress() <<
"merges with existing history... ";
142 trace_ptrt p_return_site = return_step.second;
144 const std::unique_ptr<statet> ptr_s_callee_end_copy(
148 INVARIANT(tmp !=
nullptr,
"Three-way merge requires domain support");
154 log.progress() <<
"applying transformer... ";
164 const std::unique_ptr<statet> ptr_call_site_working(
168 INVARIANT(tmp2 !=
nullptr,
"Three-way merge requires domain support");
171 log.progress() <<
"three way merge... ";
173 get_state(p_callee_start), s_working, ns);
175 log.progress() <<
"merging... ";
177 merge(s_call_site_working, p_callee_end, p_return_site) ||
194 log.debug() <<
"p_callee_end = ";
195 p_callee_end->output(
log.debug());
198 log.debug() <<
"s_callee_end = ";
199 s_callee_end.
output(
log.debug(), *
this, ns);
202 log.debug() <<
"p_return_site = ";
203 p_return_site->output(
log.debug());
206 log.debug() <<
"s_working = ";
207 s_working.
output(
log.debug(), *
this, ns);
goto_programt::const_targett locationt
std::unique_ptr< ai_storage_baset > storage
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)
message_handlert & message_handler
virtual std::unique_ptr< statet > make_temporary_state(const statet &s)
Make a copy of a state.
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.
ai_history_baset::trace_ptrt trace_ptrt
void put_in_working_set(working_sett &working_set, trace_ptrt t)
trace_ptrt get_next(working_sett &working_set)
Get the next location from the work queue.
trace_sett working_sett
The work queue, sorted using the history's ordering operator.
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 trace...
virtual statet & get_state(trace_ptrt p)
Get the state for the given history, creating it with the factory if it doesn't exist.
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
virtual bool is_bottom() const =0
virtual void output(std::ostream &, const ai_baset &, const namespacet &) const
A history object is an abstraction / representation of the control-flow part of a set of traces.
static const trace_ptrt no_caller_history
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
unsigned get_verbosity() const
Class that provides messages with a built-in verbosity 'level'.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
Basic text output of the abstract domain.
void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) override
Compute the abstract transformer for a single instruction.
virtual void merge_three_way_function_return(const ai_domain_baset &function_start, const ai_domain_baset &function_end, const namespacet &ns)
Merges just the things that have changes between "function_start" and "function_end" into "this".
bool is_bottom() const override
Find out if the domain is currently unreachable.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
An abstract interpreter, based on the default recursive-interprocedural that uses variable sensitivit...
There are different ways of handling arrays, structures, unions and pointers.