cprover
Loading...
Searching...
No Matches
value_set_pointer_abstract_object.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3 Module: analyses variable-sensitivity
4
5 Author: Diffblue Ltd.
6
7\*******************************************************************/
8
11
15#include <numeric>
16#include <util/pointer_expr.h>
17#include <util/simplify_expr.h>
18
20
23
29
31 const typet &type)
33{
34 values.insert(std::make_shared<constant_pointer_abstract_objectt>(type));
35}
36
38 const typet &new_type,
39 bool top,
40 bool bottom,
41 const abstract_object_sett &new_values)
42 : abstract_pointer_objectt(new_type, top, bottom), values(new_values)
43{
44}
45
47 const typet &type,
48 bool top,
49 bool bottom)
50 : abstract_pointer_objectt(type, top, bottom)
51{
53 std::make_shared<constant_pointer_abstract_objectt>(type, top, bottom));
54}
55
57 const exprt &expr,
58 const abstract_environmentt &environment,
59 const namespacet &ns)
60 : abstract_pointer_objectt(expr.type(), false, false)
61{
63 std::make_shared<constant_pointer_abstract_objectt>(expr, environment, ns));
64}
65
67 const abstract_environmentt &env,
68 const namespacet &ns) const
69{
70 if(is_top() || is_bottom())
71 {
72 return env.abstract_object_factory(
73 type().subtype(), ns, is_top(), !is_top());
74 }
75
77 for(auto value : values)
78 {
79 auto pointer =
80 std::dynamic_pointer_cast<const abstract_pointer_objectt>(value);
81 results.insert(pointer->read_dereference(env, ns));
82 }
83
84 return results.first();
85}
86
88 abstract_environmentt &environment,
89 const namespacet &ns,
90 const std::stack<exprt> &stack,
91 const abstract_object_pointert &new_value,
92 bool merging_write) const
93{
94 if(is_top() || is_bottom())
95 {
96 environment.havoc("Writing to a 2value pointer");
97 return shared_from_this();
98 }
99
100 for(auto value : values)
101 {
102 auto pointer =
103 std::dynamic_pointer_cast<const abstract_pointer_objectt>(value);
104 pointer->write_dereference(
105 environment, ns, stack, new_value, merging_write);
106 }
107
108 return shared_from_this();
109}
110
112 const typet &new_type,
113 const abstract_environmentt &environment,
114 const namespacet &ns) const
115{
116 INVARIANT(is_void_pointer(type()), "Only allow pointer casting from void*");
117 abstract_object_sett new_values;
118 for(auto value : values)
119 {
120 if(value->is_top()) // multiple mallocs in the same scope can cause spurious
121 continue; // TOP values, which we can safely strip out during the cast
122
123 auto pointer =
124 std::dynamic_pointer_cast<const abstract_pointer_objectt>(value);
125 new_values.insert(pointer->typecast(new_type, environment, ns));
126 }
127 return std::make_shared<value_set_pointer_abstract_objectt>(
128 new_type, is_top(), is_bottom(), new_values);
129}
130
132 const exprt &expr,
133 const std::vector<abstract_object_pointert> &operands,
134 const abstract_environmentt &environment,
135 const namespacet &ns) const
136{
137 auto rhs =
138 std::dynamic_pointer_cast<const value_set_pointer_abstract_objectt>(
139 operands.back());
140
141 auto differences = std::vector<abstract_object_pointert>{};
142
143 for(auto &lhsv : values)
144 {
145 auto lhsp = std::dynamic_pointer_cast<const abstract_pointer_objectt>(lhsv);
146 for(auto const &rhsp : rhs->values)
147 {
148 auto ops = std::vector<abstract_object_pointert>{lhsp, rhsp};
149 differences.push_back(lhsp->ptr_diff(expr, ops, environment, ns));
150 }
151 }
152
153 return std::accumulate(
154 differences.cbegin(),
155 differences.cend(),
156 differences.front(),
157 [](
158 const abstract_object_pointert &lhs,
159 const abstract_object_pointert &rhs) {
160 return abstract_objectt::merge(lhs, rhs, widen_modet::no).object;
161 });
162}
163
165 const exprt &expr,
166 const std::vector<abstract_object_pointert> &operands,
167 const abstract_environmentt &environment,
168 const namespacet &ns) const
169{
170 auto rhs =
171 std::dynamic_pointer_cast<const value_set_pointer_abstract_objectt>(
172 operands.back());
173
174 auto comparisons = std::set<exprt>{};
175
176 for(auto &lhsv : values)
177 {
178 auto lhsp = std::dynamic_pointer_cast<const abstract_pointer_objectt>(lhsv);
179 for(auto const &rhsp : rhs->values)
180 {
181 auto ops = std::vector<abstract_object_pointert>{lhsp, rhsp};
182 auto comparison = lhsp->ptr_comparison_expr(expr, ops, environment, ns);
183 auto result = simplify_expr(comparison, ns);
184 comparisons.insert(result);
185 }
186 }
187
188 if(comparisons.size() > 1)
189 return nil_exprt();
190 return *comparisons.cbegin();
191}
192
194 const abstract_object_sett &new_values) const
195{
196 PRECONDITION(!new_values.empty());
197
198 if(new_values == values)
199 return shared_from_this();
200
201 auto unwrapped_values = unwrap_and_extract_values(new_values);
202
203 auto result = std::dynamic_pointer_cast<value_set_pointer_abstract_objectt>(
204 mutable_clone());
205
206 if(unwrapped_values.size() > max_value_set_size)
207 {
208 result->set_top();
209 }
210 else
211 {
212 result->set_values(unwrapped_values);
213 }
214 return result;
215}
216
218 const abstract_object_pointert &other,
219 const widen_modet &widen_mode) const
220{
221 auto cast_other = std::dynamic_pointer_cast<const value_set_tag>(other);
222 if(cast_other)
223 {
224 auto union_values = values;
225 union_values.insert(cast_other->get_values());
226 return resolve_values(union_values);
227 }
228
229 return abstract_objectt::merge(other, widen_mode);
230}
231
233 const exprt &name) const
234{
235 if(values.size() == 1)
236 return values.first()->to_predicate(name);
237
238 auto all_predicates = exprt::operandst{};
239 std::transform(
240 values.begin(),
241 values.end(),
242 std::back_inserter(all_predicates),
243 [&name](const abstract_object_pointert &value) {
244 return value->to_predicate(name);
245 });
246 std::sort(all_predicates.begin(), all_predicates.end());
247
248 return or_exprt(all_predicates);
249}
250
252 const abstract_object_sett &other_values)
253{
254 PRECONDITION(!other_values.empty());
255 set_not_top();
256 values = other_values;
257}
258
260 std::ostream &out,
261 const ai_baset &ai,
262 const namespacet &ns) const
263{
264 if(is_top())
265 {
266 out << "TOP";
267 }
268 else if(is_bottom())
269 {
270 out << "BOTTOM";
271 }
272 else
273 {
274 out << "value-set-begin: ";
275
276 values.output(out, ai, ns);
277
278 out << " :value-set-end";
279 }
280}
281
284{
285 abstract_object_sett unwrapped_values;
286 for(auto const &value : values)
287 {
288 unwrapped_values.insert(maybe_extract_single_value(value));
289 }
290
291 return unwrapped_values;
292}
293
296{
297 auto const &value_as_set = std::dynamic_pointer_cast<const value_set_tag>(
298 maybe_singleton->unwrap_context());
299 if(value_as_set)
300 {
301 PRECONDITION(value_as_set->get_values().size() == 1);
302 PRECONDITION(!std::dynamic_pointer_cast<const context_abstract_objectt>(
303 value_as_set->get_values().first()));
304
305 return value_as_set->get_values().first();
306 }
307 else
308 return maybe_singleton;
309}
An abstract version of a program environment.
sharing_ptrt< class abstract_objectt > abstract_object_pointert
virtual void havoc(const std::string &havoc_string)
This should be used as a default case / everything else has failed The string is so that I can easily...
virtual abstract_object_pointert abstract_object_factory(const typet &type, const namespacet &ns, bool top, bool bottom) const
Look at the configuration for the sensitivity and create an appropriate abstract_object.
const_iterator begin() const
value_sett::size_type size() const
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const
void insert(const abstract_object_pointert &o)
abstract_object_pointert first() const
const_iterator end() const
virtual bool is_top() const
Find out if the abstract object is top.
virtual bool is_bottom() const
Find out if the abstract object is bottom.
virtual internal_abstract_object_pointert mutable_clone() const
static combine_result merge(const abstract_object_pointert &op1, const abstract_object_pointert &op2, const locationt &merge_location, const widen_modet &widen_mode)
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The NIL expression.
Definition: std_expr.h:2874
Boolean OR.
Definition: std_expr.h:2082
The type of an expression, extends irept.
Definition: type.h:29
abstract_object_pointert resolve_values(const abstract_object_sett &new_values) const
Update the set of stored values to new_values.
abstract_object_pointert ptr_diff(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
exprt to_predicate_internal(const exprt &name) const override
to_predicate implementation - derived classes will override
CLONE abstract_object_pointert merge(const abstract_object_pointert &other, const widen_modet &widen_mode) const override
static const size_t max_value_set_size
The threshold size for value-sets: past this threshold the object is either converted to interval or ...
void set_values(const abstract_object_sett &other_values)
Setter for updating the stored values.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
abstract_object_pointert read_dereference(const abstract_environmentt &env, const namespacet &ns) const override
A helper function to read elements from an array.
abstract_object_pointert typecast(const typet &new_type, const abstract_environmentt &environment, const namespacet &ns) const override
abstract_object_pointert write_dereference(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const abstract_object_pointert &new_value, bool merging_write) const override
Evaluate writing to a pointer's value.
exprt ptr_comparison_expr(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
An abstraction of a pointer that tracks a single pointer.
General implementation of a an abstract_objectt which can track side information in the form of a 'co...
API to expression classes for Pointers.
bool is_void_pointer(const typet &type)
This method tests, if the given typet is a pointer of type void.
Definition: pointer_expr.h:96
exprt simplify_expr(exprt src, const namespacet &ns)
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
static abstract_object_sett unwrap_and_extract_values(const abstract_object_sett &values)
static abstract_object_pointert maybe_extract_single_value(const abstract_object_pointert &maybe_singleton)
Helper for converting singleton value sets into its only value.
static abstract_object_sett unwrap_and_extract_values(const abstract_object_sett &values)
Value Set of Pointer Abstract Object.