From f0b44f733f49dc77d2acda09d99390373048ba50 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Mon, 23 Nov 2020 16:12:07 +0100
Subject: a step forward in bblock_simu_reduce

---
 aarch64/Asmblockdeps.v | 74 +++++++++++++++++++++++---------------------------
 1 file changed, 34 insertions(+), 40 deletions(-)

(limited to 'aarch64/Asmblockdeps.v')

diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v
index d778ddca..ef7f803d 100644
--- a/aarch64/Asmblockdeps.v
+++ b/aarch64/Asmblockdeps.v
@@ -2232,6 +2232,28 @@ Proof.
   * discriminate.
 Qed.
 
+Lemma incrPC_set_res_commut res: forall d vres rs,  
+  incrPC d (set_res (map_builtin_res DR res) vres rs) =
+  set_res (map_builtin_res DR res) vres (incrPC d rs).
+Proof.
+  induction res; simpl; auto.
+  - intros; apply functional_extensionality.
+    unfold incrPC; intros x0.
+    destruct (PregEq.eq x0 PC).
+    + subst; rewrite! Pregmap.gss; auto.
+    + rewrite Pregmap.gso; auto.
+      destruct (PregEq.eq x x0).
+      * subst; rewrite! Pregmap.gss; auto.
+      * rewrite !Pregmap.gso; auto.
+  - intros; rewrite IHres2. f_equal. auto.
+Qed.
+
+Lemma incrPC_undef_regs_commut l : forall d rs,
+  incrPC d (undef_regs (map preg_of l) rs) = undef_regs (map preg_of l) (incrPC d rs).
+Proof.
+  induction l; simpl; auto.
+Admitted.
+
 Lemma bblock_simu_reduce:
   forall p1 p2,
   L.bblock_simu Ge (trans_block p1) (trans_block p2) ->
@@ -2258,7 +2280,7 @@ Proof.
     inversion H4. econstructor. }
     { inversion H2; subst.
       destruct (exec_body _ _ (body p2) _ _) as [[rs2 m2]|]; try discriminate.
-intros H4. eexists; eexists; split; try reflexivity.
+    intros H4. eexists; eexists; split; try reflexivity.
     destruct (exit p2) as [[]|] eqn:EQEX2; simpl in *; try discriminate; try econstructor; eauto.
     inversion H4. rewrite H3. econstructor. }
   - (* Builtin *)
@@ -2275,46 +2297,18 @@ intros H4. eexists; eexists; split; try reflexivity.
     destruct (exec_body _ _ (body p2) _ _) as [[rs2 m2]|]; try discriminate.
     intros H4. eexists; eexists; split; try reflexivity.
     inversion H2; subst. inversion H4; subst.
-    econstructor; eauto.
-    + unfold incrPC in H5.
-      replace (rs2 SP) with (rs1 SP).
+    assert (EQ: forall r, r<>PC -> rs1 r = rs2 r).
+    { unfold incrPC in H5. intros x H; replace (rs1 x) with ((rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size p1)))) x).
+      + rewrite H5; rewrite Pregmap.gso; auto.
+      + rewrite Pregmap.gso; auto.
+    }
+   econstructor; eauto.
+    + rewrite <- (EQ SP); try discriminate.
       replace (fun r : dreg => rs2 r) with (fun r : dreg => rs1 r); auto.
-      * apply functional_extensionality.
-        intros r; destruct (PregEq.eq r PC); try discriminate.
-        replace (rs1 r) with (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size p1))) r) by auto.
-        rewrite H5; rewrite Pregmap.gso; auto.
-      * replace (rs1 SP) with (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size p1))) SP) by auto.
-        rewrite H5; rewrite Pregmap.gso; auto; try discriminate.
-    + admit.
-    
-(*  generalize (H0 (trans_state (State rs m))); clear H0.
-  intros H0 m' t0 (rs1 & m1 & H1 & H2).
-  exploit (bisimu Ge rs m (trans_state (State rs m)) p1); eauto.
-  exploit (bisimu Ge rs m (trans_state (State rs m)) p2); eauto.
-  unfold bbstep, estep.
-  rewrite H1; simpl.
-  unfold has_builtin in BLT.
-  destruct (exit p1) eqn:EQEX1. destruct c.
-  - inversion H2; subst.
-    destruct (exec_body _ _ (body p2) _ _) as [[rs2 m2]|] eqn:EQBDY2; try congruence.
-    unfold trans_block, exec in *.
-    exploit (bisimu_body); eauto. erewrite H1. simpl.
-    (*destruct (exec_body _ _ (body p2) _ _) eqn:EQBDY1.*)
-  destruct (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) p1 rs m); try (unfold Stuck in EBB; congruence).
-  intros H1 (s2' & exp2 & MS'). unfold exec in exp2, H1. rewrite exp2 in H0.
-  destruct H0 as (m2' & H0 & H2). discriminate. rewrite H0 in H1.
-  destruct (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) p2 rs m); simpl in H1.
-  * unfold match_states in H1, MS'. destruct s, s0.
-    destruct H1 as (s' & H1 & H3 & H4). inv H1. inv MS'.
-    replace (_rs0) with (_rs).
-    - replace (_m0) with (_m); auto. congruence.
-    - apply functional_extensionality. intros r.
-      generalize (H1 r). intros Hr. congruence.
-  * discriminate.*)
-
-Admitted.
-  
-(*Qed.*)
+      apply functional_extensionality.
+      intros; apply EQ; try discriminate. 
+    + rewrite !incrPC_set_res_commut, !incrPC_undef_regs_commut; rewrite H5. auto.
+Qed.
 
 (** Used for debug traces *)
 
-- 
cgit