From f6a3483c7dcac5ed56a349361a19dc1f4c985de3 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Tue, 1 Jun 2021 17:16:06 +0200 Subject: starting BTL_SEsimuref --- scheduling/BTL_SEsimuref.v | 317 +++++++++++++++++++++++++++++++++++++++++++++ scheduling/BTL_SEtheory.v | 100 +------------- 2 files changed, 318 insertions(+), 99 deletions(-) create mode 100644 scheduling/BTL_SEsimuref.v (limited to 'scheduling') diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v new file mode 100644 index 00000000..af2159cb --- /dev/null +++ b/scheduling/BTL_SEsimuref.v @@ -0,0 +1,317 @@ +(** Refinement of BTL_SEtheory data-structures + in order to introduce (and prove correct) a lower-level specification of the simulation test. + + TODO: not yet with hash-consing ? Or "fake" hash-consing only ? + + Ceci est un "bac à sable". + + - On introduit une représentation plus concrète pour les types d'état symbolique [sistate] et [sstate]. + - Etant donné une spécification intuitive "*_simu" pour tester la simulation sur cette représentation des états symboliques, + on essaye déjà de trouver les bonnes notions de raffinement "*_refines" qui permette de prouver les lemmes "*_simu_correct". + - Il faudra ensuite vérifier que l'exécution symbolique préserve ces relations de raffinement ! + +*) + +Require Import Coqlib Maps Floats. +Require Import AST Integers Values Events Memory Globalenvs Smallstep. +Require Import Op Registers. +Require Import RTL BTL OptionMonad BTL_SEtheory. + +(** * Preservation properties *) + +(* TODO: inherited from RTLpath. Use simu_proof_context + bctx2 + bctx1 instead of all the hypotheses/variables below ? *) + +Section SymbValPreserved. + +Variable ge ge': BTL.genv. + +Hypothesis symbols_preserved_BTL: forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s. + +Hypothesis senv_preserved_BTL: Senv.equiv ge ge'. + +Lemma senv_find_symbol_preserved id: + Senv.find_symbol ge id = Senv.find_symbol ge' id. +Proof. + destruct senv_preserved_BTL as (A & B & C). congruence. +Qed. + +Lemma senv_symbol_address_preserved id ofs: + Senv.symbol_address ge id ofs = Senv.symbol_address ge' id ofs. +Proof. + unfold Senv.symbol_address. rewrite senv_find_symbol_preserved. + reflexivity. +Qed. + +Variable stk stk': list stackframe. +Variable f f': function. +Variable sp: val. +Variable rs0: regset. +Variable m0: mem. + +Lemma eval_sval_preserved sv: + eval_sval (Bctx ge stk f sp rs0 m0) sv = eval_sval (Bctx ge' stk' f' sp rs0 m0) sv. +Proof. + induction sv using sval_mut with (P0 := fun lsv => eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv) + (P1 := fun sm => eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) 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. + destruct (eval_addressing _ sp _ _); auto. + rewrite IHsv; auto. + + rewrite IHsv; clear IHsv. destruct (eval_sval _ _); auto. + rewrite IHsv0; auto. + + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto. + erewrite <- eval_addressing_preserved; eauto. + destruct (eval_addressing _ sp _ _); auto. + rewrite IHsv; clear IHsv. destruct (eval_smem _ _); auto. + rewrite IHsv1; auto. +Qed. + +Lemma seval_builtin_arg_preserved m: forall bs varg, + seval_builtin_arg (Bctx ge stk f sp rs0 m0) m bs varg -> + seval_builtin_arg (Bctx ge' stk' f' sp rs0 m0) m bs varg. +Proof. + induction 1; simpl. + all: try (constructor; auto). + - rewrite <- eval_sval_preserved. assumption. + - rewrite <- senv_symbol_address_preserved. assumption. + - rewrite senv_symbol_address_preserved. eapply seval_BA_addrglobal. +Qed. + +Lemma seval_builtin_args_preserved m lbs vargs: + seval_builtin_args (Bctx ge stk f sp rs0 m0) m lbs vargs -> + seval_builtin_args (Bctx ge' stk' f' sp rs0 m0) m lbs vargs. +Proof. + induction 1; constructor; eauto. + eapply seval_builtin_arg_preserved; auto. +Qed. + +Lemma list_sval_eval_preserved lsv: + eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv. +Proof. + induction lsv; simpl; auto. + rewrite eval_sval_preserved. destruct (eval_sval _ _); auto. + rewrite IHlsv; auto. +Qed. + +Lemma smem_eval_preserved sm: + eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm. +Proof. + induction sm; simpl; auto. + rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto. + erewrite <- eval_addressing_preserved; eauto. + destruct (eval_addressing _ sp _ _); auto. + rewrite IHsm; clear IHsm. destruct (eval_smem _ _); auto. + rewrite eval_sval_preserved; auto. +Qed. + +Lemma seval_condition_preserved cond lsv sm: + seval_condition (Bctx ge stk f sp rs0 m0) cond lsv sm = seval_condition (Bctx ge' stk' f' sp rs0 m0) cond lsv sm. +Proof. + unfold seval_condition. + rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto. + rewrite smem_eval_preserved; auto. +Qed. + +End SymbValPreserved. + +(** * ... *) + +Record sis_ok ctx (sis: sistate): Prop := { + OK_PRE: (sis.(si_pre) ctx); + OK_SMEM: eval_smem ctx sis.(si_smem) <> None; + OK_SREG: forall (r: reg), eval_sval ctx (si_sreg sis r) <> None +}. +Local Hint Resolve OK_PRE OK_SMEM OK_SREG: core. +Local Hint Constructors sis_ok: core. + +Lemma sem_sok ctx sis rs m: + sem_sistate ctx sis rs m -> sis_ok ctx sis. +Proof. + unfold sem_sistate; + econstructor; + intuition congruence. +Qed. + +(* NB: refinement of (symbolic) internal state *) +Record ristate := + { + (** [ris_smem] represents the current smem symbolic evaluations. + (we also recover the history of smem in ris_smem) *) + ris_smem: smem; + (** For the values in registers: + 1) we store a list of sval evaluations + 2) we encode the symbolic regset by a PTree + a boolean indicating the default sval *) + ris_input_init: bool; + ris_ok_sval: list sval; + ris_sreg:> PTree.t sval + }. + +Definition ris_sreg_get (ris: ristate) r: sval := + match PTree.get r ris with + | None => if ris_input_init ris then Sinput r else Sundef + | Some sv => sv + end. +Coercion ris_sreg_get: ristate >-> Funclass. + +Record ris_ok ctx (ris: ristate) : Prop := { + OK_RMEM: (eval_smem ctx (ris_smem ris)) <> None; + OK_RREG: forall sv, List.In sv (ris_ok_sval ris) -> eval_sval ctx sv <> None +}. +Local Hint Resolve OK_RMEM OK_RREG: core. +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 +}. +Local Hint Resolve OK_EQUIV MEM_EQ REG_EQ VALID_PRESERV: core. +Local Hint Constructors ris_refines: core. + +Record ris_simu ris1 ris2: Prop := { + SIMU_FAILS: forall sv, List.In sv ris2.(ris_ok_sval) -> List.In sv ris1.(ris_ok_sval); + SIMU_MEM: ris1.(ris_smem) = ris2.(ris_smem); + SIMU_REG: forall r, ris_sreg_get ris1 r = ris_sreg_get ris2 r +}. +Local Hint Resolve SIMU_FAILS SIMU_MEM SIMU_REG: core. +Local Hint Constructors ris_simu: core. +Local Hint Resolve sge_match: core. + +Lemma ris_simu_ok_preserv f1 f2 ris1 ris2 (ctx:simu_proof_context): + ris_simu ris1 ris2 -> ris_ok (bctx1 f1 ctx) ris1 -> ris_ok (bctx2 f2 ctx) ris2. +Proof. + intros SIMU OK; econstructor; eauto. + - erewrite <- SIMU_MEM; eauto. + unfold bctx2; erewrite smem_eval_preserved; eauto. + - unfold bctx2; intros; erewrite eval_sval_preserved; eauto. +Qed. + +Lemma ris_simu_correct f1 f2 ris1 ris2 (ctx:simu_proof_context) sis1 sis2 rs m: + ris_simu ris1 ris2 -> + ris_refines (bctx1 f1 ctx) ris1 sis1 -> + ris_refines (bctx2 f2 ctx) ris2 sis2 -> + sem_sistate (bctx1 f1 ctx) sis1 rs m -> + sem_sistate (bctx2 f2 ctx) sis2 rs m. +Proof. + intros RIS REF1 REF2 SEM. + (* destruct REF1. destruct REF2. *) + exploit sem_sok; eauto. + erewrite OK_EQUIV; eauto. + intros ROK1. + exploit ris_simu_ok_preserv; eauto. + intros ROK2. generalize ROK2; erewrite <- OK_EQUIV; eauto. + intros SOK2. + destruct SEM as (PRE & SMEM & SREG). + unfold sem_sistate; intuition eauto. + + erewrite <- MEM_EQ, <- SIMU_MEM; eauto. + unfold bctx2; erewrite smem_eval_preserved; eauto. + erewrite MEM_EQ; eauto. + + erewrite <- REG_EQ, <- SIMU_REG; eauto. + unfold bctx2; erewrite eval_sval_preserved; eauto. + erewrite REG_EQ; eauto. +Qed. + +Definition rfv_refines ctx (rfv sfv: sfval): Prop := + forall rs m t s, sem_sfval ctx rfv rs m t s <-> sem_sfval ctx sfv rs m t s. + +Definition rfv_simu (rfv1 rfv2: sfval): Prop := rfv1 = rfv2. + +Lemma rvf_simu_correct f1 f2 rfv1 rfv2 (ctx: simu_proof_context) sfv1 sfv2 rs m t s: + rfv_simu rfv1 rfv2 -> + rfv_refines (bctx1 f1 ctx) rfv1 sfv1 -> + rfv_refines (bctx2 f2 ctx) rfv2 sfv2 -> + sem_sfval (bctx1 f1 ctx) sfv1 rs m t s -> + sem_sfval (bctx2 f2 ctx) sfv2 rs m t s. +Proof. + unfold rfv_simu, rfv_refines; intros X REF1 REF2 SEM. subst. + rewrite <- REF2. + assert (sem_sfval (bctx1 f1 ctx) rfv2 rs m t s). { rewrite REF1; auto. } +Admitted. + +(* refinement of (symbolic) state *) +Inductive rstate := + | Rfinal (ris: ristate) (rfv: sfval) + | Rcond (cond: condition) (rargs: list_sval) (rifso rifnot: rstate) + | Rabort + . + +Inductive rst_simu: rstate -> rstate -> Prop := + | Rfinal_simu ris1 ris2 rfv1 rfv2: + ris_simu ris1 ris2 -> + rfv_simu rfv1 rfv2 -> + rst_simu (Rfinal ris1 rfv1) (Rfinal ris2 rfv2) + | Rcond_simu cond rargs rifso1 rifnot1 rifso2 rifnot2: + rst_simu rifso1 rifso2 -> + rst_simu rifnot1 rifnot2 -> + rst_simu (Rcond cond rargs rifso1 rifnot1) (Rcond cond rargs rifso2 rifnot2) + | Rabort_simu: rst_simu Rabort Rabort +(* TODO: extension à voir dans un second temps ! + | Rcond_skip cond rargs rifso1 rifnot1 rst: + rst_simu rifso1 rst -> + rst_simu rifnot1 rst -> + rst_simu (Rcond cond rargs rifso1 rifnot1) rst +*) + . + +(* Comment prend on en compte le ris en cours d'execution ??? *) +Inductive rst_refines ctx: (* Prop -> *) rstate -> sstate -> Prop := + | refines_Sfinal ris sis rfv sfv (*ok: Prop*) + (*OK: ris_ok ctx ris -> ok*) + (RIS: ris_refines ctx ris sis) + (RFV: ris_ok ctx ris -> rfv_refines ctx rfv sfv) + : rst_refines ctx (*ok*) (Rfinal ris rfv) (Sfinal sis sfv) + | refines_Scond cond rargs args sm rifso rifnot ifso ifnot (*ok1 ok2: Prop*) + (*OK1: ok2 -> ok1*) + (RCOND: (* ok2 -> *) seval_condition ctx cond rargs Sinit = seval_condition ctx cond args sm) + (REFso: seval_condition ctx cond rargs Sinit = Some true -> rst_refines ctx (*ok2*) rifso ifso) + (REFnot: seval_condition ctx cond rargs Sinit = Some false -> rst_refines ctx (*ok2*) rifnot ifnot) + : rst_refines ctx (*ok1*) (Rcond cond rargs rifso rifnot) (Scond cond args sm ifso ifnot) + | refines_Sabort + : rst_refines ctx Rabort Sabort + . + +Lemma rst_simu_correct rst1 rst2: + rst_simu rst1 rst2 -> + forall f1 f2 ctx st1 st2 (*ok1 ok2*), + rst_refines (*ok1*) (bctx1 f1 ctx) rst1 st1 -> + rst_refines (*ok2*) (bctx2 f2 ctx) rst2 st2 -> + (* ok1 -> ok2 -> *) + sstate_simu f1 f2 ctx st1 st2. +Proof. + induction 1; simpl; auto. + - (* final *) intros f1 f2 ctx st1 st2 REF1 REF2 t s1 SEM1. + inv REF1. inv REF2. inv SEM1. + exploit sem_sok; eauto. + rewrite OK_EQUIV; eauto. + intros RIS_OK1. + exploit (ris_simu_ok_preserv f1 f2); eauto. + intros RIS_OK2. intuition. + exploit ris_simu_correct; eauto. + exploit rvf_simu_correct; eauto. + simpl. + eexists; split. + + econstructor; eauto. + simpl. + admit. (* TODO: condition sur les tr_inputs: à ajouter plutôt dans le simu_proof_context ! *) + + admit. + - (* cond *) intros f1 f2 ctx st1 st2 REF1 REF2 t s1 SEM1. + inv REF1. inv REF2. inv SEM1. + destruct b; simpl. + + assert (TODO1: rst_refines (bctx1 f1 ctx) rifso1 ifso). admit. + assert (TODO2: rst_refines (bctx2 f2 ctx) rifso2 ifso0). admit. + exploit IHrst_simu1; eauto. + intros (s2 & X1 & X2). + exists s2; split; eauto. + econstructor; eauto. + * assert (TODO3: seval_condition (bctx2 f2 ctx) cond args0 sm0 = Some true). admit. + eauto. + * simpl; eauto. + + admit. + - (* abort *) intros f1 f2 ctx st1 st2 REF1 REF2 t s1 SEM1. + inv REF1. inv SEM1. +Admitted. diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index 3083ca71..c7a44153 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -1057,102 +1057,4 @@ Proof. intros (s3 & STEP2 & EQ2). clear STEP1; eexists; split; eauto. eapply equiv_state_trans; eauto. -Qed. - -(** * Preservation properties *) - -Section SymbValPreserved. - -Variable ge ge': BTL.genv. - -Hypothesis symbols_preserved_BTL: forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s. - -Hypothesis senv_preserved_BTL: Senv.equiv ge ge'. - -Lemma senv_find_symbol_preserved id: - Senv.find_symbol ge id = Senv.find_symbol ge' id. -Proof. - destruct senv_preserved_BTL as (A & B & C). congruence. -Qed. - -Lemma senv_symbol_address_preserved id ofs: - Senv.symbol_address ge id ofs = Senv.symbol_address ge' id ofs. -Proof. - unfold Senv.symbol_address. rewrite senv_find_symbol_preserved. - reflexivity. -Qed. - -Variable stk stk': list stackframe. -Variable f f': function. -Variable sp: val. -Variable rs0: regset. -Variable m0: mem. - -Lemma eval_sval_preserved sv: - eval_sval (Bctx ge stk f sp rs0 m0) sv = eval_sval (Bctx ge' stk' f' sp rs0 m0) sv. -Proof. - induction sv using sval_mut with (P0 := fun lsv => eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv) - (P1 := fun sm => eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) 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. - destruct (eval_addressing _ sp _ _); auto. - rewrite IHsv; auto. - + rewrite IHsv; clear IHsv. destruct (eval_sval _ _); auto. - rewrite IHsv0; auto. - + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto. - erewrite <- eval_addressing_preserved; eauto. - destruct (eval_addressing _ sp _ _); auto. - rewrite IHsv; clear IHsv. destruct (eval_smem _ _); auto. - rewrite IHsv1; auto. -Qed. - -Lemma seval_builtin_arg_preserved m: forall bs varg, - seval_builtin_arg (Bctx ge stk f sp rs0 m0) m bs varg -> - seval_builtin_arg (Bctx ge' stk' f' sp rs0 m0) m bs varg. -Proof. - induction 1; simpl. - all: try (constructor; auto). - - rewrite <- eval_sval_preserved. assumption. - - rewrite <- senv_symbol_address_preserved. assumption. - - rewrite senv_symbol_address_preserved. eapply seval_BA_addrglobal. -Qed. - -Lemma seval_builtin_args_preserved m lbs vargs: - seval_builtin_args (Bctx ge stk f sp rs0 m0) m lbs vargs -> - seval_builtin_args (Bctx ge' stk' f' sp rs0 m0) m lbs vargs. -Proof. - induction 1; constructor; eauto. - eapply seval_builtin_arg_preserved; auto. -Qed. - -Lemma list_sval_eval_preserved lsv: - eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv. -Proof. - induction lsv; simpl; auto. - rewrite eval_sval_preserved. destruct (eval_sval _ _); auto. - rewrite IHlsv; auto. -Qed. - -Lemma smem_eval_preserved sm: - eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm. -Proof. - induction sm; simpl; auto. - rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto. - erewrite <- eval_addressing_preserved; eauto. - destruct (eval_addressing _ sp _ _); auto. - rewrite IHsm; clear IHsm. destruct (eval_smem _ _); auto. - rewrite eval_sval_preserved; auto. -Qed. - -Lemma seval_condition_preserved cond lsv sm: - seval_condition (Bctx ge stk f sp rs0 m0) cond lsv sm = seval_condition (Bctx ge' stk' f' sp rs0 m0) cond lsv sm. -Proof. - unfold seval_condition. - rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto. - rewrite smem_eval_preserved; auto. -Qed. - -End SymbValPreserved. +Qed. \ No newline at end of file -- cgit From abfc8509ec4686924095c1328179fa06766dc496 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 2 Jun 2021 08:20:58 +0200 Subject: the current "high-level" specification of the simulation test will not work ! --- scheduling/BTL_SEsimuref.v | 94 +++++++++++++++++++++++++++++++++------------- scheduling/BTL_SEtheory.v | 58 +++++++++++++++++++++++----- scheduling/BTL_Scheduler.v | 9 ++++- 3 files changed, 124 insertions(+), 37 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v index af2159cb..65052310 100644 --- a/scheduling/BTL_SEsimuref.v +++ b/scheduling/BTL_SEsimuref.v @@ -182,8 +182,8 @@ Local Hint Resolve SIMU_FAILS SIMU_MEM SIMU_REG: core. Local Hint Constructors ris_simu: core. Local Hint Resolve sge_match: core. -Lemma ris_simu_ok_preserv f1 f2 ris1 ris2 (ctx:simu_proof_context): - ris_simu ris1 ris2 -> ris_ok (bctx1 f1 ctx) ris1 -> ris_ok (bctx2 f2 ctx) ris2. +Lemma ris_simu_ok_preserv f1 f2 ris1 ris2 (ctx:simu_proof_context f1 f2): + ris_simu ris1 ris2 -> ris_ok (bctx1 ctx) ris1 -> ris_ok (bctx2 ctx) ris2. Proof. intros SIMU OK; econstructor; eauto. - erewrite <- SIMU_MEM; eauto. @@ -191,12 +191,12 @@ Proof. - unfold bctx2; intros; erewrite eval_sval_preserved; eauto. Qed. -Lemma ris_simu_correct f1 f2 ris1 ris2 (ctx:simu_proof_context) sis1 sis2 rs m: +Lemma ris_simu_correct f1 f2 ris1 ris2 (ctx:simu_proof_context f1 f2) sis1 sis2 rs m: ris_simu ris1 ris2 -> - ris_refines (bctx1 f1 ctx) ris1 sis1 -> - ris_refines (bctx2 f2 ctx) ris2 sis2 -> - sem_sistate (bctx1 f1 ctx) sis1 rs m -> - sem_sistate (bctx2 f2 ctx) sis2 rs m. + ris_refines (bctx1 ctx) ris1 sis1 -> + ris_refines (bctx2 ctx) ris2 sis2 -> + sem_sistate (bctx1 ctx) sis1 rs m -> + sem_sistate (bctx2 ctx) sis2 rs m. Proof. intros RIS REF1 REF2 SEM. (* destruct REF1. destruct REF2. *) @@ -216,21 +216,59 @@ Proof. erewrite REG_EQ; eauto. Qed. -Definition rfv_refines ctx (rfv sfv: sfval): Prop := - forall rs m t s, sem_sfval ctx rfv rs m t s <-> sem_sfval ctx sfv rs m t s. +Definition option_refines ctx (orsv: option sval) (osv: option sval) := + match orsv, osv with + | Some rsv, Some sv => eval_sval ctx rsv = eval_sval ctx sv + | None, None => True + | _, _ => False + end. + +Definition sum_refines ctx (rsi: sval + ident) (si: sval + ident) := + match rsi, si with + | inl rsv, inl sv => eval_sval ctx rsv = eval_sval ctx sv + | inr id, inr id' => id = id' + | _, _ => False + end. + +Definition bargs_refines ctx (rargs: list (builtin_arg sval)) (args: list (builtin_arg sval)): Prop := + eval_list_builtin_sval ctx rargs = eval_list_builtin_sval ctx args. + +Inductive rfv_refines ctx: sfval -> sfval -> Prop := + | refines_Sgoto pc: rfv_refines ctx (Sgoto pc) (Sgoto pc) + | refines_Scall: forall sig rvos ros rargs args r pc + (SUM:sum_refines ctx rvos ros) + (LIST:eval_list_sval ctx rargs = eval_list_sval ctx args) + ,rfv_refines ctx (Scall sig rvos rargs r pc) (Scall sig ros args r pc) + | refines_Stailcall: forall sig rvos ros rargs args + (SUM:sum_refines ctx rvos ros) + (LIST:eval_list_sval ctx rargs = eval_list_sval ctx args) + ,rfv_refines ctx (Stailcall sig rvos rargs) (Stailcall sig ros args) + | refines_Sbuiltin: forall ef lbra lba br pc + (BARGS: bargs_refines ctx lbra lba) + ,rfv_refines ctx (Sbuiltin ef lbra br pc) (Sbuiltin ef lba br pc) + | refines_Sjumptable: forall rsv sv lpc + (VAL: eval_sval ctx rsv = eval_sval ctx sv) + ,rfv_refines ctx (Sjumptable rsv lpc) (Sjumptable sv lpc) + | refines_Sreturn: forall orsv osv + (OPT:option_refines ctx orsv osv) + ,rfv_refines ctx (Sreturn orsv) (Sreturn osv) +. Definition rfv_simu (rfv1 rfv2: sfval): Prop := rfv1 = rfv2. -Lemma rvf_simu_correct f1 f2 rfv1 rfv2 (ctx: simu_proof_context) sfv1 sfv2 rs m t s: +Local Hint Constructors sem_sfval equiv_state: core. + +Lemma rvf_simu_correct f1 f2 rfv1 rfv2 (ctx: simu_proof_context f1 f2) sfv1 sfv2 rs m t s: rfv_simu rfv1 rfv2 -> - rfv_refines (bctx1 f1 ctx) rfv1 sfv1 -> - rfv_refines (bctx2 f2 ctx) rfv2 sfv2 -> - sem_sfval (bctx1 f1 ctx) sfv1 rs m t s -> - sem_sfval (bctx2 f2 ctx) sfv2 rs m t s. + rfv_refines (bctx1 ctx) rfv1 sfv1 -> + rfv_refines (bctx2 ctx) rfv2 sfv2 -> + sem_sfval (bctx1 ctx) sfv1 rs m t s -> + exists s', sem_sfval (bctx2 ctx) sfv2 rs m t s' /\ equiv_state s s'. Proof. - unfold rfv_simu, rfv_refines; intros X REF1 REF2 SEM. subst. - rewrite <- REF2. - assert (sem_sfval (bctx1 f1 ctx) rfv2 rs m t s). { rewrite REF1; auto. } + unfold rfv_simu; intros X REF1 REF2 SEM. subst. + unfold bctx2; destruct REF1; inv REF2; inv SEM; simpl. + - eexists; split; eauto; simpl. + (* eapply State_equiv; eauto. NE MARCHE PAS ! *) Admitted. (* refinement of (symbolic) state *) @@ -277,11 +315,11 @@ Inductive rst_refines ctx: (* Prop -> *) rstate -> sstate -> Prop := Lemma rst_simu_correct rst1 rst2: rst_simu rst1 rst2 -> - forall f1 f2 ctx st1 st2 (*ok1 ok2*), - rst_refines (*ok1*) (bctx1 f1 ctx) rst1 st1 -> - rst_refines (*ok2*) (bctx2 f2 ctx) rst2 st2 -> + forall f1 f2 (ctx: simu_proof_context f1 f2) st1 st2 (*ok1 ok2*), + rst_refines (*ok1*) (bctx1 ctx) rst1 st1 -> + rst_refines (*ok2*) (bctx2 ctx) rst2 st2 -> (* ok1 -> ok2 -> *) - sstate_simu f1 f2 ctx st1 st2. + sstate_simu ctx st1 st2. Proof. induction 1; simpl; auto. - (* final *) intros f1 f2 ctx st1 st2 REF1 REF2 t s1 SEM1. @@ -293,25 +331,29 @@ Proof. intros RIS_OK2. intuition. exploit ris_simu_correct; eauto. exploit rvf_simu_correct; eauto. - simpl. + simpl. (* eexists; split. + econstructor; eauto. simpl. - admit. (* TODO: condition sur les tr_inputs: à ajouter plutôt dans le simu_proof_context ! *) + clear SIS. + admit. (* TODO: condition sur les tr_inputs du simu_proof_context ! *) + (* TODO: le rfv_refines est trop sémantique ! *) + admit. - (* cond *) intros f1 f2 ctx st1 st2 REF1 REF2 t s1 SEM1. inv REF1. inv REF2. inv SEM1. destruct b; simpl. - + assert (TODO1: rst_refines (bctx1 f1 ctx) rifso1 ifso). admit. - assert (TODO2: rst_refines (bctx2 f2 ctx) rifso2 ifso0). admit. + + assert (TODO1: rst_refines (bctx1 ctx) rifso1 ifso). admit. + assert (TODO2: rst_refines (bctx2 ctx) rifso2 ifso0). admit. exploit IHrst_simu1; eauto. intros (s2 & X1 & X2). exists s2; split; eauto. econstructor; eauto. - * assert (TODO3: seval_condition (bctx2 f2 ctx) cond args0 sm0 = Some true). admit. + * assert (TODO3: seval_condition (bctx2 ctx) cond args0 sm0 = Some true). admit. eauto. * simpl; eauto. + admit. - (* abort *) intros f1 f2 ctx st1 st2 REF1 REF2 t s1 SEM1. inv REF1. inv SEM1. +*) + Admitted. diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index c7a44153..72789121 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -1022,38 +1022,76 @@ Qed. (** * High-Level specification of the symbolic simulation test as predicate [symbolic_simu] *) -Record simu_proof_context := Sctx { +(* +Definition equiv_input_regs (f1 f2: BTL.function): Prop := + (forall pc, (fn_code f1)!pc = None <-> (fn_code f2)!pc = None) + /\ (forall pc ib1 ib2, (fn_code f1)!pc = Some ib1 -> (fn_code f2)!pc = Some ib2 -> ib1.(input_regs) = ib2.(input_regs)). + +Lemma equiv_input_regs_union f1 f2: + equiv_input_regs f1 f2 -> forall tbl, union_inputs f1 tbl = union_inputs f2 tbl. +Proof. + intros (EQNone & EQSome). induction tbl as [|pc l']; simpl; auto. + generalize (EQNone pc) (EQSome pc); clear EQNone EQSome; intros EQN EQS. + do 2 autodestruct; intuition; try_simplify_someHyps. + intros; exploit EQS; eauto; clear EQS. congruence. +Qed. + +Lemma equiv_input_regs_pre f1 f2 tbl or: + equiv_input_regs f1 f2 -> pre_inputs f1 tbl or = pre_inputs f2 tbl or. +Proof. + intros; unfold pre_inputs; erewrite equiv_input_regs_union; auto. +Qed. +*) + +Record simu_proof_context {f1 f2: BTL.function} := Sctx { sge1: BTL.genv; sge2: BTL.genv; sge_match: forall s, Genv.find_symbol sge1 s = Genv.find_symbol sge2 s; sstk1: list BTL.stackframe; sstk2: list BTL.stackframe; sstk_equiv: list_forall2 equiv_stackframe sstk1 sstk2; + (* inputs_equiv: equiv_input_regs f1 f2;*) (* TODO a-t-on besoin de ça ? *) ssp: val; srs0: regset; sm0: mem }. +Arguments simu_proof_context: clear implicits. -Definition bctx1 f1 (ctx: simu_proof_context):= Bctx ctx.(sge1) ctx.(sstk1) f1 ctx.(ssp) ctx.(srs0) ctx.(sm0). -Definition bctx2 f2 (ctx: simu_proof_context):= Bctx ctx.(sge2) ctx.(sstk2) f2 ctx.(ssp) ctx.(srs0) ctx.(sm0). +Definition bctx1 {f1 f2} (ctx: simu_proof_context f1 f2):= Bctx ctx.(sge1) ctx.(sstk1) f1 ctx.(ssp) ctx.(srs0) ctx.(sm0). +Definition bctx2 {f1 f2} (ctx: simu_proof_context f1 f2):= Bctx ctx.(sge2) ctx.(sstk2) f2 ctx.(ssp) ctx.(srs0) ctx.(sm0). -Definition sstate_simu f1 f2 (ctx: simu_proof_context) (st1 st2: sstate) := - forall t s1, sem_sstate (bctx1 f1 ctx) t s1 st1 -> - exists s2, sem_sstate (bctx2 f2 ctx) t s2 st2 /\ equiv_state s1 s2. -Definition symbolic_simu f1 f2 ib1 ib2: Prop := forall ctx, sstate_simu f1 f2 ctx (sexec f1 ib1) (sexec f2 ib2). +(* TODO: A REVOIR. L'approche suivie ne marche pas !!! + +le [equiv_state] ci-dessous n'est pas assez général + => il faut un [match_state] qui va dépendre de [BTL_Scheduler.match_function] (dans le [match_stackframe]). + +Or, le [sstate_simu] qu'on cherche à définir ici, c'était pour définir ce [match_function]: circularité ! + +Une solution: définir le match_function à l'aide d'un [iblock_step_simu] ? + +Pas sûr que ça marche, on aura aussi la dépendance circulaire entre [simu_proof_context] et [match_function] ! + +Autre solution: définir [sfval_simu] syntaxiquement comme dans [RTLpath_SEtheory] pour éviter le problème de circularité ! + +*) +Definition sstate_simu {f1 f2} (ctx: simu_proof_context f1 f2) (st1 st2: sstate) := + forall t s1, sem_sstate (bctx1 ctx) t s1 st1 -> + exists s2, sem_sstate (bctx2 ctx) t s2 st2 /\ equiv_state s1 s2. + +Definition symbolic_simu f1 f2 ib1 ib2: Prop := forall (ctx: simu_proof_context f1 f2), sstate_simu ctx (sexec f1 ib1) (sexec f2 ib2). Theorem symbolic_simu_correct f1 f2 ib1 ib2: symbolic_simu f1 f2 ib1 ib2 -> - forall ctx t s1, iblock_step tr_inputs (sge1 ctx) (sstk1 ctx) f1 (ssp ctx) (srs0 ctx) (sm0 ctx) ib1 t s1 -> + forall (ctx: simu_proof_context f1 f2) t s1, iblock_step tr_inputs (sge1 ctx) (sstk1 ctx) f1 (ssp ctx) (srs0 ctx) (sm0 ctx) ib1 t s1 -> exists s2, iblock_step tr_inputs (sge2 ctx) (sstk2 ctx) f2 (ssp ctx) (srs0 ctx) (sm0 ctx) ib2 t s2 /\ equiv_state s1 s2. Proof. unfold symbolic_simu, sstate_simu. intros SIMU ctx t s1 STEP1. - exploit (sexec_correct (bctx1 f1 ctx)); simpl; eauto. + exploit (sexec_correct (bctx1 ctx)); simpl; eauto. intros; exploit SIMU; eauto. intros (s2 & SEM1 & EQ1). - exploit (sexec_exact (bctx2 f2 ctx)); simpl; eauto. + exploit (sexec_exact (bctx2 ctx)); simpl; eauto. intros (s3 & STEP2 & EQ2). clear STEP1; eexists; split; eauto. eapply equiv_state_trans; eauto. diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v index b479204c..bcddcf5d 100644 --- a/scheduling/BTL_Scheduler.v +++ b/scheduling/BTL_Scheduler.v @@ -15,7 +15,8 @@ Record match_function (f1 f2: BTL.function): Prop := { preserv_fnparams: fn_params f1 = fn_params f2; preserv_fnstacksize: fn_stacksize f1 = fn_stacksize f2; preserv_entrypoint: fn_entrypoint f1 = fn_entrypoint f2; - symbolic_simu_ok: forall pc ib1, (fn_code f1)!pc = Some ib1 -> + (* preserv_inputs: equiv_input_regs f1 f2; TODO: a-t-on besoin de ça ? *) + symbolic_simu_ok: forall pc ib1, (fn_code f1)!pc = Some ib1 -> exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2); }. @@ -23,6 +24,12 @@ Local Open Scope error_monad_scope. Definition check_symbolic_simu (f tf: BTL.function): res unit := OK tt. (* TODO: fixme *) +(* TODO: a-t-on besoin de ça ? +Lemma check_symbolic_simu_input_equiv x f1 f2: + check_symbolic_simu f1 f2 = OK x -> equiv_input_regs f1 f2. +Admitted. +*) + Lemma check_symbolic_simu_correct x f1 f2: check_symbolic_simu f1 f2 = OK x -> forall pc ib1, (fn_code f1)!pc = Some ib1 -> -- cgit