GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/floatingpoint_literal_symfpu.cpp Lines: 111 120 92.5 %
Date: 2021-03-23 Branches: 67 268 25.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file floatingpoint_literal_symfpu.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Martin Brain, Aina Niemetz, Mathias Preiner
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
#include "util/floatingpoint_literal_symfpu.h"
15
16
#include "base/check.h"
17
18
namespace CVC4 {
19
20
#ifndef CVC4_USE_SYMFPU
21
void FloatingPointLiteral::unfinished(void) const
22
{
23
  Unimplemented() << "Floating-point literals not yet implemented.";
24
}
25
26
bool FloatingPointLiteral::operator==(const FloatingPointLiteral& other) const
27
{
28
  unfinished();
29
  return false;
30
}
31
32
size_t FloatingPointLiteral::hash(void) const
33
{
34
  unfinished();
35
  return 23;
36
}
37
#endif
38
39
namespace symfpuLiteral {
40
41
// To simplify the property macros
42
typedef traits t;
43
44
template <bool isSigned>
45
320192
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::one(
46
    const CVC4BitWidth& w)
47
{
48
320192
  return wrappedBitVector<isSigned>(w, 1);
49
}
50
51
template <bool isSigned>
52
172638
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::zero(
53
    const CVC4BitWidth& w)
54
{
55
172638
  return wrappedBitVector<isSigned>(w, 0);
56
}
57
58
template <bool isSigned>
59
19640
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::allOnes(
60
    const CVC4BitWidth& w)
61
{
62
19640
  return ~wrappedBitVector<isSigned>::zero(w);
63
}
64
65
template <bool isSigned>
66
10940
CVC4Prop wrappedBitVector<isSigned>::isAllOnes() const
67
{
68
10940
  return (*this == wrappedBitVector<isSigned>::allOnes(getWidth()));
69
}
70
template <bool isSigned>
71
56991
CVC4Prop wrappedBitVector<isSigned>::isAllZeros() const
72
{
73
56991
  return (*this == wrappedBitVector<isSigned>::zero(getWidth()));
74
}
75
76
template <bool isSigned>
77
5
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::maxValue(
78
    const CVC4BitWidth& w)
79
{
80
  if (isSigned)
81
  {
82
10
    BitVector base(w - 1, 0U);
83
5
    return wrappedBitVector<true>((~base).zeroExtend(1));
84
  }
85
  else
86
  {
87
    return wrappedBitVector<false>::allOnes(w);
88
  }
89
}
90
91
template <bool isSigned>
92
21
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::minValue(
93
    const CVC4BitWidth& w)
94
{
95
  if (isSigned)
96
  {
97
42
    BitVector base(w, 1U);
98
42
    BitVector shiftAmount(w, w - 1);
99
42
    BitVector result(base.leftShift(shiftAmount));
100
21
    return wrappedBitVector<true>(result);
101
  }
102
  else
103
  {
104
    return wrappedBitVector<false>::zero(w);
105
  }
106
}
107
108
/*** Operators ***/
109
template <bool isSigned>
110
241223
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator<<(
111
    const wrappedBitVector<isSigned>& op) const
112
{
113
241223
  return BitVector::leftShift(op);
114
}
115
116
template <>
117
wrappedBitVector<true> wrappedBitVector<true>::operator>>(
118
    const wrappedBitVector<true>& op) const
119
{
120
  return BitVector::arithRightShift(op);
121
}
122
123
template <>
124
5354
wrappedBitVector<false> wrappedBitVector<false>::operator>>(
125
    const wrappedBitVector<false>& op) const
126
{
127
5354
  return BitVector::logicalRightShift(op);
128
}
129
130
template <bool isSigned>
131
5181
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator|(
132
    const wrappedBitVector<isSigned>& op) const
133
{
134
5181
  return BitVector::operator|(op);
135
}
136
137
template <bool isSigned>
138
51715
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator&(
139
    const wrappedBitVector<isSigned>& op) const
140
{
141
51715
  return BitVector::operator&(op);
142
}
143
144
template <bool isSigned>
145
11626
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator+(
146
    const wrappedBitVector<isSigned>& op) const
147
{
148
11626
  return BitVector::operator+(op);
149
}
150
151
template <bool isSigned>
152
302037
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator-(
153
    const wrappedBitVector<isSigned>& op) const
154
{
155
302037
  return BitVector::operator-(op);
156
}
157
158
template <bool isSigned>
159
456
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator*(
160
    const wrappedBitVector<isSigned>& op) const
161
{
162
456
  return BitVector::operator*(op);
163
}
164
165
template <>
166
188
wrappedBitVector<false> wrappedBitVector<false>::operator/(
167
    const wrappedBitVector<false>& op) const
168
{
169
188
  return BitVector::unsignedDivTotal(op);
170
}
171
172
template <>
173
188
wrappedBitVector<false> wrappedBitVector<false>::operator%(
174
    const wrappedBitVector<false>& op) const
175
{
176
188
  return BitVector::unsignedRemTotal(op);
177
}
178
179
template <bool isSigned>
180
124792
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator-(void) const
181
{
182
124792
  return BitVector::operator-();
183
}
184
185
template <bool isSigned>
186
23809
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator~(void) const
187
{
188
23809
  return BitVector::operator~();
189
}
190
191
template <bool isSigned>
192
140
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::increment() const
193
{
194
140
  return *this + wrappedBitVector<isSigned>::one(getWidth());
195
}
196
197
template <bool isSigned>
198
25023
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::decrement() const
199
{
200
25023
  return *this - wrappedBitVector<isSigned>::one(getWidth());
201
}
202
203
template <bool isSigned>
204
1860
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::signExtendRightShift(
205
    const wrappedBitVector<isSigned>& op) const
206
{
207
1860
  return BitVector::arithRightShift(BitVector(getWidth(), op));
208
}
209
210
/*** Modular opertaions ***/
211
// No overflow checking so these are the same as other operations
212
template <bool isSigned>
213
29088
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularLeftShift(
214
    const wrappedBitVector<isSigned>& op) const
215
{
216
29088
  return *this << op;
217
}
218
219
template <bool isSigned>
220
735
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularRightShift(
221
    const wrappedBitVector<isSigned>& op) const
222
{
223
735
  return *this >> op;
224
}
225
226
template <bool isSigned>
227
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularIncrement() const
228
{
229
  return increment();
230
}
231
232
template <bool isSigned>
233
22687
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularDecrement() const
234
{
235
22687
  return decrement();
236
}
237
238
template <bool isSigned>
239
4762
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularAdd(
240
    const wrappedBitVector<isSigned>& op) const
241
{
242
4762
  return *this + op;
243
}
244
245
template <bool isSigned>
246
4630
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularNegate() const
247
{
248
4630
  return -(*this);
249
}
250
251
/*** Comparisons ***/
252
253
template <bool isSigned>
254
119124
CVC4Prop wrappedBitVector<isSigned>::operator==(
255
    const wrappedBitVector<isSigned>& op) const
256
{
257
119124
  return BitVector::operator==(op);
258
}
259
260
template <>
261
178564
CVC4Prop wrappedBitVector<true>::operator<=(
262
    const wrappedBitVector<true>& op) const
263
{
264
178564
  return signedLessThanEq(op);
265
}
266
267
template <>
268
1238
CVC4Prop wrappedBitVector<true>::operator>=(
269
    const wrappedBitVector<true>& op) const
270
{
271
1238
  return !(signedLessThan(op));
272
}
273
274
template <>
275
6331
CVC4Prop wrappedBitVector<true>::operator<(
276
    const wrappedBitVector<true>& op) const
277
{
278
6331
  return signedLessThan(op);
279
}
280
281
template <>
282
5030
CVC4Prop wrappedBitVector<true>::operator>(
283
    const wrappedBitVector<true>& op) const
284
{
285
5030
  return !(signedLessThanEq(op));
286
}
287
288
template <>
289
452
CVC4Prop wrappedBitVector<false>::operator<=(
290
    const wrappedBitVector<false>& op) const
291
{
292
452
  return unsignedLessThanEq(op);
293
}
294
295
template <>
296
4686
CVC4Prop wrappedBitVector<false>::operator>=(
297
    const wrappedBitVector<false>& op) const
298
{
299
4686
  return !(unsignedLessThan(op));
300
}
301
302
template <>
303
1302
CVC4Prop wrappedBitVector<false>::operator<(
304
    const wrappedBitVector<false>& op) const
305
{
306
1302
  return unsignedLessThan(op);
307
}
308
309
template <>
310
37
CVC4Prop wrappedBitVector<false>::operator>(
311
    const wrappedBitVector<false>& op) const
312
{
313
37
  return !(unsignedLessThanEq(op));
314
}
315
316
/*** Type conversion ***/
317
// CVC4 nodes make no distinction between signed and unsigned, thus ...
318
template <bool isSigned>
319
1460
wrappedBitVector<true> wrappedBitVector<isSigned>::toSigned(void) const
320
{
321
1460
  return wrappedBitVector<true>(*this);
322
}
323
324
template <bool isSigned>
325
30328
wrappedBitVector<false> wrappedBitVector<isSigned>::toUnsigned(void) const
326
{
327
30328
  return wrappedBitVector<false>(*this);
328
}
329
330
/*** Bit hacks ***/
331
332
template <bool isSigned>
333
75552
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extend(
334
    CVC4BitWidth extension) const
335
{
336
  if (isSigned)
337
  {
338
17233
    return BitVector::signExtend(extension);
339
  }
340
  else
341
  {
342
58319
    return BitVector::zeroExtend(extension);
343
  }
344
}
345
346
template <bool isSigned>
347
1833
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::contract(
348
    CVC4BitWidth reduction) const
349
{
350
1833
  Assert(getWidth() > reduction);
351
352
1833
  return extract((getWidth() - 1) - reduction, 0);
353
}
354
355
template <bool isSigned>
356
24569
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::resize(
357
    CVC4BitWidth newSize) const
358
{
359
24569
  CVC4BitWidth width = getWidth();
360
361
24569
  if (newSize > width)
362
  {
363
24569
    return extend(newSize - width);
364
  }
365
  else if (newSize < width)
366
  {
367
    return contract(width - newSize);
368
  }
369
  else
370
  {
371
    return *this;
372
  }
373
}
374
375
template <bool isSigned>
376
31152
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::matchWidth(
377
    const wrappedBitVector<isSigned>& op) const
378
{
379
31152
  Assert(getWidth() <= op.getWidth());
380
31152
  return extend(op.getWidth() - getWidth());
381
}
382
383
template <bool isSigned>
384
17550
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::append(
385
    const wrappedBitVector<isSigned>& op) const
386
{
387
17550
  return BitVector::concat(op);
388
}
389
390
// Inclusive of end points, thus if the same, extracts just one bit
391
template <bool isSigned>
392
55004
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extract(
393
    CVC4BitWidth upper, CVC4BitWidth lower) const
394
{
395
55004
  Assert(upper >= lower);
396
55004
  return BitVector::extract(upper, lower);
397
}
398
399
// Explicit instantiation
400
template class wrappedBitVector<true>;
401
template class wrappedBitVector<false>;
402
403
3624
traits::rm traits::RNE(void) { return ::CVC4::ROUND_NEAREST_TIES_TO_EVEN; };
404
2077
traits::rm traits::RNA(void) { return ::CVC4::ROUND_NEAREST_TIES_TO_AWAY; };
405
1855
traits::rm traits::RTP(void) { return ::CVC4::ROUND_TOWARD_POSITIVE; };
406
3262
traits::rm traits::RTN(void) { return ::CVC4::ROUND_TOWARD_NEGATIVE; };
407
1641
traits::rm traits::RTZ(void) { return ::CVC4::ROUND_TOWARD_ZERO; };
408
// This is a literal back-end so props are actually bools
409
// so these can be handled in the same way as the internal assertions above
410
411
60684
void traits::precondition(const traits::prop& p)
412
{
413
60684
  Assert(p);
414
60684
  return;
415
}
416
12843
void traits::postcondition(const traits::prop& p)
417
{
418
12843
  Assert(p);
419
12843
  return;
420
}
421
62341
void traits::invariant(const traits::prop& p)
422
{
423
62341
  Assert(p);
424
62341
  return;
425
}
426
}  // namespace symfpuLiteral
427
428
26685
}  // namespace CVC4