GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/floatingpoint_literal_symfpu_traits.h Lines: 6 6 100.0 %
Date: 2021-09-08 Branches: 2 4 50.0 %

Line Exec Source
1
/******************************************************************************
2
 * Top contributors (to current version):
3
 *   Aina Niemetz, Martin Brain, Andres Noetzli
4
 *
5
 * This file is part of the cvc5 project.
6
 *
7
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 * in the top-level source directory and their institutional affiliations.
9
 * All rights reserved.  See the file COPYING in the top-level source
10
 * directory for licensing information.
11
 * ****************************************************************************
12
 *
13
 * SymFPU glue code for floating-point values.
14
 *
15
 * !!! This header is only to be included in floating-point literal headers !!!
16
 *
17
 * This is a symfpu literal "back-end".  It allows the library to be used as
18
 * an arbitrary precision floating-point implementation.  This is effectively
19
 * the glue between symfpu's notion of "signed bit-vector" and cvc5's
20
 * BitVector.
21
 */
22
23
#include "cvc5_private.h"
24
25
#ifndef CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H
26
#define CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H
27
28
#include <symfpu/core/unpackedFloat.h>
29
30
#include "util/bitvector.h"
31
#include "util/floatingpoint_size.h"
32
#include "util/roundingmode.h"
33
34
/* -------------------------------------------------------------------------- */
35
36
namespace cvc5 {
37
namespace symfpuLiteral {
38
39
/**
40
 * Forward declaration of wrapper so that traits can be defined early and so
41
 * used in the implementation of wrappedBitVector.
42
 */
43
template <bool T>
44
class wrappedBitVector;
45
46
using Cvc5BitWidth = uint32_t;
47
using Cvc5Prop = bool;
48
using Cvc5RM = ::cvc5::RoundingMode;
49
using Cvc5FPSize = ::cvc5::FloatingPointSize;
50
using Cvc5UnsignedBitVector = wrappedBitVector<false>;
51
using Cvc5SignedBitVector = wrappedBitVector<true>;
52
53
/**
54
 * This is the template parameter for symfpu's templates.
55
 */
56
class traits
57
{
58
 public:
59
  /** The six key types that symfpu uses. */
60
  using bwt = Cvc5BitWidth;           // bit-width type
61
  using prop = Cvc5Prop;              // boolean type
62
  using rm = Cvc5RM;                  // rounding-mode type
63
  using fpt = Cvc5FPSize;             // floating-point format type
64
  using ubv = Cvc5UnsignedBitVector;  // unsigned bit-vector type
65
  using sbv = Cvc5SignedBitVector;    // signed bit-vector type
66
67
  /** Give concrete instances of each rounding mode, mainly for comparisons. */
68
  static rm RNE(void);
69
  static rm RNA(void);
70
  static rm RTP(void);
71
  static rm RTN(void);
72
  static rm RTZ(void);
73
74
  /** The sympfu properties. */
75
  static void precondition(const prop& p);
76
  static void postcondition(const prop& p);
77
  static void invariant(const prop& p);
78
};
79
80
/**
81
 * Type function for mapping between types.
82
 */
83
template <bool T>
84
struct signedToLiteralType;
85
86
template <>
87
struct signedToLiteralType<true>
88
{
89
  using literalType = int32_t;
90
};
91
template <>
92
struct signedToLiteralType<false>
93
{
94
  using literalType = uint32_t;
95
};
96
97
/**
98
 * This extends the interface for cvc5::BitVector for compatibility with symFPU.
99
 * The template parameter distinguishes signed and unsigned bit-vectors, a
100
 * distinction symfpu uses.
101
 */
102
template <bool isSigned>
103
1757268
class wrappedBitVector : public BitVector
104
{
105
 protected:
106
  using literalType = typename signedToLiteralType<isSigned>::literalType;
107
  friend wrappedBitVector<!isSigned>;  // To allow conversion between types
108
109
  friend ::symfpu::ite<Cvc5Prop, wrappedBitVector<isSigned> >;  // For ITE
110
111
 public:
112
  /** Constructors. */
113
703686
  wrappedBitVector(const Cvc5BitWidth w, const uint32_t v) : BitVector(w, v) {}
114
10091
  wrappedBitVector(const Cvc5Prop& p) : BitVector(1, p ? 1U : 0U) {}
115
185191
  wrappedBitVector(const wrappedBitVector<isSigned>& old) : BitVector(old) {}
116
857970
  wrappedBitVector(const BitVector& old) : BitVector(old) {}
117
118
  /** Get the bit-width of this wrapped bit-vector. */
119
351711
  Cvc5BitWidth getWidth(void) const { return getSize(); }
120
121
  /** Create a zero value of given bit-width 'w'. */
122
  static wrappedBitVector<isSigned> one(const Cvc5BitWidth& w);
123
  /** Create a one value of given bit-width 'w'. */
124
  static wrappedBitVector<isSigned> zero(const Cvc5BitWidth& w);
125
  /** Create a ones value (all bits 1) of given bit-width 'w'. */
126
  static wrappedBitVector<isSigned> allOnes(const Cvc5BitWidth& w);
127
  /** Create a maximum signed/unsigned value of given bit-width 'w'. */
128
  static wrappedBitVector<isSigned> maxValue(const Cvc5BitWidth& w);
129
  /** Create a minimum signed/unsigned value of given bit-width 'w'. */
130
  static wrappedBitVector<isSigned> minValue(const Cvc5BitWidth& w);
131
132
  /** Return true if this a bit-vector representing a ones value. */
133
  Cvc5Prop isAllOnes() const;
134
  /** Return true if this a bit-vector representing a zero value. */
135
  Cvc5Prop isAllZeros() const;
136
137
  /** Left shift. */
138
  wrappedBitVector<isSigned> operator<<(
139
      const wrappedBitVector<isSigned>& op) const;
140
  /** Logical (unsigned) and arithmetic (signed) right shift. */
141
  wrappedBitVector<isSigned> operator>>(
142
      const wrappedBitVector<isSigned>& op) const;
143
144
  /**
145
   * Inherited but ...
146
   * *sigh* if we use the inherited version then it will return a
147
   * cvc5::BitVector which can be converted back to a
148
   * wrappedBitVector<isSigned> but isn't done automatically when working
149
   * out types for templates instantiation.  ITE is a particular
150
   * problem as expressions and constants no longer derive the
151
   * same type.  There aren't any good solutions in C++, we could
152
   * use CRTP but Liana wouldn't appreciate that, so the following
153
   * pointless wrapping functions are needed.
154
   */
155
156
  /** Bit-wise or. */
157
  wrappedBitVector<isSigned> operator|(
158
      const wrappedBitVector<isSigned>& op) const;
159
  /** Bit-wise and. */
160
  wrappedBitVector<isSigned> operator&(
161
      const wrappedBitVector<isSigned>& op) const;
162
  /** Bit-vector addition. */
163
  wrappedBitVector<isSigned> operator+(
164
      const wrappedBitVector<isSigned>& op) const;
165
  /** Bit-vector subtraction. */
166
  wrappedBitVector<isSigned> operator-(
167
      const wrappedBitVector<isSigned>& op) const;
168
  /** Bit-vector multiplication. */
169
  wrappedBitVector<isSigned> operator*(
170
      const wrappedBitVector<isSigned>& op) const;
171
  /** Bit-vector signed/unsigned division. */
172
  wrappedBitVector<isSigned> operator/(
173
      const wrappedBitVector<isSigned>& op) const;
174
  /** Bit-vector signed/unsigned remainder. */
175
  wrappedBitVector<isSigned> operator%(
176
      const wrappedBitVector<isSigned>& op) const;
177
  /** Bit-vector negation. */
178
  wrappedBitVector<isSigned> operator-(void) const;
179
  /** Bit-wise not. */
180
  wrappedBitVector<isSigned> operator~(void) const;
181
182
  /** Bit-vector increment. */
183
  wrappedBitVector<isSigned> increment() const;
184
  /** Bit-vector decrement. */
185
  wrappedBitVector<isSigned> decrement() const;
186
  /**
187
   * Bit-vector logical/arithmetic right shift where 'op' extended to the
188
   * bit-width of this wrapped bit-vector.
189
   */
190
  wrappedBitVector<isSigned> signExtendRightShift(
191
      const wrappedBitVector<isSigned>& op) const;
192
193
  /**
194
   * Modular operations.
195
   * Note: No overflow checking so these are the same as other operations.
196
   */
197
  wrappedBitVector<isSigned> modularLeftShift(
198
      const wrappedBitVector<isSigned>& op) const;
199
  wrappedBitVector<isSigned> modularRightShift(
200
      const wrappedBitVector<isSigned>& op) const;
201
  wrappedBitVector<isSigned> modularIncrement() const;
202
  wrappedBitVector<isSigned> modularDecrement() const;
203
  wrappedBitVector<isSigned> modularAdd(
204
      const wrappedBitVector<isSigned>& op) const;
205
  wrappedBitVector<isSigned> modularNegate() const;
206
207
  /** Bit-vector equality. */
208
  Cvc5Prop operator==(const wrappedBitVector<isSigned>& op) const;
209
  /** Bit-vector signed/unsigned less or equal than. */
210
  Cvc5Prop operator<=(const wrappedBitVector<isSigned>& op) const;
211
  /** Bit-vector sign/unsigned greater or equal than. */
212
  Cvc5Prop operator>=(const wrappedBitVector<isSigned>& op) const;
213
  /** Bit-vector signed/unsigned less than. */
214
  Cvc5Prop operator<(const wrappedBitVector<isSigned>& op) const;
215
  /** Bit-vector sign/unsigned greater or equal than. */
216
  Cvc5Prop operator>(const wrappedBitVector<isSigned>& op) const;
217
218
  /** Convert this bit-vector to a signed bit-vector. */
219
  wrappedBitVector<true> toSigned(void) const;
220
  /** Convert this bit-vector to an unsigned bit-vector. */
221
  wrappedBitVector<false> toUnsigned(void) const;
222
223
  /** Bit-vector signed/unsigned (zero) extension. */
224
  wrappedBitVector<isSigned> extend(Cvc5BitWidth extension) const;
225
226
  /**
227
   * Create a "contracted" bit-vector by cutting off the 'reduction' number of
228
   * most significant bits, i.e., by extracting the (bit-width - reduction)
229
   * least significant bits.
230
   */
231
  wrappedBitVector<isSigned> contract(Cvc5BitWidth reduction) const;
232
233
  /**
234
   * Create a "resized" bit-vector of given size bei either extending (if new
235
   * size is larger) or contracting (if it is smaller) this wrapped bit-vector.
236
   */
237
  wrappedBitVector<isSigned> resize(Cvc5BitWidth newSize) const;
238
239
  /**
240
   * Create an extension of this bit-vector that matches the bit-width of the
241
   * given bit-vector.
242
   *
243
   * Note: The size of the given bit-vector may not be larger than the size of
244
   *       this bit-vector.
245
   */
246
  wrappedBitVector<isSigned> matchWidth(
247
      const wrappedBitVector<isSigned>& op) const;
248
249
  /** Bit-vector concatenation. */
250
  wrappedBitVector<isSigned> append(const wrappedBitVector<isSigned>& op) const;
251
252
  /** Inclusive of end points, thus if the same, extracts just one bit. */
253
  wrappedBitVector<isSigned> extract(Cvc5BitWidth upper,
254
                                     Cvc5BitWidth lower) const;
255
};
256
}  // namespace symfpuLiteral
257
}  // namespace cvc5
258
259
#endif