Merge branch 'new-builtins'

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.