CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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
12#include <util/pointer_expr.h>
13#include <util/simplify_expr.h>
14
17
19#include "context_abstract_object.h" // IWYU pragma: keep
20
21#include <algorithm>
22#include <numeric>
23
26
32
41
43 const typet &type,
44 bool top,
45 bool bottom)
46 : abstract_pointer_objectt(type, top, bottom)
47{
49 std::make_shared<constant_pointer_abstract_objectt>(type, top, bottom));
50}
51
53 const exprt &expr,
54 const abstract_environmentt &environment,
55 const namespacet &ns)
56 : abstract_pointer_objectt(expr.type(), false, false)
57{
59 std::make_shared<constant_pointer_abstract_objectt>(expr, environment, ns));
60}
61
64 const namespacet &ns) const
65{
66 if(is_top() || is_bottom())
67 {
68 return env.abstract_object_factory(
69 to_pointer_type(type()).base_type(), ns, is_top(), !is_top());
70 }
71
73 for(auto value : values)
74 {
75 auto pointer =
76 std::dynamic_pointer_cast<const abstract_pointer_objectt>(value);
77 results.insert(pointer->read_dereference(env, ns));
78 }
79
80 return results.first();
81}
82
84 abstract_environmentt &environment,
85 const namespacet &ns,
86 const std::stack<exprt> &stack,
87 const abstract_object_pointert &new_value,
88 bool merging_write) const
89{
90 if(is_top() || is_bottom())
91 {
92 environment.havoc("Writing to a 2value pointer");
93 return shared_from_this();
94 }
95
96 for(auto value : values)
97 {
98 auto pointer =
99 std::dynamic_pointer_cast<const abstract_pointer_objectt>(value);
100 pointer->write_dereference(
101 environment, ns, stack, new_value, merging_write);
102 }
103
104 return shared_from_this();
105}
106
108 const typet &new_type,
109 const abstract_environmentt &environment,
110 const namespacet &ns) const
111{
112 INVARIANT(is_void_pointer(type()), "Only allow pointer casting from void*");
114 for(auto value : values)
115 {
116 if(value->is_top()) // multiple mallocs in the same scope can cause spurious
117 continue; // TOP values, which we can safely strip out during the cast
118
119 auto pointer =
120 std::dynamic_pointer_cast<const abstract_pointer_objectt>(value);
121 new_values.insert(pointer->typecast(new_type, environment, ns));
122 }
123 return std::make_shared<value_set_pointer_abstract_objectt>(
125}
126
128 const exprt &expr,
129 const std::vector<abstract_object_pointert> &operands,
130 const abstract_environmentt &environment,
131 const namespacet &ns) const
132{
133 auto rhs =
134 std::dynamic_pointer_cast<const value_set_pointer_abstract_objectt>(
135 operands.back());
136
137 auto differences = std::vector<abstract_object_pointert>{};
138
139 for(auto &lhsv : values)
140 {
141 auto lhsp = std::dynamic_pointer_cast<const abstract_pointer_objectt>(lhsv);
142 for(auto const &rhsp : rhs->values)
143 {
144 auto ops = std::vector<abstract_object_pointert>{lhsp, rhsp};
145 differences.push_back(lhsp->ptr_diff(expr, ops, environment, ns));
146 }
147 }
148
149 return std::accumulate(
150 differences.cbegin(),
151 differences.cend(),
152 differences.front(),
153 [](
154 const abstract_object_pointert &lhs,
155 const abstract_object_pointert &rhs) {
156 return abstract_objectt::merge(lhs, rhs, widen_modet::no).object;
157 });
158}
159
161 const exprt &expr,
162 const std::vector<abstract_object_pointert> &operands,
163 const abstract_environmentt &environment,
164 const namespacet &ns) const
165{
166 auto rhs =
167 std::dynamic_pointer_cast<const value_set_pointer_abstract_objectt>(
168 operands.back());
169
170 auto comparisons = std::set<exprt>{};
171
172 for(auto &lhsv : values)
173 {
174 auto lhsp = std::dynamic_pointer_cast<const abstract_pointer_objectt>(lhsv);
175 for(auto const &rhsp : rhs->values)
176 {
177 auto ops = std::vector<abstract_object_pointert>{lhsp, rhsp};
178 auto comparison = lhsp->ptr_comparison_expr(expr, ops, environment, ns);
179 auto result = simplify_expr(comparison, ns);
180 comparisons.insert(result);
181 }
182 }
183
184 if(comparisons.size() > 1)
185 return nil_exprt();
186 return *comparisons.cbegin();
187}
188
190 const abstract_object_sett &new_values) const
191{
192 PRECONDITION(!new_values.empty());
193
194 if(new_values == values)
195 return shared_from_this();
196
198
199 auto result = std::dynamic_pointer_cast<value_set_pointer_abstract_objectt>(
200 mutable_clone());
201
203 {
204 result->set_top();
205 }
206 else
207 {
208 result->set_values(unwrapped_values);
209 }
210 return result;
211}
212
214 const abstract_object_pointert &other,
215 const widen_modet &widen_mode) const
216{
217 auto cast_other = std::dynamic_pointer_cast<const value_set_tag>(other);
218 if(cast_other)
219 {
220 auto union_values = values;
221 union_values.insert(cast_other->get_values());
223 }
224
225 return abstract_objectt::merge(other, widen_mode);
226}
227
229 const exprt &name) const
230{
231 if(values.size() == 1)
232 return values.first()->to_predicate(name);
233
235 std::transform(
236 values.begin(),
237 values.end(),
238 std::back_inserter(all_predicates),
239 [&name](const abstract_object_pointert &value) {
240 return value->to_predicate(name);
241 });
242 std::sort(all_predicates.begin(), all_predicates.end());
243
244 return or_exprt(all_predicates);
245}
246
254
256 std::ostream &out,
257 const ai_baset &ai,
258 const namespacet &ns) const
259{
260 if(is_top())
261 {
262 out << "TOP";
263 }
264 else if(is_bottom())
265 {
266 out << "BOTTOM";
267 }
268 else
269 {
270 out << "value-set-begin: ";
271
272 values.output(out, ai, ns);
273
274 out << " :value-set-end";
275 }
276}
277
280{
282 for(auto const &value : values)
283 {
285 }
286
287 return unwrapped_values;
288}
289
292{
293 auto const &value_as_set = std::dynamic_pointer_cast<const value_set_tag>(
294 maybe_singleton->unwrap_context());
295 if(value_as_set)
296 {
297 PRECONDITION(value_as_set->get_values().size() == 1);
298 PRECONDITION(!std::dynamic_pointer_cast<const context_abstract_objectt>(
299 value_as_set->get_values().first()));
300
301 return value_as_set->get_values().first();
302 }
303 else
304 return maybe_singleton;
305}
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...
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.
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:117
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
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:3208
Boolean OR.
Definition std_expr.h:2270
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
internal_abstract_object_pointert mutable_clone() const override
exprt to_predicate_internal(const exprt &name) const override
to_predicate implementation - derived classes will override
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
value_set_pointer_abstract_objectt(const typet &new_type, bool top, bool bottom, const abstract_object_sett &new_values)
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.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
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.