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 }
abstract_objectt::dump_map
static void dump_map(std::ostream out, const shared_mapt &m)
Definition: abstract_object.cpp:244
sharing_mapt< irep_idt, abstract_object_pointert, false, irep_id_hash >::delta_viewt
std::vector< delta_view_itemt > delta_viewt
Delta view of the key-value pairs in two maps.
Definition: sharing_map.h:439
abstract_objectt::abstract_object_meet_internal
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.
Definition: abstract_object.cpp:101
sharing_mapt::get_delta_view
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
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:75
abstract_objectt::is_top
virtual bool is_top() const
Find out if the abstract object is top.
Definition: abstract_object.cpp:150
abstract_objectt::merge
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.
Definition: abstract_object.cpp:189
abstract_objectt::output
virtual void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print the value of the abstract object.
Definition: abstract_object.cpp:170
arith_tools.h
sharing_mapt< irep_idt, abstract_object_pointert, false, irep_id_hash >
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...
abstract_objectt::should_use_base_merge
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()...
Definition: abstract_object.cpp:211
abstract_objectt::type
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
Definition: abstract_object.cpp:53
abstract_objectt::should_use_base_meet
bool should_use_base_meet(const abstract_object_pointert &other) const
Helper function to decide if base meet implementation should be used.
Definition: abstract_object.cpp:231
abstract_environmentt
Definition: abstract_environment.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
abstract_objectt::get_statistics
virtual void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const
Definition: abstract_object.cpp:284
abstract_objectt::internal_abstract_object_pointert
internal_sharing_ptrt< class abstract_objectt > internal_abstract_object_pointert
Definition: abstract_object.h:401
namespace.h
abstract_object.h
abstract_objectt is the top of the inheritance heirarchy of objects used to represent individual vari...
type.h
Defines typet, type_with_subtypet and type_with_subtypest.
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
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_object_statisticst
Definition: abstract_object_statistics.h:19
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:251
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
nil_exprt
The NIL expression.
Definition: std_expr.h:2735
abstract_environment.h
An abstract version of a program environment.
abstract_objectt::locationst
std::set< goto_programt::const_targett > locationst
Definition: abstract_object.h:215
abstract_objectt::to_constant
virtual exprt to_constant() const
Converts to a constant expression if possible.
Definition: abstract_object.cpp:165
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2524
abstract_objectt::dump_map_diff
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.
Definition: abstract_object.cpp:261
abstract_environmentt::eval
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
Definition: abstract_environment.cpp:37
irept::is_nil
bool is_nil() const
Definition: irep.h:387
abstract_object_visitedt
std::set< abstract_object_pointert > abstract_object_visitedt
Definition: abstract_object.h:76
abstract_objectt::update_location_context
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...
Definition: abstract_object.cpp:237
abstract_objectt::bottom
bool bottom
Definition: abstract_object.h:362
simplify_expr.h
abstract_objectt::abstract_object_meet
abstract_object_pointert abstract_object_meet(const abstract_object_pointert &other) const
Helper function for base meet.
Definition: abstract_object.cpp:89
abstract_objectt::unwrap_context
virtual abstract_object_pointert unwrap_context() const
Definition: abstract_object.cpp:279
abstract_objectt::abstract_object_merge
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,...
Definition: abstract_object.cpp:64
ieee_float.h
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
abstract_objectt::verify
virtual bool verify() const
Verify the internal structure of an abstract_object is correct.
Definition: abstract_object.cpp:160
abstract_objectt::write
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.
Definition: abstract_object.cpp:139
abstract_objectt::meet
static abstract_object_pointert meet(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Interface method for the meet operation.
Definition: abstract_object.cpp:217
exprt::operands
operandst & operands()
Definition: expr.h:96
abstract_objectt::top
bool top
Definition: abstract_object.h:363
abstract_objectt::abstract_object_merge_internal
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...
Definition: abstract_object.cpp:76
abstract_objectt::is_bottom
virtual bool is_bottom() const
Find out if the abstract object is bottom.
Definition: abstract_object.cpp:155
adjust_float_expressions.h
Symbolic Execution.
std_expr.h
API to expression classes.
abstract_objectt::mutable_clone
virtual internal_abstract_object_pointert mutable_clone() const
Definition: abstract_object.h:404
abstract_objectt::t
typet t
To enforce copy-on-write these are private and have read-only accessors.
Definition: abstract_object.h:361
abstract_objectt::expression_transform
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.
Definition: abstract_object.cpp:108
constant_abstract_value.h
An abstraction of a single value that just stores a constant.
abstract_objectt::abstract_objectt
abstract_objectt(const typet &type)
Definition: abstract_object.cpp:25