From 21e269ee37b934428306f53dda0495fee30dd8fa Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 28 Jul 2014 14:29:42 +0000 Subject: All targets: add __builtin_membar ARM: add __builtin_dsb __builtin_isb git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2554 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/CBuiltins.ml | 5 +++++ arm/PrintAsm.ml | 53 ++++++++++++++++++++++++++++++---------------------- cfrontend/C2C.ml | 5 +++++ ia32/PrintAsm.ml | 3 +++ powerpc/Asmexpand.ml | 16 +++++++++------- 5 files changed, 53 insertions(+), 29 deletions(-) diff --git a/arm/CBuiltins.ml b/arm/CBuiltins.ml index b9b54e4..4446ab2 100644 --- a/arm/CBuiltins.ml +++ b/arm/CBuiltins.ml @@ -43,6 +43,11 @@ let builtins = { (TVoid [], [TPtr(TInt(IUShort, []), []); TInt(IUShort, [])], false); "__builtin_write32_reversed", (TVoid [], [TPtr(TInt(IUInt, []), []); TInt(IUInt, [])], false); + (* Synchronization *) + "__builtin_dsb", + (TVoid [], [], false); + "__builtin_isb", + (TVoid [], [], false) ] } diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index bb738a1..7dd7e48 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -515,6 +515,21 @@ let print_builtin_va_start oc r = fprintf oc " str r14, [%a, #0]\n" ireg r; n + 1 +(* Auxiliary for 64-bit integer arithmetic built-ins. They expand to + two instructions, one computing the low 32 bits of the result, + followed by another computing the high 32 bits. In cases where + the first instruction would overwrite arguments to the second + instruction, we must go through IR14 to hold the low 32 bits of the result. +*) + +let print_int64_arith oc conflict rl fn = + if conflict then begin + let n = fn IR14 in + fprintf oc " mov%t %a, %a\n" thumbS ireg rl ireg IR14; + n + 1 + end else + fn rl + (* Handling of compiler-inlined builtins *) let print_builtin_inline oc name args res = @@ -534,38 +549,25 @@ let print_builtin_inline oc name args res = fprintf oc " vsqrt.f64 %a, %a\n" freg res freg a1; 1 (* 64-bit integer arithmetic *) | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] -> - fprintf oc " rsbs %a, %a, #0\n" - ireg (if rl = ah then IR14 else rl) ireg al; + print_int64_arith oc (rl = ah) rl (fun rl -> + fprintf oc " rsbs %a, %a, #0\n" ireg rl ireg al; (* No "rsc" instruction in Thumb2. Emulate based on rsc a, b, #0 == a <- AddWithCarry(~b, 0, carry) == mvn a, b; adc a, a, #0 *) if !Clflags.option_fthumb then begin fprintf oc " mvn %a, %a\n" ireg rh ireg ah; - fprintf oc " adc %a, %a, #0\n" ireg rh ireg rh + fprintf oc " adc %a, %a, #0\n" ireg rh ireg rh; 3 end else begin - fprintf oc " rsc %a, %a, #0\n" ireg rh ireg ah - end; - if rl = ah then - fprintf oc " mov%t %a, %a\n" thumbS ireg rl ireg IR14; - 4 + fprintf oc " rsc %a, %a, #0\n" ireg rh ireg ah; 2 + end) | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> - if rl = ah || rl = bh then begin - fprintf oc " adds %a, %a, %a\n" ireg IR14 ireg al ireg bl; - fprintf oc " adc %a, %a, %a\n" ireg rh ireg ah ireg bh; - fprintf oc " mov%t %a, %a\n" thumbS ireg rl ireg IR14; 3 - end else begin + print_int64_arith oc (rl = ah || rl = bh) rl (fun rl -> fprintf oc " adds %a, %a, %a\n" ireg rl ireg al ireg bl; - fprintf oc " adc %a, %a, %a\n" ireg rh ireg ah ireg bh; 2 - end + fprintf oc " adc %a, %a, %a\n" ireg rh ireg ah ireg bh; 2) | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> - if rl = ah || rl = bh then begin - fprintf oc " subs %a, %a, %a\n" ireg IR14 ireg al ireg bl; - fprintf oc " sbc %a, %a, %a\n" ireg rh ireg ah ireg bh; - fprintf oc " mov%t %a, %a\n" thumbS ireg rl ireg IR14; 3 - end else begin + print_int64_arith oc (rl = ah || rl = bh) rl (fun rl -> fprintf oc " subs %a, %a, %a\n" ireg rl ireg al ireg bl; - fprintf oc " sbc %a, %a, %a\n" ireg rh ireg ah ireg bh; 2 - end + fprintf oc " sbc %a, %a, %a\n" ireg rh ireg ah ireg bh; 2) | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] -> fprintf oc " umull %a, %a, %a, %a\n" ireg rl ireg rh ireg a ireg b; 1 (* Memory accesses *) @@ -581,6 +583,13 @@ let print_builtin_inline oc name args res = | "__builtin_write32_reversed", [IR a1; IR a2], _ -> fprintf oc " rev %a, %a\n" ireg IR14 ireg a2; fprintf oc " str %a, [%a, #0]\n" ireg IR14 ireg a1; 2 + (* Synchronization *) + | "__builtin_membar", [], _ -> + 0 + | "__builtin_dsb", [], _ -> + fprintf oc " dsb\n"; 1 + | "__builtin_isb", [], _ -> + fprintf oc " isb\n"; 1 (* Vararg stuff *) | "__builtin_va_start", [IR a], _ -> print_builtin_va_start oc a diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index e7d8337..6ee217c 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -92,6 +92,11 @@ let builtins_generic = { (TInt(IInt, []), [TPtr(TInt(IChar, [AConst]), []); TInt(IInt, [])], false); + (* Software memory barrier *) + "__builtin_membar", + (TVoid [], + [], + false); (* Variable arguments *) (* va_start(ap,n) (preprocessing) --> __builtin_va_start(ap, arg) diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index d30c856..56e837d 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -529,6 +529,9 @@ let print_builtin_inline oc name args res = fprintf oc " movl %a, %a\n" ireg a2 ireg tmp; fprintf oc " bswap %a\n" ireg tmp; fprintf oc " movl %a, 0(%a)\n" ireg tmp ireg a1 + (* Synchronization *) + | "__builtin_membar", [], _ -> + () (* Vararg stuff *) | "__builtin_va_start", [IR a], _ -> print_builtin_va_start oc a diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 243a4d9..07cc50b 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -369,19 +369,19 @@ let expand_builtin_inline name args res = emit (Pcfi_adjust _m8) (* 64-bit integer arithmetic *) | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] -> - expand_int64_arith (rl = ah) rl (fun rl' -> - emit (Psubfic(rl', al, Cint _0)); + expand_int64_arith (rl = ah) rl (fun rl -> + emit (Psubfic(rl, al, Cint _0)); emit (Psubfze(rh, ah))) | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> - expand_int64_arith (rl = ah || rl = bh) rl (fun rl' -> - emit (Paddc(rl', al, bl)); + expand_int64_arith (rl = ah || rl = bh) rl (fun rl -> + emit (Paddc(rl, al, bl)); emit (Padde(rh, ah, bh))) | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> - expand_int64_arith (rl = ah || rl = bh) rl (fun rl' -> - emit (Psubfc(rl', bl, al)); + expand_int64_arith (rl = ah || rl = bh) rl (fun rl -> + emit (Psubfc(rl, bl, al)); emit (Psubfe(rh, bh, ah))) | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] -> - expand_int64_arith (rl = a || rl = b) rl (fun rl' -> + expand_int64_arith (rl = a || rl = b) rl (fun rl -> emit (Pmullw(rl, a, b)); emit (Pmulhwu(rh, a, b))) (* Memory accesses *) @@ -394,6 +394,8 @@ let expand_builtin_inline name args res = | "__builtin_write32_reversed", [IR a1; IR a2], _ -> emit (Pstwbrx(a2, GPR0, a1)) (* Synchronization *) + | "__builtin_membar", [], _ -> + () | "__builtin_eieio", [], _ -> emit (Peieio) | "__builtin_sync", [], _ -> -- cgit v1.2.3