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 
18 
19 class ai_baset;
20 
22  full_array_abstract_objectt,
23  array_aggregate_typet>
24 {
25 public:
31 
34 
42 
49  const exprt &expr,
50  const abstract_environmentt &environment,
51  const namespacet &ns);
52 
60  void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
61  const override;
62 
72  write_location_context(const locationt &location) const override;
74  merge_location_context(const locationt &location) const override;
75 
88  visit_sub_elements(const abstract_object_visitort &visitor) const override;
89 
90 protected:
91  CLONE
92 
105  const abstract_environmentt &env,
106  const exprt &expr,
107  const namespacet &ns) const override;
108 
121  abstract_environmentt &environment,
122  const namespacet &ns,
123  const std::stack<exprt> &stack,
124  const exprt &expr,
125  const abstract_object_pointert &value,
126  bool merging_write) const override;
127 
128  void statistics(
130  abstract_object_visitedt &visited,
131  const abstract_environmentt &env,
132  const namespacet &ns) const override;
133 
142  const abstract_object_pointert &other,
143  const widen_modet &widen_mode) const override;
144 
151  bool verify() const override;
152 
155  void set_top_internal() override;
156 
157 private:
159  const abstract_environmentt &env,
160  const exprt &expr,
161  const namespacet &ns) const;
162 
164  abstract_environmentt &environment,
165  const namespacet &ns,
166  const std::stack<exprt> &stack,
167  const exprt &expr,
168  const abstract_object_pointert &value,
169  bool merging_write) const;
170 
172  abstract_environmentt &environment,
173  const namespacet &ns,
174  const std::stack<exprt> &stack,
175  const exprt &expr,
176  const abstract_object_pointert &value,
177  bool merging_write) const;
178 
180  abstract_environmentt &environment,
181  const namespacet &ns,
182  const exprt &expr,
183  const abstract_object_pointert &value,
184  bool merging_write) const;
185 
186  // Since we don't store for any index where the value is top
187  // we don't use a regular array but instead a map of array indices
188  // to the value at that index
190  {
191  size_t operator()(const mp_integer &i) const
192  {
193  return std::hash<BigInt::ullong_t>{}(i.to_ulong());
194  }
195  };
196 
197  typedef sharing_mapt<
198  mp_integer,
200  false,
201  mp_integer_hasht>
203 
205 
206  void map_put(
207  mp_integer index,
208  const abstract_object_pointert &value,
209  bool overrun);
211  mp_integer index,
212  const abstract_environmentt &env,
213  const namespacet &ns) const;
214 
224  get_top_entry(const abstract_environmentt &env, const namespacet &ns) const;
225 
235  const full_array_pointert &other,
236  const widen_modet &widen_mode) const;
237 
238  exprt to_predicate_internal(const exprt &name) const override;
239 };
240 
241 #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
goto_programt::const_targett locationt
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
Base class for all expressions.
Definition: expr.h:54
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_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
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
sharing_mapt< mp_integer, abstract_object_pointert, false, mp_integer_hasht > shared_array_mapt
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
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:29
BigInt mp_integer
Definition: smt_terms.h:12
Pure virtual interface required of a client that can apply a copy-on-write operation to a given abstr...