cprover
full_struct_abstract_object.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Struct abstract object
4 
5 Author: Thomas Kiley, thomas.kiley@diffblue.com
6 
7 \*******************************************************************/
8 
9 #include <ostream>
10 
12 #include <util/std_expr.h>
13 #include <util/std_types.h>
14 
16 
17 // #define DEBUG
18 
19 #ifdef DEBUG
20 # include <iostream>
21 #endif
22 
25  : abstract_aggregate_baset(ao), map(ao.map)
26 {
27 }
28 
31 {
32  PRECONDITION(t.id() == ID_struct);
33  DATA_INVARIANT(verify(), "Structural invariants maintained");
34 }
35 
37  const typet &t,
38  bool top,
39  bool bottom)
40  : abstract_aggregate_baset(t, top, bottom)
41 {
42  PRECONDITION(t.id() == ID_struct);
43  DATA_INVARIANT(verify(), "Structural invariants maintained");
44 }
45 
47  const exprt &e,
48  const abstract_environmentt &environment,
49  const namespacet &ns)
50  : abstract_aggregate_baset(e, environment, ns)
51 {
52  PRECONDITION(ns.follow(e.type()).id() == ID_struct);
53 
54  const struct_typet struct_type_def = to_struct_type(ns.follow(e.type()));
55 
56  bool did_initialize_values = false;
57  auto struct_type_it = struct_type_def.components().begin();
58  for(auto param_it = e.operands().begin(); param_it != e.operands().end();
59  ++param_it, ++struct_type_it)
60  {
62  struct_type_it->get_name(),
63  environment.abstract_object_factory(param_it->type(), *param_it, ns));
64  did_initialize_values = true;
65  }
66 
67  if(did_initialize_values)
68  {
69  set_not_top();
70  }
71 
72  DATA_INVARIANT(verify(), "Structural invariants maintained");
73 }
74 
76  const abstract_environmentt &environment,
77  const exprt &expr,
78  const namespacet &ns) const
79 {
80 #ifdef DEBUG
81  std::cout << "Reading component " << member_expr.get_component_name() << '\n';
82 #endif
83 
84  if(is_top())
85  {
86  return environment.abstract_object_factory(expr.type(), ns, true, false);
87  }
88  else
89  {
90  const member_exprt &member_expr = to_member_expr(expr);
92 
93  const irep_idt c = member_expr.get_component_name();
94 
95  auto const value = map.find(c);
96 
97  if(value.has_value())
98  {
99  return value.value();
100  }
101  else
102  {
103  return environment.abstract_object_factory(
104  member_expr.type(), ns, true, false);
105  }
106  }
107 }
108 
110  abstract_environmentt &environment,
111  const namespacet &ns,
112  const std::stack<exprt> &stack,
113  const exprt &expr,
114  const abstract_object_pointert &value,
115  bool merging_write) const
116 {
117 #ifdef DEBUG
118  std::cout << "Writing component " << member_expr.get_component_name() << '\n';
119 #endif
120  const member_exprt member_expr = to_member_expr(expr);
121 
122  if(is_bottom())
123  {
124  return std::make_shared<full_struct_abstract_objectt>(
125  member_expr.compound().type(), false, true);
126  }
127 
128  const auto &result =
129  std::dynamic_pointer_cast<full_struct_abstract_objectt>(mutable_clone());
130 
131  if(!stack.empty())
132  {
133  abstract_object_pointert starting_value;
134  const irep_idt c = member_expr.get_component_name();
135  auto const old_value = map.find(c);
136  if(!old_value.has_value())
137  {
138  starting_value = environment.abstract_object_factory(
139  member_expr.type(), ns, true, false);
140  result->map.insert(
141  c, environment.write(starting_value, value, stack, ns, merging_write));
142  }
143  else
144  {
145  result->map.replace(
146  c,
147  environment.write(old_value.value(), value, stack, ns, merging_write));
148  }
149 
150  result->set_not_top();
151  DATA_INVARIANT(result->verify(), "Structural invariants maintained");
152  return result;
153  }
154  else
155  {
156 #ifdef DEBUG
157  std::cout << "Setting component" << std::endl;
158 #endif
159 
160  const irep_idt c = member_expr.get_component_name();
161  auto const old_value = result->map.find(c);
162 
163  if(merging_write)
164  {
165  if(is_top()) // struct is top
166  {
167  DATA_INVARIANT(result->verify(), "Structural invariants maintained");
168  return result;
169  }
170 
171  INVARIANT(!result->map.empty(), "If not top, map cannot be empty");
172 
173  if(!old_value.has_value()) // component is top
174  {
175  DATA_INVARIANT(result->verify(), "Structural invariants maintained");
176  return result;
177  }
178 
179  result->map.replace(c, abstract_objectt::merge(old_value.value(), value));
180  }
181  else
182  {
183  if(old_value.has_value())
184  {
185  result->map.replace(c, value);
186  }
187  else
188  {
189  result->map.insert(c, value);
190  }
191  result->set_not_top();
192  INVARIANT(!result->is_bottom(), "top != bottom");
193  }
194 
195  DATA_INVARIANT(result->verify(), "Structural invariants maintained");
196 
197  return result;
198  }
199 }
200 
202  std::ostream &out,
203  const ai_baset &ai,
204  const namespacet &ns) const
205 {
206  // To ensure that a consistent ordering of fields is output, use
207  // the underlying type declaration for this struct to determine
208  // the ordering
210 
211  bool first = true;
212 
213  out << "{";
214  for(const auto &field : type_decl.components())
215  {
216  auto value = map.find(field.get_name());
217  if(value.has_value())
218  {
219  if(!first)
220  {
221  out << ", ";
222  }
223  out << '.' << field.get_name() << '=';
224  static_cast<const abstract_object_pointert &>(value.value())
225  ->output(out, ai, ns);
226  first = false;
227  }
228  }
229  out << "}";
230 }
231 
233 {
234  // Either the object is top or bottom (=> map empty)
235  // or the map is not empty => neither top nor bottom
236  return (is_top() || is_bottom()) == map.empty();
237 }
238 
241 {
242  constant_struct_pointert cast_other =
243  std::dynamic_pointer_cast<const full_struct_abstract_objectt>(other);
244  if(cast_other)
245  {
246  return merge_constant_structs(cast_other);
247  }
248  else
249  {
250  // TODO(tkiley): How do we set the result to be toppish? Does it matter?
251  return abstract_aggregate_baset::merge(other);
252  }
253 }
254 
256  constant_struct_pointert other) const
257 {
258  if(is_bottom())
259  {
260  return std::make_shared<full_struct_abstract_objectt>(*other);
261  }
262  else
263  {
264  const auto &result =
265  std::dynamic_pointer_cast<full_struct_abstract_objectt>(mutable_clone());
266 
267  bool modified = merge_shared_maps(map, other->map, result->map);
268 
269  if(!modified)
270  {
271  DATA_INVARIANT(verify(), "Structural invariants maintained");
272  return shared_from_this();
273  }
274  else
275  {
276  INVARIANT(!result->is_top(), "Merge of maps will not generate top");
277  INVARIANT(!result->is_bottom(), "Merge of maps will not generate bottom");
278  DATA_INVARIANT(result->verify(), "Structural invariants maintained");
279  return result;
280  }
281  }
282 }
283 
285  const abstract_object_visitort &visitor) const
286 {
287  const auto &result =
288  std::dynamic_pointer_cast<full_struct_abstract_objectt>(mutable_clone());
289 
290  bool modified = false;
291 
293  result->map.get_view(view);
294 
295  for(auto &item : view)
296  {
297  auto newval = visitor.visit(item.second);
298  if(newval != item.second)
299  {
300  result->map.replace(item.first, newval);
301  modified = true;
302  }
303  }
304 
305  if(modified)
306  {
307  return result;
308  }
309  else
310  {
311  return shared_from_this();
312  }
313 }
314 
316  abstract_object_statisticst &statistics,
317  abstract_object_visitedt &visited,
318  const abstract_environmentt &env,
319  const namespacet &ns) const
320 {
322  map.get_view(view);
323  for(auto const &object : view)
324  {
325  if(visited.find(object.second) == visited.end())
326  {
327  object.second->get_statistics(statistics, visited, env, ns);
328  }
329  }
330  statistics.objects_memory_usage += memory_sizet::from_bytes(sizeof(*this));
331 }
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)
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
static abstract_object_pointert merge(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Clones the first parameter and merges it with the second.
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:120
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
operandst & operands()
Definition: expr.h:96
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 merge(abstract_object_pointert other) const override
To merge an abstract object into this 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.
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_constant_structs(constant_struct_pointert other) const
Performs an element wise merge of the map for each struct.
const irep_idt & id() const
Definition: irep.h:407
Extract member of struct or union.
Definition: std_expr.h:2528
const exprt & compound() const
Definition: std_expr.h:2569
irep_idt get_component_name() const
Definition: std_expr.h:2542
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:51
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
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
optionalt< std::reference_wrapper< const mapped_type > > find(const key_type &k) const
Find element.
Definition: sharing_map.h:1449
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:226
Base type for structs and unions.
Definition: std_types.h:57
const componentst & components() const
Definition: std_types.h:142
The type of an expression, extends irept.
Definition: type.h:28
An abstraction of a structure that stores one abstract object per field.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
API to expression classes.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2612
Pre-defined types.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:209
Pure virtual interface required of a client that can apply a copy-on-write operation to a given abstr...
virtual abstract_object_pointert visit(const abstract_object_pointert element) const =0