From 1fc20a7262e6de3234e4411ae359b2e4e5ac36ee Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 24 Nov 2020 09:42:32 +0100 Subject: Asmblockdeps is now finished --- aarch64/Asmblockdeps.v | 268 ++++++++----------------------------------------- 1 file changed, 42 insertions(+), 226 deletions(-) (limited to 'aarch64/Asmblockdeps.v') 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). *) -- cgit