Asmblockdeps is now finished

1 files changed, 42 insertions, 226 deletions

diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v
index 23cdf1ab..9b8b8d49 100644
--- a/aarch64/Asmblockdeps.v
+++ b/aarch64/Asmblockdeps.v
@@ -1969,23 +1969,7 @@ Proof.
       * rewrite assign_diff, Pregmap.gso; try rewrite H0; try rewrite ppos_discr; auto.
 Qed.
 
-Definition trans_block_aux bdy sz ex := (trans_body bdy) ++ (trans_pcincr sz (trans_exit ex) :: nil).
-
-(*Theorem bisimu rsr mr sr bdy ex sz:*)
-  (*match_states (State rsr mr) sr ->*)
-  (*match_outcome (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) ex (Ptrofs.repr sz) bdy rsr mr) (run Ge (trans_block_aux bdy sz (Some (PCtlFlow ex))) sr).*)
-(*Proof.*)
-  (*intros MS. unfold bbstep, trans_block_aux.*)
-  (*exploit (bisimu_body bdy rsr mr sr); eauto.*)
-  (*destruct (exec_body _ _ _ _ _); simpl.*)
-  (*- unfold match_states in *. intros (s' & X1 & X2). destruct s.*)
-    (*erewrite run_app_Some; eauto.*)
-    (*exploit (bisimu_exit ex sz _rs _m s'); eauto.*)
-    (*destruct Ge; simpl. destruct MS as (Y1 & Y2). destruct X2 as (X2 & X3).*)
-    (*replace_pc. erewrite !X3; simpl.*)
-    (*destruct (inst_run _ _ _ _); simpl; auto.*)
-  (*- intros X; erewrite run_app_None; eauto.*)
-(*Qed.*)
+(* Definition trans_block_aux bdy sz ex := (trans_body bdy) ++ (trans_pcincr sz (trans_exit ex) :: nil). *)
 
 Theorem bisimu rsr mr sr bb:
   match_states (State rsr mr) sr ->
@@ -2003,174 +1987,6 @@ Proof.
   - intros X; erewrite run_app_None; eauto.
 Qed.
 
-(* TODO We should use this version, but our current definitions
-does not match
-Theorem bisimu rsr mr b sr ex sz:
-    match_states (State rsr mr) sr -> 
-    match_outcome (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) ex (Ptrofs.repr sz) (body b) rsr mr) (exec Ge (trans_block b) sr).
-Proof.
-
-  intros MS. unfold bbstep.
-  exploit (bisimu_body (body b) rsr mr sr); eauto.
-  unfold exec, trans_block; simpl.
-  destruct (exec_body _ _ _ _); simpl.
-  - unfold match_states in *. intros (s' & X1 & X2). destruct s.
-    erewrite run_app_Some; eauto.
-    exploit (bisimu_exit ex sz _rs _m s' s'); eauto.
-    destruct Ge; simpl. destruct X2 as (X2 & X3). destruct MS as (Y1 & Y2).
-    replace (6) with (#PC) by auto. erewrite X3; simpl.
-    unfold trans_exit.
-    destruct (inst_run _ _ _); simpl; auto.
-  - intros X; erewrite run_app_None; eauto.
-
-  intros MS. unfold bbstep, trans_block.
-  exploit (bisimu_body (body b) rsr mr sr); eauto.
-  destruct (exec_body _ _ _ _ _); simpl.
-  - unfold match_states in *. intros (s' & X1 & X2). destruct s.
-    erewrite run_app_Some; eauto.
-    exploit (bisimu_exit ex sz _rs _m s' s'); eauto.
-    destruct Ge; simpl. destruct MS as (Y1 & Y2). destruct X2 as (X2 & X3).
-    replace (6) with (#PC) by auto. erewrite !X3; simpl.
-    destruct (inst_run _ _ _ _); simpl; auto.
-  - intros X; erewrite run_app_None; eauto.
-Qed.*)
-
-(*Theorem bisimu_bblock rsr mr sr bdy1 bdy2 ex sz:*)
-  (*match_states (State rsr mr) sr ->*)
-  (*match_outcome *)
-   (*match bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) ex (Ptrofs.repr sz) bdy1 rsr mr with*)
-   (*| Some (State rs' m') => exec_body Ge.(_lk) Ge.(_genv) bdy2 rs' m'*)
-   (*| Stuck => Stuck*)
-   (*end*)
-   (*(run Ge ((trans_block_aux bdy1 sz (Some (PCtlFlow (ex))))++(trans_body bdy2)) sr).*)
-(*Proof.*)
-  (*intros.*)
-  (*exploit (bisimu rsr mr sr bdy1 ex sz); eauto.*)
-  (*destruct (bbstep _ _ _ _ _ _); simpl.*)
-  (*- intros (s' & X1 & X2).*)
-    (*erewrite run_app_Some; eauto. destruct s.*)
-    (*eapply bisimu_body; eauto.*)
-  (*- intros; erewrite run_app_None; eauto.*)
-(*Qed.*)
-
-(*Lemma trans_body_perserves_permutation bdy1 bdy2:*)
-  (*Permutation bdy1 bdy2 ->*)
-  (*Permutation (trans_body bdy1) (trans_body bdy2).*)
-(*Proof.*)
-  (*induction 1; simpl; econstructor; eauto.*)
-(*Qed.*)
-(*
-Lemma trans_body_app bdy1: forall bdy2,
-   trans_body (bdy1++bdy2) = (trans_body bdy1) ++ (trans_body bdy2).
-Proof.
-  induction bdy1; simpl; congruence.
-Qed.
-*)
-(*Theorem trans_block_perserves_permutation bdy1 bdy2 b:*)
-  (*Permutation (bdy1 ++ bdy2) (body b) ->*)
-  (*Permutation (trans_block b) ((trans_block_aux bdy1 (size b) (exit b))++(trans_body bdy2)).*)
-(*Proof.*)
-  (*intro H; unfold trans_block, trans_block_aux.*)
-  (*eapply perm_trans.*)
-  (*- eapply Permutation_app_tail. *)
-    (*apply trans_body_perserves_permutation.*)
-    (*apply Permutation_sym; eapply H.*)
-  (*- rewrite trans_body_app. rewrite <-! app_assoc.*)
-    (*apply Permutation_app_head.*)
-    (*apply Permutation_app_comm.*)
-(*Qed.*)
-
-(*Theorem bisimu_par rs1 m1 s1' b ge fn o2:*)
-    (*Ge = Genv ge fn ->*)
-    (*match_states (State rs1 m1) s1' -> *)
-    (*parexec_bblock ge fn b rs1 m1 o2 ->*)
-  (*exists o2',*)
-     (*prun Ge (trans_block b) s1' o2'*)
-  (*/\ match_outcome o2 o2'.*)
-(*Proof.*)
-  (*intros GENV MS PAREXEC.*)
-  (*inversion PAREXEC as (bdy1 & bdy2 & PERM & WIO).*)
-  (*exploit trans_block_perserves_permutation; eauto.*)
-  (*intros Perm.*)
-  (*exploit (bisimu_par_wio_bblock ge fn rs1 m1 s1' bdy1 bdy2 (exit b) (size b)); eauto.*)
-  (*rewrite <- WIO. clear WIO.*)
-  (*intros H; eexists; split. 2: eapply H.*)
-  (*unfold prun; eexists; split; eauto. *)
-  (*destruct (prun_iw _ _ _ _); simpl; eauto.*)
-(*Qed.*)
-
-(** sequential execution *)
-(*Theorem bisimu_basic ge fn bi rs m s:*)
-  (*Ge = Genv ge fn ->*)
-  (*match_states (State rs m) s ->*)
-  (*match_outcome (exec_basic_instr ge bi rs m) (inst_run Ge (trans_basic bi) s s).*)
-(*Proof.*)
-  (*intros; unfold exec_basic_instr. rewrite inst_run_prun.*)
-  (*eapply bisimu_par_wio_basic; eauto.*)
-(*Qed.*)
-
-(*Lemma bisimu_body:*)
-  (*forall bdy ge fn rs m s,*)
-  (*Ge = Genv ge fn ->*)
-  (*match_states (State rs m) s ->*)
-  (*match_outcome (exec_body ge bdy rs m) (exec Ge (trans_body bdy) s).*)
-(*Proof.*)
-  (*induction bdy as [|i bdy]; simpl; eauto. *)
-  (*intros.*)
-  (*exploit (bisimu_basic ge fn i rs m s); eauto.*)
-  (*destruct (exec_basic_instr _ _ _ _); simpl.*)
-  (*- intros (s' & X1 & X2). rewrite X1; simpl; eauto.*)
-  (*- intros X; rewrite X; simpl; auto.*)
-(*Qed.*)
-
-(*Theorem bisimu_exit ge fn b rs m s:*)
-  (*Ge = Genv ge fn ->*)
-  (*match_states (State rs m) s ->*)
-  (*match_outcome (exec_control ge fn (exit b) (nextblock b rs) m) (inst_run Ge (trans_pcincr (size b) (trans_exit (exit b))) s s).*)
-(*Proof.*)
-  (*intros; unfold exec_control, nextblock. rewrite inst_run_prun. *)
-  (*apply (bisimu_par_control (exit b) (size b) (Val.offset_ptr (rs PC) (Ptrofs.repr (size b))) ge fn rs rs m m s s); auto.*)
-(*Qed.*)
-
-(*Lemma bbstep_is_exec_bblock: forall bb (cfi: cf_instruction) size_bb bdy rs m rs' m' t,*)
-  (*(body bb) = bdy ->*)
-  (*(exit bb) = Some (PCtlFlow cfi) ->*)
-  (*Ptrofs.repr (size bb) = size_bb ->*)
-  (*exec_bblock Ge.(_lk) Ge.(_genv) Ge.(_fn) bb rs m t rs' m'*)
-  (*<-> (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) (cfi) size_bb bdy rs m = Next rs' m' /\ t = E0).*)
-(*Proof.*)
-  (*intros.*)
-(*Admitted.*)
-
-(* TODO This is the lemma we should use if we want to modelize
-builtins in our scheduling process.
-If we do not modelize builtins, we could use a simpler definition (trace E0) *)
-(*
-Theorem bisimu' rs m rs' m' bb s:
-    match_states (State rs m) s -> 
-    (exists t, exec_bblock Ge.(_lk) Ge.(_genv) Ge.(_fn) bb rs m t rs' m')
-    <-> (exists s', (exec Ge (trans_block bb) s) = Some s' /\ match_states (State rs' m') s').
-Proof.
-  intros MS.
-  destruct (exit bb) eqn:EQEXIT.
-  destruct c eqn:EQC.
-  - split.
-    + intros (t & H).
-  rewrite bbstep_is_exec_bblock in H; eauto.
-  eexists; split. destruct H as [H0 H1].
-  generalize (bisimu )
-  unfold exec_bblock.
-  exploit (bisimu_body (body b) ge fn rs m s); eauto.
-  unfold exec, trans_block; simpl.
-  destruct (exec_body _ _ _ _); simpl.
-  - intros (s' & X1 & X2).
-    erewrite run_app_Some; eauto.
-    exploit (bisimu_exit ge fn b rs0 m0 s'); eauto.
-    subst Ge; simpl. destruct X2 as (Y1 & Y2). erewrite Y2; simpl.
-    destruct (inst_run _ _ _); simpl; auto.
-  - intros X; erewrite run_app_None; eauto.
-Qed.*)
-
 Theorem trans_state_match: forall S, match_states S (trans_state S).
 Proof.
   intros. destruct S as (rs & m). simpl.
@@ -2201,14 +2017,6 @@ Variable Ge: genv.
 
 Local Hint Resolve trans_state_match: core.
 
-(* TODO remove ? *)
-Definition exit_cfi bb : option cf_instruction :=
-  match exit bb with
-  | Some (Pbuiltin _ _ _) => None
-  | Some (PCtlFlow c) => Some c
-  | None => None
-  end.
-
 Lemma bblock_simu_reduce_aux:
   forall p1 p2,
   L.bblock_simu Ge (trans_block p1) (trans_block p2) ->
@@ -2232,6 +2040,38 @@ Proof.
   * discriminate.
 Qed.
 
+Lemma incrPC_set_res_commut res: forall d vres rs,  
+  incrPC d (set_res (map_builtin_res DR res) vres rs) =
+  set_res (map_builtin_res DR res) vres (incrPC d rs).
+Proof.
+  induction res; simpl; auto.
+  - intros; apply functional_extensionality.
+    unfold incrPC; intros x0.
+    destruct (PregEq.eq x0 PC).
+    + subst; rewrite! Pregmap.gss; auto.
+    + rewrite Pregmap.gso; auto.
+      destruct (PregEq.eq x x0).
+      * subst; rewrite! Pregmap.gss; auto.
+      * rewrite !Pregmap.gso; auto.
+  - intros; rewrite IHres2. f_equal. auto.
+Qed.
+
+Lemma incrPC_undef_regs_commut l : forall d rs,
+  incrPC d (undef_regs (map preg_of l) rs) = undef_regs (map preg_of l) (incrPC d rs).
+Proof.
+  induction l; simpl; auto.
+  intros. rewrite IHl. unfold incrPC.
+  destruct (PregEq.eq (preg_of a) PC).
+  - rewrite e. rewrite Pregmap.gss.
+    simpl. apply f_equal. unfold Pregmap.set.
+    apply functional_extensionality. intros x.
+    destruct (PregEq.eq x PC); auto.
+  - rewrite Pregmap.gso; auto.
+    apply f_equal. unfold Pregmap.set.
+    apply functional_extensionality. intros x.
+    destruct (PregEq.eq x PC); subst; auto.
+Qed.
+
 Lemma bblock_simu_reduce:
   forall p1 p2,
   L.bblock_simu Ge (trans_block p1) (trans_block p2) ->
@@ -2285,36 +2125,11 @@ intros H4. eexists; eexists; split; try reflexivity.
         rewrite H5; rewrite Pregmap.gso; auto.
       * replace (rs1 SP) with (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size p1))) SP) by auto.
         rewrite H5; rewrite Pregmap.gso; auto; try discriminate.
-    + admit.
-    
-(*  generalize (H0 (trans_state (State rs m))); clear H0.
-  intros H0 m' t0 (rs1 & m1 & H1 & H2).
-  exploit (bisimu Ge rs m (trans_state (State rs m)) p1); eauto.
-  exploit (bisimu Ge rs m (trans_state (State rs m)) p2); eauto.
-  unfold bbstep, estep.
-  rewrite H1; simpl.
-  unfold has_builtin in BLT.
-  destruct (exit p1) eqn:EQEX1. destruct c.
-  - inversion H2; subst.
-    destruct (exec_body _ _ (body p2) _ _) as [[rs2 m2]|] eqn:EQBDY2; try congruence.
-    unfold trans_block, exec in *.
-    exploit (bisimu_body); eauto. erewrite H1. simpl.
-    (*destruct (exec_body _ _ (body p2) _ _) eqn:EQBDY1.*)
-  destruct (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) p1 rs m); try (unfold Stuck in EBB; congruence).
-  intros H1 (s2' & exp2 & MS'). unfold exec in exp2, H1. rewrite exp2 in H0.
-  destruct H0 as (m2' & H0 & H2). discriminate. rewrite H0 in H1.
-  destruct (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) p2 rs m); simpl in H1.
-  * unfold match_states in H1, MS'. destruct s, s0.
-    destruct H1 as (s' & H1 & H3 & H4). inv H1. inv MS'.
-    replace (_rs0) with (_rs).
-    - replace (_m0) with (_m); auto. congruence.
-    - apply functional_extensionality. intros r.
-      generalize (H1 r). intros Hr. congruence.
-  * discriminate.*)
-
-Admitted.
-  
-(*Qed.*)
+    + rewrite !incrPC_set_res_commut.
+      rewrite !incrPC_undef_regs_commut.
+      rewrite H5.
+      reflexivity.
+Qed.
 
 (** Used for debug traces *)
 
@@ -2722,9 +2537,10 @@ Local Hint Resolve IST.bblock_simu_test_correct IST.verb_bblock_simu_test_correc
 Theorem bblock_simu_test_correct verb p1 p2 :
   WHEN bblock_simu_test verb p1 p2 ~> b THEN b=true -> forall ge fn lk, Asmblockprops.bblock_simu lk ge fn p1 p2.
 Proof.
-  wlp_simplify; eapply bblock_simu_reduce with (Ge:={| _genv := ge; _fn := fn; _lk := lk |}); eauto.
-  Admitted.
-(* Qed. *)
+  wlp_simplify; eapply bblock_simu_reduce with (Ge:={| _genv := ge; _fn := fn; _lk := lk |}); eauto;
+  intros; destruct H; auto.
+Qed.
+
 Hint Resolve bblock_simu_test_correct: wlp.
 
 (** ** Coerce bblock_simu_test into a pure function (this is a little unsafe like all oracles in CompCert). *)