CBMC: /home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/write_location_context.cpp Source File

CBMC
Loading...
Searching...
No Matches
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 "write_location_context.h"
10
11#include <algorithm>
12
13context_abstract_objectt::locationst
18
36 abstract_environmentt &environment,
37 const namespacet &ns,
38 const std::stack<exprt> &stack,
39 const exprt &specifier,
40 const abstract_object_pointert &value,
41 bool merging_write) const
42{
44 environment, ns, stack, specifier, value, merging_write);
45
46 // Only perform an update if the write to the child has in fact changed it...
48 return shared_from_this();
49
50 // Need to ensure the result of the write is still wrapped in a dependency
51 // context
52 const auto &result =
53 std::dynamic_pointer_cast<write_location_contextt>(mutable_clone());
54
55 // Update the child and record the updated write locations
56 result->set_child(updated_child);
57 auto value_context =
58 std::dynamic_pointer_cast<const write_location_contextt>(value);
59
61 {
62 result->set_last_written_locations(
63 value_context->get_last_written_locations());
64 }
65
66 return result;
67}
68
80 const abstract_object_pointert &other,
81 const widen_modet &widen_mode) const
82{
83 auto cast_other =
84 std::dynamic_pointer_cast<const write_location_contextt>(other);
85
86 if(cast_other)
87 {
88 auto merge_fn = [&widen_mode](
89 const abstract_object_pointert &op1,
90 const abstract_object_pointert &op2) {
91 return abstract_objectt::merge(op1, op2, widen_mode);
92 };
94 }
95
97}
98
99// need wrapper function here to disambiguate meet overload
101 const abstract_object_pointert &op1,
102 const abstract_object_pointert &op2)
103{
104 return abstract_objectt::meet(op1, op2);
105}
106
107abstract_object_pointert
109{
110 auto cast_other =
111 std::dynamic_pointer_cast<const write_location_contextt>(other);
112
113 if(cast_other)
115
116 return abstract_objectt::meet(other);
117}
118
120 const write_location_context_ptrt &other,
121 combine_fn fn) const
122{
123 auto combined_child = fn(child_abstract_object, other->child_abstract_object);
124
125 auto location_union = get_location_union(other->get_last_written_locations());
126 // If the union is larger than the initial set, then update.
127 bool merge_locations =
129
130 if(combined_child.modified || merge_locations)
131 {
132 const auto &result =
133 std::dynamic_pointer_cast<write_location_contextt>(mutable_clone());
134 if(combined_child.modified)
135 {
136 result->set_child(combined_child.object);
137 }
139 {
140 result->set_last_written_locations(location_union);
141 }
142
143 return result;
144 }
145
146 return shared_from_this();
147}
148
162abstract_object_pointert
164 const abstract_object_pointert &other) const
165{
166 auto other_context =
167 std::dynamic_pointer_cast<const write_location_contextt>(other);
168
169 if(other_context)
170 {
171 auto location_union =
172 get_location_union(other_context->get_last_written_locations());
173
174 // If the union is larger than the initial set, then update.
175 if(location_union.size() > get_last_written_locations().size())
176 {
177 auto result =
178 std::dynamic_pointer_cast<write_location_contextt>(mutable_clone());
179 return result->update_location_context_internal(location_union);
180 }
181 }
182 return shared_from_this();
183}
184
185context_abstract_objectt::context_abstract_object_ptrt
187 const locationst &locations) const
188{
189 auto result =
190 std::dynamic_pointer_cast<write_location_contextt>(mutable_clone());
191 result->set_last_written_locations(locations);
192 return result;
193}
194
205
215 std::ostream &out,
216 const ai_baset &ai,
217 const namespacet &ns) const
218{
220
221 // Output last written locations immediately following the child output
222 out << " @ ";
224}
225
234context_abstract_objectt::locationst
242
254 const abstract_object_pointert &before) const
255{
256 if(this == before.get())
257 {
258 // copy-on-write means pointer equality implies no modifications
259 return false;
260 }
261
262 auto before_context =
263 std::dynamic_pointer_cast<const write_location_contextt>(before);
264
265 if(!before_context)
266 {
267 // The other context is not something we understand, so must assume
268 // that the abstract_object has been modified
269 return true;
270 }
271
272 // Even if the pointers are different, it maybe that it has changed only
273 // because of a merge operation, rather than an actual write. Given that
274 // this class has knowledge of where writes have occured, use that
275 // information to determine if any writes have happened and use that as the
276 // proxy for whether the value has changed or not.
277 //
278 // For two sets of last written locations to match,
279 // each location in one set must be equal to precisely one location
280 // in the other, since a set can assume at most one match
282 before_context->get_last_written_locations();
284
285 class location_ordert
286 {
287 public:
288 bool operator()(
291{
292 return instruction->location_number > other_instruction->location_number;
293 }
294 };
295
296 typedef std::set<goto_programt::const_targett, location_ordert>
298
300 for(const auto &entry : first_write_locations)
301 {
302 lhs_location.insert(entry);
303 }
304
306 for(const auto &entry : second_write_locations)
307 {
308 rhs_location.insert(entry);
309 }
310
312 std::set_intersection(
313 lhs_location.cbegin(),
314 lhs_location.cend(),
315 rhs_location.cbegin(),
316 rhs_location.cend(),
317 std::inserter(intersection, intersection.end()),
318 location_ordert());
319 bool all_matched = intersection.size() == first_write_locations.size() &&
320 intersection.size() == second_write_locations.size();
321
322 return !all_matched;
323}
324
332 std::ostream &out,
333 const locationst &locations)
334{
335 out << "[";
336 bool comma = false;
337
338 std::set<unsigned> sorted_locations;
339 for(auto location : locations)
340 {
341 sorted_locations.insert(location->location_number);
342 }
343
344 for(auto location_number : sorted_locations)
345 {
346 if(!comma)
347 {
348 out << location_number;
349 comma = true;
350 }
351 else
352 {
353 out << ", " << location_number;
354 }
355 }
356 out << "]";
357}
widen_modet
sharing_ptrt< class abstract_objectt > abstract_object_pointert
static combine_result merge(const abstract_object_pointert &op1, const abstract_object_pointert &op2, const locationt &merge_location, const widen_modet &widen_mode)
static combine_result meet(const abstract_object_pointert &op1, const abstract_object_pointert &op2)
Interface method for the meet operation.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition ai.h:117
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
std::shared_ptr< context_abstract_objectt > context_abstract_object_ptrt
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 child_abstract_object
std::set< locationt, goto_programt::target_less_than > locationst
Base class for all expressions.
Definition expr.h:57
instructionst::const_iterator const_targett
Definition goto_program.h:614
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
abstract_object_pointert merge(const abstract_object_pointert &other, const widen_modet &widen_mode) const override
Create a new abstract object that is the result of merging this abstract object with a given abstract...
std::function< abstract_objectt::combine_result(const abstract_object_pointert &op1, const abstract_object_pointert &op2)> combine_fn
internal_abstract_object_pointert mutable_clone() const override
virtual locationst get_last_written_locations() const
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...
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 last_written_locations
abstract_object_pointert meet(const abstract_object_pointert &other) const override
Base implementation of the meet operation: only used if no more precise abstraction can be used,...
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.
static void output_last_written_locations(std::ostream &out, const locationst &locations)
Internal helper function to format and output a given set of locations.
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...
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.
void set_last_written_locations(const locationst &locations)
Sets the last written locations for this context.
std::shared_ptr< const write_location_contextt > write_location_context_ptrt
context_abstract_object_ptrt update_location_context_internal(const locationst &locations) const override
abstract_object_pointert combine(const write_location_context_ptrt &other, combine_fn fn) const
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
Clones the first parameter and merges it with the second.
static abstract_objectt::combine_result object_meet(const abstract_object_pointert &op1, const abstract_object_pointert &op2)
Maintain a context in the variable sensitvity domain that records write locations for a given abstrac...

AltStyle によって変換されたページ (->オリジナル) /