Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8

8 files changed, 61 insertions, 45 deletions

diff --git a/powerpc/Archi.v b/powerpc/Archi.v
index 8f96dafc..5b9d67cc 100644
--- a/powerpc/Archi.v
+++ b/powerpc/Archi.v
@@ -16,9 +16,8 @@
 
 (** Architecture-dependent parameters for PowerPC *)
 
+From Flocq Require Import Binary Bits.
 Require Import ZArith List.
-(*From Flocq*)
-Require Import Binary Bits.
 
 Definition ptr64 := false.
 
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index ce88778c..d8cbd94e 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -594,9 +594,7 @@ let expand_builtin_inline name args res =
       emit (Pfnmadd(res, a1, a2, a3))
   | "__builtin_fnmsub", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) ->
       emit (Pfnmsub(res, a1, a2, a3))
-  | "__builtin_fabs", [BA(FR a1)], BR(FR res) ->
-      emit (Pfabs(res, a1))
-  | "__builtin_fsqrt", [BA(FR a1)], BR(FR res) ->
+  | ("__builtin_fsqrt" | "__builtin_sqrt"), [BA(FR a1)], BR(FR res) ->
       emit (Pfsqrt(res, a1))
   | "__builtin_frsqrte", [BA(FR a1)], BR(FR res) ->
       emit (Pfrsqrte(res, a1))
@@ -767,6 +765,8 @@ let expand_builtin_inline name args res =
       emit (Pori (GPR0, GPR0, Cint _0))
   (* atomic operations *)
   | "__builtin_atomic_exchange", [BA (IR a1); BA (IR a2); BA (IR a3)],_ ->
+      (* Register constraints imposed by Machregs.v *)
+      assert(a1 = GPR3 && a2 = GPR4 && a3 = GPR5);
       emit (Plwz (GPR10,Cint _0,a2));
       emit (Psync);
       let lbl = new_label() in
@@ -786,6 +786,8 @@ let expand_builtin_inline name args res =
       emit (Pisync);
       emit (Pstw (GPR0,Cint _0, a2))
   | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR (IR res) ->
+      (* Register constraints imposed by Machregs.v *)
+      assert (a1 = GPR4 && a2 = GPR5 && res = GPR3);
       let lbl = new_label() in
       emit (Psync);
       emit (Plabel lbl);
@@ -795,6 +797,8 @@ let expand_builtin_inline name args res =
       emit (Pbf (CRbit_2, lbl));
       emit (Pisync);
   | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)],  BR (IR res) ->
+      (* Register constraints imposed by Machregs.v *)
+      assert (dst = GPR4 && exp = GPR5 && des = GPR6 && res = GPR3);
       let lbls = new_label ()
       and lblneq = new_label ()
       and lblsucc = new_label () in
diff --git a/powerpc/Builtins1.v b/powerpc/Builtins1.v
index 53c83d7e..9d7aadd9 100644
--- a/powerpc/Builtins1.v
+++ b/powerpc/Builtins1.v
@@ -19,15 +19,55 @@ Require Import String Coqlib.
 Require Import AST Integers Floats Values.
 Require Import Builtins0.
 
-Inductive platform_builtin : Type := .
+Inductive platform_builtin : Type :=
+  | BI_isel
+  | BI_uisel
+  | BI_isel64
+  | BI_uisel64
+  | BI_bsel
+  | BI_mulhw
+  | BI_mulhwu
+  | BI_mulhd
+  | BI_mulhdu.
 
 Local Open Scope string_scope.
 
 Definition platform_builtin_table : list (string * platform_builtin) :=
-  nil.
+     ("__builtin_isel", BI_isel)
+  :: ("__builtin_uisel", BI_uisel)
+  :: ("__builtin_isel64", BI_isel64)
+  :: ("__builtin_uisel64", BI_uisel64)
+  :: ("__builtin_bsel", BI_bsel)
+  :: ("__builtin_mulhw", BI_mulhw)
+  :: ("__builtin_mulhwu", BI_mulhwu)
+  :: ("__builtin_mulhd", BI_mulhd)
+  :: ("__builtin_mulhdu", BI_mulhdu)
+  :: nil.
 
 Definition platform_builtin_sig (b: platform_builtin) : signature :=
-  match b with end.
+  match b with
+  | BI_isel | BI_uisel | BI_bsel =>
+     mksignature (Tint :: Tint :: Tint :: nil) Tint cc_default
+  | BI_isel64 | BI_uisel64 =>
+     mksignature (Tint :: Tlong :: Tlong :: nil) Tlong cc_default
+  | BI_mulhw | BI_mulhwu =>
+     mksignature (Tint :: Tint :: nil) Tint cc_default
+  | BI_mulhd | BI_mulhdu =>
+     mksignature (Tlong :: Tlong :: nil) Tlong cc_default
+  end.
 
 Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) :=
