From cfee340dc514e2cfbc5df910f7aa687e78a54d41 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 2 Sep 2015 17:17:00 +0200 Subject: Added builtin for the icbtls instruction. This commit adds a builtin for the icbtls instruction. --- powerpc/Asm.v | 2 ++ powerpc/AsmToJSON.ml | 1 + powerpc/Asmexpand.ml | 10 ++++++++++ powerpc/CBuiltins.ml | 2 ++ powerpc/Machregs.v | 2 ++ powerpc/TargetPrinter.ml | 2 ++ 6 files changed, 19 insertions(+) diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 43ddc1ed..32c7ba70 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -207,6 +207,7 @@ Inductive instruction : Type := | Pfsel: freg -> freg -> freg -> freg -> instruction (**r FP conditional move *) | Pisync: instruction (**r ISYNC barrier *) | Picbi: ireg -> ireg -> instruction (**r instruction cache invalidate *) + | Picbtls: int -> ireg -> instruction (**r instruction cache block touch and lock set *) | Plbz: ireg -> constant -> ireg -> instruction (**r load 8-bit unsigned int *) | Plbzx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) | Plfd: freg -> constant -> ireg -> instruction (**r load 64-bit float *) @@ -890,6 +891,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Plwarx _ _ _ | Plwbrx _ _ _ | Picbi _ _ + | Picbtls _ _ | Pisync | Plwsync | Plhbrx _ _ _ diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index ba61b734..8493f168 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -216,6 +216,7 @@ let p_instruction oc ic = | 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 | Picbi (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Picbi\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 + | Picbtls (n,ir1) -> fprintf oc "{\"Instruction Name\":\"Picbtls\",\"Args\":[%a,%a]}" p_int_constant n p_ireg ir1 | Pisync -> fprintf oc "{\"Instruction Name\":\"Pisync\",\"Args\":[]}" | Plwsync -> fprintf oc "{\"Instruction Name\":\"Plwsync\",\"Args\":[]}" | Plbz (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plbz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index caf256ef..43d8fc6e 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -368,6 +368,12 @@ let expand_builtin_dcbtls addr loc = let emit_inst addr = emit (Pdcbtls (loc,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,addr)) in + expand_builtin_cache_common addr emit_inst + (* Handling of compiler-inlined builtins *) let expand_builtin_inline name args res = @@ -476,6 +482,10 @@ let expand_builtin_inline name args res = expand_builtin_dcbtls a loc | "__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",_,_ -> + 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" ,_,_ -> diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index 8dbf02e5..012e4d32 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -98,6 +98,8 @@ let builtins = { (TVoid [], [TPtr (TVoid [],[]);TInt (IInt, []);TInt (IInt,[])],false); "__builtin_dcbtls", (TVoid[], [TPtr (TVoid [],[]);TInt (IInt,[])],false); + "__builtin_icbtls", + (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 14edb89d..66d21021 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -208,6 +208,7 @@ 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_icbtls := ident_of_string "__builtin_icbtls". Definition builtin_constraints (ef: external_function) : list builtin_arg_constraint := @@ -217,6 +218,7 @@ Definition builtin_constraints (ef: external_function) : 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 nil | EF_vload _ => OK_addrany :: nil | EF_vstore _ => OK_addrany :: OK_default :: nil diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 764ad8a3..6a583cca 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -536,6 +536,8 @@ module Target (System : SYSTEM):TARGET = fprintf oc " fsel %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 | Picbi (r1,r2) -> fprintf oc " icbi %a,%a\n" ireg r1 ireg r2 + | Picbtls (n,r1) -> + fprintf oc " icbtls %ld, %a, %a\n" (camlint_of_coqint n) ireg GPR0 ireg r1 | Pisync -> fprintf oc " isync\n" | Plwsync -> -- cgit