cprover
Loading...
Searching...
No Matches
abstract_object.h
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
25
26#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_OBJECT_H
27#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_OBJECT_H
28
29#include <memory>
30#include <set>
31#include <stack>
32
34#include <util/sharing_map.h>
35
37class namespacet;
39enum class widen_modet;
40
41#define CLONE \
42 internal_abstract_object_pointert mutable_clone() const override \
43 { \
44 typedef std::remove_const< \
45 std::remove_reference<decltype(*this)>::type>::type current_typet; \
46 return internal_abstract_object_pointert(new current_typet(*this)); \
47 }
48
65
66template <class T>
67using sharing_ptrt = std::shared_ptr<const T>; // NOLINT(*)
68
70using abstract_object_visitedt = std::set<abstract_object_pointert>;
71
72class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
73{
74public:
76 explicit abstract_objectt(const typet &type);
77
84 abstract_objectt(const typet &type, bool top, bool bottom);
85
94 const exprt &expr,
95 const abstract_environmentt &environment,
96 const namespacet &ns);
97
106 const typet &type,
107 const exprt &expr,
108 const abstract_environmentt &environment,
109 const namespacet &ns);
110
112 {
113 }
114
118 virtual const typet &type() const;
119
124 virtual bool is_top() const;
125
129 virtual bool is_bottom() const;
130
134 virtual bool verify() const;
135
136 virtual void get_statistics(
137 abstract_object_statisticst &statistics,
139 const abstract_environmentt &env,
140 const namespacet &ns) const;
141
158 const exprt &expr,
159 const std::vector<abstract_object_pointert> &operands,
160 const abstract_environmentt &environment,
161 const namespacet &ns) const;
162
172 virtual exprt to_constant() const;
173
183 exprt to_predicate(const exprt &name) const;
184
202 abstract_environmentt &environment,
203 const namespacet &ns,
204 const std::stack<exprt> &stack,
205 const exprt &specifier,
206 const abstract_object_pointert &value,
207 bool merging_write) const;
208
215 virtual void output(
216 std::ostream &out,
217 const class ai_baset &ai,
218 const namespacet &ns) const;
219
223
224 static void dump_map(std::ostream out, const shared_mapt &m);
232 static void
233 dump_map_diff(std::ostream out, const shared_mapt &m1, const shared_mapt &m2);
234
243 virtual bool has_been_modified(const abstract_object_pointert &before) const
244 {
248 return this != before.get();
249 };
250
263 {
266 };
267 static combine_result merge(
268 const abstract_object_pointert &op1,
269 const abstract_object_pointert &op2,
270 const locationt &merge_location,
271 const widen_modet &widen_mode);
272 static combine_result merge(
273 const abstract_object_pointert &op1,
274 const abstract_object_pointert &op2,
275 const widen_modet &widen_mode);
276
284 static combine_result meet(
285 const abstract_object_pointert &op1,
286 const abstract_object_pointert &op2);
287
294 meet(const abstract_object_pointert &other) const;
295
305 write_location_context(const locationt &location) const;
306
316 merge_location_context(const locationt &location) const;
317
318 // Const versions must perform copy-on-write
320 {
321 if(is_top())
322 return shared_from_this();
323
325 clone->set_top();
326 return clone;
327 }
328
330 {
331 if(!is_top())
332 return shared_from_this();
333
335 clone->set_not_top();
336 return clone;
337 }
338
340
346 {
348 visit(const abstract_object_pointert &element) const = 0;
349 };
350
364 {
365 return shared_from_this();
366 }
367
368 virtual size_t internal_hash() const
369 {
370 return std::hash<abstract_object_pointert>{}(shared_from_this());
371 }
372
373 virtual bool internal_equality(const abstract_object_pointert &other) const
374 {
375 return shared_from_this() == other;
376 }
377
381 virtual exprt to_predicate_internal(const exprt &name) const;
382
383private:
386 bool bottom;
387 bool top;
388
389 // Hooks to allow a sub-class to perform its own operations on
390 // setting/clearing top
391 virtual void set_top_internal()
392 {
393 }
394 virtual void set_not_top_internal()
395 {
396 }
397
412
419
420protected:
421 template <class T>
422 using internal_sharing_ptrt = std::shared_ptr<T>;
423
426
427 // Macro is not used as this does not override
429 {
431 }
432
441
449 bool should_use_base_merge(const abstract_object_pointert &other) const;
450
459 const abstract_object_pointert &other,
460 const widen_modet &widen_mode) const;
461
468
473 bool should_use_base_meet(const abstract_object_pointert &other) const;
474
475 // The one exception is merge in descendant classes, which needs this
476 void set_top()
477 {
478 top = true;
479 this->set_top_internal();
480 }
482 {
483 top = false;
484 this->set_not_top_internal();
485 }
487 {
488 bottom = false;
489 }
490};
491
493{
495 typedef std::size_t result_typet;
496 result_typet operator()(argument_typet const &s) const noexcept
497 {
498 return s->internal_hash();
499 }
500};
501
503{
505 typedef std::size_t result_typet;
506 bool operator()(argument_typet const &left, argument_typet const &right) const
507 noexcept
508 {
509 return left->internal_equality(right);
510 }
511};
512
513#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_OBJECT_H
std::shared_ptr< const T > sharing_ptrt
Merge is designed to allow different abstractions to be merged gracefully.
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
virtual bool internal_equality(const abstract_object_pointert &other) const
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 void set_not_top_internal()
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 void set_top_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.
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.
std::shared_ptr< T > internal_sharing_ptrt
abstract_object_pointert make_top() const
virtual size_t internal_hash() const
virtual abstract_object_pointert visit_sub_elements(const abstract_object_visitort &visitor) const
Apply a visitor operation to all sub elements of this abstract_object.
abstract_object_pointert abstract_object_meet(const abstract_object_pointert &other) const
Helper function for base meet.
abstract_object_pointert clear_top() const
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
sharing_mapt< irep_idt, abstract_object_pointert, false, irep_id_hash > shared_mapt
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 ~abstract_objectt()
virtual bool has_been_modified(const abstract_object_pointert &before) const
Determine whether 'this' abstract_object has been modified in comparison to a previous 'before' state...
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
instructionst::const_iterator const_targett
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
A map implemented as a tree where subtrees can be shared between different maps.
The type of an expression, extends irept.
Definition type.h:29
Concrete Goto Program.
Sharing map.
abstract_object_pointert argument_typet
std::size_t result_typet
bool operator()(argument_typet const &left, argument_typet const &right) const noexcept
abstract_object_pointert argument_typet
std::size_t result_typet
result_typet operator()(argument_typet const &s) const noexcept
Pure virtual interface required of a client that can apply a copy-on-write operation to a given abstr...
virtual abstract_object_pointert visit(const abstract_object_pointert &element) const =0
Clones the first parameter and merges it with the second.
abstract_object_pointert object