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
26 : abstract_aggregate_baset(ao), map(ao.map)
27{
28}
29
32{
33 PRECONDITION(t.id() == ID_struct);
34 DATA_INVARIANT(verify(), "Structural invariants maintained");
35}
36
38 const typet &t,
39 bool top,
40 bool bottom)
41 : abstract_aggregate_baset(t, top, bottom)
42{
43 PRECONDITION(t.id() == ID_struct);
44 DATA_INVARIANT(verify(), "Structural invariants maintained");
45}
46
48 const exprt &e,
49 const abstract_environmentt &environment,
50 const namespacet &ns)
51 : abstract_aggregate_baset(e, environment, ns)
52{
53 PRECONDITION(ns.follow(e.type()).id() == ID_struct);
54
55 const struct_typet struct_type_def = to_struct_type(ns.follow(e.type()));
56
57 bool did_initialize_values = false;
58 auto struct_type_it = struct_type_def.components().begin();
59 for(auto param_it = e.operands().begin(); param_it != e.operands().end();
60 ++param_it, ++struct_type_it)
61 {
63 struct_type_it->get_name(),
64 environment.abstract_object_factory(param_it->type(), *param_it, ns));
65 did_initialize_values = true;
66 }
67
68 if(did_initialize_values)
69 {
71 }
72
73 DATA_INVARIANT(verify(), "Structural invariants maintained");
74}
75
77 const abstract_environmentt &environment,
78 const exprt &expr,
79 const namespacet &ns) const
80{
81#ifdef DEBUG
82 std::cout << "Reading component " << member_expr.get_component_name() << '\n';
83#endif
84
85 if(is_top())
86 {
87 return environment.abstract_object_factory(expr.type(), ns, true, false);
88 }
89 else
90 {
91 const member_exprt &member_expr = to_member_expr(expr);
93
94 const irep_idt c = member_expr.get_component_name();
95
96 auto const value = map.find(c);
97
98 if(value.has_value())
99 {
100 return value.value();
101 }
102 else
103 {
104 return environment.abstract_object_factory(
105 member_expr.type(), ns, true, false);
106 }
107 }
108}
109
111 abstract_environmentt &environment,
112 const namespacet &ns,
113 const std::stack<exprt> &stack,
114 const exprt &expr,
115 const abstract_object_pointert &value,
116 bool merging_write) const
117{
118#ifdef DEBUG
119 std::cout << "Writing component " << member_expr.get_component_name() << '\n';
120#endif
121 const member_exprt member_expr = to_member_expr(expr);
122
123 if(is_bottom())
124 {
125 return std::make_shared<full_struct_abstract_objectt>(
126 member_expr.compound().type(), false, true);
127 }
128
129 const auto &result =
130 std::dynamic_pointer_cast<full_struct_abstract_objectt>(mutable_clone());
131
132 if(!stack.empty())
133 {
134 abstract_object_pointert starting_value;
135 const irep_idt c = member_expr.get_component_name();
136 auto const old_value = map.find(c);
137 if(!old_value.has_value())
138 {
139 starting_value = environment.abstract_object_factory(
140 member_expr.type(), ns, true, false);
141 result->map.insert(
142 c, environment.write(starting_value, value, stack, ns, merging_write));
143 }
144 else
145 {
146 result->map.replace(
147 c,
148 environment.write(old_value.value(), value, stack, ns, merging_write));
149 }
150
151 result->set_not_top();
152 DATA_INVARIANT(result->verify(), "Structural invariants maintained");
153 return result;
154 }
155 else
156 {
157#ifdef DEBUG
158 std::cout << "Setting component" << std::endl;
159#endif
160
161 const irep_idt c = member_expr.get_component_name();
162 auto const old_value = result->map.find(c);
163
164 if(merging_write)
165 {
166 if(is_top()) // struct is top
167 {
168 DATA_INVARIANT(result->verify(), "Structural invariants maintained");
169 return result;
170 }
171
172 INVARIANT(!result->map.empty(), "If not top, map cannot be empty");
173
174 if(!old_value.has_value()) // component is top
175 {
176 DATA_INVARIANT(result->verify(), "Structural invariants maintained");
177 return result;
178 }
179
180 result->map.replace(
181 c,
182 abstract_objectt::merge(old_value.value(), value, widen_modet::no)
183 .object);
184 }
185 else
186 {
187 if(old_value.has_value())
188 {
189 result->map.replace(c, value);
190 }
191 else
192 {
193 result->map.insert(c, value);
194 }
195 result->set_not_top();
196 INVARIANT(!result->is_bottom(), "top != bottom");
197 }
198
199 DATA_INVARIANT(result->verify(), "Structural invariants maintained");
200
201 return result;
202 }
203}
204
206 std::ostream &out,
207 const ai_baset &ai,
208 const namespacet &ns) const
209{
210 // To ensure that a consistent ordering of fields is output, use
211 // the underlying type declaration for this struct to determine
212 // the ordering
214
215 bool first = true;
216
217 out << "{";
218 for(const auto &field : type_decl.components())
219 {
220 auto value = map.find(field.get_name());
221 if(value.has_value())
222 {
223 if(!first)
224 {
225 out << ", ";
226 }
227 out << '.' << field.get_name() << '=';
228 static_cast<const abstract_object_pointert &>(value.value())
229 ->output(out, ai, ns);
230 first = false;
231 }
232 }
233 out << "}";
234}
235
237{
238 // Either the object is top or bottom (=> map empty)
239 // or the map is not empty => neither top nor bottom
240 return (is_top() || is_bottom()) == map.empty();
241}
242
244 const abstract_object_pointert &other,
245 const widen_modet &widen_mode) const
246{
247 constant_struct_pointert cast_other =
248 std::dynamic_pointer_cast<const full_struct_abstract_objectt>(other);
249 if(cast_other)
250 return merge_constant_structs(cast_other, widen_mode);
251
252 return abstract_aggregate_baset::merge(other, widen_mode);
253}
254
257 const widen_modet &widen_mode) const
258{
259 if(is_bottom())
260 return std::make_shared<full_struct_abstract_objectt>(*other);
261
262 const auto &result =
263 std::dynamic_pointer_cast<full_struct_abstract_objectt>(mutable_clone());
264
265 bool modified = merge_shared_maps(map, other->map, result->map, widen_mode);
266
267 if(!modified)
268 {
269 DATA_INVARIANT(verify(), "Structural invariants maintained");
270 return shared_from_this();
271 }
272 else
273 {
274 INVARIANT(!result->is_top(), "Merge of maps will not generate top");
275 INVARIANT(!result->is_bottom(), "Merge of maps will not generate bottom");
276 DATA_INVARIANT(result->verify(), "Structural invariants maintained");
277 return result;
278 }
279}
280
282 const locationt &location) const
283{
285}
286
288 const locationt &location) const
289{
291}
292
294 const abstract_object_visitort &visitor) const
295{
296 const auto &result =
297 std::dynamic_pointer_cast<full_struct_abstract_objectt>(mutable_clone());
298
299 bool is_modified = visit_map(result->map, visitor);
300
301 return is_modified ? result : shared_from_this();
302}
303
305 const exprt &name) const
306{
307 auto all_predicates = exprt::operandst{};
308
309 for(auto field : map.get_sorted_view())
310 {
311 auto field_name = member_exprt(name, field.first, name.type());
312 auto field_expr = field.second->to_predicate(field_name);
313
314 if(!field_expr.is_true())
315 all_predicates.push_back(field_expr);
316 }
317
318 if(all_predicates.empty())
319 return true_exprt();
320 if(all_predicates.size() == 1)
321 return all_predicates.front();
322 return and_exprt(all_predicates);
323}
324
326 abstract_object_statisticst &statistics,
328 const abstract_environmentt &env,
329 const namespacet &ns) const
330{
332 map.get_view(view);
333 for(auto const &object : view)
334 {
335 if(visited.find(object.second) == visited.end())
336 {
337 object.second->get_statistics(statistics, visited, env, ns);
338 }
339 }
340 statistics.objects_memory_usage += memory_sizet::from_bytes(sizeof(*this));
341}
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:119
Boolean AND.
Definition: std_expr.h:1974
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
std::vector< exprt > operandst
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
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:2667
const exprt & compound() const
Definition: std_expr.h:2708
irep_idt get_component_name() const
Definition: std_expr.h:2681
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.
Definition: sharing_map.h:388
bool empty() const
Check if map is empty.
Definition: sharing_map.h:360
sorted_viewt get_sorted_view() const
Convenience function to get a sorted view of the map elements.
Definition: sharing_map.h:462
optionalt< std::reference_wrapper< const mapped_type > > find(const key_type &k) const
Find element.
Definition: sharing_map.h:1451
void insert_or_replace(const key_type &k, valueU &&m)
Definition: sharing_map.h:292
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
const componentst & components() const
Definition: std_types.h:147
The Boolean constant true.
Definition: std_expr.h:2856
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:510
#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:2751
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...
abstract_object_pointert object