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

7 files changed, 34 insertions, 33 deletions

diff --git a/aarch64/Archi.v b/aarch64/Archi.v
index 7d7b6887..7f39d1fa 100644
--- a/aarch64/Archi.v
+++ b/aarch64/Archi.v
@@ -6,15 +6,17 @@
 (*                                                                     *)
 (*  Copyright Institut National de Recherche en Informatique et en     *)
 (*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
 (*  under the terms of the INRIA Non-Commercial License Agreement.     *)
 (*                                                                     *)
 (* *********************************************************************)
 
 (** Architecture-dependent parameters for AArch64 *)
 
+From Flocq Require Import Binary Bits.
 Require Import ZArith List.
-(*From Flocq*)
-Require Import Binary Bits.
 
 Definition ptr64 := true.
 
diff --git a/aarch64/Asm.v b/aarch64/Asm.v
index 47cd3051..5ac577b1 100644
--- a/aarch64/Asm.v
+++ b/aarch64/Asm.v
@@ -237,6 +237,7 @@ Inductive instruction: Type :=
   | Pclz (sz: isize) (rd r1: ireg)                                    (**r count leading zero bits *)
   | Prev (sz: isize) (rd r1: ireg)                                    (**r reverse bytes *)
   | Prev16 (sz: isize) (rd r1: ireg)                                  (**r reverse bytes in each 16-bit word *)
+  | Prbit (sz: isize) (rd r1: ireg)                                   (**r reverse bits *)
   (** Conditional data processing *)
   | Pcsel (rd: ireg) (r1 r2: ireg) (c: testcond)                      (**r int conditional move *)
   | Pcset (rd: ireg) (c: testcond)                                    (**r set to 1/0 if cond is true/false *)
@@ -282,6 +283,8 @@ Inductive instruction: Type :=
   | Pfmsub (sz: fsize) (rd r1 r2 r3: freg)                            (**r [rd = r3 - r1 * r2] *)
   | Pfnmadd (sz: fsize) (rd r1 r2 r3: freg)                           (**r [rd = - r3 - r1 * r2] *)
   | Pfnmsub (sz: fsize) (rd r1 r2 r3: freg)                           (**r [rd = - r3 + r1 * r2] *)
+  | Pfmax (sz: fsize) (rd r1 r2: freg)                                (**r maximum *)
+  | Pfmin (sz: fsize) (rd r1 r2: freg)                                (**r minimum *)
   (** Floating-point comparison *)
   | Pfcmp (sz: fsize) (r1 r2: freg)                                   (**r compare [r1] and [r2] *)
   | Pfcmp0 (sz: fsize) (r1: freg)                                     (**r compare [r1] and [+0.0] *)
@@ -1107,11 +1110,14 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pclz _ _ _
   | Prev _ _ _
   | Prev16 _ _ _
+  | Prbit _ _ _
   | Pfsqrt _ _ _
   | Pfmadd _ _ _ _ _
   | Pfmsub _ _ _ _ _
   | Pfnmadd _ _ _ _ _
   | Pfnmsub _ _ _ _ _
+  | Pfmax _ _ _ _
+  | Pfmin _ _ _ _
   | Pnop
   | Pcfi_adjust _ 
   | Pcfi_rel_offset _ =>
diff --git a/aarch64/Asmexpand.ml b/aarch64/Asmexpand.ml
index b0787d0a..5b183c2d 100644
--- a/aarch64/Asmexpand.ml
+++ b/aarch64/Asmexpand.ml
@@ -337,7 +337,7 @@ let expand_builtin_inline name args res =
   | "__builtin_bswap16", [BA(IR a1)], BR(IR res) ->
      emit (Prev16(W, res, a1));
      emit (Pandimm(W, res, RR0 res, Z.of_uint 0xFFFF))
-  (* Count leading zeros and leading sign bits *)
+  (* Count leading zeros, leading sign bits, trailing zeros *)
   | "__builtin_clz",  [BA(IR a1)], BR(IR res) ->
      emit (Pclz(W, res, a1))
   | ("__builtin_clzl" | "__builtin_clzll"),  [BA(IR a1)], BR(IR res) ->
@@ -346,10 +346,14 @@ let expand_builtin_inline name args res =
      emit (Pcls(W, res, a1))
   | ("__builtin_clsl" | "__builtin_clsll"),  [BA(IR a1)], BR(IR res) ->
      emit (Pcls(X, res, a1))
+  | "__builtin_ctz",  [BA(IR a1)], BR(IR res) ->
+     emit (Prbit(W, res, a1));
+     emit (Pclz(W, res, res))
+  | ("__builtin_ctzl" | "__builtin_ctzll"),  [BA(IR a1)], BR(IR res) ->
+     emit (Prbit(X, res, a1));
+     emit (Pclz(X, res, res))
  (* Float arithmetic *)
-  | "__builtin_fabs",  [BA(FR a1)], BR(FR res) ->
-     emit (Pfabs(D, res, a1))
-  | "__builtin_fsqrt",  [BA(FR a1)], BR(FR res) ->
+  | ("__builtin_fsqrt" | "__builtin_sqrt"),  [BA(FR a1)], BR(FR res) ->
      emit (Pfsqrt(D, res, a1))
   | "__builtin_fmadd", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) ->
       emit (Pfmadd(D, res, a1, a2, a3))
