cprover
Loading...
Searching...
No Matches
abstract_aggregate_object.h
Go to the documentation of this file.
1/*******************************************************************\
2
3 Module: analyses variable-sensitivity
4
5 Author: Jez Higgins, jez@jezuk.co.uk
6
7\*******************************************************************/
8
12#ifndef CBMC_ABSTRACT_AGGREGATE_OBJECT_H
13#define CBMC_ABSTRACT_AGGREGATE_OBJECT_H
14
17#include <stack>
18
20
22{
23};
24
25template <class aggregate_typet, class aggregate_traitst>
28{
29public:
32 {
33 PRECONDITION(type.id() == aggregate_traitst::TYPE_ID());
34 }
35
36 abstract_aggregate_objectt(const typet &type, bool tp, bool bttm)
37 : abstract_objectt(type, tp, bttm)
38 {
39 PRECONDITION(type.id() == aggregate_traitst::TYPE_ID());
40 }
41
43 const exprt &expr,
44 const abstract_environmentt &environment,
45 const namespacet &ns)
46 : abstract_objectt(expr, environment, ns)
47 {
48 PRECONDITION(ns.follow(expr.type()).id() == aggregate_traitst::TYPE_ID());
49 }
50
52 const exprt &expr,
53 const std::vector<abstract_object_pointert> &operands,
54 const abstract_environmentt &environment,
55 const namespacet &ns) const override
56 {
57 if(expr.id() == aggregate_traitst::ACCESS_EXPR_ID())
58 return read_component(environment, expr, ns);
59
61 expr, operands, environment, ns);
62 }
63
65 abstract_environmentt &environment,
66 const namespacet &ns,
67 const std::stack<exprt> &stack,
68 const exprt &specifier,
69 const abstract_object_pointert &value,
70 bool merging_write) const override
71 {
72 return write_component(
73 environment, ns, stack, specifier, value, merging_write);
74 }
75
79 const abstract_environmentt &env,
80 const namespacet &ns) const override
81 {
83 aggregate_traitst::get_statistics(statistics, visited, env, ns);
84 this->statistics(statistics, visited, env, ns);
85 }
86
87protected:
89 const abstract_environmentt &environment,
90 const exprt &expr,
91 const namespacet &ns) const
92 {
93 // If we are bottom then so are the components
94 // otherwise the components could be anything
95 return environment.abstract_object_factory(
96 aggregate_traitst::read_type(expr.type(), type()),
97 ns,
98 !is_bottom(),
99 is_bottom());
100 }
101
103 abstract_environmentt &environment,
104 const namespacet &ns,
105 const std::stack<exprt> &stack,
106 const exprt &expr,
107 const abstract_object_pointert &value,
108 bool merging_write) const
109 {
110 if(is_top() || is_bottom())
111 {
112 return shared_from_this();
113 }
114 else
115 {
116 return std::make_shared<aggregate_typet>(type(), true, false);
117 }
118 }
119
120 virtual void statistics(
123 const abstract_environmentt &env,
124 const namespacet &ns) const = 0;
125
126 template <class keyt, typename hash>
127 static bool merge_shared_maps(
131 const widen_modet &widen_mode)
132 {
133 bool modified = false;
134
136 delta_viewt delta_view;
137 map1.get_delta_view(map2, delta_view, true);
138
139 for(auto &item : delta_view)
140 {
141 auto v_new =
142 abstract_objectt::merge(item.m, item.get_other_map_value(), widen_mode);
143 if(v_new.modified)
144 {
145 modified = true;
146 out_map.replace(item.k, v_new.object);
147 }
148 }
149
150 return modified;
151 }
152};
153
155{
156 static const irep_idt TYPE_ID()
157 {
158 return ID_array;
159 }
161 {
162 return ID_index;
163 }
164 static typet read_type(const typet &, const typet &object_type)
165 {
166 array_typet array_type(to_array_type(object_type));
167 return array_type.element_type();
168 }
169
170 static void get_statistics(
171 abstract_object_statisticst &statistics,
173 const abstract_environmentt &env,
174 const namespacet &ns)
175 {
176 ++statistics.number_of_arrays;
177 }
178};
179
181{
182 static const irep_idt &TYPE_ID()
183 {
184 return ID_struct;
185 }
186 static const irep_idt &ACCESS_EXPR_ID()
187 {
188 return ID_member;
189 }
190 static const typet &read_type(const typet &expr_type, const typet &)
191 {
192 return expr_type;
193 }
194
195 static void get_statistics(
196 abstract_object_statisticst &statistics,
198 const abstract_environmentt &env,
199 const namespacet &ns)
200 {
201 ++statistics.number_of_structs;
202 }
203};
204
206{
207 static const irep_idt TYPE_ID()
208 {
209 return ID_union;
210 }
212 {
213 return ID_member;
214 }
215 static typet read_type(const typet &, const typet &object_type)
216 {
217 return object_type;
218 }
219
220 static void get_statistics(
221 abstract_object_statisticst &statistics,
223 const abstract_environmentt &env,
224 const namespacet &ns)
225 {
226 }
227};
228
229#endif //CBMC_ABSTRACT_AGGREGATE_OBJECT_H
An abstract version of a program environment.
abstract_objectt is the top of the inheritance heirarchy of objects used to represent individual vari...
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Statistics gathering for the variable senstivity domain.
abstract_aggregate_objectt(const typet &type, bool tp, bool bttm)
virtual abstract_object_pointert read_component(const abstract_environmentt &environment, const exprt &expr, const namespacet &ns) const
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, const widen_modet &widen_mode)
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
abstract_aggregate_objectt(const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
abstract_aggregate_objectt(const typet &type)
virtual void statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const =0
abstract_object_pointert write(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &specifier, const abstract_object_pointert &value, bool merging_write) const override
A helper function to evaluate writing to a component of an abstract object.
abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
Interface for transforms.
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 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 is_bottom() const
Find out if the abstract object is bottom.
virtual abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const
Interface for transforms.
static combine_result merge(const abstract_object_pointert &op1, const abstract_object_pointert &op2, const locationt &merge_location, const widen_modet &widen_mode)
virtual void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
Arrays with given size.
Definition std_types.h:763
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:777
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
typet & type()
Return the type of the expression.
Definition expr.h:82
const irep_idt & id() const
Definition irep.h:396
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition namespace.cpp:49
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.
void replace(const key_type &k, valueU &&m)
Replace element, element must exist in map.
void get_delta_view(const sharing_mapt &other, delta_viewt &delta_view, const bool only_common=true) const
Get a delta view of the elements in the map.
The type of an expression, extends irept.
Definition type.h:29
#define PRECONDITION(CONDITION)
Definition invariant.h:463
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:832
static typet read_type(const typet &, const typet &object_type)
static void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns)
static const irep_idt TYPE_ID()
static const irep_idt ACCESS_EXPR_ID()
static const typet & read_type(const typet &expr_type, const typet &)
static void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns)
static const irep_idt & TYPE_ID()
static const irep_idt & ACCESS_EXPR_ID()
static typet read_type(const typet &, const typet &object_type)
static const irep_idt TYPE_ID()
static void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns)
static const irep_idt ACCESS_EXPR_ID()