27 std::ostream &out)
const 31 if(f_it->second.body_available())
34 out <<
"//// Function: " << f_it->first <<
"\n";
38 output(ns, f_it->second.body, f_it->first, out);
47 std::ostream &out)
const 51 out <<
"**** " << i_it->location_number <<
" " 52 << i_it->source_location <<
"\n";
71 if(f_it->second.body_available())
82 return std::move(result);
101 location[
"locationNumber"]=
103 location[
"sourceLocation"]=
105 location[
"abstractState"] =
109 std::ostringstream out;
116 return std::move(contents);
123 xmlt program(
"program");
127 xmlt function(
"function");
129 function.set_attribute(
131 f_it->second.body_available() ?
"true" :
"false");
133 if(f_it->second.body_available())
135 function.new_element(
output_xml(ns, f_it->second.body, f_it->first));
165 i_it->source_location.as_string());
170 std::ostringstream out;
177 return function_body;
184 goto_functionst::function_mapt::const_iterator
226 working_sett::iterator i=working_set.begin();
228 working_set.erase(i);
234 const irep_idt &function_identifier,
242 if(!goto_program.
empty())
249 while(!working_set.empty())
255 function_identifier, l, working_set, goto_program, goto_functions, ns))
263 const irep_idt &function_identifier,
279 std::unique_ptr<statet> tmp_state(
282 statet &new_values=*tmp_state;
284 bool have_new_values=
false;
286 if(l->is_function_call() &&
301 have_new_values=
true;
309 function_identifier, l, function_identifier, to_l, *
this, ns);
311 if(
merge(new_values, l, to_l))
312 have_new_values=
true;
326 const irep_idt &calling_function_identifier,
330 const goto_functionst::function_mapt::const_iterator f_it,
342 if(!goto_function.body_available())
347 calling_function_identifier,
349 calling_function_identifier,
354 return merge(*tmp_state, l_call, l_return);
357 assert(!goto_function.body.instructions.empty());
363 locationt l_begin=goto_function.body.instructions.begin();
370 calling_function_identifier, l_call, f_it->first, l_begin, *
this, ns);
375 if(
merge(*tmp_state, l_call, l_begin))
380 fixedpoint(f_it->first, goto_function.body, goto_functions, ns);
387 locationt l_end=--goto_function.body.instructions.end();
388 assert(l_end->is_end_function());
393 if(end_state.is_bottom())
398 f_it->first, l_end, calling_function_identifier, l_return, *
this, ns);
401 return merge(*tmp_state, l_end, l_return);
406 const irep_idt &calling_function_identifier,
409 const exprt &
function,
419 function.
id() == ID_symbol,
420 "Function pointers and indirect calls must be removed before analysis.");
426 goto_functionst::function_mapt::const_iterator it =
431 "Function " +
id2string(identifier) +
"not in function map");
434 calling_function_identifier,
449 goto_functionst::function_mapt::const_iterator
453 fixedpoint(f_it->first, f_it->second.body, goto_functions, ns);
474 const irep_idt &_function_identifier,
477 : function_identifier(_function_identifier),
478 goto_program(&_goto_program),
488 typedef std::list<wl_entryt> thread_wlt;
489 thread_wlt thread_wl;
494 if(is_threaded(t_it))
496 thread_wl.push_back(wl_entryt(it->first, it->second.body, t_it));
499 it->second.body.instructions.end();
508 bool new_shared=
true;
513 for(
const auto &wl_entry : thread_wl)
519 merge(begin_state, sh_target, wl_entry.location);
521 while(!working_set.empty())
526 wl_entry.function_identifier,
529 *(wl_entry.goto_program),
536 if(l->is_end_function())
537 new_shared|=
merge_shared(shared_state, l, sh_target, ns);
virtual statet & get_state(locationt l)=0
Get the state for the given location, creating it in a default way if it doesn't exist.
Over-approximate Concurrency for Threaded Goto Programs.
virtual void make_bottom()=0
no states
const std::string & id2string(const irep_idt &d)
void put_in_working_set(working_sett &working_set, locationt l)
goto_programt::const_targett locationt
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
const irep_idt & get_identifier() const
virtual void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, ai_baset &ai, const namespacet &ns)=0
how function calls are treated: a) there is an edge from each call site to the function head b) there...
virtual bool merge(const statet &src, locationt from, locationt to)=0
function_mapt function_map
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
virtual std::unique_ptr< statet > abstract_state_before(locationt l) const =0
Get a copy of the abstract state before the given instruction, without needing to know what kind of d...
virtual jsont output_json(const namespacet &ns, const goto_functionst &goto_functions) const
Output the abstract states for the whole program as JSON.
std::map< unsigned, locationt > working_sett
The work queue, sorted by location number.
virtual void output(const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
Output the abstract states for a whole program.
jsont & push_back(const jsont &json)
bool do_function_call_rec(const irep_idt &calling_function_identifier, locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, const goto_functionst &goto_functions, const namespacet &ns)
virtual void initialize(const goto_programt &goto_program)
Initialize all the abstract states for a single function.
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
instructionst instructions
The list of instructions in the goto program.
API to expression classes.
void set_attribute(const std::string &attribute, unsigned value)
instructionst::const_iterator const_targett
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
::goto_functiont goto_functiont
#define PRECONDITION(CONDITION)
codet representation of a function call statement.
A collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
virtual bool merge_shared(const statet &src, locationt from, locationt to, const namespacet &ns)=0
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
virtual void finalize()
Override this to add a cleanup or post-processing step after fixedpoint has run.
void sequential_fixedpoint(const goto_functionst &goto_functions, const namespacet &ns)
std::vector< exprt > operandst
A generic container class for the GOTO intermediate representation of one function.
bool fixedpoint(const irep_idt &function_identifier, 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)=0
Make a copy of a state.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
bool visit(const irep_idt &function_identifier, locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
Perform one step of abstract interpretation from location l Depending on the instruction type it may ...
xmlt & new_element(const std::string &key)
targett add_instruction()
Adds an instruction at the end.
Base class for all expressions.
locationt get_next(working_sett &working_set)
Get the next location from the work queue.
bool empty() const
Is the program empty?
bool do_function_call(const irep_idt &calling_function_identifier, locationt l_call, locationt l_return, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, const namespacet &ns)
void concurrent_fixedpoint(const goto_functionst &goto_functions, const namespacet &ns)
virtual xmlt output_xml(const namespacet &ns, const goto_functionst &goto_functions) const
Output the abstract states for the whole program as XML.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define forall_goto_functions(it, functions)
void 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 ...
#define forall_goto_program_instructions(it, program)
const code_function_callt & to_code_function_call(const codet &code)