ARM port: add support for Thumb2. To be tested.

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

16 files changed, 316 insertions, 261 deletions

diff --git a/runtime/arm/i64_dtos.S b/runtime/arm/i64_dtos.S
index e454fd4..638a5ff 100644
--- a/runtime/arm/i64_dtos.S
+++ b/runtime/arm/i64_dtos.S
@@ -34,66 +34,67 @@
 
 @ Helper functions for 64-bit integer arithmetic.  ARM version.
 
-        .text
+#include "sysdeps.h"	
 
 @@@ Conversion from double float to signed 64-bit integer
 	
-	.global __i64_dtos
-__i64_dtos:
-#ifdef VARIANT_hardfloat	
-	fmrrd r0, r1, d0
+FUNCTION(__i64_dtos)
+#ifndef VARIANT_eabi
+	vmov r0, r1, d0
 #endif	
-        mov r12, r1, asr #31    @ save sign of result in r12
+        ASR r12, r1, #31       @ save sign of result in r12
   @ extract unbiased exponent ((HI & 0x7FF00000) >> 20) - (1023 + 52) in r2
   @ note: 1023 + 52 = 1075 = 1024 + 51
   @ note: (HI & 0x7FF00000) >> 20 = (HI << 1) >> 21
-        mov r2, r1, lsl #1
-        mov r2, r2, lsr #21
-        sub r2, r2, #51
-        sub r2, r2, #1024
+        LSL r2, r1, #1
+        LSR r2, r2, #21
+        SUB r2, r2, #51
+        SUB r2, r2, #1024
   @ check range of exponent
         cmn r2, #52             @ if EXP < -52, |double| is < 1.0
         blt 1f
         cmp r2, #11             @ if EXP >= 63 - 52, |double| is >= 2^63
         bge 2f
   @ extract true mantissa
-        bic r1, r1, #0xFF000000
-        bic r1, r1, #0x00F00000 @ HI &= ~0xFFF00000
-        orr r1, r1, #0x00100000 @ HI |= 0x00100000
+        BIC r1, r1, #0xFF000000
+        BIC r1, r1, #0x00F00000 @ HI &= ~0xFFF00000
+        ORR r1, r1, #0x00100000 @ HI |= 0x00100000
   @ shift it appropriately
         cmp r2, #0
         blt 3f
   @ EXP >= 0: shift left by EXP.  Note that EXP < 12        
         rsb r3, r2, #32         @ r3 = 32 - amount
-        mov r1, r1, lsl r2
-        orr r1, r1, r0, lsr r3
-        mov r0, r0, lsl r2
+        LSL r1, r1, r2
+        LSR r3, r0, r3
+        ORR r1, r1, r3
+        LSL r0, r0, r2
 	b 4f
   @ EXP < 0: shift right by -EXP.  Note that -EXP <= 52 but can be >= 32        
-3:      rsb r2, r2, #0          @ r2 = -EXP - shift amount
-        rsb r3, r2, #32         @ r3 = 32 - amount
-        mov r0, r0, lsr r2
-        orr r0, r0, r1, lsl r3
-	sub r3, r2, #32         @ r3 = amount - 32  (see i64_shr.s)
-	orr r0, r0, r1, lsr r3
-        mov r1, r1, lsr r2
+3:      RSB r2, r2, #0          @ r2 = -EXP = shift amount
+        RSB r3, r2, #32         @ r3 = 32 - amount
+        LSR r0, r0, r2
+        LSL r3, r1, r3
+        ORR r0, r0, r3
+	SUB r3, r2, #32         @ r3 = amount - 32  (see i64_shr.s)
+	LSR r3, r1, r3
+	ORR r0, r0, r3
+        LSR r1, r1, r2
   @ apply sign to result
-4:      eor r0, r0, r12
-        eor r1, r1, r12
+4:      EOR r0, r0, r12
+        EOR r1, r1, r12
         subs r0, r0, r12
         sbc r1, r1, r12
         bx lr
   @ special cases
-1:      mov r0, #0 @ result is 0
-        mov r1, #0
+1:      MOV r0, #0              @ result is 0
+        MOV r1, #0
         bx lr
-2:      cmp r4, #0
+2:      cmp r12, #0
         blt 6f
         mvn r0, #0              @ result is 0x7F....FF (MAX_SINT)
-        mov r1, r0, lsr #1
+        LSR r1, r0, #1
         bx lr
-6:      mov r0, #0              @ result is 0x80....00 (MIN_SINT)
-        mov r1, #0x80000000
+6:      MOV r0, #0              @ result is 0x80....00 (MIN_SINT)
+        MOV r1, #0x80000000
         bx lr
