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

6 files changed, 3 insertions, 42 deletions

diff --git a/arm/Archi.v b/arm/Archi.v
index 738341cc..c334c2a7 100644
--- a/arm/Archi.v
+++ b/arm/Archi.v
@@ -16,9 +16,8 @@
 
 (** Architecture-dependent parameters for ARM *)
 
+From Flocq Require Import Binary Bits.
 Require Import ZArith List.
-(*From Flocq*)
-Require Import Binary Bits.
 
 Definition ptr64 := false.
 
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index 6996c9bb..104bfc94 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -349,9 +349,7 @@ let expand_builtin_inline name args res =
      emit (Prsb(res, res, SOimm _32));
      emit (Plabel lbl2)
   (* Float arithmetic *)
-  | "__builtin_fabs",  [BA(FR a1)], BR(FR res) ->
-     emit (Pfabsd (res,a1))
-  | "__builtin_fsqrt", [BA(FR a1)], BR(FR res) ->
+  | ("__builtin_fsqrt" | "__builtin_sqrt"), [BA(FR a1)], BR(FR res) ->
      emit (Pfsqrt (res,a1))
   (* 64-bit integer arithmetic *)
   | "__builtin_negl", [BA_splitlong(BA(IR ah), BA(IR al))],
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index 92ae524f..b3c64ba9 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -225,7 +225,7 @@ Proof.
   TailNoLabel.
   eapply tail_nolabel_trans; TailNoLabel.
 Qed.
-Hint Resolve indexed_memory_access_label.
+Hint Resolve indexed_memory_access_label: labels.
 
 Remark loadind_label:
   forall base ofs ty dst k c, loadind base ofs ty dst k = OK c -> tail_nolabel k c.
diff --git a/arm/CBuiltins.ml b/arm/CBuiltins.ml
index d6a1ea35..6462a8c5 100644
--- a/arm/CBuiltins.ml
+++ b/arm/CBuiltins.ml
@@ -22,19 +22,6 @@ let builtins = {
     "__builtin_va_list", TPtr(TVoid [], [])
   ];
   builtin_functions = [
-    (* Integer arithmetic *)
-    "__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);
     (* Memory accesses *)
     "__builtin_read16_reversed",
       (TInt(IUShort, []), [TPtr(TInt(IUShort, [AConst]), [])], false);
diff --git a/arm/Machregsaux.ml b/arm/Machregsaux.ml
index 14c75155..24a33e9e 100644
--- a/arm/Machregsaux.ml
+++ b/arm/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 = "R14"  || s = "r14"
-
-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/arm/Machregsaux.mli b/arm/Machregsaux.mli
index d7117c21..01b0f9fd 100644
--- a/arm/Machregsaux.mli
+++ b/arm/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