cprover
Loading...
Searching...
No Matches
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 <iostream>
10
12
14#include <util/simplify_expr.h>
15#include <util/std_expr.h>
16
17#include "abstract_object.h"
18
20 : t(type), bottom(false), top(true)
21{
22}
23
24abstract_objectt::abstract_objectt(const typet &type, bool top, bool bottom)
25 : t(type), bottom(bottom), top(top)
26{
27 PRECONDITION(!(top && bottom));
28}
29
31 const exprt &expr,
32 const abstract_environmentt &environment,
33 const namespacet &ns)
34 : t(expr.type()), bottom(false), top(true)
35{
36}
37
39 const typet &type,
40 const exprt &expr,
41 const abstract_environmentt &environment,
42 const namespacet &ns)
43 : t(type), bottom(false), top(true)
44{
45}
46
48{
49 return t;
50}
51
53 const abstract_object_pointert &other,
54 const widen_modet &widen_mode) const
55{
56 return abstract_object_merge(other);
57}
58
60 const abstract_object_pointert &other) const
61{
62 if(is_top() || other->bottom)
63 return this->abstract_object_merge_internal(other);
64
66 merged->set_top();
67 merged->bottom = false;
68 return merged->abstract_object_merge_internal(other);
69}
70
72 const abstract_object_pointert &other) const
73{
74 // Default implementation
75 return shared_from_this();
76}
77
80{
81 return abstract_object_meet(other);
82}
83
85 const abstract_object_pointert &other) const
86{
87 if(is_top())
88 return other;
89
90 if(is_bottom() || other->top)
91 return this->abstract_object_meet_internal(other);
92
94 met->bottom = true;
95 met->top = false;
96 return met->abstract_object_meet_internal(other);
97}
98
100 const abstract_object_pointert &other) const
101{
102 // Default implementation
103 return shared_from_this();
104}
105
106static bool is_pointer_addition(const exprt &expr)
107{
108 return (expr.id() == ID_plus) && (expr.type().id() == ID_pointer) &&
109 (expr.operands().size() == 2) && is_number(expr.operands()[1].type());
110}
111
113 const exprt &expr,
114 const std::vector<abstract_object_pointert> &operands,
115 const abstract_environmentt &environment,
116 const namespacet &ns) const
117{
118 exprt copy = expr;
119
120 for(exprt &op : copy.operands())
121 {
122 abstract_object_pointert op_abstract_object = environment.eval(op, ns);
123 const exprt &const_op = op_abstract_object->to_constant();
124 op = const_op.is_nil() ? op : const_op;
125 }
126
127 if(!is_pointer_addition(copy))
128 copy = simplify_expr(copy, ns);
129
130 for(const exprt &op : copy.operands())
131 {
132 abstract_object_pointert op_abstract_object = environment.eval(op, ns);
133 const exprt &const_op = op_abstract_object->to_constant();
134
135 if(const_op.is_nil())
136 {
137 return environment.abstract_object_factory(copy.type(), ns, true, false);
138 }
139 }
140
141 return environment.abstract_object_factory(copy.type(), copy, ns);
142}
143
145 abstract_environmentt &environment,
146 const namespacet &ns,
147 const std::stack<exprt> &stack,
148 const exprt &specifier,
149 const abstract_object_pointert &value,
150 bool merging_write) const
151{
152 return environment.abstract_object_factory(type(), ns, true, false);
153}
154
156{
157 return top;
158}
159
161{
162 return bottom;
163}
164
166{
167 return !(top && bottom);
168}
169
171{
172 return nil_exprt();
173}
174
176{
177 if(is_top())
178 return true_exprt();
179 if(is_bottom())
180 return false_exprt();
181 return to_predicate_internal(name);
182}
183
185{
187 return nil_exprt();
188}
189
191 std::ostream &out,
192 const ai_baset &ai,
193 const namespacet &ns) const
194{
195 if(top)
196 {
197 out << "TOP";
198 }
199 else if(bottom)
200 {
201 out << "BOTTOM";
202 }
203 else
204 {
205 out << "Unknown";
206 }
207}
208
210 const abstract_object_pointert &op1,
211 const abstract_object_pointert &op2,
212 const locationt &merge_location,
213 const widen_modet &widen_mode)
214{
215 abstract_object_pointert result = merge(op1, op2, widen_mode).object;
216 result = result->merge_location_context(merge_location);
217
218 // If no modifications, we will return the original pointer
219 return {result, result != op1};
220}
221
223 const abstract_object_pointert &op1,
224 const abstract_object_pointert &op2,
225 const widen_modet &widen_mode)
226{
227 abstract_object_pointert result = op1->should_use_base_merge(op2)
228 ? op1->abstract_object_merge(op2)
229 : op1->merge(op2, widen_mode);
230
231 // If no modifications, we will return the original pointer
232 return {result, result != op1};
233}
234
236 const abstract_object_pointert &other) const
237{
238 return is_top() || other->is_bottom() || other->is_top();
239}
240
242 const abstract_object_pointert &op1,
243 const abstract_object_pointert &op2)
244{
245 abstract_object_pointert result = op1->should_use_base_meet(op2)
246 ? op1->abstract_object_meet(op2)
247 : op1->meet(op2);
248 // If no modifications, we will return the original pointer
249 return {result, result != op1};
250}
251
253 const abstract_object_pointert &other) const
254{
255 return is_bottom() || is_top() || other->is_bottom() || other->is_top();
256}
257
260{
261 return shared_from_this();
262}
263
266{
267 return shared_from_this();
268}
269
271 std::ostream out,
273{
275 m.get_view(view);
276
277 out << "{";
278 bool first = true;
279 for(auto &item : view)
280 {
281 out << (first ? "" : ", ") << item.first;
282 first = false;
283 }
284 out << "}";
285}
286
288 std::ostream out,
291{
292 shared_mapt::delta_viewt delta_view;
293 m1.get_delta_view(m2, delta_view, false);
294
295 out << "DELTA{";
296 bool first = true;
297 for(auto &item : delta_view)
298 {
299 out << (first ? "" : ", ") << item.k << "=" << item.is_in_both_maps();
300 first = false;
301 }
302 out << "}";
303}
304
306{
307 return shared_from_this();
308}
309
311 abstract_object_statisticst &statistics,
313 const abstract_environmentt &env,
314 const namespacet &ns) const
315{
316 const auto &this_ptr = shared_from_this();
317 PRECONDITION(visited.find(this_ptr) == visited.end());
318 visited.insert(this_ptr);
319}
An abstract version of a program environment.
static bool is_pointer_addition(const exprt &expr)
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
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.
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 write_location_context(const locationt &location) const
Update the write location context for an abstract object.
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.
virtual exprt to_predicate_internal(const exprt &name) const
to_predicate implementation - derived classes will override
goto_programt::const_targett locationt
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.
exprt to_predicate(const exprt &name) const
Converts to an invariant expression.
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_meet(const abstract_object_pointert &other) const
Helper function for base meet.
static combine_result merge(const abstract_object_pointert &op1, const abstract_object_pointert &op2, const locationt &merge_location, const widen_modet &widen_mode)
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()...
virtual void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print the value of the abstract object.
static combine_result meet(const abstract_object_pointert &op1, const abstract_object_pointert &op2)
Interface method for the meet operation.
virtual abstract_object_pointert merge_location_context(const locationt &location) const
Update the merge location context for an abstract object.
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 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
virtual abstract_object_pointert unwrap_context() const
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:119
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:92
The Boolean constant false.
Definition: std_expr.h:2865
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The NIL expression.
Definition: std_expr.h:2874
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:939
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 Boolean constant true.
Definition: std_expr.h:2856
The type of an expression, extends irept.
Definition: type.h:29
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
Mathematical types.
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.
Clones the first parameter and merges it with the second.
abstract_object_pointert object