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
15#include <util/namespace.h>
16
19
21
22#include <stack>
23
27
28template <class aggregate_typet, class aggregate_traitst>
31{
32public:
35 {
36 PRECONDITION(type.id() == aggregate_traitst::TYPE_ID());
37 }
38
40 const exprt &expr,
41 const abstract_environmentt &environment,
42 const namespacet &ns)
43 : abstract_objectt(expr, environment, ns)
44 {
45 PRECONDITION(ns.follow(expr.type()).id() == aggregate_traitst::TYPE_ID());
46 }
47
49 const exprt &expr,
50 const std::vector<abstract_object_pointert> &operands,
51 const abstract_environmentt &environment,
52 const namespacet &ns) const override
53 {
54 if(expr.id() == aggregate_traitst::ACCESS_EXPR_ID())
55 return read_component(environment, expr, ns);
56
58 expr, operands, environment, ns);
59 }
60
62 abstract_environmentt &environment,
63 const namespacet &ns,
64 const std::stack<exprt> &stack,
65 const exprt &specifier,
66 const abstract_object_pointert &value,
67 bool merging_write) const override
68 {
69 return write_component(
70 environment, ns, stack, specifier, value, merging_write);
71 }
72
77 const namespacet &ns) const override
78 {
80 aggregate_traitst::get_statistics(statistics, visited, env, ns);
81 this->statistics(statistics, visited, env, ns);
82 }
83
84protected:
86 const abstract_environmentt &environment,
87 const exprt &expr,
88 const namespacet &ns) const
89 {
90 // If we are bottom then so are the components
91 // otherwise the components could be anything
92 return environment.abstract_object_factory(
93 aggregate_traitst::read_type(expr.type(), type()),
94 ns,
95 !is_bottom(),
96 is_bottom());
97 }
98
100 abstract_environmentt &environment,
101 const namespacet &ns,
102 const std::stack<exprt> &stack,
103 const exprt &expr,
104 const abstract_object_pointert &value,
105 bool merging_write) const
106 {
107 if(is_top() || is_bottom())
108 {
109 return shared_from_this();
110 }
111 else
112 {
113 return std::make_shared<aggregate_typet>(type(), true, false);
114 }
115 }
116
117 virtual void statistics(
121 const namespacet &ns) const = 0;
122
123 template <class keyt, typename hash>
124 static bool merge_shared_maps(
128 const widen_modet &widen_mode)
129 {
130 bool modified = false;
131
134 map1.get_delta_view(map2, delta_view, true);
135
136 for(auto &item : delta_view)
137 {
138 auto v_new =
139 abstract_objectt::merge(item.m, item.get_other_map_value(), widen_mode);
140 if(v_new.modified)
141 {
142 modified = true;
143 out_map.replace(item.k, v_new.object);
144 }
145 }
146
147 return modified;
148 }
149};
150
152{
153 static const irep_idt TYPE_ID()
154 {
155 return ID_array;
156 }
158 {
159 return ID_index;
160 }
161 static typet read_type(const typet &, const typet &object_type)
162 {
164 return array_type.element_type();
165 }
166
167 static void get_statistics(
168 abstract_object_statisticst &statistics,
171 const namespacet &ns)
172 {
173 ++statistics.number_of_arrays;
174 }
175};
176
178{
179 static const irep_idt &TYPE_ID()
180 {
181 return ID_struct;
182 }
183 static const irep_idt &ACCESS_EXPR_ID()
184 {
185 return ID_member;
186 }
187 static const typet &read_type(const typet &expr_type, const typet &)
188 {
189 return expr_type;
190 }
191
192 static void get_statistics(
193 abstract_object_statisticst &statistics,
196 const namespacet &ns)
197 {
198 ++statistics.number_of_structs;
199 }
200};
201
203{
204 static const irep_idt TYPE_ID()
205 {
206 return ID_union;
207 }
209 {
210 return ID_member;
211 }
212 static typet read_type(const typet &, const typet &object_type)
213 {
214 return object_type;
215 }
216
217 static void get_statistics(
218 abstract_object_statisticst &statistics,
221 const namespacet &ns)
222 {
223 }
224};
225
226#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)
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Arrays with given size.
Definition std_types.h:763
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
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
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:844
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()