cprover
full_array_abstract_object.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3 Module: Variable Sensitivity
4
5 Author: Thomas Kiley, thomas.kiley@diffblue.com
6
7\*******************************************************************/
8
9#include <ostream>
10
13#include <util/arith_tools.h>
15#include <util/std_expr.h>
16
20#include "map_visit.h"
21
23{
24 bool is_good;
26 bool overrun;
27};
28
30 const exprt &expr,
31 const abstract_environmentt &env,
32 const namespacet &ns);
34 const mp_integer &index,
35 const abstract_environmentt &env,
36 const namespacet &ns);
37
38template <typename index_fn>
40 const abstract_environmentt &environment,
41 const exprt &expr,
42 const namespacet &ns,
43 index_fn &fn)
44{
45 const index_exprt &index_expr = to_index_expr(expr);
46 auto evaluated_index = environment.eval(index_expr.index(), ns);
47 auto index_range = (std::dynamic_pointer_cast<const abstract_value_objectt>(
48 evaluated_index->unwrap_context()))
49 ->index_range(ns);
50
51 sharing_ptrt<abstract_objectt> result = nullptr;
52 for(const auto &index : index_range)
53 {
54 auto at_index = fn(index_exprt(index_expr.array(), index));
55
56 result =
57 (result == nullptr)
58 ? at_index
60
61 if(result->is_top()) // no point in continuing once we've gone top
62 break;
63 }
64 return result;
65}
66
69{
70 DATA_INVARIANT(verify(), "Structural invariants maintained");
71}
72
74 typet type,
75 bool top,
76 bool bottom)
77 : abstract_aggregate_baset(type, top, bottom)
78{
79 DATA_INVARIANT(verify(), "Structural invariants maintained");
80}
81
83 const exprt &expr,
84 const abstract_environmentt &environment,
85 const namespacet &ns)
86 : abstract_aggregate_baset(expr, environment, ns)
87{
88 if(expr.id() == ID_array)
89 {
90 mp_integer i = 0;
91 for(const exprt &entry : expr.operands())
92 {
93 auto index = eval_index(i, environment, ns);
94 map_put(index.value, environment.eval(entry, ns), index.overrun);
95 ++i;
96 }
98 }
99 DATA_INVARIANT(verify(), "Structural invariants maintained");
100}
101
103{
104 // Either the object is top or bottom (=> map empty)
105 // or the map is not empty => neither top nor bottom
107 (is_top() || is_bottom()) == map.empty();
108}
109
111{
112 // A structural invariant of constant_array_abstract_objectt is that
113 // (is_top() || is_bottom()) => map.empty()
114 map.clear();
115}
116
118 const abstract_object_pointert &other,
119 const widen_modet &widen_mode) const
120{
121 auto cast_other =
122 std::dynamic_pointer_cast<const full_array_abstract_objectt>(other);
123 if(cast_other)
124 return full_array_merge(cast_other, widen_mode);
125
126 return abstract_aggregate_baset::merge(other, widen_mode);
127}
128
130 const full_array_pointert &other,
131 const widen_modet &widen_mode) const
132{
133 if(is_bottom())
134 return std::make_shared<full_array_abstract_objectt>(*other);
135
136 const auto &result =
137 std::dynamic_pointer_cast<full_array_abstract_objectt>(mutable_clone());
138
139 bool modified = merge_shared_maps(map, other->map, result->map, widen_mode);
140 if(!modified)
141 {
142 DATA_INVARIANT(verify(), "Structural invariants maintained");
143 return shared_from_this();
144 }
145 else
146 {
147 INVARIANT(!result->is_top(), "Merge of maps will not generate top");
148 INVARIANT(!result->is_bottom(), "Merge of maps will not generate bottom");
149 DATA_INVARIANT(result->verify(), "Structural invariants maintained");
150 return result;
151 }
152}
153
155 std::ostream &out,
156 const ai_baset &ai,
157 const namespacet &ns) const
158{
159 if(is_top() || is_bottom())
160 {
162 }
163 else
164 {
165 out << "{";
166 for(const auto &entry : map.get_sorted_view())
167 {
168 out << "[" << entry.first << "] = ";
169 entry.second->output(out, ai, ns);
170 out << "\n";
171 }
172 out << "}";
173 }
174}
175
177 const abstract_environmentt &environment,
178 const exprt &expr,
179 const namespacet &ns) const
180{
181 if(is_top())
182 return environment.abstract_object_factory(expr.type(), ns, true, false);
183
184 auto read_element_fn =
185 [this, &environment, &ns](const index_exprt &index_expr) {
186 return this->read_element(environment, index_expr, ns);
187 };
188
189 auto result = apply_to_index_range(environment, expr, ns, read_element_fn);
190
191 return (result != nullptr) ? result : get_top_entry(environment, ns);
192}
193
195 abstract_environmentt &environment,
196 const namespacet &ns,
197 const std::stack<exprt> &stack,
198 const exprt &expr,
199 const abstract_object_pointert &value,
200 bool merging_write) const
201{
202 auto write_element_fn =
203 [this, &environment, &ns, &stack, &value, &merging_write](
204 const index_exprt &index_expr) {
205 return this->write_element(
206 environment, ns, stack, index_expr, value, merging_write);
207 };
208
209 auto result = apply_to_index_range(environment, expr, ns, write_element_fn);
210
211 return (result != nullptr) ? result : make_top();
212}
213
215 const abstract_environmentt &env,
216 const exprt &expr,
217 const namespacet &ns) const
218{
220 auto index = eval_index(expr, env, ns);
221
222 if(index.is_good)
223 return map_find_or_top(index.value, env, ns);
224
225 // Although we don't know where we are reading from, and therefore
226 // we should be returning a TOP value, we may still have useful
227 // additional information in elements of the array - such as write
228 // histories so we merge all the known array elements with TOP and return
229 // that.
230
231 // Create a new TOP value of the appropriate element type
232 auto result = get_top_entry(env, ns);
233
234 // Merge each known element into the TOP value
235 for(const auto &element : map.get_view())
236 result =
237 abstract_objectt::merge(result, element.second, widen_modet::no).object;
238
239 return result;
240}
241
243 abstract_environmentt &environment,
244 const namespacet &ns,
245 const std::stack<exprt> &stack,
246 const exprt &expr,
247 const abstract_object_pointert &value,
248 bool merging_write) const
249{
250 if(is_bottom())
251 {
253 environment, ns, stack, expr, value, merging_write);
254 }
255
256 if(!stack.empty())
257 return write_sub_element(
258 environment, ns, stack, expr, value, merging_write);
259
260 return write_leaf_element(environment, ns, expr, value, merging_write);
261}
262
264 abstract_environmentt &environment,
265 const namespacet &ns,
266 const std::stack<exprt> &stack,
267 const exprt &expr,
268 const abstract_object_pointert &value,
269 bool merging_write) const
270{
271 const auto &result =
272 std::dynamic_pointer_cast<full_array_abstract_objectt>(mutable_clone());
273
274 auto index = eval_index(expr, environment, ns);
275
276 if(index.is_good)
277 {
278 // We were able to evaluate the index to a value, which we
279 // assume is in bounds...
280 auto const existing_value = map_find_or_top(index.value, environment, ns);
281 result->map_put(
282 index.value,
283 environment.write(existing_value, value, stack, ns, merging_write),
284 index.overrun);
285 result->set_not_top();
286 DATA_INVARIANT(result->verify(), "Structural invariants maintained");
287 return result;
288 }
289 else
290 {
291 // We were not able to evaluate the index to a value
292 for(const auto &starting_value : map.get_view())
293 {
294 // Merging write since we don't know which index we are writing to
295 result->map.replace(
296 starting_value.first,
297 environment.write(starting_value.second, value, stack, ns, true));
298
299 result->set_not_top();
300 }
301
302 DATA_INVARIANT(result->verify(), "Structural invariants maintained");
303 return result;
304 }
305}
306
308 abstract_environmentt &environment,
309 const namespacet &ns,
310 const exprt &expr,
311 const abstract_object_pointert &value,
312 bool merging_write) const
313{
314 const auto &result =
315 std::dynamic_pointer_cast<full_array_abstract_objectt>(mutable_clone());
316
317 auto index = eval_index(expr, environment, ns);
318
319 if(index.is_good)
320 {
321 // We were able to evaluate the index expression to a constant
322 if(merging_write)
323 {
324 if(is_top())
325 {
326 DATA_INVARIANT(result->verify(), "Structural invariants maintained");
327 return result;
328 }
329
330 INVARIANT(!result->map.empty(), "If not top, map cannot be empty");
331
332 auto old_value = result->map.find(index.value);
333 if(old_value.has_value()) // if not found it's top, so nothing to merge
334 {
335 result->map.replace(
336 index.value,
337 abstract_objectt::merge(old_value.value(), value, widen_modet::no)
338 .object);
339 }
340
341 DATA_INVARIANT(result->verify(), "Structural invariants maintained");
342 return result;
343 }
344 else
345 {
346 result->map_put(index.value, value, index.overrun);
347 result->set_not_top();
348
349 DATA_INVARIANT(result->verify(), "Structural invariants maintained");
350 return result;
351 }
352 }
353
354 // try to write to all
355 // TODO(tkiley): Merge with each entry
357 environment, ns, std::stack<exprt>(), expr, value, merging_write);
358}
359
361 mp_integer index_value,
362 const abstract_object_pointert &value,
363 bool overrun)
364{
365 auto old_value = map.find(index_value);
366
367 if(!old_value.has_value())
368 map.insert(index_value, value);
369 else
370 {
371 // if we're over the max_index, merge with existing value
372 auto replacement_value =
373 overrun
374 ? abstract_objectt::merge(old_value.value(), value, widen_modet::no)
375 .object
376 : value;
377
378 map.replace(index_value, replacement_value);
379 }
380}
381
383 mp_integer index_value,
384 const abstract_environmentt &env,
385 const namespacet &ns) const
386{
387 auto value = map.find(index_value);
388 if(value.has_value())
389 return value.value();
390 return get_top_entry(env, ns);
391}
392
394 const abstract_environmentt &env,
395 const namespacet &ns) const
396{
397 return env.abstract_object_factory(type().subtype(), ns, true, false);
398}
399
401 const locationt &location) const
402{
404}
405
407 const locationt &location) const
408{
410}
411
413 const abstract_object_visitort &visitor) const
414{
415 const auto &result =
416 std::dynamic_pointer_cast<full_array_abstract_objectt>(mutable_clone());
417
418 bool is_modified = visit_map(result->map, visitor);
419
420 return is_modified ? result : shared_from_this();
421}
422
424 const exprt &name) const
425{
426 auto all_predicates = exprt::operandst{};
427
428 for(auto field : map.get_sorted_view())
429 {
430 auto ii = from_integer(field.first.to_long(), integer_typet());
431 auto index = index_exprt(name, ii);
432 auto field_expr = field.second->to_predicate(index);
433
434 if(!field_expr.is_true())
435 all_predicates.push_back(field_expr);
436 }
437
438 if(all_predicates.empty())
439 return true_exprt();
440 if(all_predicates.size() == 1)
441 return all_predicates.front();
442 return and_exprt(all_predicates);
443}
444
446 abstract_object_statisticst &statistics,
448 const abstract_environmentt &env,
449 const namespacet &ns) const
450{
451 for(const auto &object : map.get_view())
452 {
453 if(visited.find(object.second) == visited.end())
454 {
455 object.second->get_statistics(statistics, visited, env, ns);
456 }
457 }
458 statistics.objects_memory_usage += memory_sizet::from_bytes(sizeof(*this));
459}
460
462 const exprt &expr,
463 const abstract_environmentt &env,
464 const namespacet &ns)
465{
466 const auto &index_expr = to_index_expr(expr);
467 auto index_abstract_object = env.eval(index_expr.index(), ns);
468 auto value = index_abstract_object->to_constant();
469
470 if(!value.is_constant())
471 return {false};
472
473 mp_integer out_index;
474 bool result = to_integer(to_constant_expr(value), out_index);
475 if(result)
476 return {false};
477
478 return eval_index(out_index, env, ns);
479}
480
482 const mp_integer &index,
483 const abstract_environmentt &env,
484 const namespacet &ns)
485{
486 auto max_array_index = env.configuration().maximum_array_index;
487 bool overrun = (index >= max_array_index);
488
489 return {true, overrun ? max_array_index : index, overrun};
490}
An abstract version of a program environment.
std::shared_ptr< const T > sharing_ptrt
Merge is designed to allow different abstractions to be merged gracefully.
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Common behaviour for abstract objects modelling values - constants, intervals, etc.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:19
static bool merge_shared_maps(const sharing_mapt< keyt, abstract_object_pointert, false, hash > &map1, const sharing_mapt< keyt, abstract_object_pointert, false, hash > &map2, sharing_mapt< keyt, abstract_object_pointert, false, hash > &out_map, const widen_modet &widen_mode)
virtual abstract_object_pointert write_component(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &expr, const abstract_object_pointert &value, bool merging_write) const
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
const vsd_configt & configuration() const
Exposes the environment configuration.
virtual abstract_object_pointert write(const abstract_object_pointert &lhs, const abstract_object_pointert &rhs, std::stack< exprt > remaining_stack, const namespacet &ns, bool merge_write)
Used within assign to do the actual dispatch.
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.
virtual bool is_top() const
Find out if the abstract object is top.
virtual bool verify() const
Verify the internal structure of an abstract_object is correct.
virtual bool is_bottom() const
Find out if the abstract object is bottom.
virtual internal_abstract_object_pointert mutable_clone() const
goto_programt::const_targett locationt
abstract_object_pointert make_top() 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 void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print the value of the abstract object.
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
Boolean AND.
Definition: std_expr.h:1974
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
abstract_object_pointert merge(const abstract_object_pointert &other, const widen_modet &widen_mode) const override
Tries to do an array/array merge if merging with a constant array If it can't, falls back to parent m...
void map_put(mp_integer index, const abstract_object_pointert &value, bool overrun)
exprt to_predicate_internal(const exprt &name) const override
to_predicate implementation - derived classes will override
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
the current known value about this object.
abstract_object_pointert get_top_entry(const abstract_environmentt &env, const namespacet &ns) const
Short hand method for creating a top element of the array.
abstract_object_pointert map_find_or_top(mp_integer index, const abstract_environmentt &env, const namespacet &ns) const
abstract_object_pointert write_element(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &expr, const abstract_object_pointert &value, bool merging_write) const
bool verify() const override
To validate that the struct object is in a valid state.
CLONE abstract_object_pointert read_component(const abstract_environmentt &env, const exprt &expr, const namespacet &ns) const override
A helper function to read elements from an array.
abstract_object_pointert merge_location_context(const locationt &location) const override
Update the merge location context for an abstract object.
void set_top_internal() override
Perform any additional structural modifications when setting this object to TOP.
abstract_object_pointert full_array_merge(const full_array_pointert &other, const widen_modet &widen_mode) const
Merges an array into this array.
abstract_object_pointert write_component(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &expr, const abstract_object_pointert &value, bool merging_write) const override
A helper function to evaluate writing to a index of an array.
abstract_object_pointert visit_sub_elements(const abstract_object_visitort &visitor) const override
Apply a visitor operation to all sub elements of this abstract_object.
abstract_object_pointert read_element(const abstract_environmentt &env, const exprt &expr, const namespacet &ns) const
abstract_object_pointert write_leaf_element(abstract_environmentt &environment, const namespacet &ns, const exprt &expr, const abstract_object_pointert &value, bool merging_write) const
abstract_object_pointert write_sub_element(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &expr, const abstract_object_pointert &value, bool merging_write) const
abstract_object_pointert write_location_context(const locationt &location) const override
Update the location context for an abstract object.
void statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
sharing_ptrt< full_array_abstract_objectt > const full_array_pointert
Array index operator.
Definition: std_expr.h:1328
exprt & index()
Definition: std_expr.h:1363
exprt & array()
Definition: std_expr.h:1353
Unbounded, signed integers (mathematical integers, not bitvectors)
const irep_idt & id() const
Definition: irep.h:396
static memory_sizet from_bytes(std::size_t bytes)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
void insert(const key_type &k, valueU &&m)
Insert element, element must not exist in map.
Definition: sharing_map.h:1348
void replace(const key_type &k, valueU &&m)
Replace element, element must exist in map.
Definition: sharing_map.h:1425
bool empty() const
Check if map is empty.
Definition: sharing_map.h:360
sorted_viewt get_sorted_view() const
Convenience function to get a sorted view of the map elements.
Definition: sharing_map.h:462
void clear()
Clear map.
Definition: sharing_map.h:366
optionalt< std::reference_wrapper< const mapped_type > > find(const key_type &k) const
Find element.
Definition: sharing_map.h:1451
void get_view(V &view) const
Get a view of the elements in the map A view is a list of pairs with the components being const refer...
The Boolean constant true.
Definition: std_expr.h:2856
The type of an expression, extends irept.
Definition: type.h:29
abstract_object_pointert apply_to_index_range(const abstract_environmentt &environment, const exprt &expr, const namespacet &ns, index_fn &fn)
static eval_index_resultt eval_index(const exprt &expr, const abstract_environmentt &env, const namespacet &ns)
An abstraction of an array value.
bool visit_map(mapt &map, const visitort &visitor)
Definition: map_visit.h:12
Mathematical types.
BigInt mp_integer
Definition: smt_terms.h:12
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
Pure virtual interface required of a client that can apply a copy-on-write operation to a given abstr...
abstract_object_pointert object
Captures the user-supplied configuration for VSD, determining which domain abstractions are used,...