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 #include <ostream>
9 
11 #include <util/arith_tools.h>
12 #include <util/namespace.h>
13 #include <util/std_expr.h>
14 
16 
17 bool eval_index(
18  const exprt &index,
19  const abstract_environmentt &env,
20  const namespacet &ns,
21  mp_integer &out_index);
22 
23 template <typename index_fn>
25  const abstract_environmentt &environment,
26  const exprt &expr,
27  const namespacet &ns,
28  index_fn &fn)
29 {
30  const index_exprt &index_expr = to_index_expr(expr);
31  auto evaluated_index = environment.eval(index_expr.index(), ns);
32  auto index_range = (std::dynamic_pointer_cast<const abstract_value_objectt>(
33  evaluated_index->unwrap_context()))
34  ->index_range(ns);
35 
36  if(!index_range->advance_to_next())
37  return nullptr;
38 
39  sharing_ptrt<abstract_objectt> result = nullptr;
40  do
41  {
42  auto at_index = fn(index_exprt(index_expr.array(), index_range->current()));
43 
44  result = (result == nullptr) ? at_index
45  : abstract_objectt::merge(result, at_index);
46  } while(!result->is_top() && index_range->advance_to_next());
47  return result;
48 }
49 
52 {
53  DATA_INVARIANT(verify(), "Structural invariants maintained");
54 }
55 
57  typet type,
58  bool top,
59  bool bottom)
60  : abstract_aggregate_baset(type, top, bottom)
61 {
62  DATA_INVARIANT(verify(), "Structural invariants maintained");
63 }
64 
66  const exprt &expr,
67  const abstract_environmentt &environment,
68  const namespacet &ns)
69  : abstract_aggregate_baset(expr, environment, ns)
70 {
71  if(expr.id() == ID_array)
72  {
73  int index = 0;
74  for(const exprt &entry : expr.operands())
75  {
76  map.insert(mp_integer(index), environment.eval(entry, ns));
77  ++index;
78  }
79  set_not_top();
80  }
81  DATA_INVARIANT(verify(), "Structural invariants maintained");
82 }
83 
85 {
86  // Either the object is top or bottom (=> map empty)
87  // or the map is not empty => neither top nor bottom
89  (is_top() || is_bottom()) == map.empty();
90 }
91 
93 {
94  // A structural invariant of constant_array_abstract_objectt is that
95  // (is_top() || is_bottom()) => map.empty()
96  map.clear();
97 }
98 
101 {
102  auto cast_other =
103  std::dynamic_pointer_cast<const full_array_abstract_objectt>(other);
104  if(cast_other)
105  {
106  return full_array_merge(cast_other);
107  }
108  else
109  {
110  // TODO(tkiley): How do we set the result to be toppish? Does it matter?
111  return abstract_aggregate_baset::merge(other);
112  }
113 }
114 
116  const full_array_pointert other) const
117 {
118  if(is_bottom())
119  {
120  return std::make_shared<full_array_abstract_objectt>(*other);
121  }
122  else
123  {
124  const auto &result =
125  std::dynamic_pointer_cast<full_array_abstract_objectt>(mutable_clone());
126 
127  bool modified = merge_shared_maps(map, other->map, result->map);
128  if(!modified)
129  {
130  DATA_INVARIANT(verify(), "Structural invariants maintained");
131  return shared_from_this();
132  }
133  else
134  {
135  INVARIANT(!result->is_top(), "Merge of maps will not generate top");
136  INVARIANT(!result->is_bottom(), "Merge of maps will not generate bottom");
137  DATA_INVARIANT(result->verify(), "Structural invariants maintained");
138  return result;
139  }
140  }
141 }
142 
144  std::ostream &out,
145  const ai_baset &ai,
146  const namespacet &ns) const
147 {
148  if(is_top() || is_bottom())
149  {
151  }
152  else
153  {
154  out << "{";
155  for(const auto &entry : map.get_sorted_view())
156  {
157  out << "[" << entry.first << "] = ";
158  entry.second->output(out, ai, ns);
159  out << "\n";
160  }
161  out << "}";
162  }
163 }
164 
166  const abstract_environmentt &environment,
167  const exprt &expr,
168  const namespacet &ns) const
169 {
170  if(is_top())
171  return environment.abstract_object_factory(expr.type(), ns, true, false);
172 
173  auto read_element_fn =
174  [this, &environment, &ns](const index_exprt &index_expr) {
175  return this->read_element(environment, index_expr, ns);
176  };
177 
178  auto result = apply_to_index_range(environment, expr, ns, read_element_fn);
179 
180  return (result != nullptr) ? result : get_top_entry(environment, ns);
181 }
182 
184  abstract_environmentt &environment,
185  const namespacet &ns,
186  const std::stack<exprt> &stack,
187  const exprt &expr,
188  const abstract_object_pointert &value,
189  bool merging_write) const
190 {
191  auto write_element_fn =
192  [this, &environment, &ns, &stack, &value, &merging_write](
193  const index_exprt &index_expr) {
194  return this->write_element(
195  environment, ns, stack, index_expr, value, merging_write);
196  };
197 
198  auto result = apply_to_index_range(environment, expr, ns, write_element_fn);
199 
200  return (result != nullptr) ? result : make_top();
201 }
202 
204  const abstract_environmentt &env,
205  const exprt &expr,
206  const namespacet &ns) const
207 {
209  mp_integer index_value;
210  if(eval_index(expr, env, ns, index_value))
211  {
212  // Here we are assuming it is always in bounds
213  auto const value = map.find(index_value);
214  if(value.has_value())
215  return value.value();
216  return get_top_entry(env, ns);
217  }
218  else
219  {
220  // Although we don't know where we are reading from, and therefore
221  // we should be returning a TOP value, we may still have useful
222  // additional information in elements of the array - such as write
223  // histories so we merge all the known array elements with TOP and return
224  // that.
225 
226  // Create a new TOP value of the appropriate element type
227  abstract_object_pointert result = get_top_entry(env, ns);
228 
229  // Merge each known element into the TOP value
230  for(const auto &element : map.get_view())
231  result = abstract_objectt::merge(result, element.second);
232 
233  return result;
234  }
235 }
236 
238  abstract_environmentt &environment,
239  const namespacet &ns,
240  const std::stack<exprt> &stack,
241  const exprt &expr,
242  const abstract_object_pointert &value,
243  bool merging_write) const
244 {
245  if(is_bottom())
246  {
248  environment, ns, stack, expr, value, merging_write);
249  }
250 
251  if(!stack.empty())
252  return write_sub_element(
253  environment, ns, stack, expr, value, merging_write);
254 
255  return write_leaf_element(environment, ns, expr, value, merging_write);
256 }
257 
259  abstract_environmentt &environment,
260  const namespacet &ns,
261  const std::stack<exprt> &stack,
262  const exprt &expr,
263  const abstract_object_pointert &value,
264  bool merging_write) const
265 {
266  const auto &result =
267  std::dynamic_pointer_cast<full_array_abstract_objectt>(mutable_clone());
268 
269  mp_integer index_value;
270  bool good_index = eval_index(expr, environment, ns, index_value);
271 
272  if(good_index)
273  {
274  // We were able to evaluate the index to a value, which we
275  // assume is in bounds...
276  auto const old_value = map.find(index_value);
277 
278  if(old_value.has_value())
279  {
280  result->map.replace(
281  index_value,
282  environment.write(old_value.value(), value, stack, ns, merging_write));
283  }
284  else
285  {
286  result->map.insert(
287  index_value,
288  environment.write(
289  get_top_entry(environment, ns), value, stack, ns, merging_write));
290  }
291 
292  result->set_not_top();
293  DATA_INVARIANT(result->verify(), "Structural invariants maintained");
294  return result;
295  }
296  else
297  {
298  // We were not able to evaluate the index to a value
299  for(const auto &starting_value : map.get_view())
300  {
301  // Merging write since we don't know which index we are writing to
302  result->map.replace(
303  starting_value.first,
304  environment.write(starting_value.second, value, stack, ns, true));
305 
306  result->set_not_top();
307  }
308 
309  DATA_INVARIANT(result->verify(), "Structural invariants maintained");
310  return result;
311  }
312 }
313 
315  abstract_environmentt &environment,
316  const namespacet &ns,
317  const exprt &expr,
318  const abstract_object_pointert &value,
319  bool merging_write) const
320 {
321  const auto &result =
322  std::dynamic_pointer_cast<full_array_abstract_objectt>(mutable_clone());
323 
324  mp_integer index_value;
325  bool good_index = eval_index(expr, environment, ns, index_value);
326 
327  if(good_index)
328  {
329  // We were able to evaluate the index expression to a constant
330  if(merging_write)
331  {
332  if(is_top())
333  {
334  DATA_INVARIANT(result->verify(), "Structural invariants maintained");
335  return result;
336  }
337 
338  INVARIANT(!result->map.empty(), "If not top, map cannot be empty");
339 
340  auto old_value = result->map.find(index_value);
341  if(old_value.has_value()) // if not found it's top, so nothing to merge
342  {
343  result->map.replace(
344  index_value, abstract_objectt::merge(old_value.value(), value));
345  }
346 
347  DATA_INVARIANT(result->verify(), "Structural invariants maintained");
348  return result;
349  }
350  else
351  {
352  auto old_value = result->map.find(index_value);
353 
354  if(old_value.has_value())
355  result->map.replace(index_value, value);
356  else
357  result->map.insert(index_value, value);
358 
359  result->set_not_top();
360  DATA_INVARIANT(result->verify(), "Structural invariants maintained");
361  return result;
362  }
363  }
364 
365  // try to write to all
366  // TODO(tkiley): Merge with each entry
368  environment, ns, std::stack<exprt>(), expr, value, merging_write);
369 }
370 
372  const abstract_environmentt &env,
373  const namespacet &ns) const
374 {
375  return env.abstract_object_factory(type().subtype(), ns, true, false);
376 }
377 
379  const abstract_object_visitort &visitor) const
380 {
381  const auto &result =
382  std::dynamic_pointer_cast<full_array_abstract_objectt>(mutable_clone());
383 
384  bool modified = false;
385  for(auto &item : result->map.get_view())
386  {
387  auto newval = visitor.visit(item.second);
388  if(newval != item.second)
389  {
390  result->map.replace(item.first, std::move(newval));
391  modified = true;
392  }
393  }
394 
395  if(modified)
396  {
397  return result;
398  }
399  else
400  {
401  return shared_from_this();
402  }
403 }
404 
406  abstract_object_statisticst &statistics,
407  abstract_object_visitedt &visited,
408  const abstract_environmentt &env,
409  const namespacet &ns) const
410 {
411  for(const auto &object : map.get_view())
412  {
413  if(visited.find(object.second) == visited.end())
414  {
415  object.second->get_statistics(statistics, visited, env, ns);
416  }
417  }
418  statistics.objects_memory_usage += memory_sizet::from_bytes(sizeof(*this));
419 }
420 
422  const exprt &expr,
423  const abstract_environmentt &env,
424  const namespacet &ns,
425  mp_integer &out_index)
426 {
427  const index_exprt &index = to_index_expr(expr);
428  abstract_object_pointert index_abstract_object = env.eval(index.index(), ns);
429  exprt value = index_abstract_object->to_constant();
430 
431  if(!value.is_constant())
432  return false;
433 
434  constant_exprt constant_index = to_constant_expr(value);
435  bool result = to_integer(constant_index, out_index);
436  return !result;
437 }
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
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)
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
abstract_object_pointert make_top() const
virtual void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print the value of the abstract object.
static abstract_object_pointert merge(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Clones the first parameter and merges it with the second.
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:120
A constant literal expression.
Definition: std_expr.h:2668
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:40
operandst & operands()
Definition: expr.h:96
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 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.
void set_top_internal() override
Perform any additional structural modifications when setting this object to TOP.
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
void statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
abstract_object_pointert full_array_merge(const full_array_pointert other) const
Merges an array into this array.
sharing_ptrt< full_array_abstract_objectt > const full_array_pointert
abstract_object_pointert merge(abstract_object_pointert other) const override
Tries to do an array/array merge if merging with a constant array If it can't, falls back to parent m...
Array index operator.
Definition: std_expr.h:1243
exprt & array()
Definition: std_expr.h:1259
exprt & index()
Definition: std_expr.h:1269
const irep_idt & id() const
Definition: irep.h:407
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:92
void insert(const key_type &k, valueU &&m)
Insert element, element must not exist in map.
Definition: sharing_map.h:1346
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:1449
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 type of an expression, extends irept.
Definition: type.h:28
bool eval_index(const exprt &index, const abstract_environmentt &env, const namespacet &ns, mp_integer &out_index)
abstract_object_pointert apply_to_index_range(const abstract_environmentt &environment, const exprt &expr, const namespacet &ns, index_fn &fn)
An abstraction of an array value.
BigInt mp_integer
Definition: mp_arith.h:19
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2701
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
Pure virtual interface required of a client that can apply a copy-on-write operation to a given abstr...
virtual abstract_object_pointert visit(const abstract_object_pointert element) const =0