exec_body_simulation without star'

1 files changed, 101 insertions, 0 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 4ee7c550..6b5b0913 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -967,6 +967,16 @@ Proof.
     generalize (list_length_z_aux_increase _ l1 2); omega.
 Qed.
 
+Lemma eval_addressing_preserved a rs1 rs2:
+  (forall r : preg, r <> PC -> rs1 r = rs2 r) ->
+  eval_addressing lk a rs1 = Asm.eval_addressing tge a rs2.
+Proof.
+  intros EQ.
+  destruct a; simpl; try (rewrite !EQ; congruence). auto.
+Qed.
+
+Ltac next_stuck_cong := try (unfold Next, Stuck in *; congruence).
+
 Lemma exec_basic_simulation:
   forall tf n rs1 m1 rs1' m1' rs2 m2 bi tbi
   (BASIC: exec_basic lk ge bi rs1 m1 = Next rs1' m1')
@@ -975,6 +985,26 @@ Lemma exec_basic_simulation:
   exists rs2' m2', Asm.exec_instr tge tf tbi
                                   rs2 m2 = Next rs2' m2'
                    /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2').
+Proof.
+  intros.
+  destruct bi.
+  2: {
+    simpl in*. destruct ld. 
+    { monadInv TRANSBI. destruct rd as [[r|]|]; try congruence. inversion EQ; subst.
+      simpl in *. unfold exec_load, Asm.exec_load in *.
+      inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst.
+      rewrite <- (eval_addressing_preserved a rs1 rs2); auto.
+      destruct (Mem.loadv _ _ _).
+      + inversion BASIC; auto. repeat (econstructor; eauto).
+        * intros. unfold Asm.nextinstr. rewrite (Pregmap.gso (i := r) (j := PC)); auto.
+          destruct (PregEq.eq r x).
+          { subst. rewrite !Pregmap.gss; auto. }
+          { rewrite !Pregmap.gso; auto. }
+        * unfold Asm.nextinstr. rewrite Pregmap.gss. rewrite !Pregmap.gso; try congruence. admit.
+      + next_stuck_cong. }
+    all:admit.
+    
+  } all:admit.
 Admitted.
 
 Lemma exec_body_simulation_star': forall
@@ -1100,6 +1130,77 @@ Proof.
       rewrite H in H0; simpl in H0; repeat rewrite length_agree in H0; omega.
 Qed.
 
+Lemma exec_body_simulation_plus_alt li: forall b ofs f bb rs m s2 rs' m'
+  (BLI: li = body bb)
+  (ATPC: rs PC = Vptr b ofs)
+  (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
+  (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb)
+  (NEMPTY_BODY: body bb <> nil)
+  (MATCHI: match_internal (list_length_z (header bb)) (State rs m) s2)
+  (BODY: exec_body lk ge (body bb) rs m = Next rs' m'),
+  exists s2', plus Asm.step tge s2 E0 s2'
+             /\ match_internal (size bb - (Z.of_nat (length_opt (exit bb)))) (State rs' m') s2'.
+Proof.
+  induction li as [|a [|b]]; simpl.
+  - (* len(body bb) == 0 *)
+    congruence.
+  - (* len(body bb) == 1 *)
+    (* Contruct the MI hypothesis. *)
+    intros. rewrite <- BLI in *. simpl in *.
+    exploit internal_functions_unfold; eauto.
+    intros (tc & FINDtf & TRANStf & _). 
+    assert (BDYLENPOS: (0 < length (body bb))%nat). { rewrite <- BLI; simpl; omega. }
+    exploit find_basic_instructions; eauto.
+    rewrite <- BLI; intros FINDBI.
+    destruct FINDBI as (i_next & (bi_next' & (NTHBI & TRANSBI & FIND_INSTR))).
+    inversion NTHBI; subst bi_next'.
+    destruct (exec_basic _ _ _ _ _) eqn:EXEC_BASIC; next_stuck_cong.
+    inversion BODY. subst.
+    destruct s as (rs1 & m1); simpl in *.
+    destruct s2 as (rs2 & m2); simpl in *.
+    exploit exec_basic_simulation; eauto.
+    intros (rs_next' & m_next' & EXEC_INSTR & MI_NEXT).
+
+    (* Code from the star' lemma bellow. We need this to exploit exec_step_internal. *)
+    exploit exec_basic_dont_move_PC; eauto. intros AGPC.
+    inversion MI_NEXT as [A B C D E M_NEXT_AGREE RS_NEXT_AGREE ATPC_NEXT PC_OFS_NEXT RS RS'].
+    subst A. subst B. subst C. subst D. subst E.
+    rewrite ATPC in AGPC. symmetry in AGPC, ATPC_NEXT.
+
+    inv MATCHI. symmetry in AGPC0.
+    rewrite ATPC in AGPC0.
+    unfold Val.offset_ptr in AGPC0.
+    simpl in FIND_INSTR; rewrite Z.add_0_r in FIND_INSTR.
+
+    assert (Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned)
+    by (eapply size_of_blocks_bounds; eauto).
+    generalize (header_size_lt_block_size bb). rewrite length_agree; intros HEADER_LT.
+    generalize (Ptrofs.unsigned_range_2 ofs). intros (A & B).
+    
+    (* Execute internal step. *)
+    exploit (Asm.exec_step_internal tge b (Ptrofs.add ofs (Ptrofs.repr ((list_length_z (header bb)))))
+             {| Asm.fn_sig := fn_sig f; Asm.fn_code := tc |}
+             i_next rs2 m2); eauto.
+    { unfold Ptrofs.add. repeat (rewrite Ptrofs.unsigned_repr);
+      try rewrite length_agree; try split; try omega.
+      simpl; rewrite <- length_agree; assumption. }
+
+    (* This is our STEP hypothesis. *)
+    intros STEP_NEXT.
+    
+    (* XXX New code --> no need to use the star' lemma this way. *)
+    eexists; split.
+    + apply plus_one. eauto.
+    + assert (BDYLEN: list_length_z (body bb) = 1).
+      { rewrite <- BLI. apply list_length_z_cons. }
+      assert (LEN1: size bb - Z.of_nat (length_opt (exit bb)) = list_length_z (header bb) + list_length_z (body bb)).
+      { rewrite bblock_size_aux. omega. }
+      rewrite BDYLEN in LEN1. rewrite LEN1. apply MI_NEXT.
+  - (* len(body bb) >= 1 *)
+    (* Comment factoriser le code pour éviter de répéter les étapes du ca précédent ? Utiliser une ltac serait trop lourd ? *)
+
+Admitted.
+
 Lemma exec_body_simulation_plus b ofs f bb rs m s2 rs' m': forall
   (ATPC: rs PC = Vptr b ofs)
   (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))