cfi_simu finished

1 files changed, 36 insertions, 15 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index df83e6a7..833c6f03 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -1815,21 +1815,42 @@ Proof.
     destruct b.
     * exploit next_inst_incr_pc_preserved; eauto.
     * exploit goto_label_preserved; eauto.
-      (*  - (* Pbtbl *)
-    simpl; eexists; eexists; split.
-    + rewrite <- H0.
-      assert (  rs2 # X16 <- Vundef r1
-             = (incrPC (Ptrofs.repr size_b) rs1) # X16 <- Vundef r1
-             ) as EQUNDEFX16. {
-        unfold incrPC, Pregmap.set.
-        destruct (PregEq.eq r1 X16) as [X16 | X16]; auto.
-        destruct (PregEq.eq r1 PC) as [PC' | PC']; try discriminate.
-        inv MI; rewrite AG; auto.
-      } rewrite <- EQUNDEFX16.
-      (* TODO Asm.goto_label and goto_label *) admit.
-    + constructor.
-*)
-Admitted.
+  - (* Pbtbl *)
+    assert (rs2 # X16 <- Vundef r1 = (incrPC (Ptrofs.repr (size bb)) rs1) # X16 <- Vundef r1)
+    as EQUNDEFX16. {
+      unfold incrPC, Pregmap.set.
+      destruct (PregEq.eq r1 X16) as [X16 | X16]; auto.
+      destruct (PregEq.eq r1 PC) as [PC' | PC']; try discriminate.
+      inv MATCHI; rewrite AG; auto.
+    } rewrite <- EQUNDEFX16 in H0.
+    destruct_reg_inv; next_stuck_cong.
+    unfold goto_label, Asm.goto_label in *.
+    rewrite <- (label_pos_preserved f); auto.
+    inversion MATCHI; subst.
+    destruct label_pos; next_stuck_cong.
+    destruct (((incrPC (Ptrofs.repr (size bb)) rs1) # X16 <- Vundef) # X17 <- Vundef PC) eqn:INCRPC; next_stuck_cong.
+    inversion H0; auto. repeat (econstructor; eauto).
+    rewrite !Pregmap.gso; try congruence.
+    rewrite <- AGPC.
+    unfold incrPC in *.
+    destruct (rs1 PC) eqn:EQRS1; simpl in *; try discriminate.
+    replace (((rs2 # X16 <- Vundef) # X17 <- Vundef) # PC <- (Vptr b0 (Ptrofs.repr z))) with
+      ((((rs1 # PC <- (Vptr b0 (Ptrofs.add i1 (Ptrofs.repr (size bb))))) # X16 <-
+      Vundef) # X17 <- Vundef) # PC <- (Vptr b (Ptrofs.repr z))); auto.
+    eapply functional_extensionality; intros x.
+    destruct (PregEq.eq x PC); subst.
+    + rewrite Pregmap.gso in INCRPC; try congruence.
+      rewrite Pregmap.gso in INCRPC; try congruence.
+      rewrite Pregmap.gss in INCRPC.
+      rewrite !Pregmap.gss in *; congruence.
+    + rewrite Pregmap.gso; auto.
+      rewrite (Pregmap.gso (i := x) (j := PC)); auto.
+      destruct (PregEq.eq x X17); subst.
+      * rewrite !Pregmap.gss; auto.
+      * rewrite !(Pregmap.gso (i := x) (j:= X17)); auto. destruct (PregEq.eq x X16); subst.
+        -- rewrite !Pregmap.gss; auto.
+        -- rewrite !Pregmap.gso; auto.
+Qed.
 
 Lemma last_instruction_cannot_be_label bb:
   list_nth_z (header bb) (size bb - 1) = None.