Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1

4 files changed, 25 insertions, 9 deletions

diff --git a/aarch64/Machregs.v b/aarch64/Machregs.v
index 3d27f48f..bfe23e83 100644
--- a/aarch64/Machregs.v
+++ b/aarch64/Machregs.v
@@ -158,7 +158,7 @@ Definition destroyed_by_builtin (ef: external_function): list mreg :=
   match ef with
   | EF_memcpy sz al => R15 :: R17 :: R29 :: nil
   | EF_inline_asm txt sg clob => destroyed_by_clobber clob
-  | EF_profiling _ _ => R15 :: R17 :: nil
+  | EF_profiling _ _ => R15 :: R17 :: R29 :: nil
   | _ => nil
   end.
 
diff --git a/aarch64/Machregsaux.mli b/aarch64/Machregsaux.mli
new file mode 100644
index 00000000..01b0f9fd
--- /dev/null
+++ b/aarch64/Machregsaux.mli
@@ -0,0 +1,17 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Auxiliary functions on machine registers *)
+
+val is_scratch_register: string -> bool
+
+val class_of_type: AST.typ -> int
diff --git a/aarch64/PeepholeOracle.ml b/aarch64/PeepholeOracle.ml
index 18f41fed..2b214df4 100644
--- a/aarch64/PeepholeOracle.ml
+++ b/aarch64/PeepholeOracle.ml
@@ -401,9 +401,8 @@ let pair_rep_inv insta =
    * for one type of inst. Lists contains integers which
    * are the indices of insts in the main array "insta". *)
   init_symb_mem ();
-  for i = Array.length insta - 1 downto 1 do
+  for i = Array.length insta - 1 downto 0 do
     let h0 = insta.(i) in
-    let h1 = insta.(i - 1) in
     (* Here we need to update every symbolic memory according to the matched inst *)
     update_pot_rep_basic h0 insta (Ldr P32) true;
     update_pot_rep_basic h0 insta (Ldr P64) true;
@@ -413,9 +412,9 @@ let pair_rep_inv insta =
     update_pot_rep_basic h0 insta (Str P64) true;
     update_pot_rep_basic h0 insta (Str P32f) true;
     update_pot_rep_basic h0 insta (Str P64f) true;
-    match (h0, h1) with
+    match h0 with
     (* Non-consecutive ldr *)
-    | PLoad (PLd_rd_a (ldi, rd1, ADimm (b1, n1))), _ ->
+    | PLoad (PLd_rd_a (ldi, rd1, ADimm (b1, n1))) ->
         if is_compat_load ldi then (
           (* Search a previous compatible load *)
           let ld_t = get_load_pht ldi in
@@ -445,7 +444,7 @@ let pair_rep_inv insta =
                        (trans_ldi ldi, rd1, r, chunk_load ldi, c, ADimm (b, n1)))));
           Hashtbl.replace symb_mem ld_t pot_rep)
     (* Non-consecutive str *)
-    | PStore (PSt_rs_a (sti, rd1, ADimm (b1, n1))), _ ->
+    | PStore (PSt_rs_a (sti, rd1, ADimm (b1, n1))) ->
         if is_compat_store sti then (
           (* Search a previous compatible store *)
           let st_t = get_store_pht sti in
@@ -469,7 +468,7 @@ let pair_rep_inv insta =
                      (trans_sti sti, rd1, r, chunk_store sti, c, ADimm (b, n1))));
           Hashtbl.replace symb_mem st_t pot_rep
           (* Any other inst *))
-    | i, _ -> (
+    | i -> (
         (* Clear list of candidates if there is a non supported store *)
         match i with PStore _ -> reset_str_symb_mem () | _ -> ())
   done
diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml
index 229aa1b4..1ca3be16 100644
--- a/aarch64/TargetPrinter.ml
+++ b/aarch64/TargetPrinter.ml
@@ -349,8 +349,8 @@ module Target(System: SYSTEM): TARGET =
       fprintf oc "%s:\n" lbl;
       fprintf oc "	ldaxr	x17, [x15]\n";
       fprintf oc "	add	x17, x17, 1\n";
-      fprintf oc "	stlxr	w17, x17, [x15]\n";
-      fprintf oc "	cbnz	w17, %s\n" lbl;
+      fprintf oc "	stlxr	w29, x17, [x15]\n";
+      fprintf oc "	cbnz	w29, %s\n" lbl;
       fprintf oc "%s end profiling %a %d\n" comment
         Profilingaux.pp_id id kind;;