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 &_ns,
23 propt &_prop,
25 bool get_array_constraints = false);
26
27 void finish_eager_conversion() override;
28
29 std::size_t boolbv_width(const typet &type) const override
30 {
31 return bv_pointers_width(type);
32 }
33
35 endianness_map(const typet &type, bool little_endian) const override;
36
37protected:
39
41 {
42 public:
43 explicit bv_pointers_widtht(const namespacet &_ns) : boolbv_widtht(_ns)
44 {
45 }
46
47 std::size_t operator()(const typet &type) const override;
48
49 std::size_t get_object_width(const pointer_typet &type) const;
50 std::size_t get_offset_width(const pointer_typet &type) const;
51 std::size_t get_address_width(const pointer_typet &type) const;
52 };
54
55 // NOLINTNEXTLINE(readability/identifiers)
56 typedef boolbvt SUB;
57
59 bvt encode(std::size_t object, const pointer_typet &type) const;
60
61 virtual bvt convert_pointer_type(const exprt &expr);
62
64 virtual bvt add_addr(const exprt &expr);
65
66 // overloading
67 literalt convert_rest(const exprt &expr) override;
68 bvt convert_bitvector(const exprt &expr) override; // no cache
69
71 const exprt &expr,
72 const bvt &bv,
73 std::size_t offset,
74 const typet &type) const override;
75
78
81 const pointer_typet &type,
82 const bvt &bv,
83 const mp_integer &x);
86 const pointer_typet &type,
87 const bvt &bv,
88 const mp_integer &factor,
89 const exprt &index);
92 const pointer_typet &type,
93 const bvt &bv,
94 const mp_integer &factor,
95 const bvt &index_bv);
96
98 {
101
102 postponedt(bvt _bv, bvt _op, exprt _expr)
103 : bv(std::move(_bv)), op(std::move(_op)), expr(std::move(_expr))
104 {
105 }
106 };
107
108 typedef std::list<postponedt> postponed_listt;
110
111 void do_postponed(const postponedt &postponed);
112
118 bvt object_literals(const bvt &bv, const pointer_typet &type) const
119 {
120 const std::size_t offset_width = bv_pointers_width.get_offset_width(type);
121 const std::size_t object_width = bv_pointers_width.get_object_width(type);
122 PRECONDITION(bv.size() >= offset_width + object_width);
123
124 return bvt(
125 bv.begin() + offset_width, bv.begin() + offset_width + object_width);
126 }
127
133 bvt offset_literals(const bvt &bv, const pointer_typet &type) const
134 {
135 const std::size_t offset_width = bv_pointers_width.get_offset_width(type);
136 PRECONDITION(bv.size() >= offset_width);
137
138 return bvt(bv.begin(), bv.begin() + offset_width);
139 }
140
146 static bvt object_offset_encoding(const bvt &object, const bvt &offset)
147 {
148 bvt result;
149 result.reserve(offset.size() + object.size());
150 result.insert(result.end(), offset.begin(), offset.end());
151 result.insert(result.end(), object.begin(), object.end());
152
153 return result;
154 }
155};
156
157#endif // CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
message_handlert & message_handler
Definition: arrays.h:58
bool get_array_constraints
Definition: arrays.h:113
Definition: boolbv.h:44
bv_pointers_widtht(const namespacet &_ns)
Definition: bv_pointers.h:43
std::size_t get_object_width(const pointer_typet &type) const
Definition: bv_pointers.cpp:94
std::size_t get_address_width(const pointer_typet &type) const
std::size_t get_offset_width(const pointer_typet &type) const
static bvt object_offset_encoding(const bvt &object, const bvt &offset)
Construct a pointer encoding from given encodings of object and offset.
Definition: bv_pointers.h:146
bv_pointers_widtht bv_pointers_width
Definition: bv_pointers.h:53
void do_postponed(const postponedt &postponed)
literalt convert_rest(const exprt &expr) override
pointer_logict pointer_logic
Definition: bv_pointers.h:38
NODISCARD bvt encode(std::size_t object, const pointer_typet &type) const
virtual NODISCARD bvt add_addr(const exprt &expr)
virtual bvt convert_pointer_type(const exprt &expr)
postponed_listt postponed_list
Definition: bv_pointers.h:109
endianness_mapt endianness_map(const typet &type, bool little_endian) const override
Definition: bv_pointers.cpp:68
NODISCARD bvt offset_arithmetic(const pointer_typet &type, const bvt &bv, const mp_integer &x)
boolbvt SUB
Definition: bv_pointers.h:56
void finish_eager_conversion() override
exprt bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset, const typet &type) const override
NODISCARD optionalt< bvt > convert_address_of_rec(const exprt &expr)
std::list< postponedt > postponed_listt
Definition: bv_pointers.h:108
std::size_t boolbv_width(const typet &type) const override
Definition: bv_pointers.h:29
bvt convert_bitvector(const exprt &expr) 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...
Definition: bv_pointers.h:118
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...
Definition: bv_pointers.h:133
resultt operator()()
Run the decision procedure to solve the problem.
Maps a big-endian offset to a little-endian offset.
Base class for all expressions.
Definition: expr.h:54
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 ...
Definition: pointer_expr.h:24
TO_BE_DOCUMENTED.
Definition: prop.h:24
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
nonstd::optional< T > optionalt
Definition: optional.h:35
Pointer Logic.
BigInt mp_integer
Definition: smt_terms.h:12
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
postponedt(bvt _bv, bvt _op, exprt _expr)
Definition: bv_pointers.h:102