aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-09-07 09:40:24 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-09-07 09:40:24 +0200
commita168d6a141e77a5fa98017b23ab2aadc5748fe94 (patch)
tree95dc6301836fbd445094f5070c35eb9f1e4ab62f /powerpc
parent47d0e5256ab79b402faae14260fa2fabc1d24dcb (diff)
downloadcompcert-kvx-a168d6a141e77a5fa98017b23ab2aadc5748fe94.tar.gz
compcert-kvx-a168d6a141e77a5fa98017b23ab2aadc5748fe94.zip
Simplified generation of builtins for cache instructions.
The cache instructions need no special constraint on the address argument. Therefore also the generation of the address is no longer needed.
Diffstat (limited to 'powerpc')
-rw-r--r--powerpc/Asmexpand.ml75
-rw-r--r--powerpc/Machregs.v6
2 files changed, 21 insertions, 60 deletions
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 3e57cdbf..a2c07baf 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -324,56 +324,6 @@ 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,GPR0,addr));
- end else if Int.eq rw _1 then begin
- emit (Pdcbtst (loc,GPR0,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,GPR0,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,GPR0,addr)) in
- expand_builtin_cache_common addr emit_inst
-
(* Handling of compiler-inlined builtins *)
let expand_builtin_inline name args res =
@@ -468,7 +418,7 @@ let expand_builtin_inline name args res =
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");
+ raise (Error "the argument of __builtin_mbar must be 0 or 1");
emit (Pmbar mo)
| "__builin_mbar",_, _ ->
raise (Error "the argument of __builtin_mbar must be a constant");
@@ -484,16 +434,27 @@ let expand_builtin_inline name args res =
emit (Pdcbi (GPR0,a1))
| "__builtin_icbi", [BA(IR a1)],_ ->
emit (Picbi(GPR0,a1))
- | "__builtin_dcbtls", [a; BA_int loc],_ ->
- expand_builtin_dcbtls a loc
+ | "__builtin_dcbtls", [BA (IR a1); BA_int loc],_ ->
+ if not ((Int.eq loc _0) || (Int.eq loc _2)) then
+ raise (Error "the second argument of __builtin_dcbtls must be a constant between 0 and 2");
+ emit (Pdcbtls (loc,GPR0,a1))
| "__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", [BA (IR a1); BA_int loc],_ ->
+ if not ((Int.eq loc _0) || (Int.eq loc _2)) then
+ raise (Error "the second argument of __builtin_icbtls must be 0 or 2");
+ emit (Picbtls (loc,GPR0,a1))
| "__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" , [BA (IR a1) ;BA_int rw; BA_int loc],_ ->
+ if not (Int.ltu loc _4) then
+ raise (Error "the last argument of __builtin_prefetch must be 0, 1 or 2");
+ if Int.eq rw _0 then begin
+ emit (Pdcbt (loc,GPR0,a1));
+ end else if Int.eq rw _1 then begin
+ emit (Pdcbtst (loc,GPR0,a1));
+ end else
+ raise (Error "the second argument of __builtin_prefetch must be 0 or 1")
| "__builtin_prefetch" ,_,_ ->
raise (Error "the second and third argument of __builtin_prefetch must be a constant")
| "__builtin_dcbz",[BA (IR a1)],_ ->
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index 402f07d1..a2017dca 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -217,9 +217,9 @@ Definition builtin_constraints (ef: external_function) :
| EF_builtin id sg =>
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 if ident_eq id builtin_icbtls then OK_addrany::OK_const::nil
+ else if ident_eq id builtin_prefetch then OK_default :: OK_const :: OK_const :: nil
+ else if ident_eq id builtin_dcbtls then OK_default::OK_const::nil
+ else if ident_eq id builtin_icbtls then OK_default::OK_const::nil
else if ident_eq id builtin_mbar then OK_const::nil
else nil
| EF_vload _ => OK_addrany :: nil