From 4f187fdafdac0cf4a8b83964c89d79741dbd813e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 21 Aug 2015 17:53:44 +0200 Subject: Adapt the PowerPC port to the new builtin representation. __builtin_get_spr() and __builtin_set_spr() work, but horrible error message if the SPR argument is not a constant. powerpc/AsmToJSON.ml needs updating. --- powerpc/Asm.v | 49 +++---- powerpc/AsmToJSON.ml | 11 +- powerpc/Asmexpand.ml | 357 +++++++++++++++++++++++++---------------------- powerpc/Asmgen.v | 4 +- powerpc/Asmgenproof.v | 44 ++---- powerpc/CBuiltins.ml | 7 +- powerpc/Machregs.v | 28 +++- powerpc/SelectOp.vp | 20 +-- powerpc/SelectOpproof.v | 6 +- powerpc/TargetPrinter.ml | 17 ++- 10 files changed, 285 insertions(+), 258 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asm.v b/powerpc/Asm.v index b7656dc4..a724f932 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -232,6 +232,8 @@ Inductive instruction : Type := | Pmr: ireg -> ireg -> instruction (**r integer move *) | Pmtctr: ireg -> instruction (**r move ireg to CTR *) | Pmtlr: ireg -> instruction (**r move ireg to LR *) + | Pmfspr: ireg -> int -> instruction (**r move from special register *) + | Pmtspr: int -> ireg -> instruction (**r move to special register *) | Pmulli: ireg -> ireg -> constant -> instruction (**r integer multiply immediate *) | Pmullw: ireg -> ireg -> ireg -> instruction (**r integer multiply *) | Pmulhw: ireg -> ireg -> ireg -> instruction (**r multiply high signed *) @@ -279,8 +281,7 @@ Inductive instruction : Type := | Pxori: ireg -> ireg -> constant -> instruction (**r bitwise xor with immediate *) | Pxoris: ireg -> ireg -> constant -> instruction (**r bitwise xor with immediate high *) | Plabel: label -> instruction (**r define a code label *) - | Pbuiltin: external_function -> list preg -> list preg -> instruction (**r built-in function (pseudo) *) - | Pannot: external_function -> list (annot_arg preg) -> instruction (**r annotation statement (pseudo) *) + | Pbuiltin: external_function -> list (builtin_arg preg) -> builtin_res preg -> instruction (**r built-in function (pseudo) *) | Pcfi_adjust: int -> instruction (**r .cfi_adjust debug directive *) | Pcfi_rel_offset: int -> instruction. (**r .cfi_rel_offset lr debug directive *) @@ -386,6 +387,15 @@ Fixpoint set_regs (rl: list preg) (vl: list val) (rs: regset) : regset := | _, _ => rs end. +(** Assigning the result of a builtin *) + +Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset := + match res with + | BR r => rs#r <- v + | BR_none => rs + | BR_longofwords hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs) + end. + Section RELSEM. (** Looking up instructions in a code sequence by position. *) @@ -852,10 +862,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr rs) m | Pbuiltin ef args res => Stuck (**r treated specially below *) - | Pannot ef args => - Stuck (**r treated specially below *) - (** The following instructions and directives are not generated directly by Asmgen, - so we do not model them. *) + (** The following instructions and directives are not generated + directly by [Asmgen], so we do not model them. *) | Pbdnz _ | Pcntlzw _ _ | Pcreqv _ _ _ @@ -881,6 +889,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Plhbrx _ _ _ | Plwzu _ _ _ | Pmfcr _ + | Pmfspr _ _ + | Pmtspr _ _ | Pstwbrx _ _ _ | Pstwcx_ _ _ _ | Pstfdu _ _ _ @@ -954,24 +964,16 @@ Inductive step: state -> trace -> state -> Prop := exec_instr f i rs m = Next rs' m' -> step (State rs m) E0 (State rs' m') | exec_step_builtin: - forall b ofs f ef args res rs m t vl rs' m', + forall b ofs f ef args res rs m vargs t vres rs' m', rs PC = Vptr b ofs -> Genv.find_funct_ptr ge b = Some (Internal f) -> find_instr (Int.unsigned ofs) f.(fn_code) = Some (Pbuiltin ef args res) -> - external_call' ef ge (map rs args) m t vl m' -> + eval_builtin_args ge rs (rs GPR1) m args vargs -> + external_call ef ge vargs m t vres m' -> rs' = nextinstr - (set_regs res vl + (set_res res vres (undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) -> step (State rs m) t (State rs' m') - | exec_step_annot: - forall b ofs f ef args rs m vargs t v m', - rs PC = Vptr b ofs -> - Genv.find_funct_ptr ge b = Some (Internal f) -> - find_instr (Int.unsigned ofs) f.(fn_code) = Some (Pannot ef args) -> - eval_annot_args ge rs (rs GPR1) m args vargs -> - external_call ef ge vargs m t v m' -> - step (State rs m) t - (State (nextinstr rs) m') | exec_step_external: forall b ef args res rs m t rs' m', rs PC = Vptr b Int.zero -> @@ -1035,12 +1037,8 @@ Ltac Equalities := split. constructor. auto. discriminate. discriminate. - inv H11. - exploit external_call_determ'. eexact H4. eexact H9. intros [A B]. - split. auto. intros. destruct B; auto. subst. auto. - inv H12. - assert (vargs0 = vargs) by (eapply eval_annot_args_determ; eauto). subst vargs0. - exploit external_call_determ. eexact H5. eexact H13. intros [A B]. + assert (vargs0 = vargs) by (eapply eval_builtin_args_determ; eauto). subst vargs0. + exploit external_call_determ. eexact H5. eexact H11. intros [A B]. split. auto. intros. destruct B; auto. subst. auto. assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0. exploit external_call_determ'. eexact H3. eexact H8. intros [A B]. @@ -1048,7 +1046,6 @@ Ltac Equalities := (* trace length *) red; intros. inv H; simpl. omega. - inv H3; eapply external_call_trace_length; eauto. eapply external_call_trace_length; eauto. inv H2; eapply external_call_trace_length; eauto. (* initial states *) @@ -1068,4 +1065,4 @@ Definition data_preg (r: preg) : bool := | CR0_0 => false | CR0_1 => false | CR0_2 => false | CR0_3 => false | CARRY => false | _ => true - end. \ No newline at end of file + end. diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index d66dd163..3440e16f 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -243,6 +243,8 @@ let p_instruction oc ic = | Pmr (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pmr\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 | Pmtctr ir -> fprintf oc "{\"Instruction Name\":\"Pmtctr\",\"Args\":[%a]}" p_ireg ir | Pmtlr ir -> fprintf oc "{\"Instruction Name\":\"Pmtlr\",\"Args\":[%a]}" p_ireg ir + | Pmfspr(ir, n) -> fprintf oc "{\"Instruction Name\":\"Pmfspr\",\"Args\":[%a,%a]}" p_ireg ir p_int n + | Pmtspr(n, ir) -> fprintf oc "{\"Instruction Name\":\"Pmtspr\",\"Args\":[%a,%a]}" p_int n p_ireg ir | Pmulli (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pmulli\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c | Pmullw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pmulw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pmulhw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pmulhw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 @@ -289,7 +291,9 @@ let p_instruction oc ic = | Pxori (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pxori\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c | Pxoris (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pxoris\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c | Plabel l -> fprintf oc "{\"Instruction Name\":\"Plabel\",\"Args\":[%a]}" p_label l - | Pbuiltin (ef,args1,args2) -> + | Pbuiltin (ef,args1,args2) -> () +(* FIXME *) +(* begin match ef with | EF_inline_asm (i,s,il) -> fprintf oc "{\"Instruction Name\":\"Inline_asm\",\"Args\":[%a%a%a%a]}" p_atom_constant i (p_list_cont p_char_list) il @@ -297,7 +301,8 @@ let p_instruction oc ic = | _ -> (* Should all be folded away *) assert false end - | Pannot _ (* We do not check the annotations *) +*) +(* END FIXME *) | Pcfi_adjust _ (* Only debug relevant *) | Pcfi_rel_offset _ -> () (* Only debug relevant *) @@ -329,7 +334,7 @@ let p_fundef oc (name,f) = let alignment = atom_alignof name and inline = atom_is_inline name and static = atom_is_static name - and instr = List.filter (function Pannot _ | Pcfi_adjust _ | Pcfi_rel_offset _ -> false | _ -> true) f.fn_code in + and instr = List.filter (function Pcfi_adjust _ | Pcfi_rel_offset _ -> false | _ -> true) f.fn_code in let c_section,l_section,j_section = match (atom_sections name) with [a;b;c] -> a,b,c | _ -> assert false in fprintf oc "{\"Fun Name\":%a,\n\"Fun Storage Class\":%a,\n\"Fun Alignment\":%a,\n\"Fun Section Code\":%a,\"Fun Section Literals\":%a,\"Fun Section Jumptable\":%a,\n\"Fun Inline\":%B,\n\"Fun Code\":%a}\n" p_atom name p_storage static p_int_opt alignment diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index ae4d694a..9f6c5f76 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -44,11 +44,11 @@ let emit_addimm rd rs n = (* Handling of annotations *) let expand_annot_val txt targ args res = - emit (Pannot(EF_annot(txt, [targ]), List.map (fun r -> AA_base r) args)); + emit (Pbuiltin(EF_annot(txt, [targ]), args, BR_none)); begin match args, res with - | [IR src], [IR dst] -> + | [BA(IR src)], BR(IR dst) -> if dst <> src then emit (Pmr(dst, src)) - | [FR src], [FR dst] -> + | [BA(FR src)], BR(FR dst) -> if dst <> src then emit (Pfmr(dst, src)) | _, _ -> assert false @@ -62,34 +62,64 @@ let expand_annot_val txt targ args res = So, use 64-bit accesses only if alignment >= 4. Note that lfd and stfd cannot trap on ill-formed floats. *) +let memcpy_small_arg sz arg otherarg tmp1 tmp2 = + match arg with + | BA (IR r) -> + (r, _0) + | BA_addrstack ofs -> + if Int.eq (Asmgen.high_s ofs) Int.zero + && Int.eq (Asmgen.high_s (Int.add ofs (Int.repr (Z.of_uint sz)))) + Int.zero + then (GPR1, ofs) + else begin + let tmp = if otherarg = BA (IR tmp1) then tmp2 else tmp1 in + emit_addimm tmp GPR1 ofs; + (tmp, _0) + end + | _ -> + assert false + let expand_builtin_memcpy_small sz al src dst = - let rec copy ofs sz = + let (rsrc, osrc) = memcpy_small_arg sz src dst GPR11 GPR12 in + let (rdst, odst) = memcpy_small_arg sz dst src GPR12 GPR11 in + let rec copy osrc odst sz = if sz >= 8 && al >= 4 && !Clflags.option_ffpu then begin - emit (Plfd(FPR13, Cint ofs, src)); - emit (Pstfd(FPR13, Cint ofs, dst)); - copy (Int.add ofs _8) (sz - 8) + emit (Plfd(FPR13, Cint osrc, rsrc)); + emit (Pstfd(FPR13, Cint odst, rdst)); + copy (Int.add osrc _8) (Int.add odst _8) (sz - 8) end else if sz >= 4 then begin - emit (Plwz(GPR0, Cint ofs, src)); - emit (Pstw(GPR0, Cint ofs, dst)); - copy (Int.add ofs _4) (sz - 4) + emit (Plwz(GPR0, Cint osrc, rsrc)); + emit (Pstw(GPR0, Cint odst, rdst)); + copy (Int.add osrc _4) (Int.add odst _4) (sz - 4) end else if sz >= 2 then begin - emit (Plhz(GPR0, Cint ofs, src)); - emit (Psth(GPR0, Cint ofs, dst)); - copy (Int.add ofs _2) (sz - 2) + emit (Plhz(GPR0, Cint osrc, rsrc)); + emit (Psth(GPR0, Cint odst, rdst)); + copy (Int.add osrc _2) (Int.add odst _2) (sz - 2) end else if sz >= 1 then begin - emit (Plbz(GPR0, Cint ofs, src)); - emit (Pstb(GPR0, Cint ofs, dst)); - copy (Int.add ofs _1) (sz - 1) + emit (Plbz(GPR0, Cint osrc, rsrc)); + emit (Pstb(GPR0, Cint odst, rdst)); + copy (Int.add osrc _1) (Int.add odst _1) (sz - 1) end in - copy _0 sz + copy osrc odst sz + +let memcpy_big_arg arg tmp = + (* Set [tmp] to the value of [arg] minus 4 *) + match arg with + | BA (IR r) -> + emit (Paddi(tmp, r, Cint _m4)) + | BA_addrstack ofs -> + emit_addimm tmp GPR1 (Int.add ofs _m4) + | _ -> + assert false let expand_builtin_memcpy_big sz al src dst = assert (sz >= 4); emit_loadimm GPR0 (Z.of_uint (sz / 4)); emit (Pmtctr GPR0); - let (s,d) = if dst <> GPR11 then (GPR11, GPR12) else (GPR12, GPR11) in - emit (Paddi(s, src, Cint _m4)); - emit (Paddi(d, dst, Cint _m4)); + let (s, d) = + if dst <> BA (IR GPR11) then (GPR11, GPR12) else (GPR12, GPR11) in + memcpy_big_arg src s; + memcpy_big_arg dst d; let lbl = new_label() in emit (Plabel lbl); emit (Plwzu(GPR0, Cint _4, s)); @@ -109,7 +139,7 @@ let expand_builtin_memcpy_big sz al src dst = let expand_builtin_memcpy sz al args = let (dst, src) = - match args with [IR d; IR s] -> (d, s) | _ -> assert false in + match args with [d; s] -> (d, s) | _ -> assert false in if sz <= (if !Clflags.option_ffpu && al >= 4 then if !Clflags.option_Osize then 35 else 51 else if !Clflags.option_Osize then 19 else 27) @@ -118,140 +148,129 @@ let expand_builtin_memcpy sz al args = (* Handling of volatile reads and writes *) -let expand_builtin_vload_common chunk base offset res = +let offset_constant cst delta = + match cst with + | Cint n -> + let n' = Int.add n delta in + if Int.eq (Asmgen.high_s n') Int.zero then Some (Cint n') else None + | Csymbol_sda(id, ofs) -> + Some (Csymbol_sda(id, Int.add ofs delta)) + | _ -> None + +let rec expand_builtin_vload_common chunk base offset res = match chunk, res with - | Mint8unsigned, IR res -> + | Mint8unsigned, BR(IR res) -> emit (Plbz(res, offset, base)) - | Mint8signed, IR res -> + | Mint8signed, BR(IR res) -> emit (Plbz(res, offset, base)); emit (Pextsb(res, res)) - | Mint16unsigned, IR res -> + | Mint16unsigned, BR(IR res) -> emit (Plhz(res, offset, base)) - | Mint16signed, IR res -> + | Mint16signed, BR(IR res) -> emit (Plha(res, offset, base)) - | (Mint32 | Many32), IR res -> + | (Mint32 | Many32), BR(IR res) -> emit (Plwz(res, offset, base)) - | Mfloat32, FR res -> + | Mfloat32, BR(FR res) -> emit (Plfs(res, offset, base)) - | (Mfloat64 | Many64), FR res -> + | (Mfloat64 | Many64), BR(FR res) -> emit (Plfd(res, offset, base)) - (* Mint64 is special-cased below *) - | _ -> - assert false + | Mint64, BR_longofwords(BR(IR hi), BR(IR lo)) -> + begin match offset_constant offset _4 with + | Some offset' -> + if hi <> base then begin + emit (Plwz(hi, offset, base)); + emit (Plwz(lo, offset', base)) + end else begin + emit (Plwz(lo, offset', base)); + emit (Plwz(hi, offset, base)) + end + | None -> + emit (Paddi(GPR11, base, offset)); + expand_builtin_vload_common chunk GPR11 (Cint _0) res + end + | _, _ -> assert false let expand_builtin_vload chunk args res = - begin match args, res with - | [IR addr], [res] when chunk <> Mint64 -> + match args with + | [BA(IR addr)] -> expand_builtin_vload_common chunk addr (Cint _0) res - | [IR addr], [IR res1; IR res2] when chunk = Mint64 -> - if addr <> res1 then begin - emit (Plwz(res1, Cint _0, addr)); - emit (Plwz(res2, Cint _4, addr)) + | [BA_addrstack ofs] -> + if Int.eq (Asmgen.high_s ofs) Int.zero then + expand_builtin_vload_common chunk GPR1 (Cint ofs) res + else begin + emit_addimm GPR11 GPR1 ofs; + expand_builtin_vload_common chunk GPR11 (Cint _0) res + end + | [BA_addrglobal(id, ofs)] -> + if symbol_is_small_data id ofs then + expand_builtin_vload_common chunk GPR0 (Csymbol_sda(id, ofs)) res + else if symbol_is_rel_data id ofs then begin + emit (Paddis(GPR11, GPR0, Csymbol_rel_high(id, ofs))); + expand_builtin_vload_common chunk GPR11 (Csymbol_rel_low(id, ofs)) res end else begin - emit (Plwz(res2, Cint _4, addr)); - emit (Plwz(res1, Cint _0, addr)) + emit (Paddis(GPR11, GPR0, Csymbol_high(id, ofs))); + expand_builtin_vload_common chunk GPR11 (Csymbol_low(id, ofs)) res end | _ -> assert false - end - -let expand_builtin_vload_global chunk id ofs args res = - begin match res with - | [res] when chunk <> Mint64 -> - emit (Paddis(GPR11, GPR0, Csymbol_high(id, ofs))); - expand_builtin_vload_common chunk GPR11 (Csymbol_low(id, ofs)) res - | [IR res1; IR res2] when chunk = Mint64 -> - emit (Paddis(res1, GPR0, Csymbol_high(id, ofs))); - emit (Plwz(res1, Csymbol_low(id, ofs), res1)); - let ofs = Int.add ofs _4 in - emit (Paddis(res2, GPR0, Csymbol_high(id, ofs))); - emit (Plwz(res2, Csymbol_low(id, ofs), res2)) - | _ -> - assert false - end - -let expand_builtin_vload_sda chunk id ofs args res = - begin match res with - | [res] when chunk <> Mint64 -> - expand_builtin_vload_common chunk GPR0 (Csymbol_sda(id, ofs)) res - | [IR res1; IR res2] when chunk = Mint64 -> - emit (Plwz(res1, Csymbol_sda(id, ofs), GPR0)); - let ofs = Int.add ofs _4 in - emit (Plwz(res2, Csymbol_sda(id, ofs), GPR0)) - | _ -> - assert false - end -let expand_builtin_vload_rel chunk id ofs args res = - emit (Paddis(GPR11, GPR0, Csymbol_rel_high(id, ofs))); - emit (Paddi(GPR11, GPR11, Csymbol_rel_low(id, ofs))); - expand_builtin_vload chunk [IR GPR11] res +let temp_for_vstore src = + let rl = AST.params_of_builtin_arg src in + if not (List.mem (IR GPR11) rl) then GPR11 + else if not (List.mem (IR GPR12) rl) then GPR12 + else GPR10 let expand_builtin_vstore_common chunk base offset src = match chunk, src with - | (Mint8signed | Mint8unsigned), IR src -> + | (Mint8signed | Mint8unsigned), BA(IR src) -> emit (Pstb(src, offset, base)) - | (Mint16signed | Mint16unsigned), IR src -> + | (Mint16signed | Mint16unsigned), BA(IR src) -> emit (Psth(src, offset, base)) - | (Mint32 | Many32), IR src -> + | (Mint32 | Many32), BA(IR src) -> emit (Pstw(src, offset, base)) - | Mfloat32, FR src -> + | Mfloat32, BA(FR src) -> emit (Pstfs(src, offset, base)) - | (Mfloat64 | Many64), FR src -> + | (Mfloat64 | Many64), BA(FR src) -> emit (Pstfd(src, offset, base)) - (* Mint64 is special-cased below *) - | _ -> - assert false + | Mint64, BA_longofwords(BA(IR hi), BA(IR lo)) -> + begin match offset_constant offset _4 with + | Some offset' -> + emit (Pstw(hi, offset, base)); + emit (Pstw(lo, offset', base)) + | None -> + let tmp = temp_for_vstore src in + emit (Paddi(tmp, base, offset)); + emit (Pstw(hi, Cint _0, tmp)); + emit (Pstw(lo, Cint _4, tmp)) + end + | _, _ -> assert false let expand_builtin_vstore chunk args = - begin match args with - | [IR addr; src] when chunk <> Mint64 -> + match args with + | [BA(IR addr); src] -> expand_builtin_vstore_common chunk addr (Cint _0) src - | [IR addr; IR src1; IR src2] when chunk = Mint64 -> - emit (Pstw(src1, Cint _0, addr)); - emit (Pstw(src2, Cint _4, addr)) - | _ -> - assert false - end - -let expand_builtin_vstore_global chunk id ofs args = - begin match args with - | [src] when chunk <> Mint64 -> - let tmp = if src = IR GPR11 then GPR12 else GPR11 in - emit (Paddis(tmp, GPR0, Csymbol_high(id, ofs))); - expand_builtin_vstore_common chunk tmp (Csymbol_low(id, ofs)) src - | [IR src1; IR src2] when chunk = Mint64 -> - let tmp = - if not (List.mem GPR12 [src1; src2]) then GPR12 else - if not (List.mem GPR11 [src1; src2]) then GPR11 else GPR10 in - emit (Paddis(tmp, GPR0, Csymbol_high(id, ofs))); - emit (Pstw(src1, Csymbol_low(id, ofs), tmp)); - let ofs = Int.add ofs _4 in - emit (Paddis(tmp, GPR0, Csymbol_high(id, ofs))); - emit (Pstw(src2, Csymbol_low(id, ofs), tmp)) - | _ -> - assert false - end - -let expand_builtin_vstore_sda chunk id ofs args = - begin match args with - | [src] when chunk <> Mint64 -> - expand_builtin_vstore_common chunk GPR0 (Csymbol_sda(id, ofs)) src - | [IR src1; IR src2] when chunk = Mint64 -> - emit (Pstw(src1, Csymbol_sda(id, ofs), GPR0)); - let ofs = Int.add ofs _4 in - emit (Pstw(src2, Csymbol_sda(id, ofs), GPR0)) + | [BA_addrstack ofs; src] -> + if Int.eq (Asmgen.high_s ofs) Int.zero then + expand_builtin_vstore_common chunk GPR1 (Cint ofs) src + else begin + let tmp = temp_for_vstore src in + emit_addimm tmp GPR1 ofs; + expand_builtin_vstore_common chunk tmp (Cint _0) src + end + | [BA_addrglobal(id, ofs); src] -> + if symbol_is_small_data id ofs then + expand_builtin_vstore_common chunk GPR0 (Csymbol_sda(id, ofs)) src + else if symbol_is_rel_data id ofs then begin + let tmp = temp_for_vstore src in + emit (Paddis(tmp, GPR0, Csymbol_rel_high(id, ofs))); + expand_builtin_vstore_common chunk tmp (Csymbol_rel_low(id, ofs)) src + end else begin + let tmp = temp_for_vstore src in + emit (Paddis(tmp, GPR0, Csymbol_high(id, ofs))); + expand_builtin_vstore_common chunk tmp (Csymbol_low(id, ofs)) src + end | _ -> assert false - end - -let expand_builtin_vstore_rel chunk id ofs args = - let tmp = - if not (List.mem (IR GPR12) args) then GPR12 else - if not (List.mem (IR GPR11) args) then GPR11 else GPR10 in - emit (Paddis(tmp, GPR0, Csymbol_rel_high(id, ofs))); - emit (Paddi(tmp, tmp, Csymbol_rel_low(id, ofs))); - expand_builtin_vstore chunk (IR tmp :: args) (* Handling of varargs *) @@ -308,43 +327,43 @@ let expand_builtin_inline name args res = (* Can use as temporaries: GPR0, FPR13 *) match name, args, res with (* Integer arithmetic *) - | "__builtin_mulhw", [IR a1; IR a2], [IR res] -> + | "__builtin_mulhw", [BA(IR a1); BA(IR a2)], BR(IR res) -> emit (Pmulhw(res, a1, a2)) - | "__builtin_mulhwu", [IR a1; IR a2], [IR res] -> + | "__builtin_mulhwu", [BA(IR a1); BA(IR a2)], BR(IR res) -> emit (Pmulhwu(res, a1, a2)) - | "__builtin_clz", [IR a1], [IR res] -> + | "__builtin_clz", [BA(IR a1)], BR(IR res) -> emit (Pcntlzw(res, a1)) - | ("__builtin_bswap" | "__builtin_bswap32"), [IR a1], [IR res] -> + | ("__builtin_bswap" | "__builtin_bswap32"), [BA(IR a1)], BR(IR res) -> emit (Pstwu(a1, Cint _m8, GPR1)); emit (Pcfi_adjust _8); emit (Plwbrx(res, GPR0, GPR1)); emit (Paddi(GPR1, GPR1, Cint _8)); emit (Pcfi_adjust _m8) - | "__builtin_bswap16", [IR a1], [IR res] -> + | "__builtin_bswap16", [BA(IR a1)], BR(IR res) -> emit (Prlwinm(GPR0, a1, _8, coqint_of_camlint 0x0000FF00l)); emit (Prlwinm(res, a1, coqint_of_camlint 24l, coqint_of_camlint 0x000000FFl)); emit (Por(res, GPR0, res)) (* Float arithmetic *) - | "__builtin_fmadd", [FR a1; FR a2; FR a3], [FR res] -> + | "__builtin_fmadd", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) -> emit (Pfmadd(res, a1, a2, a3)) - | "__builtin_fmsub", [FR a1; FR a2; FR a3], [FR res] -> + | "__builtin_fmsub", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) -> emit (Pfmsub(res, a1, a2, a3)) - | "__builtin_fnmadd", [FR a1; FR a2; FR a3], [FR res] -> + | "__builtin_fnmadd", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) -> emit (Pfnmadd(res, a1, a2, a3)) - | "__builtin_fnmsub", [FR a1; FR a2; FR a3], [FR res] -> + | "__builtin_fnmsub", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) -> emit (Pfnmsub(res, a1, a2, a3)) - | "__builtin_fabs", [FR a1], [FR res] -> + | "__builtin_fabs", [BA(FR a1)], BR(FR res) -> emit (Pfabs(res, a1)) - | "__builtin_fsqrt", [FR a1], [FR res] -> + | "__builtin_fsqrt", [BA(FR a1)], BR(FR res) -> emit (Pfsqrt(res, a1)) - | "__builtin_frsqrte", [FR a1], [FR res] -> + | "__builtin_frsqrte", [BA(FR a1)], BR(FR res) -> emit (Pfrsqrte(res, a1)) - | "__builtin_fres", [FR a1], [FR res] -> + | "__builtin_fres", [BA(FR a1)], BR(FR res) -> emit (Pfres(res, a1)) - | "__builtin_fsel", [FR a1; FR a2; FR a3], [FR res] -> + | "__builtin_fsel", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) -> emit (Pfsel(res, a1, a2, a3)) - | "__builtin_fcti", [FR a1], [IR res] -> + | "__builtin_fcti", [BA(FR a1)], BR(IR res) -> emit (Pfctiw(FPR13, a1)); emit (Pstfdu(FPR13, Cint _m8, GPR1)); emit (Pcfi_adjust _8); @@ -352,30 +371,36 @@ let expand_builtin_inline name args res = emit (Paddi(GPR1, GPR1, Cint _8)); emit (Pcfi_adjust _m8) (* 64-bit integer arithmetic *) - | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] -> + | "__builtin_negl", [BA_longofwords(BA(IR ah), BA(IR al))], + BR_longofwords(BR(IR rh), BR(IR rl)) -> 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] -> + | "__builtin_addl", [BA_longofwords(BA(IR ah), BA(IR al)); + BA_longofwords(BA(IR bh), BA(IR bl))], + BR_longofwords(BR(IR rh), BR(IR rl)) -> 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] -> + | "__builtin_subl", [BA_longofwords(BA(IR ah), BA(IR al)); + BA_longofwords(BA(IR bh), BA(IR bl))], + BR_longofwords(BR(IR rh), BR(IR rl)) -> 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] -> + | "__builtin_mull", [BA(IR a); BA(IR b)], + BR_longofwords(BR(IR rh), BR(IR rl)) -> expand_int64_arith (rl = a || rl = b) rl (fun rl -> emit (Pmullw(rl, a, b)); emit (Pmulhwu(rh, a, b))) (* Memory accesses *) - | "__builtin_read16_reversed", [IR a1], [IR res] -> + | "__builtin_read16_reversed", [BA(IR a1)], BR(IR res) -> emit (Plhbrx(res, GPR0, a1)) - | "__builtin_read32_reversed", [IR a1], [IR res] -> + | "__builtin_read32_reversed", [BA(IR a1)], BR(IR res) -> emit (Plwbrx(res, GPR0, a1)) - | "__builtin_write16_reversed", [IR a1; IR a2], _ -> + | "__builtin_write16_reversed", [BA(IR a1); BA(IR a2)], _ -> emit (Psthbrx(a2, GPR0, a1)) - | "__builtin_write32_reversed", [IR a1; IR a2], _ -> + | "__builtin_write32_reversed", [BA(IR a1); BA(IR a2)], _ -> emit (Pstwbrx(a2, GPR0, a1)) (* Synchronization *) | "__builtin_membar", [], _ -> @@ -391,15 +416,25 @@ let expand_builtin_inline name args res = | "__builtin_trap", [], _ -> emit (Ptrap) (* Vararg stuff *) - | "__builtin_va_start", [IR a], _ -> + | "__builtin_va_start", [BA(IR a)], _ -> expand_builtin_va_start a - (* Catch-all *) - | "__builtin_dcbf", [IR a1],_ -> + (* Cache control *) + | "__builtin_dcbf", [BA(IR a1)],_ -> emit (Pdcbf (GPR0,a1)) - | "__builtin_dcbi", [IR a1],_ -> + | "__builtin_dcbi", [BA(IR a1)],_ -> emit (Pdcbi (GPR0,a1)) - | "__builtin_icbi", [IR a1],_ -> + | "__builtin_icbi", [BA(IR a1)],_ -> emit (Picbi(GPR0,a1)) + (* Special registers *) + | "__builtin_get_spr", [BA_int n], BR(IR res) -> + emit (Pmfspr(res, n)) + | "__builtin_get_spr", _, _ -> + invalid_arg ("the argument of __builtin_get_spr must be a constant") + | "__builtin_set_spr", [BA_int n; BA(IR a1)], _ -> + emit (Pmtspr(n, a1)) + | "__builtin_set_spr", _, _ -> + invalid_arg ("the first argument of __builtin_set_spr must be a constant") + (* Catch-all *) | _ -> invalid_arg ("unrecognized builtin " ^ name) @@ -484,25 +519,11 @@ let expand_instruction instr = expand_builtin_vload chunk args res | EF_vstore chunk -> expand_builtin_vstore chunk args - | EF_vload_global(chunk, id, ofs) -> - if symbol_is_small_data id ofs then - expand_builtin_vload_sda chunk id ofs args res - else if symbol_is_rel_data id ofs then - expand_builtin_vload_rel chunk id ofs args res - else - expand_builtin_vload_global chunk id ofs args res - | EF_vstore_global(chunk, id, ofs) -> - if symbol_is_small_data id ofs then - expand_builtin_vstore_sda chunk id ofs args - else if symbol_is_rel_data id ofs then - expand_builtin_vstore_rel chunk id ofs args - else - expand_builtin_vstore_global chunk id ofs args | EF_memcpy(sz, al) -> expand_builtin_memcpy (Z.to_int sz) (Z.to_int al) args | EF_annot_val(txt, targ) -> expand_annot_val txt targ args res - | EF_inline_asm(txt, sg, clob) -> + | EF_annot _ | EF_debug _ | EF_inline_asm _ -> emit instr | _ -> assert false diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 7ee6c770..541fe7c6 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -648,9 +648,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbs symb sig :: k) | Mbuiltin ef args res => - OK (Pbuiltin ef (map preg_of args) (map preg_of res) :: k) - | Mannot ef args => - OK (Pannot ef (List.map (map_annot_arg preg_of) args) :: k) + OK (Pbuiltin ef (List.map (map_builtin_arg preg_of) args) (map_builtin_res preg_of res) :: k) | Mlabel lbl => OK (Plabel lbl :: k) | Mgoto lbl => diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 27b32ba1..ece6af1a 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -754,48 +754,32 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen. unfold rs5; auto 10 with asmgen. - (* Mbuiltin *) - inv AT. monadInv H3. + inv AT. monadInv H4. exploit functions_transl; eauto. intro FN. - generalize (transf_function_no_overflow _ _ H2); intro NOOV. - exploit external_call_mem_extends'; eauto. eapply preg_vals; eauto. + generalize (transf_function_no_overflow _ _ H3); intro NOOV. + exploit builtin_args_match; eauto. intros [vargs' [P Q]]. + exploit external_call_mem_extends; eauto. intros [vres' [m2' [A [B [C D]]]]]. left. econstructor; split. apply plus_one. eapply exec_step_builtin. eauto. eauto. eapply find_instr_tail; eauto. - eapply external_call_symbols_preserved'; eauto. + erewrite <- sp_val by eauto. + eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eauto. econstructor; eauto. - Simpl. rewrite set_pregs_other_2. rewrite undef_regs_other_2. rewrite <- H0. simpl. econstructor; eauto. + instantiate (2 := tf); instantiate (1 := x). + unfold nextinstr. rewrite Pregmap.gss. + rewrite set_res_other. rewrite undef_regs_other_2. + rewrite <- H1. simpl. econstructor; eauto. eapply code_tail_next_int; eauto. - apply preg_notin_charact; auto with asmgen. - apply preg_notin_charact; auto with asmgen. - apply agree_nextinstr. eapply agree_set_mregs; auto. + rewrite preg_notin_charact. intros. auto with asmgen. + auto with asmgen. + apply agree_nextinstr. eapply agree_set_res; auto. eapply agree_undef_regs; eauto. intros; apply undef_regs_other_2; auto. congruence. -- (* Mannot *) - inv AT. monadInv H4. - exploit functions_transl; eauto. intro FN. - generalize (transf_function_no_overflow _ _ H3); intro NOOV. - exploit annot_args_match; eauto. intros [vargs' [P Q]]. - exploit external_call_mem_extends; eauto. - intros [vres' [m2' [A [B [C D]]]]]. - left. econstructor; split. apply plus_one. - eapply exec_step_annot. eauto. eauto. - eapply find_instr_tail; eauto. eauto. - erewrite <- sp_val by eauto. - eapply eval_annot_args_preserved with (ge1 := ge); eauto. - exact symbols_preserved. - eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - eapply match_states_intro with (ep := false); eauto with coqlib. - unfold nextinstr. rewrite Pregmap.gss. - rewrite <- H1; simpl. econstructor; eauto. - eapply code_tail_next_int; eauto. - apply agree_nextinstr. auto. - congruence. - - (* Mgoto *) assert (f0 = f) by congruence. subst f0. inv AT. monadInv H4. diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index 06a7e395..75dbd23d 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -93,7 +93,12 @@ let builtins = { "__builtin_dcbi", (TVoid [],[TPtr(TVoid [], [])],false); "__builtin_icbi", - (TVoid [],[TPtr(TVoid [], [])],false) + (TVoid [],[TPtr(TVoid [], [])],false); + (* Access to special registers *) + "__builtin_get_spr", + (TInt(IUInt, []), [TInt(IInt, [])], false); + "__builtin_set_spr", + (TVoid [], [TInt(IInt, []); TInt(IUInt, [])], false) ] } diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index 3b7cbb76..b9af652a 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -163,11 +163,9 @@ Fixpoint destroyed_by_clobber (cl: list string): list mreg := Definition destroyed_by_builtin (ef: external_function): list mreg := match ef with | EF_builtin _ _ => F13 :: nil - | EF_vload _ => nil - | EF_vstore _ => nil - | EF_vload_global _ _ _ => R11 :: nil - | EF_vstore_global Mint64 _ _ => R10 :: R11 :: R12 :: nil - | EF_vstore_global _ _ _ => R11 :: R12 :: nil + | EF_vload _ => R11 :: nil + | EF_vstore Mint64 => R10 :: R11 :: R12 :: nil + | EF_vstore _ => R11 :: R12 :: nil | EF_memcpy _ _ => R11 :: R12 :: F13 :: nil | EF_inline_asm txt sg clob => destroyed_by_clobber clob | _ => nil @@ -203,3 +201,23 @@ Definition two_address_op (op: operation) : bool := | Oroli _ _ => true | _ => false end. + +(* Constraints on constant propagation for builtins *) + +Definition builtin_get_spr := ident_of_string "__builtin_get_spr". +Definition builtin_set_spr := ident_of_string "__builtin_set_spr". + +Definition builtin_constraints (ef: external_function) : + list builtin_arg_constraint := + match ef with + | EF_builtin id sg => + if ident_eq id builtin_get_spr then OK_const :: nil + else if ident_eq id builtin_set_spr then OK_const :: OK_default :: nil + else nil + | EF_vload _ => OK_addrany :: nil + | EF_vstore _ => OK_addrany :: OK_default :: nil + | EF_memcpy _ _ => OK_addrstack :: OK_addrstack :: nil + | EF_annot txt targs => map (fun _ => OK_all) targs + | EF_debug kind txt targs => map (fun _ => OK_all) targs + | _ => nil + end. diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index 618643b8..31f7e2e4 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -524,17 +524,17 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) := | _ => (Aindexed Int.zero, e:::Enil) end. -(** ** Arguments of annotations *) +(** ** Arguments of builtins *) -Nondetfunction annot_arg (e: expr) := +Nondetfunction builtin_arg (e: expr) := match e with - | Eop (Ointconst n) Enil => AA_int n - | Eop (Oaddrsymbol id ofs) Enil => AA_addrglobal id ofs - | Eop (Oaddrstack ofs) Enil => AA_addrstack ofs + | Eop (Ointconst n) Enil => BA_int n + | Eop (Oaddrsymbol id ofs) Enil => BA_addrglobal id ofs + | Eop (Oaddrstack ofs) Enil => BA_addrstack ofs | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) => - AA_long (Int64.ofwords h l) - | Eop Omakelong (h ::: l ::: Enil) => AA_longofwords (AA_base h) (AA_base l) - | Eload chunk (Aglobal id ofs) Enil => AA_loadglobal chunk id ofs - | Eload chunk (Ainstack ofs) Enil => AA_loadstack chunk ofs - | _ => AA_base e + BA_long (Int64.ofwords h l) + | Eop Omakelong (h ::: l ::: Enil) => BA_longofwords (BA h) (BA l) + | Eload chunk (Aglobal id ofs) Enil => BA_loadglobal chunk id ofs + | Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs + | _ => BA e end. diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index c51b650b..147132dd 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -999,12 +999,12 @@ Proof. rewrite Int.add_zero. auto. Qed. -Theorem eval_annot_arg: +Theorem eval_builtin_arg: forall a v, eval_expr ge sp e m nil a v -> - CminorSel.eval_annot_arg ge sp e m (annot_arg a) v. + CminorSel.eval_builtin_arg ge sp e m (builtin_arg a) v. Proof. - intros until v. unfold annot_arg; case (annot_arg_match a); intros; InvEval. + intros until v. unfold builtin_arg; case (builtin_arg_match a); intros; InvEval. - constructor. - constructor. - constructor. diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 8610f750..5431d88d 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -599,6 +599,10 @@ module Target (System : SYSTEM):TARGET = fprintf oc " mtctr %a\n" ireg r1 | Pmtlr(r1) -> fprintf oc " mtlr %a\n" ireg r1 + | Pmfspr(rd, spr) -> + fprintf oc " mfspr %a, %ld\n" ireg rd (camlint_of_coqint spr) + | Pmtspr(spr, rs) -> + fprintf oc " mtspr %ld, %a\n" (camlint_of_coqint spr) ireg rs | Pmulli(r1, r2, c) -> fprintf oc " mulli %a, %a, %a\n" ireg r1 ireg r2 constant c | Pmullw(r1, r2, r3) -> @@ -693,6 +697,8 @@ module Target (System : SYSTEM):TARGET = fprintf oc "%a:\n" label (transl_label lbl) | Pbuiltin(ef, args, res) -> begin match ef with + | EF_annot(txt, targs) -> + print_annot_stmt oc (extern_atom txt) targs args | EF_inline_asm(txt, sg, clob) -> fprintf oc "%s begin inline assembly\n\t" comment; print_inline_asm preg oc (extern_atom txt) sg args res; @@ -700,13 +706,6 @@ module Target (System : SYSTEM):TARGET = | _ -> assert false end - | Pannot(ef, args) -> - begin match ef with - | EF_annot(txt, targs) -> - print_annot_stmt oc (extern_atom txt) targs args - | _ -> - assert false - end | Pcfi_adjust n -> cfi_adjust oc (camlint_of_coqint n) | Pcfi_rel_offset n -> @@ -731,8 +730,8 @@ module Target (System : SYSTEM):TARGET = | Plfi(r1, c) -> 2 | Plfis(r1, c) -> 2 | Plabel lbl -> 0 - | Pbuiltin(ef, args, res) -> 0 - | Pannot(ef, args) -> 0 + | Pbuiltin((EF_annot _ | EF_debug _), args, res) -> 0 + | Pbuiltin(ef, args, res) -> 3 | Pcfi_adjust _ | Pcfi_rel_offset _ -> 0 | _ -> 1 -- cgit From 33dfbe7601ad16fcea5377563fa7ceb4053cb85a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 22 Aug 2015 09:46:37 +0200 Subject: Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong. Use EF_debug instead of EF_annot for line number annotations. Introduce PrintAsmaux.print_debug_info (very incomplete). powerpc/Asmexpand: revise expand_memcpy_small. --- powerpc/Asm.v | 2 +- powerpc/Asmexpand.ml | 36 +++++++++++++++++------------------- powerpc/SelectOp.vp | 2 +- powerpc/TargetPrinter.ml | 17 +++++------------ 4 files changed, 24 insertions(+), 33 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asm.v b/powerpc/Asm.v index a724f932..589d66fe 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -393,7 +393,7 @@ Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset := match res with | BR r => rs#r <- v | BR_none => rs - | BR_longofwords hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs) + | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs) end. Section RELSEM. diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 9f6c5f76..e09291cc 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -62,7 +62,7 @@ let expand_annot_val txt targ args res = So, use 64-bit accesses only if alignment >= 4. Note that lfd and stfd cannot trap on ill-formed floats. *) -let memcpy_small_arg sz arg otherarg tmp1 tmp2 = +let memcpy_small_arg sz arg tmp = match arg with | BA (IR r) -> (r, _0) @@ -71,17 +71,15 @@ let memcpy_small_arg sz arg otherarg tmp1 tmp2 = && Int.eq (Asmgen.high_s (Int.add ofs (Int.repr (Z.of_uint sz)))) Int.zero then (GPR1, ofs) - else begin - let tmp = if otherarg = BA (IR tmp1) then tmp2 else tmp1 in - emit_addimm tmp GPR1 ofs; - (tmp, _0) - end + else begin emit_addimm tmp GPR1 ofs; (tmp, _0) end | _ -> assert false let expand_builtin_memcpy_small sz al src dst = - let (rsrc, osrc) = memcpy_small_arg sz src dst GPR11 GPR12 in - let (rdst, odst) = memcpy_small_arg sz dst src GPR12 GPR11 in + let (tsrc, tdst) = + if dst <> BA (IR GPR11) then (GPR11, GPR12) else (GPR12, GPR11) in + let (rsrc, osrc) = memcpy_small_arg sz src tsrc in + let (rdst, odst) = memcpy_small_arg sz dst tdst in let rec copy osrc odst sz = if sz >= 8 && al >= 4 && !Clflags.option_ffpu then begin emit (Plfd(FPR13, Cint osrc, rsrc)); @@ -174,7 +172,7 @@ let rec expand_builtin_vload_common chunk base offset res = emit (Plfs(res, offset, base)) | (Mfloat64 | Many64), BR(FR res) -> emit (Plfd(res, offset, base)) - | Mint64, BR_longofwords(BR(IR hi), BR(IR lo)) -> + | Mint64, BR_splitlong(BR(IR hi), BR(IR lo)) -> begin match offset_constant offset _4 with | Some offset' -> if hi <> base then begin @@ -232,7 +230,7 @@ let expand_builtin_vstore_common chunk base offset src = emit (Pstfs(src, offset, base)) | (Mfloat64 | Many64), BA(FR src) -> emit (Pstfd(src, offset, base)) - | Mint64, BA_longofwords(BA(IR hi), BA(IR lo)) -> + | Mint64, BA_splitlong(BA(IR hi), BA(IR lo)) -> begin match offset_constant offset _4 with | Some offset' -> emit (Pstw(hi, offset, base)); @@ -371,25 +369,25 @@ let expand_builtin_inline name args res = emit (Paddi(GPR1, GPR1, Cint _8)); emit (Pcfi_adjust _m8) (* 64-bit integer arithmetic *) - | "__builtin_negl", [BA_longofwords(BA(IR ah), BA(IR al))], - BR_longofwords(BR(IR rh), BR(IR rl)) -> + | "__builtin_negl", [BA_splitlong(BA(IR ah), BA(IR al))], + BR_splitlong(BR(IR rh), BR(IR rl)) -> expand_int64_arith (rl = ah) rl (fun rl -> emit (Psubfic(rl, al, Cint _0)); emit (Psubfze(rh, ah))) - | "__builtin_addl", [BA_longofwords(BA(IR ah), BA(IR al)); - BA_longofwords(BA(IR bh), BA(IR bl))], - BR_longofwords(BR(IR rh), BR(IR rl)) -> + | "__builtin_addl", [BA_splitlong(BA(IR ah), BA(IR al)); + BA_splitlong(BA(IR bh), BA(IR bl))], + BR_splitlong(BR(IR rh), BR(IR rl)) -> expand_int64_arith (rl = ah || rl = bh) rl (fun rl -> emit (Paddc(rl, al, bl)); emit (Padde(rh, ah, bh))) - | "__builtin_subl", [BA_longofwords(BA(IR ah), BA(IR al)); - BA_longofwords(BA(IR bh), BA(IR bl))], - BR_longofwords(BR(IR rh), BR(IR rl)) -> + | "__builtin_subl", [BA_splitlong(BA(IR ah), BA(IR al)); + BA_splitlong(BA(IR bh), BA(IR bl))], + BR_splitlong(BR(IR rh), BR(IR rl)) -> expand_int64_arith (rl = ah || rl = bh) rl (fun rl -> emit (Psubfc(rl, bl, al)); emit (Psubfe(rh, bh, ah))) | "__builtin_mull", [BA(IR a); BA(IR b)], - BR_longofwords(BR(IR rh), BR(IR rl)) -> + BR_splitlong(BR(IR rh), BR(IR rl)) -> expand_int64_arith (rl = a || rl = b) rl (fun rl -> emit (Pmullw(rl, a, b)); emit (Pmulhwu(rh, a, b))) diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index 31f7e2e4..6d39569e 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -533,7 +533,7 @@ Nondetfunction builtin_arg (e: expr) := | Eop (Oaddrstack ofs) Enil => BA_addrstack ofs | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) => BA_long (Int64.ofwords h l) - | Eop Omakelong (h ::: l ::: Enil) => BA_longofwords (BA h) (BA l) + | Eop Omakelong (h ::: l ::: Enil) => BA_splitlong (BA h) (BA l) | Eload chunk (Aglobal id ofs) Enil => BA_loadglobal chunk id ofs | Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs | _ => BA e diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 5431d88d..ced26783 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -358,17 +358,6 @@ module Target (System : SYSTEM):TARGET = assert (!count = 2 || (!count = 0 && !last)); (!mb, !me-1) - (* Handling of annotations *) - - let print_annot_stmt oc txt targs args = - if Str.string_match re_file_line txt 0 then begin - print_file_line oc (Str.matched_group 1 txt) - (int_of_string (Str.matched_group 2 txt)) - end else begin - fprintf oc "%s annotation: " comment; - print_annot_stmt preg_annot "R1" oc txt targs args - end - (* Determine if the displacement of a conditional branch fits the short form *) let short_cond_branch tbl pc lbl_dest = @@ -698,7 +687,11 @@ module Target (System : SYSTEM):TARGET = | Pbuiltin(ef, args, res) -> begin match ef with | EF_annot(txt, targs) -> - print_annot_stmt oc (extern_atom txt) targs args + fprintf oc "%s annotation: " comment; + print_annot_text preg_annot "r1" oc (extern_atom txt) args + | EF_debug(kind, txt, targs) -> + print_debug_info comment print_file_line preg_annot "r1" oc + (P.to_int kind) (extern_atom txt) args | EF_inline_asm(txt, sg, clob) -> fprintf oc "%s begin inline assembly\n\t" comment; print_inline_asm preg oc (extern_atom txt) sg args res; -- cgit From e5be647428d5aa2139dd8fd2e86b8046b4d0aa35 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 24 Aug 2015 15:08:49 +0200 Subject: Improve error reporting in Asmexpand. --- powerpc/Asmexpand.ml | 51 ++++++++++++++++++++++++++++++++------------------- 1 file changed, 32 insertions(+), 19 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index e09291cc..5216214b 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -21,6 +21,7 @@ open Memdata open Asm open Asmexpandaux +exception Error of string (* Useful constants and helper functions *) @@ -51,7 +52,7 @@ let expand_annot_val txt targ args res = | [BA(FR src)], BR(FR dst) -> if dst <> src then emit (Pfmr(dst, src)) | _, _ -> - assert false + raise (Error "ill-formed __builtin_annot_val") end (* Handling of memcpy *) @@ -62,14 +63,16 @@ let expand_annot_val txt targ args res = So, use 64-bit accesses only if alignment >= 4. Note that lfd and stfd cannot trap on ill-formed floats. *) +let offset_in_range ofs = + Int.eq (Asmgen.high_s ofs) Int.zero + let memcpy_small_arg sz arg tmp = match arg with | BA (IR r) -> (r, _0) | BA_addrstack ofs -> - if Int.eq (Asmgen.high_s ofs) Int.zero - && Int.eq (Asmgen.high_s (Int.add ofs (Int.repr (Z.of_uint sz)))) - Int.zero + if offset_in_range ofs + && offset_in_range (Int.add ofs (Int.repr (Z.of_uint sz))) then (GPR1, ofs) else begin emit_addimm tmp GPR1 ofs; (tmp, _0) end | _ -> @@ -150,7 +153,7 @@ let offset_constant cst delta = match cst with | Cint n -> let n' = Int.add n delta in - if Int.eq (Asmgen.high_s n') Int.zero then Some (Cint n') else None + if offset_in_range n' then Some (Cint n') else None | Csymbol_sda(id, ofs) -> Some (Csymbol_sda(id, Int.add ofs delta)) | _ -> None @@ -186,14 +189,15 @@ let rec expand_builtin_vload_common chunk base offset res = emit (Paddi(GPR11, base, offset)); expand_builtin_vload_common chunk GPR11 (Cint _0) res end - | _, _ -> assert false + | _, _ -> + assert false let expand_builtin_vload chunk args res = match args with | [BA(IR addr)] -> expand_builtin_vload_common chunk addr (Cint _0) res | [BA_addrstack ofs] -> - if Int.eq (Asmgen.high_s ofs) Int.zero then + if offset_in_range ofs then expand_builtin_vload_common chunk GPR1 (Cint ofs) res else begin emit_addimm GPR11 GPR1 ofs; @@ -241,14 +245,15 @@ let expand_builtin_vstore_common chunk base offset src = emit (Pstw(hi, Cint _0, tmp)); emit (Pstw(lo, Cint _4, tmp)) end - | _, _ -> assert false + | _, _ -> + assert false let expand_builtin_vstore chunk args = match args with | [BA(IR addr); src] -> expand_builtin_vstore_common chunk addr (Cint _0) src | [BA_addrstack ofs; src] -> - if Int.eq (Asmgen.high_s ofs) Int.zero then + if offset_in_range ofs then expand_builtin_vstore_common chunk GPR1 (Cint ofs) src else begin let tmp = temp_for_vstore src in @@ -427,14 +432,14 @@ let expand_builtin_inline name args res = | "__builtin_get_spr", [BA_int n], BR(IR res) -> emit (Pmfspr(res, n)) | "__builtin_get_spr", _, _ -> - invalid_arg ("the argument of __builtin_get_spr must be a constant") + raise (Error "the argument of __builtin_get_spr must be a constant") | "__builtin_set_spr", [BA_int n; BA(IR a1)], _ -> emit (Pmtspr(n, a1)) | "__builtin_set_spr", _, _ -> - invalid_arg ("the first argument of __builtin_set_spr must be a constant") + raise (Error "the first argument of __builtin_set_spr must be a constant") (* Catch-all *) | _ -> - invalid_arg ("unrecognized builtin " ^ name) + raise (Error ("unrecognized builtin " ^ name)) (* Calls to variadic functions: condition bit 6 must be set if at least one argument is a float; clear otherwise. @@ -530,13 +535,21 @@ let expand_instruction instr = emit instr let expand_function fn = - set_current_function fn; - List.iter expand_instruction fn.fn_code; - get_current_function () + try + set_current_function fn; + List.iter expand_instruction fn.fn_code; + Errors.OK (get_current_function ()) + with Error s -> + Errors.Error (Errors.msg (coqstring_of_camlstring s)) let expand_fundef = function - | Internal f -> Internal (expand_function f) - | External ef -> External ef + | Internal f -> + begin match expand_function f with + | Errors.OK tf -> Errors.OK (Internal tf) + | Errors.Error msg -> Errors.Error msg + end + | External ef -> + Errors.OK (External ef) -let expand_program (p: Asm.program) : Asm.program = - AST.transform_program expand_fundef p +let expand_program (p: Asm.program) : Asm.program Errors.res = + AST.transform_partial_program expand_fundef p -- cgit From 75d50c12ee220fecf955b1626c78b78636cbca92 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 1 Sep 2015 16:44:29 +0200 Subject: Added the gcc builtin prefetch. This commit implements the gcc __builtin_prefetch in a form with all arguments for the powerpc architecture. The resulting instructions are the dcbt and dcbtst instructions in Server Category. --- powerpc/Asm.v | 4 ++++ powerpc/AsmToJSON.ml | 2 ++ powerpc/Asmexpand.ml | 11 +++++++++++ powerpc/CBuiltins.ml | 2 ++ powerpc/Machregs.v | 2 ++ powerpc/TargetPrinter.ml | 4 ++++ 6 files changed, 25 insertions(+) (limited to 'powerpc') diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 589d66fe..dbb819d1 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -167,6 +167,8 @@ Inductive instruction : Type := | Pcrxor: crbit -> crbit -> crbit -> instruction (**r xor between condition bits *) | Pdcbf: ireg -> ireg -> instruction (**r data cache flush *) | Pdcbi: ireg -> ireg -> instruction (**r data cache invalidate *) + | Pdcbt: int -> ireg -> instruction (**r data cache block touch *) + | Pdcbtst: int -> ireg -> instruction (**r data cache block touch *) | Pdivw: ireg -> ireg -> ireg -> instruction (**r signed division *) | Pdivwu: ireg -> ireg -> ireg -> instruction (**r unsigned division *) | Peieio: instruction (**r EIEIO barrier *) @@ -870,6 +872,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pcrxor _ _ _ | Pdcbf _ _ | Pdcbi _ _ + | Pdcbt _ _ + | Pdcbtst _ _ | Peieio | Pfctiw _ _ | Pfctiwz _ _ diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 3440e16f..fb73aec5 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -177,6 +177,8 @@ let p_instruction oc ic = | Pcrxor (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcrxor\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3 | Pdcbf (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pdcbf\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 | Pdcbi (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pdcbi\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 + | Pdcbt (n,ir1) -> fprintf oc "{\"Instruction Name\":\"Pdcbt\",\"Args\":[%a,%a]}" p_int n p_ireg ir1 + | Pdcbtst (n,ir1) -> fprintf oc "{\"Instruction Name\":\"Pdcbtst\",\"Args\":[%a,%a]}" p_int n p_ireg ir1 | Pdivw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pdivw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pdivwu (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pdivwu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Peieio -> fprintf oc "{\"Instruction Name\":\"Peieio,\"Args\":[]}" diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 5216214b..57765c50 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -428,6 +428,17 @@ let expand_builtin_inline name args res = emit (Pdcbi (GPR0,a1)) | "__builtin_icbi", [BA(IR a1)],_ -> emit (Picbi(GPR0,a1)) + | "__builtin_prefetch" , [BA (IR addr);BA_int rw; BA_int loc],_ -> + if not ((loc >= _0) && (loc < _4)) then + raise (Error "the last argument of __builtin_prefetch must be a constant between 0 and 3"); + if Int.eq rw _0 then begin + emit (Pdcbt (loc,addr)); + end else if Int.eq rw _1 then begin + emit (Pdcbtst (loc,addr)); + end else + raise (Error "the second argument of __builtin_prefetch must be either 0 or 1") + | "__builtin_prefetch" ,_,_ -> + raise (Error "the second and third argument of __builtin_prefetch must be a constant") (* Special registers *) | "__builtin_get_spr", [BA_int n], BR(IR res) -> emit (Pmfspr(res, n)) diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index 75dbd23d..701690b2 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -94,6 +94,8 @@ let builtins = { (TVoid [],[TPtr(TVoid [], [])],false); "__builtin_icbi", (TVoid [],[TPtr(TVoid [], [])],false); + "__builtin_prefetch", + (TVoid [], [TPtr (TVoid [],[]);TInt (IInt, []);TInt (IInt,[])],false); (* Access to special registers *) "__builtin_get_spr", (TInt(IUInt, []), [TInt(IInt, [])], false); diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index b9af652a..62a4a0a5 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -206,6 +206,7 @@ Definition two_address_op (op: operation) : bool := Definition builtin_get_spr := ident_of_string "__builtin_get_spr". Definition builtin_set_spr := ident_of_string "__builtin_set_spr". +Definition builtin_prefetch := ident_of_string "__builtin_prefetch". Definition builtin_constraints (ef: external_function) : list builtin_arg_constraint := @@ -213,6 +214,7 @@ Definition builtin_constraints (ef: external_function) : | EF_builtin id sg => if ident_eq id builtin_get_spr then OK_const :: nil else if ident_eq id builtin_set_spr then OK_const :: OK_default :: nil + else if ident_eq id builtin_prefetch then OK_addrany :: OK_const :: OK_const :: nil else nil | EF_vload _ => OK_addrany :: nil | EF_vstore _ => OK_addrany :: OK_default :: nil diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index ced26783..b0f296ef 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -462,6 +462,10 @@ module Target (System : SYSTEM):TARGET = fprintf oc " dcbf %a, %a\n" ireg r1 ireg r2 | Pdcbi (r1,r2) -> fprintf oc " dcbi %a, %a\n" ireg r1 ireg r2 + | Pdcbt (c,r1) -> + fprintf oc " dcbt %a, %a, %s\n" ireg GPR0 ireg r1 (Z.to_string c) + | Pdcbtst (c,r1) -> + fprintf oc " dcbtst %a, %a, %s\n" ireg GPR0 ireg r1 (Z.to_string c) | Pdivw(r1, r2, r3) -> fprintf oc " divw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pdivwu(r1, r2, r3) -> -- cgit From db8e35c6abf58c82853b94f416aa76b33efc1f65 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 2 Sep 2015 13:50:24 +0200 Subject: Added builtin for dcbtls THis commit adds a builtin function for the dcbtls instruction. Additionaly it changes the printing of the dcbt and dcbtst instruction to embedded mode and adds support for different address variants. --- powerpc/Asm.v | 4 +++- powerpc/AsmToJSON.ml | 3 ++- powerpc/Asmexpand.ml | 59 ++++++++++++++++++++++++++++++++++++++++-------- powerpc/CBuiltins.ml | 2 ++ powerpc/Machregs.v | 2 ++ powerpc/TargetPrinter.ml | 6 +++-- 6 files changed, 63 insertions(+), 13 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asm.v b/powerpc/Asm.v index dbb819d1..43ddc1ed 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -168,7 +168,8 @@ Inductive instruction : Type := | Pdcbf: ireg -> ireg -> instruction (**r data cache flush *) | Pdcbi: ireg -> ireg -> instruction (**r data cache invalidate *) | Pdcbt: int -> ireg -> instruction (**r data cache block touch *) - | Pdcbtst: int -> ireg -> instruction (**r data cache block touch *) + | Pdcbtst: int -> ireg -> instruction (**r data cache block touch *) + | Pdcbtls: int -> ireg -> instruction (**r data cache block touch and lock set *) | Pdivw: ireg -> ireg -> ireg -> instruction (**r signed division *) | Pdivwu: ireg -> ireg -> ireg -> instruction (**r unsigned division *) | Peieio: instruction (**r EIEIO barrier *) @@ -874,6 +875,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pdcbi _ _ | Pdcbt _ _ | Pdcbtst _ _ + | Pdcbtls _ _ | Peieio | Pfctiw _ _ | Pfctiwz _ _ diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index fb73aec5..cc4f6306 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -179,6 +179,7 @@ let p_instruction oc ic = | Pdcbi (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pdcbi\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 | Pdcbt (n,ir1) -> fprintf oc "{\"Instruction Name\":\"Pdcbt\",\"Args\":[%a,%a]}" p_int n p_ireg ir1 | Pdcbtst (n,ir1) -> fprintf oc "{\"Instruction Name\":\"Pdcbtst\",\"Args\":[%a,%a]}" p_int n p_ireg ir1 + | Pdcbtls (n,ir1) -> fprintf oc "{\"Instruction Name\":\"Pdcbtls\",\"Args\":[%a,%a]}" p_int n p_ireg ir1 | Pdivw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pdivw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pdivwu (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pdivwu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Peieio -> fprintf oc "{\"Instruction Name\":\"Peieio,\"Args\":[]}" @@ -336,7 +337,7 @@ let p_fundef oc (name,f) = let alignment = atom_alignof name and inline = atom_is_inline name and static = atom_is_static name - and instr = List.filter (function Pcfi_adjust _ | Pcfi_rel_offset _ -> false | _ -> true) f.fn_code in + and instr = List.filter (function Pbuiltin _| Pcfi_adjust _ | Pcfi_rel_offset _ -> false | _ -> true) f.fn_code in let c_section,l_section,j_section = match (atom_sections name) with [a;b;c] -> a,b,c | _ -> assert false in fprintf oc "{\"Fun Name\":%a,\n\"Fun Storage Class\":%a,\n\"Fun Alignment\":%a,\n\"Fun Section Code\":%a,\"Fun Section Literals\":%a,\"Fun Section Jumptable\":%a,\n\"Fun Inline\":%B,\n\"Fun Code\":%a}\n" p_atom name p_storage static p_int_opt alignment diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 57765c50..e0357a4a 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -324,6 +324,50 @@ let expand_builtin_va_start r = let expand_int64_arith conflict rl fn = if conflict then (fn GPR0; emit (Pmr(rl, GPR0))) else fn rl +(* Handling of cache instructions *) + +(* Auxiliary function to generate address for the cache function *) +let expand_builtin_cache_common addr f = + let add = match addr with + | BA (IR a1) -> a1 + | BA_addrstack ofs -> + emit_addimm GPR11 GPR1 ofs; + GPR11 + | BA_addrglobal(id, ofs) -> + if symbol_is_small_data id ofs then begin + emit (Paddi (GPR11, GPR0, Csymbol_sda(id, ofs))); + GPR11 + end else if symbol_is_rel_data id ofs then begin + emit (Paddis(GPR11, GPR0, Csymbol_rel_high(id, ofs))); + emit (Paddi(GPR11, GPR11, Csymbol_rel_low(id, ofs))); + GPR11 + end else begin + emit (Paddis(GPR11, GPR0, Csymbol_high(id, ofs))); + emit (Paddi (GPR11, GPR11, Csymbol_low(id, ofs))); + GPR11 + end + | _ -> raise (Error "Argument is not an address") in + f add + +let expand_builtin_prefetch addr rw loc = + if not ((loc >= _0) && (loc <= _2)) then + raise (Error "the last argument of __builtin_prefetch must be a constant between 0 and 2"); + let emit_prefetch_instr addr = + if Int.eq rw _0 then begin + emit (Pdcbt (loc,addr)); + end else if Int.eq rw _1 then begin + emit (Pdcbtst (loc,addr)); + end else + raise (Error "the second argument of __builtin_prefetch must be either 0 or 1") + in + expand_builtin_cache_common addr emit_prefetch_instr + +let expand_builtin_dcbtls addr loc = + if not ((loc >= _0) && (loc <= _2)) then + raise (Error "the second argument of __builtin_dcbtls must be a constant between 0 and 2"); + let emit_inst addr = emit (Pdcbtls (loc,addr)) in + expand_builtin_cache_common addr emit_inst + (* Handling of compiler-inlined builtins *) let expand_builtin_inline name args res = @@ -428,15 +472,12 @@ let expand_builtin_inline name args res = emit (Pdcbi (GPR0,a1)) | "__builtin_icbi", [BA(IR a1)],_ -> emit (Picbi(GPR0,a1)) - | "__builtin_prefetch" , [BA (IR addr);BA_int rw; BA_int loc],_ -> - if not ((loc >= _0) && (loc < _4)) then - raise (Error "the last argument of __builtin_prefetch must be a constant between 0 and 3"); - if Int.eq rw _0 then begin - emit (Pdcbt (loc,addr)); - end else if Int.eq rw _1 then begin - emit (Pdcbtst (loc,addr)); - end else - raise (Error "the second argument of __builtin_prefetch must be either 0 or 1") + | "__builtin_dcbtls", [a; BA_int loc],_ -> + expand_builtin_dcbtls a loc + | "__builtin_dcbtls",_,_ -> + raise (Error "the second argument of __builtin_dcbtls must be a constant") + | "__builtin_prefetch" , [a1 ;BA_int rw; BA_int loc],_ -> + expand_builtin_prefetch a1 rw loc | "__builtin_prefetch" ,_,_ -> raise (Error "the second and third argument of __builtin_prefetch must be a constant") (* Special registers *) diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index 701690b2..8dbf02e5 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -96,6 +96,8 @@ let builtins = { (TVoid [],[TPtr(TVoid [], [])],false); "__builtin_prefetch", (TVoid [], [TPtr (TVoid [],[]);TInt (IInt, []);TInt (IInt,[])],false); + "__builtin_dcbtls", + (TVoid[], [TPtr (TVoid [],[]);TInt (IInt,[])],false); (* Access to special registers *) "__builtin_get_spr", (TInt(IUInt, []), [TInt(IInt, [])], false); diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index 62a4a0a5..14edb89d 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -207,6 +207,7 @@ Definition two_address_op (op: operation) : bool := Definition builtin_get_spr := ident_of_string "__builtin_get_spr". Definition builtin_set_spr := ident_of_string "__builtin_set_spr". Definition builtin_prefetch := ident_of_string "__builtin_prefetch". +Definition builtin_dcbtls := ident_of_string "__builtin_dcbtls". Definition builtin_constraints (ef: external_function) : list builtin_arg_constraint := @@ -215,6 +216,7 @@ Definition builtin_constraints (ef: external_function) : if ident_eq id builtin_get_spr then OK_const :: nil else if ident_eq id builtin_set_spr then OK_const :: OK_default :: nil else if ident_eq id builtin_prefetch then OK_addrany :: OK_const :: OK_const :: nil + else if ident_eq id builtin_dcbtls then OK_addrany::OK_const::nil else nil | EF_vload _ => OK_addrany :: nil | EF_vstore _ => OK_addrany :: OK_default :: nil diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index b0f296ef..b5fa50dc 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -463,9 +463,11 @@ module Target (System : SYSTEM):TARGET = | Pdcbi (r1,r2) -> fprintf oc " dcbi %a, %a\n" ireg r1 ireg r2 | Pdcbt (c,r1) -> - fprintf oc " dcbt %a, %a, %s\n" ireg GPR0 ireg r1 (Z.to_string c) + fprintf oc " dcbt %s, %a, %a\n" (Z.to_string c) ireg GPR0 ireg r1 | Pdcbtst (c,r1) -> - fprintf oc " dcbtst %a, %a, %s\n" ireg GPR0 ireg r1 (Z.to_string c) + fprintf oc " dcbtst %s, %a, %a\n" (Z.to_string c) ireg GPR0 ireg r1 + | Pdcbtls (c,r1) -> + fprintf oc " dcbtls %s, %a, %a\n" (Z.to_string c) ireg GPR0 ireg r1 | Pdivw(r1, r2, r3) -> fprintf oc " divw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pdivwu(r1, r2, r3) -> -- cgit From ba235b5d841528ac87b5c8cca79df3734a4a8976 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 2 Sep 2015 14:03:51 +0200 Subject: Print p_int_constant instead of p_int in AsmToJSON. --- powerpc/AsmToJSON.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'powerpc') diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index cc4f6306..ba61b734 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -177,9 +177,9 @@ let p_instruction oc ic = | Pcrxor (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcrxor\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3 | Pdcbf (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pdcbf\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 | Pdcbi (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pdcbi\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 - | Pdcbt (n,ir1) -> fprintf oc "{\"Instruction Name\":\"Pdcbt\",\"Args\":[%a,%a]}" p_int n p_ireg ir1 - | Pdcbtst (n,ir1) -> fprintf oc "{\"Instruction Name\":\"Pdcbtst\",\"Args\":[%a,%a]}" p_int n p_ireg ir1 - | Pdcbtls (n,ir1) -> fprintf oc "{\"Instruction Name\":\"Pdcbtls\",\"Args\":[%a,%a]}" p_int n p_ireg ir1 + | Pdcbt (n,ir1) -> fprintf oc "{\"Instruction Name\":\"Pdcbt\",\"Args\":[%a,%a]}" p_int_constant n p_ireg ir1 + | Pdcbtst (n,ir1) -> fprintf oc "{\"Instruction Name\":\"Pdcbtst\",\"Args\":[%a,%a]}" p_int_constant n p_ireg ir1 + | Pdcbtls (n,ir1) -> fprintf oc "{\"Instruction Name\":\"Pdcbtls\",\"Args\":[%a,%a]}" p_int_constant n p_ireg ir1 | Pdivw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pdivw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pdivwu (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pdivwu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Peieio -> fprintf oc "{\"Instruction Name\":\"Peieio,\"Args\":[]}" @@ -246,8 +246,8 @@ let p_instruction oc ic = | Pmr (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pmr\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 | Pmtctr ir -> fprintf oc "{\"Instruction Name\":\"Pmtctr\",\"Args\":[%a]}" p_ireg ir | Pmtlr ir -> fprintf oc "{\"Instruction Name\":\"Pmtlr\",\"Args\":[%a]}" p_ireg ir - | Pmfspr(ir, n) -> fprintf oc "{\"Instruction Name\":\"Pmfspr\",\"Args\":[%a,%a]}" p_ireg ir p_int n - | Pmtspr(n, ir) -> fprintf oc "{\"Instruction Name\":\"Pmtspr\",\"Args\":[%a,%a]}" p_int n p_ireg ir + | Pmfspr(ir, n) -> fprintf oc "{\"Instruction Name\":\"Pmfspr\",\"Args\":[%a,%a]}" p_ireg ir p_int_constant n + | Pmtspr(n, ir) -> fprintf oc "{\"Instruction Name\":\"Pmtspr\",\"Args\":[%a,%a]}" p_int_constant n p_ireg ir | Pmulli (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pmulli\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c | Pmullw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pmulw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pmulhw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pmulhw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 -- cgit From 30ebbcd0731f680d1d283afb99318fb9d6e9cead Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 2 Sep 2015 15:56:42 +0200 Subject: Allow only CT values of 0 and 2 in dcbtls instruction. The dcbtls instruction allows only the values 0 and 2 according to the PPC Isa. --- powerpc/Asmexpand.ml | 2 +- powerpc/TargetPrinter.ml | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index e0357a4a..caf256ef 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -363,7 +363,7 @@ let expand_builtin_prefetch addr rw loc = expand_builtin_cache_common addr emit_prefetch_instr let expand_builtin_dcbtls addr loc = - if not ((loc >= _0) && (loc <= _2)) then + if not ((loc == _0) || (loc = _2)) then raise (Error "the second argument of __builtin_dcbtls must be a constant between 0 and 2"); let emit_inst addr = emit (Pdcbtls (loc,addr)) in expand_builtin_cache_common addr emit_inst diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index b5fa50dc..764ad8a3 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -463,11 +463,11 @@ module Target (System : SYSTEM):TARGET = | Pdcbi (r1,r2) -> fprintf oc " dcbi %a, %a\n" ireg r1 ireg r2 | Pdcbt (c,r1) -> - fprintf oc " dcbt %s, %a, %a\n" (Z.to_string c) ireg GPR0 ireg r1 + fprintf oc " dcbt %ld, %a, %a\n" (camlint_of_coqint c) ireg GPR0 ireg r1 | Pdcbtst (c,r1) -> - fprintf oc " dcbtst %s, %a, %a\n" (Z.to_string c) ireg GPR0 ireg r1 + fprintf oc " dcbtst %ld, %a, %a\n" (camlint_of_coqint c) ireg GPR0 ireg r1 | Pdcbtls (c,r1) -> - fprintf oc " dcbtls %s, %a, %a\n" (Z.to_string c) ireg GPR0 ireg r1 + fprintf oc " dcbtls %ld, %a, %a\n" (camlint_of_coqint c) ireg GPR0 ireg r1 | Pdivw(r1, r2, r3) -> fprintf oc " divw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pdivwu(r1, r2, r3) -> -- cgit From cfee340dc514e2cfbc5df910f7aa687e78a54d41 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 2 Sep 2015 17:17:00 +0200 Subject: Added builtin for the icbtls instruction. This commit adds a builtin for the icbtls instruction. --- powerpc/Asm.v | 2 ++ powerpc/AsmToJSON.ml | 1 + powerpc/Asmexpand.ml | 10 ++++++++++ powerpc/CBuiltins.ml | 2 ++ powerpc/Machregs.v | 2 ++ powerpc/TargetPrinter.ml | 2 ++ 6 files changed, 19 insertions(+) (limited to 'powerpc') diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 43ddc1ed..32c7ba70 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -207,6 +207,7 @@ Inductive instruction : Type := | Pfsel: freg -> freg -> freg -> freg -> instruction (**r FP conditional move *) | Pisync: instruction (**r ISYNC barrier *) | Picbi: ireg -> ireg -> instruction (**r instruction cache invalidate *) + | Picbtls: int -> ireg -> instruction (**r instruction cache block touch and lock set *) | Plbz: ireg -> constant -> ireg -> instruction (**r load 8-bit unsigned int *) | Plbzx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) | Plfd: freg -> constant -> ireg -> instruction (**r load 64-bit float *) @@ -890,6 +891,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Plwarx _ _ _ | Plwbrx _ _ _ | Picbi _ _ + | Picbtls _ _ | Pisync | Plwsync | Plhbrx _ _ _ diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index ba61b734..8493f168 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -216,6 +216,7 @@ let p_instruction oc ic = | Pfres (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfres\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 | Pfsel (fr1,fr2,fr3,fr4) -> fprintf oc "{\"Instruction Name\":\"Pfsel\",\"Args\":[%a,%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 p_freg fr4 | Picbi (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Picbi\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 + | Picbtls (n,ir1) -> fprintf oc "{\"Instruction Name\":\"Picbtls\",\"Args\":[%a,%a]}" p_int_constant n p_ireg ir1 | Pisync -> fprintf oc "{\"Instruction Name\":\"Pisync\",\"Args\":[]}" | Plwsync -> fprintf oc "{\"Instruction Name\":\"Plwsync\",\"Args\":[]}" | Plbz (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plbz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index caf256ef..43d8fc6e 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -368,6 +368,12 @@ let expand_builtin_dcbtls addr loc = let emit_inst addr = emit (Pdcbtls (loc,addr)) in expand_builtin_cache_common addr emit_inst +let expand_builtin_icbtls addr loc = + if not ((loc == _0) || (loc = _2)) then + raise (Error "the second argument of __builtin_icbtls must be a constant between 0 and 2"); + let emit_inst addr = emit (Picbtls (loc,addr)) in + expand_builtin_cache_common addr emit_inst + (* Handling of compiler-inlined builtins *) let expand_builtin_inline name args res = @@ -476,6 +482,10 @@ let expand_builtin_inline name args res = expand_builtin_dcbtls a loc | "__builtin_dcbtls",_,_ -> raise (Error "the second argument of __builtin_dcbtls must be a constant") + | "__builtin_icbtls", [a; BA_int loc],_ -> + expand_builtin_icbtls a loc + | "__builtin_icbtls",_,_ -> + raise (Error "the second argument of __builtin_icbtls must be a constant") | "__builtin_prefetch" , [a1 ;BA_int rw; BA_int loc],_ -> expand_builtin_prefetch a1 rw loc | "__builtin_prefetch" ,_,_ -> diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index 8dbf02e5..012e4d32 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -98,6 +98,8 @@ let builtins = { (TVoid [], [TPtr (TVoid [],[]);TInt (IInt, []);TInt (IInt,[])],false); "__builtin_dcbtls", (TVoid[], [TPtr (TVoid [],[]);TInt (IInt,[])],false); + "__builtin_icbtls", + (TVoid[], [TPtr (TVoid [],[]);TInt (IInt,[])],false); (* Access to special registers *) "__builtin_get_spr", (TInt(IUInt, []), [TInt(IInt, [])], false); diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index 14edb89d..66d21021 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -208,6 +208,7 @@ Definition builtin_get_spr := ident_of_string "__builtin_get_spr". Definition builtin_set_spr := ident_of_string "__builtin_set_spr". Definition builtin_prefetch := ident_of_string "__builtin_prefetch". Definition builtin_dcbtls := ident_of_string "__builtin_dcbtls". +Definition builtin_icbtls := ident_of_string "__builtin_icbtls". Definition builtin_constraints (ef: external_function) : list builtin_arg_constraint := @@ -217,6 +218,7 @@ Definition builtin_constraints (ef: external_function) : else if ident_eq id builtin_set_spr then OK_const :: OK_default :: nil else if ident_eq id builtin_prefetch then OK_addrany :: OK_const :: OK_const :: nil else if ident_eq id builtin_dcbtls then OK_addrany::OK_const::nil + else if ident_eq id builtin_icbtls then OK_addrany::OK_const::nil else nil | EF_vload _ => OK_addrany :: nil | EF_vstore _ => OK_addrany :: OK_default :: nil diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 764ad8a3..6a583cca 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -536,6 +536,8 @@ module Target (System : SYSTEM):TARGET = fprintf oc " fsel %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 | Picbi (r1,r2) -> fprintf oc " icbi %a,%a\n" ireg r1 ireg r2 + | Picbtls (n,r1) -> + fprintf oc " icbtls %ld, %a, %a\n" (camlint_of_coqint n) ireg GPR0 ireg r1 | Pisync -> fprintf oc " isync\n" | Plwsync -> -- cgit From 38959ad2b2d35a7d1b3479ef4298a5d754350cd8 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 3 Sep 2015 11:08:25 +0200 Subject: New builtin for dcbz instruction. This commit adds a builtin for the dcbz instructions. Additionally the dcbt,dcbtst,dcbtls and icbtls instruction are changed to their actually form all taking one additional register in Asm.v. --- powerpc/Asm.v | 18 ++++++++++-------- powerpc/AsmToJSON.ml | 9 +++++---- powerpc/Asmexpand.ml | 10 ++++++---- powerpc/CBuiltins.ml | 2 ++ powerpc/TargetPrinter.ml | 18 ++++++++++-------- 5 files changed, 33 insertions(+), 24 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 32c7ba70..6444baf9 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -167,9 +167,10 @@ Inductive instruction : Type := | Pcrxor: crbit -> crbit -> crbit -> instruction (**r xor between condition bits *) | Pdcbf: ireg -> ireg -> instruction (**r data cache flush *) | Pdcbi: ireg -> ireg -> instruction (**r data cache invalidate *) - | Pdcbt: int -> ireg -> instruction (**r data cache block touch *) - | Pdcbtst: int -> ireg -> instruction (**r data cache block touch *) - | Pdcbtls: int -> ireg -> instruction (**r data cache block touch and lock set *) + | Pdcbt: int -> ireg -> ireg -> instruction (**r data cache block touch *) + | Pdcbtst: int -> ireg -> ireg -> instruction (**r data cache block touch *) + | Pdcbtls: int -> ireg -> ireg -> instruction (**r data cache block touch and lock *) + | Pdcbz: ireg -> ireg -> instruction (**r data cache block zero *) | Pdivw: ireg -> ireg -> ireg -> instruction (**r signed division *) | Pdivwu: ireg -> ireg -> ireg -> instruction (**r unsigned division *) | Peieio: instruction (**r EIEIO barrier *) @@ -207,7 +208,7 @@ Inductive instruction : Type := | Pfsel: freg -> freg -> freg -> freg -> instruction (**r FP conditional move *) | Pisync: instruction (**r ISYNC barrier *) | Picbi: ireg -> ireg -> instruction (**r instruction cache invalidate *) - | Picbtls: int -> ireg -> instruction (**r instruction cache block touch and lock set *) + | Picbtls: int -> ireg -> ireg -> instruction (**r instruction cache block touch and lock set *) | Plbz: ireg -> constant -> ireg -> instruction (**r load 8-bit unsigned int *) | Plbzx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) | Plfd: freg -> constant -> ireg -> instruction (**r load 64-bit float *) @@ -874,9 +875,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pcrxor _ _ _ | Pdcbf _ _ | Pdcbi _ _ - | Pdcbt _ _ - | Pdcbtst _ _ - | Pdcbtls _ _ + | Pdcbt _ _ _ + | Pdcbtst _ _ _ + | Pdcbtls _ _ _ + | Pdcbz _ _ | Peieio | Pfctiw _ _ | Pfctiwz _ _ @@ -891,7 +893,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Plwarx _ _ _ | Plwbrx _ _ _ | Picbi _ _ - | Picbtls _ _ + | Picbtls _ _ _ | Pisync | Plwsync | Plhbrx _ _ _ diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 8493f168..83d01dc5 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -177,9 +177,10 @@ let p_instruction oc ic = | Pcrxor (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcrxor\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3 | Pdcbf (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pdcbf\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 | Pdcbi (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pdcbi\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 - | Pdcbt (n,ir1) -> fprintf oc "{\"Instruction Name\":\"Pdcbt\",\"Args\":[%a,%a]}" p_int_constant n p_ireg ir1 - | Pdcbtst (n,ir1) -> fprintf oc "{\"Instruction Name\":\"Pdcbtst\",\"Args\":[%a,%a]}" p_int_constant n p_ireg ir1 - | Pdcbtls (n,ir1) -> fprintf oc "{\"Instruction Name\":\"Pdcbtls\",\"Args\":[%a,%a]}" p_int_constant n p_ireg ir1 + | Pdcbt (n,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pdcbt\",\"Args\":[%a,%a,%a]}" p_int_constant n p_ireg ir1 p_ireg ir2 + | Pdcbtst (n,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pdcbtst\",\"Args\":[%a,%a,%a]}" p_int_constant n p_ireg ir1 p_ireg ir2 + | Pdcbtls (n,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pdcbtls\",\"Args\":[%a,%a,%a]}" p_int_constant n p_ireg ir1 p_ireg ir2 + | Pdcbz (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pdcbz\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 | Pdivw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pdivw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pdivwu (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pdivwu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Peieio -> fprintf oc "{\"Instruction Name\":\"Peieio,\"Args\":[]}" @@ -216,7 +217,7 @@ let p_instruction oc ic = | Pfres (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfres\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 | Pfsel (fr1,fr2,fr3,fr4) -> fprintf oc "{\"Instruction Name\":\"Pfsel\",\"Args\":[%a,%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 p_freg fr4 | Picbi (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Picbi\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 - | Picbtls (n,ir1) -> fprintf oc "{\"Instruction Name\":\"Picbtls\",\"Args\":[%a,%a]}" p_int_constant n p_ireg ir1 + | Picbtls (n,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Picbtls\",\"Args\":[%a,%a,%a]}" p_int_constant n p_ireg ir1 p_ireg ir2 | Pisync -> fprintf oc "{\"Instruction Name\":\"Pisync\",\"Args\":[]}" | Plwsync -> fprintf oc "{\"Instruction Name\":\"Plwsync\",\"Args\":[]}" | Plbz (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plbz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 43d8fc6e..f266f3ec 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -354,9 +354,9 @@ let expand_builtin_prefetch addr rw loc = raise (Error "the last argument of __builtin_prefetch must be a constant between 0 and 2"); let emit_prefetch_instr addr = if Int.eq rw _0 then begin - emit (Pdcbt (loc,addr)); + emit (Pdcbt (loc,GPR0,addr)); end else if Int.eq rw _1 then begin - emit (Pdcbtst (loc,addr)); + emit (Pdcbtst (loc,GPR0,addr)); end else raise (Error "the second argument of __builtin_prefetch must be either 0 or 1") in @@ -365,13 +365,13 @@ let expand_builtin_prefetch addr rw loc = let expand_builtin_dcbtls addr loc = if not ((loc == _0) || (loc = _2)) then raise (Error "the second argument of __builtin_dcbtls must be a constant between 0 and 2"); - let emit_inst addr = emit (Pdcbtls (loc,addr)) in + let emit_inst addr = emit (Pdcbtls (loc,GPR0,addr)) in expand_builtin_cache_common addr emit_inst let expand_builtin_icbtls addr loc = if not ((loc == _0) || (loc = _2)) then raise (Error "the second argument of __builtin_icbtls must be a constant between 0 and 2"); - let emit_inst addr = emit (Picbtls (loc,addr)) in + let emit_inst addr = emit (Picbtls (loc,GPR0,addr)) in expand_builtin_cache_common addr emit_inst (* Handling of compiler-inlined builtins *) @@ -490,6 +490,8 @@ let expand_builtin_inline name args res = expand_builtin_prefetch a1 rw loc | "__builtin_prefetch" ,_,_ -> raise (Error "the second and third argument of __builtin_prefetch must be a constant") + | "__builtin_dcbz",[BA (IR a1)],_ -> + emit (Pdcbz (GPR0,a1)) (* Special registers *) | "__builtin_get_spr", [BA_int n], BR(IR res) -> emit (Pmfspr(res, n)) diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index 012e4d32..0785c7fa 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -100,6 +100,8 @@ let builtins = { (TVoid[], [TPtr (TVoid [],[]);TInt (IInt,[])],false); "__builtin_icbtls", (TVoid[], [TPtr (TVoid [],[]);TInt (IInt,[])],false); + "__builtin_dcbz", + (TVoid[], [TPtr (TVoid [],[])],false); (* Access to special registers *) "__builtin_get_spr", (TInt(IUInt, []), [TInt(IInt, [])], false); diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 6a583cca..ffd01b69 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -462,12 +462,14 @@ module Target (System : SYSTEM):TARGET = fprintf oc " dcbf %a, %a\n" ireg r1 ireg r2 | Pdcbi (r1,r2) -> fprintf oc " dcbi %a, %a\n" ireg r1 ireg r2 - | Pdcbt (c,r1) -> - fprintf oc " dcbt %ld, %a, %a\n" (camlint_of_coqint c) ireg GPR0 ireg r1 - | Pdcbtst (c,r1) -> - fprintf oc " dcbtst %ld, %a, %a\n" (camlint_of_coqint c) ireg GPR0 ireg r1 - | Pdcbtls (c,r1) -> - fprintf oc " dcbtls %ld, %a, %a\n" (camlint_of_coqint c) ireg GPR0 ireg r1 + | Pdcbt (c,r1,r2) -> + fprintf oc " dcbt %ld, %a, %a\n" (camlint_of_coqint c) ireg r1 ireg r2 + | Pdcbtst (c,r1,r2) -> + fprintf oc " dcbtst %ld, %a, %a\n" (camlint_of_coqint c) ireg r1 ireg r2 + | Pdcbtls (c,r1,r2) -> + fprintf oc " dcbtls %ld, %a, %a\n" (camlint_of_coqint c) ireg r1 ireg r2 + | Pdcbz (r1,r2) -> + fprintf oc " dcbz %a, %a\n" ireg r1 ireg r2 | Pdivw(r1, r2, r3) -> fprintf oc " divw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pdivwu(r1, r2, r3) -> @@ -536,8 +538,8 @@ module Target (System : SYSTEM):TARGET = fprintf oc " fsel %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 | Picbi (r1,r2) -> fprintf oc " icbi %a,%a\n" ireg r1 ireg r2 - | Picbtls (n,r1) -> - fprintf oc " icbtls %ld, %a, %a\n" (camlint_of_coqint n) ireg GPR0 ireg r1 + | Picbtls (n,r1,r2) -> + fprintf oc " icbtls %ld, %a, %a\n" (camlint_of_coqint n) ireg r1 ireg r2 | Pisync -> fprintf oc " isync\n" | Plwsync -> -- cgit From c74211d87eb53cb310703dec2c504b26d7f24bdf Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 3 Sep 2015 13:22:28 +0200 Subject: Added builtin for mbar instruction. This commit adds a builtin function for the mbar instruction. --- powerpc/Asm.v | 2 ++ powerpc/AsmToJSON.ml | 1 + powerpc/Asmexpand.ml | 6 ++++++ powerpc/CBuiltins.ml | 2 ++ powerpc/Machregs.v | 2 ++ powerpc/TargetPrinter.ml | 2 ++ 6 files changed, 15 insertions(+) (limited to 'powerpc') diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 6444baf9..863ed6a1 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -231,6 +231,7 @@ Inductive instruction : Type := | Plwzx_a: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) | Plwarx: ireg -> ireg -> ireg -> instruction (**r load with reservation *) | Plwbrx: ireg -> ireg -> ireg -> instruction (**r load 32-bit int and reverse endianness *) + | Pmbar: int -> instruction (**r memory barrier *) | Pmfcr: ireg -> instruction (**r move condition register to reg *) | Pmfcrbit: ireg -> crbit -> instruction (**r move condition bit to reg (pseudo) *) | Pmflr: ireg -> instruction (**r move LR to reg *) @@ -898,6 +899,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Plwsync | Plhbrx _ _ _ | Plwzu _ _ _ + | Pmbar _ | Pmfcr _ | Pmfspr _ _ | Pmtspr _ _ diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 83d01dc5..3550cd64 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -242,6 +242,7 @@ let p_instruction oc ic = | Plwzx_a (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plwzx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Plwarx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plwarx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Plwbrx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plwbrx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pmbar c -> fprintf oc "{\"Instruction Name\":\"Pmbar\",\"Args\":[%a]}" p_int_constant c | Pmfcr ir -> fprintf oc "{\"Instruction Name\":\"Pmfcr\",\"Args\":[%a]}" p_ireg ir | Pmfcrbit (ir,crb) -> assert false (* Should not occur *) | Pmflr ir -> fprintf oc "{\"Instruction Name\":\"Pmflr\",\"Args\":[%a]}" p_ireg ir diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index f266f3ec..3e57cdbf 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -466,6 +466,12 @@ let expand_builtin_inline name args res = emit (Pisync) | "__builtin_lwsync", [], _ -> emit (Plwsync) + | "__builtin_mbar", [BA_int mo], _ -> + if not (mo = _0 || mo = _1) then + raise (Error "the argument of __builtin_mbar must be either 0 or 1"); + emit (Pmbar mo) + | "__builin_mbar",_, _ -> + raise (Error "the argument of __builtin_mbar must be a constant"); | "__builtin_trap", [], _ -> emit (Ptrap) (* Vararg stuff *) diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index 0785c7fa..e18fdb2d 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -85,6 +85,8 @@ let builtins = { (TVoid [], [], false); "__builtin_lwsync", (TVoid [], [], false); + "__builtin_mbar", + (TVoid [], [TInt(IInt, [])], false); "__builtin_trap", (TVoid [], [], false); (* Cache isntructions *) diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index 66d21021..402f07d1 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -209,6 +209,7 @@ Definition builtin_set_spr := ident_of_string "__builtin_set_spr". Definition builtin_prefetch := ident_of_string "__builtin_prefetch". Definition builtin_dcbtls := ident_of_string "__builtin_dcbtls". Definition builtin_icbtls := ident_of_string "__builtin_icbtls". +Definition builtin_mbar := ident_of_string "__builtin_mbar". Definition builtin_constraints (ef: external_function) : list builtin_arg_constraint := @@ -219,6 +220,7 @@ Definition builtin_constraints (ef: external_function) : else if ident_eq id builtin_prefetch then OK_addrany :: OK_const :: OK_const :: nil else if ident_eq id builtin_dcbtls then OK_addrany::OK_const::nil else if ident_eq id builtin_icbtls then OK_addrany::OK_const::nil + else if ident_eq id builtin_mbar then OK_const::nil else nil | EF_vload _ => OK_addrany :: nil | EF_vstore _ => OK_addrany :: OK_default :: nil diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index ffd01b69..af5dafed 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -586,6 +586,8 @@ module Target (System : SYSTEM):TARGET = fprintf oc " lwzu %a, %a(%a)\n" ireg r1 constant c ireg r2 | Plwzx(r1, r2, r3) | Plwzx_a(r1, r2, r3) -> fprintf oc " lwzx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pmbar mo -> + fprintf oc " mbar %ld\n" (camlint_of_coqint mo) | Pmfcr(r1) -> fprintf oc " mfcr %a\n" ireg r1 | Pmfcrbit(r1, bit) -> -- cgit From 8dca8ab5b4ee6a73c15c44892fa59b42f8157854 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 3 Sep 2015 16:21:05 +0200 Subject: Fixed minor typo in AsmToJSON. --- powerpc/AsmToJSON.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'powerpc') diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 3550cd64..5b618c8e 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -252,7 +252,7 @@ let p_instruction oc ic = | Pmfspr(ir, n) -> fprintf oc "{\"Instruction Name\":\"Pmfspr\",\"Args\":[%a,%a]}" p_ireg ir p_int_constant n | Pmtspr(n, ir) -> fprintf oc "{\"Instruction Name\":\"Pmtspr\",\"Args\":[%a,%a]}" p_int_constant n p_ireg ir | Pmulli (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pmulli\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c - | Pmullw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pmulw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pmullw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pmullw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pmulhw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pmulhw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pmulhwu (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pmulhwu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pnand (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pnand\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 -- cgit From 296a95911bebae79f7bcc54ab9c05b1614bb8e9b Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 3 Sep 2015 16:24:47 +0200 Subject: Fixed minor typo in printing of the Plbzx instruction in AsmToJSON. --- powerpc/AsmToJSON.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'powerpc') diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 5b618c8e..2c1c65b5 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -221,7 +221,7 @@ let p_instruction oc ic = | Pisync -> fprintf oc "{\"Instruction Name\":\"Pisync\",\"Args\":[]}" | Plwsync -> fprintf oc "{\"Instruction Name\":\"Plwsync\",\"Args\":[]}" | Plbz (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plbz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 - | Plbzx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pblzx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Plbzx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plbzx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Plfd (fr,c,ir) | Plfd_a (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Plfd\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir | Plfdx (fr,ir1,ir2) -- cgit From 707741859e747221af46daa982752b61a8076647 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 3 Sep 2015 17:00:18 +0200 Subject: Added json printing of Pbctr. --- powerpc/AsmToJSON.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'powerpc') diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 2c1c65b5..c86dad4e 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -158,7 +158,7 @@ let p_instruction oc ic = | Pandi_ (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pandi_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c | Pandis_ (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pandis_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c | Pb l -> fprintf oc "{\"Instruction Name\":\"Pb\",\"Args\":[%a]}" p_label l - | Pbctr s -> assert false (* Should not occur *) + | Pbctr s -> fprintf oc "{\"Instruction Name\":\"Pbctr\",\"Args\":[]}" | Pbctrl s -> fprintf oc "{\"Instruction Name\":\"Pbctrl\",\"Args\":[]}" | Pbdnz l -> fprintf oc "{\"Instruction Name\":\"Pbdnz\",\"Args\":[%a]}" p_label l | Pbf (c,l) -> fprintf oc "{\"Instruction Name\":\"Pbf\",\"Args\":[%a,%a]}" p_crbit c p_label l -- cgit From 47d0e5256ab79b402faae14260fa2fabc1d24dcb Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 4 Sep 2015 12:51:27 +0200 Subject: Fixed typo in AsmToJSON for instruction Pstfdu. --- powerpc/AsmToJSON.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'powerpc') diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index c86dad4e..5f875ebf 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -271,7 +271,7 @@ let p_instruction oc ic = | Pstbx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstbx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pstfd (fr,c,ir) | Pstfd_a (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Pstfd\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir - | Pstfdu (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Pstdu\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir + | Pstfdu (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Pstfdu\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir | Pstfdx (fr,ir1,ir2) | Pstfdx_a (fr,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pstfdx\",\"Args\":[%a,%a,%a]}" p_freg fr p_ireg ir1 p_ireg ir2 | Pstfs (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Pstfs\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir -- cgit