PArithComp subcases OK

1 files changed, 75 insertions, 110 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 173ce8f8..f0350628 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -1027,6 +1027,12 @@ Ltac destruct_ir0_reg :=
       => unfold ir0 in *; destruct r; find_rwrt_ag; eauto
   end.
 
+Ltac pc_not_sp :=
+  match goal with
+  | [ |- ?PC <> ?SP ]
+      => destruct (PregEq.eq SP PC); repeat congruence; discriminate
+  end.
+
 Ltac update_x_access_x :=
   subst; rewrite !Pregmap.gss; auto.
 
@@ -1143,91 +1149,52 @@ Lemma exec_basic_simulation:
 Proof.
   intros.
   destruct bi.
-  - (* PArith *)
+  { (* PArith *)
     simpl in *; destruct i.
-    + (* PArithP *)
-      destruct i;
-      try (monadInv TRANSBI);
-      try (destruct_reg_inv);
-      exploit next_inst_preserved; eauto;
-      try (destruct_reg_size).
-    + (* PArithPP *)
+    1,2,3,4,5,6: (* PArithP, PArithPP, PArithPPP, PArithRR0R, PArithRR0, PArithARRRR0 *)
       destruct i;
       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).
-    + (* PArithPPP *)
-      destruct i;
-      try (monadInv TRANSBI);
-      try (destruct_reg_inv);
-      try (inv_matchi);
-      try (exploit next_inst_preserved; eauto);
-      try (destruct_reg_size).
-    + (* PArithRR0R *)
-      destruct i;
-      try (monadInv TRANSBI);
-      try (inv_matchi);
-      try (exploit next_inst_preserved; eauto);
-      try (destruct_reg_size);
-      try (destruct_ir0_reg).
-    + (* PArithRR0 *)
-      destruct i;
-      try (monadInv TRANSBI);
-      try (inv_matchi);
-      try (exploit next_inst_preserved; eauto);
-      try (destruct_reg_size);
-      try (destruct_ir0_reg).
-    + (* PArithARRRR0 *)
-      destruct i;
-      try (monadInv TRANSBI);
-      try (inv_matchi);
-      try (exploit next_inst_preserved; eauto);
-      try (destruct_reg_size);
+      try (repeat destruct_reg_size);
       try (destruct_ir0_reg).
-    + (* PArithComparisonPP *)
-      destruct i;
-      try (monadInv TRANSBI);
-      try (inv_matchi);
-      try (destruct_reg_inv);
-      simpl in *;
-      inversion BASIC; clear BASIC; subst;
-      eexists; eexists; split; eauto;
-      unfold compare_long, compare_int, compare_float, compare_single;
-      try (destruct_reg_size);
-      try (destruct_reg_size);
-      try (destruct_reg_size);
-      repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]);
-      try (econstructor; eauto);
-      try (eapply nextinstr_agree_but_pc; eauto);
-      try (eapply ptrofs_nextinstr_agree; eauto).
-      (* TODO find a solution to avoid destructing a lot of subcases *)
-           (** destruct sz.*)
-             (*{ [> Vsingle <]*)
-              (*try (exploit next_inst_preserved; eauto). intros.*)
-               (*destruct (rs1 x).*)
-               (*unfold Asm.nextinstr.*)
-               (*inversion MATCHI.*)
-             (*}*)
-      all:admit.
-    + (* PArithComparisonR0R *)
+    { (* PArithComparisonPP *)
       destruct i;
       try (monadInv TRANSBI);
       try (inv_matchi);
       try (destruct_reg_inv);
-      try (destruct_reg_size);
-      simpl in *;
-      inversion BASIC; clear BASIC; subst;
-      eexists; eexists; split; eauto;
-      unfold compare_long, compare_int, compare_float, compare_single;
-      repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]);
-      try (econstructor; eauto);
-      try (destruct_ir0_reg);
-      try (eapply nextinstr_agree_but_pc; eauto);
-      try (eapply ptrofs_nextinstr_agree; eauto).
-    + (* PArithComparisonP *)
+      simpl in *.
+      1,2: (* compare_long *)
+        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)]);
+        try (econstructor; eauto);
+        try (eapply nextinstr_agree_but_pc; eauto);
+        try (eapply ptrofs_nextinstr_agree; eauto).
+
+      destruct sz.
+      - (* compare_single *)
+        unfold compare_single in BASIC.
+        destruct (rs1 x), (rs1 x0);
+        inversion BASIC;
+        eexists; eexists; split; eauto;
+        repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]);
+        try (econstructor; eauto);
+        try (eapply nextinstr_agree_but_pc; eauto);
+        try (eapply ptrofs_nextinstr_agree; eauto).
+      - (* compare_float *)
+        unfold compare_float in BASIC.
+        destruct (rs1 x), (rs1 x0);
+        inversion BASIC;
+        eexists; eexists; split; eauto;
+        repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]);
+        try (econstructor; eauto);
+        try (eapply nextinstr_agree_but_pc; eauto);
+        try (eapply ptrofs_nextinstr_agree; eauto). }
+    1,2: (* PArithComparisonR0R, PArithComparisonP *)
       destruct i;
       try (monadInv TRANSBI);
       try (inv_matchi);