-	.type __i64_dtos, %function
-        .size __i64_dtos, . - __i64_dtos
+ENDFUNCTION(__i64_dtos)
diff --git a/runtime/arm/i64_dtou.S b/runtime/arm/i64_dtou.S
index a9e7b65..1c632d2 100644
--- a/runtime/arm/i64_dtou.S
+++ b/runtime/arm/i64_dtou.S
@@ -34,58 +34,58 @@
 
 @ Helper functions for 64-bit integer arithmetic.  ARM version.
 
-        .text
+#include "sysdeps.h"
 
 @@@ Conversion from double float to unsigned 64-bit integer	
 
-	.global __i64_dtou
-__i64_dtou:
-#ifdef VARIANT_hardfloat	
-	fmrrd r0, r1, d0
+FUNCTION(__i64_dtou)
+#ifndef VARIANT_eabi
+	vmov r0, r1, d0
 #endif	
         cmp r1, #0              @ is double < 0 ?
         blt 1f                  @ then it converts to 0
   @ extract unbiased exponent ((HI & 0x7FF00000) >> 20) - (1023 + 52) in r2
   @ note: 1023 + 52 = 1075 = 1024 + 51
   @ note: (HI & 0x7FF00000) >> 20 = (HI << 1) >> 21
-        mov r2, r1, lsl #1
-        mov r2, r2, lsr #21
-        sub r2, r2, #51
-        sub r2, r2, #1024
+        LSL r2, r1, #1
+        LSR r2, r2, #21
+        SUB r2, r2, #51
+        SUB r2, r2, #1024
   @ check range of exponent
         cmn r2, #52             @ if EXP < -52, double is < 1.0
         blt 1f
         cmp r2, #12             @ if EXP >= 64 - 52, double is >= 2^64
         bge 2f
   @ extract true mantissa
-        bic r1, r1, #0xFF000000
-        bic r1, r1, #0x00F00000 @ HI &= ~0xFFF00000
-        orr r1, r1, #0x00100000 @ HI |= 0x00100000
+        BIC r1, r1, #0xFF000000
+        BIC r1, r1, #0x00F00000 @ HI &= ~0xFFF00000
+        ORR r1, r1, #0x00100000 @ HI |= 0x00100000
   @ shift it appropriately
         cmp r2, #0
         blt 3f
   @ EXP >= 0: shift left by EXP.  Note that EXP < 12        
         rsb r3, r2, #32         @ r3 = 32 - amount
-        mov r1, r1, lsl r2
-        orr r1, r1, r0, lsr r3
-        mov r0, r0, lsl r2
+        LSL r1, r1, r2
+        LSR r3, r0, r3
+        ORR r1, r1, r3
+        LSL r0, r0, r2
 	bx lr
   @ EXP < 0: shift right by -EXP.  Note that -EXP <= 52 but can be >= 32        
-3:      rsb r2, r2, #0          @ r2 = -EXP - shift amount
-        rsb r3, r2, #32         @ r3 = 32 - amount
-        mov r0, r0, lsr r2
-        orr r0, r0, r1, lsl r3
-	sub r3, r2, #32         @ r3 = amount - 32  (see i64_shr.s)
-	orr r0, r0, r1, lsr r3
-        mov r1, r1, lsr r2
+3:      RSB r2, r2, #0          @ r2 = -EXP = shift amount
+        RSB r3, r2, #32         @ r3 = 32 - amount
+        LSR r0, r0, r2
+        LSL r3, r1, r3
+        ORR r0, r0, r3
+	SUB r3, r2, #32         @ r3 = amount - 32  (see i64_shr.s)
+	LSR r3, r1, r3
+	ORR r0, r0, r3
+        LSR r1, r1, r2
         bx lr
   @ special cases
-1:      mov r0, #0              @ result is 0
-        mov r1, #0
+1:      MOV r0, #0              @ result is 0
+        MOV r1, #0
         bx lr
 2:      mvn r0, #0              @ result is 0xFF....FF (MAX_UINT)
-        mvn r1, #0
+        MOV r1, r0
         bx lr
-	.type __i64_dtou, %function
-        .size __i64_dtou, . - __i64_dtou
-	
+ENDFUNCTION(__i64_dtou)
diff --git a/runtime/arm/i64_sar.s b/runtime/arm/i64_sar.S
index a96d092..1bbd8a7 100644
--- a/runtime/arm/i64_sar.s
+++ b/runtime/arm/i64_sar.S
@@ -34,24 +34,24 @@
 
 @ Helper functions for 64-bit integer arithmetic.  ARM version.
 
-        .text
+#include "sysdeps.h"
 
 @@@ Shift right signed
 
