cprover
abstract_aggregate_object.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity
4 
5  Author: Jez Higgins, jez@jezuk.co.uk
6 
7 \*******************************************************************/
8 
12 #ifndef CBMC_ABSTRACT_AGGREGATE_OBJECT_H
13 #define CBMC_ABSTRACT_AGGREGATE_OBJECT_H
14 
17 #include <stack>
18 
20 {
21 };
22 
23 template <class aggregate_typet, class aggregate_traitst>
26 {
27 public:
30  {
31  PRECONDITION(type.id() == aggregate_traitst::TYPE_ID());
32  }
33 
34  abstract_aggregate_objectt(const typet &type, bool tp, bool bttm)
35  : abstract_objectt(type, tp, bttm)
36  {
37  PRECONDITION(type.id() == aggregate_traitst::TYPE_ID());
38  }
39 
41  const exprt &expr,
42  const abstract_environmentt &environment,
43  const namespacet &ns)
44  : abstract_objectt(expr, environment, ns)
45  {
46  PRECONDITION(ns.follow(expr.type()).id() == aggregate_traitst::TYPE_ID());
47  }
48 
50  const exprt &expr,
51  const std::vector<abstract_object_pointert> &operands,
52  const abstract_environmentt &environment,
53  const namespacet &ns) const override
54  {
55  if(expr.id() == aggregate_traitst::ACCESS_EXPR_ID())
56  return read_component(environment, expr, ns);
57 
59  expr, operands, environment, ns);
60  }
61 
63  abstract_environmentt &environment,
64  const namespacet &ns,
65  const std::stack<exprt> &stack,
66  const exprt &specifier,
67  const abstract_object_pointert &value,
68  bool merging_write) const override
69  {
70  return write_component(
71  environment, ns, stack, specifier, value, merging_write);
72  }
73 
76  abstract_object_visitedt &visited,
77  const abstract_environmentt &env,
78  const namespacet &ns) const override
79  {
81  aggregate_traitst::get_statistics(statistics, visited, env, ns);
82  this->statistics(statistics, visited, env, ns);
83  }
84 
85 protected:
87  const abstract_environmentt &environment,
88  const exprt &expr,
89  const namespacet &ns) const
90  {
91  // If we are bottom then so are the components
92  // otherwise the components could be anything
93  return environment.abstract_object_factory(
94  aggregate_traitst::read_type(expr.type(), type()),
95  ns,
96  !is_bottom(),
97  is_bottom());
98  }
99 
101  abstract_environmentt &environment,
102  const namespacet &ns,
103  const std::stack<exprt> &stack,
104  const exprt &expr,
105  const abstract_object_pointert &value,
106  bool merging_write) const
107  {
108  if(is_top() || is_bottom())
109  {
110  return shared_from_this();
111  }
112  else
113  {
114  return std::make_shared<aggregate_typet>(type(), true, false);
115  }
116  }
117 
118  virtual void statistics(
120  abstract_object_visitedt &visited,
121  const abstract_environmentt &env,
122  const namespacet &ns) const = 0;
123 
124  template <class keyt, typename hash>
125  static bool merge_shared_maps(
129  {
130  bool modified = false;
131 
133  delta_viewt delta_view;
134  map1.get_delta_view(map2, delta_view, true);
135 
136  for(auto &item : delta_view)
137  {
138  bool changes = false;
140  abstract_objectt::merge(item.m, item.get_other_map_value(), changes);
141  if(changes)
142  {
143  modified = true;
144  out_map.replace(item.k, v_new);
145  }
146  }
147 
148  return modified;
149  }
150 };
151 
153 {
154  static const irep_idt TYPE_ID()
155  {
156  return ID_array;
157  }
158  static const irep_idt ACCESS_EXPR_ID()
159  {
160  return ID_index;
161  }
162  static typet read_type(const typet &, const typet &object_type)
163  {
164  array_typet array_type(to_array_type(object_type));
165  return array_type.subtype();
166  }
167 
168  static void get_statistics(
169  abstract_object_statisticst &statistics,
170  abstract_object_visitedt &visited,
171  const abstract_environmentt &env,
172  const namespacet &ns)
173  {
174  ++statistics.number_of_arrays;
175  }
176 };
177 
179 {
180  static const irep_idt &TYPE_ID()
181  {
182  return ID_struct;
183  }
184  static const irep_idt &ACCESS_EXPR_ID()
185  {
186  return ID_member;
187  }
188  static const typet &read_type(const typet &expr_type, const typet &)
189  {
190  return expr_type;
191  }
192 
193  static void get_statistics(
194  abstract_object_statisticst &statistics,
195  abstract_object_visitedt &visited,
196  const abstract_environmentt &env,
197  const namespacet &ns)
198  {
199  ++statistics.number_of_structs;
200  }
201 };
202 
204 {
205  static const irep_idt TYPE_ID()
206  {
207  return ID_union;
208  }
209  static const irep_idt ACCESS_EXPR_ID()
210  {
211  return ID_member;
212  }
213  static typet read_type(const typet &, const typet &object_type)
214  {
215  return object_type;
216  }
217 
218  static void get_statistics(
219  abstract_object_statisticst &statistics,
220  abstract_object_visitedt &visited,
221  const abstract_environmentt &env,
222  const namespacet &ns)
223  {
224  }
225 };
226 
227 #endif //CBMC_ABSTRACT_AGGREGATE_OBJECT_H
An abstract version of a program environment.
abstract_objectt is the top of the inheritance heirarchy of objects used to represent individual vari...
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
abstract_aggregate_objectt(const typet &type, bool tp, bool bttm)
virtual abstract_object_pointert read_component(const abstract_environmentt &environment, const exprt &expr, const namespacet &ns) const
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
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)
abstract_aggregate_objectt(const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
abstract_aggregate_objectt(const typet &type)
virtual void statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const =0
abstract_object_pointert write(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &specifier, const abstract_object_pointert &value, bool merging_write) const override
A helper function to evaluate writing to a component of an abstract object.
abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
Interface for transforms.
virtual 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
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 abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const
Interface for transforms.
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.
virtual void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
Arrays with given size.
Definition: std_types.h:968
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
const irep_idt & id() const
Definition: irep.h:407
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
A map implemented as a tree where subtrees can be shared between different maps.
Definition: sharing_map.h:190
void replace(const key_type &k, valueU &&m)
Replace element, element must exist in map.
Definition: sharing_map.h:1423
void get_delta_view(const sharing_mapt &other, delta_viewt &delta_view, const bool only_common=true) const
Get a delta view of the elements in the map.
Definition: sharing_map.h:936
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1018
static typet read_type(const typet &, const typet &object_type)
static void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns)
static const irep_idt TYPE_ID()
static const irep_idt ACCESS_EXPR_ID()
static const typet & read_type(const typet &expr_type, const typet &)
static void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns)
static const irep_idt & TYPE_ID()
static const irep_idt & ACCESS_EXPR_ID()
static typet read_type(const typet &, const typet &object_type)
static const irep_idt TYPE_ID()
static void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns)
static const irep_idt ACCESS_EXPR_ID()