50 valuest::const_iterator v_entry=
values.find(identifier);
51 if(v_entry==
values.end() ||
52 v_entry->second.empty())
57 for(
const auto &
id : v_entry->second)
79 "ai has type reaching_definitions_analysist");
87 else if(from->is_start_thread())
90 else if(from->is_function_call())
93 else if(from->is_end_function())
96 else if(from->is_assign())
99 else if(from->is_decl())
104 if(to->is_function_call())
112 const bool is_must_alias=rw_set.get_w_set().size()==1;
116 const irep_idt &identifier=it->first;
119 if(ns.
lookup(identifier, symbol_ptr))
121 assert(symbol_ptr!=0);
129 for(
const auto &range : ranges)
130 kill(identifier, range.first, range.second);
145 valuest::iterator entry=
values.find(identifier);
158 for(valuest::iterator it=
values.begin();
162 const irep_idt &identifier=it->first;
164 if(!ns.
lookup(identifier).is_shared() &&
169 valuest::iterator next=it;
189 if(function_from != function_to)
191 for(valuest::iterator it=
values.begin();
195 const irep_idt &identifier=it->first;
199 if((ns.
lookup(identifier, sym) ||
205 valuest::iterator next=it;
218 for(
const auto ¶m : code_type.parameters())
220 const irep_idt &identifier=param.get_identifier();
222 if(identifier.
empty())
226 if(param_bits.has_value())
229 gen(from, identifier, 0, -1);
255 for(
const auto &new_value : new_values)
257 const irep_idt &identifier=new_value.first;
260 (!ns.
lookup(identifier).is_shared() &&
263 for(
const auto &
id : new_value.second)
270 for(
const auto &
id : new_value.second)
279 for(
const auto ¶m : code_type.
parameters())
281 const irep_idt &identifier=param.get_identifier();
283 if(identifier.
empty())
286 valuest::iterator entry=
values.find(identifier);
316 const bool is_must_alias=rw_set.get_w_set().size()==1;
320 const irep_idt &identifier=it->first;
323 if(ns.
lookup(identifier, symbol_ptr))
328 "Symbol is in symbol table");
336 for(
const auto &range : ranges)
337 kill(identifier, range.first, range.second);
339 for(
const auto &range : ranges)
340 gen(from, identifier, range.first, range.second);
349 assert(range_start>=0);
357 assert(range_end>range_start);
359 valuest::iterator entry=
values.find(identifier);
363 bool clear_export_cache=
false;
366 for(values_innert::iterator
367 it=entry->second.begin();
368 it!=entry->second.end();
382 clear_export_cache=
true;
384 entry->second.erase(it++);
388 clear_export_cache=
true;
394 entry->second.erase(it++);
399 clear_export_cache=
true;
410 entry->second.erase(it++);
414 clear_export_cache=
true;
420 entry->second.erase(it++);
424 if(clear_export_cache)
427 values_innert::iterator it=entry->second.begin();
428 for(
const auto &
id : new_values)
430 while(it!=entry->second.end() && *it<id)
432 if(it==entry->second.end() ||
id<*it)
434 entry->second.insert(it,
id);
436 else if(it!=entry->second.end())
448 assert(range_start>=0);
451 valuest::iterator entry=
values.find(identifier);
455 XXX export_cache_available=
false;
460 for(rangest::iterator it=ranges.begin();
463 if(it->second.first!=-1 &&
464 it->second.first <= range_start)
466 else if(it->first >= range_start)
472 it->second.first=range_start;
489 if(range_start==0 && range_end==0)
492 assert(range_start>=0);
495 assert(range_end>range_start || range_end==-1);
511 std::pair<valuest::iterator, bool> entry=
513 rangest &ranges=entry.first->second;
517 for(rangest::iterator it=ranges.begin();
521 if(it->second.second!=from ||
522 (it->second.first!=-1 && it->second.first <= range_start) ||
523 (range_end!=-1 && it->first >= range_end))
525 else if(it->first > range_start)
528 merged_range_end=std::max(range_end, it->second.first);
531 else if(it->second.first==-1 ||
533 it->second.first >= range_end))
540 it->second.first=range_end;
546 ranges.insert(std::make_pair(
548 std::make_pair(merged_range_end, from)));
556 out <<
"Reaching definitions:\n";
564 for(
const auto &value :
values)
566 const irep_idt &identifier=value.first;
570 out <<
" " << identifier <<
"[";
572 for(ranges_at_loct::const_iterator itl=ranges.begin();
575 for(rangest::const_iterator itr=itl->second.begin();
576 itr!=itl->second.end();
579 if(itr!=itl->second.begin() ||
583 out << itr->first <<
":" << itr->second;
584 out <<
"@" << itl->first->location_number;
601 ranges_at_loct::iterator itr=it->second.begin();
602 for(
const auto &o : ito->second)
604 while(itr!=it->second.end() && itr->first<o.first)
606 if(itr==it->second.end() || o.first<itr->first)
608 it->second.insert(o);
611 else if(itr!=it->second.end())
613 assert(itr->first==o.first);
615 for(
const auto &o_range : o.second)
616 more=
gen(itr->second, o_range.first, o_range.second) ||
623 values_innert::iterator itr=dest.begin();
624 for(
const auto &
id : other)
626 while(itr!=dest.end() && *itr<id)
628 if(itr==dest.end() ||
id<*itr)
630 dest.insert(itr,
id);
633 else if(itr!=dest.end())
653 valuest::iterator it=
values.begin();
654 for(
const auto &value : other.
values)
656 while(it!=
values.end() && it->first<value.first)
658 if(it==
values.end() || value.first<it->first)
665 assert(it->first==value.first);
697 valuest::iterator it=
values.begin();
698 for(
const auto &value : other.
values)
700 const irep_idt &identifier=value.first;
702 if(!ns.
lookup(identifier).is_shared()
706 while(it!=
values.end() && it->first<value.first)
708 if(it==
values.end() || value.first<it->first)
715 assert(it->first==value.first);
737 export_cachet::const_iterator entry=
export_cache.find(identifier);
742 return entry->second;
748 auto value_sets_=util_make_unique<value_set_analysis_fit>(
ns);
749 (*value_sets_)(goto_functions);
752 is_threaded=util_make_unique<is_threadedt>(goto_functions);
754 is_dirty=util_make_unique<dirtyt>(goto_functions);
void kill(const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
void initialize(const goto_functionst &goto_functions) override
Initialize all the abstract states for a whole program.
void transform_end_function(const namespacet &ns, const irep_idt &function_from, locationt from, locationt to, reaching_definitions_analysist &rd)
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
ai_domain_baset::locationt definition_at
The iterator to the GOTO instruction where the variable has been written to.
Variables whose address is taken.
const code_deadt & to_code_dead(const codet &code)
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const irep_idt & get_identifier() const
range_spect to_range_spect(const mp_integer &size)
std::unique_ptr< dirtyt > is_dirty
const dirtyt & get_is_dirty() const
bool merge_inner(values_innert &dest, const values_innert &other)
Identifies a GOTO instruction where a given variable is defined (i.e.
range_spect bit_begin
The two integers below define a range of bits (i.e.
sparse_bitvector_analysist< reaching_definitiont > * bv_container
It points to the actual reaching definitions data of individual program variables.
statet & get_state(locationt l) override
Get the state for the given location, creating it in a default way if it doesn't exist.
const char * to_string() const
virtual void initialize(const goto_programt &goto_program)
Initialize all the abstract states for a single function.
void transform_function_call(const namespacet &ns, const irep_idt &function_from, locationt from, const irep_idt &function_to, reaching_definitions_analysist &rd)
irep_idt identifier
The name of the variable which was defined.
virtual ~reaching_definitions_analysist()
void kill_inf(const irep_idt &identifier, const range_spect &range_start)
void populate_cache(const irep_idt &identifier) const
Given the passed variable name identifier it collects data from bv_container for each ID in values[id...
std::unordered_map< irep_idt, values_innert > valuest
bool gen(locationt from, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
A utility function which updates internal data structures by inserting a new reaching definition reco...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void goto_rw(goto_programt::const_targett target, const code_assignt &assign, rw_range_sett &rw_set)
std::unique_ptr< value_setst > value_sets
value_setst & get_value_sets() const
void transform_start_thread(const namespacet &ns, reaching_definitions_analysist &rd)
codet representation of a function call statement.
void output(std::ostream &out, const ai_baset &, const namespacet &) const final override
A collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Because the class is inherited from ai_domain_baset, its instance represents an element of a domain o...
void transform_dead(const namespacet &ns, locationt from)
Computes an instance obtained from a *this by transformation over DEAD v GOTO instruction.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
bool merge_shared(const rd_range_domaint &other, locationt from, locationt to, const namespacet &ns)
tvt has_values
This (three value logic) flag determines, whether the instance represents top, bottom, or any other element of the lattice, by values TRUE, FALSE, and UNKNOWN respectively.
valuest values
It is an ordered map from program variable names to IDs of reaching_definitiont instances stored in m...
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis...
std::vector< typename inner_mapt::const_iterator > values
It is a map from an ID to the corresponding reaching_definitiont instance inside the map value_map...
const V & get(const std::size_t value_index) const
bool merge(const rd_range_domaint &other, locationt from, locationt to)
Implements the join operation of two instances *this and other`.
The basic interface of an abstract interpreter.
void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, ai_baset &ai, const namespacet &ns) final override
Computes an instance obtained from the instance *this by transformation over a GOTO instruction refer...
const parameterst & parameters() const
export_cachet export_cache
It is a helper data structure.
reaching_definitions_analysist(const namespacet &_ns)
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)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
std::unique_ptr< is_threadedt > is_threaded
std::map< locationt, rangest > ranges_at_loct
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
const irep_idt & get_identifier() const
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)