-	.global __i64_sar
-__i64_sar:
-        and r2, r2, #63         @ normalize amount to 0...63
+FUNCTION(__i64_sar)
+        AND r2, r2, #63         @ normalize amount to 0...63
         rsbs r3, r2, #32        @ r3 = 32 - amount
         ble 1f                  @ branch if <= 0, namely if amount >= 32
-        mov r0, r0, lsr r2
-        orr r0, r1, lsl r3
-        mov r1, r1, asr r2
+        LSR r0, r0, r2
+	LSL r3, r1, r3
+        ORR r0, r1, r3
+        ASR r1, r1, r2
         bx lr
 1:
-        sub r2, r2, #32
-        mov r0, r1, asr r2
-        mov r1, r1, asr #31
+        SUB r2, r2, #32
+        ASR r0, r1, r2
+        ASR r1, r1, #31
         bx lr
-	.type __i64_sar, %function
-	.size __i64_sar, . - __i64_sar
+ENDFUNCTION(__i64_sar)
+
 	
diff --git a/runtime/arm/i64_smod.s b/runtime/arm/i64_sdiv.S
index 8e766a0..dd88c12 100644
--- a/runtime/arm/i64_smod.s
+++ b/runtime/arm/i64_sdiv.S
@@ -34,31 +34,28 @@
 
 @ Helper functions for 64-bit integer arithmetic.  ARM version.
 
-        .text
+#include "sysdeps.h"
 
-@@@ Signed modulus	
-
-	.global __i64_smod
-__i64_smod:
+@@@ Signed division	
+	
+FUNCTION(__i64_sdiv)
         push {r4, r5, r6, r7, r8, r10, lr}
-	mov r10, r1              @ r10 = sign of result
-        mov r4, r1, asr#31       @ take absolute value of N
-        eor r0, r0, r4           @ N = (N ^ (N >>s 31)) - (N >>s 31)
-        eor r1, r1, r4
+        ASR r4, r1, #31          @ r4 = sign of N
+        ASR r5, r3, #31          @ r5 = sign of D
+        EOR r10, r4, r5          @ r10 = sign of result
+        EOR r0, r0, r4           @ take absolute value of N
+        EOR r1, r1, r4           @ N = (N ^ (N >>s 31)) - (N >>s 31)
         subs r0, r0, r4
         sbc r1, r1, r4
-        mov r4, r3, asr #31      @ take absolute value of D
-        eor r2, r2, r4
-        eor r3, r3, r4
-        subs r2, r2, r4
-        sbc r3, r3, r4
+        EOR r2, r2, r5           @ take absolute value of D
+        EOR r3, r3, r5
+        subs r2, r2, r5
+        sbc r3, r3, r5
         bl __i64_udivmod         @ do unsigned division
-        eor r0, r0, r10, asr#31  @ apply expected sign
-        eor r1, r1, r10, asr#31
-        subs r0, r0, r10, asr#31
-        sbc r1, r1, r10, asr#31
+        EOR r0, r4, r10          @ apply expected sign
+        EOR r1, r5, r10
+        subs r0, r0, r10
+        sbc r1, r1, r10
         pop {r4, r5, r6, r7, r8, r10, lr}
         bx lr
-	.type __i64_smod, %function
-	.size __i64_smod, . - __i64_smod
-	
+ENDFUNCTION(__i64_sdiv)
diff --git a/runtime/arm/i64_shl.s b/runtime/arm/i64_shl.S
index afd92db..66569d3 100644
--- a/runtime/arm/i64_shl.s
+++ b/runtime/arm/i64_shl.S
@@ -34,7 +34,7 @@
 
 @ Helper functions for 64-bit integer arithmetic.  ARM version.
 
-        .text
+#include "sysdeps.h"	
 
 @@@ Shift left	
 
@@ -47,26 +47,25 @@
 @ If N = 0:
 @    RH = XH | 0 | 0
 @    RL = XL
