12 #define USE_DEPRECATED_STATIC_ANALYSIS_H 46 if(to->is_end_function())
50 assert(to->is_function_call());
71 fixedpoint(function_identifier, goto_program, goto_functions);
76 std::ostream &out)
const 80 if(f_it->second.body_available())
83 out <<
"//// Function: " << f_it->first <<
"\n";
87 output(f_it->second.body, f_it->first, out);
95 std::ostream &out)
const 99 out <<
"**** " << i_it->location_number <<
" " 100 << i_it->source_location <<
"\n";
129 update(f_it->second.body);
157 assert(!working_set.empty());
159 working_sett::iterator i=working_set.begin();
161 working_set.erase(i);
167 const irep_idt &function_identifier,
182 while(!working_set.empty())
186 if(
visit(function_identifier, l, working_set, goto_program, goto_functions))
194 const irep_idt &function_identifier,
211 std::unique_ptr<statet> tmp_state(
214 statet &new_values=*tmp_state;
216 if(l->is_function_call())
233 ns, function_identifier, l, function_identifier, to_l);
237 bool have_new_values=
238 merge(other, new_values, to_l);
243 if(have_new_values || !other.
seen)
255 const goto_functionst::function_mapt::const_iterator f_it,
261 if(!goto_function.body_available())
264 assert(!goto_function.body.instructions.empty());
268 locationt l_begin=goto_function.body.instructions.begin();
272 tmp_state->
transform(
ns, calling_function, l_call, f_it->first, l_begin);
279 if(
merge(begin_state, *tmp_state, l_begin))
294 fixedpoint(f_it->first, goto_function.body, goto_functions);
300 locationt l_end=--goto_function.body.instructions.end();
302 assert(l_end->is_end_function());
307 std::unique_ptr<statet> tmp_state(
309 tmp_state->
transform(
ns, f_it->first, l_end, calling_function, l_return);
314 merge(new_state, *tmp_state, l_return);
320 ns, calling_function, l_call, calling_function, l_return);
328 const exprt &
function,
337 if(
function.
id()==ID_symbol)
349 goto_functionst::function_mapt::const_iterator it=
353 throw "failed to find function "+
id2string(identifier);
366 else if(
function.
id()==ID_if)
368 if(
function.operands().size()!=3)
369 throw "if takes three arguments";
391 merge(new_state, *n2, l_return);
393 else if(
function.
id()==ID_dereference)
396 std::list<exprt> values;
402 for(
const auto &value : values)
404 if(value.id()==ID_object_descriptor)
416 merge(new_state, *n2, l_return);
420 else if(
function.
id() == ID_null_object ||
421 function.
id() == ID_integer_address)
425 else if(
function.
id()==ID_member ||
function.
id()==ID_index)
429 else if(
function.
id()==
"builtin-function")
435 throw "unexpected function_call argument: "+
436 function.id_string();
447 fixedpoint(it->first, it->second.body, goto_functions);
468 const irep_idt &_function_identifier,
471 : function_identifier(_function_identifier),
472 goto_program(&_goto_program),
482 typedef std::list<wl_entryt> thread_wlt;
483 thread_wlt thread_wl;
488 if(is_threaded(t_it))
490 thread_wl.push_back(wl_entryt(it->first, it->second.body, t_it));
493 it->second.body.instructions.end();
503 bool new_shared=
true;
508 for(
const auto &thread : thread_wl)
514 merge(begin_state, shared_state, thread.location);
516 while(!working_set.empty())
521 thread.function_identifier,
524 *thread.goto_program,
530 if(l->is_end_function())
533 new_shared|=
merge_shared(shared_state, end_state, sh_target);
const irept & get_nil_irep()
static exprt get_guard(locationt from, locationt to)
virtual std::unique_ptr< statet > make_temporary_state(statet &s)=0
Over-approximate Concurrency for Threaded Goto Programs.
std::map< unsigned, locationt > working_sett
const std::string & id2string(const irep_idt &d)
virtual statet & get_state(locationt l)=0
recursion_sett recursion_set
Deprecated expression utility functions.
void sequential_fixedpoint(const goto_functionst &goto_functions)
const irep_idt & get_identifier() const
virtual void output(const goto_functionst &goto_functions, std::ostream &out) const
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
void do_function_call_rec(const irep_idt &calling_function, locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions)
virtual bool merge_shared(statet &a, const statet &b, 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.
static exprt get_return_lhs(locationt to)
void do_function_call(const irep_idt &calling_function, locationt l_call, locationt l_return, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, statet &new_state)
virtual bool has_location(locationt l) const =0
bool visit(const irep_idt &function_identifier, locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions)
virtual void generate_state(locationt l)=0
functions_donet functions_done
virtual void output(const namespacet &, std::ostream &) const
void put_in_working_set(working_sett &working_set, locationt l)
The Boolean constant true.
virtual bool merge(statet &a, const statet &b, locationt to)=0
instructionst instructions
The list of instructions in the goto program.
API to expression classes.
instructionst::const_iterator const_targett
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
::goto_functiont goto_functiont
void concurrent_fixedpoint(const goto_functionst &goto_functions)
goto_programt::const_targett locationt
Split an expression into a base object and a (byte) offset.
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 void get_reference_set(locationt l, const exprt &expr, std::list< exprt > &dest)=0
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
virtual void operator()(const irep_idt &function_identifier, const goto_programt &goto_program)
std::vector< exprt > operandst
void generate_states(const goto_functionst &goto_functions)
A generic container class for the GOTO intermediate representation of one function.
targett add_instruction()
Adds an instruction at the end.
Base class for all expressions.
virtual void update(const goto_programt &goto_program)
bool fixedpoint(const irep_idt &function_identifier, const goto_programt &goto_program, const goto_functionst &goto_functions)
locationt get_next(working_sett &working_set)
virtual void initialize(const goto_programt &goto_program)
virtual void transform(const namespacet &ns, const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to)=0
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true ...
const code_function_callt & to_code_function_call(const codet &code)