Some subcases for exec cfi simu

1 files changed, 68 insertions, 95 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 7862e9a6..089514cd 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -1664,6 +1664,7 @@ Lemma exec_cfi_simulation:
                    /\ match_states (State rs1' m1') (State rs2' m2').
 Proof.
   intros.
+  assert (BBPOS: size bb >= 1) by eapply bblock_size_pos.
   destruct cfi; inv CFI; simpl.
   - (* Pb *)
     exploit goto_label_preserved; eauto.
@@ -1680,106 +1681,78 @@ Proof.
         exploit next_inst_incr_pc_preserved; eauto.
       all: repeat (econstructor; eauto).
   - (* Pbl *)
-    eexists; eexists; split.
-    + eauto.
-    + assert ( ((incrPC (Ptrofs.repr (size bb)) rs1) # X30 <- (incrPC (Ptrofs.repr (size bb)) rs1 PC))
-                                                     # PC <-  (Genv.symbol_address ge id Ptrofs.zero)
-             = (rs2 # X30 <- (Val.offset_ptr (rs2 PC) Ptrofs.one))
-                             # PC <- (Genv.symbol_address tge id Ptrofs.zero)
-             ) as EQRS. {
-        unfold incrPC. unfold Pregmap.set. simpl. apply functional_extensionality.
-        intros x. destruct (PregEq.eq x PC).
-        * rewrite symbol_addresses_preserved. reflexivity.
-        * destruct (PregEq.eq x X30).
-          -- inv MATCHI. rewrite <- AGPC. rewrite Val.offset_ptr_assoc.
-             unfold Ptrofs.add, Ptrofs.one. repeat (rewrite Ptrofs.unsigned_repr).
-             ++ replace (size bb - 1 + 1) with (size bb) by omega. reflexivity.
-             ++ split; try omega. apply one_le_max_unsigned.
-             ++ generalize (bblock_size_pos bb); omega.
-          -- inv MATCHI; rewrite AG; try assumption; reflexivity.
-      } rewrite EQRS; inv MATCHI; reflexivity.
+    eexists; eexists; split; eauto.
+    assert ( ((incrPC (Ptrofs.repr (size bb)) rs1) # X30 <- (incrPC (Ptrofs.repr (size bb)) rs1 PC))
+                                                   # PC <-  (Genv.symbol_address ge id Ptrofs.zero)
+           = (rs2 # X30 <- (Val.offset_ptr (rs2 PC) Ptrofs.one))
+                           # PC <- (Genv.symbol_address tge id Ptrofs.zero)
+           ) as EQRS. {
+      unfold incrPC. unfold Pregmap.set. simpl. apply functional_extensionality.
+      intros x. destruct (PregEq.eq x PC).
+      * rewrite symbol_addresses_preserved. reflexivity.
+      * destruct (PregEq.eq x X30).
+        -- inv MATCHI. rewrite <- AGPC. rewrite Val.offset_ptr_assoc.
+           unfold Ptrofs.add, Ptrofs.one. repeat (rewrite Ptrofs.unsigned_repr); try omega.
+           replace (size bb - 1 + 1) with (size bb) by omega. reflexivity.
+        -- inv MATCHI; rewrite AG; try assumption; reflexivity.
+    } rewrite EQRS; inv MATCHI; reflexivity.
   - (* Pbs *)
-    eexists; eexists; split.
-    + eauto.
-    + assert ( (incrPC (Ptrofs.repr (size bb)) rs1) # PC <-
-                             (Genv.symbol_address ge id Ptrofs.zero)
-             = rs2 # PC <- (Genv.symbol_address tge id Ptrofs.zero)
-             ) as EQRS. {
-        unfold incrPC, Pregmap.set. rewrite symbol_addresses_preserved. inv MATCHI.
-        apply functional_extensionality. intros x. destruct (PregEq.eq x PC); auto.
-      } rewrite EQRS; inv MATCHI; reflexivity.
-(*
+    eexists; eexists; split; eauto.
+    assert ( (incrPC (Ptrofs.repr (size bb)) rs1) # PC <-
+                           (Genv.symbol_address ge id Ptrofs.zero)
+           = rs2 # PC <- (Genv.symbol_address tge id Ptrofs.zero)
+           ) as EQRS. {
+      unfold incrPC, Pregmap.set. rewrite symbol_addresses_preserved. inv MATCHI.
+      apply functional_extensionality. intros x. destruct (PregEq.eq x PC); auto.
+    } rewrite EQRS; inv MATCHI; reflexivity.
   - (* Pblr *)
-    simpl; eexists; eexists; split.
-    + rewrite <- H0.
-      unfold incrPC. rewrite Pregmap.gss. rewrite Pregmap.gso; try discriminate.
-      assert ( (rs2 # X30 <- (Val.offset_ptr (rs2 PC) Ptrofs.one)) # PC <- (rs2 r)
-             = ((rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b)))
-                     # X30 <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b)))
-                     # PC <- (rs1 r)
-             ) as EQRS. {
-        unfold Pregmap.set. apply functional_extensionality.
-        intros x; destruct (PregEq.eq x PC) as [X | X].
-        - inv MI; rewrite AG; auto. discriminate.
-        - destruct (PregEq.eq x X30) as [X' | X'].
-          + inv MI. rewrite <- AGPC.
-            rewrite Val.offset_ptr_assoc. unfold Ptrofs.one.
-            rewrite Ptrofs.add_unsigned. rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr.
-            rewrite Z.sub_add; reflexivity.
-            * split; try omega. apply one_le_max_unsigned.
-            * split; try omega.
-              (* TODO size_b - 1 <= Ptrofs.max_unsigned needs extra hypothesis *) admit.
-          + inv MI; rewrite AG; auto.
-      } rewrite EQRS. inv MI; auto.
-    + constructor.
+    eexists; eexists; split; eauto.
+    unfold incrPC. rewrite Pregmap.gss. rewrite Pregmap.gso; try discriminate.
+    assert ( (rs2 # X30 <- (Val.offset_ptr (rs2 PC) Ptrofs.one)) # PC <- (rs2 r)
+           = ((rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size bb))))
+                   # X30 <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size bb))))
+                   # PC <- (rs1 r)
+           ) as EQRS. {
+      unfold Pregmap.set. apply functional_extensionality.
+      intros x; destruct (PregEq.eq x PC) as [X | X].
+      - inv_matchi; rewrite AG; auto.
+      - destruct (PregEq.eq x X30) as [X' | X'].
+        + inversion MATCHI; subst. rewrite <- AGPC.
+          rewrite Val.offset_ptr_assoc. unfold Ptrofs.one.
+          rewrite Ptrofs.add_unsigned. rewrite Ptrofs.unsigned_repr; try omega. rewrite Ptrofs.unsigned_repr; try omega.
+          rewrite Z.sub_add; reflexivity.
+        + inv_matchi.
+    } rewrite EQRS. inv_matchi.
   - (* Pbr *)
-    simpl; eexists; eexists; split.
-    + rewrite <- H0.
-      unfold incrPC. rewrite Pregmap.gso; try discriminate.
-      assert (  rs2 # PC <- (rs2 r)
-             = (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b)))
-                    # PC <- (rs1 r)
-             ) as EQRS. {
-        unfold Pregmap.set; apply functional_extensionality.
-        intros x; destruct (PregEq.eq x PC) as [X | X]; try discriminate.
-        - inv MI; rewrite AG; try discriminate. reflexivity.
-        - inv MI; rewrite AG; auto.
-      } rewrite EQRS; inv MI; auto.
-    + constructor.
+    eexists; eexists; split; eauto.
+    unfold incrPC. rewrite Pregmap.gso; try discriminate.
+    assert (  rs2 # PC <- (rs2 r)
+           = (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size bb))))
+                  # PC <- (rs1 r)
+           ) as EQRS. {
+      unfold Pregmap.set; apply functional_extensionality.
+      intros x; destruct (PregEq.eq x PC) as [X | X]; try discriminate; inv_matchi. }
+      rewrite EQRS; inv_matchi.
   - (* Pret *)
