GCC Code Coverage Report
Directory: . Exec Total Coverage
File: deps/install/include/symfpu/core/unpackedFloat.h Lines: 133 133 100.0 %
Date: 2021-03-23 Branches: 247 452 54.6 %

Line Exec Source
1
/*
2
** Copyright (C) 2018 Martin Brain
3
**
4
** See the file LICENSE for licensing information.
5
*/
6
7
/*
8
** unpackedFloat.h
9
**
10
** Martin Brain
11
** martin.brain@cs.ox.ac.uk
12
** 03/06/14
13
**
14
** The working representation of a floating-point number.  This is
15
** from the packed representation in a few ways:
16
**
17
**  1. Explicit flags for NaN, Inf and Zero.
18
**  2. Significand is biased.
19
**  3. Hidden bit is explicit.
20
**  4. Subnormals are normalised.
21
**
22
** This makes numbers more uniform and makes it easier to implement
23
** compact and efficient algorithms.
24
*/
25
26
#include "symfpu/utils/common.h"
27
#include "symfpu/utils/properties.h"
28
#include "symfpu/utils/numberOfRoundingModes.h"
29
30
#include "symfpu/core/ite.h"
31
#include "symfpu/core/operations.h"
32
33
// For debugging only
34
#include <iostream>
35
36
#ifndef SYMFPU_UNPACKED_FLOAT
37
#define SYMFPU_UNPACKED_FLOAT
38
39
namespace symfpu {
40
41
  template<class t>
42
39642
    class unpackedFloat {
43
  public :
44
    // Typedef the names from the traits for convenience
45
    typedef typename t::bwt bwt;
46
    typedef typename t::fpt fpt;
47
    typedef typename t::prop prop;
48
    typedef typename t::sbv sbv;
49
    typedef typename t::ubv ubv;
50
51
52
  protected :
53
    // TODO : protect these again
54
  public :
55
    prop nan;
56
    prop inf;
57
    prop zero;
58
59
    prop sign;
60
    sbv exponent;
61
    ubv significand;
62
  protected :
63
64
    // It is possible, but hopefully as difficult as possible to create,
65
    // via the constructor an invalid unpacked float
66
67
    // A piecewise / literal constructor using fpclass
68
    enum fpclass { FPCLASS_NAN, FPCLASS_INF, FPCLASS_ZERO, FPCLASS_NUMBER };
69
70
7967
    unpackedFloat (const fpclass c, const prop &s, const sbv &exp, const ubv &signif) :
71
22962
      nan(c == FPCLASS_NAN), inf(c == FPCLASS_INF), zero(c == FPCLASS_ZERO),
72
23275
      sign(s), exponent(exp), significand(signif)
73
7967
      {}
74
75
76
    // Should only be used by ite
77
    friend ite<prop, unpackedFloat<t> >;
78
79
    // TODO : See above -- this should only be used by ite
80
  public :
81
15656
    unpackedFloat (const prop &iteNaN, const prop &iteInf, const prop &iteZero,
82
		   const prop &iteSign, const sbv &iteExponent, const ubv &iteSignificand) :
83
      nan(iteNaN), inf(iteInf), zero(iteZero),
84
15656
      sign(iteSign), exponent(iteExponent), significand(iteSignificand)
85
15656
      {}
86
  private :
87
88
    // Used for special values
89
    // However this will also be passed through the operations, thus
90
    // if it is also a valid normal number then it will make proving
91
    // invariants easier.  In this case it is the value 1.0.
92
93
33829
    static sbv defaultExponent(const fpt &fmt) {
94
33829
      return sbv::zero(unpackedFloat<t>::exponentWidth(fmt));
95
    }
96
97
33829
    static ubv defaultSignificand(const fpt &fmt) {
98
33829
      bwt significandWidth = unpackedFloat<t>::significandWidth(fmt);
99
100
33829
      return ubv::one(significandWidth) << ubv(significandWidth, (significandWidth - 1));
101
    }
102
103
104
105
  public :
106
6672
    unpackedFloat (const prop &s, const sbv &exp, const ubv &signif) :
107
      nan(false), inf(false), zero(false),
108
6672
      sign(s), exponent(exp), significand(signif)
109
6672
      {}
110
111
7498
    unpackedFloat (const unpackedFloat<t> &old) :
112
19464
      nan(old.nan), inf(old.inf), zero(old.zero),
113
20474
      sign(old.sign), exponent(old.exponent), significand(old.significand)
114
7498
      {}
115
116
    // Copy and over-write sign
117
1096
    unpackedFloat (const unpackedFloat<t> &old, const prop &s) :
118
3129
      nan(old.nan), inf(old.inf), zero(old.zero),
119
3182
      sign(ITE(old.nan, old.sign, s)), exponent(old.exponent), significand(old.significand)
120
1096
      {}
121
122
    // Swap back-ends
123
      template <class s> friend class unpackedFloat;
124
125
    template <class s>
126
262
    unpackedFloat (const unpackedFloat<s> &old) :
127
786
      nan(old.nan), inf(old.inf), zero(old.zero),
128
1048
      sign(old.sign), exponent(old.exponent), significand(old.significand)
129
262
      {}
130
131
132
3665
    static unpackedFloat<t> makeZero(const fpt &fmt, const prop &s) {
133
3665
      return unpackedFloat<t>(FPCLASS_ZERO, s, defaultExponent(fmt), defaultSignificand(fmt));
134
    }
135
136
2705
    static unpackedFloat<t> makeInf(const fpt &fmt, const prop &s) {
137
2705
      return unpackedFloat<t>(FPCLASS_INF, s, defaultExponent(fmt), defaultSignificand(fmt));
138
    }
139
140
1597
    static unpackedFloat<t> makeNaN(const fpt &fmt) {
141
1597
      return unpackedFloat<t>(FPCLASS_NAN, false, defaultExponent(fmt), defaultSignificand(fmt));
142
    }
143
144
31516
    inline const prop & getNaN(void) const { return this->nan; }
145
25914
    inline const prop & getInf(void) const { return this->inf; }
146
27524
    inline const prop & getZero(void) const { return this->zero; }
147
37359
    inline const prop & getSign(void) const { return this->sign; }
148
19624
    inline const sbv & getExponent(void) const { return this->exponent; }
149
22397
    inline const ubv & getSignificand(void) const { return this->significand; }
150
151
    //    inline unpackedFloat<t> changeSign(const prop &newSign) {
152
    //      return unpackedFloat<t>(*this, newSign);
153
    //    }
154
155
156
157
158
    // Get the number of bits in the unpacked format corresponding to a
159
    // given packed format.  These are the unpacked counter-parts of
160
    //  format.exponentWidth() and format.significandWidth()
161
162
397046
    static bwt exponentWidth(const fpt &format) {
163
164
      // Note that there is one more exponent above 0 than there is
165
      // below.  This is the opposite of 2's compliment but this is not
166
      // a problem because the highest packed exponent corresponds to
167
      // inf and NaN and is thus does not need to be represented in the
168
      // unpacked format.
169
      // However we do need to increase it to allow subnormals (packed)
170
      // to be normalised.
171
172
397046
      bwt width = format.exponentWidth();
173
174
      // Could be improved to remove overflow concerns
175
397046
      uint64_t minimumExponent = ((1 << (width - 1)) - 2) + (format.significandWidth() - 1);
176
177
      // Increase width until even the smallest subnormal can be normalised
178
1191978
      while ((1UL << (width - 1)) < minimumExponent) {
179
397466
	++width;
180
      }
181
182
397046
      return width;
183
    }
184
185
149790
    static bwt significandWidth(const fpt &format) {
186
      // Hidden bit is already included in the floating-point format
187
149790
      return format.significandWidth();
188
    }
189
190
191
192
193
    // These should all evaluate to a literal value but are given as
194
    // sbv's to make their use easier and to avoid concerns of overflow.
195
196
204617
    static sbv bias(const fpt &format) {
197
204617
      bwt w(exponentWidth(format));
198
409234
      sbv one(sbv::one(w));
199
200
409234
      return (one << sbv(w,(format.exponentWidth() - 1))) - one;
201
    }
202
203
204
37260
    static sbv maxNormalExponent(const fpt &format) {
205
37260
      return bias(format);
206
    }
207
208
71163
    static sbv minNormalExponent(const fpt &format) {
209
71163
      return -(bias(format) - sbv::one(exponentWidth(format)));
210
    }
211
212
89180
    static sbv maxSubnormalExponent(const fpt &format) {
213
89180
      return -bias(format);
214
    }
215
216
59896
    static sbv minSubnormalExponent(const fpt &format) {
217
59896
      return maxSubnormalExponent(format) - sbv(exponentWidth(format),(significandWidth(format) - 2));
218
    }
219
220
    // Note the different return type as this is used for iteration in remainder
221
105
    static bwt maximumExponentDifference(const fpt &format) {
222
105
      bwt maxNormalExp = (1ULL << (format.exponentWidth() - 1)) - 1;
223
105
      bwt minSubnormalExp = -maxNormalExp - (significandWidth(format) - 2);
224
105
      return maxNormalExp - minSubnormalExp;
225
    }
226
227
    // knownInFormat uses the format invariant to simplify the test
228
6725
    inline prop inNormalRange(const fpt &format, const prop &knownInFormat) const {
229
16864
      return ((minNormalExponent(format) <= exponent) &&
230
16828
	      ((exponent <= maxNormalExponent(format) || knownInFormat)));
231
    }
232
233
    // knownInFormat uses the format invariant to simplify the test
234
29284
    inline prop inSubnormalRange(const fpt &format, const prop &knownInFormat) const {
235
      // To share tests with the inNormalRange test...
236
37601
      prop upperBound(!(minNormalExponent(format) <= exponent));
237
29284
      INVARIANT(upperBound == (exponent <= maxSubnormalExponent(format)));
238
239
41934
      return (((minSubnormalExponent(format) <= exponent) || knownInFormat) &&
240
58568
	      upperBound);
241
    }
242
243
25862
    inline prop inNormalOrSubnormalRange(const fpt &format, const prop &knownInFormat) const {
244
104270
      return ((minSubnormalExponent(format) <= exponent) &&
245
109278
	      (exponent <= maxNormalExponent(format))) || knownInFormat;
246
    }
247
248
249
250
    // The amount needed to normalise the number
251
32549
    inline sbv getSubnormalAmount(const fpt &format) const {
252
      return max<t>(minNormalExponent(format) - exponent,
253
32549
		    sbv::zero(exponent.getWidth()));
254
    }
255
256
551
    inline prop isPositiveInf (void) const {
257
551
      return this->inf && !this->sign;
258
    }
259
260
558
    inline prop isNegativeInf (void) const {
261
558
      return this->inf && this->sign;
262
    }
263
264
265
266
    // Likewise, this is a convenience function
267
29606
    static ubv leadingOne(const bwt sigWidth) {
268
29606
      return ubv::one(sigWidth) << ubv(sigWidth, (sigWidth - 1));
269
    }
270
271
6687
    static ubv nanPattern(const bwt sigWidth) {
272
6687
      return ubv::one(sigWidth) << ubv(sigWidth, (sigWidth - 1)); // For a qNaN, change for sNaN
273
    }
274
275
276
277
23
    unpackedFloat<t> extend (const bwt expExtension, const bwt sigExtension) const {
278
      return unpackedFloat<t>(this->nan,
279
			      this->inf,
280
			      this->zero,
281
			      this->sign,
282
			      this->exponent.extend(expExtension),
283
23
			      this->significand.extend(sigExtension) << ubv((this->significand.getWidth() + sigExtension), sigExtension));
284
    }
285
286
287
    // Moves the leading 1 up to the correct position, adjusting the
288
    // exponent as required.
289
1088
    unpackedFloat<t> normaliseUp (const fpt &/*format*/) const {
290
1088
      PRECONDITION(!(nan || inf || zero));  // Should not be attempting to normalise these.
291
292
2176
      normaliseShiftResult<t> normal(normaliseShift<t>(this->significand));
293
294
1088
      bwt exponentWidth(this->exponent.getWidth());
295
1088
      INVARIANT(normal.shiftAmount.getWidth() < exponentWidth); // May loose data / be incorrect for very small exponents and very large significands
296
297
2176
      sbv signedAlignAmount(normal.shiftAmount.resize(exponentWidth).toSigned());
298
2176
      sbv correctedExponent(this->exponent - signedAlignAmount);
299
300
      // Optimisation : could move the zero detect version in if used in all cases
301
      //  catch - it zero detection in unpacking is different.
302
2176
      return unpackedFloat<t>(this->sign, correctedExponent, normal.normalised);
303
    }
304
305
306
109
    unpackedFloat<t> normaliseUpDetectZero (const fpt &format) const {
307
109
      PRECONDITION(!(nan || inf || zero));  // Should not be attempting to normalise these.
308
309
218
      normaliseShiftResult<t> normal(normaliseShift<t>(this->significand));
310
311
109
      bwt exponentWidth(this->exponent.getWidth());
312
109
      INVARIANT(normal.shiftAmount.getWidth() < exponentWidth); // May loose data / be incorrect for very small exponents and very large significands
313
314
218
      sbv signedAlignAmount(normal.shiftAmount.resize(exponentWidth).toSigned());
315
218
      sbv correctedExponent(this->exponent - signedAlignAmount);
316
317
      return ITE(normal.isZero,
318
		 unpackedFloat<t>::makeZero(format, this->sign),
319
218
		 unpackedFloat<t>(this->sign, correctedExponent, normal.normalised));
320
    }
321
322
#if 0
323
    // Moves the leading 1 up to the correct position, adjusting the
324
    // exponent as required.
325
    unpackedFloat<t> normaliseUp (const fpt &/*format*/) const {
326
      PRECONDITION(!(nan || inf || zero));  // Should not be attempting to normalise these.
327
328
      ubv alignAmount(countLeadingZeros<t>(this->significand));
329
330
      ubv alignedSignificand(this->significand.modularLeftShift(alignAmount)); // CLZ means data is not lost
331
332
      sbv signedAlignAmount(alignAmount.extract(this->exponent.getWidth() - 1,0).toSigned());
333
      // May loose data / be incorrect for very small exponents and very large significands
334
      sbv correctedExponent(this->exponent - signedAlignAmount);
335
336
      // Optimisation : could move the zero detect version in if used in all cases
337
      return unpackedFloat<t>(this->sign, correctedExponent, alignedSignificand);
338
    }
339
340
    unpackedFloat<t> normaliseUpDetectZero (const fpt &format) const {
341
      unpackedFloat<t> normal(this->normaliseUp(format));
342
343
      return ITE(this->significand.isAllZeros(),
344
		 unpackedFloat<t>::makeZero(format, this->sign),
345
		 normal);
346
    }
347
#endif
348
349
350
#if 0
351
    unpackedFloat<t> normaliseUp (const fpt &format) const {
352
      PRECONDITION(!(nan || inf || zero));  // Should not be attempting to normalise these.
353
354
      unpackedFloat<t> working(*this);
355
      bwt sigWidth = unpackedFloat<t>::significandWidth(format);
356
      bwt exWidth = unpackedFloat<t>::exponentWidth(format);
357
358
      // TODO : is range checking needed here?  Only in obscure use cases.
359
360
      for (bwt power = previousPowerOfTwo(sigWidth); power != 0; power >>= 1) {
361
	bwt rem = sigWidth - power;
362
363
	INVARIANT(rem > 0);
364
365
	ubv mask(ubv::allOnes(power).extend(rem) << rem);
366
	prop shiftNeeded((mask & working.significand).isAllZeros());
367
368
	// Has to be modular as in the case it is not needed,
369
	// performing the shift will loose information.
370
	working.significand = ITE(shiftNeeded, working.significand.modularLeftShift(power), working.significand);
371
	working.exponent = ITE(shiftNeeded, working.exponent - sbv(exWidth,power), working.exponent);
372
        // Optimisation : rather than add each cycle, build shiftNeeded into a number and add once.
373
      }
374
375
      return working;
376
    }
377
#endif
378
379
380
381
    // Is a well formed unpacked struct of the given format?
382
    // The format is needed to ensure that subnormals are correct.
383
    // This invariant does not hold at all points in the code!
384
25862
    prop valid(const fpt &format) const {
385
386
25862
      bwt exWidth = exponentWidth(format);
387
25862
      bwt sigWidth = significandWidth(format);
388
389
25862
      PRECONDITION((exWidth == exponent.getWidth()) &&
390
		   (sigWidth == significand.getWidth()));
391
392
      // At most one flag is true
393
30870
      prop atMostOneFlag(!(nan && inf) && !(nan && zero) && !(inf && zero));
394
395
      // If one flag is true then exponent and significand are defaults
396
30870
      prop oneFlag(nan || inf || zero);
397
30870
      prop exponentIsDefault(defaultExponent(format) == exponent);
398
30870
      prop significandIsDefault(defaultSignificand(format) == significand);
399
30870
      prop flagImpliesDefaultExponent(IMPLIES(oneFlag, exponentIsDefault));
400
30870
      prop flagImpliesDefaultSignificand(IMPLIES(oneFlag, significandIsDefault));
401
402
      // NaN has sign = 0
403
30870
      prop NaNImpliesSignFalse(IMPLIES(nan, !sign));
404
405
      // Exponent is in range
406
30870
      prop exponentInRange(inNormalOrSubnormalRange(format, prop(false)));
407
408
      // Has a leading one
409
30870
      prop hasLeadingOne(!(leadingOne(unpackedFloat<t>::significandWidth(format)) & significand).isAllZeros());
410
411
      // Subnormal numbers require an additional check to make sure they
412
      // do not have an unrepresentable amount of significand bits.
413
51724
      sbv subnormalAmount(this->getSubnormalAmount(format));
414
25862
      INVARIANT((sbv::zero(exWidth) <= subnormalAmount) &&
415
		(subnormalAmount <= sbv(exWidth,sigWidth)));
416
417
      // Invariant implies this following steps do not loose data
418
51724
      ubv mask(orderEncode<t>(subnormalAmount.toUnsigned().matchWidth(significand)));
419
420
30870
      prop correctlyAbbreviated((mask & significand).isAllZeros());
421
422
30870
      prop subnormalImpliesTrailingZeros(IMPLIES(inSubnormalRange(format, prop(false)), correctlyAbbreviated));
423
424
425
20854
      return (atMostOneFlag &&
426
20854
	      (flagImpliesDefaultExponent && flagImpliesDefaultSignificand) &&
427
20854
	      NaNImpliesSignFalse &&
428
20854
	      exponentInRange &&
429
41708
	      hasLeadingOne &&
430
51724
	      subnormalImpliesTrailingZeros);
431
    }
432
433
434
435
      /* Older version
436
       * Correct but replaced with a version which gives more propagation friendly assertions.
437
       */
438
#if 0
439
    prop valid(const fpt &format) const {
440
441
      bwt exWidth = exponentWidth(format);
442
      bwt sigWidth = significandWidth(format);
443
444
      PRECONDITION((exWidth == exponent.getWidth()) &&
445
		   (sigWidth == significand.getWidth()));
446
447
      prop hasLeadingOne(!(leadingOne(unpackedFloat<t>::significandWidth(format)) & significand).isAllZeros());
448
449
450
451
      // Subnormal numbers require an additional check to make sure they
452
      // do not have an unrepresentable amount of significand bits.
453
      sbv subnormalAmount(this->getSubnormalAmount(format));
454
      INVARIANT((sbv::zero(exWidth) <= subnormalAmount) &&
455
		(subnormalAmount <= sbv(exWidth,sigWidth)));
456
457
      // Invariant implies this following steps do not loose data
458
      ubv trimmedSubnormalAmount(subnormalAmount.toUnsigned().extract(positionOfLeadingOne(sigWidth),0));
459
      ubv mask(trimmedSubnormalAmount.orderEncode(sigWidth));
460
461
      prop correctlyAbbreviated((mask & significand).isAllZeros());
462
463
464
465
      prop normalCase   (!nan && !inf && !zero && inNormalRange(format, prop(false))    && hasLeadingOne);
466
      prop subnormalCase(!nan && !inf && !zero && inSubnormalRange(format, prop(false)) && hasLeadingOne && correctlyAbbreviated);
467
468
469
470
      prop exponentIsDefault(defaultExponent(format) == exponent);
471
      prop significandIsDefault(defaultSignificand(format) == significand);
472
473
      prop NaNCase ( nan && !inf && !zero && exponentIsDefault && significandIsDefault && !sign);
474
      prop InfCase (!nan &&  inf && !zero && exponentIsDefault && significandIsDefault);
475
      prop ZeroCase(!nan && !inf &&  zero && exponentIsDefault && significandIsDefault);
476
477
      return (NaNCase || InfCase || ZeroCase || normalCase || subnormalCase);
478
479
    }
480
#endif
481
482
483
    // Just for debugging
484
    void print (void) const {
485
      std::cerr << "nan : " << this->nan << '\t'
486
		<< "inf : " << this->inf << '\t'
487
		<< "zero : " << this->zero << '\t'
488
		<< "sign : " << this->sign << '\t'
489
		<< "exponent : " << this->exponent << '\t'
490
		<< "significand : " << this->significand << std::endl;
491
    }
492
493
  };
494
495
template <class t>
496
  struct ite<typename t::prop, unpackedFloat<t> > {
497
15498
  static const unpackedFloat<t> iteOp (const typename t::prop &cond,
498
			    const unpackedFloat<t> &l,
499
			    const unpackedFloat<t> &r) {
500
29788
    return unpackedFloat<t>(ITE(cond, l.nan, r.nan),
501
29788
			    ITE(cond, l.inf, r.inf),
502
29788
			    ITE(cond, l.zero, r.zero),
503
29788
			    ITE(cond, l.sign, r.sign),
504
			    ITE(cond, l.exponent, r.exponent),
505
45286
			    ITE(cond, l.significand, r.significand));
506
    }
507
 };
508
509
510
511
512
}
513
514
#endif