cprover
Loading...
Searching...
No Matches
full_struct_abstract_object.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Struct abstract object
4
5Author: Thomas Kiley, thomas.kiley@diffblue.com
6
7\*******************************************************************/
8
9#include <ostream>
10
12#include <util/std_expr.h>
13
16#include "map_visit.h"
17
18// #define DEBUG
19
20#ifdef DEBUG
21# include <iostream>
22#endif
23
29
31 const typet &t,
32 bool top,
33 bool bottom)
34 : abstract_aggregate_baset(t, top, bottom)
35{
37 DATA_INVARIANT(verify(), "Structural invariants maintained");
38}
39
41 const exprt &e,
42 const abstract_environmentt &environment,
43 const namespacet &ns)
44 : abstract_aggregate_baset(e, environment, ns)
45{
46 PRECONDITION(ns.follow(e.type()).id() == ID_struct);
47
49
50 bool did_initialize_values = false;
51 auto struct_type_it = struct_type_def.components().begin();
52 for(auto param_it = e.operands().begin(); param_it != e.operands().end();
54 {
56 struct_type_it->get_name(),
57 environment.abstract_object_factory(param_it->type(), *param_it, ns));
59 }
60
62 {
64 }
65
66 DATA_INVARIANT(verify(), "Structural invariants maintained");
67}
68
70 const abstract_environmentt &environment,
71 const exprt &expr,
72 const namespacet &ns) const
73{
74#ifdef DEBUG
75 std::cout << "Reading component " << to_member_expr(expr).get_component_name()
76 << '\n';
77#endif
78
79 if(is_top())
80 {
81 return environment.abstract_object_factory(expr.type(), ns, true, false);
82 }
83 else
84 {
87
88 const irep_idt c = member_expr.get_component_name();
89
90 auto const value = map.find(c);
91
92 if(value.has_value())
93 {
94 return value.value();
95 }
96 else
97 {
98 return environment.abstract_object_factory(
99 member_expr.type(), ns, true, false);
100 }
101 }
102}
103
105 abstract_environmentt &environment,
106 const namespacet &ns,
107 const std::stack<exprt> &stack,
108 const exprt &expr,
109 const abstract_object_pointert &value,
110 bool merging_write) const
111{
113#ifdef DEBUG
114 std::cout << "Writing component " << member_expr.get_component_name() << '\n';
115#endif
116
117 if(is_bottom())
118 {
119 return std::make_shared<full_struct_abstract_objectt>(
120 member_expr.compound().type(), false, true);
121 }
122
123 const auto &result =
124 std::dynamic_pointer_cast<full_struct_abstract_objectt>(mutable_clone());
125
126 if(!stack.empty())
127 {
129 const irep_idt c = member_expr.get_component_name();
130 auto const old_value = map.find(c);
131 if(!old_value.has_value())
132 {
134 member_expr.type(), ns, true, false);
135 result->map.insert(
136 c, environment.write(starting_value, value, stack, ns, merging_write));
137 }
138 else
139 {
140 result->map.replace(
141 c,
142 environment.write(old_value.value(), value, stack, ns, merging_write));
143 }
144
145 result->set_not_top();
146 DATA_INVARIANT(result->verify(), "Structural invariants maintained");
147 return result;
148 }
149 else
150 {
151#ifdef DEBUG
152 std::cout << "Setting component" << std::endl;
153#endif
154
155 const irep_idt c = member_expr.get_component_name();
156 auto const old_value = result->map.find(c);
157
158 if(merging_write)
159 {
160 if(is_top()) // struct is top
161 {
162 DATA_INVARIANT(result->verify(), "Structural invariants maintained");
163 return result;
164 }
165
166 INVARIANT(!result->map.empty(), "If not top, map cannot be empty");
167
168 if(!old_value.has_value()) // component is top
169 {
170 DATA_INVARIANT(result->verify(), "Structural invariants maintained");
171 return result;
172 }
173
174 result->map.replace(
175 c,
176 abstract_objectt::merge(old_value.value(), value, widen_modet::no)
177 .object);
178 }
179 else
180 {
181 if(old_value.has_value())
182 {
183 result->map.replace(c, value);
184 }
185 else
186 {
187 result->map.insert(c, value);
188 }
189 result->set_not_top();
190 INVARIANT(!result->is_bottom(), "top != bottom");
191 }
192
193 DATA_INVARIANT(result->verify(), "Structural invariants maintained");
194
195 return result;
196 }
197}
198
200 std::ostream &out,
201 const ai_baset &ai,
202 const namespacet &ns) const
203{
204 // To ensure that a consistent ordering of fields is output, use
205 // the underlying type declaration for this struct to determine
206 // the ordering
208
209 bool first = true;
210
211 out << "{";
212 for(const auto &field : type_decl.components())
213 {
214 auto value = map.find(field.get_name());
215 if(value.has_value())
216 {
217 if(!first)
218 {
219 out << ", ";
220 }
221 out << '.' << field.get_name() << '=';
222 static_cast<const abstract_object_pointert &>(value.value())
223 ->output(out, ai, ns);
224 first = false;
225 }
226 }
227 out << "}";
228}
229
231{
232 // Either the object is top or bottom (=> map empty)
233 // or the map is not empty => neither top nor bottom
234 return (is_top() || is_bottom()) == map.empty();
235}
236
238 const abstract_object_pointert &other,
239 const widen_modet &widen_mode) const
240{
242 std::dynamic_pointer_cast<const full_struct_abstract_objectt>(other);
243 if(cast_other)
245
247}
248
251 const widen_modet &widen_mode) const
252{
253 if(is_bottom())
254 return std::make_shared<full_struct_abstract_objectt>(*other);
255
256 const auto &result =
257 std::dynamic_pointer_cast<full_struct_abstract_objectt>(mutable_clone());
258
259 bool modified = merge_shared_maps(map, other->map, result->map, widen_mode);
260
261 if(!modified)
262 {
263 DATA_INVARIANT(verify(), "Structural invariants maintained");
264 return shared_from_this();
265 }
266 else
267 {
268 INVARIANT(!result->is_top(), "Merge of maps will not generate top");
269 INVARIANT(!result->is_bottom(), "Merge of maps will not generate bottom");
270 DATA_INVARIANT(result->verify(), "Structural invariants maintained");
271 return result;
272 }
273}
274
280
286
289{
290 const auto &result =
291 std::dynamic_pointer_cast<full_struct_abstract_objectt>(mutable_clone());
292
293 bool is_modified = visit_map(result->map, visitor);
294
295 return is_modified ? result : shared_from_this();
296}
297
299 const exprt &name) const
300{
301 const auto &compound_type = to_struct_union_type(name.type());
303
304 for(auto field : map.get_sorted_view())
305 {
306 auto field_name =
307 member_exprt(name, compound_type.get_component(field.first));
308 auto field_expr = field.second->to_predicate(field_name);
309
310 if(!field_expr.is_true())
311 all_predicates.push_back(field_expr);
312 }
313
314 if(all_predicates.empty())
315 return true_exprt();
316 if(all_predicates.size() == 1)
317 return all_predicates.front();
319}
320
322 abstract_object_statisticst &statistics,
325 const namespacet &ns) const
326{
329 for(auto const &object : view)
330 {
331 if(visited.find(object.second) == visited.end())
332 {
333 object.second->get_statistics(statistics, visited, env, ns);
334 }
335 }
336 statistics.objects_memory_usage += memory_sizet::from_bytes(sizeof(*this));
337}
An abstract version of a program environment.
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
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)
virtual abstract_object_pointert write(const abstract_object_pointert &lhs, const abstract_object_pointert &rhs, std::stack< exprt > remaining_stack, const namespacet &ns, bool merge_write)
Used within assign to do the actual dispatch.
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 internal_abstract_object_pointert mutable_clone() const
goto_programt::const_targett locationt
static combine_result merge(const abstract_object_pointert &op1, const abstract_object_pointert &op2, const locationt &merge_location, const widen_modet &widen_mode)
typet t
To enforce copy-on-write these are private and have read-only accessors.
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:118
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Boolean AND.
Definition std_expr.h:2071
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
std::vector< exprt > operandst
Definition expr.h:58
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
void output(std::ostream &out, const class ai_baset &ai, const class namespacet &ns) const override
To provide a human readable string to the out representing the current known value about this object.
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 component of a struct.
bool verify() const override
Function: full_struct_abstract_objectt::verify.
void statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
abstract_object_pointert write_location_context(const locationt &location) const override
Update the location context for an abstract object.
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_object_pointert merge_constant_structs(constant_struct_pointert other, const widen_modet &widen_mode) const
Performs an element wise merge of the map for each struct.
abstract_object_pointert merge_location_context(const locationt &location) const override
Update the merge location context for an abstract object.
sharing_ptrt< full_struct_abstract_objectt > constant_struct_pointert
CLONE abstract_object_pointert read_component(const abstract_environmentt &environment, const exprt &expr, const namespacet &ns) const override
A helper function to evaluate the abstract object contained within a struct.
full_struct_abstract_objectt(const full_struct_abstract_objectt &ao)
Explicit copy-constructor to make it clear that the shared_map used to store the values of fields is ...
abstract_object_pointert merge(const abstract_object_pointert &other, const widen_modet &widen_mode) const override
To merge an abstract object into this abstract object.
exprt to_predicate_internal(const exprt &name) const override
to_predicate implementation - derived classes will override
const irep_idt & id() const
Definition irep.h:396
Extract member of struct or union.
Definition std_expr.h:2794
static memory_sizet from_bytes(std::size_t bytes)
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
std::vector< view_itemt > viewt
View of the key-value pairs in the map.
bool empty() const
Check if map is empty.
sorted_viewt get_sorted_view() const
Convenience function to get a sorted view of the map elements.
optionalt< std::reference_wrapper< const mapped_type > > find(const key_type &k) const
Find element.
void insert_or_replace(const key_type &k, valueU &&m)
void get_view(V &view) const
Get a view of the elements in the map A view is a list of pairs with the components being const refer...
Structure type, corresponds to C style structs.
Definition std_types.h:231
Base type for structs and unions.
Definition std_types.h:62
The Boolean constant true.
Definition std_expr.h:3008
The type of an expression, extends irept.
Definition type.h:29
An abstraction of a structure that stores one abstract object per field.
bool visit_map(mapt &map, const visitort &visitor)
Definition map_visit.h:12
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
API to expression classes.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2886
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition std_types.h:214
Pure virtual interface required of a client that can apply a copy-on-write operation to a given abstr...