Expand 64-bit integer comparisons into 32-bit integer comparisons.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2218 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

8 files changed, 2 insertions, 392 deletions

diff --git a/runtime/Makefile b/runtime/Makefile
index 3565fb1..a2af8d5 100644
--- a/runtime/Makefile
+++ b/runtime/Makefile
@@ -2,8 +2,8 @@ include ../Makefile.config
 
 CFLAGS=-O1 -g -Wall
 INCLUDES=
-OBJS=i64_dtos.o i64_dtou.o i64_sar.o i64_scmp.o i64_sdiv.o i64_shl.o \
-  i64_shr.o i64_smod.o i64_stod.o i64_ucmp.o i64_udivmod.o i64_udiv.o \
+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_udivmod.o i64_udiv.o \
   i64_umod.o i64_utod.o
 LIB=libcompcert.a
 
diff --git a/runtime/arm/i64_scmp.s b/runtime/arm/i64_scmp.s
deleted file mode 100644
index 144a13c..0000000
--- a/runtime/arm/i64_scmp.s
+++ /dev/null
@@ -1,56 +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.  ARM version.
-
-        .text
-
-@@@ Signed comparison	
-	
-	.global __i64_scmp
-__i64_scmp:
-        cmp r0, r2              @ compare low words (unsigned)
-        moveq r0, #0            @ res = 0 if eq
-        movhi r0, #1            @ res = 1 if unsigned higher
-        mvnlo r0, #0            @ res = -1 if unsigned lower
-        cmp r1, r3              @ compare high words (signed)
-	addgt r0, r0, #2        @ res += 2 if signed greater
-	sublt r0, r0, #2        @ res -= 2 if signed less
-   @ here, r0 = 0 if X == Y
-   @       r0 = -3, -2, -1 if X < Y
-   @       r0 = 1, 2, 3 if X > Y
-        bx      lr
-	.type __i64_scmp, %function
-	.size __i64_scmp, . - __i64_scmp
-	
diff --git a/runtime/arm/i64_ucmp.s b/runtime/arm/i64_ucmp.s
deleted file mode 100644
index 51a5fdb..0000000
--- a/runtime/arm/i64_ucmp.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.  ARM version.
-
-        .text
-
-@@@ Unsigned comparison	
-	
-	.global __i64_ucmp
-__i64_ucmp:
-        cmp r1, r3      @ compare high words
-        cmpeq r0, r2    @ if equal, compare low words instead
-        moveq r0, #0    @ res = 0 if eq
-        movhi r0, #1    @ res = 1 if unsigned higher
-        mvnlo r0, #0    @ res = -1 if unsigned lower
-        bx lr
-	.type __i64_ucmp, %function
-	.size __i64_ucmp, . - __i64_ucmp
-	
diff --git a/runtime/ia32/i64_scmp.S b/runtime/ia32/i64_scmp.S
deleted file mode 100644
index 93ef2c2..0000000
--- a/runtime/ia32/i64_scmp.S
+++ /dev/null
@@ -1,58 +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.  IA32 version.
-	
-#include "sysdeps.h"
-
-// Signed comparison
-
-FUNCTION(__i64_scmp)
-        movl 8(%esp), %eax              // compare high words (signed)
-        cmpl 16(%esp), %eax
-        je 1f                           // if different,
-        setg %al                        // extract result 
-        setl %dl
-        subb %dl, %al
-        movsbl %al, %eax
-        ret
-1:      movl 4(%esp), %eax              // if high words equal,
-        cmpl 12(%esp), %eax             // compare low words (unsigned)
-        seta %al                        // and extract result
-        setb %dl
-        subb %dl, %al
-        movsbl %al, %eax
-        ret
-ENDFUNCTION(__i64_scmp)
-
diff --git a/runtime/ia32/i64_ucmp.S b/runtime/ia32/i64_ucmp.S
deleted file mode 100644
index 3415986..0000000
--- a/runtime/ia32/i64_ucmp.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.  IA32 version.
-	
-#include "sysdeps.h"
-
-// Unsigned comparison
-
-FUNCTION(__i64_ucmp)
-        movl 8(%esp), %eax              // compare high words
-        cmpl 16(%esp), %eax
-        jne 1f                          // if high words equal,
-        movl 4(%esp), %eax              // compare low words
-        cmpl 12(%esp), %eax
-1:      seta %al                        // AL = 1 if >, 0 if <=
-        setb %dl                        // DL = 1 if <, 0 if >=
-        subb %dl, %al                   // AL = 0 if same, 1 if >, -1 if <
-        movsbl %al, %eax
-        ret
-ENDFUNCTION(__i64_ucmp)
diff --git a/runtime/powerpc/i64_scmp.s b/runtime/powerpc/i64_scmp.s
deleted file mode 100644
index 87811e0..0000000
--- a/runtime/powerpc/i64_scmp.s
+++ /dev/null
@@ -1,72 +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 version.
-
-        .text
-
-### Signed comparison        
-
-        .balign 16
-        .globl __i64_scmp
-__i64_scmp:
-        cmpw cr0, r3, r5        # compare high words (signed)
-	cmplw cr1, r4, r6       # compare low words (unsigned)
-        mfcr r0
-# At this point, the bits of r0 are as follow:	
-#   bit 31: XH < YH
-#   bit 30: XH > YH        
-#   bit 27: XL > YL	
-#   bit 26: XL < YL	
-        rlwinm r3, r0, 0, 0, 1  # r3 = r0 & 0xC000_0000
-        srawi r3, r3, 24        # r4 = r4 >>s 28
-# r3 = -0x80 if XH < YH
-#    = 0x40  if XH > YH
-#    = 0     if XH = YH        
-        rlwinm r4, r0, 4, 0, 1  # r4 = (r0 << 4) & 0xC000_0000
-        srawi r4, r4, 28        # r4 = r4 >>s 28
-# r4 = -8  if XL < YL
-#    =  4  if XL > YL
-#    =  0  if XL = YL        
-	add     r3, r3, r4
-# r3 = -0x80 or -0x80 - 8 or -0x80 + 4 or -8 if X < Y 
-#         (in all cases, r3 < 0 if X < Y)	
-#    = 0x40 or 0x40 - 8 or 0x40 + 4 or 4 if X > Y 
-#         (in all cases, r3 > 0 if X > Y)	
-#    = 0 if X = Y
-        blr
-        .type __i64_scmp, @function
-        .size __i64_scmp, .-__i64_scmp
-	
-        
\ No newline at end of file
diff --git a/runtime/powerpc/i64_ucmp.s b/runtime/powerpc/i64_ucmp.s
deleted file mode 100644
index 708bc74..0000000
--- a/runtime/powerpc/i64_ucmp.s
+++ /dev/null
@@ -1,72 +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 version.
-
-        .text
-
-### Unsigned comparison        
-
-        .balign 16
-        .globl __i64_ucmp
-__i64_ucmp:
-        cmplw cr0, r3, r5       # compare high words (unsigned)
-	cmplw cr1, r4, r6       # compare low words (unsigned)
-        mfcr r0
-# At this point, the bits of r0 are as follow:	
-#   bit 31: XH < YH
-#   bit 30: XH > YH        
-#   bit 27: XL > YL	
-#   bit 26: XL < YL	
-        rlwinm r3, r0, 0, 0, 1  # r3 = r0 & 0xC000_0000
-        srawi r3, r3, 24        # r4 = r4 >>s 28
-# r3 = -0x80 if XH < YH
-#    = 0x40  if XH > YH
-#    = 0     if XH = YH        
-        rlwinm r4, r0, 4, 0, 1  # r4 = (r0 << 4) & 0xC000_0000
-        srawi r4, r4, 28        # r4 = r4 >>s 28
-# r4 = -8  if XL < YL
-#    =  4  if XL > YL
-#    =  0  if XL = YL        
-	add     r3, r3, r4
-# r3 = -0x80 or -0x80 - 8 or -0x80 + 4 or -8 if X < Y 
-#         (in all cases, r3 < 0 if X < Y)	
-#    = 0x40 or 0x40 - 8 or 0x40 + 4 or 4 if X > Y 
-#         (in all cases, r3 > 0 if X > Y)	
-#    = 0 if X = Y
-        blr
-        .type __i64_ucmp, @function
-        .size __i64_ucmp, .-__i64_ucmp
-	
-        
\ No newline at end of file
diff --git a/runtime/test/test_int64.c b/runtime/test/test_int64.c
index 49e732a..0a7dfc4 100644
--- a/runtime/test/test_int64.c
+++ b/runtime/test/test_int64.c
@@ -50,9 +50,6 @@ extern u64 __i64_shl(u64 x, unsigned amount);
 extern u64 __i64_shr(u64 x, unsigned amount);
 extern s64 __i64_sar(s64 x, unsigned amount);
 
