28 std::ostringstream out;
38 std::ostringstream out;
57 if(condition.
id()==ID_index)
61 if(!no_simplification)
64 return no_simplification;
66 else if(condition.
id()==ID_dereference)
70 if(!no_simplification)
73 return no_simplification;
75 else if(condition.
id()==ID_member)
83 if(!no_simplification)
86 return no_simplification;
95 std::ostream &out)
const 99 if(f_it->second.body_available())
102 out <<
"//// Function: " << f_it->first <<
"\n";
106 output(ns, f_it->second.body, f_it->first, out);
115 std::ostream &out)
const 119 out <<
"**** " << i_it->location_number <<
" " 120 << i_it->source_location <<
"\n";
122 find_state(i_it).output(out, *
this, ns);
142 if(f_it->second.body_available())
169 location[
"locationNumber"]=
171 location[
"sourceLocation"]=
173 location[
"domain"]=find_state(i_it).output_json(*
this, ns);
176 std::ostringstream out;
193 xmlt program(
"program");
197 xmlt function(
"function");
199 function.set_attribute(
201 f_it->second.body_available() ?
"true" :
"false");
203 if(f_it->second.body_available())
205 function.new_element(
output_xml(ns, f_it->second.body, f_it->first));
229 std::to_string(i_it->location_number));
232 i_it->source_location.as_string());
237 std::ostringstream out;
244 return function_body;
251 goto_functionst::function_mapt::const_iterator
255 entry_state(f_it->second.body);
266 initialize(goto_function.body);
274 get_state(i_it).make_bottom();
280 initialize(it->second);
286 assert(!working_set.empty());
288 working_sett::iterator i=working_set.begin();
290 working_set.erase(i);
303 if(!goto_program.
empty())
310 while(!working_set.empty())
314 if(visit(l, working_set, goto_program, goto_functions, ns))
330 statet ¤t=get_state(l);
337 std::unique_ptr<statet> tmp_state(
338 make_temporary_state(current));
340 statet &new_values=*tmp_state;
342 bool have_new_values=
false;
344 if(l->is_function_call() &&
351 if(do_function_call_rec(
356 have_new_values=
true;
363 new_values.
transform(l, to_l, *
this, ns);
365 if(merge(new_values, l, to_l))
366 have_new_values=
true;
372 put_in_working_set(working_set, to_l);
382 const goto_functionst::function_mapt::const_iterator f_it,
392 if(!goto_function.body_available())
395 std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_call)));
396 tmp_state->transform(l_call, l_return, *
this, ns);
398 return merge(*tmp_state, l_call, l_return);
401 assert(!goto_function.body.instructions.empty());
407 locationt l_begin=goto_function.body.instructions.begin();
412 std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_call)));
413 tmp_state->transform(l_call, l_begin, *
this, ns);
418 if(merge(*tmp_state, l_call, l_begin))
423 fixedpoint(goto_function.body, goto_functions, ns);
430 locationt l_end=--goto_function.body.instructions.end();
431 assert(l_end->is_end_function());
434 std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_end)));
435 tmp_state->transform(l_end, l_return, *
this, ns);
438 return merge(*tmp_state, l_end, l_return);
444 const exprt &
function,
453 if(
function.
id()==ID_symbol)
455 const irep_idt &identifier=
function.get(ID_identifier);
457 if(recursion_set.find(identifier)!=recursion_set.end())
463 recursion_set.insert(identifier);
465 goto_functionst::function_mapt::const_iterator it=
469 throw "failed to find function "+
id2string(identifier);
471 new_data=do_function_call(
478 recursion_set.erase(identifier);
480 else if(
function.
id()==ID_if)
482 if(
function.operands().size()!=3)
483 throw "if has three operands";
486 do_function_call_rec(
494 do_function_call_rec(
501 if(new_data1 || new_data2)
504 else if(
function.
id()==ID_dereference)
509 else if(
function.
id()==
"NULL-object")
513 else if(
function.
id()==ID_member ||
function.
id()==ID_index)
519 throw "unexpected function_call argument: "+
520 function.id_string();
530 goto_functionst::function_mapt::const_iterator
534 fixedpoint(f_it->second.body, goto_functions, ns);
541 sequential_fixedpoint(goto_functions, ns);
550 statet &shared_state=get_state(sh_target);
554 thread_wlt thread_wl;
559 if(is_threaded(t_it))
561 thread_wl.push_back(std::make_pair(&(it->second.body), t_it));
564 it->second.body.instructions.end();
567 merge_shared(shared_state, l_end, sh_target, ns);
573 bool new_shared=
true;
578 for(
const auto &wl_pair : thread_wl)
581 put_in_working_set(working_set, wl_pair.second);
583 statet &begin_state=get_state(wl_pair.second);
584 merge(begin_state, sh_target, wl_pair.second);
586 while(!working_set.empty())
590 visit(l, working_set, *(wl_pair.first), goto_functions, ns);
595 if(l->is_end_function())
596 new_shared|=merge_shared(shared_state, l, sh_target, ns);
Over-approximate Concurrency for Threaded Goto Programs.
targett add_instruction()
Adds an instruction at the end.
const std::string & id2string(const irep_idt &d)
goto_programt::const_targett locationt
exprt simplify_expr(const exprt &src, const namespacet &ns)
instructionst instructions
The list of instructions in the goto program.
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
virtual jsont output_json(const ai_baset &ai, const namespacet &ns) const
bool empty() const
Is the program empty?
virtual jsont output_json(const namespacet &ns, const goto_functionst &goto_functions) const
Output the domains for the whole program as JSON.
xmlt xml(const source_locationt &location)
virtual void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)=0
std::list< Target > get_successors(Target target) const
Extract member of struct or union.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
std::map< unsigned, locationt > working_sett
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
virtual void output(const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
jsont & push_back(const jsont &json)
const exprt & compound() const
const irep_idt & id() const
instructionst::const_iterator const_targett
bool do_function_call_rec(locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, const goto_functionst &goto_functions, const namespacet &ns)
bool do_function_call(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)
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const
Operator to dereference a pointer.
static irep_idt entry_point()
API to expression classes.
void set_attribute(const std::string &attribute, unsigned value)
void entry_state(const goto_programt &)
goto_function_templatet< goto_programt > goto_functiont
function_mapt function_map
xmlt & new_element(const std::string &name)
void sequential_fixedpoint(const goto_functionst &goto_functions, const namespacet &ns)
std::vector< exprt > operandst
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
bool fixedpoint(const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
bool visit(locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
virtual bool ai_simplify_lhs(exprt &condition, const namespacet &ns) const
Use the information in the domain to simplify the expression on the LHS of an assignment.
virtual xmlt output_xml(const ai_baset &ai, const namespacet &ns) const
Base class for all expressions.
virtual void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const
locationt get_next(working_sett &working_set)
virtual void initialize(const goto_programt &)
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 domains for the whole program as XML.
#define forall_goto_functions(it, functions)
std::ostream & output_instruction(const class namespacet &ns, const irep_idt &identifier, std::ostream &out, instructionst::const_iterator it) const
See below.
#define forall_goto_program_instructions(it, program)
json_objectt json(const source_locationt &location)
const code_function_callt & to_code_function_call(const codet &code)
virtual void make_entry()=0