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

CBMC
Loading...
Searching...
No Matches
data_dependency_context.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: analyses variable-sensitivity data_dependency_context
4
5Author: Diffblue Ltd
6
7\*******************************************************************/
8
14#include <algorithm>
15
16#include "data_dependency_context.h"
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()),
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
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()),
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 dependenciest &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();
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()),
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
130context_abstract_objectt::context_abstract_object_ptrt
132 const locationst &locations) const
133{
134 auto result =
135 std::dynamic_pointer_cast<data_dependency_contextt>(mutable_clone());
136 result->set_last_written_locations(locations);
137 result->set_data_deps(locations);
138 return result;
139}
140
147{
148 // `locationst` is unsorted, so convert this to a sorted `dependenciest`
149 dependenciest dependencies(locations.begin(), locations.end());
150 set_data_deps(dependencies);
151}
152
160{
162 std::set_intersection(
163 data_deps.cbegin(),
164 data_deps.cend(),
165 dependencies.cbegin(),
166 dependencies.cend(),
167 std::inserter(intersection, intersection.end()),
169
170 // If this is the first write to the context then it is also used as
171 // the initial set of data dependency dominators as well.
172 if(data_deps.empty())
173 data_dominators = dependencies;
174
175 data_deps = dependencies;
176}
177
195 abstract_environmentt &environment,
196 const namespacet &ns,
197 const std::stack<exprt> &stack,
198 const exprt &specifier,
199 const abstract_object_pointert &value,
200 bool merging_write) const
201{
202 auto updated_parent =
203 std::dynamic_pointer_cast<data_dependency_contextt>(mutable_clone());
204 const auto cast_value =
205 std::dynamic_pointer_cast<const data_dependency_contextt>(value);
206
207 updated_parent->set_data_deps(cast_value->data_deps);
208
209 return updated_parent->write_location_contextt::write(
210 environment, ns, stack, specifier, value, merging_write);
211}
212
224 const abstract_object_pointert &other,
225 const widen_modet &widen_mode) const
226{
227 auto cast_other =
228 std::dynamic_pointer_cast<const data_dependency_contextt>(other);
229
230 if(cast_other)
231 {
232 const auto merged_parent =
233 std::dynamic_pointer_cast<const data_dependency_contextt>(
235
237 }
238
239 return abstract_objectt::merge(other, widen_mode);
240}
241
242abstract_object_pointert
244{
245 auto cast_other =
246 std::dynamic_pointer_cast<const data_dependency_contextt>(other);
247
248 if(cast_other)
249 {
250 const auto meet_parent =
251 std::dynamic_pointer_cast<const data_dependency_contextt>(
252 this->write_location_contextt::meet(other));
253
255 }
256
257 return abstract_objectt::meet(other);
258}
259
261 const data_dependency_context_ptrt &other,
262 const data_dependency_context_ptrt &parent) const
263{
264 const auto updated_parent =
265 std::dynamic_pointer_cast<const data_dependency_contextt>(
266 parent->insert_data_deps(other->data_deps));
267
268 const auto &result = std::dynamic_pointer_cast<data_dependency_contextt>(
269 updated_parent->mutable_clone());
270
271 // On a merge, data_dominators are the intersection of this object and the
272 // other object. In other words, the dominators at this merge point are
273 // those dominators that exist in all possible execution paths to this
274 // merge point.
275 result->data_dominators.clear();
276 std::set_intersection(
277 data_dominators.begin(),
278 data_dominators.end(),
279 other->data_dominators.begin(),
280 other->data_dominators.end(),
281 std::inserter(result->data_dominators, result->data_dominators.end()),
283
284 // It is critically important that we only return a newly constructed result
285 // abstract object *iff* the data has actually changed, otherwise AI may
286 // never reach a fixpoint
287 bool value_change = get_child() != result->get_child();
288 if(value_change || has_been_modified(result))
289 return result;
290 else
291 return shared_from_this();
292}
293
307abstract_object_pointert
309 const abstract_object_pointert &other) const
310{
311 auto other_context =
312 std::dynamic_pointer_cast<const data_dependency_contextt>(other);
313
314 if(other_context)
315 {
316 const auto merged_parent =
317 std::dynamic_pointer_cast<const data_dependency_contextt>(
319
320 return merged_parent->insert_data_deps(other_context->data_deps);
321 }
322 return shared_from_this();
323}
324
330std::set<goto_programt::const_targett, goto_programt::target_less_than>
332{
333 std::set<goto_programt::const_targett, goto_programt::target_less_than>
334 result;
335 for(const auto &d : data_deps)
336 result.insert(d);
337 return result;
338}
339
345std::set<goto_programt::const_targett, goto_programt::target_less_than>
347{
348 std::set<goto_programt::const_targett, goto_programt::target_less_than>
349 result;
350 for(const auto &d : data_dominators)
351 result.insert(d);
352 return result;
353}
354
356 std::ostream &out,
357 const class ai_baset &ai,
358 const namespacet &ns) const
359{
360 this->write_location_contextt::output(out, ai, ns);
361
362 out << "[Data dependencies: ";
363
364 bool comma = false;
365 for(auto d : data_deps)
366 {
367 out << (comma ? ", " : "") << d->location_number;
368 comma = true;
369 }
370 out << ']';
371
372 out << "[Data dominators: ";
373
374 comma = false;
375 for(auto d : data_dominators)
376 {
377 out << (comma ? ", " : "") << d->location_number;
378 comma = true;
379 }
380 out << ']';
381}
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
virtual void clear()
Reset the abstract state.
Definition ai.h:269
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
std::set< locationt, goto_programt::target_less_than > locationst
abstract_object_pointert get_child() const
std::set< goto_programt::const_targett, goto_programt::target_less_than > get_data_dominators() const
Return the set of data dominators associated with this node.
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...
internal_abstract_object_pointert mutable_clone() const override
dependenciest data_deps
dependenciest data_dominators
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 insert_data_deps(const dependenciest &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, goto_programt::target_less_than > get_data_dependencies() const
Return the set of data dependencies associated with this node.
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::shared_ptr< const data_dependency_contextt > data_dependency_context_ptrt
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.
context_abstract_object_ptrt update_location_context_internal(const locationst &locations) const override
abstract_object_pointert combine(const data_dependency_context_ptrt &other, const data_dependency_context_ptrt &parent) const
void set_data_deps(const locationst &locations)
Set the given set of data dependencies for from the 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,...
std::set< goto_programt::const_targett, location_ordert > dependenciest
Base class for all expressions.
Definition expr.h:57
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...
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.
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,...
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.
Definition graph.h:115

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