diff options
Diffstat (limited to 'ia32')
-rw-r--r-- | ia32/Asm.v | 2 | ||||
-rw-r--r-- | ia32/Asmexpand.ml | 22 | ||||
-rw-r--r-- | ia32/SelectOp.vp | 2 | ||||
-rw-r--r-- | ia32/TargetPrinter.ml | 17 |
4 files changed, 18 insertions, 25 deletions
@@ -293,7 +293,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/ia32/Asmexpand.ml b/ia32/Asmexpand.ml index 8996794b..a2a7a9be 100644 --- a/ia32/Asmexpand.ml +++ b/ia32/Asmexpand.ml @@ -140,7 +140,7 @@ let expand_builtin_vload_common chunk addr res = emit (Pmovsw_rm (res,addr)) | Mint32, BR(IR res) -> emit (Pmov_rm (res,addr)) - | Mint64, BR_longofwords(BR(IR res1), BR(IR res2)) -> + | Mint64, BR_splitlong(BR(IR res1), BR(IR res2)) -> let addr' = offset_addressing addr _4 in if not (Asmgen.addressing_mentions addr res2) then begin emit (Pmov_rm (res2,addr)); @@ -176,7 +176,7 @@ let expand_builtin_vstore_common chunk addr src tmp = emit (Pmovw_mr (addr,src)) | Mint32, BA(IR src) -> emit (Pmov_mr (addr,src)) - | Mint64, BA_longofwords(BA(IR src1), BA(IR src2)) -> + | Mint64, BA_splitlong(BA(IR src1), BA(IR src2)) -> let addr' = offset_addressing addr _4 in emit (Pmov_mr (addr,src2)); emit (Pmov_mr (addr',src1)) @@ -293,26 +293,26 @@ let expand_builtin_inline name args res = (fun r1 r2 r3 -> Pfnmsub213(r1, r2, r3)) (fun r1 r2 r3 -> Pfnmsub231(r1, r2, r3)) (* 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)) -> assert (ah = EDX && al = EAX && rh = EDX && rl = EAX); emit (Pneg EAX); emit (Padc_ri (EDX,_0)); emit (Pneg EDX) - | "__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)) -> assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX); emit (Padd_rr (EAX,EBX)); emit (Padc_rr (EDX,ECX)) - | "__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)) -> assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX); emit (Psub_rr (EAX,EBX)); emit (Psbb_rr (EDX,ECX)) | "__builtin_mull", [BA(IR a); BA(IR b)], - BR_longofwords(BR(IR rh), BR(IR rl)) -> + BR_splitlong(BR(IR rh), BR(IR rl)) -> assert (a = EAX && b = EDX && rh = EDX && rl = EAX); emit (Pmul_r EDX) (* Memory accesses *) diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp index 744902ec..bc331b9c 100644 --- a/ia32/SelectOp.vp +++ b/ia32/SelectOp.vp @@ -516,7 +516,7 @@ Nondetfunction builtin_arg (e: expr) := | Eop (Olea (Ainstack 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/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index beddd1e8..9e4babb7 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -337,17 +337,6 @@ module Target(System: SYSTEM):TARGET = - inlined by the compiler: take their arguments in arbitrary registers; preserve all registers except ECX, EDX, XMM6 and XMM7. *) -(* 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 "%esp" oc txt targs args - end - (* Handling of varargs *) let print_builtin_va_start oc r = @@ -658,7 +647,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 "%esp" oc (extern_atom txt) args + | EF_debug(kind, txt, targs) -> + print_debug_info comment print_file_line preg "%esp" 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; |