35 std::dynamic_pointer_cast<const data_dependency_contextt>(before);
46 std::set_intersection(
49 cast_before->data_deps.cbegin(),
50 cast_before->data_deps.cend(),
60 std::set_intersection(
63 cast_before->data_dominators.cbegin(),
64 cast_before->data_dominators.cend(),
69 intersection.size() == cast_before->data_dominators.size();
87 const bool first_write =
data_deps.empty();
93 new_dependencies = dependencies;
102 std::inserter(new_dependencies, new_dependencies.begin()),
107 if(new_dependencies.empty())
108 return shared_from_this();
111 std::dynamic_pointer_cast<data_dependency_contextt>(
mutable_clone());
113 for(
auto l : new_dependencies)
115 result->data_deps.insert(l);
122 for(
auto l : new_dependencies)
124 result->data_dominators.insert(l);
144 std::set_intersection(
147 dependencies.cbegin(),
154 return shared_from_this();
157 std::dynamic_pointer_cast<data_dependency_contextt>(
mutable_clone());
159 result->data_deps = dependencies;
165 result->data_dominators = dependencies;
189 const std::stack<exprt> &stack,
190 const exprt &specifier,
192 bool merging_write)
const
194 const auto updated_parent =
195 std::dynamic_pointer_cast<const data_dependency_contextt>(
197 environment, ns, stack, specifier, value, merging_write));
199 const auto cast_value =
200 std::dynamic_pointer_cast<const data_dependency_contextt>(value);
202 return updated_parent->set_data_deps(cast_value->data_deps);
218 const bool update_sub_elements)
const
220 const auto updated_parent =
221 std::dynamic_pointer_cast<const data_dependency_contextt>(
223 locations, update_sub_elements));
225 return updated_parent->set_data_deps(locations);
241 std::dynamic_pointer_cast<const data_dependency_contextt>(other);
245 const auto merged_parent =
246 std::dynamic_pointer_cast<const data_dependency_contextt>(
249 const auto updated_parent =
250 std::dynamic_pointer_cast<const data_dependency_contextt>(
251 merged_parent->insert_data_deps(cast_other->data_deps));
253 const auto &result = std::dynamic_pointer_cast<data_dependency_contextt>(
254 updated_parent->mutable_clone());
260 result->data_dominators.clear();
261 std::set_intersection(
264 cast_other->data_dominators.begin(),
265 cast_other->data_dominators.end(),
266 std::inserter(result->data_dominators, result->data_dominators.end()),
275 return shared_from_this();
299 std::dynamic_pointer_cast<const data_dependency_contextt>(other);
303 const auto merged_parent =
304 std::dynamic_pointer_cast<const data_dependency_contextt>(
307 return merged_parent->insert_data_deps(other_context->data_deps);
309 return shared_from_this();
317 std::set<goto_programt::const_targett>
320 std::set<goto_programt::const_targett> result;
331 std::set<goto_programt::const_targett>
334 std::set<goto_programt::const_targett> result;
347 out <<
"[Data dependencies: ";
352 out << (comma ?
", " :
"") << d->location_number;
357 out <<
"[Data dominators: ";
362 out << (comma ?
", " :
"") << d->location_number;
sharing_ptrt< class abstract_objectt > abstract_object_pointert
virtual internal_abstract_object_pointert mutable_clone() const
static abstract_object_pointert merge(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Clones the first parameter and merges it with the second.
std::set< goto_programt::const_targett > locationst
This is the basic interface of the abstract interpreter with default implementations of the core func...
std::set< goto_programt::const_targett > get_data_dominators() const
Return the set of data dominators associated with this node.
CLONE abstract_object_pointert merge(abstract_object_pointert other) const override
Create a new abstract object that is the result of merging this abstract object with a given abstract...
abstract_object_pointert set_data_deps(const dependencest &dependencies) const
Set the given set of data dependencies for this data_dependency_context object.
abstract_object_pointert update_location_context(const abstract_objectt::locationst &locations, const bool update_sub_elements) const override
Update the location context for an abstract object, potentially propogating the update to any childre...
abstract_object_pointert insert_data_deps(const dependencest &dependencies) const
Insert the given set of data dependencies into the data dependencies set for this data_dependency_con...
std::set< goto_programt::const_targett > get_data_dependencies() const
Return the set of data dependencies associated with this node.
bool has_been_modified(const abstract_object_pointert before) const override
Determine whether 'this' abstract_object has been modified in comparison to a previous 'before' state...
void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const override
Output a representation of the value of this abstract object.
abstract_object_pointert write(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &specifier, const abstract_object_pointert &value, bool merging_write) const override
A helper function to evaluate writing to a component of an abstract object.
abstract_object_pointert abstract_object_merge_internal(const abstract_object_pointert other) const override
Helper function for abstract_objectt::abstract_object_merge to perform any additional actions after t...
std::set< goto_programt::const_targett, location_ordert > dependencest
dependencest data_dominators
Base class for all expressions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
CLONE abstract_object_pointert merge(abstract_object_pointert other) const override
Create a new abstract object that is the result of merging this abstract object with a given abstract...
abstract_object_pointert update_location_context(const abstract_objectt::locationst &locations, const bool update_sub_elements) const override
Update the location context for an abstract object, potentially propagating the update to any childre...
void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const override
Output a representation of the value of this abstract object.
abstract_object_pointert write(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &specifier, const abstract_object_pointert &value, bool merging_write) const override
A helper function to evaluate writing to a component of an abstract object.
abstract_object_pointert abstract_object_merge_internal(const abstract_object_pointert other) const override
Helper function for abstract_objectt::abstract_object_merge to perform any additional actions after t...
bool has_been_modified(const abstract_object_pointert before) const override
Determine whether 'this' abstract_object has been modified in comparison to a previous 'before' state...
Maintain data dependencies as a context in the variable sensitivity domain.
void intersection(const typename graph_nodet< E >::edgest &a, const typename graph_nodet< E >::edgest &b, typename graph_nodet< E >::edgest &dest)
Compute intersection of two edge sets, in linear time.