New lemmas and subcases for cfi_simu

1 files changed, 68 insertions, 49 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 089514cd..87392139 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -1555,6 +1555,30 @@ Proof.
     apply f_equal2; auto. omega.
 Qed.
 
+Lemma asm_label_pos_header: forall z a x0 x1 lbl
+  (HUNF: unfold_body (body a) = OK x1),
+  Asm.label_pos lbl (z + size a) x0 =
+  Asm.label_pos lbl (z + list_length_z (header a)) ((x1 ++ unfold_exit (exit a)) ++ x0).
+Proof.
+  intros.
+  unfold size.
+  rewrite <- plus_assoc. rewrite Nat2Z.inj_add.
+  rewrite list_length_z_nat.
+  replace (z + (Z.of_nat (Datatypes.length (header a)) + Z.of_nat (Datatypes.length (body a) + length_opt (exit a)))) with (z + Z.of_nat (Datatypes.length (header a)) + Z.of_nat (Datatypes.length (body a) + length_opt (exit a))) by omega.
+  eapply (label_pos_body (body a) x0 x1 (z + Z.of_nat (Datatypes.length (header a))) (exit a) lbl). auto.
+Qed.
+
+Lemma header_size_cons_nil: forall (l0: label) (l1: list label)
+  (HSIZE: list_length_z (l0 :: l1) <= 1),
+  l1 = nil.
+Proof.
+  intros.
+  destruct l1 as [l2|l1]; try congruence. rewrite !list_length_z_cons in HSIZE.
+  assert (list_length_z l2 >= 0) by eapply list_length_z_pos.
+  assert (list_length_z l2 + 1 + 1 >= 2) by omega.
+  assert (2 <= 1) by omega. contradiction H1. omega.
+Qed.
+
 Lemma label_pos_preserved_gen bbs: forall lbl c z
   (HUNF: unfold bbs = OK c),
   label_pos lbl z bbs = Asm.label_pos lbl z c.
@@ -1567,22 +1591,13 @@ Proof.
     + erewrite label_in_header_list; eauto.
       simpl in *. destruct (peq lbl lbl); try congruence.
     + erewrite IHbbs; eauto.
-      assert (Asm.label_pos lbl (z + size a) x0 = Asm.label_pos lbl (z + list_length_z (header a)) ((x1 ++ unfold_exit (exit a)) ++ x0)).
-      { unfold size.
-        rewrite <- plus_assoc. rewrite Nat2Z.inj_add.
-        rewrite list_length_z_nat.
-        replace (z + (Z.of_nat (Datatypes.length (header a)) + Z.of_nat (Datatypes.length (body a) + length_opt (exit a)))) with (z + Z.of_nat (Datatypes.length (header a)) + Z.of_nat (Datatypes.length (body a) + length_opt (exit a))) by omega.
-        eapply (label_pos_body (body a) x0 x1 (z + Z.of_nat (Datatypes.length (header a))) (exit a) lbl). auto. }
+      rewrite (asm_label_pos_header z a x0 x1 lbl); auto.
       unfold is_label in *.
       destruct (header a).
-      * replace (z + list_length_z (@nil label)) with (z) in H; eauto.
+      * replace (z + list_length_z (@nil label)) with (z); eauto.
         unfold list_length_z. simpl. omega.
-      * assert (l1 = nil).
-        { destruct l1; try congruence. rewrite !list_length_z_cons in l.
-          assert (list_length_z l2 >= 0) by eapply list_length_z_pos.
-          assert (list_length_z l2 + 1 + 1 >= 2) by omega.
-          assert (2 <= 1) by omega. contradiction H2. omega. }
-        subst. simpl in *. destruct (in_dec _ _) as [HIN|HNIN]; try congruence.
+      * eapply header_size_cons_nil in l as HL1.
+        subst. simpl in *. destruct (in_dec _ _); try congruence.
         simpl in *.
         destruct (peq _ _); try intuition congruence.
 Qed.
@@ -1652,6 +1667,17 @@ Proof.
        rewrite H1. econstructor.
 Qed.
 
+Lemma pc_reg_overwrite: forall (r: ireg) rs1 m1 rs2 m2 bb
+  (MATCHI: match_internal (size bb - 1) (State rs1 m1) (State rs2 m2)),
+  rs2 # PC <- (rs2 r) =
+  (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size bb)))) # PC <-
+  (rs1 r).
+Proof.
+  intros.
+  unfold Pregmap.set; apply functional_extensionality.
+  intros x; destruct (PregEq.eq x PC) as [X | X]; try discriminate; inv_matchi.
+Qed.
+
 Lemma exec_cfi_simulation:
   forall bb f tf rs1 m1 rs1' m1' rs2 m2 cfi
   (SIZE: size bb <= Ptrofs.max_unsigned)
@@ -1726,53 +1752,46 @@ Proof.
   - (* Pbr *)
     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.
+    rewrite (pc_reg_overwrite r rs1 m1' rs2 m2 bb); auto.
+    inv_matchi.
   - (* Pret *)
     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.
+    rewrite (pc_reg_overwrite r rs1 m1' rs2 m2 bb); auto.
+    inv_matchi.
   - (* Pcbnz *)
     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.
+    erewrite incrPC_agree_but_pc in H0; try congruence.
+    destruct eval_testzero; next_stuck_cong.
     destruct b.
     * exploit next_inst_incr_pc_preserved; eauto.
     * exploit goto_label_preserved; eauto.
-      (*
   - (* Pcbz *)
-    simpl; eexists; eexists; split.
-    + rewrite <- H0.
-      unfold eval_branch. (* TODO, will be very similar to Pcbnz *) admit.
-    + constructor.
-  - (* Pcbz *)
-    simpl; eexists; eexists; split.
-    + rewrite <- H0.
-      unfold eval_branch.
-      replace (incrPC (Ptrofs.repr size_b) rs1 r) with (rs2 r). 2: {
-          symmetry; rewrite incrPC_agree_but_pc; try discriminate; auto;
-          inv MI; rewrite AG; try discriminate; auto.
-      } (* TODO, cf. Pcbnz *) admit.
-    + constructor.
+    inv_matchi.
+    unfold eval_branch in *.
+    erewrite incrPC_agree_but_pc in H0; try congruence.
+    destruct eval_testzero; next_stuck_cong.
+    destruct b.
+    * exploit goto_label_preserved; eauto.
+    * exploit next_inst_incr_pc_preserved; eauto.
+  - (* Ptbnbz *)
+    inv_matchi.
+    unfold eval_branch in *.
+    erewrite incrPC_agree_but_pc in H0; try congruence.
+    destruct eval_testbit; next_stuck_cong.
+    destruct b.
+    * exploit goto_label_preserved; eauto.
+    * exploit next_inst_incr_pc_preserved; eauto.
   - (* Ptbz *)
-    simpl; eexists; eexists; split.
-    + rewrite <- H0.
-      (* TODO, cf. Pcbz *) admit.
-    + constructor.
-  - (* Pbtbl *)
+    inv_matchi.
+    unfold eval_neg_branch in *.
+    erewrite incrPC_agree_but_pc in H0; try congruence.
+    destruct eval_testbit; next_stuck_cong.
+    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