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 
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  {
70  set_not_top();
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,
327  abstract_object_visitedt &visited,
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 }
widen_modet
widen_modet
Definition: abstract_environment.h:33
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:147
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:69
abstract_objectt::is_top
virtual bool is_top() const
Find out if the abstract object is top.
Definition: abstract_object.cpp:155
full_struct_abstract_objectt::visit_sub_elements
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.
Definition: full_struct_abstract_object.cpp:293
abstract_objectt::locationt
goto_programt::const_targett locationt
Definition: abstract_object.h:220
abstract_aggregate_objectt< full_struct_abstract_objectt, struct_aggregate_typet >::merge_shared_maps
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)
Definition: abstract_aggregate_object.h:127
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
visit_map
bool visit_map(mapt &map, const visitort &visitor)
Definition: map_visit.h:12
abstract_environmentt::write
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.
Definition: abstract_environment.cpp:237
to_struct_union_type
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214
widen_modet::no
@ no
full_struct_abstract_objectt::constant_struct_pointert
sharing_ptrt< full_struct_abstract_objectt > constant_struct_pointert
Definition: full_struct_abstract_object.h:23
typet
The type of an expression, extends irept.
Definition: type.h:28
sharing_mapt::get_view
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...
full_struct_abstract_objectt::map
shared_struct_mapt map
Definition: full_struct_abstract_object.h:106
struct_union_typet
Base type for structs and unions.
Definition: std_types.h:62
full_struct_abstract_objectt::merge_constant_structs
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.
Definition: full_struct_abstract_object.cpp:255
abstract_objectt::type
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
Definition: abstract_object.cpp:47
sharing_mapt::get_sorted_view
sorted_viewt get_sorted_view() const
Convenience function to get a sorted view of the map elements.
Definition: sharing_map.h:462
and_exprt
Boolean AND.
Definition: std_expr.h:1920
full_struct_abstract_objectt::read_component
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.
Definition: full_struct_abstract_object.cpp:76
abstract_environmentt
Definition: abstract_environment.h:41
exprt
Base class for all expressions.
Definition: expr.h:54
sharing_mapt::map
nodet map
Definition: sharing_map.h:649
full_struct_abstract_objectt::write_location_context
abstract_object_pointert write_location_context(const locationt &location) const override
Update the location context for an abstract object.
Definition: full_struct_abstract_object.cpp:281
full_struct_abstract_objectt::full_struct_abstract_objectt
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 ...
Definition: full_struct_abstract_object.cpp:24
full_struct_abstract_objectt
Definition: full_struct_abstract_object.h:21
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
full_struct_abstract_object.h
An abstraction of a structure that stores one abstract object per field.
sharing_mapt< irep_idt, abstract_object_pointert, false, irep_id_hash >::viewt
std::vector< view_itemt > viewt
View of the key-value pairs in the map.
Definition: sharing_map.h:388
abstract_objectt::merge
static combine_result merge(const abstract_object_pointert &op1, const abstract_object_pointert &op2, const locationt &merge_location, const widen_modet &widen_mode)
Definition: abstract_object.cpp:209
full_struct_abstract_objectt::statistics
void statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
Definition: full_struct_abstract_object.cpp:325
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
abstract_object_statisticst
Definition: abstract_object_statistics.h:19
member_exprt::compound
const exprt & compound() const
Definition: std_expr.h:2654
abstract_environmentt::abstract_object_factory
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.
Definition: abstract_environment.cpp:312
full_struct_abstract_objectt::output
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.
Definition: full_struct_abstract_object.cpp:205
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
abstract_environment.h
An abstract version of a program environment.
map_visit.h
sharing_mapt::insert_or_replace
void insert_or_replace(const key_type &k, valueU &&m)
Definition: sharing_map.h:292
abstract_aggregate_objectt< full_struct_abstract_objectt, struct_aggregate_typet >
sharing_mapt::empty
bool empty() const
Check if map is empty.
Definition: sharing_map.h:360
irept::id
const irep_idt & id() const
Definition: irep.h:407
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
full_struct_abstract_objectt::merge
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.
Definition: full_struct_abstract_object.cpp:243
abstract_object_visitedt
std::set< abstract_object_pointert > abstract_object_visitedt
Definition: abstract_object.h:70
abstract_objectt::abstract_object_visitort
Pure virtual interface required of a client that can apply a copy-on-write operation to a given abstr...
Definition: abstract_object.h:346
location_update_visitort
Definition: location_update_visitor.h:16
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2613
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:231
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
full_struct_abstract_objectt::merge_location_context
abstract_object_pointert merge_location_context(const locationt &location) const override
Update the merge location context for an abstract object.
Definition: full_struct_abstract_object.cpp:287
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
abstract_objectt::set_not_top
void set_not_top()
Definition: abstract_object.h:481
full_struct_abstract_objectt::write_component
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.
Definition: full_struct_abstract_object.cpp:110
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:2627
exprt::operands
operandst & operands()
Definition: expr.h:92
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
abstract_objectt::is_bottom
virtual bool is_bottom() const
Find out if the abstract object is bottom.
Definition: abstract_object.cpp:160
abstract_objectt::combine_result::object
abstract_object_pointert object
Definition: abstract_object.h:264
full_struct_abstract_objectt::to_predicate_internal
exprt to_predicate_internal(const exprt &name) const override
to_predicate implementation - derived classes will override
Definition: full_struct_abstract_object.cpp:304
true_exprt
The Boolean constant true.
Definition: std_expr.h:2802
full_struct_abstract_objectt::verify
bool verify() const override
Function: full_struct_abstract_objectt::verify.
Definition: full_struct_abstract_object.cpp:236
std_expr.h
API to expression classes.
location_update_visitor.h
memory_sizet::from_bytes
static memory_sizet from_bytes(std::size_t bytes)
Definition: memory_units.cpp:38
abstract_objectt::mutable_clone
virtual internal_abstract_object_pointert mutable_clone() const
Definition: abstract_object.h:428
abstract_objectt::t
typet t
To enforce copy-on-write these are private and have read-only accessors.
Definition: abstract_object.h:385
sharing_mapt::find
optionalt< std::reference_wrapper< const mapped_type > > find(const key_type &k) const
Find element.
Definition: sharing_map.h:1451
merge_location_update_visitort
Definition: location_update_visitor.h:35