-@ If 1 <= N <= 31:  1 <= 32-N <= 31  and  255 <= N-32 mod 256 <= 255
+@ If 1 <= N <= 31:  1 <= 32-N <= 31  and  2s5 <= N-32 mod 256 <= 255
 @    RH = (XH << N) | (XL >> (32-N) | 0
 @    RL = XL << N        
 @ If N = 32:
 @    RH = 0 | XL | 0
 @    RL = 0
-@ If 33 <= N <= 63: 255 <= 32-N mod 256 <= 255 and 1 <= N-32 <= 31
+@ If 33 <= N <= 63: 225 <= 32-N mod 256 <= 255 and 1 <= N-32 <= 31
 @    RH = 0 | 0 | (XL << (N-32))
 @    RL = 0
 	
-	.global __i64_shl
-__i64_shl:
-        and r2, r2, #63         @ normalize amount to 0...63
-        rsb r3, r2, #32         @ r3 = 32 - amount
-        mov r1, r1, lsl r2
-        orr r1, r1, r0, lsr r3
-	sub r3, r2, #32         @ r3 = amount - 32
-	orr r1, r1, r0, lsl r3
-        mov r0, r0, lsl r2
+FUNCTION(__i64_shl)
+        AND r2, r2, #63         @ normalize amount to 0...63
+        RSB r3, r2, #32         @ r3 = 32 - amount
+        LSL r1, r1, r2
+        LSR r3, r0, r3
+        ORR r1, r1, r3
+	SUB r3, r2, #32         @ r3 = amount - 32
+	LSL r3, r0, r3
+	ORR r1, r1, r3
+        LSL r0, r0, r2
         bx lr
-	.type __i64_shl, %function
-	.size __i64_shl, . - __i64_shl
-
+ENDFUNCTION(__i64_shl)
diff --git a/runtime/arm/i64_shr.s b/runtime/arm/i64_shr.S
index 9d60441..a5418f4 100644
--- a/runtime/arm/i64_shr.s
+++ b/runtime/arm/i64_shr.S
@@ -34,7 +34,7 @@
 
 @ Helper functions for 64-bit integer arithmetic.  ARM version.
 
-        .text
+#include "sysdeps.h"
 
 @@@ Shift right unsigned	
 
@@ -57,16 +57,15 @@
 @    RL = 0 | 0 | (XH >> (N-32))
 @    RH = 0
 
-	.global __i64_shr
-__i64_shr:
-        and r2, r2, #63         @ normalize amount to 0...63
-        rsb r3, r2, #32         @ r3 = 32 - amount
-        mov r0, r0, lsr r2
-        orr r0, r0, r1, lsl r3
-	sub r3, r2, #32         @ r3 = amount - 32
-	orr r0, r0, r1, lsr r3
-        mov r1, r1, lsr r2
+FUNCTION(__i64_shr)
+        AND r2, r2, #63         @ normalize amount to 0...63
+        RSB r3, r2, #32         @ r3 = 32 - amount
+        LSR r0, r0, r2
+        LSL r3, r1, r3
+        ORR r0, r0, r3
+	SUB r3, r2, #32         @ r3 = amount - 32
+	LSR r3, r1, r3
+	ORR r0, r0, r3
+        LSR r1, r1, r2
         bx lr
-	.type __i64_shr, %function
-	.size __i64_shr, . - __i64_shr
-	
+ENDFUNCTION(__i64_shr)
diff --git a/runtime/arm/i64_sdiv.s b/runtime/arm/i64_smod.S
index e96008d..b109ecc 100644
--- a/runtime/arm/i64_sdiv.s
+++ b/runtime/arm/i64_smod.S
@@ -34,33 +34,28 @@
 
 @ Helper functions for 64-bit integer arithmetic.  ARM version.
 
-        .text
+#include "sysdeps.h"
 
-@@@ Signed division	
+@@@ Signed modulus
 	
-	.global __i64_sdiv
-__i64_sdiv:
+FUNCTION(__i64_smod)
         push {r4, r5, r6, r7, r8, r10, lr}
-        eor r10, r1, r3          @ r10 = sign of result
-        mov r4, r1, asr #31      @ take absolute value of N
-        eor r0, r0, r4           @ N = (N ^ (N >>s 31)) - (N >>s 31)
-        eor r1, r1, r4
+        ASR r4, r1, #31          @ r4 = sign of N
+        ASR r5, r3, #31          @ r5 = sign of D
+        MOV r10, r4              @ r10 = sign of result
+        EOR r0, r0, r4           @ take absolute value of N
+        EOR r1, r1, r4           @ N = (N ^ (N >>s 31)) - (N >>s 31)
         subs r0, r0, r4
         sbc r1, r1, r4
-        mov r4, r3, asr #31      @ take absolute value of D
-        eor r2, r2, r4
-        eor r3, r3, r4
-        subs r2, r2, r4
-        sbc r3, r3, r4
+        EOR r2, r2, r5           @ take absolute value of D
+        EOR r3, r3, r5
+        subs r2, r2, r5
+        sbc r3, r3, r5
         bl __i64_udivmod         @ do unsigned division
-        mov r0, r4
-        mov r1, r5
-        eor r0, r0, r10, asr#31  @ apply expected sign
-        eor r1, r1, r10, asr#31
-        subs r0, r0, r10, asr#31
-        sbc r1, r1, r10, asr#31
+        EOR r0, r0, r10          @ apply expected sign
+        EOR r1, r1, r10
+        subs r0, r0, r10
+        sbc r1, r1, r10
         pop {r4, r5, r6, r7, r8, r10, lr}
         bx lr
-	.type __i64_sdiv, %function
-	.size __i64_sdiv, . - __i64_sdiv
-	
+ENDFUNCTION(__i64_smod)
diff --git a/runtime/arm/i64_stod.S b/runtime/arm/i64_stod.S
index 7e5a06f..81e43e2 100644
--- a/runtime/arm/i64_stod.S
+++ b/runtime/arm/i64_stod.S
@@ -34,24 +34,23 @@
 
 @ Helper functions for 64-bit integer arithmetic.  ARM version.
 
-        .text
+#include "sysdeps.h"
 
 @@@ Conversion from signed 64-bit integer to double float
 	
-	.global __i64_stod
+FUNCTION(__i64_stod)
 __i64_stod:
-        fmsr s0, r0
-        fuitod d0, s0           @ convert low half to double (unsigned)
-        fmsr s2, r1
-        fsitod d1, s2           @ convert high half to double (signed)
-        fldd d2, .LC1           @ d2 = 2^32
-        fmacd d0, d1, d2        @ d0 = d0 + d1 * d2 = double value of int64
+        vmov    s0, r0
+        vcvt.f64.u32 d0, s0     @ convert low half to double (unsigned)
+        vmov    s2, r1
+        vcvt.f64.s32 d1, s2     @ convert high half to double (signed)
+        vldr    d2, .LC1        @ d2 = 2^32
+        vmla.f64 d0, d1, d2     @ d0 = d0 + d1 * d2 = double value of int64
 #ifdef VARIANT_eabi	
-	fmrrd r0, r1, d0        @ return result in r0, r1
+	vmov	r0, r1, d0      @ return result in r0, r1
 #endif
         bx lr
-	.type __i64_stod, %function
-	.size __i64_stod, . - __i64_stod
+ENDFUNCTION(__i64_stod)
 
         .balign 8
 .LC1:   .quad 0x41f0000000000000 @ 2^32 in double precision
diff --git a/runtime/arm/i64_stof.S b/runtime/arm/i64_stof.S
index 3f33f04..f1051f5 100644
--- a/runtime/arm/i64_stof.S
+++ b/runtime/arm/i64_stof.S
@@ -34,15 +34,14 @@
 
 @ Helper functions for 64-bit integer arithmetic.  ARM version.
 
-        .text
+#include "sysdeps.h"
 
 @@@ Conversion from signed 64-bit integer to single float
 	
-	.global __i64_stof
-__i64_stof:
+FUNCTION(__i64_stof)
     @ Check whether -2^53 <= X < 2^53
-        mov r2, r1, asr #21
-        mov r3, r1, asr #31     @ (r2,r3) = X >> 53
+        ASR r2, r1, #21
+        ASR r3, r1, #31         @ (r2,r3) = X >> 53
         adds r2, r2, #1
         adc r3, r3, #0          @ (r2,r3) = X >> 53 + 1
         cmp r3, #2
@@ -50,30 +49,29 @@ __i64_stof:
    @ 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)
