cprover
Loading...
Searching...
No Matches
bv_pointers.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#ifndef CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
11#define CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
12
13#include <util/nodiscard.h>
14
15#include "boolbv.h"
16#include "pointer_logic.h"
17
19{
20public:
22 const namespacet &,
23 propt &,
25 bool get_array_constraints = false);
26
27 void finish_eager_conversion() override;
28
30 endianness_map(const typet &, bool little_endian) const override;
31
32protected:
34
35 std::size_t get_object_width(const pointer_typet &) const;
36 std::size_t get_offset_width(const pointer_typet &) const;
37 std::size_t get_address_width(const pointer_typet &) const;
38
39 // NOLINTNEXTLINE(readability/identifiers)
40 typedef boolbvt SUB;
41
43 bvt encode(const mp_integer &object, const pointer_typet &) const;
44
45 virtual bvt convert_pointer_type(const exprt &);
46
48 virtual bvt add_addr(const exprt &);
49
50 // overloading
51 literalt convert_rest(const exprt &) override;
52 bvt convert_bitvector(const exprt &) override; // no cache
53
54 exprt
55 bv_get_rec(const exprt &, const bvt &, std::size_t offset) const override;
56
59
61 bvt offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &);
64 const pointer_typet &,
65 const bvt &,
66 const mp_integer &factor,
67 const exprt &index);
70 const pointer_typet &type,
71 const bvt &bv,
72 const exprt &factor,
73 const exprt &index);
76 const pointer_typet &,
77 const bvt &,
78 const mp_integer &factor,
79 const bvt &index_bv);
80
82 {
85
87 : bv(std::move(_bv)), op(std::move(_op)), expr(std::move(_expr))
88 {
89 }
90 };
91
92 typedef std::list<postponedt> postponed_listt;
94
96
102 bvt object_literals(const bvt &bv, const pointer_typet &type) const;
103
109 bvt offset_literals(const bvt &bv, const pointer_typet &type) const;
110
116 static bvt object_offset_encoding(const bvt &object, const bvt &offset);
117};
118
119#endif // CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
bool get_array_constraints
Definition arrays.h:113
std::size_t get_object_width(const pointer_typet &) const
void do_postponed(const postponedt &postponed)
NODISCARD optionalt< bvt > convert_address_of_rec(const exprt &)
pointer_logict pointer_logic
Definition bv_pointers.h:33
NODISCARD bvt offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &)
postponed_listt postponed_list
Definition bv_pointers.h:93
std::size_t get_address_width(const pointer_typet &) const
virtual NODISCARD bvt add_addr(const exprt &)
endianness_mapt endianness_map(const typet &, bool little_endian) const override
boolbvt SUB
Definition bv_pointers.h:40
void finish_eager_conversion() override
exprt bv_get_rec(const exprt &, const bvt &, std::size_t offset) const override
static bvt object_offset_encoding(const bvt &object, const bvt &offset)
Construct a pointer encoding from given encodings of object and offset.
NODISCARD bvt encode(const mp_integer &object, const pointer_typet &) const
std::list< postponedt > postponed_listt
Definition bv_pointers.h:92
std::size_t get_offset_width(const pointer_typet &) const
literalt convert_rest(const exprt &) override
bv_pointerst(const namespacet &, propt &, message_handlert &, bool get_array_constraints=false)
bvt convert_bitvector(const exprt &) override
Converts an expression into its gate-level representation and returns a vector of literals correspond...
bvt object_literals(const bvt &bv, const pointer_typet &type) const
Given a pointer encoded in bv, extract the literals identifying the object that the pointer points to...
bvt offset_literals(const bvt &bv, const pointer_typet &type) const
Given a pointer encoded in bv, extract the literals representing the offset into an object that the p...
virtual bvt convert_pointer_type(const exprt &)
Maps a big-endian offset to a little-endian offset.
Base class for all expressions.
Definition expr.h:56
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
TO_BE_DOCUMENTED.
Definition prop.h:25
The type of an expression, extends irept.
Definition type.h:29
std::vector< literalt > bvt
Definition literal.h:201
STL namespace.
#define NODISCARD
Definition nodiscard.h:22
Pointer Logic.
postponedt(bvt _bv, bvt _op, exprt _expr)
Definition bv_pointers.h:86