Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3

7 files changed, 9 insertions, 46 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/Asm.v b/arm/Asm.v
index 194074ac..293df274 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -696,7 +696,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pfsubd r1 r2 r3 =>
       Next (nextinstr (rs#r1 <- (Val.subf rs#r2 rs#r3))) m
   | Pflid r1 f =>
-      Next (nextinstr (rs#r1 <- (Vfloat f))) m
+      Next (nextinstr (rs#IR14 <- Vundef #r1 <- (Vfloat f))) m
   | Pfcmpd r1 r2 =>
       Next (nextinstr (compare_float rs rs#r1 rs#r2)) m
   | Pfcmpzd r1 =>
@@ -923,7 +923,7 @@ Inductive step: state -> trace -> state -> Prop :=
       external_call ef ge vargs m t vres m' ->
       rs' = nextinstr
               (set_res res vres
-                (undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) ->
+                (undef_regs (IR IR14 :: map preg_of (destroyed_by_builtin ef)) rs)) ->
       step (State rs m) t (State rs' m')
   | exec_step_external:
       forall b ef args res rs m t rs' m',
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..fd70c9ad 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.
@@ -761,13 +761,15 @@ Opaque loadind.
   econstructor; eauto.
   instantiate (2 := tf); instantiate (1 := x).
   unfold nextinstr. rewrite Pregmap.gss.
-  rewrite set_res_other. rewrite undef_regs_other_2.
+  rewrite set_res_other. simpl. rewrite undef_regs_other_2.
+  rewrite Pregmap.gso by auto with asmgen.
   rewrite <- H1. simpl. econstructor; eauto.
   eapply code_tail_next_int; eauto.
   rewrite preg_notin_charact. intros. auto with asmgen.
   auto with asmgen.
   apply agree_nextinstr. eapply agree_set_res; auto.
-  eapply agree_undef_regs; eauto. intros; apply undef_regs_other_2; auto.
+  eapply agree_undef_regs; eauto.
+  intros. simpl. rewrite undef_regs_other_2; auto. apply Pregmap.gso. auto with asmgen.
   congruence.
 
 - (* Mgoto *)
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