cprover
write_location_context.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity write_location_context
4 
5  Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
9 #include <ostream>
10 
12 #include <util/std_types.h>
13 
14 #include "write_location_context.h"
15 
28  const abstract_objectt::locationst &locations,
29  const bool update_sub_elements) const
30 {
31  const auto &result =
32  std::dynamic_pointer_cast<write_location_contextt>(mutable_clone());
33 
34  if(update_sub_elements)
35  {
36  abstract_object_pointert visited_child =
38  ->update_location_context(locations, update_sub_elements)
39  ->visit_sub_elements(location_update_visitort(locations));
40  result->set_child(visited_child);
41  }
42 
43  result->set_last_written_locations(locations);
44  return result;
45 }
46 
49 {
51 }
52 
70  abstract_environmentt &environment,
71  const namespacet &ns,
72  const std::stack<exprt> &stack,
73  const exprt &specifier,
74  const abstract_object_pointert &value,
75  bool merging_write) const
76 {
77  abstract_object_pointert updated_child = child_abstract_object->write(
78  environment, ns, stack, specifier, value, merging_write);
79 
80  // Only perform an update if the write to the child has in fact changed it...
81  if(updated_child == child_abstract_object)
82  return shared_from_this();
83 
84  // Need to ensure the result of the write is still wrapped in a dependency
85  // context
86  const auto &result =
87  std::dynamic_pointer_cast<write_location_contextt>(mutable_clone());
88 
89  // Update the child and record the updated write locations
90  result->set_child(updated_child);
91  auto value_context =
92  std::dynamic_pointer_cast<const write_location_contextt>(value);
93 
94  if(value_context)
95  {
96  result->set_last_written_locations(
97  value_context->get_last_written_locations());
98  }
99 
100  return result;
101 }
102 
114 {
115  auto cast_other =
116  std::dynamic_pointer_cast<const write_location_contextt>(other);
117 
118  if(cast_other)
119  {
120  bool child_modified = false;
121 
122  auto merged_child = abstract_objectt::merge(
123  child_abstract_object, cast_other->child_abstract_object, child_modified);
124 
125  abstract_objectt::locationst location_union =
126  get_location_union(cast_other->get_last_written_locations());
127  // If the union is larger than the initial set, then update.
128  bool merge_locations =
129  location_union.size() > get_last_written_locations().size();
130 
131  if(child_modified || merge_locations)
132  {
133  const auto &result =
134  std::dynamic_pointer_cast<write_location_contextt>(mutable_clone());
135  if(child_modified)
136  {
137  result->set_child(merged_child);
138  }
139  if(merge_locations)
140  {
141  result->set_last_written_locations(location_union);
142  }
143 
144  return result;
145  }
146 
147  return shared_from_this();
148  }
149 
150  return abstract_objectt::merge(other);
151 }
152 
168  const abstract_object_pointert other) const
169 {
170  auto other_context =
171  std::dynamic_pointer_cast<const write_location_contextt>(other);
172 
173  if(other_context)
174  {
175  abstract_objectt::locationst location_union =
176  get_location_union(other_context->get_last_written_locations());
177 
178  // If the union is larger than the initial set, then update.
179  if(location_union.size() > get_last_written_locations().size())
180  {
182  return result->update_location_context(location_union, false);
183  }
184  }
185  return shared_from_this();
186 }
187 
194  const abstract_objectt::locationst &locations)
195 {
196  last_written_locations = locations;
197 }
198 
208  std::ostream &out,
209  const ai_baset &ai,
210  const namespacet &ns) const
211 {
213 
214  // Output last written locations immediately following the child output
215  out << " @ ";
217 }
218 
229 {
230  locationst existing_locations = get_last_written_locations();
231  existing_locations.insert(locations.begin(), locations.end());
232 
233  return existing_locations;
234 }
235 
247  const abstract_object_pointert before) const
248 {
249  if(this == before.get())
250  {
251  // copy-on-write means pointer equality implies no modifications
252  return false;
253  }
254 
255  auto before_context =
256  std::dynamic_pointer_cast<const write_location_contextt>(before);
257 
258  if(!before_context)
259  {
260  // The other context is not something we understand, so must assume
261  // that the abstract_object has been modified
262  return true;
263  }
264 
265  // Even if the pointers are different, it maybe that it has changed only
266  // because of a merge operation, rather than an actual write. Given that
267  // this class has knowledge of where writes have occured, use that
268  // information to determine if any writes have happened and use that as the
269  // proxy for whether the value has changed or not.
270  //
271  // For two sets of last written locations to match,
272  // each location in one set must be equal to precisely one location
273  // in the other, since a set can assume at most one match
274  const abstract_objectt::locationst &first_write_locations =
275  before_context->get_last_written_locations();
276  const abstract_objectt::locationst &second_write_locations =
278 
279  class location_ordert
280  {
281  public:
282  bool operator()(
283  goto_programt::const_targett instruction,
284  goto_programt::const_targett other_instruction) const
285  {
286  return instruction->location_number > other_instruction->location_number;
287  }
288  };
289 
290  typedef std::set<goto_programt::const_targett, location_ordert>
291  sorted_locationst;
292 
293  sorted_locationst lhs_location;
294  for(const auto &entry : first_write_locations)
295  {
296  lhs_location.insert(entry);
297  }
298 
299  sorted_locationst rhs_location;
300  for(const auto &entry : second_write_locations)
301  {
302  rhs_location.insert(entry);
303  }
304 
306  std::set_intersection(
307  lhs_location.cbegin(),
308  lhs_location.cend(),
309  rhs_location.cbegin(),
310  rhs_location.cend(),
311  std::inserter(intersection, intersection.end()),
312  location_ordert());
313  bool all_matched = intersection.size() == first_write_locations.size() &&
314  intersection.size() == second_write_locations.size();
315 
316  return !all_matched;
317 }
318 
326  std::ostream &out,
327  const abstract_objectt::locationst &locations)
328 {
329  out << "[";
330  bool comma = false;
331 
332  std::set<unsigned> sorted_locations;
333  for(auto location : locations)
334  {
335  sorted_locations.insert(location->location_number);
336  }
337 
338  for(auto location_number : sorted_locations)
339  {
340  if(!comma)
341  {
342  out << location_number;
343  comma = true;
344  }
345  else
346  {
347  out << ", " << location_number;
348  }
349  }
350  out << "]";
351 }
An abstract version of a program environment.
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...
Definition: ai.h:120
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.
CLONE abstract_object_pointert child_abstract_object
Base class for all expressions.
Definition: expr.h:54
instructionst::const_iterator const_targett
Definition: goto_program.h:551
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
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...
abstract_objectt::locationst last_written_locations
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.
locationst get_location_union(const locationst &locations) const
Construct the union of the location set of the current object, and a the provided location set.
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.
virtual abstract_objectt::locationst get_last_written_locations() const
void set_last_written_locations(const abstract_objectt::locationst &locations)
Sets the last written locations for this context.
static void output_last_written_locations(std::ostream &out, const abstract_objectt::locationst &locations)
Internal helper function to format and output a given set of locations.
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...
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
Pre-defined types.
Maintain a context in the variable sensitvity domain that records write locations for a given abstrac...