GCC Code Coverage Report
Directory: . Exec Total Coverage
File: build-coverage/src/util/floatingpoint_literal_symfpu.h Lines: 13 13 100.0 %
Date: 2021-03-23 Branches: 4 8 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file floatingpoint_literal_symfpu.h.in
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Martin Brain, Andres Noetzli
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief SymFPU glue code for floating-point values.
13
 **
14
 ** !!! This header is not to be included in any other headers !!!
15
 **/
16
#include "cvc4_public.h"
17
18
#ifndef CVC4__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_H
19
#define CVC4__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_H
20
21
#include "util/bitvector.h"
22
#include "util/roundingmode.h"
23
24
// clang-format off
25
#if 1
26
// clang-format on
27
#include <symfpu/core/unpackedFloat.h>
28
#endif /* 1 */
29
30
/* -------------------------------------------------------------------------- */
31
32
namespace CVC4 {
33
34
class FloatingPointSize;
35
class FloatingPoint;
36
37
/* -------------------------------------------------------------------------- */
38
39
/**
40
 * This is a symfpu literal "back-end".  It allows the library to be used as
41
 * an arbitrary precision floating-point implementation.  This is effectively
42
 * the glue between symfpu's notion of "signed bit-vector" and CVC4's
43
 * BitVector.
44
 */
45
namespace symfpuLiteral {
46
47
/* -------------------------------------------------------------------------- */
48
49
/**
50
 * Forward declaration of wrapper so that traits can be defined early and so
51
 * used in the implementation of wrappedBitVector.
52
 */
53
template <bool T>
54
class wrappedBitVector;
55
56
using CVC4BitWidth = uint32_t;
57
using CVC4Prop = bool;
58
using CVC4RM = ::CVC4::RoundingMode;
59
using CVC4FPSize = ::CVC4::FloatingPointSize;
60
using CVC4UnsignedBitVector = wrappedBitVector<false>;
61
using CVC4SignedBitVector = wrappedBitVector<true>;
62
63
/**
64
 * This is the template parameter for symfpu's templates.
65
 */
66
class traits
67
{
68
 public:
69
  /** The six key types that symfpu uses. */
70
  using bwt = CVC4BitWidth;           // bit-width type
71
  using prop = CVC4Prop;              // boolean type
72
  using rm = CVC4RM;                  // rounding-mode type
73
  using fpt = CVC4FPSize;             // floating-point format type
74
  using ubv = CVC4UnsignedBitVector;  // unsigned bit-vector type
75
  using sbv = CVC4SignedBitVector;    // signed bit-vector type
76
77
  /** Give concrete instances of each rounding mode, mainly for comparisons. */
78
  static rm RNE(void);
79
  static rm RNA(void);
80
  static rm RTP(void);
81
  static rm RTN(void);
82
  static rm RTZ(void);
83
84
  /** The sympfu properties. */
85
  static void precondition(const prop& p);
86
  static void postcondition(const prop& p);
87
  static void invariant(const prop& p);
88
};
89
90
/**
91
 * Type function for mapping between types.
92
 */
93
template <bool T>
94
struct signedToLiteralType;
95
96
template <>
97
struct signedToLiteralType<true>
98
{
99
  using literalType = int32_t;
100
};
101
template <>
102
struct signedToLiteralType<false>
103
{
104
  using literalType = uint32_t;
105
};
106
107
/**
108
 * This extends the interface for CVC4::BitVector for compatibility with symFPU.
109
 * The template parameter distinguishes signed and unsigned bit-vectors, a
110
 * distinction symfpu uses.
111
 */
112
template <bool isSigned>
113
1943070
class wrappedBitVector : public BitVector
114
{
115
 protected:
116
  using literalType = typename signedToLiteralType<isSigned>::literalType;
117
  friend wrappedBitVector<!isSigned>;  // To allow conversion between types
118
119
// clang-format off
120
#if 1
121
  // clang-format on
122
  friend ::symfpu::ite<CVC4Prop, wrappedBitVector<isSigned> >;  // For ITE
123
#endif /* 1 */
124
125
 public:
126
  /** Constructors. */
127
780911
  wrappedBitVector(const CVC4BitWidth w, const uint32_t v) : BitVector(w, v) {}
128
10590
  wrappedBitVector(const CVC4Prop& p) : BitVector(1, p ? 1U : 0U) {}
129
202582
  wrappedBitVector(const wrappedBitVector<isSigned>& old) : BitVector(old) {}
130
948690
  wrappedBitVector(const BitVector& old) : BitVector(old) {}
131
132
  /** Get the bit-width of this wrapped bit-vector. */
133
380725
  CVC4BitWidth getWidth(void) const { return getSize(); }
134
135
  /** Create a zero value of given bit-width 'w'. */
136
  static wrappedBitVector<isSigned> one(const CVC4BitWidth& w);
137
  /** Create a one value of given bit-width 'w'. */
138
  static wrappedBitVector<isSigned> zero(const CVC4BitWidth& w);
139
  /** Create a ones value (all bits 1) of given bit-width 'w'. */
140
  static wrappedBitVector<isSigned> allOnes(const CVC4BitWidth& w);
141
  /** Create a maximum signed/unsigned value of given bit-width 'w'. */
142
  static wrappedBitVector<isSigned> maxValue(const CVC4BitWidth& w);
143
  /** Create a minimum signed/unsigned value of given bit-width 'w'. */
144
  static wrappedBitVector<isSigned> minValue(const CVC4BitWidth& w);
145
146
  /** Return true if this a bit-vector representing a ones value. */
147
  CVC4Prop isAllOnes() const;
148
  /** Return true if this a bit-vector representing a zero value. */
149
  CVC4Prop isAllZeros() const;
150
151
  /** Left shift. */
152
  wrappedBitVector<isSigned> operator<<(
153
      const wrappedBitVector<isSigned>& op) const;
154
  /** Logical (unsigned) and arithmetic (signed) right shift. */
155
  wrappedBitVector<isSigned> operator>>(
156
      const wrappedBitVector<isSigned>& op) const;
157
158
  /**
159
   * Inherited but ...
160
   * *sigh* if we use the inherited version then it will return a
161
   * CVC4::BitVector which can be converted back to a
162
   * wrappedBitVector<isSigned> but isn't done automatically when working
163
   * out types for templates instantiation.  ITE is a particular
164
   * problem as expressions and constants no longer derive the
165
   * same type.  There aren't any good solutions in C++, we could
166
   * use CRTP but Liana wouldn't appreciate that, so the following
167
   * pointless wrapping functions are needed.
168
   */
169
170
  /** Bit-wise or. */
171
  wrappedBitVector<isSigned> operator|(
172
      const wrappedBitVector<isSigned>& op) const;
173
  /** Bit-wise and. */
174
  wrappedBitVector<isSigned> operator&(
175
      const wrappedBitVector<isSigned>& op) const;
176
  /** Bit-vector addition. */
177
  wrappedBitVector<isSigned> operator+(
178
      const wrappedBitVector<isSigned>& op) const;
179
  /** Bit-vector subtraction. */
180
  wrappedBitVector<isSigned> operator-(
181
      const wrappedBitVector<isSigned>& op) const;
182
  /** Bit-vector multiplication. */
183
  wrappedBitVector<isSigned> operator*(
184
      const wrappedBitVector<isSigned>& op) const;
185
  /** Bit-vector signed/unsigned division. */
186
  wrappedBitVector<isSigned> operator/(
187
      const wrappedBitVector<isSigned>& op) const;
188
  /** Bit-vector signed/unsigned remainder. */
189
  wrappedBitVector<isSigned> operator%(
190
      const wrappedBitVector<isSigned>& op) const;
191
  /** Bit-vector negation. */
192
  wrappedBitVector<isSigned> operator-(void) const;
193
  /** Bit-wise not. */
194
  wrappedBitVector<isSigned> operator~(void) const;
195
196
  /** Bit-vector increment. */
197
  wrappedBitVector<isSigned> increment() const;
198
  /** Bit-vector decrement. */
199
  wrappedBitVector<isSigned> decrement() const;
200
  /**
201
   * Bit-vector logical/arithmetic right shift where 'op' extended to the
202
   * bit-width of this wrapped bit-vector.
203
   */
204
  wrappedBitVector<isSigned> signExtendRightShift(
205
      const wrappedBitVector<isSigned>& op) const;
206
207
  /**
208
   * Modular operations.
209
   * Note: No overflow checking so these are the same as other operations.
210
   */
211
  wrappedBitVector<isSigned> modularLeftShift(
212
      const wrappedBitVector<isSigned>& op) const;
213
  wrappedBitVector<isSigned> modularRightShift(
214
      const wrappedBitVector<isSigned>& op) const;
215
  wrappedBitVector<isSigned> modularIncrement() const;
216
  wrappedBitVector<isSigned> modularDecrement() const;
217
  wrappedBitVector<isSigned> modularAdd(
218
      const wrappedBitVector<isSigned>& op) const;
219
  wrappedBitVector<isSigned> modularNegate() const;
220
221
  /** Bit-vector equality. */
222
  CVC4Prop operator==(const wrappedBitVector<isSigned>& op) const;
223
  /** Bit-vector signed/unsigned less or equal than. */
224
  CVC4Prop operator<=(const wrappedBitVector<isSigned>& op) const;
225
  /** Bit-vector sign/unsigned greater or equal than. */
226
  CVC4Prop operator>=(const wrappedBitVector<isSigned>& op) const;
227
  /** Bit-vector signed/unsigned less than. */
228
  CVC4Prop operator<(const wrappedBitVector<isSigned>& op) const;
229
  /** Bit-vector sign/unsigned greater or equal than. */
230
  CVC4Prop operator>(const wrappedBitVector<isSigned>& op) const;
231
232
  /** Convert this bit-vector to a signed bit-vector. */
233
  wrappedBitVector<true> toSigned(void) const;
234
  /** Convert this bit-vector to an unsigned bit-vector. */
235
  wrappedBitVector<false> toUnsigned(void) const;
236
237
  /** Bit-vector signed/unsigned (zero) extension. */
238
  wrappedBitVector<isSigned> extend(CVC4BitWidth extension) const;
239
240
  /**
241
   * Create a "contracted" bit-vector by cutting off the 'reduction' number of
242
   * most significant bits, i.e., by extracting the (bit-width - reduction)
243
   * least significant bits.
244
   */
245
  wrappedBitVector<isSigned> contract(CVC4BitWidth reduction) const;
246
247
  /**
248
   * Create a "resized" bit-vector of given size bei either extending (if new
249
   * size is larger) or contracting (if it is smaller) this wrapped bit-vector.
250
   */
251
  wrappedBitVector<isSigned> resize(CVC4BitWidth newSize) const;
252
253
  /**
254
   * Create an extension of this bit-vector that matches the bit-width of the
255
   * given bit-vector.
256
   *
257
   * Note: The size of the given bit-vector may not be larger than the size of
258
   *       this bit-vector.
259
   */
260
  wrappedBitVector<isSigned> matchWidth(
261
      const wrappedBitVector<isSigned>& op) const;
262
263
  /** Bit-vector concatenation. */
264
  wrappedBitVector<isSigned> append(const wrappedBitVector<isSigned>& op) const;
265
266
  /** Inclusive of end points, thus if the same, extracts just one bit. */
267
  wrappedBitVector<isSigned> extract(CVC4BitWidth upper,
268
                                     CVC4BitWidth lower) const;
269
};
270
271
/* -------------------------------------------------------------------------- */
272
273
}  // namespace symfpuLiteral
274
275
/* -------------------------------------------------------------------------- */
276
277
// clang-format off
278
#if 1
279
// clang-format on
280
using SymFPUUnpackedFloatLiteral = ::symfpu::unpackedFloat<symfpuLiteral::traits>;
281
#endif
282
283
3383
class FloatingPointLiteral
284
{
285
  friend class FloatingPoint;
286
 public:
287
  /** Constructors. */
288
289
  /** Create an FP literal from a FloatingPoint. */
290
  FloatingPointLiteral(FloatingPoint& other);
291
// clang-format off
292
#if 1
293
// clang-format on
294
295
  /** Create an FP literal from a symFPU unpacked float. */
296
2349
  FloatingPointLiteral(SymFPUUnpackedFloatLiteral symuf) : d_symuf(symuf){};
297
298
  /**
299
   * Create a FP literal from unpacked representation.
300
   *
301
   * This unpacked representation accounts for additional bits required for the
302
   * exponent to allow subnormals to be normalized.
303
   *
304
   * This should NOT be used to create a literal from its IEEE bit-vector
305
   * representation -- for this, the above constructor is to be used while
306
   * creating a SymFPUUnpackedFloatLiteral via symfpu::unpack.
307
   */
308
12
  FloatingPointLiteral(const bool sign,
309
                       const BitVector& exp,
310
                       const BitVector& sig)
311
12
      : d_symuf(SymFPUUnpackedFloatLiteral(sign, exp, sig))
312
  {
313
12
  }
314
#else
315
  FloatingPointLiteral(uint32_t, uint32_t, double) { unfinished(); };
316
#endif
317
5744
  ~FloatingPointLiteral() {}
318
319
// clang-format off
320
#if 1
321
// clang-format on
322
  /** Return wrapped floating-point literal. */
323
262
  const SymFPUUnpackedFloatLiteral& getSymUF() const { return d_symuf; }
324
#else
325
  /** Catch-all for unimplemented functions. */
326
  void unfinished(void) const;
327
  /** Dummy hash function. */
328
  size_t hash(void) const;
329
  /** Dummy comparison operator overload. */
330
  bool operator==(const FloatingPointLiteral& other) const;
331
#endif
332
333
 private:
334
// clang-format off
335
#if 1
336
// clang-format on
337
  /** The actual floating-point value, a SymFPU unpackedFloat. */
338
  SymFPUUnpackedFloatLiteral d_symuf;
339
#endif
340
};
341
342
343
/* -------------------------------------------------------------------------- */
344
345
}
346
347
#endif