From f401437a97b09726d029e3a1b65143f34baaea70 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 24 Feb 2013 09:40:25 +0000 Subject: Updated ARM and PowerPC ports with new handling of __builtin_annot. ARM: add support for builtin_volatile_{read,write}_global, after all. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2127 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/ConstpropOp.vp | 4 --- arm/ConstpropOpproof.v | 13 ------- arm/PrintAsm.ml | 98 ++++++++++++++++++++++++++++++-------------------- 3 files changed, 59 insertions(+), 56 deletions(-) (limited to 'arm') diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp index a9cbad5..7e3217e 100644 --- a/arm/ConstpropOp.vp +++ b/arm/ConstpropOp.vp @@ -335,8 +335,4 @@ Nondetfunction addr_strength_reduction (addr, args) end. -Definition builtin_strength_reduction - (ef: external_function) (args: list reg) (vl: list approx) := - (ef, args). - End STRENGTH_REDUCTION. diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index e7e6a41..c7de86d 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -450,19 +450,6 @@ Proof. auto. Qed. -Lemma builtin_strength_reduction_correct: - forall ef args vl m t vres m', - vl = approx_regs app args -> - external_call ef ge rs##args m t vres m' -> - let (ef', args') := builtin_strength_reduction ef args vl in - external_call ef' ge rs##args' m t vres m'. -Proof. - (* force MATCH to be used *) - assert (val_match_approx (approx_reg app 1%positive) rs#(1%positive)) - by (apply MATCH). - unfold builtin_strength_reduction; intros; simpl; auto. -Qed. - End STRENGTH_REDUCTION. End ANALYSIS. diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 186e327..278b6b1 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -226,9 +226,9 @@ let call_helper oc fn dst arg1 arg2 = (* Handling of annotations *) -let print_annot_stmt oc txt args = +let print_annot_stmt oc txt targs args = fprintf oc "%s annotation: " comment; - PrintAnnot.print_annot_stmt preg "sp" oc txt args + PrintAnnot.print_annot_stmt preg "sp" oc txt targs args let print_annot_val oc txt args res = fprintf oc "%s annotation: " comment; @@ -306,50 +306,66 @@ let print_builtin_memcpy oc sz al args = (* Handling of volatile reads and writes *) +let print_builtin_vload_common oc chunk args res = + match chunk, args, res with + | Mint8unsigned, [IR addr], IR res -> + fprintf oc " ldrb %a, [%a, #0]\n" ireg res ireg addr; 1 + | Mint8signed, [IR addr], IR res -> + fprintf oc " ldrsb %a, [%a, #0]\n" ireg res ireg addr; 1 + | Mint16unsigned, [IR addr], IR res -> + fprintf oc " ldrh %a, [%a, #0]\n" ireg res ireg addr; 1 + | Mint16signed, [IR addr], IR res -> + fprintf oc " ldrsh %a, [%a, #0]\n" ireg res ireg addr; 1 + | Mint32, [IR addr], IR res -> + fprintf oc " ldr %a, [%a, #0]\n" ireg res ireg addr; 1 + | Mfloat32, [IR addr], FR res -> + fprintf oc " flds %a, [%a, #0]\n" freg_single res ireg addr; + fprintf oc " fcvtds %a, %a\n" freg res freg_single res; 2 + | (Mfloat64 | Mfloat64al32), [IR addr], FR res -> + fprintf oc " fldd %a, [%a, #0]\n" freg res ireg addr; 1 + | _ -> + assert false + let print_builtin_vload oc chunk args res = fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; - let n = - begin match chunk, args, res with - | Mint8unsigned, [IR addr], IR res -> - fprintf oc " ldrb %a, [%a, #0]\n" ireg res ireg addr; 1 - | Mint8signed, [IR addr], IR res -> - fprintf oc " ldrsb %a, [%a, #0]\n" ireg res ireg addr; 1 - | Mint16unsigned, [IR addr], IR res -> - fprintf oc " ldrh %a, [%a, #0]\n" ireg res ireg addr; 1 - | Mint16signed, [IR addr], IR res -> - fprintf oc " ldrsh %a, [%a, #0]\n" ireg res ireg addr; 1 - | Mint32, [IR addr], IR res -> - fprintf oc " ldr %a, [%a, #0]\n" ireg res ireg addr; 1 - | Mfloat32, [IR addr], FR res -> - fprintf oc " flds %a, [%a, #0]\n" freg_single res ireg addr; - fprintf oc " fcvtds %a, %a\n" freg res freg_single res; 2 - | (Mfloat64 | Mfloat64al32), [IR addr], FR res -> - fprintf oc " fldd %a, [%a, #0]\n" freg res ireg addr; 1 - | _ -> - assert false - end in + let n = print_builtin_vload_common oc chunk args res in fprintf oc "%s end builtin __builtin_volatile_read\n" comment; n +let print_builtin_vload_global oc chunk id ofs args res = + fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; + let lbl = label_symbol id ofs in + fprintf oc " ldr %a, .L%d @ %a\n" ireg IR14 lbl print_symb_ofs (id, ofs); + let n = print_builtin_vload_common oc chunk [IR IR14] res in + fprintf oc "%s end builtin __builtin_volatile_read\n" comment; n + 1 + +let print_builtin_vstore_common oc chunk args = + match chunk, args with + | (Mint8signed | Mint8unsigned), [IR addr; IR src] -> + fprintf oc " strb %a, [%a, #0]\n" ireg src ireg addr; 1 + | (Mint16signed | Mint16unsigned), [IR addr; IR src] -> + fprintf oc " strh %a, [%a, #0]\n" ireg src ireg addr; 1 + | Mint32, [IR addr; IR src] -> + fprintf oc " str %a, [%a, #0]\n" ireg src ireg addr; 1 + | Mfloat32, [IR addr; FR src] -> + fprintf oc " fcvtsd %a, %a\n" freg_single FR6 freg src; + fprintf oc " fsts %a, [%a, #0]\n" freg_single FR6 ireg addr; 2 + | (Mfloat64 | Mfloat64al32), [IR addr; FR src] -> + fprintf oc " fstd %a, [%a, #0]\n" freg src ireg addr; 1 + | _ -> + assert false + let print_builtin_vstore oc chunk args = fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; - let n = - begin match chunk, args with - | (Mint8signed | Mint8unsigned), [IR addr; IR src] -> - fprintf oc " strb %a, [%a, #0]\n" ireg src ireg addr; 1 - | (Mint16signed | Mint16unsigned), [IR addr; IR src] -> - fprintf oc " strh %a, [%a, #0]\n" ireg src ireg addr; 1 - | Mint32, [IR addr; IR src] -> - fprintf oc " str %a, [%a, #0]\n" ireg src ireg addr; 1 - | Mfloat32, [IR addr; FR src] -> - fprintf oc " fcvtsd %a, %a\n" freg_single FR6 freg src; - fprintf oc " fsts %a, [%a, #0]\n" freg_single FR6 ireg addr; 2 - | (Mfloat64 | Mfloat64al32), [IR addr; FR src] -> - fprintf oc " fstd %a, [%a, #0]\n" freg src ireg addr; 1 - | _ -> - assert false - end in + let n = print_builtin_vstore_common oc chunk args in fprintf oc "%s end builtin __builtin_volatile_write\n" comment; n +let print_builtin_vstore_global oc chunk id ofs args = + fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; + let lbl = label_symbol id ofs in + fprintf oc " ldr %a, .L%d @ %a\n" ireg IR14 lbl print_symb_ofs (id, ofs); + let n = print_builtin_vstore_common oc chunk (IR IR14 :: args) in + fprintf oc "%s end builtin __builtin_volatile_write\n" comment; n + 1 + (* Magic sequence for byte-swapping *) let print_bswap oc src tmp dst = @@ -612,6 +628,10 @@ let print_instruction oc = function print_builtin_vload oc chunk args res | EF_vstore chunk -> print_builtin_vstore oc chunk args + | EF_vload_global(chunk, id, ofs) -> + print_builtin_vload_global oc chunk id ofs args res + | EF_vstore_global(chunk, id, ofs) -> + print_builtin_vstore_global oc chunk id ofs args | EF_memcpy(sz, al) -> print_builtin_memcpy oc (Int32.to_int (camlint_of_coqint sz)) (Int32.to_int (camlint_of_coqint al)) args @@ -628,7 +648,7 @@ let print_instruction oc = function | Pannot(ef, args) -> begin match ef with | EF_annot(txt, targs) -> - print_annot_stmt oc (extern_atom txt) args; 0 + print_annot_stmt oc (extern_atom txt) targs args; 0 | _ -> assert false end -- cgit v1.2.3