Added builtin for dcbtls

THis commit adds a builtin function for the dcbtls instruction.
Additionaly it changes the printing of the dcbt and dcbtst instruction to
embedded mode and adds support for different address variants.

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