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.
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...