-	mov r2, #0x700
-        orr r2, r2, #0xFF       @ r2 = 0x7FF
-        and r3, r0, r2          @ extract bits 0 to 11 of X
-        add r3, r3, r2          @ r3 = (X & 0x7FF) + 0x7FF
+	MOV r2, #0x700
+        ORR r2, r2, #0xFF       @ r2 = 0x7FF
+        AND r3, r0, r2          @ extract bits 0 to 11 of X
+        ADD r3, r3, r2          @ r3 = (X & 0x7FF) + 0x7FF
    @ bit 12 of r3 is 0 if all low 12 bits of X are 0, 1 otherwise
    @ bits 13-31 of r3 are 0
-        orr r0, r0, r3          @ correct bit number 12 of X
-	bic r0, r0, r2          @ set to 0 bits 0 to 11 of X
+        ORR r0, r0, r3          @ correct bit number 12 of X
+	BIC r0, r0, r2          @ set to 0 bits 0 to 11 of X
    @ Convert to double
-1:      fmsr s0, r0
-        fuitod d0, s0           @ convert low half to double (unsigned)
-        fmsr s2, r1
-        fsitod d1, s2           @ convert high half to double (signed)
-        fldd d2, .LC1           @ d2 = 2^32
-        fmacd d0, d1, d2        @ d0 = d0 + d1 * d2 = double value of int64
+1:      vmov s0, r0
+        vcvt.f64.u32 d0, s0     @ convert low half to double (unsigned)
+        vmov s2, r1
+        vcvt.f64.s32 d1, s2     @ convert high half to double (signed)
+        vldr d2, .LC1           @ d2 = 2^32
+        vmla.f64 d0, d1, d2     @ d0 = d0 + d1 * d2 = double value of int64
    @ Round to single
-        fcvtsd s0, d0
+        vcvt.f32.f64 s0, d0
 #ifdef VARIANT_eabi	
    @ Return result in r0
