CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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
19abstract_objectt::abstract_objectt(const typet &type, bool top, bool bottom)
20 : t(type), bottom(bottom), top(top)
21{
22 PRECONDITION(!(top && bottom));
23}
24
26 const exprt &expr,
27 const abstract_environmentt &environment,
28 const namespacet &ns)
29 : t(expr.type()), bottom(false), top(true)
30{
31}
32
34{
35 return t;
36}
37
44
46 const abstract_object_pointert &other) const
47{
48 if(is_top() || other->bottom)
49 return this->abstract_object_merge_internal(other);
50
52 merged->set_top();
53 merged->bottom = false;
54 return merged->abstract_object_merge_internal(other);
55}
56
58 const abstract_object_pointert &other) const
59{
60 // Default implementation
61 return shared_from_this();
62}
63
66{
67 return abstract_object_meet(other);
68}
69
71 const abstract_object_pointert &other) const
72{
73 if(is_top())
74 return other;
75
76 if(is_bottom() || other->top)
77 return this->abstract_object_meet_internal(other);
78
80 met->bottom = true;
81 met->top = false;
82 return met->abstract_object_meet_internal(other);
83}
84
86 const abstract_object_pointert &other) const
87{
88 // Default implementation
89 return shared_from_this();
90}
91
92static bool is_pointer_addition(const exprt &expr)
93{
94 return (expr.id() == ID_plus) && (expr.type().id() == ID_pointer) &&
95 (expr.operands().size() == 2) && is_number(expr.operands()[1].type());
96}
97
99 const exprt &expr,
100 const std::vector<abstract_object_pointert> &operands,
101 const abstract_environmentt &environment,
102 const namespacet &ns) const
103{
104 exprt copy = expr;
105
106 for(exprt &op : copy.operands())
107 {
109 const exprt &const_op = op_abstract_object->to_constant();
110 op = const_op.is_nil() ? op : const_op;
111 }
112
113 if(!is_pointer_addition(copy))
114 copy = simplify_expr(copy, ns);
115
116 for(const exprt &op : copy.operands())
117 {
119 const exprt &const_op = op_abstract_object->to_constant();
120
121 if(const_op.is_nil())
122 {
123 return environment.abstract_object_factory(copy.type(), ns, true, false);
124 }
125 }
126
127 return environment.abstract_object_factory(copy.type(), copy, ns);
128}
129
131 abstract_environmentt &environment,
132 const namespacet &ns,
133 const std::stack<exprt> &stack,
134 const exprt &specifier,
135 const abstract_object_pointert &value,
136 bool merging_write) const
137{
138 return environment.abstract_object_factory(type(), ns, true, false);
139}
140
142{
143 return top;
144}
145
147{
148 return bottom;
149}
150
152{
153 return !(top && bottom);
154}
155
157{
158 return nil_exprt();
159}
160
162{
163 if(is_top())
164 return true_exprt();
165 if(is_bottom())
166 return false_exprt();
167 return to_predicate_internal(name);
168}
169
171{
173 return nil_exprt();
174}
175
177 std::ostream &out,
178 const ai_baset &ai,
179 const namespacet &ns) const
180{
181 if(top)
182 {
183 out << "TOP";
184 }
185 else if(bottom)
186 {
187 out << "BOTTOM";
188 }
189 else
190 {
191 out << "Unknown";
192 }
193}
194
196 const abstract_object_pointert &op1,
197 const abstract_object_pointert &op2,
199 const widen_modet &widen_mode)
200{
201 abstract_object_pointert result = merge(op1, op2, widen_mode).object;
202 result = result->merge_location_context(merge_location);
203
204 // If no modifications, we will return the original pointer
205 return {result, result != op1};
206}
207
209 const abstract_object_pointert &op1,
210 const abstract_object_pointert &op2,
211 const widen_modet &widen_mode)
212{
213 abstract_object_pointert result = op1->should_use_base_merge(op2)
214 ? op1->abstract_object_merge(op2)
215 : op1->merge(op2, widen_mode);
216
217 // If no modifications, we will return the original pointer
218 return {result, result != op1};
219}
220
222 const abstract_object_pointert &other) const
223{
224 return is_top() || other->is_bottom() || other->is_top();
225}
226
228 const abstract_object_pointert &op1,
229 const abstract_object_pointert &op2)
230{
231 abstract_object_pointert result = op1->should_use_base_meet(op2)
232 ? op1->abstract_object_meet(op2)
233 : op1->meet(op2);
234 // If no modifications, we will return the original pointer
235 return {result, result != op1};
236}
237
239 const abstract_object_pointert &other) const
240{
241 return is_bottom() || is_top() || other->is_bottom() || other->is_top();
242}
243
246{
247 return shared_from_this();
248}
249
252{
253 return shared_from_this();
254}
255
257 std::ostream out,
259{
261 m.get_view(view);
262
263 out << "{";
264 bool first = true;
265 for(auto &item : view)
266 {
267 out << (first ? "" : ", ") << item.first;
268 first = false;
269 }
270 out << "}";
271}
272
274 std::ostream out,
277{
279 m1.get_delta_view(m2, delta_view, false);
280
281 out << "DELTA{";
282 bool first = true;
283 for(auto &item : delta_view)
284 {
285 out << (first ? "" : ", ") << item.k << "=" << item.is_in_both_maps();
286 first = false;
287 }
288 out << "}";
289}
290
295
297 abstract_object_statisticst &statistics,
300 const namespacet &ns) const
301{
302 const auto &this_ptr = shared_from_this();
303 PRECONDITION(visited.find(this_ptr) == visited.end());
304 visited.insert(this_ptr);
305}
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.
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.
abstract_objectt(const typet &type, bool top, bool bottom)
Start the abstract object at either top or bottom or neither Asserts if both top and bottom are true.
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:117
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:498
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
The Boolean constant false.
Definition std_expr.h:3199
const irep_idt & id() const
Definition irep.h:388
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:3208
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:3190
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:525
#define PRECONDITION(CONDITION)
Definition invariant.h:463
API to expression classes.
Clones the first parameter and merges it with the second.