46 return std::unique_ptr<statet>(p.release());
84 for(
const auto &
id :
v_entry->second)
109 "ai has type reaching_definitions_analysist");
117 else if(
from->is_start_thread())
120 else if(
from->is_function_call())
123 else if(
from->is_end_function())
126 else if(
from->is_assign())
129 else if(
from->is_decl())
132 else if(
from->is_other())
142 const irep_idt &identifier =
from->dead_symbol().get_identifier();
144 valuest::iterator entry=
values.find(identifier);
157 for(valuest::iterator it=
values.begin();
161 const irep_idt &identifier=it->first;
163 if(!ns.
lookup(identifier).is_shared() &&
168 valuest::iterator next=it;
189 for(valuest::iterator it=
values.begin();
193 const irep_idt &identifier=it->first;
198 !
sym->is_shared()) &&
203 valuest::iterator next=it;
219 if(identifier.
empty())
238 if(
from->call_lhs().is_not_nil())
260 const irep_idt &identifier=new_value.first;
263 (!ns.
lookup(identifier).is_shared() &&
266 for(
const auto &
id : new_value.second)
273 for(
const auto &
id : new_value.second)
286 if(identifier.
empty())
289 valuest::iterator entry=
values.find(identifier);
299 if(
call->call_lhs().is_not_nil())
326 "Symbol is in symbol table");
335 for(
const auto &range :
ranges)
336 kill(identifier, range.first, range.second);
338 for(
const auto &range :
ranges)
339 gen(
from, identifier, range.first, range.second);
358 valuest::iterator entry=
values.find(identifier);
365 for(values_innert::iterator
366 it=entry->second.begin();
367 it!=entry->second.end();
384 entry->second.erase(it++);
394 entry->second.erase(it++);
409 entry->second.erase(it++);
419 entry->second.erase(it++);
426 values_innert::iterator it=entry->second.begin();
429 while(it!=entry->second.end() && *it<id)
431 if(it==entry->second.end() ||
id<*it)
433 entry->second.insert(it,
id);
435 else if(it!=entry->second.end())
450 valuest::iterator entry=
values.find(identifier);
459 for(rangest::iterator it=
ranges.begin();
462 if(it->second.first!=-1 &&
503 std::pair<valuest::iterator, bool> entry=
509 for(rangest::iterator it=
ranges.begin();
513 if(it->second.second!=
from ||
514 (it->second.first!=-1 && it->second.first <=
range_start) ||
523 else if(it->second.first==-1 ||
538 ranges.insert(std::make_pair(
548 out <<
"Reaching definitions:\n";
556 for(
const auto &value :
values)
558 const irep_idt &identifier=value.first;
562 out <<
" " << identifier <<
"[";
564 for(ranges_at_loct::const_iterator
itl=
ranges.begin();
567 for(rangest::const_iterator
itr=
itl->second.begin();
571 if(
itr!=
itl->second.begin() ||
575 out <<
itr->first <<
":" <<
itr->second;
576 out <<
"@" <<
itl->first->location_number;
593 ranges_at_loct::iterator
itr=it->second.begin();
594 for(
const auto &o :
ito->second)
596 while(
itr!=it->second.end() &&
itr->first<o.first)
598 if(
itr==it->second.end() || o.first<
itr->first)
600 it->second.insert(o);
603 else if(
itr!=it->second.end())
607 for(
const auto &
o_range : o.second)
615 values_innert::iterator
itr=dest.begin();
616 for(
const auto &
id : other)
618 while(
itr!=dest.end() && *
itr<id)
620 if(
itr==dest.end() ||
id<*
itr)
622 dest.insert(
itr,
id);
625 else if(
itr!=dest.end())
644 valuest::iterator it=
values.begin();
645 for(
const auto &value : other.
values)
647 while(it!=
values.end() && it->first<value.first)
649 if(it==
values.end() || value.first<it->first)
688 valuest::iterator it=
values.begin();
689 for(
const auto &value : other.
values)
691 const irep_idt &identifier=value.first;
693 if(!ns.
lookup(identifier).is_shared()
697 while(it!=
values.end() && it->first<value.first)
699 if(it==
values.end() || value.first<it->first)
728 export_cachet::const_iterator entry=
export_cache.find(identifier);
733 return entry->second;
739 auto value_sets_ = std::make_unique<value_set_analysis_fit>(
ns);
740 (*value_sets_)(goto_functions);
743 is_threaded = std::make_unique<is_threadedt>(goto_functions);
745 is_dirty = std::make_unique<dirtyt>(goto_functions);
Generic exception types primarily designed for use with invariants.
This is the basic interface of the abstract interpreter with default implementations of the core func...
virtual void initialize(const irep_idt &function_id, const goto_programt &goto_program)
Initialize all the abstract states for a single function.
ai_history_baset::trace_ptrt trace_ptrt
goto_programt::const_targett locationt
ai_domain_factory_baset::locationt locationt
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Base class for concurrency-aware abstract interpretation.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A collection of goto functions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Data type to describe upper and lower bounds of the range of bits that a read or write access may aff...
static range_spect unknown()
static range_spect to_range_spect(const mp_integer &size)
This ensures that all domains are constructed with the appropriate pointer back to the analysis engin...
rd_range_domain_factoryt(sparse_bitvector_analysist< reaching_definitiont > *_bv_container, message_handlert &message_handler)
std::unique_ptr< statet > make(locationt) const override
message_handlert & message_handler
sparse_bitvector_analysist< reaching_definitiont > *const bv_container
Because the class is inherited from ai_domain_baset, its instance represents an element of a domain o...
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...
export_cachet export_cache
It is a helper data structure.
void output(std::ostream &out, const ai_baset &, const namespacet &) const final override
void kill_inf(const irep_idt &identifier, const range_spect &range_start)
void transform_dead(const namespacet &ns, locationt from)
Computes an instance obtained from a *this by transformation over DEAD v GOTO instruction.
void transform_start_thread(const namespacet &ns, reaching_definitions_analysist &rd)
const ranges_at_loct & get(const irep_idt &identifier) const
void clear_cache(const irep_idt &identifier) const
sparse_bitvector_analysist< reaching_definitiont > *const bv_container
It points to the actual reaching definitions data of individual program variables.
void transform_function_call(const namespacet &ns, const irep_idt &function_from, locationt from, const irep_idt &function_to, reaching_definitions_analysist &rd)
bool merge(const rd_range_domaint &other, trace_ptrt from, trace_ptrt to)
Implements the "join" operation of two instances *this and other.
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)
void transform_assign(const namespacet &ns, locationt from, const irep_idt &function_to, locationt to, reaching_definitions_analysist &rd)
bool merge_inner(values_innert &dest, const values_innert &other)
std::multimap< range_spect, range_spect > rangest
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...
void kill(const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
std::map< locationt, rangest, goto_programt::target_less_than > ranges_at_loct
tvt has_values
This (three value logic) flag determines, whether the instance represents top, bottom,...
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...
std::map< irep_idt, values_innert > valuest
valuest values
It is an ordered map from program variable names to IDs of reaching_definitiont instances stored in m...
bool merge_shared(const rd_range_domaint &other, locationt from, locationt to, const namespacet &ns)
std::set< std::size_t > values_innert
message_handlert & message_handler
value_setst & get_value_sets() const
virtual ~reaching_definitions_analysist()
std::unique_ptr< is_threadedt > is_threaded
const dirtyt & get_is_dirty() const
const is_threadedt & get_is_threaded() const
std::unique_ptr< dirtyt > is_dirty
std::unique_ptr< value_setst > value_sets
reaching_definitions_analysist(const namespacet &_ns, message_handlert &)
void initialize(const goto_functionst &goto_functions) override
Initialize all the abstract states for a whole program.
const V & get(const std::size_t value_index) 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::size_t add(const V &value)
Expression to hold a symbol (variable)
const char * to_string() const
Variables whose address is taken.
static void goto_rw(const irep_idt &function, goto_programt::const_targett target, const exprt &lhs, const exprt &function_expr, const exprt::operandst &arguments, rw_range_sett &rw_set)
Over-approximate Concurrency for Threaded Goto Programs.
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis,...
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
#define CHECK_RETURN(CONDITION)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
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.
ai_domain_baset::locationt definition_at
The iterator to the GOTO instruction where the variable has been written to.
irep_idt identifier
The name of the variable which was defined.
Value Set Propagation (flow insensitive)