Go to the documentation of this file.
44 auto p = util_make_unique<rd_range_domaint>(
bv_container);
46 return std::unique_ptr<statet>(p.release());
75 valuest::const_iterator v_entry=
values.find(identifier);
76 if(v_entry==
values.end() ||
77 v_entry->second.empty())
82 for(
const auto &
id : v_entry->second)
99 locationt from{trace_from->current_location()};
100 locationt to{trace_to->current_location()};
107 "ai has type reaching_definitions_analysist");
115 else if(from->is_start_thread())
118 else if(from->is_function_call())
121 else if(from->is_end_function())
124 else if(from->is_assign())
127 else if(from->is_decl())
132 if(to->is_function_call())
140 const bool is_must_alias=rw_set.
get_w_set().size()==1;
142 for(
const auto &written_object_entry : rw_set.
get_w_set())
144 const irep_idt &identifier = written_object_entry.first;
147 if(ns.
lookup(identifier, symbol_ptr))
149 assert(symbol_ptr!=0);
152 rw_set.
get_ranges(written_object_entry.second);
158 for(
const auto &range : ranges)
159 kill(identifier, range.first, range.second);
172 const irep_idt &identifier = from->dead_symbol().get_identifier();
174 valuest::iterator entry=
values.find(identifier);
187 for(valuest::iterator it=
values.begin();
191 const irep_idt &identifier=it->first;
193 if(!ns.
lookup(identifier).is_shared() &&
198 valuest::iterator next=it;
218 if(function_from != function_to)
220 for(valuest::iterator it=
values.begin();
224 const irep_idt &identifier=it->first;
228 if((ns.
lookup(identifier, sym) ||
234 valuest::iterator next=it;
247 for(
const auto ¶m : code_type.
parameters())
249 const irep_idt &identifier=param.get_identifier();
251 if(identifier.
empty())
255 if(param_bits.has_value())
258 gen(from, identifier, 0, -1);
285 for(
const auto &new_value : new_values)
287 const irep_idt &identifier=new_value.first;
290 (!ns.
lookup(identifier).is_shared() &&
293 for(
const auto &
id : new_value.second)
300 for(
const auto &
id : new_value.second)
309 for(
const auto ¶m : code_type.
parameters())
311 const irep_idt &identifier=param.get_identifier();
313 if(identifier.
empty())
316 valuest::iterator entry=
values.find(identifier);
346 goto_rw(function_to, to, rw_set);
347 const bool is_must_alias=rw_set.
get_w_set().size()==1;
349 for(
const auto &written_object_entry : rw_set.
get_w_set())
351 const irep_idt &identifier = written_object_entry.first;
354 if(ns.
lookup(identifier, symbol_ptr))
359 "Symbol is in symbol table");
362 rw_set.
get_ranges(written_object_entry.second);
368 for(
const auto &range : ranges)
369 kill(identifier, range.first, range.second);
371 for(
const auto &range : ranges)
372 gen(from, identifier, range.first, range.second);
381 assert(range_start>=0);
389 assert(range_end>range_start);
391 valuest::iterator entry=
values.find(identifier);
395 bool clear_export_cache=
false;
398 for(values_innert::iterator
399 it=entry->second.begin();
400 it!=entry->second.end();
414 clear_export_cache=
true;
416 entry->second.erase(it++);
420 clear_export_cache=
true;
426 entry->second.erase(it++);
431 clear_export_cache=
true;
442 entry->second.erase(it++);
446 clear_export_cache=
true;
452 entry->second.erase(it++);
456 if(clear_export_cache)
459 values_innert::iterator it=entry->second.begin();
460 for(
const auto &
id : new_values)
462 while(it!=entry->second.end() && *it<
id)
464 if(it==entry->second.end() ||
id<*it)
466 entry->second.insert(it,
id);
468 else if(it!=entry->second.end())
480 assert(range_start>=0);
483 valuest::iterator entry=
values.find(identifier);
487 XXX export_cache_available=
false;
492 for(rangest::iterator it=ranges.begin();
495 if(it->second.first!=-1 &&
496 it->second.first <= range_start)
498 else if(it->first >= range_start)
504 it->second.first=range_start;
521 if(range_start==0 && range_end==0)
524 assert(range_start>=0);
527 assert(range_end>range_start || range_end==-1);
543 std::pair<valuest::iterator, bool> entry=
545 rangest &ranges=entry.first->second;
549 for(rangest::iterator it=ranges.begin();
553 if(it->second.second!=from ||
554 (it->second.first!=-1 && it->second.first <= range_start) ||
555 (range_end!=-1 && it->first >= range_end))
557 else if(it->first > range_start)
560 merged_range_end=std::max(range_end, it->second.first);
563 else if(it->second.first==-1 ||
565 it->second.first >= range_end))
572 it->second.first=range_end;
578 ranges.insert(std::make_pair(
580 std::make_pair(merged_range_end, from)));
588 out <<
"Reaching definitions:\n";
596 for(
const auto &value :
values)
598 const irep_idt &identifier=value.first;
602 out <<
" " << identifier <<
"[";
604 for(ranges_at_loct::const_iterator itl=ranges.begin();
607 for(rangest::const_iterator itr=itl->second.begin();
608 itr!=itl->second.end();
611 if(itr!=itl->second.begin() ||
615 out << itr->first <<
":" << itr->second;
616 out <<
"@" << itl->first->location_number;
633 ranges_at_loct::iterator itr=it->second.begin();
634 for(
const auto &o : ito->second)
636 while(itr!=it->second.end() && itr->first<o.first)
638 if(itr==it->second.end() || o.first<itr->first)
640 it->second.insert(o);
643 else if(itr!=it->second.end())
645 assert(itr->first==o.first);
647 for(
const auto &o_range : o.second)
648 more=
gen(itr->second, o_range.first, o_range.second) ||
655 values_innert::iterator itr=dest.begin();
656 for(
const auto &
id : other)
658 while(itr!=dest.end() && *itr<
id)
660 if(itr==dest.end() ||
id<*itr)
662 dest.insert(itr,
id);
665 else if(itr!=dest.end())
685 valuest::iterator it=
values.begin();
686 for(
const auto &value : other.
values)
688 while(it!=
values.end() && it->first<value.first)
690 if(it==
values.end() || value.first<it->first)
697 assert(it->first==value.first);
729 valuest::iterator it=
values.begin();
730 for(
const auto &value : other.
values)
732 const irep_idt &identifier=value.first;
734 if(!ns.
lookup(identifier).is_shared()
738 while(it!=
values.end() && it->first<value.first)
740 if(it==
values.end() || value.first<it->first)
747 assert(it->first==value.first);
769 export_cachet::const_iterator entry=
export_cache.find(identifier);
774 return entry->second;
780 auto value_sets_=util_make_unique<value_set_analysis_fit>(
ns);
781 (*value_sets_)(goto_functions);
784 is_threaded=util_make_unique<is_threadedt>(goto_functions);
786 is_dirty=util_make_unique<dirtyt>(goto_functions);
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
valuest values
It is an ordered map from program variable names to IDs of reaching_definitiont instances stored in m...
Variables whose address is taken.
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...
reaching_definitions_analysist(const namespacet &_ns)
#define CHECK_RETURN(CONDITION)
value_setst & get_value_sets() const
const range_domaint & get_ranges(const std::unique_ptr< range_domain_baset > &ranges) const
ai_domain_baset::locationt definition_at
The iterator to the GOTO instruction where the variable has been written to.
void transform_assign(const namespacet &ns, locationt from, const irep_idt &function_to, locationt to, reaching_definitions_analysist &rd)
static void goto_rw(const irep_idt &function, goto_programt::const_targett target, const code_assignt &assign, rw_range_sett &rw_set)
std::map< locationt, rangest > ranges_at_loct
const is_threadedt & get_is_threaded() const
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.
std::set< std::size_t > values_innert
tvt has_values
This (three value logic) flag determines, whether the instance represents top, bottom,...
bool merge(const rd_range_domaint &other, locationt from, locationt to)
Implements the join operation of two instances *this and other.
sparse_bitvector_analysist< reaching_definitiont > *const bv_container
It points to the actual reaching definitions data of individual program variables.
Expression to hold a symbol (variable)
range_spect bit_begin
The two integers below define a range of bits (i.e.
const ranges_at_loct & get(const irep_idt &identifier) const
ai_history_baset::trace_ptrt trace_ptrt
range_spect to_range_spect(const mp_integer &size)
std::size_t add(const V &value)
void transform_function_call(const namespacet &ns, const irep_idt &function_from, locationt from, const irep_idt &function_to, reaching_definitions_analysist &rd)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
std::unique_ptr< T > util_make_unique(Ts &&... ts)
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
std::unique_ptr< is_threadedt > is_threaded
irep_idt identifier
The name of the variable which was defined.
#define PRECONDITION(CONDITION)
const irep_idt & get_identifier() const
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Over-approximate Concurrency for Threaded Goto Programs.
Because the class is inherited from ai_domain_baset, its instance represents an element of a domain o...
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) final override
Computes an instance obtained from the instance *this by transformation over a GOTO instruction refer...
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...
const code_function_callt & to_code_function_call(const codet &code)
const char * to_string() const
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis,...
Value Set Propagation (flow insensitive)
const parameterst & parameters() const
std::multimap< range_spect, range_spect > rangest
bool merge_inner(values_innert &dest, const values_innert &other)
sparse_bitvector_analysist< reaching_definitiont > *const bv_container
void transform_dead(const namespacet &ns, locationt from)
Computes an instance obtained from a *this by transformation over DEAD v GOTO instruction.
virtual ~reaching_definitions_analysist()
virtual void initialize(const irep_idt &function_id, const goto_programt &goto_program)
Initialize all the abstract states for a single function.
A collection of goto functions.
goto_programt::const_targett locationt
std::unique_ptr< statet > make(locationt) const override
void transform_start_thread(const namespacet &ns, reaching_definitions_analysist &rd)
const dirtyt & get_is_dirty() const
bool merge_shared(const rd_range_domaint &other, locationt from, locationt to, const namespacet &ns)
Base class for concurrency-aware abstract interpretation.
This is the basic interface of the abstract interpreter with default implementations of the core func...
rd_range_domain_factoryt(sparse_bitvector_analysist< reaching_definitiont > *_bv_container)
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
void initialize(const goto_functionst &goto_functions) override
Initialize all the abstract states for a whole program.
ai_domain_baset::locationt locationt
export_cachet export_cache
It is a helper data structure.
void kill_inf(const irep_idt &identifier, const range_spect &range_start)
Identifies a GOTO instruction where a given variable is defined (i.e.
void kill(const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
void output(std::ostream &out, const ai_baset &, const namespacet &) const final override
void transform_end_function(const namespacet &ns, const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, reaching_definitions_analysist &rd)
std::unique_ptr< dirtyt > is_dirty
This ensures that all domains are constructed with the appropriate pointer back to the analysis engin...
void clear_cache(const irep_idt &identifier) const
std::map< irep_idt, values_innert > valuest
virtual statet & get_state(locationt l)
const V & get(const std::size_t value_index) const
std::unique_ptr< value_setst > value_sets
const objectst & get_w_set() const