From a753f08de8382141aec2b4517fb87ad4e5fcc512 Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Thu, 14 Dec 2017 10:19:03 +0100 Subject: Use instructions with immediate operands that don't need replacement by the assembler (add ra, rb, #-1 --> sub ra, rb, #1) --- arm/Asmexpand.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'arm/Asmexpand.ml') diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index dd960484..6c6b4a11 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -32,7 +32,6 @@ let _8 = coqint_of_camlint 8l let _16 = coqint_of_camlint 16l let _32 = coqint_of_camlint 32l let _64 = coqint_of_camlint 64l -let _m1 = coqint_of_camlint (-1l) (* Emit instruction sequences that set or offset a register by a constant. *) (* No S suffix because they are applied to SP most of the time. *) @@ -318,7 +317,7 @@ let expand_builtin_inline name args res = emit (Pclz (res, ah)); emit (Padd (res, res, SOreg IR14)) | ("__builtin_ctz" | "__builtin_ctzl"), [BA(IR a1)], BR(IR res) -> - emit (Padd(IR14, a1, SOimm _m1)); (* tmp := x-1 *) + emit (Psub(IR14, a1, SOimm _1)); (* tmp := x-1 *) emit (Pmvn(res, SOreg a1)); (* res := ~(x) *) emit (Pand(res, IR14, SOreg res)); (* res := tmp & ~(x) *) emit (Pclz(res, res)); (* res := #leading zeros *) @@ -330,7 +329,7 @@ let expand_builtin_inline name args res = emit (Pcmp (al, SOimm _0)); emit (Pbne lbl1); (* low word is zero, count trailing zeros in high word and increment by 32 *) - emit (Padd(IR14, ah, SOimm _m1)); + emit (Psub(IR14, ah, SOimm _1)); emit (Pmvn(res, SOreg ah)); emit (Pand(res, IR14, SOreg res)); emit (Pclz(res, res)); @@ -338,7 +337,7 @@ let expand_builtin_inline name args res = emit (Pb lbl2); (* count trailing zeros in low word *) emit (Plabel lbl1); - emit (Padd(IR14, al, SOimm _m1)); + emit (Psub(IR14, al, SOimm _1)); emit (Pmvn(res, SOreg al)); emit (Pand(res, IR14, SOreg res)); emit (Pclz(res, res)); -- cgit