cprover
data_dependency_context.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: analyses variable-sensitivity data_dependency_context
4 
5 Author: Diffblue Ltd
6 
7 \*******************************************************************/
8 
14 #include <algorithm>
15 
17 
29  const abstract_object_pointert before) const
30 {
32  return true;
33 
34  auto cast_before =
35  std::dynamic_pointer_cast<const data_dependency_contextt>(before);
36 
37  if(!cast_before)
38  {
39  // The other context is not something we understand, so must assume
40  // that the abstract_object has been modified
41  return true;
42  }
43 
44  // Check whether the data dependencies have changed as well
46  std::set_intersection(
47  data_deps.cbegin(),
48  data_deps.cend(),
49  cast_before->data_deps.cbegin(),
50  cast_before->data_deps.cend(),
51  std::inserter(intersection, intersection.end()),
52  location_ordert());
53  bool all_matched = intersection.size() == data_deps.size() &&
54  intersection.size() == cast_before->data_deps.size();
55 
56  if(!all_matched)
57  return true;
58 
59  intersection.clear();
60  std::set_intersection(
61  data_dominators.cbegin(),
62  data_dominators.cend(),
63  cast_before->data_dominators.cbegin(),
64  cast_before->data_dominators.cend(),
65  std::inserter(intersection, intersection.end()),
66  location_ordert());
67 
68  all_matched = intersection.size() == data_dominators.size() &&
69  intersection.size() == cast_before->data_dominators.size();
70 
71  return !all_matched;
72 }
73 
83  const dependencest &dependencies) const
84 {
85  // If this is the first write to the context then it is also used as
86  // the initial set of data dependency dominators as well.
87  const bool first_write = data_deps.empty();
88  dependencest new_dependencies;
89 
90  // Workout what new data dependencies need to be inserted
91  if(first_write)
92  {
93  new_dependencies = dependencies;
94  }
95  else
96  {
97  std::set_difference(
98  dependencies.begin(),
99  dependencies.end(),
100  data_deps.begin(),
101  data_deps.end(),
102  std::inserter(new_dependencies, new_dependencies.begin()),
103  location_ordert{});
104  }
105 
106  // If there are no new dependencies to add, just return
107  if(new_dependencies.empty())
108  return shared_from_this();
109 
110  const auto &result =
111  std::dynamic_pointer_cast<data_dependency_contextt>(mutable_clone());
112 
113  for(auto l : new_dependencies)
114  {
115  result->data_deps.insert(l);
116  }
117 
118  if(first_write)
119  {
120  // If this was the first insertion of any dependencies, then these
121  // data dependencies are also data dominators as well
122  for(auto l : new_dependencies)
123  {
124  result->data_dominators.insert(l);
125  }
126  }
127  return result;
128 }
129 
140 {
141  // If the dependencies will not change, just return 'this'
143 
144  std::set_intersection(
145  data_deps.cbegin(),
146  data_deps.cend(),
147  dependencies.cbegin(),
148  dependencies.cend(),
149  std::inserter(intersection, intersection.end()),
150  location_ordert());
151  if(
152  intersection.size() == data_deps.size() &&
153  intersection.size() == dependencies.size())
154  return shared_from_this();
155 
156  const auto &result =
157  std::dynamic_pointer_cast<data_dependency_contextt>(mutable_clone());
158 
159  result->data_deps = dependencies;
160 
161  // If this is the first write to the context then it is also used as
162  // the initial set of data dependency dominators as well.
163  if(data_deps.empty())
164  {
165  result->data_dominators = dependencies;
166  }
167  return result;
168 }
169 
187  abstract_environmentt &environment,
188  const namespacet &ns,
189  const std::stack<exprt> &stack,
190  const exprt &specifier,
191  const abstract_object_pointert &value,
192  bool merging_write) const
193 {
194  const auto updated_parent =
195  std::dynamic_pointer_cast<const data_dependency_contextt>(
197  environment, ns, stack, specifier, value, merging_write));
198 
199  const auto cast_value =
200  std::dynamic_pointer_cast<const data_dependency_contextt>(value);
201 
202  return updated_parent->set_data_deps(cast_value->data_deps);
203 }
204 
217  const abstract_objectt::locationst &locations,
218  const bool update_sub_elements) const
219 {
220  const auto updated_parent =
221  std::dynamic_pointer_cast<const data_dependency_contextt>(
223  locations, update_sub_elements));
224 
225  return updated_parent->set_data_deps(locations);
226 }
227 
239 {
240  auto cast_other =
241  std::dynamic_pointer_cast<const data_dependency_contextt>(other);
242 
243  if(cast_other)
244  {
245  const auto merged_parent =
246  std::dynamic_pointer_cast<const data_dependency_contextt>(
247  this->write_location_contextt::merge(other));
248 
249  const auto updated_parent =
250  std::dynamic_pointer_cast<const data_dependency_contextt>(
251  merged_parent->insert_data_deps(cast_other->data_deps));
252 
253  const auto &result = std::dynamic_pointer_cast<data_dependency_contextt>(
254  updated_parent->mutable_clone());
255 
256  // On a merge, data_dominators are the intersection of this object and the
257  // other object. In other words, the dominators at this merge point are
258  // those dominators that exist in all possible execution paths to this
259  // merge point.
260  result->data_dominators.clear();
261  std::set_intersection(
262  data_dominators.begin(),
263  data_dominators.end(),
264  cast_other->data_dominators.begin(),
265  cast_other->data_dominators.end(),
266  std::inserter(result->data_dominators, result->data_dominators.end()),
267  location_ordert());
268 
269  // It is critically important that we only return a newly constructed result
270  // abstract object *iff* the data has actually changed, otherwise AI may
271  // never reach a fixpoint
272  if(has_been_modified(result))
273  return result;
274  else
275  return shared_from_this();
276  }
277 
278  return abstract_objectt::merge(other);
279 }
280 
296  const abstract_object_pointert other) const
297 {
298  auto other_context =
299  std::dynamic_pointer_cast<const data_dependency_contextt>(other);
300 
301  if(other_context)
302  {
303  const auto merged_parent =
304  std::dynamic_pointer_cast<const data_dependency_contextt>(
306 
307  return merged_parent->insert_data_deps(other_context->data_deps);
308  }
309  return shared_from_this();
310 }
311 
317 std::set<goto_programt::const_targett>
319 {
320  std::set<goto_programt::const_targett> result;
321  for(const auto &d : data_deps)
322  result.insert(d);
323  return result;
324 }
325 
331 std::set<goto_programt::const_targett>
333 {
334  std::set<goto_programt::const_targett> result;
335  for(const auto &d : data_dominators)
336  result.insert(d);
337  return result;
338 }
339 
341  std::ostream &out,
342  const class ai_baset &ai,
343  const namespacet &ns) const
344 {
345  this->write_location_contextt::output(out, ai, ns);
346 
347  out << "[Data dependencies: ";
348 
349  bool comma = false;
350  for(auto d : data_deps)
351  {
352  out << (comma ? ", " : "") << d->location_number;
353  comma = true;
354  }
355  out << ']';
356 
357  out << "[Data dominators: ";
358 
359  comma = false;
360  for(auto d : data_dominators)
361  {
362  out << (comma ? ", " : "") << d->location_number;
363  comma = true;
364  }
365  out << ']';
366 }
data_dependency_contextt::output
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.
Definition: data_dependency_context.cpp:340
data_dependency_contextt::update_location_context
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...
Definition: data_dependency_context.cpp:216
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:75
abstract_objectt::merge
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.
Definition: abstract_object.cpp:189
data_dependency_contextt::write
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.
Definition: data_dependency_context.cpp:186
data_dependency_contextt::get_data_dependencies
std::set< goto_programt::const_targett > get_data_dependencies() const
Return the set of data dependencies associated with this node.
Definition: data_dependency_context.cpp:318
abstract_environmentt
Definition: abstract_environment.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
data_dependency_contextt::location_ordert
Definition: data_dependency_context.h:80
write_location_contextt::has_been_modified
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...
Definition: write_location_context.cpp:246
write_location_contextt::output
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.
Definition: write_location_context.cpp:207
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
intersection
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.
Definition: graph.h:115
data_dependency_contextt::merge
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...
Definition: data_dependency_context.cpp:238
abstract_objectt::locationst
std::set< goto_programt::const_targett > locationst
Definition: abstract_object.h:215
write_location_contextt::update_location_context
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...
Definition: write_location_context.cpp:27
write_location_contextt::write
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.
Definition: write_location_context.cpp:69
data_dependency_context.h
Maintain data dependencies as a context in the variable sensitivity domain.
data_dependency_contextt::dependencest
std::set< goto_programt::const_targett, location_ordert > dependencest
Definition: data_dependency_context.h:89
data_dependency_contextt::get_data_dominators
std::set< goto_programt::const_targett > get_data_dominators() const
Return the set of data dominators associated with this node.
Definition: data_dependency_context.cpp:332
write_location_contextt::merge
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...
Definition: write_location_context.cpp:113
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
data_dependency_contextt::has_been_modified
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...
Definition: data_dependency_context.cpp:28
data_dependency_contextt::insert_data_deps
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...
Definition: data_dependency_context.cpp:82
data_dependency_contextt::abstract_object_merge_internal
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...
Definition: data_dependency_context.cpp:295
data_dependency_contextt::set_data_deps
abstract_object_pointert set_data_deps(const dependencest &dependencies) const
Set the given set of data dependencies for this data_dependency_context object.
Definition: data_dependency_context.cpp:139
abstract_objectt::mutable_clone
virtual internal_abstract_object_pointert mutable_clone() const
Definition: abstract_object.h:404
data_dependency_contextt::data_deps
dependencest data_deps
Definition: data_dependency_context.h:90
data_dependency_contextt::data_dominators
dependencest data_dominators
Definition: data_dependency_context.h:91
write_location_contextt::abstract_object_merge_internal
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...
Definition: write_location_context.cpp:167