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 +++++++++++++++++++++++---------------- ia32/PrintAsm.ml | 4 +- powerpc/ConstpropOp.vp | 11 ----- powerpc/ConstpropOpproof.v | 18 ------- powerpc/PrintAsm.ml | 6 +-- test/regression/Results/volatile2 | 14 ++++++ test/regression/volatile2.c | 15 ++++++ 9 files changed, 93 insertions(+), 90 deletions(-) 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 diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 4f62640..4768606 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -231,9 +231,9 @@ let need_masks = ref false (* 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 "ESP" oc txt args + PrintAnnot.print_annot_stmt preg "ESP" oc txt targs args let print_annot_val oc txt args res = fprintf oc "%s annotation: " comment; diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp index 973be92..9131a46 100644 --- a/powerpc/ConstpropOp.vp +++ b/powerpc/ConstpropOp.vp @@ -293,15 +293,4 @@ Nondetfunction addr_strength_reduction (addr, args) end. -Nondetfunction builtin_strength_reduction - (ef: external_function) (args: list reg) (vl: list approx) := - match ef, args, vl with - | EF_vload chunk, r1 :: nil, G symb n1 :: nil => - (EF_vload_global chunk symb n1, nil) - | EF_vstore chunk, r1 :: r2 :: nil, G symb n1 :: v2 :: nil => - (EF_vstore_global chunk symb n1, r2 :: nil) - | _, _, _ => - (ef, args) - end. - End STRENGTH_REDUCTION. diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index 7d557c6..84e1e5b 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -430,24 +430,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. - intros until m'. unfold builtin_strength_reduction. - destruct (builtin_strength_reduction_match ef args vl); simpl; intros; InvApproxRegs; SimplVMA. - unfold symbol_address in H. destruct (Genv.find_symbol ge symb) as [b|] eqn:?; rewrite H in H0. - rewrite volatile_load_global_charact. exists b; auto. - inv H0. - unfold symbol_address in H1. destruct (Genv.find_symbol ge symb) as [b|] eqn:?; rewrite H1 in H0. - rewrite volatile_store_global_charact. exists b; auto. - inv H0. - auto. -Qed. - End STRENGTH_REDUCTION. End ANALYSIS. diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 9c0f471..c9203ec 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -231,9 +231,9 @@ let rolm_mask n = (* 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 "R1" oc txt args + PrintAnnot.print_annot_stmt preg "R1" oc txt targs args let print_annot_val oc txt args res = fprintf oc "%s annotation: " comment; @@ -737,7 +737,7 @@ let print_instruction oc tbl pc fallthrough = function | Pannot(ef, args) -> begin match ef with | EF_annot(txt, targs) -> - print_annot_stmt oc (extern_atom txt) args + print_annot_stmt oc (extern_atom txt) targs args | _ -> assert false end diff --git a/test/regression/Results/volatile2 b/test/regression/Results/volatile2 index 5f88874..e6a9903 100644 --- a/test/regression/Results/volatile2 +++ b/test/regression/Results/volatile2 @@ -12,3 +12,17 @@ float 1: OK float 2: OK double 1: OK double 2: OK +global signed char 1: OK +global signed char 2: OK +global unsigned char 1: OK +global unsigned char 2: OK +global signed short 1: OK +global signed short 2: OK +global unsigned short 1: OK +global unsigned short 2: OK +global int 1: OK +global int 2: OK +global float 1: OK +global float 2: OK +global double 1: OK +global double 2: OK diff --git a/test/regression/volatile2.c b/test/regression/volatile2.c index 0608650..306eb8c 100644 --- a/test/regression/volatile2.c +++ b/test/regression/volatile2.c @@ -8,6 +8,14 @@ *((ty *) &x) = v2; \ printf("%s 2: %s\n", msg, *((volatile ty *) &x) == v2 ? "OK" : "FAILED"); +signed char gsc; +unsigned char guc; +signed short gss; +unsigned short gus; +int gi; +float gf; +double gd; + int main() { signed char sc; @@ -25,6 +33,13 @@ int main() TEST("int", int, i, 0x123456, 0x7890AB); TEST("float", float, f, 0.5, 256.0); TEST("double", double, d, 3.1415, 2.718); + TEST("global signed char", signed char, gsc, 12, 34); + TEST("global unsigned char", unsigned char, guc, 56, 78); + TEST("global signed short", signed short, gss, 1234, 5678); + TEST("global unsigned short", unsigned short, gus, 1357, 2468); + TEST("global int", int, gi, 0x123456, 0x7890AB); + TEST("global float", float, gf, 0.5, 256.0); + TEST("global double", double, gd, 3.1415, 2.718); return 0; } -- cgit v1.2.3