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
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 {
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 {
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,
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{
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
309
311 abstract_object_statisticst &statistics,
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...
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
virtual bool merge(const statet &src, trace_ptrt from, trace_ptrt to)
Merge the state src, flowing from tracet from to tracet to, into the state currently stored for trace...
Definition ai.h:500
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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
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.
std::vector< delta_view_itemt > delta_viewt
Delta view of the key-value pairs in two maps.
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.