From c74211d87eb53cb310703dec2c504b26d7f24bdf Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 3 Sep 2015 13:22:28 +0200 Subject: Added builtin for mbar instruction. This commit adds a builtin function for the mbar instruction. --- powerpc/Asm.v | 2 ++ powerpc/AsmToJSON.ml | 1 + powerpc/Asmexpand.ml | 6 ++++++ powerpc/CBuiltins.ml | 2 ++ powerpc/Machregs.v | 2 ++ powerpc/TargetPrinter.ml | 2 ++ 6 files changed, 15 insertions(+) diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 6444baf9..863ed6a1 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -231,6 +231,7 @@ Inductive instruction : Type := | Plwzx_a: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) | Plwarx: ireg -> ireg -> ireg -> instruction (**r load with reservation *) | Plwbrx: ireg -> ireg -> ireg -> instruction (**r load 32-bit int and reverse endianness *) + | Pmbar: int -> instruction (**r memory barrier *) | Pmfcr: ireg -> instruction (**r move condition register to reg *) | Pmfcrbit: ireg -> crbit -> instruction (**r move condition bit to reg (pseudo) *) | Pmflr: ireg -> instruction (**r move LR to reg *) @@ -898,6 +899,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Plwsync | Plhbrx _ _ _ | Plwzu _ _ _ + | Pmbar _ | Pmfcr _ | Pmfspr _ _ | Pmtspr _ _ diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 83d01dc5..3550cd64 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -242,6 +242,7 @@ let p_instruction oc ic = | Plwzx_a (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plwzx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Plwarx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plwarx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Plwbrx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plwbrx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pmbar c -> fprintf oc "{\"Instruction Name\":\"Pmbar\",\"Args\":[%a]}" p_int_constant c | Pmfcr ir -> fprintf oc "{\"Instruction Name\":\"Pmfcr\",\"Args\":[%a]}" p_ireg ir | Pmfcrbit (ir,crb) -> assert false (* Should not occur *) | Pmflr ir -> fprintf oc "{\"Instruction Name\":\"Pmflr\",\"Args\":[%a]}" p_ireg ir diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index f266f3ec..3e57cdbf 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -466,6 +466,12 @@ let expand_builtin_inline name args res = emit (Pisync) | "__builtin_lwsync", [], _ -> 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"); + emit (Pmbar mo) + | "__builin_mbar",_, _ -> + raise (Error "the argument of __builtin_mbar must be a constant"); | "__builtin_trap", [], _ -> emit (Ptrap) (* Vararg stuff *) diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index 0785c7fa..e18fdb2d 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -85,6 +85,8 @@ let builtins = { (TVoid [], [], false); "__builtin_lwsync", (TVoid [], [], false); + "__builtin_mbar", + (TVoid [], [TInt(IInt, [])], false); "__builtin_trap", (TVoid [], [], false); (* Cache isntructions *) diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index 66d21021..402f07d1 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -209,6 +209,7 @@ 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_mbar := ident_of_string "__builtin_mbar". Definition builtin_constraints (ef: external_function) : list builtin_arg_constraint := @@ -219,6 +220,7 @@ Definition builtin_constraints (ef: external_function) : 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_mbar then 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 ffd01b69..af5dafed 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -586,6 +586,8 @@ module Target (System : SYSTEM):TARGET = fprintf oc " lwzu %a, %a(%a)\n" ireg r1 constant c ireg r2 | Plwzx(r1, r2, r3) | Plwzx_a(r1, r2, r3) -> fprintf oc " lwzx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pmbar mo -> + fprintf oc " mbar %ld\n" (camlint_of_coqint mo) | Pmfcr(r1) -> fprintf oc " mfcr %a\n" ireg r1 | Pmfcrbit(r1, bit) -> -- cgit