cprover
bv_pointers.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: 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 
18 class bv_pointerst:public boolbvt
19 {
20 public:
22  const namespacet &_ns,
23  propt &_prop,
25  bool get_array_constraints = false);
26 
27  void post_process() 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 
37 protected:
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 
58  NODISCARD
59  bvt encode(std::size_t object, const pointer_typet &type) const;
60 
61  virtual bvt convert_pointer_type(const exprt &expr);
62 
63  NODISCARD
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 
76  NODISCARD
78 
79  NODISCARD
81  const pointer_typet &type,
82  const bvt &bv,
83  const mp_integer &x);
84  NODISCARD
86  const pointer_typet &type,
87  const bvt &bv,
88  const mp_integer &factor,
89  const exprt &index);
90  NODISCARD
92  const pointer_typet &type,
93  const bvt &bv,
94  const mp_integer &factor,
95  const bvt &index_bv);
96 
97  struct postponedt
98  {
99  bvt bv, op;
101  };
102 
103  typedef std::list<postponedt> postponed_listt;
105 
106  void do_postponed(const postponedt &postponed);
107 
113  bvt object_literals(const bvt &bv, const pointer_typet &type) const
114  {
115  const std::size_t offset_width = bv_pointers_width.get_offset_width(type);
116  const std::size_t object_width = bv_pointers_width.get_object_width(type);
117  PRECONDITION(bv.size() >= offset_width + object_width);
118 
119  return bvt(
120  bv.begin() + offset_width, bv.begin() + offset_width + object_width);
121  }
122 
128  bvt offset_literals(const bvt &bv, const pointer_typet &type) const
129  {
130  const std::size_t offset_width = bv_pointers_width.get_offset_width(type);
131  PRECONDITION(bv.size() >= offset_width);
132 
133  return bvt(bv.begin(), bv.begin() + offset_width);
134  }
135 
141  static bvt object_offset_encoding(const bvt &object, const bvt &offset)
142  {
143  bvt result;
144  result.reserve(offset.size() + object.size());
145  result.insert(result.end(), offset.begin(), offset.end());
146  result.insert(result.end(), object.begin(), object.end());
147 
148  return result;
149  }
150 };
151 
152 #endif // CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
message_handlert & message_handler
Definition: arrays.h:56
bool get_array_constraints
Definition: arrays.h:111
Definition: boolbv.h:41
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:93
std::size_t get_address_width(const pointer_typet &type) const
std::size_t get_offset_width(const pointer_typet &type) const
std::size_t operator()(const typet &type) const override
Definition: bv_pointers.cpp:73
bv_pointerst(const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false)
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:141
bv_pointers_widtht bv_pointers_width
Definition: bv_pointers.h:53
void do_postponed(const postponedt &postponed)
void post_process() override
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:104
endianness_mapt endianness_map(const typet &type, bool little_endian) const override
Definition: bv_pointers.cpp:67
NODISCARD bvt offset_arithmetic(const pointer_typet &type, const bvt &bv, const mp_integer &x)
boolbvt SUB
Definition: bv_pointers.h:56
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:103
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:113
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:128
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:92
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1495
TO_BE_DOCUMENTED.
Definition: prop.h:25
The type of an expression, extends irept.
Definition: type.h:28
std::vector< literalt > bvt
Definition: literal.h:201
BigInt mp_integer
Definition: mp_arith.h:19
#define NODISCARD
Definition: nodiscard.h:22
nonstd::optional< T > optionalt
Definition: optional.h:35
Pointer Logic.
#define PRECONDITION(CONDITION)
Definition: invariant.h:464