cprover
full_array_abstract_object.h
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 
11 
12 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_ARRAY_ABSTRACT_OBJECT_H
13 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_ARRAY_ABSTRACT_OBJECT_H
14 
15 #include <iosfwd>
16 #include <vector>
17 
20 
21 class ai_baset;
22 
24  full_array_abstract_objectt,
25  array_aggregate_typet>
26 {
27 public:
33 
36 
44 
51  const exprt &expr,
52  const abstract_environmentt &environment,
53  const namespacet &ns);
54 
62  void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
63  const override;
64 
77  visit_sub_elements(const abstract_object_visitort &visitor) const override;
78 
79 protected:
80  CLONE
81 
94  const abstract_environmentt &env,
95  const exprt &expr,
96  const namespacet &ns) const override;
97 
110  abstract_environmentt &environment,
111  const namespacet &ns,
112  const std::stack<exprt> &stack,
113  const exprt &expr,
114  const abstract_object_pointert &value,
115  bool merging_write) const override;
116 
117  void statistics(
119  abstract_object_visitedt &visited,
120  const abstract_environmentt &env,
121  const namespacet &ns) const override;
122 
130 
137  bool verify() const override;
138 
141  void set_top_internal() override;
142 
143 private:
145  const abstract_environmentt &env,
146  const exprt &expr,
147  const namespacet &ns) const;
148 
150  abstract_environmentt &environment,
151  const namespacet &ns,
152  const std::stack<exprt> &stack,
153  const exprt &expr,
154  const abstract_object_pointert &value,
155  bool merging_write) const;
156 
158  abstract_environmentt &environment,
159  const namespacet &ns,
160  const std::stack<exprt> &stack,
161  const exprt &expr,
162  const abstract_object_pointert &value,
163  bool merging_write) const;
164 
166  abstract_environmentt &environment,
167  const namespacet &ns,
168  const exprt &expr,
169  const abstract_object_pointert &value,
170  bool merging_write) const;
171 
172  // Since we don't store for any index where the value is top
173  // we don't use a regular array but instead a map of array indices
174  // to the value at that index
176  {
177  size_t operator()(const mp_integer &i) const
178  {
179  return std::hash<BigInt::ullong_t>{}(i.to_ulong());
180  }
181  };
182 
183  typedef sharing_mapt<
184  mp_integer,
186  false,
187  mp_integer_hasht>
189 
191 
201  get_top_entry(const abstract_environmentt &env, const namespacet &ns) const;
202 
211  full_array_merge(const full_array_pointert other) const;
212 };
213 
214 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_ARRAY_ABSTRACT_OBJECT_H
Common behaviour for abstract objects modelling aggregate values - arrays, structs,...
std::shared_ptr< const T > sharing_ptrt
Merge is designed to allow different abstractions to be merged gracefully.
#define CLONE
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
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
Base class for all expressions.
Definition: expr.h:54
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_aggregate_objectt< full_array_abstract_objectt, array_aggregate_typet > abstract_aggregate_baset
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
sharing_mapt< mp_integer, abstract_object_pointert, false, mp_integer_hasht > shared_array_mapt
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...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
A map implemented as a tree where subtrees can be shared between different maps.
Definition: sharing_map.h:190
The type of an expression, extends irept.
Definition: type.h:28
An abstraction of a single value that just stores a constant.
BigInt mp_integer
Definition: mp_arith.h:19
Pure virtual interface required of a client that can apply a copy-on-write operation to a given abstr...