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.
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.