From 603e931f49ef04188a58895ce38d892511b75b78 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 30 Jul 2011 15:35:29 +0000 Subject: ARM: added reversed load/store builtins + bswap builtin (to be tested) IA32: added bswap builtin Updated Changelog git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1693 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- Changelog | 27 +++++++++++++++++++++++---- arm/CBuiltins.ml | 20 +++++++++++++++++--- arm/PrintAsm.ml | 36 ++++++++++++++++++++++++++++++++++++ ia32/CBuiltins.ml | 3 +++ ia32/PrintAsm.ml | 5 +++++ 5 files changed, 84 insertions(+), 7 deletions(-) diff --git a/Changelog b/Changelog index 56fcb61a..a2677f77 100644 --- a/Changelog +++ b/Changelog @@ -1,7 +1,14 @@ -- Fixed two omissions in the semantics of CompCert C (reported by Brian Campbell): - . Functions calls through a function pointer had undefined semantics. - . Conditional expressions "e1 ? e2 : e3" where e2 and e3 have different - types were missing a cast to their common type. +Release 1.9, 2011-xx-xx +======================= + +- The reduction semantics of CompCert C was made executable and turned + into a reference interpreter for CompCert C, enabling animation of + the semantics. (Thanks to Brian Campbell for suggesting this approach.) + Usage is: ccomp -interp [options] source.c + Options include: + -trace to print a detailed trace of reduction steps + -random to randomize execution order + -all to explore all possible execution orders in parallel - Revised and strengthened the top-level statements of semantic preservation. In particular, we now show: @@ -11,6 +18,11 @@ the compiled code performs at least these I/O before continuing with an arbitrary behavior. +- Fixed two omissions in the semantics of CompCert C (reported by Brian Campbell): + . Functions calls through a function pointer had undefined semantics. + . Conditional expressions "e1 ? e2 : e3" where e2 and e3 have different + types were missing a cast to their common type. + - Revised handling of annotation statements. Now they come in two forms: 1. __builtin_annot("format", x1, ..., xN) (arbitrarily many arguments; no code generated, even if some @@ -22,6 +34,13 @@ - Related clean-ups in the handling of external functions and compiler built-ins. +- ARM code generator was ported to the new ABI (EABI in ARM parlance, + armel in Debian parlance), using VFD instructions for floating-point. + (Successfully tested on a Trimslice platform running Ubuntu 11.04.) + +- IA32 code generator: added -fno-sse option to prevent generation of + SSE instructions for memory copy operations. + Release 1.8.2, 2011-05-24 ========================= diff --git a/arm/CBuiltins.ml b/arm/CBuiltins.ml index 2e493883..dc4ca60e 100644 --- a/arm/CBuiltins.ml +++ b/arm/CBuiltins.ml @@ -18,10 +18,24 @@ open Cparser open C -(* No ARM builtins for the moment *) - let builtins = { Builtins.typedefs = []; - Builtins.functions = [] + Builtins.functions = [ + (* Integer arithmetic *) + "__builtin_bswap", + (TInt(IUInt, []), [TInt(IUInt, [])], false); + (* Float arithmetic *) + "__builtin_fsqrt", + (TFloat(FDouble, []), [TFloat(FDouble, [])], false); + (* Memory accesses *) + "__builtin_read_int16_reversed", + (TInt(IUShort, []), [TPtr(TInt(IUShort, [AConst]), [])], false); + "__builtin_read_int32_reversed", + (TInt(IUInt, []), [TPtr(TInt(IUInt, [AConst]), [])], false); + "__builtin_write_int16_reversed", + (TVoid [], [TPtr(TInt(IUShort, []), []); TInt(IUShort, [])], false); + "__builtin_write_int32_reversed", + (TVoid [], [TPtr(TInt(IUInt, []), []); TInt(IUInt, [])], false); + ] } diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index f1beded0..c50acba8 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -370,14 +370,50 @@ let print_builtin_vstore oc chunk args = end in fprintf oc "%s end builtin __builtin_volatile_write\n" comment; n +(* Magic sequence for byte-swapping *) + +let print_bswap oc src dst tmp = + (* tmp <> src, tmp <> dst, but can have dst = src *) + (* src = A . B .C . D *) + fprintf oc " eor %a, %a, %a, ror #16\n" ireg tmp ireg src ireg src; + (* tmp = A^C . B^D . C^A . D^B *) + fprintf oc " bic %a, %a, #0x00FF0000\n" ireg tmp ireg tmp; + (* tmp = A^C . 000 . C^A . D^B *) + fprintf oc " mov %a, %a, ror #8\n" ireg dst ireg src; + (* dst = D . A . B . C *) + fprintf oc " eor %a, %a, %a, lsr #8\n" ireg dst ireg dst ireg tmp + (* dst = D . A^A^C . B . C^C^A = D . C . B . A *) + (* Handling of compiler-inlined builtins *) let print_builtin_inline oc name args res = fprintf oc "%s begin %s\n" comment name; let n = match name, args, res with + (* Integer arithmetic *) + | "__builtin_bswap", [IR a1], IR res -> + print_bswap oc a1 IR14 res; 4 (* Float arithmetic *) | "__builtin_fabs", [FR a1], FR res -> fprintf oc " fabsd %a, %a\n" freg res freg a1; 1 + | "__builtin_fsqrt", [FR a1], FR res -> + fprintf oc " fsqrtd %a, %a\n" freg res freg a1; 1 + (* Memory accesses *) + | "__builtin_read_int16_reversed", [IR a1], IR res -> + fprintf oc " ldrh %a, [%a, #0]\n" ireg res ireg a1; + fprintf oc " mov %a, %a, lsr #8\n" ireg IR14 ireg res; + fprintf oc " orr %a, %a, %a, lsl #8\n" ireg res ireg IR14 ireg res; 3 + | "__builtin_read_int32_reversed", [IR a1], IR res -> + fprintf oc " ldr %a, [%a, #0]\n" ireg res ireg a1; + print_bswap oc res IR14 res; 5 + | "__builtin_write_int16_reversed", [IR a1; IR a2], _ -> + fprintf oc " mov %a, %a, lsr #8\n" ireg IR14 ireg a2; + fprintf oc " and %a, %a, #0xFF\n" ireg IR14 ireg IR14; + fprintf oc " orr %a, %a, %a, lsl #8\n" ireg IR14 ireg IR14 ireg a2; + fprintf oc " strh %a, [%a, #0]\n" ireg IR14 ireg a1; 4 + | "__builtin_write_int32_reversed", [IR a1; IR a2], _ -> + let tmp = if a1 = IR10 then IR12 else IR10 in + print_bswap oc a2 IR14 tmp; + fprintf oc " str %a, [%a, #0]\n" ireg tmp ireg a1; 5 (* Catch-all *) | _ -> invalid_arg ("unrecognized builtin " ^ name) diff --git a/ia32/CBuiltins.ml b/ia32/CBuiltins.ml index 9cd31da5..3b94744c 100644 --- a/ia32/CBuiltins.ml +++ b/ia32/CBuiltins.ml @@ -21,6 +21,9 @@ open C let builtins = { Builtins.typedefs = []; Builtins.functions = [ + (* Integer arithmetic *) + "__builtin_bswap", + (TInt(IUInt, []), [TInt(IUInt, [])], false); (* Float arithmetic *) "__builtin_fsqrt", (TFloat(FDouble, []), [TFloat(FDouble, [])], false); diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 842957ff..6f02a8a7 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -412,6 +412,11 @@ 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 + (* Integer arithmetic *) + | "__builtin_bswap", [IR a1], IR res -> + if a1 <> res then + fprintf oc " movl %a, %a\n" ireg a1 ireg res; + fprintf oc " bswap %a\n" ireg res (* Float arithmetic *) | "__builtin_fabs", [FR a1], FR res -> need_masks := true; -- cgit