Merge branch 'master' into ppc64

Resolved conflicts in:configure	powerpc/Asmexpand.ml

1 files changed, 17 insertions, 2 deletions

diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index e4006523..20bec532 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -160,9 +160,16 @@ Fixpoint destroyed_by_clobber (cl: list string): list mreg :=
       end
   end.
 
+Definition builtin_atomic_exchange := ident_of_string "__builtin_atomic_exchange".
+Definition builtin_sync_and_fetch := ident_of_string "__builtin_sync_fetch_and_add".
+Definition builtin_atomic_compare_exchange := ident_of_string "__builtin_atomic_compare_exchange".
+
 Definition destroyed_by_builtin (ef: external_function): list mreg :=
   match ef with
-  | EF_builtin _ _ => F13 :: nil
+  | EF_builtin id sg =>
+    if ident_eq id builtin_atomic_exchange then R10::nil
+    else if ident_eq id builtin_atomic_compare_exchange then R10::R11::nil
+    else F13 :: nil
   | EF_vload _ => R11 :: nil
   | EF_vstore Mint64 => R10 :: R11 :: R12 :: nil
   | EF_vstore _ => R11 :: R12 :: nil
@@ -183,8 +190,16 @@ Definition temp_for_parent_frame: mreg :=
 Definition mregs_for_operation (op: operation): list (option mreg) * option mreg :=
   (nil, None).
 
+
 Definition mregs_for_builtin (ef: external_function): list (option mreg) * list (option mreg) :=
-  (nil, nil).
+  match ef with
+    | EF_builtin id sg =>
+      if ident_eq id builtin_atomic_exchange then ((Some R3)::(Some R4)::(Some R5)::nil,nil)
+      else if ident_eq id builtin_sync_and_fetch then ((Some R4)::(Some R5)::nil,(Some R3)::nil)
+      else if ident_eq id builtin_atomic_compare_exchange then ((Some R4)::(Some R5)::(Some R6)::nil, (Some R3):: nil)
+      else (nil, nil)
+    | _ => (nil, nil)
+  end.
 
 Global Opaque
     destroyed_by_op destroyed_by_load destroyed_by_store