aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/Machregs.v
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2015-08-21 17:53:44 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2015-08-21 17:53:44 +0200
commit4f187fdafdac0cf4a8b83964c89d79741dbd813e (patch)
treed99aa80714b2b07817133ea8e4fc00a16f4b0adf /powerpc/Machregs.v
parent84c3580d0514c24a7c29eeec635e16183c3c5c65 (diff)
downloadcompcert-kvx-4f187fdafdac0cf4a8b83964c89d79741dbd813e.tar.gz
compcert-kvx-4f187fdafdac0cf4a8b83964c89d79741dbd813e.zip
Adapt the PowerPC port to the new builtin representation.
__builtin_get_spr() and __builtin_set_spr() work, but horrible error message if the SPR argument is not a constant. powerpc/AsmToJSON.ml needs updating.
Diffstat (limited to 'powerpc/Machregs.v')
-rw-r--r--powerpc/Machregs.v28
1 files changed, 23 insertions, 5 deletions
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index 3b7cbb76..b9af652a 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -163,11 +163,9 @@ Fixpoint destroyed_by_clobber (cl: list string): list mreg :=
Definition destroyed_by_builtin (ef: external_function): list mreg :=
match ef with
| EF_builtin _ _ => F13 :: nil
- | EF_vload _ => nil
- | EF_vstore _ => nil
- | EF_vload_global _ _ _ => R11 :: nil
- | EF_vstore_global Mint64 _ _ => R10 :: R11 :: R12 :: nil
- | EF_vstore_global _ _ _ => R11 :: R12 :: nil
+ | EF_vload _ => R11 :: nil
+ | EF_vstore Mint64 => R10 :: R11 :: R12 :: nil
+ | EF_vstore _ => R11 :: R12 :: nil
| EF_memcpy _ _ => R11 :: R12 :: F13 :: nil
| EF_inline_asm txt sg clob => destroyed_by_clobber clob
| _ => nil
@@ -203,3 +201,23 @@ Definition two_address_op (op: operation) : bool :=
| Oroli _ _ => true
| _ => false
end.
+
+(* Constraints on constant propagation for builtins *)
+
+Definition builtin_get_spr := ident_of_string "__builtin_get_spr".
+Definition builtin_set_spr := ident_of_string "__builtin_set_spr".
+
+Definition builtin_constraints (ef: external_function) :
+ list builtin_arg_constraint :=
+ match ef with
+ | 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 nil
+ | EF_vload _ => OK_addrany :: nil
+ | EF_vstore _ => OK_addrany :: OK_default :: nil
+ | EF_memcpy _ _ => OK_addrstack :: OK_addrstack :: nil
+ | EF_annot txt targs => map (fun _ => OK_all) targs
+ | EF_debug kind txt targs => map (fun _ => OK_all) targs
+ | _ => nil
+ end.