23 std::ostream &out)
const
30 out <<
"//// Function: " <<
gf_entry.first <<
"\n";
43 std::ostream &out)
const
49 out <<
"**** " <<
i_it->location_number <<
" " <<
i_it->source_location()
80 return std::move(result);
95 std::ostringstream out;
104 contents.push_back(std::move(location));
114 xmlt program(
"program");
121 {
"body_available",
gf_entry.second.body_available() ?
"true" :
"false"}},
124 if(
gf_entry.second.body_available())
149 {{
"location_number", std::to_string(
i_it->location_number)},
150 {
"source_location",
i_it->source_location().as_string()}},
154 std::ostringstream out;
156 location.set_attribute(
"instruction", out.str());
169 goto_functionst::function_mapt::const_iterator
218 std::set<trace_ptrt, ai_history_baset::compare_historyt>>::value,
219 "begin must return the minimal entry");
260 goto_functionst::function_mapt::const_iterator
f_it =
279 log.progress() <<
"ai_baset::visit " << l->location_number <<
" in "
283 if(l->is_function_call())
287 "function calls only have one successor");
291 "function call successor / return location must be the next instruction");
294 function_id, p,
working_set, goto_program, goto_functions, ns);
296 else if(l->is_end_function())
300 "The end function instruction should have no successors.");
303 function_id, p,
working_set, goto_program, goto_functions, ns);
338 log.progress() <<
"ai_baset::visit_edge from "
339 << p->current_location()->location_number <<
" to "
340 <<
to_l->location_number <<
"... ";
352 log.progress() <<
"gives a new history... ";
356 log.progress() <<
"merges with existing history... ";
367 log.progress() <<
"applying transformer... ";
373 log.progress() <<
"merging... ";
374 bool return_value =
false;
393 log.debug() <<
"p = ";
397 log.debug() <<
"current = ";
401 log.debug() <<
"to_p = ";
405 log.debug() <<
"new_values = ";
424 log.progress() <<
"ai_baset::visit_edge_function_call from "
425 <<
p_call->current_location()->location_number <<
" to "
454 log.progress() <<
"ai_baset::visit_function_call at "
472 goto_functionst::function_mapt::const_iterator it =
503 "Function pointers and indirect calls must be removed before "
532 log.progress() <<
"ai_baset::visit_end_function " << function_id
550 log.progress() <<
"ai_recursive_interproceduralt::visit_edge_function_call"
551 <<
" from " <<
p_call->current_location()->location_number
591 l_end->is_end_function(),
592 "The last instruction of a goto_program must be END_FUNCTION");
604 for(
auto p_end : *traces)
goto_programt::const_targett locationt
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 com...
std::unique_ptr< ai_storage_baset > storage
virtual statet & get_state(trace_ptrt p)
Get the state for the given history, creating it with the factory if it doesn't exist.
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 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.
message_handlert & message_handler
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)
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)
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 ...
virtual 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)
virtual void initialize(const irep_idt &function_id, const goto_programt &goto_program)
Initialize all the abstract states for a single function.
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.
virtual std::unique_ptr< statet > make_temporary_state(const statet &s)
Make a copy of a state.
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 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 d...
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.
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.
std::unique_ptr< ai_history_factory_baset > history_factory
For creating history objects.
virtual void finalize()
Override this to add a cleanup or post-processing step after fixedpoint has run.
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
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...
xmlt & new_element(const std::string &key)
#define forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.