-	fmrs r0, s0
+	vmov r0, s0
 #endif	
         bx lr
-	.type __i64_stof, %function
-	.size __i64_stof, . - __i64_stof
-
+ENDFUNCTION(__i64_stof)
+	
         .balign 8
 .LC1:   .quad 0x41f0000000000000 @ 2^32 in double precision
diff --git a/runtime/arm/i64_udiv.s b/runtime/arm/i64_udiv.S
index de41e00..3b59944 100644
--- a/runtime/arm/i64_udiv.s
+++ b/runtime/arm/i64_udiv.S
@@ -34,18 +34,15 @@
 
 @ Helper functions for 64-bit integer arithmetic.  ARM version.
 
-        .text
+#include "sysdeps.h"
 
 @@@ Unsigned division	
 	
-	.global __i64_udiv
-__i64_udiv:
+FUNCTION(__i64_udiv)
         push {r4, r5, r6, r7, r8, lr}
         bl __i64_udivmod
-        mov r0, r4
-        mov r1, r5
+        MOV r0, r4
+        MOV r1, r5
         pop {r4, r5, r6, r7, r8, lr}
         bx lr
-	.type __i64_udiv, %function
-	.size __i64_udiv, . - __i64_udiv
-	
+ENDFUNCTION(__i64_udiv)	
diff --git a/runtime/arm/i64_udivmod.s b/runtime/arm/i64_udivmod.S
index e3d9c87..e5373ad 100644
--- a/runtime/arm/i64_udivmod.s
+++ b/runtime/arm/i64_udivmod.S
@@ -34,7 +34,7 @@
 
 @ Helper functions for 64-bit integer arithmetic.  ARM version.
 
-        .text
+#include "sysdeps.h"
 
 @@@ Auxiliary function for division and modulus. Don't call from C
 
@@ -42,14 +42,14 @@
 @ On exit:   Q = (r4, r5) quotient     R = (r0, r1) remainder	
 @ Locals:    M = (r6, r7) mask         TMP = r8 temporary	
 	
-	.global __i64_udivmod
-__i64_udivmod:
+FUNCTION(__i64_udivmod)
         orrs r8, r2, r3         @ is D == 0?
+	it eq
         bxeq lr                 @ if so, return with unspecified results
-        mov r4, #0              @ Q = 0
-        mov r5, #0
-        mov r6, #1              @ M = 1
-        mov r7, #0
+        MOV r4, #0              @ Q = 0
+        MOV r5, #0
+        MOV r6, #1              @ M = 1
+        MOV r7, #0
 1:      cmp r3, #0              @ while ((signed) D >= 0) ...
         blt 2f
         subs r8, r0, r2         @ ... and N >= D ...
@@ -69,12 +69,11 @@ __i64_udivmod:
         adc r1, r1, r3          @ N = N + D
         bic r4, r4, r6          @ Q = Q & ~M
         bic r5, r5, r7
-3:      movs r7, r7, lsr #1     @ M = M >> 1
-        mov r6, r6, rrx
-        movs r3, r3, lsr #1     @ D = D >> 1
-        mov r2, r2, rrx
+3:      lsrs r7, r7, #1         @ M = M >> 1
+        rrx r6, r6
+        lsrs r3, r3, #1         @ D = D >> 1
+        rrx r2, r2
         orrs r8, r6, r7         @ repeat while (M != 0) ...
         bne 2b
         bx lr
-	.type __i64_udivmod, %function
-	.size __i64_udivmod, . - __i64_udivmod
+ENDFUNCTION(__i64_udivmod)
diff --git a/runtime/arm/i64_umod.s b/runtime/arm/i64_umod.S
index 80af56e..e59fd20 100644
--- a/runtime/arm/i64_umod.s
+++ b/runtime/arm/i64_umod.S
@@ -34,16 +34,13 @@
 
 @ Helper functions for 64-bit integer arithmetic.  ARM version.
 
-        .text
+#include "sysdeps.h"
 
-@@@ Unsigned modulus	
+@@@ Unsigned remainder
 	
-	.global __i64_umod
-__i64_umod:
+FUNCTION(__i64_umod)
         push {r4, r5, r6, r7, r8, lr}
         bl __i64_udivmod         @ remainder is already in r0,r1
         pop {r4, r5, r6, r7, r8, lr}
         bx lr
-	.type __i64_umod, %function
-	.size __i64_umod, . - __i64_umod
-	
+ENDFUNCTION(__i64_umod)	
diff --git a/runtime/arm/i64_utod.S b/runtime/arm/i64_utod.S
index 1110874..b12d7c2 100644
--- a/runtime/arm/i64_utod.S
+++ b/runtime/arm/i64_utod.S
@@ -34,25 +34,23 @@
 
 @ Helper functions for 64-bit integer arithmetic.  ARM version.
 
