Added builtin for the icbtls instruction.

This commit adds a builtin for the icbtls instruction.

6 files changed, 19 insertions, 0 deletions

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