cprover
Loading...
Searching...
No Matches
bv_pointers_wide.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#ifndef CPROVER_CPROVER_BV_POINTERS_WIDE_H
10#define CPROVER_CPROVER_BV_POINTERS_WIDE_H
11
12#include <util/nodiscard.h>
13#include <util/pointer_expr.h>
14
17
18#include "endianness_map_wide.h"
19
21{
22public:
24 const namespacet &,
25 propt &,
27 bool get_array_constraints = false);
28
29 void finish_eager_conversion() override;
30
31 std::size_t boolbv_width(const typet &type) const override
32 {
33 if(type.id() == ID_pointer)
34 return 2 * to_pointer_type(type).get_width();
35 else
36 return boolbvt::boolbv_width(type);
37 }
38
40 endianness_map(const typet &type, bool little_endian) const override
41 {
42 return endianness_map_widet{type, little_endian, ns};
43 }
44
45protected:
47
48 std::size_t get_object_width(const pointer_typet &) const;
49 std::size_t get_offset_width(const pointer_typet &) const;
50
51 // NOLINTNEXTLINE(readability/identifiers)
52 typedef boolbvt SUB;
53
55 bvt encode(const mp_integer &object, const pointer_typet &) const;
56
57 virtual bvt convert_pointer_type(const exprt &);
58
60 virtual bvt add_addr(const exprt &);
61
62 // overloading
63 literalt convert_rest(const exprt &) override;
64 bvt convert_bitvector(const exprt &) override; // no cache
65
66 exprt
67 bv_get_rec(const exprt &, const bvt &, std::size_t offset) const override;
68
71
73 bvt offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &);
76 const pointer_typet &,
77 const bvt &,
78 const mp_integer &factor,
79 const exprt &index);
82 const pointer_typet &,
83 const bvt &,
84 const mp_integer &factor,
85 const bvt &index_bv);
86
88 {
91
93 : bv(std::move(_bv)), op(std::move(_op)), expr(std::move(_expr))
94 {
95 }
96 };
97
98 typedef std::list<postponedt> postponed_listt;
100
101 void do_postponed(const postponedt &postponed);
102
108 bvt object_literals(const bvt &bv, const pointer_typet &type) const;
109
115 bvt offset_literals(const bvt &bv, const pointer_typet &type) const;
116
122 static bvt object_offset_encoding(const bvt &object, const bvt &offset);
123
126 std::vector<bvt> numbered_pointers;
127};
128
129#endif // CPROVER_CPROVER_BV_POINTERS_WIDE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
const namespacet & ns
Definition arrays.h:56
bool get_array_constraints
Definition arrays.h:113
virtual std::size_t boolbv_width(const typet &type) const
Definition boolbv.h:99
virtual bvt convert_pointer_type(const exprt &)
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...
literalt convert_rest(const exprt &) override
bvt convert_bitvector(const exprt &) override
Converts an expression into its gate-level representation and returns a vector of literals correspond...
std::size_t get_object_width(const pointer_typet &) const
static bvt object_offset_encoding(const bvt &object, const bvt &offset)
Construct a pointer encoding from given encodings of object and offset.
NODISCARD optionalt< bvt > convert_address_of_rec(const exprt &)
NODISCARD bvt encode(const mp_integer &object, const pointer_typet &) const
std::vector< bvt > numbered_pointers
Table that maps a 'pointer number' to its full-width bit-vector.
pointer_logict pointer_logic
postponed_listt postponed_list
NODISCARD bvt offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &)
std::list< postponedt > postponed_listt
endianness_mapt endianness_map(const typet &type, bool little_endian) const override
void do_postponed(const postponedt &postponed)
exprt bv_get_rec(const exprt &, const bvt &, std::size_t offset) const override
virtual NODISCARD bvt add_addr(const exprt &)
void finish_eager_conversion() override
std::size_t get_offset_width(const pointer_typet &) const
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...
std::size_t boolbv_width(const typet &type) const override
Maps a big-endian offset to a little-endian offset.
Base class for all expressions.
Definition expr.h:56
const irep_idt & id() const
Definition irep.h:396
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
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Pointer Logic.
BigInt mp_integer
Definition smt_terms.h:18
postponedt(bvt _bv, bvt _op, exprt _expr)