aboutsummaryrefslogtreecommitdiffstats
path: root/runtime
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-04-08 21:45:42 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-04-08 21:45:42 +0200
commit63915fbebe707cc1de7c0ed5a24148cac45a742c (patch)
treeda503cba224f14281a2ee841930b8843459cb42b /runtime
parentf78d61faf3db94ac1704ce0d11291211b5307629 (diff)
parente326ed9f28a2ed6869f0cb356ef9a8e189cb0a47 (diff)
downloadcompcert-kvx-63915fbebe707cc1de7c0ed5a24148cac45a742c.tar.gz
compcert-kvx-63915fbebe707cc1de7c0ed5a24148cac45a742c.zip
Merge remote-tracking branch 'origin/mppa-work' into mppa-thread
Diffstat (limited to 'runtime')
-rw-r--r--runtime/arm/i64_stof.S9
-rw-r--r--runtime/include/math.h7
-rw-r--r--runtime/powerpc/i64_stof.s17
-rw-r--r--runtime/powerpc/i64_utof.s10
-rw-r--r--runtime/powerpc64/i64_utof.s10
5 files changed, 29 insertions, 24 deletions
diff --git a/runtime/arm/i64_stof.S b/runtime/arm/i64_stof.S
index bcfa471c..11e00a2a 100644
--- a/runtime/arm/i64_stof.S
+++ b/runtime/arm/i64_stof.S
@@ -39,12 +39,11 @@
@@@ Conversion from signed 64-bit integer to single float
FUNCTION(__compcert_i64_stof)
- @ Check whether -2^53 <= X < 2^53
- ASR r2, Reg0HI, #21
- ASR r3, Reg0HI, #31 @ (r2,r3) = X >> 53
+ @ Check whether -2^53 <= X < 2^53
+ ASR r2, Reg0HI, #21 @ r2 = high 32 bits of X >> 53
+ @ -2^53 <= X < 2^53 iff r2 is -1 or 0, that is, iff r2 + 1 is 0 or 1
adds r2, r2, #1
- adc r3, r3, #0 @ (r2,r3) = X >> 53 + 1
- cmp r3, #2
+ cmp r2, #2
blo 1f
@ X is large enough that double rounding can occur.
@ Avoid it by nudging X away from the points where double rounding
diff --git a/runtime/include/math.h b/runtime/include/math.h
index d6475df1..01b8d8d8 100644
--- a/runtime/include/math.h
+++ b/runtime/include/math.h
@@ -1,6 +1,8 @@
#ifndef _COMPCERT_MATH_H
#define _COMPCERT_MATH_H
+#ifdef __K1C__
+
#define isfinite(__y) (fpclassify((__y)) >= FP_ZERO)
#include_next <math.h>
@@ -16,4 +18,9 @@
#define fmaf(x, y, z) __builtin_fmaf((x),(y),(z))
#endif
+#else
+
+#include_next <math.h>
+
+#endif
#endif
diff --git a/runtime/powerpc/i64_stof.s b/runtime/powerpc/i64_stof.s
index 97fa6bb8..ea23a1c8 100644
--- a/runtime/powerpc/i64_stof.s
+++ b/runtime/powerpc/i64_stof.s
@@ -43,20 +43,19 @@
__compcert_i64_stof:
mflr r9
# Check whether -2^53 <= X < 2^53
- srawi r5, r3, 31
- srawi r6, r3, 21 # (r5,r6) = X >> 53
- addic r6, r6, 1
- addze r5, r5 # (r5,r6) = (X >> 53) + 1
+ srawi r5, r3, 21 # r5 = high 32 bits of X >> 53
+ # -2^53 <= X < 2^53 iff r5 is -1 or 0, that is, iff r5 + 1 is 0 or 1
+ addi r5, r5, 1
cmplwi r5, 2
blt 1f
# X is large enough that double rounding can occur.
# Avoid it by nudging X away from the points where double rounding
# occurs (the "round to odd" technique)
- rlwinm r0, r4, 0, 21, 31 # extract bits 0 to 11 of X
- addi r0, r0, 0x7FF # r0 = (X & 0x7FF) + 0x7FF
- # bit 12 of r0 is 0 if all low 12 bits of X are 0, 1 otherwise
- # bits 13-31 of r0 are 0
- or r4, r4, r0 # correct bit number 12 of X
+ rlwinm r5, r4, 0, 21, 31 # extract bits 0 to 11 of X
+ addi r5, r5, 0x7FF # r5 = (X & 0x7FF) + 0x7FF
+ # bit 12 of r5 is 0 if all low 12 bits of X are 0, 1 otherwise
+ # bits 13-31 of r5 are 0
+ or r4, r4, r5 # correct bit number 12 of X
rlwinm r4, r4, 0, 0, 20 # set to 0 bits 0 to 11 of X
# Convert to double, then round to single
1: bl __compcert_i64_stod
diff --git a/runtime/powerpc/i64_utof.s b/runtime/powerpc/i64_utof.s
index cdb2f867..4a2a172b 100644
--- a/runtime/powerpc/i64_utof.s
+++ b/runtime/powerpc/i64_utof.s
@@ -48,11 +48,11 @@ __compcert_i64_utof:
# X is large enough that double rounding can occur.
# Avoid it by nudging X away from the points where double rounding
# occurs (the "round to odd" technique)
- rlwinm r0, r4, 0, 21, 31 # extract bits 0 to 11 of X
- addi r0, r0, 0x7FF # r0 = (X & 0x7FF) + 0x7FF
- # bit 12 of r0 is 0 if all low 12 bits of X are 0, 1 otherwise
- # bits 13-31 of r0 are 0
- or r4, r4, r0 # correct bit number 12 of X
+ rlwinm r5, r4, 0, 21, 31 # extract bits 0 to 11 of X
+ addi r5, r5, 0x7FF # r5 = (X & 0x7FF) + 0x7FF
+ # bit 12 of r5 is 0 if all low 12 bits of X are 0, 1 otherwise
+ # bits 13-31 of r5 are 0
+ or r4, r4, r5 # correct bit number 12 of X
rlwinm r4, r4, 0, 0, 20 # set to 0 bits 0 to 11 of X
# Convert to double, then round to single
1: bl __compcert_i64_utod
diff --git a/runtime/powerpc64/i64_utof.s b/runtime/powerpc64/i64_utof.s
index cdb2f867..4a2a172b 100644
--- a/runtime/powerpc64/i64_utof.s
+++ b/runtime/powerpc64/i64_utof.s
@@ -48,11 +48,11 @@ __compcert_i64_utof:
# X is large enough that double rounding can occur.
# Avoid it by nudging X away from the points where double rounding
# occurs (the "round to odd" technique)
- rlwinm r0, r4, 0, 21, 31 # extract bits 0 to 11 of X
- addi r0, r0, 0x7FF # r0 = (X & 0x7FF) + 0x7FF
- # bit 12 of r0 is 0 if all low 12 bits of X are 0, 1 otherwise
- # bits 13-31 of r0 are 0
- or r4, r4, r0 # correct bit number 12 of X
+ rlwinm r5, r4, 0, 21, 31 # extract bits 0 to 11 of X
+ addi r5, r5, 0x7FF # r5 = (X & 0x7FF) + 0x7FF
+ # bit 12 of r5 is 0 if all low 12 bits of X are 0, 1 otherwise
+ # bits 13-31 of r5 are 0
+ or r4, r4, r5 # correct bit number 12 of X
rlwinm r4, r4, 0, 0, 20 # set to 0 bits 0 to 11 of X
# Convert to double, then round to single
1: bl __compcert_i64_utod