Go to the documentation of this file.
17 #include <type_traits>
26 std::ostream &out)
const
30 if(f_it->second.body_available())
33 out <<
"//// Function: " << f_it->first <<
"\n";
37 output(ns, f_it->first, f_it->second.body, out);
46 std::ostream &out)
const
50 out <<
"**** " << i_it->location_number <<
" "
51 << i_it->source_location <<
"\n";
70 if(f_it->second.body_available())
81 return std::move(result);
94 std::ostringstream out;
99 {
"sourceLocation",
json_stringt(i_it->source_location.as_string())},
106 return std::move(contents);
113 xmlt program(
"program");
120 {
"body_available", f_it->second.body_available() ?
"true" :
"false"}},
123 if(f_it->second.body_available())
146 {
"source_location", i_it->source_location.as_string()}},
150 std::ostringstream out;
152 location.set_attribute(
"instruction", out.str());
157 return function_body;
165 goto_functionst::function_mapt::const_iterator
214 std::set<trace_ptrt, ai_history_baset::compare_historyt>>::value,
215 "begin must return the minimal entry");
216 auto first = working_set.begin();
220 working_set.erase(first);
239 while(!working_set.empty())
244 if(
visit(function_id, p, working_set, goto_program, goto_functions, ns))
256 goto_functionst::function_mapt::const_iterator f_it =
260 fixedpoint(start_trace, f_it->first, f_it->second.body, goto_functions, ns);
275 if(l->is_function_call())
279 "function calls only have one successor");
283 "function call successor / return location must be the next instruction");
286 function_id, p, working_set, goto_program, goto_functions, ns);
288 else if(l->is_end_function())
292 "The end function instruction should have no successors.");
295 function_id, p, working_set, goto_program, goto_functions, ns);
331 p->step(to_l, *(
storage->abstract_traces_before(to_l)), caller_history);
340 statet &new_values = *tmp_state;
343 new_values.
transform(function_id, p, to_function_id, to_p, *
this, ns);
349 merge(new_values, p, to_p) ||
361 const irep_idt &calling_function_id,
384 const irep_idt &calling_function_id,
391 locationt l_call = p_call->current_location();
404 if(callee_expression.
id() == ID_symbol)
406 const irep_idt &callee_function_id =
409 goto_functionst::function_mapt::const_iterator it =
414 "Function " +
id2string(callee_function_id) +
"not in function map");
418 if(callee_fun.body_available())
439 callee_expression.
id() == ID_symbol,
440 "Function pointers and indirect calls must be removed before "
473 const irep_idt &calling_function_id,
514 l_end->is_end_function(),
515 "The last instruction of a goto_program must be END_FUNCTION");
518 auto traces =
storage->abstract_traces_before(l_end);
520 bool new_data =
false;
527 for(
auto p_end : *traces)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
virtual jsont output_json(const namespacet &ns, const goto_functionst &goto_functions) const
Output the abstract states for the whole program as JSON.
trace_ptrt get_next(working_sett &working_set)
Get the next location from the work queue.
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)
goto_programt::const_targett locationt
trace_sett working_sett
The work queue, sorted using the history's ordering operator.
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)
virtual std::unique_ptr< statet > make_temporary_state(const statet &s)
Make a copy of a state.
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...
void put_in_working_set(working_sett &working_set, trace_ptrt t)
virtual xmlt output_xml(const namespacet &ns, const goto_functionst &goto_functions) const
Output the abstract states for the whole program as XML.
Base class for all expressions.
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...
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
static const trace_ptrt no_caller_history
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
function_mapt function_map
virtual bool is_bottom() const =0
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
codet representation of a function call statement.
virtual statet & get_state(trace_ptrt p)
Get the state for the given history, creating it with the factory if it doesn't exist.
virtual void transform(const irep_idt &function_from, trace_ptrt from, const irep_idt &function_to, trace_ptrt to, ai_baset &ai, const namespacet &ns)
how function calls are treated: a) there is an edge from each call site to the function head b) there...
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const std::string & id2string(const irep_idt &d)
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
#define PRECONDITION(CONDITION)
const irep_idt & get_identifier() const
std::unique_ptr< ai_storage_baset > storage
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
std::unique_ptr< ai_history_factory_baset > history_factory
For creating history objects.
const irep_idt & id() const
const code_function_callt & to_code_function_call(const codet &code)
virtual void finalize()
Override this to add a cleanup or post-processing step after fixedpoint has run.
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)
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 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...
::goto_functiont goto_functiont
instructionst instructions
The list of instructions in the goto program.
virtual void initialize(const irep_idt &function_id, const goto_programt &goto_program)
Initialize all the abstract states for a single function.
A collection of goto functions.
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.
A history object is an abstraction / representation of the control-flow part of a set of traces.
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.
A generic container class for the GOTO intermediate representation of one function.
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)
#define forall_goto_functions(it, functions)
ai_history_baset::trace_ptrt trace_ptrt
virtual void make_entry()=0
Make this domain a reasonable entry-point state.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
API to expression classes.
jsont & push_back(const jsont &json)
#define forall_goto_program_instructions(it, program)
xmlt & new_element(const std::string &key)
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