GCC Code Coverage Report
Directory: . Exec Total Coverage
File: deps/install/include/symfpu/core/compare.h Lines: 62 65 95.4 %
Date: 2021-03-23 Branches: 228 357 63.9 %

Line Exec Source
1
/*
2
** Copyright (C) 2018 Martin Brain
3
**
4
** See the file LICENSE for licensing information.
5
*/
6
7
/*
8
** compare.h
9
**
10
** Martin Brain
11
** martin.brain@cs.ox.ac.uk
12
** 25/08/14
13
**
14
** Comparison between floating-point numbers
15
**
16
*/
17
18
#include "symfpu/core/unpackedFloat.h"
19
#include "symfpu/core/ite.h"
20
21
#ifndef SYMFPU_COMPARE
22
#define SYMFPU_COMPARE
23
24
namespace symfpu {
25
26
  // SMT-LIB equality
27
  template <class t>
28
3105
    typename t::prop smtlibEqual (const typename t::fpt &format,
29
				  const unpackedFloat<t> &left,
30
				  const unpackedFloat<t> &right) {
31
    typedef typename t::prop prop;
32
33
3105
    PRECONDITION(left.valid(format));
34
3105
    PRECONDITION(right.valid(format));
35
36
    // Relies on a number of properties of the unpacked format
37
    // particularly the use of default exponents, significands and signs
38
39
9680
    prop flagsEqual((left.getNaN() == right.getNaN()) &&
40
5787
		    (left.getInf() == right.getInf()) &&
41
8474
		    (left.getZero() == right.getZero()) &&
42
3052
		    (left.getSign() == right.getSign()));
43
44
3488
    prop flagsAndExponent(flagsEqual && left.getExponent() == right.getExponent());
45
46
    // Avoid comparing (and thus instantiating) the significand unless necessary
47
3105
    probabilityAnnotation<t,prop>(flagsAndExponent, UNLIKELY);
48
49
8932
    prop res(ITE(flagsAndExponent,
50
5827
		 left.getSignificand() == right.getSignificand(),
51
		 prop(false)));
52
53
3488
    return res;
54
  }
55
56
  // IEEE-754 Equality (not actually an equivalence relation but ...)
57
  template <class t>
58
    typename t::prop ieee754Equal (const typename t::fpt &format,
59
				   const unpackedFloat<t> &left,
60
				   const unpackedFloat<t> &right) {
61
62
    typedef typename t::prop prop;
63
64
    PRECONDITION(left.valid(format));
65
    PRECONDITION(right.valid(format));
66
67
    prop neitherNan(!left.getNaN() && !right.getNaN());   // All comparison with NaN are false
68
    prop bothZero(left.getZero() && right.getZero());  // Both zeros are equal
69
    prop neitherZero(!left.getZero() && !right.getZero());
70
71
    prop flagsAndExponent(neitherNan &&
72
			  (bothZero || (neitherZero &&
73
					(left.getInf() == right.getInf() &&
74
					 left.getSign() == right.getSign() &&
75
					 left.getExponent() == right.getExponent()))));
76
77
    // Avoid comparing (and thus instantiating) the significand unless necessary
78
    probabilityAnnotation<t,prop>(flagsAndExponent, UNLIKELY);
79
80
    prop res(ITE(flagsAndExponent, left.getSignificand() == right.getSignificand(), prop(false)));
81
82
    return res;
83
  }
84
85
86
  // Share the common comparison code between functions
87
  // equality == true if the equal case returns true
88
  // IEEE-754 semantics for ordering with NaN
89
  // (i.e. unordered with everything, not even equal to itself)
90
  template <class t>
91
502
    typename t::prop ordering (const typename t::fpt &format,
92
			       const unpackedFloat<t> &left,
93
			       const unpackedFloat<t> &right,
94
			       const typename t::prop equality) {
95
96
    typedef typename t::prop prop;
97
98
502
    PRECONDITION(left.valid(format));
99
502
    PRECONDITION(right.valid(format));
100
101
    // All comparison with NaN are false
102
550
    prop neitherNaN(!left.getNaN() && !right.getNaN());
103
104
    // Either is an infinity (wrong in the case of NaN but will be corrected)
105
2008
    prop infCase( (left.isNegativeInf() && ITE(equality, prop(true), !right.isNegativeInf()) ) ||
106
1800
		  (right.isPositiveInf() && ITE(equality, prop(true), !left.isPositiveInf()) ) ||
107
987
		  (ITE(equality, left.getInf() && right.getInf() && left.getSign() == right.getSign(), prop(false))) );
108
109
110
    // Either is a zero (wrong in the case of NaN but will be corrected)
111
1646
    prop zeroCase( ( left.getZero() && !right.getZero() && !right.getSign()) ||
112
1390
		   (right.getZero() && !left.getZero()  &&  left.getSign()) ||
113
837
		   (ITE(equality, left.getZero() && right.getZero(), prop(false))) );
114
115
116
    // Normal and subnormal case
117
2056
    prop normalOrSubnormal(!left.getNaN()  && !right.getNaN() &&
118
1409
			   !left.getInf()  && !right.getInf() &&
119
1281
			   !left.getZero() && !right.getZero());
120
121
550
    prop negativeLessThanPositive(normalOrSubnormal && left.getSign() && !right.getSign());
122
123
550
    prop exponentNeeded(normalOrSubnormal && left.getSign() == right.getSign());
124
502
    probabilityAnnotation<t>(exponentNeeded, UNLIKELY);
125
126
705
    prop positiveCase(!left.getSign() && !right.getSign() &&
127
203
		      left.getExponent() < right.getExponent());
128
587
    prop negativeCase( left.getSign() &&  right.getSign() &&
129
85
		      left.getExponent() > right.getExponent());
130
131
132
550
    prop exponentEqual(left.getExponent() == right.getExponent());
133
134
550
    prop significandNeeded(exponentNeeded && exponentEqual);
135
502
    probabilityAnnotation<t>(significandNeeded, VERYUNLIKELY);
136
137
705
    prop positiveExEqCase(!left.getSign() && !right.getSign() &&
138
203
			  left.getSignificand() < right.getSignificand());
139
587
    prop negativeExEqCase( left.getSign() &&  right.getSign() &&
140
85
			   left.getSignificand() > right.getSignificand());
141
142
705
    prop positiveExEqCaseEq(!left.getSign() && !right.getSign() &&
143
203
			    left.getSignificand() <= right.getSignificand());
144
587
    prop negativeExEqCaseEq( left.getSign() &&  right.getSign() &&
145
85
			     left.getSignificand() >= right.getSignificand());
146
147
908
    return ITE(!normalOrSubnormal,
148
908
	       neitherNaN && (infCase || zeroCase),
149
908
	       ITE(!exponentNeeded,
150
		   negativeLessThanPositive,
151
908
		   ITE(!significandNeeded,
152
908
		       positiveCase || negativeCase,
153
908
		       ITE(equality,
154
908
			   positiveExEqCaseEq || negativeExEqCaseEq,
155
1458
			   positiveExEqCase || negativeExEqCase))));
156
  }
157
158
159
  template <class t>
160
6
    typename t::prop lessThan (const typename t::fpt &format,
161
			       const unpackedFloat<t> &left,
162
			       const unpackedFloat<t> &right) {
163
6
    PRECONDITION(left.valid(format));
164
6
    PRECONDITION(right.valid(format));
165
166
    typedef typename t::prop prop;
167
168
6
    return ordering(format, left, right, prop(false));
169
  }
170
171
172
  template <class t>
173
72
    typename t::prop lessThanOrEqual (const typename t::fpt &format,
174
				      const unpackedFloat<t> &left,
175
				      const unpackedFloat<t> &right) {
176
72
    PRECONDITION(left.valid(format));
177
72
    PRECONDITION(right.valid(format));
178
179
    typedef typename t::prop prop;
180
181
72
    return ordering(format, left, right, prop(true));
182
  }
183
184
185
  // Note that IEEE-754 says that max(+0,-0) = +/-0 and max(-0,+0) = +/- 0
186
  template <class t>
187
424
  unpackedFloat<t> max (const typename t::fpt &format,
188
			const unpackedFloat<t> &left,
189
			const unpackedFloat<t> &right,
190
			const typename t::prop &zeroCase) {
191
848
    return ITE(left.getNaN() || ordering(format, left, right, zeroCase),
192
	       right,
193
848
	       left);
194
  }
195
196
  // Note that IEEE-754 says that min(+0,-0) = +/-0 and min(-0,+0) = +/- 0
197
  // this will always return the left one.
198
  template <class t>
199
  unpackedFloat<t> min (const typename t::fpt &format,
200
			const unpackedFloat<t> &left,
201
			const unpackedFloat<t> &right,
202
			const typename t::prop &zeroCase) {
203
    return ITE(right.getNaN() || ordering(format, left, right, zeroCase),
204
	       left,
205
	       right);
206
  }
207
208
209
210
  template <class t>
211
    typename t::prop originalLessThan (const typename t::fpt &format,
212
				       const unpackedFloat<t> &left,
213
				       const unpackedFloat<t> &right) {
214
215
    typedef typename t::prop prop;
216
217
    PRECONDITION(left.valid(format));
218
    PRECONDITION(right.valid(format));
219
220
    // Optimisation : merge < and ==
221
222
223
    // All comparison with NaN are false
224
    prop neitherNan(!left.getNaN() && !right.getNaN());
225
226
    // Infinities are bigger than everything but themself
227
    prop eitherInf(left.getInf() || right.getInf());
228
    prop infCase(( left.isNegativeInf() && !right.isNegativeInf()) ||
229
		 (!left.isPositiveInf() &&  right.isPositiveInf()));
230
231
232
    // Both zero are equal
233
    prop eitherZero(left.getZero() || right.getZero());
234
    prop zeroCase(( left.getZero() && !right.getZero() && !right.getSign()) ||
235
		  (!left.getZero() &&   left.getSign() &&  right.getZero()));
236
237
238
    // Normal and subnormal
239
240
    prop negativeLessThanPositive(left.getSign() && !right.getSign());  // - < +
241
    prop positiveCase(!left.getSign() && !right.getSign() &&
242
		      ((left.getExponent() < right.getExponent()) ||
243
		       (left.getExponent() == right.getExponent() &&
244
			left.getSignificand() < right.getSignificand())));
245
246
    prop negativeCase(left.getSign() && right.getSign() &&
247
		      ((left.getExponent() > right.getExponent()) ||
248
		       (left.getExponent() == right.getExponent() &&
249
			left.getSignificand() > right.getSignificand())));
250
251
252
    return neitherNan &&
253
      ITE(eitherInf,
254
	  infCase,
255
	  ITE(eitherZero,
256
	      zeroCase,
257
	      negativeLessThanPositive || positiveCase || negativeCase));
258
  }
259
260
  // Optimised combination of the two
261
  template <class t>
262
    typename t::prop originalLessThanOrEqual (const typename t::fpt &format,
263
					      const unpackedFloat<t> &left,
264
					      const unpackedFloat<t> &right) {
265
266
    typedef typename t::prop prop;
267
268
    PRECONDITION(left.valid(format));
269
    PRECONDITION(right.valid(format));
270
271
    // Optimisation : merge < and ==
272
273
274
    // All comparison with NaN are false
275
    prop neitherNan(!left.getNaN() && !right.getNaN());
276
277
    // Infinities are bigger than everything but themself
278
    prop eitherInf(left.getInf() || right.getInf());
279
    prop infCase( (left.getInf() && right.getInf() && left.getSign() == right.getSign()) ||
280
		  left.isNegativeInf() ||
281
		  right.isPositiveInf());
282
283
284
    // Both zero are equal
285
    prop eitherZero(left.getZero() || right.getZero());
286
    prop zeroCase((left.getZero() && right.getZero()) ||
287
		  ( left.getZero() && !right.getSign()) ||
288
		  ( left.getSign() &&  right.getZero()));
289
290
291
    // Normal and subnormal
292
293
    prop negativeLessThanPositive(left.getSign() && !right.getSign());  // - < +
294
    prop positiveCase(!left.getSign() && !right.getSign() &&
295
		      ((left.getExponent() < right.getExponent()) ||
296
		       (left.getExponent() == right.getExponent() &&
297
			left.getSignificand() <= right.getSignificand())));
298
299
    prop negativeCase(left.getSign() && right.getSign() &&
300
		      ((left.getExponent() > right.getExponent()) ||
301
		       (left.getExponent() == right.getExponent() &&
302
			left.getSignificand() >= right.getSignificand())));
303
304
305
    return neitherNan &&
306
      ITE(eitherInf,
307
	  infCase,
308
	  ITE(eitherZero,
309
	      zeroCase,
310
	      negativeLessThanPositive || positiveCase || negativeCase));
311
  }
312
313
}
314
315
#endif