From 1b1e5cfc70899d759ed099832b8821372e024ad0 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 9 Jun 2021 06:56:31 +0200 Subject: valid_pointer_preserv dans BTL_SEtheory => opportunites de *grosses* simplifications (à venir ) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- scheduling/BTL_SEsimuref.v | 79 ++++++++-------------------------------------- scheduling/BTL_SEtheory.v | 50 +++++++++++++++++------------ 2 files changed, 42 insertions(+), 87 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v index 5098659d..40c28934 100644 --- a/scheduling/BTL_SEsimuref.v +++ b/scheduling/BTL_SEsimuref.v @@ -67,11 +67,9 @@ Local Hint Constructors ris_ok: core. Record ris_refines ctx (ris: ristate) (sis: sistate): Prop := { OK_EQUIV: sis_ok ctx sis <-> ris_ok ctx ris; MEM_EQ: ris_ok ctx ris -> eval_smem ctx ris.(ris_smem) = eval_smem ctx sis.(si_smem); - REG_EQ: ris_ok ctx ris -> forall r, eval_sval ctx (ris_sreg_get ris r) = eval_sval ctx (si_sreg sis r); - (* the below invariant allows to evaluate operations in the initial memory of the path instead of the current memory *) - VALID_PRESERV: forall m b ofs, eval_smem ctx sis.(si_smem) = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer (cm0 ctx) b ofs + REG_EQ: ris_ok ctx ris -> forall r, eval_sval ctx (ris_sreg_get ris r) = eval_sval ctx (si_sreg sis r) }. -Local Hint Resolve OK_EQUIV MEM_EQ REG_EQ VALID_PRESERV: core. +Local Hint Resolve OK_EQUIV MEM_EQ REG_EQ: core. Local Hint Constructors ris_refines: core. Record ris_simu ris1 ris2: Prop := { @@ -218,11 +216,11 @@ Inductive rst_refines ctx: rstate -> sstate -> Prop := (RIS: ris_refines ctx ris sis) (RFV: ris_ok ctx ris -> rfv_refines ctx rfv sfv) : rst_refines ctx (Rfinal ris rfv) (Sfinal sis sfv) - | Refcond cond rargs args sm rifso rifnot ifso ifnot - (RCOND: seval_condition ctx cond rargs Sinit = seval_condition ctx cond args sm) - (REFso: seval_condition ctx cond rargs Sinit = Some true -> rst_refines ctx rifso ifso) - (REFnot: seval_condition ctx cond rargs Sinit = Some false -> rst_refines ctx rifnot ifnot) - : rst_refines ctx (Rcond cond rargs rifso rifnot) (Scond cond args sm ifso ifnot) + | Refcond cond rargs args rifso rifnot ifso ifnot + (RCOND: seval_condition ctx cond rargs = seval_condition ctx cond args) + (REFso: seval_condition ctx cond rargs = Some true -> rst_refines ctx rifso ifso) + (REFnot: seval_condition ctx cond rargs = Some false -> rst_refines ctx rifnot ifnot) + : rst_refines ctx (Rcond cond rargs rifso rifnot) (Scond cond args ifso ifnot) | Refabort : rst_refines ctx Rabort Sabort . @@ -245,7 +243,7 @@ Proof. intros ROK1. exploit ris_simu_ok_preserv; eauto. - (* cond_simu *) - destruct (seval_condition (bctx1 ctx) cond args sm) eqn: SCOND; try congruence. + destruct (seval_condition (bctx1 ctx) cond args) eqn: SCOND; try congruence. generalize RCOND0. erewrite <- seval_condition_preserved, RCOND by eauto. intros SCOND0; rewrite <- SCOND0 in RCOND0. @@ -255,34 +253,6 @@ Proof. * exploit IHrst_simu2; eauto. Qed. - -(* TODO: useless ? -Record routcome := rout { - r_sis: ristate; - r_sfv: sfval; -}. - -Local Open Scope option_monad_scope. - -Fixpoint run_sem_irstate ctx (rst:rstate): option routcome := - match rst with - | Rfinal ris sfv => Some (rout ris sfv) - | Rcond cond args ifso ifnot => - SOME b <- seval_condition ctx cond args Sinit IN - run_sem_irstate ctx (if b then ifso else ifnot) - | Rabort => None - end. - -(* Non: pas assez de "matching" syntaxique entre rst et st pour rst_simu_correct -Definition rst_refines ctx rst st:= - (run_sem_isstate ctx st=None <-> run_sem_irstate ctx rst=None) - /\ (forall ris rfv sis sfv, run_sem_irstate ctx rst = Some (rout ris rfv) -> run_sem_isstate ctx st = Some (sout sis sfv) -> - (ris_refines ctx ris sis) /\ (ris_ok ctx ris -> rfv_refines ctx rfv sfv)). - -*) -*) - - (** * Refinement of the symbolic execution *) Local Hint Constructors rfv_refines optrsv_refines rsvident_refines rsvident_refines: core. @@ -341,7 +311,6 @@ Proof. congruence. + destruct 1; simpl in *. unfold ris_sreg_get; simpl. intros; rewrite PTree.gempty; eauto. - + try_simplify_someHyps. Qed. Definition rset_smem rm (ris:ristate): ristate := @@ -369,12 +338,11 @@ Qed. Lemma rset_mem_correct ctx rm sm ris sis: (eval_smem ctx ris.(ris_smem) = None -> eval_smem ctx rm = None) -> - (forall m b ofs, eval_smem ctx sm = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer (cm0 ctx) b ofs) -> ris_refines ctx ris sis -> (ris_ok ctx ris -> eval_smem ctx rm = eval_smem ctx sm) -> ris_refines ctx (rset_smem rm ris) (set_smem sm sis). Proof. - destruct 3; intros. + destruct 2; intros. econstructor; eauto. + rewrite ok_set_mem, ok_rset_mem; intuition congruence. + rewrite ok_rset_mem; intuition eauto. @@ -393,9 +361,6 @@ Lemma rexec_store_correct ctx chunk addr args src ris sis: Proof. intros REF; eapply rset_mem_correct; simpl; eauto. + intros X; rewrite X. repeat autodestruct; eauto. - + intros m b ofs; repeat autodestruct. - intros; erewrite <- Mem.storev_preserv_valid; [| eauto]. - eauto. + intros OK; erewrite eval_list_sval_refpreserv, MEM_EQ, REG_EQ; eauto. Qed. @@ -448,7 +413,7 @@ Qed. Definition rexec_op op args dst (ris:ristate): ristate := let args := list_sval_inj (List.map ris args) in - rset_sreg dst (Sop op args Sinit) ris. + rset_sreg dst (Sop op args) ris. Lemma rexec_op_correct ctx op args dst ris sis: ris_refines ctx ris sis -> @@ -456,10 +421,6 @@ Lemma rexec_op_correct ctx op args dst ris sis: Proof. intros REF; eapply rset_reg_correct; simpl; eauto. intros OK; erewrite eval_list_sval_refpreserv; eauto. - do 2 autodestruct; auto. - + intros. erewrite <- op_valid_pointer_eq; eauto. - + erewrite <- MEM_EQ; eauto. - intros; exploit OK_RMEM; eauto. destruct 1. Qed. Definition rexec_load trap chunk addr args dst (ris:ristate): ristate := @@ -474,24 +435,10 @@ Proof. intros OK; erewrite eval_list_sval_refpreserv, MEM_EQ; eauto. Qed. -Lemma seval_condition_valid_preserv ctx cond args sm - (OK: eval_smem ctx sm <> None) - (VALID_PRESERV: forall m b ofs, eval_smem ctx sm = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer (cm0 ctx) b ofs) - :seval_condition ctx cond args sm = seval_condition ctx cond args Sinit. -Proof. - unfold seval_condition; autodestruct; simpl; try congruence. - intros EVAL_LIST. - autodestruct; try congruence. - intros. - eapply cond_valid_pointer_eq; intros. - exploit VALID_PRESERV; eauto. -Qed. - Lemma seval_condition_refpreserv ctx cond args ris sis: ris_refines ctx ris sis -> ris_ok ctx ris -> - seval_condition ctx cond (list_sval_inj (map ris args)) Sinit = - seval_condition ctx cond (list_sval_inj (map sis args)) Sinit. + seval_condition ctx cond (list_sval_inj (map ris args)) = seval_condition ctx cond (list_sval_inj (map sis args)). Proof. intros; unfold seval_condition. erewrite eval_list_sval_refpreserv; eauto. @@ -654,7 +601,7 @@ Fixpoint history ctx ib sis (k:sistate -> option (list sistate)): option (list s history ctx ib1 sis (fun sis2 => history ctx ib2 sis2 k) | Bcond cond args ifso ifnot _ => let args := list_sval_inj (List.map sis args) in - SOME b <- seval_condition ctx cond args sis.(si_smem) IN + SOME b <- seval_condition ctx cond args IN SOME oks <- history ctx (if b then ifso else ifnot) sis k IN Some (sis::oks) end @@ -846,7 +793,7 @@ Proof. exploit (OK2 sis); auto. assert (rOK: ris_ok ctx ris). { erewrite <- OK_EQUIV; eauto. } generalize COND. - erewrite seval_condition_valid_preserv, <- seval_condition_refpreserv; eauto. + erewrite <- seval_condition_refpreserv; eauto. intros; econstructor; try_simplify_someHyps. Qed. diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index 464bb0f0..97dc7fc8 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -29,7 +29,7 @@ Record iblock_exec_context := Bctx { Inductive sval := | Sundef | Sinput (r: reg) - | Sop (op:operation) (lsv: list_sval) (sm: smem) + | Sop (op:operation) (lsv: list_sval) | Sload (sm: smem) (trap: trapping_mode) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) with list_sval := | Snil @@ -55,10 +55,9 @@ Fixpoint eval_sval ctx (sv: sval): option val := match sv with | Sundef => Some Vundef | Sinput r => Some ((crs0 ctx)#r) - | Sop op l sm => + | Sop op l => SOME args <- eval_list_sval ctx l IN - SOME m <- eval_smem ctx sm IN - eval_operation (cge ctx) (csp ctx) op args m + eval_operation (cge ctx) (csp ctx) op args (cm0 ctx) | Sload sm trap chunk addr lsv => match trap with | TRAP => @@ -98,6 +97,16 @@ with eval_smem ctx (sm: smem): option mem := Mem.storev chunk m a sv end. + +Lemma valid_pointer_preserv ctx sm: + forall m b ofs, eval_smem ctx sm = Some m -> Mem.valid_pointer (cm0 ctx) b ofs = Mem.valid_pointer m b ofs. +Proof. + induction sm; simpl; intros; try_simplify_someHyps; auto. + repeat autodestruct; intros; erewrite IHsm by reflexivity. + eapply Mem.storev_preserv_valid; eauto. +Qed. +Local Hint Resolve valid_pointer_preserv: core. + Lemma eval_list_sval_inj ctx l (sreg: reg -> sval) rs: (forall r : reg, eval_sval ctx (sreg r) = Some (rs # r)) -> eval_list_sval ctx (list_sval_inj (map sreg l)) = Some (rs ## l). @@ -105,10 +114,9 @@ Proof. intros H; induction l as [|r l]; simpl; repeat autodestruct; auto. Qed. -Definition seval_condition ctx (cond: condition) (lsv: list_sval) (sm: smem) : option bool := +Definition seval_condition ctx (cond: condition) (lsv: list_sval): option bool := SOME args <- eval_list_sval ctx lsv IN - SOME m <- eval_smem ctx sm IN - eval_condition cond args m. + eval_condition cond args (cm0 ctx). (** * Auxiliary definitions on Builtins *) @@ -565,7 +573,7 @@ Qed. Definition sexec_op op args dst sis: sistate := let args := list_sval_inj (List.map sis.(si_sreg) args) in - set_sreg dst (Sop op args sis.(si_smem)) sis. + set_sreg dst (Sop op args) sis. Lemma sexec_op_correct ctx op args dst sis rs m v (EVAL: eval_operation (cge ctx) (csp ctx) op rs ## args m = Some v) @@ -577,6 +585,7 @@ Proof. rewrite Regmap.gss; simpl; auto. erewrite eval_list_sval_inj; simpl; auto. try_simplify_someHyps. + intros; erewrite op_valid_pointer_eq; eauto. - intros; rewrite Regmap.gso; auto. Qed. @@ -619,11 +628,11 @@ Qed. Lemma seval_condition_eq ctx cond args sis rs m (SIS : sem_sistate ctx sis rs m) - :seval_condition ctx cond (list_sval_inj (map (si_sreg sis) args)) (si_smem sis) = eval_condition cond rs ## args m. + :seval_condition ctx cond (list_sval_inj (map (si_sreg sis) args)) = eval_condition cond rs ## args m. Proof. destruct SIS as (PRE&MEM®); unfold seval_condition; simpl. erewrite eval_list_sval_inj; simpl; auto. - erewrite MEM; auto. + eapply cond_valid_pointer_eq; eauto. Qed. (** * Compute sistate associated to final values *) @@ -698,7 +707,7 @@ Qed. (* symbolic state *) Inductive sstate := | Sfinal (sis: sistate) (sfv: sfval) - | Scond (cond: condition) (args: list_sval) (sm: smem) (ifso ifnot: sstate) + | Scond (cond: condition) (args: list_sval) (ifso ifnot: sstate) | Sabort . @@ -711,8 +720,8 @@ Record soutcome := sout { Fixpoint run_sem_isstate ctx (st:sstate): option soutcome := match st with | Sfinal sis sfv => Some (sout sis sfv) - | Scond cond args sm ifso ifnot => - SOME b <- seval_condition ctx cond args sm IN + | Scond cond args ifso ifnot => + SOME b <- seval_condition ctx cond args IN run_sem_isstate ctx (if b then ifso else ifnot) | Sabort => None end. @@ -723,10 +732,10 @@ Inductive sem_sstate ctx stk t s: sstate -> Prop := (SIS: sem_sistate ctx sis (str_regs (cf ctx) sfv rs) m) (SFV: sem_sfval ctx stk sfv rs m t s) : sem_sstate ctx stk t s (Sfinal sis sfv) - | sem_Scond b cond args sm ifso ifnot - (SEVAL: seval_condition ctx cond args sm = Some b) + | sem_Scond b cond args ifso ifnot + (SEVAL: seval_condition ctx cond args = Some b) (SELECT: sem_sstate ctx stk t s (if b then ifso else ifnot)) - : sem_sstate ctx stk t s (Scond cond args sm ifso ifnot) + : sem_sstate ctx stk t s (Scond cond args ifso ifnot) (* NB: Sabort: fails to produce a transition *) . @@ -784,7 +793,7 @@ Fixpoint sexec_rec f ib sis (k: sistate -> sstate): sstate := let args := list_sval_inj (List.map sis.(si_sreg) args) in let ifso := sexec_rec f ifso sis k in let ifnot := sexec_rec f ifnot sis k in - Scond cond args sis.(si_smem) ifso ifnot + Scond cond args ifso ifnot end . @@ -954,6 +963,7 @@ Proof. simpl. destruct SIS as (PRE&MEM®). erewrite eval_list_sval_inj; simpl; auto. try_simplify_someHyps. + intros; erewrite op_valid_pointer_eq; eauto. Qed. Lemma sexec_load_TRAP_abort ctx chunk addr args dst sis rs m @@ -1177,7 +1187,6 @@ Proof. induction sv using sval_mut with (P0 := fun lsv => eval_list_sval (bctx1 ctx) lsv = eval_list_sval (bctx2 ctx) lsv) (P1 := fun sm => eval_smem (bctx1 ctx) sm = eval_smem (bctx2 ctx) sm); simpl; auto. + rewrite IHsv; clear IHsv. destruct (eval_list_sval _ _); auto. - rewrite IHsv0; clear IHsv0. destruct (eval_smem _ _); auto. erewrite eval_operation_preserved; eauto. + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto. erewrite eval_addressing_preserved; eauto. @@ -1228,12 +1237,11 @@ Proof. reflexivity. Qed. -Lemma seval_condition_preserved cond lsv sm: - seval_condition (bctx1 ctx) cond lsv sm = seval_condition (bctx2 ctx) cond lsv sm. +Lemma seval_condition_preserved cond lsv: + seval_condition (bctx1 ctx) cond lsv = seval_condition (bctx2 ctx) cond lsv. Proof. unfold seval_condition. rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto. - rewrite smem_eval_preserved; auto. Qed. (* TODO: useless ? -- cgit