Postpass scheduling OK

- Modifying Asmblockdeps to adapt to Pfmovimm new specification
- Changing the Asmgenproof to adapt PArith in consequence
- Modifying the oracle to specify correct wlocs
- Cleaning everywhere

1 files changed, 35 insertions, 13 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index d062654b..7266cce8 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -787,18 +787,19 @@ Lemma exec_arith_instr_dont_move_PC ai rs rs': forall
 Proof.
   destruct ai; simpl; intros;
   try (rewrite <- BASIC; rewrite Pregmap.gso; auto; discriminate).
-  - destruct i; simpl in BASIC.
-    + unfold compare_long in BASIC; rewrite <- BASIC.
-      repeat rewrite Pregmap.gso; try discriminate. reflexivity.
-    + unfold compare_long in BASIC; rewrite <- BASIC.
-      repeat rewrite Pregmap.gso; try discriminate. reflexivity.
-    + destruct sz;
-      try (unfold compare_single in BASIC || unfold compare_float in BASIC);
-      destruct (rs r1), (rs r2);
-      try (rewrite <- BASIC; repeat rewrite Pregmap.gso; try (discriminate || reflexivity)).
-  - destruct i; simpl in BASIC; destruct is;
-      try (unfold compare_int in BASIC || unfold compare_long in BASIC);
-      try (rewrite <- BASIC; repeat rewrite Pregmap.gso; try (discriminate || reflexivity)).
+  - destruct i; simpl in BASIC;
+    unfold compare_long in BASIC; rewrite <- BASIC;
+    repeat rewrite Pregmap.gso; try discriminate; reflexivity.
+  - destruct i; simpl in BASIC. 
+    1,2: rewrite <- BASIC; repeat rewrite Pregmap.gso; try discriminate; reflexivity.
+    destruct sz;
+    try (unfold compare_single in BASIC || unfold compare_float in BASIC);
+    destruct (rs r1), (rs r2);
+    try (rewrite <- BASIC; repeat rewrite Pregmap.gso; try (discriminate || reflexivity)).
+  - destruct i; simpl in BASIC;
+    destruct is;
+    try (unfold compare_int in BASIC || unfold compare_long in BASIC);
+    try (rewrite <- BASIC; repeat rewrite Pregmap.gso; try (discriminate || reflexivity)).
   - destruct i; simpl in BASIC; destruct sz;
     try (unfold compare_single in BASIC || unfold compare_float in BASIC);
     destruct (rs r1);
@@ -1259,7 +1260,28 @@ Proof.
   destruct bi.
   { (* PArith *)
     simpl in *; destruct i.
-    1,2,3,4,5,6: (* PArithP, PArithPP, PArithPPP, PArithRR0R, PArithRR0, PArithARRRR0 *)
+    1: {
+      destruct i.
+      1,2,3: 
+        try (destruct sumbool_rec; try congruence);
+        try (monadInv TRANSBI);
+        try (destruct_reg_inv);
+        try (inv_matchi);
+        try (exploit next_inst_preserved; eauto);
+        try (repeat destruct_reg_size);
+        try (destruct_ir0_reg).
+      1,2: (* Special case for Pfmovimmd / Pfmovimms *)
+        try (monadInv TRANSBI);
+        try (destruct_reg_inv);
+        try (inv_matchi);
+        inversion BASIC; clear BASIC; subst;
+        eexists; eexists; split; eauto;
+        repeat (eapply match_internal_nextinstr_set_parallel; try congruence);
+        try (econstructor; eauto);
+        try (eapply nextinstr_agree_but_pc; eauto);
+        try (eapply ptrofs_nextinstr_agree; eauto).
+    }
+    1,2,3,4,5: (* PArithP, PArithPP, PArithPPP, PArithRR0R, PArithRR0, PArithARRRR0 *)
       destruct i;
       try (destruct sumbool_rec; try congruence);
       try (monadInv TRANSBI);