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
Definition: goto_program.h:593
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.
Definition: sharing_map.h:190
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