diff options
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/Asm.v | 10 | ||||
| -rw-r--r-- | powerpc/AsmToJSON.ml | 6 | ||||
| -rw-r--r-- | powerpc/Asmexpand.ml | 100 | ||||
| -rw-r--r-- | powerpc/Asmgen.v | 2 | ||||
| -rw-r--r-- | powerpc/CBuiltins.ml | 12 | ||||
| -rw-r--r-- | powerpc/Machregs.v | 6 | ||||
| -rw-r--r-- | powerpc/TargetPrinter.ml | 6 |
7 files changed, 72 insertions, 70 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 863ed6a1..3c7bdd15 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -142,7 +142,7 @@ Inductive instruction : Type := | Paddic: ireg -> ireg -> constant -> instruction (**r add immediate and set carry *) | Paddis: ireg -> ireg -> constant -> instruction (**r add immediate high *) | Paddze: ireg -> ireg -> instruction (**r add carry *) - | Pallocframe: Z -> int -> instruction (**r allocate new stack frame (pseudo) *) + | Pallocframe: Z -> int -> int -> instruction (**r allocate new stack frame (pseudo) *) | Pand_: ireg -> ireg -> ireg -> instruction (**r bitwise and *) | Pandc: ireg -> ireg -> ireg -> instruction (**r bitwise and-complement *) | Pandi_: ireg -> ireg -> constant -> instruction (**r and immediate and set conditions *) @@ -157,6 +157,7 @@ Inductive instruction : Type := | Pblr: instruction (**r branch to contents of register LR *) | Pbt: crbit -> label -> instruction (**r branch if true *) | Pbtbl: ireg -> list label -> instruction (**r N-way branch through a jump table (pseudo) *) + | Pcmpb: ireg -> ireg -> ireg -> instruction (**r compare bytes *) | Pcmplw: ireg -> ireg -> instruction (**r unsigned integer comparison *) | Pcmplwi: ireg -> constant -> instruction (**r same, with immediate argument *) | Pcmpw: ireg -> ireg -> instruction (**r signed integer comparison *) @@ -206,6 +207,7 @@ Inductive instruction : Type := | Pfrsqrte: freg -> freg -> instruction (**r approximate reciprocal of square root *) | Pfres: freg -> freg -> instruction (**r approximate inverse *) | Pfsel: freg -> freg -> freg -> freg -> instruction (**r FP conditional move *) + | Pisel: ireg -> ireg -> ireg -> crbit -> instruction (**r integer select *) | Pisync: instruction (**r ISYNC barrier *) | Picbi: ireg -> ireg -> instruction (**r instruction cache invalidate *) | Picbtls: int -> ireg -> ireg -> instruction (**r instruction cache block touch and lock set *) @@ -323,7 +325,7 @@ lbl: .double floatcst lfd rdst, 0(r1) addi r1, r1, 8 >> -- [Pallocframe sz ofs]: in the formal semantics, this pseudo-instruction +- [Pallocframe sz ofs retofs]: in the formal semantics, this pseudo-instruction allocates a memory block with bounds [0] and [sz], stores the value of register [r1] (the stack pointer, by convention) at offset [ofs] in this block, and sets [r1] to a pointer to the bottom of this @@ -622,7 +624,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Paddze rd r1 => Next (nextinstr (rs#rd <- (Val.add rs#r1 rs#CARRY) #CARRY <- (Val.add_carry rs#r1 Vzero rs#CARRY))) m - | Pallocframe sz ofs => + | Pallocframe sz ofs _ => let (m1, stk) := Mem.alloc m 0 sz in let sp := Vptr stk Int.zero in match Mem.storev Mint32 m1 (Val.add sp (Vint ofs)) rs#GPR1 with @@ -871,6 +873,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 _ + | Pcmpb _ _ _ | Pcntlzw _ _ | Pcreqv _ _ _ | Pcrxor _ _ _ @@ -891,6 +894,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pfrsqrte _ _ | Pfres _ _ | Pfsel _ _ _ _ + | Pisel _ _ _ _ | Plwarx _ _ _ | Plwbrx _ _ _ | Picbi _ _ diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 5f875ebf..a7e66701 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -152,7 +152,7 @@ let p_instruction oc ic = | Paddic (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Paddic\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c | Paddis (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Paddis\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c | Paddze (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Paddze\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 - | Pallocframe (c,i) -> assert false(* Should not occur *) + | Pallocframe (c,i,r) -> assert false(* Should not occur *) | Pand_ (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pand_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pandc (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pandc\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pandi_ (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pandi_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c @@ -167,6 +167,7 @@ let p_instruction oc ic = | Pblr -> fprintf oc "{\"Instruction Name\":\"Pblr\",\"Args\":[]}" | Pbt (cr,l) -> fprintf oc "{\"Instruction Name\":\"Pbt\",\"Args\":[%a,%a]}" p_crbit cr p_label l | Pbtbl (i,lb) -> fprintf oc "{\"Instruction Name\":\"Pbtl\",\"Args\":[%a%a]}" p_ireg i (p_list_cont p_label) lb + | Pcmpb (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pcmpb\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pcmplw (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pcmplw\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 | Pcmplwi (ir,c) -> fprintf oc "{\"Instruction Name\":\"Pcmplwi\",\"Args\":[%a,%a]}" p_ireg ir p_constant c | Pcmpw (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pcmpw\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 @@ -216,6 +217,7 @@ let p_instruction oc ic = | Pfrsqrte (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfsqrte\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 | 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 + | Pisel (ir1,ir2,ir3,cr) -> fprintf oc "{\"Instruction Name\":\"Pisel\",\"Args\":[%a,%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 p_crbit cr | Picbi (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Picbi\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 | 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\":[]}" @@ -286,7 +288,7 @@ let p_instruction oc ic = | Pstwx_a (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pstwux (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwux\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pstwbrx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwbrx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 - | Pstwcx_ (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwc_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pstwcx_ (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwcx_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Psubfc (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Psubfc\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Psubfe (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Psubfe\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Psubfze (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Psubfe\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 3e57cdbf..b9fe1d7f 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -276,6 +276,9 @@ let expand_builtin_vstore chunk args = assert false (* Handling of varargs *) +let linkregister_offset = ref Int.zero + +let retaddr_offset = ref Int.zero let current_function_stacksize = ref 0l @@ -324,56 +327,6 @@ 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 = @@ -386,6 +339,8 @@ let expand_builtin_inline name args res = emit (Pmulhwu(res, a1, a2)) | "__builtin_clz", [BA(IR a1)], BR(IR res) -> emit (Pcntlzw(res, a1)) + | "__builtin_cmpb", [BA(IR a1); BA(IR a2)], BR(IR res) -> + emit (Pcmpb (res,a1,a2)) | ("__builtin_bswap" | "__builtin_bswap32"), [BA(IR a1)], BR(IR res) -> emit (Pstwu(a1, Cint _m8, GPR1)); emit (Pcfi_adjust _8); @@ -468,7 +423,7 @@ let expand_builtin_inline name args res = 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"); + raise (Error "the argument of __builtin_mbar must be 0 or 1"); emit (Pmbar mo) | "__builin_mbar",_, _ -> raise (Error "the argument of __builtin_mbar must be a constant"); @@ -484,16 +439,27 @@ let expand_builtin_inline name args res = emit (Pdcbi (GPR0,a1)) | "__builtin_icbi", [BA(IR a1)],_ -> emit (Picbi(GPR0,a1)) - | "__builtin_dcbtls", [a; BA_int loc],_ -> - expand_builtin_dcbtls a loc + | "__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)) | "__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", [BA (IR a1); BA_int loc],_ -> + if not ((Int.eq loc _0) || (Int.eq loc _2)) then + raise (Error "the second argument of __builtin_icbtls must be 0 or 2"); + emit (Picbtls (loc,GPR0,a1)) | "__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" , [BA (IR a1) ;BA_int rw; BA_int loc],_ -> + if not (Int.ltu loc _4) then + raise (Error "the last argument of __builtin_prefetch must be 0, 1 or 2"); + if Int.eq rw _0 then begin + emit (Pdcbt (loc,GPR0,a1)); + end else if Int.eq rw _1 then begin + emit (Pdcbtst (loc,GPR0,a1)); + end else + raise (Error "the second argument of __builtin_prefetch must be 0 or 1") | "__builtin_prefetch" ,_,_ -> raise (Error "the second and third argument of __builtin_prefetch must be a constant") | "__builtin_dcbz",[BA (IR a1)],_ -> @@ -507,6 +473,20 @@ let expand_builtin_inline name args res = emit (Pmtspr(n, a1)) | "__builtin_set_spr", _, _ -> 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 + and ofs = !linkregister_offset in + if sz < 0x8000l then + emit (Paddi(res, GPR1, Cint(coqint_of_camlint sz))) + else + emit (Plwz(res, Cint ofs, GPR1)) + | "__builtin_return_address",_,BR (IR 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 (Pisel (res,a3,a2,CRbit_2)) (* Catch-all *) | _ -> raise (Error ("unrecognized builtin " ^ name)) @@ -534,7 +514,7 @@ let num_crbit = function let expand_instruction instr = match instr with - | Pallocframe(sz, ofs) -> + | 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); @@ -553,7 +533,9 @@ let expand_instruction instr = {sig_args = []; sig_res = None; sig_cc = cc_default})); emit (Pmtlr GPR0) end; - current_function_stacksize := sz + current_function_stacksize := sz; + linkregister_offset := ofs; + retaddr_offset := retofs | Pbctr sg | Pbctrl sg | Pbl(_, sg) | Pbs(_, sg) -> set_cr6 sg; emit instr diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 541fe7c6..db3b7028 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -711,7 +711,7 @@ Definition transl_code' (f: Mach.function) (il: list Mach.instruction) (it1p: bo Definition transl_function (f: Mach.function) := do c <- transl_code' f f.(Mach.fn_code) false; OK (mkfunction f.(Mach.fn_sig) - (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) :: + (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) f.(fn_retaddr_ofs) :: Pmflr GPR0 :: Pstw GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: Pcfi_rel_offset f.(fn_retaddr_ofs) :: c)). diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index e18fdb2d..1bb8c6f7 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -36,6 +36,8 @@ let builtins = { (TInt(IUInt, []), [TInt(IUInt, [])], false); "__builtin_bswap16", (TInt(IUShort, []), [TInt(IUShort, [])], false); + "__builtin_cmpb", + (TInt (IUInt, []), [TInt(IUInt, []);TInt(IUInt, [])], false); (* Float arithmetic *) "__builtin_fmadd", (TFloat(FDouble, []), @@ -108,7 +110,15 @@ let builtins = { "__builtin_get_spr", (TInt(IUInt, []), [TInt(IInt, [])], false); "__builtin_set_spr", - (TVoid [], [TInt(IInt, []); TInt(IUInt, [])], false) + (TVoid [], [TInt(IInt, []); TInt(IUInt, [])], false); + (* Frame and return address *) + "__builtin_call_frame", + (TPtr (TVoid [],[]),[],false); + "__builtin_return_address", + (TPtr (TVoid [],[]),[],false); + (* isel *) + "__builtin_isel", + (TInt (IInt, []),[TInt(IBool, []);TInt(IInt, []);TInt(IInt, [])],false) ] } diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index 402f07d1..a2017dca 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -217,9 +217,9 @@ 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 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_prefetch then OK_default :: OK_const :: OK_const :: nil + else if ident_eq id builtin_dcbtls then OK_default::OK_const::nil + else if ident_eq id builtin_icbtls then OK_default::OK_const::nil else if ident_eq id builtin_mbar then OK_const::nil else nil | EF_vload _ => OK_addrany :: nil diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index c126f641..58117ee7 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -384,7 +384,7 @@ module Target (System : SYSTEM):TARGET = fprintf oc " addis %a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c | Paddze(r1, r2) -> fprintf oc " addze %a, %a\n" ireg r1 ireg r2 - | Pallocframe(sz, ofs) -> + | Pallocframe(sz, ofs, _) -> assert false | Pand_(r1, r2, r3) -> fprintf oc " and. %a, %a, %a\n" ireg r1 ireg r2 ireg r3 @@ -443,6 +443,8 @@ module Target (System : SYSTEM):TARGET = fprintf oc " bctr\n"; jumptables := (lbl, tbl) :: !jumptables; fprintf oc "%s end pseudoinstr btbl\n" comment + | Pcmpb (r1, r2, r3) -> + fprintf oc " cmpb %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pcmplw(r1, r2) -> fprintf oc " cmplw %a, %a, %a\n" creg 0 ireg r1 ireg r2 | Pcmplwi(r1, c) -> @@ -537,6 +539,8 @@ module Target (System : SYSTEM):TARGET = fprintf oc " fres %a, %a\n" freg r1 freg r2 | Pfsel(r1, r2, r3, r4) -> fprintf oc " fsel %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 + | Pisel (r1,r2,r3,cr) -> + fprintf oc " isel %a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 crbit cr | Picbi (r1,r2) -> fprintf oc " icbi %a,%a\n" ireg r1 ireg r2 | Picbtls (n,r1,r2) -> |