cprover
Loading...
Searching...
No Matches
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
19class ai_baset;
20
22 full_array_abstract_objectt,
23 array_aggregate_typet>
24{
25public:
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
90protected:
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(
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
157private:
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<
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.
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...