diff options
Diffstat (limited to 'powerpc/Asmexpand.ml')
-rw-r--r-- | powerpc/Asmexpand.ml | 452 |
1 files changed, 277 insertions, 175 deletions
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index ae4d694a..3e57cdbf 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 *) @@ -44,14 +45,14 @@ 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 + raise (Error "ill-formed __builtin_annot_val") end (* Handling of memcpy *) @@ -62,34 +63,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 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 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 + | _ -> + assert false + let expand_builtin_memcpy_small sz al src dst = - let rec copy ofs sz = + 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 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 +140,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 +149,131 @@ 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 offset_in_range n' 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 *) - | _ -> + | Mint64, BR_splitlong(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 offset_in_range ofs 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 *) - | _ -> + | Mint64, BA_splitlong(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 offset_in_range ofs 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 *) @@ -302,49 +324,99 @@ 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,GPR0,addr)); + end else if Int.eq rw _1 then begin + emit (Pdcbtst (loc,GPR0,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,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,GPR0,addr)) in + expand_builtin_cache_common addr emit_inst + (* Handling of compiler-inlined builtins *) 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 +424,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_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", [IR ah; IR al; IR bh; IR bl], [IR rh; 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", [IR ah; IR al; IR bh; IR bl], [IR rh; 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", [IR a; IR b], [IR rh; IR rl] -> + | "__builtin_mull", [BA(IR a); BA(IR b)], + 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))) (* 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", [], _ -> @@ -388,20 +466,50 @@ 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 *) - | "__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)) + | "__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_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" ,_,_ -> + 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)) + | "__builtin_get_spr", _, _ -> + 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", _, _ -> + 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. @@ -484,25 +592,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 @@ -511,13 +605,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 |