cprover
Loading...
Searching...
No Matches
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
28
30 const exprt &expr,
32 const namespacet &ns);
34 const mp_integer &index,
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{
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)
125
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
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
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
379 }
380}
381
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
395 const namespacet &ns) const
396{
397 return env.abstract_object_factory(type().subtype(), ns, true, false);
398}
399
405
411
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{
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();
443}
444
446 abstract_object_statisticst &statistics,
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,
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
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,
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::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)
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
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.
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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
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.
void replace(const key_type &k, valueU &&m)
Replace element, element must exist in map.
bool empty() const
Check if map is empty.
sorted_viewt get_sorted_view() const
Convenience function to get a sorted view of the map elements.
void clear()
Clear map.
optionalt< std::reference_wrapper< const mapped_type > > find(const key_type &k) const
Find element.
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
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
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...
Captures the user-supplied configuration for VSD, determining which domain abstractions are used,...