Pb, Pbc, and nextinst incrPC preserved lemma

1 files changed, 79 insertions, 41 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 895e354a..c89a4320 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -1620,6 +1620,72 @@ Proof.
   exploit list_nth_z_range; eauto. omega.
 Qed.
 
+Lemma basic_block_header_length: forall bb,
+  (length (header bb) <= 1)%nat.
+Proof.
+Admitted.
+
+Lemma label_pos_preserved f lbl z tf: forall
+  (FINDF: transf_function f = OK tf),
+  label_pos lbl z (fn_blocks f) = Asm.label_pos lbl z (Asm.fn_code tf).
+Proof.
+Admitted.
+
+Lemma goto_label_preserved bb rs1 m1 rs1' m1' rs2 m2 lbl f tf v: forall
+  (FINDF: transf_function f = OK tf)
+  (BOUNDED: size bb <= Ptrofs.max_unsigned)
+  (MATCHI: match_internal (size bb - 1) (State rs1 m1) (State rs2 m2))
+  (HGOTO: goto_label f lbl (incrPC v rs1) m1 = Next rs1' m1'),
+  exists (rs2' : regset) (m2' : mem), Asm.goto_label tf lbl rs2 m2 = Next rs2' m2'
+  /\ match_states (State rs1' m1') (State rs2' m2').
+Proof.
+  intros.
+  unfold goto_label, Asm.goto_label in *.
+  rewrite <- (label_pos_preserved f); auto.
+  inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst.
+  destruct label_pos; next_stuck_cong.
+  destruct (incrPC v rs1 PC) eqn:INCRPC; next_stuck_cong.
+  inversion HGOTO; auto. repeat (econstructor; eauto).
+  rewrite <- EQPC.
+  unfold incrPC in *.
+  rewrite !Pregmap.gss in *.
+  destruct (rs1 PC) eqn:EQRS1; simpl in *; try congruence.
+  replace (rs2 # PC <- (Vptr b0 (Ptrofs.repr z))) with ((rs1 # PC <- (Vptr b0 (Ptrofs.add i0 v))) # PC <- (Vptr b (Ptrofs.repr z))); auto.
+  eapply functional_extensionality. intros.
+  destruct (PregEq.eq x PC); subst.
+  rewrite !Pregmap.gss. congruence.
+  rewrite !Pregmap.gso; auto.
+Qed.
+
+Lemma next_inst_incr_pc_preserved bb rs1 m1 rs1' m1' rs2 m2 f tf: forall
+  (FINDF: transf_function f = OK tf)
+  (BOUNDED: size bb <= Ptrofs.max_unsigned)
+  (MATCHI: match_internal (size bb - 1) (State rs1 m1) (State rs2 m2))
+  (NEXT: Next (incrPC (Ptrofs.repr (size bb)) rs1) m2 = Next rs1' m1'),
+  exists (rs2' : regset) (m2' : mem), 
+  Next (Asm.nextinstr rs2) m2 = Next rs2' m2'
+  /\ match_states (State rs1' m1') (State rs2' m2').
+Proof.
+  intros; simpl in *; unfold incrPC in NEXT;
+  inv_matchi;
+  assert (size bb >= 1) by eapply bblock_size_pos;
+  assert (0 <= size bb - 1 <= Ptrofs.max_unsigned) by omega;
+  inversion NEXT; subst;
+  eexists; eexists; split; eauto.
+  assert (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size bb))) = Asm.nextinstr rs2). {
+    unfold Pregmap.set. apply functional_extensionality.
+    intros x. destruct (PregEq.eq x PC).
+    -- unfold Asm.nextinstr. rewrite <- AGPC.
+       rewrite Val.offset_ptr_assoc. rewrite Ptrofs.add_unsigned.
+       rewrite (Ptrofs.unsigned_repr (size bb - 1)); try omega.
+       rewrite Ptrofs.unsigned_one.
+       replace (size bb - 1 + 1) with (size bb) by omega.
+       rewrite e. rewrite Pregmap.gss.
+       reflexivity.
+    -- eapply nextinstr_agree_but_pc; eauto. }
+       rewrite H1. econstructor.
+Qed.
+
 Lemma exec_cfi_simulation:
   forall bb f tf rs1 m1 rs1' m1' rs2 m2 cfi
   (SIZE: size bb <= Ptrofs.max_unsigned)
@@ -1634,10 +1700,19 @@ Proof.
   intros.
   destruct cfi; inv CFI; simpl.
   - (* Pb *)
-    (*eexists; eexists; split.*)
-    (*eauto.*)
-    admit.
-  - (* Pbc *) admit.
+    exploit goto_label_preserved; eauto.
+  - (* Pbc *)
+    inv_matchi.
+    unfold eval_testcond in *. destruct c;
+    erewrite !incrPC_agree_but_pc in H0; try rewrite <- !AG; try congruence.
+    all:
+      destruct_reg_size;
+      try destruct b eqn:EQB.
+      1,4,7,10,13,16,19,22,25,28,31,34:
+        exploit goto_label_preserved; eauto.
+      1,3,5,7,9,11,13,15,17,19,21,23:
+        exploit next_inst_incr_pc_preserved; eauto.
+      all: repeat (econstructor; eauto).
   - (* Pbl *)
     eexists; eexists; split.
     + eauto.
@@ -1774,43 +1849,6 @@ Proof.
 *)
 Admitted.
 
-Lemma basic_block_header_length: forall bb,
-  (length (header bb) <= 1)%nat.
-Proof.
-Admitted.
-
-Lemma label_pos_preserved f lbl z tf: forall
-  (FINDF: transf_function f = OK tf),
-  label_pos lbl z (fn_blocks f) = Asm.label_pos lbl z (Asm.fn_code tf).
-Proof.
-Admitted.
-
-Lemma goto_label_preserved bb rs1 m1 rs1' m1' rs2 m2 lbl f tf v: forall
-  (FINDF: transf_function f = OK tf)
-  (BOUNDED: size bb <= Ptrofs.max_unsigned)
-  (MATCHI: match_internal (size bb - 1) (State rs1 m1) (State rs2 m2))
-  (HGOTO: goto_label f lbl (incrPC v rs1) m1 = Next rs1' m1'),
-  exists (rs2' : regset) (m2' : mem), Asm.goto_label tf lbl rs2 m2 = Next rs2' m2'
-  /\ match_states (State rs1' m1') (State rs2' m2').
-Proof.
-  intros.
-  unfold goto_label, Asm.goto_label in *.
-  rewrite <- (label_pos_preserved f); auto.
-  inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst.
-  destruct label_pos; next_stuck_cong.
-  destruct (incrPC v rs1 PC) eqn:INCRPC; next_stuck_cong.
-  inversion HGOTO; auto. repeat (econstructor; eauto).
-  rewrite <- EQPC.
-  unfold incrPC in *.
-  rewrite !Pregmap.gss in *.
-  destruct (rs1 PC) eqn:EQRS1; simpl in *; try congruence.
-  replace (rs2 # PC <- (Vptr b0 (Ptrofs.repr z))) with ((rs1 # PC <- (Vptr b0 (Ptrofs.add i0 v))) # PC <- (Vptr b (Ptrofs.repr z))); auto.
-  eapply functional_extensionality. intros.
-  destruct (PregEq.eq x PC); subst.
-  rewrite !Pregmap.gss. congruence.
-  rewrite !Pregmap.gso; auto.
-Qed.
-
 Lemma last_instruction_cannot_be_label bb:
   list_nth_z (header bb) (size bb - 1) = None.
 Proof.