-        .text
+#include "sysdeps.h"
 
 @@@ Conversion from unsigned 64-bit integer to double float
 	
-	.global __i64_utod
-__i64_utod:
-        fmsr s0, r0
-        fuitod d0, s0           @ convert low half to double (unsigned)
-        fmsr s2, r1
-        fuitod d1, s2           @ convert high half to double (unsigned)
-        fldd d2, .LC1           @ d2 = 2^32
-        fmacd d0, d1, d2        @ d0 = d0 + d1 * d2 = double value of int64
+FUNCTION(__i64_utod)
+__i64_stod:
+        vmov    s0, r0
+        vcvt.f64.u32 d0, s0     @ convert low half to double (unsigned)
+        vmov    s2, r1
+        vcvt.f64.u32 d1, s2     @ convert high half to double (unsigned)
+        vldr    d2, .LC1        @ d2 = 2^32
+        vmla.f64 d0, d1, d2     @ d0 = d0 + d1 * d2 = double value of int64
 #ifdef VARIANT_eabi	
-	fmrrd r0, r1, d0        @ return result in r0, r1
-#endif	
+	vmov	r0, r1, d0      @ return result in r0, r1
+#endif
         bx lr
-	.type __i64_utod, %function
-	.size __i64_utod, . - __i64_utod
-	
+ENDFUNCTION(__i64_utod)
+
         .balign 8
 .LC1:   .quad 0x41f0000000000000 @ 2^32 in double precision
-	
diff --git a/runtime/arm/i64_utof.S b/runtime/arm/i64_utof.S
index a959076..711cda0 100644
--- a/runtime/arm/i64_utof.S
+++ b/runtime/arm/i64_utof.S
@@ -34,42 +34,40 @@
 
 @ Helper functions for 64-bit integer arithmetic.  ARM version.
 
-        .text
+#include "sysdeps.h"
 
 @@@ Conversion from unsigned 64-bit integer to single float
 	
-	.global __i64_utof
-__i64_utof:
+FUNCTION(__i64_utof)
     @ Check whether X < 2^53
-        movs r2, r1, lsr #21    @ test if X >> 53 == 0
+        lsrs r2, r1, #21        @ test if X >> 53 == 0
         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)
-	mov r2, #0x700
-        orr r2, r2, #0xFF       @ r2 = 0x7FF
-        and r3, r0, r2          @ extract bits 0 to 11 of X
-        add r3, r3, r2          @ r3 = (X & 0x7FF) + 0x7FF
+	MOV r2, #0x700
+        ORR r2, r2, #0xFF       @ r2 = 0x7FF
+        AND r3, r0, r2          @ extract bits 0 to 11 of X
+        ADD r3, r3, r2          @ r3 = (X & 0x7FF) + 0x7FF
    @ bit 12 of r3 is 0 if all low 12 bits of X are 0, 1 otherwise
    @ bits 13-31 of r3 are 0
-        orr r0, r0, r3          @ correct bit number 12 of X
-	bic r0, r0, r2          @ set to 0 bits 0 to 11 of X
+        ORR r0, r0, r3          @ correct bit number 12 of X
+	BIC r0, r0, r2          @ set to 0 bits 0 to 11 of X
    @ Convert to double
-1:      fmsr s0, r0
-        fuitod d0, s0           @ convert low half to double (unsigned)
-        fmsr s2, r1
-        fuitod d1, s2           @ convert high half to double (unsigned)
-        fldd d2, .LC1           @ d2 = 2^32
-        fmacd d0, d1, d2        @ d0 = d0 + d1 * d2 = double value of int64
+1:      vmov s0, r0
+        vcvt.f64.u32 d0, s0     @ convert low half to double (unsigned)
+        vmov s2, r1
+        vcvt.f64.u32 d1, s2     @ convert high half to double (unsigned)
+        vldr d2, .LC1           @ d2 = 2^32
+        vmla.f64 d0, d1, d2     @ d0 = d0 + d1 * d2 = double value of int64
    @ Round to single
-        fcvtsd s0, d0
+        vcvt.f32.f64 s0, d0
 #ifdef VARIANT_eabi	
    @ Return result in r0
-	fmrs r0, s0
+	vmov r0, s0
 #endif	
         bx lr
-	.type __i64_utof, %function
-	.size __i64_utof, . - __i64_utof
+ENDFUNCTION(__i64_utof)
 
         .balign 8
 .LC1:   .quad 0x41f0000000000000 @ 2^32 in double precision
