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
36
38 const typet &t,
39 bool top,
40 bool bottom)
41 : abstract_aggregate_baset(t, top, bottom)
42{
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
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();
61 {
63 struct_type_it->get_name(),
64 environment.abstract_object_factory(param_it->type(), *param_it, ns));
66 }
67
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 {
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
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 {
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 {
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{
248 std::dynamic_pointer_cast<const full_struct_abstract_objectt>(other);
249 if(cast_other)
251
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
286
292
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{
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();
323}
324
326 abstract_object_statisticst &statistics,
329 const namespacet &ns) const
330{
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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
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: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...