diff options
| -rw-r--r-- | powerpc/Asm.v | 4 | ||||
| -rw-r--r-- | powerpc/AsmToJSON.ml | 3 | ||||
| -rw-r--r-- | powerpc/Asmexpand.ml | 59 | ||||
| -rw-r--r-- | powerpc/CBuiltins.ml | 2 | ||||
| -rw-r--r-- | powerpc/Machregs.v | 2 | ||||
| -rw-r--r-- | powerpc/TargetPrinter.ml | 6 |
6 files changed, 63 insertions, 13 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index dbb819d1..43ddc1ed 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -168,7 +168,8 @@ Inductive instruction : Type := | Pdcbf: ireg -> ireg -> instruction (**r data cache flush *) | Pdcbi: ireg -> ireg -> instruction (**r data cache invalidate *) | Pdcbt: int -> ireg -> instruction (**r data cache block touch *) - | Pdcbtst: int -> ireg -> instruction (**r data cache block touch *) + | Pdcbtst: int -> ireg -> instruction (**r data cache block touch *) + | Pdcbtls: int -> ireg -> instruction (**r data cache block touch and lock set *) | Pdivw: ireg -> ireg -> ireg -> instruction (**r signed division *) | Pdivwu: ireg -> ireg -> ireg -> instruction (**r unsigned division *) | Peieio: instruction (**r EIEIO barrier *) @@ -874,6 +875,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pdcbi _ _ | Pdcbt _ _ | Pdcbtst _ _ + | Pdcbtls _ _ | Peieio | Pfctiw _ _ | Pfctiwz _ _ diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index fb73aec5..cc4f6306 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -179,6 +179,7 @@ let p_instruction oc ic = | Pdcbi (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pdcbi\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 | Pdcbt (n,ir1) -> fprintf oc "{\"Instruction Name\":\"Pdcbt\",\"Args\":[%a,%a]}" p_int n p_ireg ir1 | Pdcbtst (n,ir1) -> fprintf oc "{\"Instruction Name\":\"Pdcbtst\",\"Args\":[%a,%a]}" p_int n p_ireg ir1 + | Pdcbtls (n,ir1) -> fprintf oc "{\"Instruction Name\":\"Pdcbtls\",\"Args\":[%a,%a]}" p_int n p_ireg ir1 | Pdivw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pdivw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pdivwu (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pdivwu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Peieio -> fprintf oc "{\"Instruction Name\":\"Peieio,\"Args\":[]}" @@ -336,7 +337,7 @@ let p_fundef oc (name,f) = let alignment = atom_alignof name and inline = atom_is_inline name and static = atom_is_static name - and instr = List.filter (function Pcfi_adjust _ | Pcfi_rel_offset _ -> false | _ -> true) f.fn_code in + and instr = List.filter (function Pbuiltin _| Pcfi_adjust _ | Pcfi_rel_offset _ -> false | _ -> true) f.fn_code in let c_section,l_section,j_section = match (atom_sections name) with [a;b;c] -> a,b,c | _ -> assert false in fprintf oc "{\"Fun Name\":%a,\n\"Fun Storage Class\":%a,\n\"Fun Alignment\":%a,\n\"Fun Section Code\":%a,\"Fun Section Literals\":%a,\"Fun Section Jumptable\":%a,\n\"Fun Inline\":%B,\n\"Fun Code\":%a}\n" p_atom name p_storage static p_int_opt alignment diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 57765c50..e0357a4a 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -324,6 +324,50 @@ 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,addr)); + end else if Int.eq rw _1 then begin + emit (Pdcbtst (loc,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,addr)) in + expand_builtin_cache_common addr emit_inst + (* Handling of compiler-inlined builtins *) let expand_builtin_inline name args res = @@ -428,15 +472,12 @@ let expand_builtin_inline name args res = emit (Pdcbi (GPR0,a1)) | "__builtin_icbi", [BA(IR a1)],_ -> emit (Picbi(GPR0,a1)) - | "__builtin_prefetch" , [BA (IR addr);BA_int rw; BA_int loc],_ -> - if not ((loc >= _0) && (loc < _4)) then - raise (Error "the last argument of __builtin_prefetch must be a constant between 0 and 3"); - if Int.eq rw _0 then begin - emit (Pdcbt (loc,addr)); - end else if Int.eq rw _1 then begin - emit (Pdcbtst (loc,addr)); - end else - raise (Error "the second argument of __builtin_prefetch must be either 0 or 1") + | "__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_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") (* Special registers *) diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index 701690b2..8dbf02e5 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -96,6 +96,8 @@ let builtins = { (TVoid [],[TPtr(TVoid [], [])],false); "__builtin_prefetch", (TVoid [], [TPtr (TVoid [],[]);TInt (IInt, []);TInt (IInt,[])],false); + "__builtin_dcbtls", + (TVoid[], [TPtr (TVoid [],[]);TInt (IInt,[])],false); (* Access to special registers *) "__builtin_get_spr", (TInt(IUInt, []), [TInt(IInt, [])], false); diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index 62a4a0a5..14edb89d 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -207,6 +207,7 @@ Definition two_address_op (op: operation) : bool := Definition builtin_get_spr := ident_of_string "__builtin_get_spr". Definition builtin_set_spr := ident_of_string "__builtin_set_spr". Definition builtin_prefetch := ident_of_string "__builtin_prefetch". +Definition builtin_dcbtls := ident_of_string "__builtin_dcbtls". Definition builtin_constraints (ef: external_function) : list builtin_arg_constraint := @@ -215,6 +216,7 @@ Definition builtin_constraints (ef: external_function) : 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 nil | EF_vload _ => OK_addrany :: nil | EF_vstore _ => OK_addrany :: OK_default :: nil diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index b0f296ef..b5fa50dc 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -463,9 +463,11 @@ module Target (System : SYSTEM):TARGET = | Pdcbi (r1,r2) -> fprintf oc " dcbi %a, %a\n" ireg r1 ireg r2 | Pdcbt (c,r1) -> - fprintf oc " dcbt %a, %a, %s\n" ireg GPR0 ireg r1 (Z.to_string c) + fprintf oc " dcbt %s, %a, %a\n" (Z.to_string c) ireg GPR0 ireg r1 | Pdcbtst (c,r1) -> - fprintf oc " dcbtst %a, %a, %s\n" ireg GPR0 ireg r1 (Z.to_string c) + fprintf oc " dcbtst %s, %a, %a\n" (Z.to_string c) ireg GPR0 ireg r1 + | Pdcbtls (c,r1) -> + fprintf oc " dcbtls %s, %a, %a\n" (Z.to_string c) ireg GPR0 ireg r1 | Pdivw(r1, r2, r3) -> fprintf oc " divw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pdivwu(r1, r2, r3) -> |