aboutsummaryrefslogtreecommitdiffstats
path: root/runtime
diff options
context:
space:
mode:
Diffstat (limited to 'runtime')
-rw-r--r--runtime/Makefile18
-rw-r--r--runtime/README4
-rw-r--r--runtime/powerpc/ppc64/i64_dtos.s52
-rw-r--r--runtime/powerpc/ppc64/i64_sar.s51
-rw-r--r--runtime/powerpc/ppc64/i64_sdiv.s52
-rw-r--r--runtime/powerpc/ppc64/i64_shl.s50
-rw-r--r--runtime/powerpc/ppc64/i64_shr.s51
-rw-r--r--runtime/powerpc/ppc64/i64_stod.s50
-rw-r--r--runtime/powerpc/ppc64/i64_udiv.s51
-rw-r--r--runtime/powerpc/ppc64/i64_umod.s53
-rw-r--r--runtime/powerpc64/i64_dtou.s (renamed from runtime/powerpc/ppc64/i64_dtou.s)0
-rw-r--r--runtime/powerpc64/i64_stof.s (renamed from runtime/powerpc/ppc64/i64_stof.s)0
-rw-r--r--runtime/powerpc64/i64_utod.s (renamed from runtime/powerpc/ppc64/i64_utod.s)0
-rw-r--r--runtime/powerpc64/i64_utof.s (renamed from runtime/powerpc/ppc64/i64_smod.s)40
-rw-r--r--runtime/powerpc64/vararg.s163
15 files changed, 200 insertions, 435 deletions
diff --git a/runtime/Makefile b/runtime/Makefile
index b819991d..213779a4 100644
--- a/runtime/Makefile
+++ b/runtime/Makefile
@@ -10,8 +10,18 @@ ARCH=x86_32
endif
endif
+ifeq ($(ARCH),powerpc)
+ifeq ($(MODEL),ppc64)
+ARCH=powerpc64
+else ifeq ($(MODEL),e5500)
+ARCH=powerpc64
+endif
+endif
+
ifeq ($(ARCH),x86_64)
OBJS=i64_dtou.o i64_utod.o i64_utof.o vararg.o
+else ifeq ($(ARCH),powerpc64)
+OBJS=i64_dtou.o i64_stof.o i64_utod.o i64_utof.o vararg.o
else
OBJS=i64_dtos.o i64_dtou.o i64_sar.o i64_sdiv.o i64_shl.o \
i64_shr.o i64_smod.o i64_stod.o i64_stof.o \
@@ -28,14 +38,6 @@ INCLUDES=include/float.h include/stdarg.h include/stdbool.h \
VPATH=$(ARCH)
-ifeq ($(ARCH),powerpc)
-ifeq ($(MODEL),ppc64)
-VPATH=powerpc/ppc64 $(ARCH)
-else ifeq ($(MODEL),e5500)
-VPATH=powerpc/ppc64 $(ARCH)
-endif
-endif
-
ifeq ($(strip $(HAS_RUNTIME_LIB)),true)
all: $(LIB)
else
diff --git a/runtime/README b/runtime/README
index 5d824300..f38ed894 100644
--- a/runtime/README
+++ b/runtime/README
@@ -1,11 +1,11 @@
This is the support library for CompCert-generated code.
+
It provides helper functions for:
- 64-bit integer arithmetic
- implementing the va_arg macro from <stdarg.h>
The implementation is written in assembly language in the
-arm/ ia32/ powerpc/ directories.
+arm/ powerpc/ powerpc64/ riscV/ x86_32/ x86_64/ directories.
The c/ directory contains a C implementation of the 64-bit integer functions.
It is provided for reference and as a guide for the asm implementations.
-
diff --git a/runtime/powerpc/ppc64/i64_dtos.s b/runtime/powerpc/ppc64/i64_dtos.s
deleted file mode 100644
index 95f7f700..00000000
--- a/runtime/powerpc/ppc64/i64_dtos.s
+++ /dev/null
@@ -1,52 +0,0 @@
-# *****************************************************************
-#
-# The Compcert verified compiler
-#
-# Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-# en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-# * Redistributions of source code must retain the above copyright
-# notice, this list of conditions and the following disclaimer.
-# * Redistributions in binary form must reproduce the above copyright
-# notice, this list of conditions and the following disclaimer in the
-# documentation and/or other materials provided with the distribution.
-# * Neither the name of the <organization> nor the
-# names of its contributors may be used to endorse or promote products
-# derived from this software without specific prior written permission.
-#
-# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
-# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
-# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
-# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
-# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
-# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
-# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
-# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
-# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
-# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
-# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-#
-# *********************************************************************
-
-# Helper functions for 64-bit integer arithmetic. PowerPC 64 version.
-
- .text
-
-### Conversion from double float to signed long
-
- .balign 16
- .globl __i64_dtos
-__i64_dtos:
- fctidz f1, f1
- stfdu f1, -16(r1)
- lwz r3, 0(r1)
- lwz r4, 4(r1)
- addi r1, r1, 16
- blr
- .type __i64_dtos, @function
- .size __i64_dtos, .-__i64_dtos
- \ No newline at end of file
diff --git a/runtime/powerpc/ppc64/i64_sar.s b/runtime/powerpc/ppc64/i64_sar.s
deleted file mode 100644
index 4fc4451e..00000000
--- a/runtime/powerpc/ppc64/i64_sar.s
+++ /dev/null
@@ -1,51 +0,0 @@
-# *****************************************************************
-#
-# The Compcert verified compiler
-#
-# Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-# en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-# * Redistributions of source code must retain the above copyright
-# notice, this list of conditions and the following disclaimer.
-# * Redistributions in binary form must reproduce the above copyright
-# notice, this list of conditions and the following disclaimer in the
-# documentation and/or other materials provided with the distribution.
-# * Neither the name of the <organization> nor the
-# names of its contributors may be used to endorse or promote products
-# derived from this software without specific prior written permission.
-#
-# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
-# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
-# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
-# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
-# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
-# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
-# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
-# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
-# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
-# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
-# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-#
-# *********************************************************************
-
-# Helper functions for 64-bit integer arithmetic. PowerPC 64 version.
-
- .text
-
-# Shift right signed
-
- .balign 16
- .globl __i64_sar
-__i64_sar:
- rldimi r4, r3, 32, 0 # reassemble (r3,r4) as a 64-bit integer in r4
- srad r4, r4, r5
- srdi r3, r4, 32 # split r4 into (r3,r4)
- blr
- .type __i64_sar, @function
- .size __i64_sar, .-__i64_sar
-
- \ No newline at end of file
diff --git a/runtime/powerpc/ppc64/i64_sdiv.s b/runtime/powerpc/ppc64/i64_sdiv.s
deleted file mode 100644
index 2bf5b574..00000000
--- a/runtime/powerpc/ppc64/i64_sdiv.s
+++ /dev/null
@@ -1,52 +0,0 @@
-# *****************************************************************
-#
-# The Compcert verified compiler
-#
-# Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-# en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-# * Redistributions of source code must retain the above copyright
-# notice, this list of conditions and the following disclaimer.
-# * Redistributions in binary form must reproduce the above copyright
-# notice, this list of conditions and the following disclaimer in the
-# documentation and/or other materials provided with the distribution.
-# * Neither the name of the <organization> nor the
-# names of its contributors may be used to endorse or promote products
-# derived from this software without specific prior written permission.
-#
-# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
-# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
-# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
-# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
-# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
-# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
-# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
-# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
-# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
-# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
-# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-#
-# *********************************************************************
-
-# Helper functions for 64-bit integer arithmetic. PowerPC 64 version.
-
- .text
-
-### Signed division
-
- .balign 16
- .globl __i64_sdiv
-__i64_sdiv:
- rldimi r4, r3, 32, 0 # reassemble (r3,r4) as a 64-bit integer in r4
- rldimi r6, r5, 32, 0 # reassemble (r5,r6) as a 64-bit integer in r6
- divd r4, r4, r6
- srdi r3, r4, 32 # split r4 into (r3,r4)
- blr
- .type __i64_sdiv, @function
- .size __i64_sdiv, .-__i64_sdiv
-
- \ No newline at end of file
diff --git a/runtime/powerpc/ppc64/i64_shl.s b/runtime/powerpc/ppc64/i64_shl.s
deleted file mode 100644
index 955de565..00000000
--- a/runtime/powerpc/ppc64/i64_shl.s
+++ /dev/null
@@ -1,50 +0,0 @@
-# *****************************************************************
-#
-# The Compcert verified compiler
-#
-# Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-# en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-# * Redistributions of source code must retain the above copyright
-# notice, this list of conditions and the following disclaimer.
-# * Redistributions in binary form must reproduce the above copyright
-# notice, this list of conditions and the following disclaimer in the
-# documentation and/or other materials provided with the distribution.
-# * Neither the name of the <organization> nor the
-# names of its contributors may be used to endorse or promote products
-# derived from this software without specific prior written permission.
-#
-# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
-# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
-# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
-# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
-# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
-# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
-# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
-# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
-# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
-# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
-# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-#
-# *********************************************************************
-
-# Helper functions for 64-bit integer arithmetic. PowerPC 64 version.
-
- .text
-
-# Shift left
-
- .balign 16
- .globl __i64_shl
-__i64_shl:
- rldimi r4, r3, 32, 0 # reassemble (r3,r4) as a 64-bit integer in r4
- sld r4, r4, r5
- srdi r3, r4, 32 # split r4 into (r3,r4)
- blr
- .type __i64_shl, @function
- .size __i64_shl, .-__i64_shl
- \ No newline at end of file
diff --git a/runtime/powerpc/ppc64/i64_shr.s b/runtime/powerpc/ppc64/i64_shr.s
deleted file mode 100644
index ca5ac9b2..00000000
--- a/runtime/powerpc/ppc64/i64_shr.s
+++ /dev/null
@@ -1,51 +0,0 @@
-# *****************************************************************
-#
-# The Compcert verified compiler
-#
-# Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-# en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-# * Redistributions of source code must retain the above copyright
-# notice, this list of conditions and the following disclaimer.
-# * Redistributions in binary form must reproduce the above copyright
-# notice, this list of conditions and the following disclaimer in the
-# documentation and/or other materials provided with the distribution.
-# * Neither the name of the <organization> nor the
-# names of its contributors may be used to endorse or promote products
-# derived from this software without specific prior written permission.
-#
-# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
-# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
-# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
-# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
-# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
-# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
-# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
-# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
-# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
-# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
-# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-#
-# *********************************************************************
-
-# Helper functions for 64-bit integer arithmetic. PowerPC 64 version.
-
- .text
-
-# Shift right unsigned
-
- .balign 16
- .globl __i64_shr
-__i64_shr:
- rldimi r4, r3, 32, 0 # reassemble (r3,r4) as a 64-bit integer in r4
- srd r4, r4, r5
- srdi r3, r4, 32 # split r4 into (r3,r4)
- blr
- .type __i64_shr, @function
- .size __i64_shr, .-__i64_shr
-
- \ No newline at end of file
diff --git a/runtime/powerpc/ppc64/i64_stod.s b/runtime/powerpc/ppc64/i64_stod.s
deleted file mode 100644
index 3636d0b5..00000000
--- a/runtime/powerpc/ppc64/i64_stod.s
+++ /dev/null
@@ -1,50 +0,0 @@
-# *****************************************************************
-#
-# The Compcert verified compiler
-#
-# Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-# en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-# * Redistributions of source code must retain the above copyright
-# notice, this list of conditions and the following disclaimer.
-# * Redistributions in binary form must reproduce the above copyright
-# notice, this list of conditions and the following disclaimer in the
-# documentation and/or other materials provided with the distribution.
-# * Neither the name of the <organization> nor the
-# names of its contributors may be used to endorse or promote products
-# derived from this software without specific prior written permission.
-#
-# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
-# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
-# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
-# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
-# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
-# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
-# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
-# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
-# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
-# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
-# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-#
-# *********************************************************************
-
-# Helper functions for 64-bit integer arithmetic. PowerPC 64 version.
-
-### Conversion from signed long to double float
-
- .balign 16
- .globl __i64_stod
-__i64_stod:
- rldimi r4, r3, 32, 0 # reassemble (r3,r4) as a 64-bit integer in r4
- stdu r4, -16(r1)
- lfd f1, 0(r1)
- fcfid f1, f1
- addi r1, r1, 16
- blr
- .type __i64_stod, @function
- .size __i64_stod, .-__i64_stod
-
diff --git a/runtime/powerpc/ppc64/i64_udiv.s b/runtime/powerpc/ppc64/i64_udiv.s
deleted file mode 100644
index a6a3bcb3..00000000
--- a/runtime/powerpc/ppc64/i64_udiv.s
+++ /dev/null
@@ -1,51 +0,0 @@
-# *****************************************************************
-#
-# The Compcert verified compiler
-#
-# Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-# en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-# * Redistributions of source code must retain the above copyright
-# notice, this list of conditions and the following disclaimer.
-# * Redistributions in binary form must reproduce the above copyright
-# notice, this list of conditions and the following disclaimer in the
-# documentation and/or other materials provided with the distribution.
-# * Neither the name of the <organization> nor the
-# names of its contributors may be used to endorse or promote products
-# derived from this software without specific prior written permission.
-#
-# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
-# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
-# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
-# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
-# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
-# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
-# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
-# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
-# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
-# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
-# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-#
-# *********************************************************************
-
-# Helper functions for 64-bit integer arithmetic. PowerPC 64 version.
-
- .text
-
-### Unsigned division
-
- .balign 16
- .globl __i64_udiv
-__i64_udiv:
- rldimi r4, r3, 32, 0 # reassemble (r3,r4) as a 64-bit integer in r4
- rldimi r6, r5, 32, 0 # reassemble (r5,r6) as a 64-bit integer in r6
- divdu r4, r4, r6
- srdi r3, r4, 32 # split r4 into (r3,r4)
- blr
- .type __i64_udiv, @function
- .size __i64_udiv, .-__i64_udiv
-
diff --git a/runtime/powerpc/ppc64/i64_umod.s b/runtime/powerpc/ppc64/i64_umod.s
deleted file mode 100644
index 6bda1903..00000000
--- a/runtime/powerpc/ppc64/i64_umod.s
+++ /dev/null
@@ -1,53 +0,0 @@
-# *****************************************************************
-#
-# The Compcert verified compiler
-#
-# Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-# en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-# * Redistributions of source code must retain the above copyright
-# notice, this list of conditions and the following disclaimer.
-# * Redistributions in binary form must reproduce the above copyright
-# notice, this list of conditions and the following disclaimer in the
-# documentation and/or other materials provided with the distribution.
-# * Neither the name of the <organization> nor the
-# names of its contributors may be used to endorse or promote products
-# derived from this software without specific prior written permission.
-#
-# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
-# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
-# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
-# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
-# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
-# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
-# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
-# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
-# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
-# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
-# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-#
-# *********************************************************************
-
-# Helper functions for 64-bit integer arithmetic. PowerPC 64 version.
-
- .text
-
-### Unsigned modulus
-
- .balign 16
- .globl __i64_umod
-__i64_umod:
- rldimi r4, r3, 32, 0 # reassemble (r3,r4) as a 64-bit integer in r4
- rldimi r6, r5, 32, 0 # reassemble (r5,r6) as a 64-bit integer in r6
- divdu r0, r4, r6
- mulld r0, r0, r6
- subf r4, r0, r4
- srdi r3, r4, 32 # split r4 into (r3,r4)
- blr
- .type __i64_umod, @function
- .size __i64_umod, .-__i64_umod
-
diff --git a/runtime/powerpc/ppc64/i64_dtou.s b/runtime/powerpc64/i64_dtou.s
index 60d5c9bf..60d5c9bf 100644
--- a/runtime/powerpc/ppc64/i64_dtou.s
+++ b/runtime/powerpc64/i64_dtou.s
diff --git a/runtime/powerpc/ppc64/i64_stof.s b/runtime/powerpc64/i64_stof.s
index 8830d594..8830d594 100644
--- a/runtime/powerpc/ppc64/i64_stof.s
+++ b/runtime/powerpc64/i64_stof.s
diff --git a/runtime/powerpc/ppc64/i64_utod.s b/runtime/powerpc64/i64_utod.s
index ddde91dd..ddde91dd 100644
--- a/runtime/powerpc/ppc64/i64_utod.s
+++ b/runtime/powerpc64/i64_utod.s
diff --git a/runtime/powerpc/ppc64/i64_smod.s b/runtime/powerpc64/i64_utof.s
index 35be366d..2617cbda 100644
--- a/runtime/powerpc/ppc64/i64_smod.s
+++ b/runtime/powerpc64/i64_utof.s
@@ -32,23 +32,33 @@
#
# *********************************************************************
-# Helper functions for 64-bit integer arithmetic. PowerPC 64 version.
+# Helper functions for 64-bit integer arithmetic. PowerPC version.
.text
-## Signed remainder
-
+### Conversion from unsigned long to single float
+
.balign 16
- .globl __i64_smod
-__i64_smod:
- rldimi r4, r3, 32, 0 # reassemble (r3,r4) as a 64-bit integer in r4
- rldimi r6, r5, 32, 0 # reassemble (r5,r6) as a 64-bit integer in r6
- divd r0, r4, r6
- mulld r0, r0, r6
- subf r4, r0, r4
- srdi r3, r4, 32 # split r4 into (r3,r4)
+ .globl __i64_utof
+__i64_utof:
+ mflr r9
+ # Check whether X < 2^53
+ andis. r0, r3, 0xFFE0 # test bits 53...63 of X
+ beq 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 r4, r4, 0, 0, 20 # set to 0 bits 0 to 11 of X
+ # Convert to double, then round to single
+1: bl __i64_utod
+ mtlr r9
+ frsp f1, f1
blr
- .type __i64_smod, @function
- .size __i64_smod, .-__i64_smod
-
- \ No newline at end of file
+ .type __i64_utof, @function
+ .size __i64_utof, .-__i64_utof
+
diff --git a/runtime/powerpc64/vararg.s b/runtime/powerpc64/vararg.s
new file mode 100644
index 00000000..8d7e62c8
--- /dev/null
+++ b/runtime/powerpc64/vararg.s
@@ -0,0 +1,163 @@
+# *****************************************************************
+#
+# The Compcert verified compiler
+#
+# Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+# en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+# * Redistributions of source code must retain the above copyright
+# notice, this list of conditions and the following disclaimer.
+# * Redistributions in binary form must reproduce the above copyright
+# notice, this list of conditions and the following disclaimer in the
+# documentation and/or other materials provided with the distribution.
+# * Neither the name of the <organization> nor the
+# names of its contributors may be used to endorse or promote products
+# derived from this software without specific prior written permission.
+#
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for variadic functions <stdarg.h>. IA32 version
+
+# typedef struct {
+# unsigned char ireg; // index of next integer register
+# unsigned char freg; // index of next FP register
+# char * stk; // pointer to next argument in stack
+# struct {
+# int iregs[8];
+# double fregs[8];
+# } * regs; // pointer to saved register area
+# } va_list[1];
+#
+# unsigned int __compcert_va_int32(va_list ap);
+# unsigned long long __compcert_va_int64(va_list ap);
+# double __compcert_va_float64(va_list ap);
+
+ .text
+
+ .balign 16
+ .globl __compcert_va_int32
+__compcert_va_int32:
+ # r3 = ap = address of va_list structure
+ lbz r4, 0(r3) # r4 = ap->ireg = next integer register
+ cmplwi r4, 8
+ bge 1f
+ # Next argument was passed in an integer register
+ lwz r5, 8(r3) # r5 = ap->regs = base of saved register area
+ rlwinm r6, r4, 2, 0, 29 # r6 = r4 * 4
+ addi r4, r4, 1 # increment ap->ireg
+ stb r4, 0(r3)
+ lwzx r3, r5, r6 # load argument in r3
+ blr
+ # Next argument was passed on stack
+1: lwz r5, 4(r3) # r5 = ap->stk = next argument passed on stack
+ addi r5, r5, 4 # advance ap->stk by 4
+ stw r5, 4(r3)
+ lwz r3, -4(r5) # load argument in r3
+ blr
+ .type __compcert_va_int32, @function
+ .size __compcert_va_int32, .-__compcert_va_int32
+
+ .balign 16
+ .globl __compcert_va_int64
+__compcert_va_int64:
+ # r3 = ap = address of va_list structure
+ lbz r4, 0(r3) # r4 = ap->ireg = next integer register
+ cmplwi r4, 7
+ bge 1f
+ # Next argument was passed in two consecutive integer register
+ lwz r5, 8(r3) # r5 = ap->regs = base of saved register area
+ addi r4, r4, 3 # round r4 up to an even number and add 2
+ rlwinm r4, r4, 0, 0, 30
+ rlwinm r6, r4, 2, 0, 29 # r6 = r4 * 4
+ add r5, r5, r6 # r5 = address of argument + 8
+ stb r4, 0(r3) # update ap->ireg
+ lwz r3, -8(r5) # load argument in r3:r4
+ lwz r4, -4(r5)
+ blr
+ # Next argument was passed on stack
+1: lwz r5, 4(r3) # r5 = ap->stk = next argument passed on stack
+ li r4, 8
+ stb r4, 0(r3) # set ap->ireg = 8 so that no ireg is left
+ addi r5, r5, 15 # round r5 to a multiple of 8 and add 8
+ rlwinm r5, r5, 0, 0, 28
+ stw r5, 4(r3) # update ap->stk
+ lwz r3, -8(r5) # load argument in r3:r4
+ lwz r4, -4(r5)
+ blr
+ .type __compcert_va_int64, @function
+ .size __compcert_va_int64, .-__compcert_va_int64
+
+ .balign 16
+ .globl __compcert_va_float64
+__compcert_va_float64:
+ # r3 = ap = address of va_list structure
+ lbz r4, 1(r3) # r4 = ap->freg = next float register
+ cmplwi r4, 8
+ bge 1f
+ # Next argument was passed in a FP register
+ lwz r5, 8(r3) # r5 = ap->regs = base of saved register area
+ rlwinm r6, r4, 3, 0, 28 # r6 = r4 * 8
+ add r5, r5, r6
+ lfd f1, 32(r5) # load argument in f1
+ addi r4, r4, 1 # increment ap->freg
+ stb r4, 1(r3)
+ blr
+ # Next argument was passed on stack
+1: lwz r5, 4(r3) # r5 = ap->stk = next argument passed on stack
+ addi r5, r5, 15 # round r5 to a multiple of 8 and add 8
+ rlwinm r5, r5, 0, 0, 28
+ lfd f1, -8(r5) # load argument in f1
+ stw r5, 4(r3) # update ap->stk
+ blr
+ .type __compcert_va_float64, @function
+ .size __compcert_va_float64, .-__compcert_va_int64
+
+ .balign 16
+ .globl __compcert_va_composite
+__compcert_va_composite:
+ b __compcert_va_int32
+ .type __compcert_va_composite, @function
+ .size __compcert_va_composite, .-__compcert_va_composite
+
+# Save integer and FP registers at beginning of vararg function
+
+ .balign 16
+ .globl __compcert_va_saveregs
+__compcert_va_saveregs:
+ lwz r11, 0(r1) # r11 point to top of our frame
+ stwu r3, -96(r11) # register save area is 96 bytes below
+ stw r4, 4(r11)
+ stw r5, 8(r11)
+ stw r6, 12(r11)
+ stw r7, 16(r11)
+ stw r8, 20(r11)
+ stw r9, 24(r11)
+ stw r10, 28(r11)
+ bf 6, 1f # don't save FP regs if CR6 bit is clear
+ stfd f1, 32(r11)
+ stfd f2, 40(r11)
+ stfd f3, 48(r11)
+ stfd f4, 56(r11)
+ stfd f5, 64(r11)
+ stfd f6, 72(r11)
+ stfd f7, 80(r11)
+ stfd f8, 88(r11)
+1: blr
+ .type __compcert_va_saveregs, @function
+ .size __compcert_va_saveregs, .-__compcert_va_saveregs