Some subcases for exec_basic_simu

- Ploadsymbol
- Pcvtsw2x
- Pcvtuw2x
- Pcvtx2w
- First subcase for PArithCompPP

1 files changed, 49 insertions, 86 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 81c1bbbc..8003b975 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -1072,6 +1072,7 @@ Ltac destruct_reg_size :=
   end.
 
 Ltac find_rwrt_ag :=
+  simpl in *;
   match goal with
   | [ AG: forall r, r <> ?PC -> _ r = _ r |- _ ]
       => repeat rewrite <- AG; try congruence
@@ -1177,77 +1178,29 @@ Proof.
       try (destruct_reg_size);
       try (destruct_ir0_reg).
     + (* PArithComparisonPP *)
-      destruct i;
+      destruct i.
+      {
       try (monadInv TRANSBI);
       try (inv_matchi);
-      try (destruct_reg_inv);
-      simpl in *;
-      inversion BASIC; clear BASIC; subst;
-       eexists; eexists; split; eauto;
+      try (destruct_reg_inv).
+      simpl in *.
+      inversion BASIC; clear BASIC; subst.
+      eexists; eexists; split; eauto.
+      unfold compare_long.
+      repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]).
+      econstructor; eauto.
+      * intros. unfold Asm.nextinstr.
+        rewrite Pregmap.gso; eauto.
+      * unfold Asm.nextinstr. rewrite Pregmap.gss.
+        rewrite <- Ptrofs.unsigned_one. rewrite <- (Ptrofs.unsigned_repr n); eauto.
+        rewrite <- Ptrofs.add_unsigned. rewrite <- Val.offset_ptr_assoc. rewrite AGPC; eauto.
+      }
+
+
+
       unfold compare_long, compare_int, compare_float, compare_single;
       repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]).
-      all: admit.
-      (*-- try (monadInv TRANSBI).*)
-         (*[>try (inv_matchi).<]*)
-         (*[>try (destruct_reg_inv).<]*)
-         (*[>try (exploit next_inst_preserved; eauto);<]*)
-
-         (*simpl in *. inversion MATCHI; subst.*)
-         (*inversion BASIC. repeat (econstructor; eauto).*)
-          (** intros. unfold Asm.nextinstr, compare_long.*)
-            (*rewrite (Pregmap.gso (i := r) (j := PC)); try congruence.*)
-            (*rewrite (Pregmap.gso (i := r) (j := CV)); try congruence.*)
-            (*destruct (PregEq.eq r CV).*)
-            (*{ *)
-              (*subst. rewrite !Pregmap.gss.*)
-              (*rewrite (Pregmap.gso (i := CV) (j := CC)).*)
-              (*destruct (PregEq.eq CV CC).*)
-              (*{ *)
-                (*rewrite Pregmap.gso.*)
-                (*destruct (PregEq.eq CV CZ).*)
-                (*{*)
-                  (*rewrite Pregmap.gso.*)
-                  (*destruct (PregEq.eq CV CN).*)
-                  (*{*)
-                    (*unfold Val.subl_overflow.*)
-                    (*destruct (rs2 x0); try congruence.*)
-                  (*}*)
-                  (*{*)
-                    (*unfold Val.subl_overflow.*)
-                    (*destruct (rs2 x0); try congruence.*)
-                  (*}*)
-                  (*{ *)
-                    (*try congruence.*)
-                  (*}*)
-                (*}*)
-                (*{ rewrite !Pregmap.gso; try congruence. }*)
-                (*{ try congruence. }*)
-              (*}*)
-              (*{ *)
-                (*rewrite Pregmap.gso.*)
-                (*destruct (PregEq.eq CV CZ).*)
-                (*{*)
-                  (*rewrite Pregmap.gso.*)
-                  (*destruct (PregEq.eq CV CN).*)
-                  (*{*)
-                    (*unfold Val.subl_overflow.*)
-                    (*destruct (rs2 x0); try congruence.*)
-                  (*}*)
-                  (*{*)
-                    (*unfold Val.subl_overflow.*)
-                    (*destruct (rs2 x0); try congruence.*)
-                  (*}*)
-                  (*{ *)
-                    (*try congruence.*)
-                  (*}*)
-                (*}*)
-                (*{ *)
-                  (*rewrite !Pregmap.gso; try congruence.*)
-                  (*unfold Val.subl_overflow.*)
-                  (*destruct (rs2 x0); try congruence.*)
-                (*}*)
-                (*{ try congruence. }*)
-              (*}*)
+
       all:admit.
     + (* PArithComparisonR0R *)
       all:admit.
@@ -1289,30 +1242,40 @@ Proof.
   - (* Pallocframe *)
     monadInv TRANSBI.
     simpl in *.
-
-    inv_matchi.
-    simpl in *.
+    inversion MATCHI; subst.
+    destruct Mem.alloc.
     inversion BASIC. repeat (econstructor; eauto).
-    destruct (Mem.alloc m2 0 sz).
-    unfold Asm.nextinstr.
-    rewrite !Pregmap.gso; try congruence.
-    destruct (PregEq.eq SP PC).
-    { rewrite e in *.
-      rewrite <- AGPC. 
-      rewrite Val.offset_ptr_assoc.
-      (*rewrite <- Ptrofs.unsigned_one. rewrite <- (Ptrofs.unsigned_repr n); eauto.*)
-      rewrite (Ptrofs.add_unsigned (Ptrofs.repr n) (Ptrofs.one)). rewrite Ptrofs.unsigned_one.
-      rewrite Ptrofs.unsigned_repr.
-      unfold Next.
+    unfold Asm.nextinstr. rewrite <- AG.
+    destruct (Mem.store _ _ _ _ _); try congruence; eauto.
+      
     (* TODO *)
     all:admit.
-
-
-  all:admit.
+  - (* Pfreeframe *)
+    (* TODO seems similar as the above subcase *)
+    all:admit.
+  - (* Ploadsymbol *)
+    try (monadInv TRANSBI);
+    try (inv_matchi);
+    try (exploit next_inst_preserved; eauto);
+    simpl in *;
+    rewrite symbol_addresses_preserved; eauto.
+  - (* Pcvtsw2x *)
+    try (monadInv TRANSBI);
+    try (inv_matchi);
+    try (exploit next_inst_preserved; eauto);
+    try (find_rwrt_ag).
+  - (* Pcvtuw2x *)
+    try (monadInv TRANSBI);
+    try (inv_matchi);
+    try (exploit next_inst_preserved; eauto);
+    try (find_rwrt_ag).
+  - (* Pcvtx2w *)
+    try (monadInv TRANSBI);
+    try (inv_matchi);
+    try (exploit next_inst_preserved; eauto);
+    try (find_rwrt_ag).
 Admitted.
 
-
-
 Lemma exec_body_simulation_star': forall
   b ofs f bb tc bis end_of_body rs_start m_start s_start rs_end m_end
   (ATPC: rs_start PC = Vptr b ofs)