Added builtin for mbar instruction.

This commit adds a builtin function for the mbar instruction.

6 files changed, 15 insertions, 0 deletions

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) ->