cprover
abstract_object.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity
4 
5  Author: Thomas Kiley, thomas.kiley@diffblue.com
6 
7 \*******************************************************************/
8 
9 #include <array>
10 #include <iostream>
11 
14 
16 #include <util/arith_tools.h>
17 #include <util/ieee_float.h>
18 #include <util/namespace.h>
19 #include <util/simplify_expr.h>
20 #include <util/std_expr.h>
21 #include <util/type.h>
22 
23 #include "abstract_object.h"
24 
26  : t(type), bottom(false), top(true)
27 {
28 }
29 
30 abstract_objectt::abstract_objectt(const typet &type, bool top, bool bottom)
31  : t(type), bottom(bottom), top(top)
32 {
33  PRECONDITION(!(top && bottom));
34 }
35 
37  const exprt &expr,
38  const abstract_environmentt &environment,
39  const namespacet &ns)
40  : t(expr.type()), bottom(false), top(true)
41 {
42 }
43 
45  const typet &type,
46  const exprt &expr,
47  const abstract_environmentt &environment,
48  const namespacet &ns)
49  : t(type), bottom(false), top(true)
50 {
51 }
52 
54 {
55  return t;
56 }
57 
60 {
61  return abstract_object_merge(other);
62 }
63 
65  const abstract_object_pointert other) const
66 {
67  if(is_top() || other->bottom)
68  return this->abstract_object_merge_internal(other);
69 
71  merged->set_top();
72  merged->bottom = false;
73  return merged->abstract_object_merge_internal(other);
74 }
75 
77  const abstract_object_pointert other) const
78 {
79  // Default implementation
80  return shared_from_this();
81 }
82 
85 {
86  return abstract_object_meet(other);
87 }
88 
90  const abstract_object_pointert &other) const
91 {
92  if(is_bottom() || other->top)
93  return this->abstract_object_meet_internal(other);
94 
96  met->bottom = true;
97  met->top = false;
98  return met->abstract_object_meet_internal(other);
99 }
100 
102  const abstract_object_pointert &other) const
103 {
104  // Default implementation
105  return shared_from_this();
106 }
107 
109  const exprt &expr,
110  const std::vector<abstract_object_pointert> &operands,
111  const abstract_environmentt &environment,
112  const namespacet &ns) const
113 {
114  exprt copy = expr;
115 
116  for(exprt &op : copy.operands())
117  {
118  abstract_object_pointert op_abstract_object = environment.eval(op, ns);
119  const exprt &const_op = op_abstract_object->to_constant();
120  op = const_op.is_nil() ? op : const_op;
121  }
122 
123  simplify(copy, ns);
124 
125  for(const exprt &op : copy.operands())
126  {
127  abstract_object_pointert op_abstract_object = environment.eval(op, ns);
128  const exprt &const_op = op_abstract_object->to_constant();
129 
130  if(const_op.is_nil())
131  {
132  return environment.abstract_object_factory(copy.type(), ns, true, false);
133  }
134  }
135 
136  return environment.abstract_object_factory(copy.type(), copy, ns);
137 }
138 
140  abstract_environmentt &environment,
141  const namespacet &ns,
142  const std::stack<exprt> &stack,
143  const exprt &specifier,
144  const abstract_object_pointert &value,
145  bool merging_write) const
146 {
147  return environment.abstract_object_factory(type(), ns, true, false);
148 }
149 
151 {
152  return top;
153 }
154 
156 {
157  return bottom;
158 }
159 
161 {
162  return !(top && bottom);
163 }
164 
166 {
167  return nil_exprt();
168 }
169 
171  std::ostream &out,
172  const ai_baset &ai,
173  const namespacet &ns) const
174 {
175  if(top)
176  {
177  out << "TOP";
178  }
179  else if(bottom)
180  {
181  out << "BOTTOM";
182  }
183  else
184  {
185  out << "Unknown";
186  }
187 }
188 
192  bool &out_modifications)
193 {
194  abstract_object_pointert result = op1->should_use_base_merge(op2)
195  ? op1->abstract_object_merge(op2)
196  : op1->merge(op2);
197  // If no modifications, we will return the original pointer
198  out_modifications = result != op1;
199 
200  return result;
201 }
202 
206 {
207  bool dummy;
208  return merge(op1, op2, dummy);
209 }
210 
212  const abstract_object_pointert other) const
213 {
214  return is_top() || other->is_bottom() || other->is_top();
215 }
216 
220  bool &out_modifications)
221 {
222  abstract_object_pointert result = op1->should_use_base_meet(op2)
223  ? op1->abstract_object_meet(op2)
224  : op1->meet(op2);
225  // If no modifications, we will return the original pointer
226  out_modifications = result != op1;
227 
228  return result;
229 }
230 
232  const abstract_object_pointert &other) const
233 {
234  return is_bottom() || other->is_bottom() || other->is_top();
235 }
236 
238  const locationst &locations,
239  const bool update_sub_elements) const
240 {
241  return shared_from_this();
242 }
243 
245  std::ostream out,
247 {
248  shared_mapt::viewt view;
249  m.get_view(view);
250 
251  out << "{";
252  bool first = true;
253  for(auto &item : view)
254  {
255  out << (first ? "" : ", ") << item.first;
256  first = false;
257  }
258  out << "}";
259 }
260 
262  std::ostream out,
265 {
266  shared_mapt::delta_viewt delta_view;
267  m1.get_delta_view(m2, delta_view, false);
268 
269  out << "DELTA{";
270  bool first = true;
271  for(auto &item : delta_view)
272  {
273  out << (first ? "" : ", ") << item.k << "=" << item.is_in_both_maps();
274  first = false;
275  }
276  out << "}";
277 }
278 
280 {
281  return shared_from_this();
282 }
283 
285  abstract_object_statisticst &statistics,
286  abstract_object_visitedt &visited,
287  const abstract_environmentt &env,
288  const namespacet &ns) const
289 {
290  const auto &this_ptr = shared_from_this();
291  PRECONDITION(visited.find(this_ptr) == visited.end());
292  visited.insert(this_ptr);
293 }
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
Symbolic Execution.
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
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 exprt to_constant() const
Converts to a constant expression if possible.
static abstract_object_pointert meet(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Interface method for the meet operation.
abstract_objectt(const typet &type)
virtual bool is_top() const
Find out if the abstract object is top.
static void dump_map(std::ostream out, const shared_mapt &m)
virtual bool verify() const
Verify the internal structure of an abstract_object is correct.
virtual 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
A helper function to evaluate writing to a component of an abstract object.
virtual bool is_bottom() const
Find out if the abstract object is bottom.
virtual internal_abstract_object_pointert mutable_clone() const
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.
bool should_use_base_meet(const abstract_object_pointert &other) const
Helper function to decide if base meet implementation should be used.
virtual abstract_object_pointert abstract_object_meet_internal(const abstract_object_pointert &other) const
Helper function for base meet, in case additional work was needed.
static void dump_map_diff(std::ostream out, const shared_mapt &m1, const shared_mapt &m2)
Dump all elements in m1 that are different or missing in m2.
abstract_object_pointert abstract_object_merge(const abstract_object_pointert other) const
Create a new abstract object that is the result of the merge, unless the object would be unchanged,...
virtual abstract_object_pointert update_location_context(const locationst &locations, const bool update_sub_elements) const
Update the location context for an abstract object, potentially propogating the update to any childre...
bool should_use_base_merge(const abstract_object_pointert other) const
To detect the cases where the base merge is sufficient to do a merge We can't do if this->is_bottom()...
abstract_object_pointert abstract_object_meet(const abstract_object_pointert &other) const
Helper function for base meet.
virtual void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print the value of the abstract object.
virtual abstract_object_pointert abstract_object_merge_internal(const abstract_object_pointert other) const
Helper function for abstract_objectt::abstract_object_merge to perform any additional actions after t...
internal_sharing_ptrt< class abstract_objectt > internal_abstract_object_pointert
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 abstract_object_pointert unwrap_context() const
std::set< goto_programt::const_targett > locationst
typet t
To enforce copy-on-write these are private and have read-only accessors.
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.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
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
bool is_nil() const
Definition: irep.h:387
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
The NIL expression.
Definition: std_expr.h:2735
std::vector< view_itemt > viewt
View of the key-value pairs in the map.
Definition: sharing_map.h:388
std::vector< delta_view_itemt > delta_viewt
Delta view of the key-value pairs in two maps.
Definition: sharing_map.h:439
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
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...
The type of an expression, extends irept.
Definition: type.h:28
An abstraction of a single value that just stores a constant.
bool simplify(exprt &expr, const namespacet &ns)
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
API to expression classes.
Defines typet, type_with_subtypet and type_with_subtypest.