diff --git a/runtime/arm/sysdeps.h b/runtime/arm/sysdeps.h
new file mode 100644
index 0000000..b72af0f
--- /dev/null
+++ b/runtime/arm/sysdeps.h
@@ -0,0 +1,84 @@
+// *****************************************************************
+//
+//               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.
+//
+// *********************************************************************
+
+// System dependencies
+
+#ifdef THUMB
+#define FUNCTION(f) \
+	.text; \
+	.thumb; \
+	.thumb_func; \
+	.global f; \
+f:
+#else
+#define FUNCTION(f) \
+	.text; \
+	.arm; \
+	.global f; \
+f:
+#endif
+
+#define ENDFUNCTION(f) \
+	.type f, %function; .size f, . - f
+
+// In Thumb2 mode, some instructions have shorter encodings in their "S" form
+// (update condition flags).  For cases where the condition flags do not
+// matter, we use the following macros for these instructions.
+// In classic ARM mode, we prefer not to use the "S" form unless necessary.
+
+#ifdef THUMB
+#define THUMB_S(x) x##s
+#else
+#define THUMB_S(x) x
+#endif
+
+#define ADD THUMB_S(add)
+#define AND THUMB_S(and)
+#define ASR THUMB_S(asr)
+#define BIC THUMB_S(bic)
+#define EOR THUMB_S(eor)
+#define LSL THUMB_S(lsl)
+#define LSR THUMB_S(lsr)
+#define MOV THUMB_S(mov)
+#define ORR THUMB_S(orr)
+#define RSB THUMB_S(rsb)
+#define SUB THUMB_S(sub)
+
+	.syntax unified
+#ifdef THUMB
+	.arch	armv7
+#else
+	.arch	armv6
+#endif
+	.fpu	vfpv2
diff --git a/runtime/arm/vararg.S b/runtime/arm/vararg.S
index 8d431d3..e352582 100644
--- a/runtime/arm/vararg.S
+++ b/runtime/arm/vararg.S
@@ -34,50 +34,44 @@
 
 @ Helper functions for variadic functions <stdarg.h>.  ARM version
 
-        .text
+#include "sysdeps.h"
 
 @ typedef void * va_list;
 @ unsigned int __compcert_va_int32(va_list * ap);
 @ unsigned long long __compcert_va_int64(va_list * ap);
 @ double __compcert_va_float64(va_list * ap);
 
-        .global __compcert_va_int32
-__compcert_va_int32:
+FUNCTION(__compcert_va_int32)
 	                        @ r0 = ap parameter
         ldr     r1, [r0, #0]    @ r1 = pointer to next argument
-        add     r1, r1, #4      @ advance ap by 4
+        ADD     r1, r1, #4      @ advance ap by 4
         str     r1, [r0, #0]
         ldr     r0, [r1, #-4]    @ load next argument and return it in r0
         bx      lr
-        .type __compcert_va_int32, %function
-        .size __compcert_va_int32, . - __compcert_va_int32
+ENDFUNCTION(__compcert_va_int32)
 
-        .global __compcert_va_int64
-__compcert_va_int64:
+FUNCTION(__compcert_va_int64)
 	                        @ r0 = ap parameter
         ldr     r1, [r0, #0]    @ r1 = pointer to next argument
-        add     r1, r1, #15     @ 8-align and advance by 8
-        bic     r1, r1, #7
+        ADD     r1, r1, #15     @ 8-align and advance by 8
+        BIC     r1, r1, #7
         str     r1, [r0, #0]    @ update ap
         ldr     r0, [r1, #-8]   @ load next argument and return it in r0,r1
         ldr     r1, [r1, #-4]
         bx      lr
-        .type __compcert_va_int64, %function
-        .size __compcert_va_int64, . - __compcert_va_int64
+ENDFUNCTION(__compcert_va_int64)
 
-        .global __compcert_va_float64
-__compcert_va_float64:
+FUNCTION(__compcert_va_float64)
 	                        @ r0 = ap parameter
         ldr     r1, [r0, #0]    @ r1 = pointer to next argument
-        add     r1, r1, #15     @ 8-align and advance by 8
-        bic     r1, r1, #7
+        ADD     r1, r1, #15     @ 8-align and advance by 8
+        BIC     r1, r1, #7
         str     r1, [r0, #0]    @ update ap
-#ifdef VARIANT_hardfloat
-        fldd    d0, [r1, #-8]   @ load next argument and return it in d0
-#else
+#ifdef VARIANT_eabi
         ldr     r0, [r1, #-8]   @ load next argument and return it in r0,r1
         ldr     r1, [r1, #-4]
+#else	
+        vldr    d0, [r1, #-8]   @ load next argument and return it in d0
 #endif	
         bx      lr
-        .type __compcert_va_float64, %function
-        .size __compcert_va_float64, . - __compcert_va_float64
+ENDFUNCTION(__compcert_va_float64)