diff options
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/Asm.v | 2 | ||||
| -rw-r--r-- | powerpc/Asmexpand.ml | 67 | ||||
| -rw-r--r-- | powerpc/CBuiltins.ml | 7 | ||||
| -rw-r--r-- | powerpc/Machregs.v | 9 | ||||
| -rw-r--r-- | powerpc/TargetPrinter.ml | 2 |
5 files changed, 80 insertions, 7 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 3c7bdd15..66bb4607 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -153,6 +153,7 @@ Inductive instruction : Type := | Pbdnz: label -> instruction (**r decrement CTR and branch if not zero *) | Pbf: crbit -> label -> instruction (**r branch if false *) | Pbl: ident -> signature -> instruction (**r branch and link *) + | Pbne: label -> instruction (**r branch not equal *) | Pbs: ident -> signature -> instruction (**r branch to symbol *) | Pblr: instruction (**r branch to contents of register LR *) | Pbt: crbit -> label -> instruction (**r branch if true *) @@ -873,6 +874,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out (** The following instructions and directives are not generated directly by [Asmgen], so we do not model them. *) | Pbdnz _ + | Pbne _ | Pcmpb _ _ _ | Pcntlzw _ _ | Pcreqv _ _ _ diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 3fffc037..beaef42f 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -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 @@ -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 @@ -485,8 +485,65 @@ 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 (GPR11,GPR0,a1)); + emit (Pstwcx_ (GPR10,GPR0,a1)); + emit (Pbne lbl); + emit (Pisync); + emit (Pstw (GPR11,Cint _0,a3)) + | "__builtin_atomic_load", [BA (IR a1); BA (IR a2)],_ -> + let lbl = new_label() in + emit (Psync); + emit (Plabel lbl); + emit (Plwz (a1,Cint _0,a1)); + emit (Pcmpw (a1,a1)); + emit (Pbne lbl); + emit (Pisync); + emit (Pstw (a1,Cint _0, a2)); + | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR (IR res) -> + let tmpres = if a1 = res then + GPR11 + else + res in + let lbl = new_label() in + emit (Psync); + emit (Plabel lbl); + emit (Plwarx (tmpres,GPR0,a1)); + emit (Padd (a2,tmpres,a2)); + emit (Pstwcx_ (a2,GPR0,a1)); + emit (Pbne lbl); + emit (Pisync); + if (tmpres <> res) then + emit (Pmr (res,tmpres)) + | "__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,exp)); + emit (Psync); + emit (Plabel lbls); + emit (Plwarx (GPR12,GPR0,dst)); + emit (Pcmpw (GPR12,GPR10)); + emit (Pbne lblneq); + emit (Pstwcx_ (GPR11,GPR0,dst)); + emit (Pbne lbls); + emit (Plabel lblneq); + emit (Pisync); + emit (Pmfcr dst); + emit (Prlwinm (dst,dst,(Z.of_uint 3),_1)); + emit (Pcmpwi (dst,(Cint _0))); + emit (Pbne lblsucc); + emit (Pstw (GPR12,(Cint _0),exp)); + emit (Plabel lblsucc); + emit (Pmr (res,dst)); (* Catch-all *) | _ -> raise (Error ("unrecognized builtin " ^ name)) @@ -517,7 +574,7 @@ let expand_instruction 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..b61028d3 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -118,7 +118,12 @@ 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) ] } diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index a2017dca..4391d5a8 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -160,9 +160,15 @@ 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_and_fetch". + 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::R11::F13:: nil + else if ident_eq id builtin_sync_and_fetch then R11::F13::nil + else F13 :: nil | EF_vload _ => R11 :: nil | EF_vstore Mint64 => R10 :: R11 :: R12 :: nil | EF_vstore _ => R11 :: R12 :: nil @@ -183,6 +189,7 @@ 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). diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index eca7a1b8..f5295777 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -414,6 +414,8 @@ module Target (System : SYSTEM):TARGET = end | Pbl(s, sg) -> fprintf oc " bl %a\n" symbol s + | Pbne lbl -> + fprintf oc " bne- %a\n" label (transl_label lbl) | Pbs(s, sg) -> fprintf oc " b %a\n" symbol s | Pblr -> |