30 valuest::const_iterator v_entry=
values.find(identifier);
31 if(v_entry==
values.end() ||
32 v_entry->second.empty())
37 for(
const auto &
id : v_entry->second)
57 "ai has type reaching_definitions_analysist");
65 else if(from->is_start_thread())
68 else if(from->is_function_call())
71 else if(from->is_end_function())
74 else if(from->is_assign())
77 else if(from->is_decl())
82 if(to->is_function_call())
90 const bool is_must_alias=rw_set.get_w_set().size()==1;
94 const irep_idt &identifier=it->first;
97 if(ns.
lookup(identifier, symbol_ptr))
99 assert(symbol_ptr!=0);
107 for(
const auto &range : ranges)
108 kill(identifier, range.first, range.second);
122 valuest::iterator entry=
values.find(identifier);
135 for(valuest::iterator it=
values.begin();
139 const irep_idt &identifier=it->first;
141 if(!ns.
lookup(identifier).is_shared() &&
146 valuest::iterator next=it;
170 for(valuest::iterator it=
values.begin();
174 const irep_idt &identifier=it->first;
178 if((ns.
lookup(identifier, sym) ||
184 valuest::iterator next=it;
197 for(
const auto ¶m : code_type.parameters())
199 const irep_idt &identifier=param.get_identifier();
201 if(identifier.
empty())
206 gen(from, identifier, 0, size);
233 for(
const auto &new_value : new_values)
235 const irep_idt &identifier=new_value.first;
238 (!ns.
lookup(identifier).is_shared() &&
241 for(
const auto &
id : new_value.second)
248 for(
const auto &
id : new_value.second)
258 for(
const auto ¶m : code_type.
parameters())
260 const irep_idt &identifier=param.get_identifier();
262 if(identifier.
empty())
265 valuest::iterator entry=
values.find(identifier);
295 const bool is_must_alias=rw_set.get_w_set().size()==1;
299 const irep_idt &identifier=it->first;
302 if(ns.
lookup(identifier, symbol_ptr))
307 "Symbol is in symbol table");
315 for(
const auto &range : ranges)
316 kill(identifier, range.first, range.second);
318 for(
const auto &range : ranges)
319 gen(from, identifier, range.first, range.second);
328 assert(range_start>=0);
336 assert(range_end>range_start);
338 valuest::iterator entry=
values.find(identifier);
342 bool clear_export_cache=
false;
345 for(values_innert::iterator
346 it=entry->second.begin();
347 it!=entry->second.end();
361 clear_export_cache=
true;
363 entry->second.erase(it++);
367 clear_export_cache=
true;
373 entry->second.erase(it++);
378 clear_export_cache=
true;
389 entry->second.erase(it++);
393 clear_export_cache=
true;
399 entry->second.erase(it++);
403 if(clear_export_cache)
406 values_innert::iterator it=entry->second.begin();
407 for(
const auto &
id : new_values)
409 while(it!=entry->second.end() && *it<id)
411 if(it==entry->second.end() ||
id<*it)
413 entry->second.insert(it,
id);
415 else if(it!=entry->second.end())
427 assert(range_start>=0);
430 valuest::iterator entry=
values.find(identifier);
434 XXX export_cache_available=
false;
439 for(rangest::iterator it=ranges.begin();
442 if(it->second.first!=-1 &&
443 it->second.first <= range_start)
445 else if(it->first >= range_start)
451 it->second.first=range_start;
464 if(range_start==0 && range_end==0)
467 assert(range_start>=0);
470 assert(range_end>range_start || range_end==-1);
486 std::pair<valuest::iterator, bool> entry=
488 rangest &ranges=entry.first->second;
492 for(rangest::iterator it=ranges.begin();
496 if(it->second.second!=from ||
497 (it->second.first!=-1 && it->second.first <= range_start) ||
498 (range_end!=-1 && it->first >= range_end))
500 else if(it->first > range_start)
503 merged_range_end=std::max(range_end, it->second.first);
506 else if(it->second.first==-1 ||
508 it->second.first >= range_end))
515 it->second.first=range_end;
521 ranges.insert(std::make_pair(
523 std::make_pair(merged_range_end, from)));
531 out <<
"Reaching definitions:\n";
539 for(
const auto &value :
values)
541 const irep_idt &identifier=value.first;
545 out <<
" " << identifier <<
"[";
547 for(ranges_at_loct::const_iterator itl=ranges.begin();
550 for(rangest::const_iterator itr=itl->second.begin();
551 itr!=itl->second.end();
554 if(itr!=itl->second.begin() ||
558 out << itr->first <<
":" << itr->second;
559 out <<
"@" << itl->first->location_number;
576 ranges_at_loct::iterator itr=it->second.begin();
577 for(
const auto &o : ito->second)
579 while(itr!=it->second.end() && itr->first<o.first)
581 if(itr==it->second.end() || o.first<itr->first)
583 it->second.insert(o);
586 else if(itr!=it->second.end())
588 assert(itr->first==o.first);
590 for(
const auto &o_range : o.second)
591 more=
gen(itr->second, o_range.first, o_range.second) ||
598 values_innert::iterator itr=dest.begin();
599 for(
const auto &
id : other)
601 while(itr!=dest.end() && *itr<id)
603 if(itr==dest.end() ||
id<*itr)
605 dest.insert(itr,
id);
608 else if(itr!=dest.end())
628 valuest::iterator it=
values.begin();
629 for(
const auto &value : other.
values)
631 while(it!=
values.end() && it->first<value.first)
633 if(it==
values.end() || value.first<it->first)
640 assert(it->first==value.first);
672 valuest::iterator it=
values.begin();
673 for(
const auto &value : other.
values)
675 const irep_idt &identifier=value.first;
677 if(!ns.
lookup(identifier).is_shared()
681 while(it!=
values.end() && it->first<value.first)
683 if(it==
values.end() || value.first<it->first)
690 assert(it->first==value.first);
712 export_cachet::const_iterator entry=
export_cache.find(identifier);
717 return entry->second;
734 (*value_sets_)(goto_functions);
void kill(const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Over-approximate Concurrency for Threaded Goto Programs.
#define forall_rw_range_set_w_objects(it, rw_set)
void clear_cache(const irep_idt &identifier) const
void transform_function_call(const namespacet &ns, locationt from, locationt to, reaching_definitions_analysist &rd)
ai_domain_baset::locationt definition_at
Variables whose address is taken.
const code_deadt & to_code_dead(const codet &code)
std::unordered_map< irep_idt, values_innert, irep_id_hash > valuest
const irep_idt & get_identifier() const
range_spect to_range_spect(const mp_integer &size)
void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) final
const dirtyt & get_is_dirty() const
bool merge_inner(values_innert &dest, const values_innert &other)
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
sparse_bitvector_analysist< reaching_definitiont > * bv_container
const char * to_string() const
instructionst::const_iterator const_targett
virtual ~reaching_definitions_analysist()
void kill_inf(const irep_idt &identifier, const range_spect &range_start)
void populate_cache(const irep_idt &identifier) const
bool gen(locationt from, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
void goto_rw(goto_programt::const_targett target, const code_assignt &assign, rw_range_sett &rw_set)
value_setst & get_value_sets() const
void transform_start_thread(const namespacet &ns, reaching_definitions_analysist &rd)
void transform_dead(const namespacet &ns, locationt from)
bool merge_shared(const rd_range_domaint &other, locationt from, locationt to, const namespacet &ns)
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis...
virtual void initialize(const goto_functionst &goto_functions)
std::vector< typename inner_mapt::const_iterator > values
const V & get(const std::size_t value_index) const
bool merge(const rd_range_domaint &other, locationt from, locationt to)
virtual statet & get_state(goto_programt::const_targett l)
is_threadedt * is_threaded
const parameterst & parameters() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
export_cachet export_cache
virtual void initialize(const goto_programt &)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
std::size_t add(const V &value)
goto_programt::const_targett locationt
std::multimap< range_spect, range_spect > rangest
void transform_assign(const namespacet &ns, locationt from, locationt to, reaching_definitions_analysist &rd)
Expression to hold a symbol (variable)
Value Set Propagation (flow insensitive)
void transform_end_function(const namespacet &ns, locationt from, locationt to, reaching_definitions_analysist &rd)
std::map< locationt, rangest > ranges_at_loct
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
std::set< std::size_t > values_innert
const is_threadedt & get_is_threaded() const
const ranges_at_loct & get(const irep_idt &identifier) const
const code_function_callt & to_code_function_call(const codet &code)