-    simpl; eexists; eexists; split.
-    + rewrite <- H0.
-      unfold incrPC. rewrite Pregmap.gso; try discriminate.
-      assert (  rs2 # PC <- (rs2 r)
-             = (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b))) # PC <- (rs1 r)
-             ) as EQRS. {
-        unfold Pregmap.set; apply functional_extensionality.
-        intros x; destruct (PregEq.eq x PC) as [X | X]; try discriminate.
-        - inv MI; rewrite AG; try discriminate. reflexivity.
-        - inv MI; rewrite AG; auto.
-      } rewrite EQRS; inv MI; auto.
-    + constructor.
+    eexists; eexists; split; eauto.
+    unfold incrPC. rewrite Pregmap.gso; try discriminate.
+    assert (  rs2 # PC <- (rs2 r)
+           = (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size bb)))) # PC <- (rs1 r)
+           ) as EQRS. {
+      unfold Pregmap.set; apply functional_extensionality.
+      intros x; destruct (PregEq.eq x PC) as [X | X]; try discriminate; inv_matchi. }
+    rewrite EQRS; inv_matchi.
   - (* Pcbnz *)
-    simpl; eexists; eexists; split.
-    + rewrite <- H0.
-      unfold eval_neg_branch. destruct sz.
-      * simpl. inv MI. rewrite <- AG; try discriminate.
-        replace (incrPC (Ptrofs.repr size_b) rs1 r) with (rs1 r). 2: {
-          symmetry. rewrite incrPC_agree_but_pc; try discriminate; auto.
-        }
-        assert (Asm.nextinstr rs2 = (incrPC (Ptrofs.repr size_b) rs1)) as EQTrue. {
-          unfold incrPC, Asm.nextinstr, Ptrofs.one. rewrite <- AGPC.
-          rewrite Val.offset_ptr_assoc. rewrite Ptrofs.add_unsigned.
-          rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr.
-          - rewrite Z.sub_add; unfold Pregmap.set; apply functional_extensionality.
-            intros x; destruct (PregEq.eq x PC) as [ X | X ]; auto. rewrite AG; trivial.
-          - split; try omega. apply one_le_max_unsigned.
-          - split; try omega.
-            (* TODO size_b - 1 <= Ptrofs.max_unsigned needs extra hypothesis *) admit.
-        } rewrite EQTrue. fold Stuck.
-          (* TODO show that Asm.goto_label and goto_label behave the same *) admit.
-      * (* TODO see/merge above case *) admit.
-    + constructor.
+    inv_matchi.
+    unfold eval_neg_branch in *.
+    replace (incrPC (Ptrofs.repr (size bb)) rs1 r) with (rs1 r) in *. 2: {
+      symmetry. rewrite incrPC_agree_but_pc; try discriminate; auto.
+    }
+    destruct eval_testzero; try next_stuck_cong.
+    destruct b.
+    * exploit next_inst_incr_pc_preserved; eauto.
+    * exploit goto_label_preserved; eauto.
+      (*
   - (* Pcbz *)
     simpl; eexists; eexists; split.
     + rewrite <- H0.