@@ -1240,22 +1207,23 @@ Proof.
       try (destruct_reg_size);
       repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]);
       try (econstructor; eauto);
+      try (destruct_ir0_reg);
       try (eapply nextinstr_agree_but_pc; eauto);
       try (eapply ptrofs_nextinstr_agree; eauto).
-    + (* Pcset *)
+    { (* Pcset *)
       try (monadInv TRANSBI);
-      try (inv_matchi);
+      try (inv_matchi).
       try (exploit next_inst_preserved; eauto);
-      simpl in *; intros;
+      try (simpl in *; intros;
       unfold if_opt_bool_val in *; unfold eval_testcond in *;
-      rewrite <- !AG; try congruence; eauto.
-    + (* Pfmovi *)
+      rewrite <- !AG; try congruence; eauto). }
+    { (* Pfmovi *)
       try (monadInv TRANSBI);
       try (inv_matchi);
       try (destruct_reg_size);
       try (destruct_ir0_reg);
-      try (exploit next_inst_preserved; eauto).
-    + (* Pcsel *)
+      try (exploit next_inst_preserved; eauto). }
+    { (* Pcsel *)
       try (destruct_reg_inv);
       try (monadInv TRANSBI);
       try (destruct_reg_inv);
@@ -1263,20 +1231,20 @@ Proof.
       try (exploit next_inst_preserved; eauto);
       simpl in *; intros;
       unfold if_opt_bool_val in *; unfold eval_testcond in *;
-      rewrite <- !AG; try congruence; eauto.
-    + (* Pfnmul *)
+      rewrite <- !AG; try congruence; eauto. }
+    { (* Pfnmul *)
       try (monadInv TRANSBI);
       try (inv_matchi);
       try (destruct_reg_size);
       try (exploit next_inst_preserved; eauto);
-      try (find_rwrt_ag).
-  - (* PLoad *)
+      try (find_rwrt_ag). } }
+  { (* PLoad *)
     destruct ld; monadInv TRANSBI; try destruct_ireg_inv; exploit load_preserved; eauto;
-    intros; simpl in *; destruct sz; eauto.
-  - (* PStore *)
+    intros; simpl in *; destruct sz; eauto. }
+  { (* PStore *)
     destruct st; monadInv TRANSBI; try destruct_ireg_inv; exploit store_preserved; eauto;
-    simpl in *; inv_matchi; find_rwrt_ag.
-  - (* Pallocframe *)
+    simpl in *; inv_matchi; find_rwrt_ag. }
+  { (* Pallocframe *)
     monadInv TRANSBI.
     simpl in *.
     inversion MATCHI; subst;
@@ -1287,36 +1255,33 @@ Proof.
     (* TODO find a way to complete this proof *)
     + eexists; eexists; split; eauto.
       repeat (eapply match_internal_nextinstr_set_parallel; [ try congruence | idtac | try reflexivity ]).
-      destruct (PregEq.eq SP PC); try (repeat congruence); discriminate.
-      -- admit.
-      -- eapply AG; destruct (PregEq.eq SP PC); try (repeat congruence); discriminate.
+      pc_not_sp.
+      -- econstructor; eauto.
+         all:admit.
+      -- eapply AG; pc_not_sp.
     + repeat (econstructor; eauto).
       admit.
       
     (* TODO *)
-    all:admit.
-  - (* Pfreeframe *)
+    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);
-    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 *)
+    monadInv TRANSBI.
+    simpl in *.
+    inversion MATCHI; subst;
+    destruct Mem.loadv in BASIC;
+    inversion BASIC; subst; clear BASIC.
+    destruct Mem.loadv.
+    (* TODO find a way to complete this proof *)
+    + eexists; eexists; split; eauto.
+      repeat (eapply match_internal_nextinstr_set_parallel; [ try congruence | idtac | try reflexivity ]).
+      all:admit.
+    + all:admit. }
+  1,2,3,4: (* Ploadsymbol, Pcvtsw2x, Pcvtuw2x, Pcvtx2w *)
     try (monadInv TRANSBI);
     try (inv_matchi);
     try (exploit next_inst_preserved; eauto);
+    rewrite symbol_addresses_preserved; eauto;
     try (find_rwrt_ag).
 Admitted.