-extern int __i64_ucmp(u64 x, u64 y);
-extern int __i64_scmp(s64 x, s64 y);
-
 extern double __i64_utod(u64 x);
 extern double __i64_stod(s64 x);
 extern u64 __i64_dtou(double d);
@@ -140,32 +137,6 @@ static void test1(u64 x, u64 y)
   if (t != (s64) x >> i) 
     error++, printf("%016llx >>s %d = %016llx, expected %016llx\n", x, i, t, (s64) x >> i);
 
-  i = __i64_ucmp(x, y);
-  if (x == y) {
-    if (! (i == 0))
-      error++, printf("ucmp(%016llx, %016llx) = %d, expected 0\n", x, y, i);
-  }
-  else if (x < y) {
-    if (! (i < 0))
-      error++, printf("ucmp(%016llx, %016llx) = %d, expected < 0\n", x, y, i);
-  } else {
-    if (! (i > 0))
-      error++, printf("ucmp(%016llx, %016llx) = %d, expected > 0\n", x, y, i);
-  }
-
-  i = __i64_scmp(x, y);
-  if (x == y) {
-    if (! (i == 0))
-      error++, printf("scmp(%016llx, %016llx) = %d, expected 0\n", x, y, i);
-  }
-  else if ((s64)x < (s64)y) {
-    if (! (i < 0))
-      error++, printf("scmp(%016llx, %016llx) = %d, expected < 0\n", x, y, i);
-  } else {
-    if (! (i > 0))
-      error++, printf("scmp(%016llx, %016llx) = %d, expected > 0\n", x, y, i);
-  }
-
   f = __i64_utod(x);
   g = (double) x;
   if (f != g)