diff options
-rw-r--r-- | powerpc/Asmexpand.ml | 75 | ||||
-rw-r--r-- | powerpc/CBuiltins.ml | 11 | ||||
-rw-r--r-- | powerpc/Machregs.v | 19 |
3 files changed, 90 insertions, 15 deletions
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 050380ae..5a365123 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -41,7 +41,7 @@ let emit_addimm rd rs n = List.iter emit (Asmgen.addimm rd rs n []) - + (* Handling of annotations *) let expand_annot_val txt targ args res = @@ -64,7 +64,7 @@ let expand_annot_val txt targ args res = Note that lfd and stfd cannot trap on ill-formed floats. *) let offset_in_range ofs = - Int.eq (Asmgen.high_s ofs) Int.zero + Int.eq (Asmgen.high_s ofs) _0 let memcpy_small_arg sz arg tmp = match arg with @@ -79,7 +79,7 @@ let memcpy_small_arg sz arg tmp = assert false let expand_builtin_memcpy_small sz al src dst = - let (tsrc, tdst) = + 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 @@ -117,7 +117,7 @@ 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) = + 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; @@ -185,7 +185,7 @@ let rec expand_builtin_vload_common chunk base offset res = emit (Plwz(lo, offset', base)); emit (Plwz(hi, offset, base)) end - | None -> + | None -> emit (Paddi(GPR11, base, offset)); expand_builtin_vload_common chunk GPR11 (Cint _0) res end @@ -239,7 +239,7 @@ let expand_builtin_vstore_common chunk base offset src = | Some offset' -> emit (Pstw(hi, offset, base)); emit (Pstw(lo, offset', base)) - | None -> + | None -> let tmp = temp_for_vstore src in emit (Paddi(tmp, base, offset)); emit (Pstw(hi, Cint _0, tmp)); @@ -276,9 +276,9 @@ let expand_builtin_vstore chunk args = assert false (* Handling of varargs *) -let linkregister_offset = ref Int.zero +let linkregister_offset = ref _0 -let retaddr_offset = ref Int.zero +let retaddr_offset = ref _0 let current_function_stacksize = ref 0l @@ -442,7 +442,7 @@ let expand_builtin_inline name args res = | "__builtin_dcbtls", [BA (IR a1); BA_int loc],_ -> if not ((Int.eq loc _0) || (Int.eq loc _2)) then raise (Error "the second argument of __builtin_dcbtls must be 0 or 2"); - emit (Pdcbtls (loc,GPR0,a1)) + emit (Pdcbtls (loc,GPR0,a1)) | "__builtin_dcbtls",_,_ -> raise (Error "the second argument of __builtin_dcbtls must be a constant") | "__builtin_icbtls", [BA (IR a1); BA_int loc],_ -> @@ -475,7 +475,7 @@ let expand_builtin_inline name args res = raise (Error "the first argument of __builtin_set_spr must be a constant") (* Frame and return address *) | "__builtin_call_frame", _,BR (IR res) -> - let sz = !current_function_stacksize + let sz = !current_function_stacksize and ofs = !linkregister_offset in if sz < 0x8000l then emit (Paddi(res, GPR1, Cint(coqint_of_camlint sz))) @@ -485,8 +485,59 @@ let expand_builtin_inline name args res = emit (Plwz (res, Cint! retaddr_offset,GPR1)) (* isel *) | "__builtin_isel", [BA (IR a1); BA (IR a2); BA (IR a3)],BR (IR res) -> - emit (Pcmpwi (a1,Cint (Int.zero))); + emit (Pcmpwi (a1,Cint (_0))); emit (Pisel (res,a3,a2,CRbit_2)) + (* atomic operations *) + | "__builtin_atomic_exchange", [BA (IR a1); BA (IR a2); BA (IR a3)],_ -> + emit (Plwz (GPR10,Cint _0,a2)); + emit (Psync); + let lbl = new_label() in + emit (Plabel lbl); + emit (Plwarx (GPR0,GPR0,a1)); + emit (Pstwcx_ (GPR10,GPR0,a1)); + emit (Pbf (CRbit_2,lbl)); + emit (Pisync); + emit (Pstw (GPR0,Cint _0,a3)) + | "__builtin_atomic_load", [BA (IR a1); BA (IR a2)],_ -> + let lbl = new_label () in + emit (Psync); + emit (Plwz (GPR0,Cint _0,a1)); + emit (Pcmpw (GPR0,GPR0)); + emit (Pbf (CRbit_2,lbl)); + emit (Plabel lbl); + emit (Pisync); + emit (Pstw (GPR0,Cint _0, a2)) + | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR (IR res) -> + let lbl = new_label() in + emit (Psync); + emit (Plabel lbl); + emit (Plwarx (res,GPR0,a1)); + emit (Padd (GPR0,res,a2)); + emit (Pstwcx_ (GPR0,GPR0,a1)); + emit (Pbf (CRbit_2, lbl)); + emit (Pisync); + | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)], BR (IR res) -> + let lbls = new_label () + and lblneq = new_label () + and lblsucc = new_label () in + emit (Plwz (GPR10,Cint _0,exp)); + emit (Plwz (GPR11,Cint _0,des)); + emit (Psync); + emit (Plabel lbls); + emit (Plwarx (GPR0,GPR0,dst)); + emit (Pcmpw (GPR0,GPR10)); + emit (Pbf (CRbit_2,lblneq)); + emit (Pstwcx_ (GPR11,GPR0,dst)); + emit (Pbf (CRbit_2,lbls)); + emit (Plabel lblneq); + (* Here, CR2 is true if the exchange succeeded, false if it failed *) + emit (Pisync); + emit (Pmfcr GPR10); + emit (Prlwinm (res,GPR10,(Z.of_uint 3),_1)); + (* Update exp with the current value of dst if the exchange failed *) + emit (Pbt (CRbit_2,lblsucc)); + emit (Pstw (GPR0,Cint _0,exp)); + emit (Plabel lblsucc) (* Catch-all *) | _ -> raise (Error ("unrecognized builtin " ^ name)) @@ -517,7 +568,7 @@ let expand_instruction_simple instr = | Pallocframe(sz, ofs,retofs) -> let variadic = (!current_function).fn_sig.sig_cc.cc_vararg in let sz = camlint_of_coqint sz in - assert (ofs = Int.zero); + assert (ofs = _0); let sz = if variadic then Int32.add sz 96l else sz in let adj = Int32.neg sz in if adj >= -0x8000l then diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index 1bb8c6f7..a9e4f5e3 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -118,7 +118,16 @@ let builtins = { (TPtr (TVoid [],[]),[],false); (* isel *) "__builtin_isel", - (TInt (IInt, []),[TInt(IBool, []);TInt(IInt, []);TInt(IInt, [])],false) + (TInt (IInt, []),[TInt(IBool, []);TInt(IInt, []);TInt(IInt, [])],false); + (* atomic operations *) + "__builtin_atomic_exchange", + (TVoid [], [TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[])],false); + "__builtin_atomic_load", + (TVoid [], [TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[])],false); + "__builtin_atomic_compare_exchange", + (TInt (IBool, []), [TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[])],false); + "__builtin_sync_fetch_and_add", + (TInt (IInt, []), [TPtr (TInt(IInt, []),[]);TInt(IInt, [])],false); ] } diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index a2017dca..f94c3b64 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -160,9 +160,16 @@ Fixpoint destroyed_by_clobber (cl: list string): list mreg := end end. +Definition builtin_atomic_exchange := ident_of_string "__builtin_atomic_exchange". +Definition builtin_sync_and_fetch := ident_of_string "__builtin_sync_fetch_and_add". +Definition builtin_atomic_compare_exchange := ident_of_string "__builtin_atomic_compare_exchange". + Definition destroyed_by_builtin (ef: external_function): list mreg := match ef with - | EF_builtin _ _ => F13 :: nil + | EF_builtin id sg => + if ident_eq id builtin_atomic_exchange then R10::nil + else if ident_eq id builtin_atomic_compare_exchange then R10::R11::nil + else F13 :: nil | EF_vload _ => R11 :: nil | EF_vstore Mint64 => R10 :: R11 :: R12 :: nil | EF_vstore _ => R11 :: R12 :: nil @@ -183,8 +190,16 @@ Definition temp_for_parent_frame: mreg := Definition mregs_for_operation (op: operation): list (option mreg) * option mreg := (nil, None). + Definition mregs_for_builtin (ef: external_function): list (option mreg) * list (option mreg) := - (nil, nil). + match ef with + | EF_builtin id sg => + if ident_eq id builtin_atomic_exchange then ((Some R3)::(Some R4)::(Some R5)::nil,nil) + else if ident_eq id builtin_sync_and_fetch then ((Some R4)::(Some R5)::nil,(Some R3)::nil) + else if ident_eq id builtin_atomic_compare_exchange then ((Some R4)::(Some R5)::(Some R6)::nil, (Some R3):: nil) + else (nil, nil) + | _ => (nil, nil) + end. Global Opaque destroyed_by_op destroyed_by_load destroyed_by_store |