@@ -359,6 +363,10 @@ let expand_builtin_inline name args res =
       emit (Pfnmadd(D, res, a1, a2, a3))
   | "__builtin_fnmsub", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) ->
       emit (Pfnmsub(D, res, a1, a2, a3))
+  | "__builtin_fmax", [BA (FR a1); BA (FR a2)], BR (FR res) ->
+      emit (Pfmax (D, res, a1, a2))
+  | "__builtin_fmin", [BA (FR a1); BA (FR a2)], BR (FR res) ->
+      emit (Pfmin (D, res, a1, a2))
   (* Vararg *)
   | "__builtin_va_start", [BA(IR a)], _ ->
       expand_builtin_va_start a
diff --git a/aarch64/CBuiltins.ml b/aarch64/CBuiltins.ml
index fdc1372d..e2a9c87a 100644
--- a/aarch64/CBuiltins.ml
+++ b/aarch64/CBuiltins.ml
@@ -6,6 +6,9 @@
 (*                                                                     *)
 (*  Copyright Institut National de Recherche en Informatique et en     *)
 (*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
 (*  under the terms of the INRIA Non-Commercial License Agreement.     *)
 (*                                                                     *)
 (* *********************************************************************)
@@ -29,14 +32,6 @@ let builtins = {
     "__builtin_fence",
       (TVoid [], [], false);
     (* Integer arithmetic *)
-    "__builtin_bswap64",
-      (TInt(IULongLong, []), [TInt(IULongLong, [])], false);
-    "__builtin_clz",
-      (TInt(IInt, []), [TInt(IUInt, [])], false);
-    "__builtin_clzl",
-      (TInt(IInt, []), [TInt(IULong, [])], false);
-    "__builtin_clzll",
-      (TInt(IInt, []), [TInt(IULongLong, [])], false);
     "__builtin_cls",
       (TInt(IInt, []), [TInt(IInt, [])], false);
     "__builtin_clsl",
diff --git a/aarch64/Machregsaux.ml b/aarch64/Machregsaux.ml
index f13a9ff5..41db3bd4 100644
--- a/aarch64/Machregsaux.ml
+++ b/aarch64/Machregsaux.ml
@@ -12,28 +12,9 @@
 
 (** 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 = "X16" || s = "x16" || s = "X30" || s = "x30"
 
-
-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 = Conventions1.is_callee_save r
-                           
 let class_of_type = function
   | AST.Tint | AST.Tlong -> 0
   | AST.Tfloat | AST.Tsingle -> 1
diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml
index 8d74daf4..6ba44cf0 100644
--- a/aarch64/TargetPrinter.ml
+++ b/aarch64/TargetPrinter.ml
@@ -399,6 +399,8 @@ module Target : TARGET =
         fprintf oc "	rev	%a, %a\n" ireg (sz, rd) ireg (sz, r1)
     | Prev16(sz, rd, r1) ->
         fprintf oc "	rev16	%a, %a\n" ireg (sz, rd) ireg (sz, r1)
+    | Prbit(sz, rd, r1) ->
+        fprintf oc "	rbit	%a, %a\n" ireg (sz, rd) ireg (sz, r1)
     (* Conditional data processing *)
     | Pcsel(rd, r1, r2, c) ->
         fprintf oc "	csel	%a, %a, %a, %s\n" xreg rd xreg r1 xreg r2 (condition_name c)
@@ -489,6 +491,10 @@ module Target : TARGET =
         fprintf oc "	fnmadd	%a, %a, %a, %a\n" freg (sz, rd) freg (sz, r1) freg (sz, r2) freg (sz, r3)
     | Pfnmsub(sz, rd, r1, r2, r3) ->
         fprintf oc "	fnmsub	%a, %a, %a, %a\n" freg (sz, rd) freg (sz, r1) freg (sz, r2) freg (sz, r3)
+    | Pfmax (sz, rd, r1, r2) ->
+        fprintf oc "	fmax	%a, %a, %a\n" freg (sz, rd) freg (sz, r1) freg (sz, r2)
+    | Pfmin (sz, rd, r1, r2) ->
+        fprintf oc "	fmin	%a, %a, %a\n" freg (sz, rd) freg (sz, r1) freg (sz, r2)
     (* Floating-point comparison *)
     | Pfcmp(sz, r1, r2) ->
         fprintf oc "	fcmp	%a, %a\n" freg (sz, r1) freg (sz, r2)
diff --git a/aarch64/extractionMachdep.v b/aarch64/extractionMachdep.v
index e82056e2..5f26dc28 100644
--- a/aarch64/extractionMachdep.v
+++ b/aarch64/extractionMachdep.v
@@ -6,6 +6,9 @@
 (*                                                                     *)
 (*  Copyright Institut National de Recherche en Informatique et en     *)
 (*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
 (*  under the terms of the INRIA Non-Commercial License Agreement.     *)
 (*                                                                     *)
 (* *********************************************************************)