From 0df99dc46209a9fe5026b83227ef73280f0dab70 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Sun, 6 Dec 2020 16:46:42 +0100
Subject: AArch64 modeling of registers destroyed by pseudo-instructions

Pfmovimms, Pfmovimmd destroy X16
Pbtbl preserves X17
Inlined built-in functions destroy X16 and X30
---
 aarch64/Asm.v         |  8 ++++----
 aarch64/Asmgenproof.v | 11 +++++++----
 2 files changed, 11 insertions(+), 8 deletions(-)

(limited to 'aarch64')

diff --git a/aarch64/Asm.v b/aarch64/Asm.v
index 5ac577b1..346cb649 100644
--- a/aarch64/Asm.v
+++ b/aarch64/Asm.v
@@ -970,9 +970,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pfmov rd r1 =>
       Next (nextinstr (rs#rd <- (rs#r1))) m
   | Pfmovimms rd f =>
-      Next (nextinstr (rs#rd <- (Vsingle f))) m
+      Next (nextinstr (rs#X16 <- Vundef #rd <- (Vsingle f))) m
   | Pfmovimmd rd f =>
-      Next (nextinstr (rs#rd <- (Vfloat f))) m
+      Next (nextinstr (rs#X16 <- Vundef #rd <- (Vfloat f))) m
   | Pfmovi S rd r1 =>
       Next (nextinstr (rs#rd <- (float32_of_bits rs##r1))) m
   | Pfmovi D rd r1 =>
@@ -1097,7 +1097,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       | Vint n =>
           match list_nth_z tbl (Int.unsigned n) with
           | None => Stuck
-          | Some lbl => goto_label f lbl (rs#X16 <- Vundef #X17 <- Vundef) m
+          | Some lbl => goto_label f lbl (rs#X16 <- Vundef) m
           end
       | _ => Stuck
       end
@@ -1212,7 +1212,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 X16 :: IR X30 :: 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/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index eeff1956..b60623a6 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -831,13 +831,16 @@ Local Transparent destroyed_by_op.
   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. rewrite undef_regs_other.
   rewrite <- H1. simpl. econstructor; eauto.
   eapply code_tail_next_int; eauto.
-  rewrite preg_notin_charact. intros. auto with asmgen.
+  simpl; intros. destruct H4. congruence. destruct H4. congruence.
+  exploit list_in_map_inv; eauto. intros (mr & U & V). subst.
+  auto with asmgen.
   auto with asmgen.
   apply agree_nextinstr. eapply agree_set_res; auto.
-  eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto.
+  eapply agree_undef_regs; eauto. intros.
+  simpl. rewrite undef_regs_other_2; auto. Simpl.
   congruence.
 
 - (* Mgoto *)
@@ -879,7 +882,7 @@ Local Transparent destroyed_by_op.
   exploit functions_transl; eauto. intro FN.
   generalize (transf_function_no_overflow _ _ H5); intro NOOV.
   exploit find_label_goto_label. eauto. eauto.
-  instantiate (2 := rs0#X16 <- Vundef #X17 <- Vundef).
+  instantiate (2 := rs0#X16 <- Vundef).
   Simpl. eauto.
   eauto.
   intros [tc' [rs' [A [B C]]]].
-- 
cgit