-  match b with end.
+  match b with
+  | BI_isel | BI_uisel | BI_bsel =>
+    mkbuiltin_n3t Tint Tint Tint Tint (fun c n1 n2 => if Int.eq c Int.zero then n2 else n1)
+  | BI_isel64 | BI_uisel64 =>
+    mkbuiltin_n3t Tint Tlong Tlong Tlong (fun c n1 n2 => if Int.eq c Int.zero then n2 else n1)
+  | BI_mulhw =>
+    mkbuiltin_n2t Tint Tint Tint Int.mulhs
+  | BI_mulhwu =>
+    mkbuiltin_n2t Tint Tint Tint Int.mulhu
+  | BI_mulhd =>
+    mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhs
+  | BI_mulhdu =>
+    mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhu
+  end.
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml
index e29a41f1..e0826877 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -28,18 +28,6 @@ let builtins = {
       (TInt(IInt, []), [TInt(IInt, []); TInt(IInt, [])], false);
     "__builtin_mulhwu",
       (TInt(IUInt, []), [TInt(IUInt, []); TInt(IUInt, [])], false);
-    "__builtin_clz",
-      (TInt(IInt, []), [TInt(IUInt, [])], false);
-    "__builtin_clzl",
-      (TInt(IInt, []), [TInt(IULong, [])], false);
-    "__builtin_clzll",
-      (TInt(IInt, []), [TInt(IULongLong, [])], false);
-    "__builtin_ctz",
-      (TInt(IInt, []), [TInt(IUInt, [])], false);
-    "__builtin_ctzl",
-      (TInt(IInt, []), [TInt(IULong, [])], false);
-    "__builtin_ctzll",
-      (TInt(IInt, []), [TInt(IULongLong, [])], false);
     "__builtin_cmpb",
       (TInt (IUInt, []),  [TInt(IUInt, []);TInt(IUInt, [])], false);
     (* Integer arithmetic in 32/64-bit hybrid mode *)
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index e7c8758b..07622a0e 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -232,7 +232,7 @@ Definition mregs_for_builtin (ef: external_function): list (option mreg) * list
     | EF_builtin id sg =>
       if string_dec id "__builtin_atomic_exchange" then ((Some R3)::(Some R4)::(Some R5)::nil,nil)
       else if string_dec id "__builtin_sync_fetch_and_add" then ((Some R4)::(Some R5)::nil,(Some R3)::nil)
-      else if string_dec id "___builtin_atomic_compare_exchange" then ((Some R4)::(Some R5)::(Some R6)::nil, (Some R3):: nil)
+      else if string_dec id "__builtin_atomic_compare_exchange" then ((Some R4)::(Some R5)::(Some R6)::nil, (Some R3):: nil)
       else (nil, nil)
     | _ => (nil, nil)
   end.
diff --git a/powerpc/Machregsaux.ml b/powerpc/Machregsaux.ml
index 0b0d4548..d17382ad 100644
--- a/powerpc/Machregsaux.ml
+++ b/powerpc/Machregsaux.ml
@@ -12,27 +12,7 @@
 
 (** Auxiliary functions on machine registers *)
 
-open Camlcoq
-open Machregs
-
-let register_names : (mreg, string) Hashtbl.t = Hashtbl.create 31
-
-let _ =
-  List.iter
-    (fun (s, r) -> Hashtbl.add register_names r (camlstring_of_coqstring s))
-    Machregs.register_names
-
 let is_scratch_register s = s = "R0" || s = "r0"
-
-let name_of_register r =
-  try Some (Hashtbl.find register_names r) with Not_found -> None
-
-let register_by_name s =
-  Machregs.register_by_name (coqstring_uppercase_ascii_of_camlstring s)
-
-let can_reserve_register r =
-  List.mem r Conventions1.int_callee_save_regs
-  || List.mem r Conventions1.float_callee_save_regs
                                               
 let class_of_type = function
   | AST.Tint | AST.Tlong -> 0
diff --git a/powerpc/Machregsaux.mli b/powerpc/Machregsaux.mli
index d7117c21..01b0f9fd 100644
--- a/powerpc/Machregsaux.mli
+++ b/powerpc/Machregsaux.mli
@@ -12,9 +12,6 @@
 
 (** Auxiliary functions on machine registers *)
 
-val name_of_register: Machregs.mreg -> string option
-val register_by_name: string -> Machregs.mreg option
 val is_scratch_register: string -> bool
-val can_reserve_register: Machregs.mreg -> bool
 
 val class_of_type: AST.typ -> int
diff --git a/powerpc/PrintOp.ml b/powerpc/PrintOp.ml
index 8d7f17ab..77791827 100644
--- a/powerpc/PrintOp.ml
+++ b/powerpc/PrintOp.ml
@@ -42,6 +42,14 @@ let print_condition reg pp = function
       fprintf pp "%a & 0x%lx == 0" reg r1 (camlint_of_coqint n)
   | (Cmasknotzero n, [r1]) ->
       fprintf pp "%a & 0x%lx != 0" reg r1 (camlint_of_coqint n)
+  | (Ccompl c, [r1;r2]) ->
+      fprintf pp "%a %sls %a" reg r1 (comparison_name c) reg r2
+  | (Ccomplu c, [r1;r2]) ->
+      fprintf pp "%a %slu %a" reg r1 (comparison_name c) reg r2
+  | (Ccomplimm(c, n), [r1]) ->
+      fprintf pp "%a %sls %Ld" reg r1 (comparison_name c) (camlint64_of_coqint n)
+  | (Ccompluimm(c, n), [r1]) ->
+      fprintf pp "%a %slu %Ld" reg r1 (comparison_name c) (camlint64_of_coqint n)
   | _ ->
       fprintf pp "<bad condition>"