From 37c8b2a474bb07890f21db0535b5886bec4e4e6d Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 2 Jun 2021 14:48:59 +0200 Subject: fix the definition of [symbolic_simu] in BTL_SEtheory --- scheduling/BTL_SEsimuref.v | 116 ++--------------- scheduling/BTL_SEtheory.v | 307 +++++++++++++++++++++++++++++++++++---------- 2 files changed, 251 insertions(+), 172 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v index 65052310..e9ae11e0 100644 --- a/scheduling/BTL_SEsimuref.v +++ b/scheduling/BTL_SEsimuref.v @@ -1,9 +1,7 @@ (** 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". + Ceci est un "bac à sable". TODO: A REVOIR COMPLETEMENT. Introduire "fake" hash-consing - 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, @@ -17,106 +15,6 @@ 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 := { @@ -187,8 +85,8 @@ Lemma ris_simu_ok_preserv f1 f2 ris1 ris2 (ctx:simu_proof_context f1 f2): 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. + erewrite <- smem_eval_preserved; eauto. + - intros; erewrite <- eval_sval_preserved; eauto. Qed. Lemma ris_simu_correct f1 f2 ris1 ris2 (ctx:simu_proof_context f1 f2) sis1 sis2 rs m: @@ -199,7 +97,6 @@ Lemma ris_simu_correct f1 f2 ris1 ris2 (ctx:simu_proof_context f1 f2) sis1 sis2 sem_sistate (bctx2 ctx) sis2 rs m. Proof. intros RIS REF1 REF2 SEM. - (* destruct REF1. destruct REF2. *) exploit sem_sok; eauto. erewrite OK_EQUIV; eauto. intros ROK1. @@ -209,13 +106,15 @@ Proof. 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 <- smem_eval_preserved; eauto. erewrite MEM_EQ; eauto. + erewrite <- REG_EQ, <- SIMU_REG; eauto. - unfold bctx2; erewrite eval_sval_preserved; eauto. + erewrite <- eval_sval_preserved; eauto. erewrite REG_EQ; eauto. Qed. +(* TODO: + 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 @@ -357,3 +256,4 @@ Proof. *) Admitted. +*) \ No newline at end of file diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index 72789121..c437846e 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -16,7 +16,7 @@ Require Import RTL BTL OptionMonad. Record iblock_exec_context := Bctx { cge: BTL.genv; - cstk: list stackframe; + (* cstk: list stackframe; *) (* having the stack here does seem not a good idea *) cf: function; csp: val; crs0: regset; @@ -400,39 +400,39 @@ Definition sfind_function ctx (svos : sval + ident): option fundef := Import ListNotations. Local Open Scope list_scope. -Inductive sem_sfval ctx: sfval -> regset -> mem -> trace -> state -> Prop := +Inductive sem_sfval ctx stk: sfval -> regset -> mem -> trace -> state -> Prop := | exec_Sgoto pc rs m: - sem_sfval ctx (Sgoto pc) rs m E0 (State (cstk ctx) (cf ctx) (csp ctx) pc (tr_inputs ctx.(cf) [pc] None rs) m) - | exec_Sreturn stk osv rs m m' v: - (csp ctx) = (Vptr stk Ptrofs.zero) -> - Mem.free m stk 0 (cf ctx).(fn_stacksize) = Some m' -> + sem_sfval ctx stk (Sgoto pc) rs m E0 (State stk (cf ctx) (csp ctx) pc (tr_inputs ctx.(cf) [pc] None rs) m) + | exec_Sreturn pstk osv rs m m' v: + (csp ctx) = (Vptr pstk Ptrofs.zero) -> + Mem.free m pstk 0 (cf ctx).(fn_stacksize) = Some m' -> match osv with Some sv => eval_sval ctx sv | None => Some Vundef end = Some v -> - sem_sfval ctx (Sreturn osv) rs m - E0 (Returnstate (cstk ctx) v m') + sem_sfval ctx stk (Sreturn osv) rs m + E0 (Returnstate stk v m') | exec_Scall rs m sig svos lsv args res pc fd: sfind_function ctx svos = Some fd -> funsig fd = sig -> eval_list_sval ctx lsv = Some args -> - sem_sfval ctx (Scall sig svos lsv res pc) rs m - E0 (Callstate (Stackframe res (cf ctx) (csp ctx) pc (tr_inputs ctx.(cf) [pc] (Some res) rs)::cstk ctx) fd args m) - | exec_Stailcall stk rs m sig svos args fd m' lsv: + sem_sfval ctx stk (Scall sig svos lsv res pc) rs m + E0 (Callstate (Stackframe res (cf ctx) (csp ctx) pc (tr_inputs ctx.(cf) [pc] (Some res) rs)::stk) fd args m) + | exec_Stailcall pstk rs m sig svos args fd m' lsv: sfind_function ctx svos = Some fd -> funsig fd = sig -> - (csp ctx) = Vptr stk Ptrofs.zero -> - Mem.free m stk 0 (cf ctx).(fn_stacksize) = Some m' -> + (csp ctx) = Vptr pstk Ptrofs.zero -> + Mem.free m pstk 0 (cf ctx).(fn_stacksize) = Some m' -> eval_list_sval ctx lsv = Some args -> - sem_sfval ctx (Stailcall sig svos lsv) rs m - E0 (Callstate (cstk ctx) fd args m') + sem_sfval ctx stk (Stailcall sig svos lsv) rs m + E0 (Callstate stk fd args m') | exec_Sbuiltin m' rs m vres res pc t sargs ef vargs: seval_builtin_args ctx m sargs vargs -> external_call ef (cge ctx) vargs m t vres m' -> - sem_sfval ctx (Sbuiltin ef sargs res pc) rs m - t (State (cstk ctx) (cf ctx) (csp ctx) pc (regmap_setres res vres (tr_inputs (cf ctx) [pc] (reg_builtin_res res) rs)) m') + sem_sfval ctx stk (Sbuiltin ef sargs res pc) rs m + t (State stk (cf ctx) (csp ctx) pc (regmap_setres res vres (tr_inputs (cf ctx) [pc] (reg_builtin_res res) rs)) m') | exec_Sjumptable sv tbl pc' n rs m: eval_sval ctx sv = Some (Vint n) -> list_nth_z tbl (Int.unsigned n) = Some pc' -> - sem_sfval ctx (Sjumptable sv tbl) rs m - E0 (State (cstk ctx) (cf ctx) (csp ctx) pc' (tr_inputs ctx.(cf) tbl None rs) m) + sem_sfval ctx stk (Sjumptable sv tbl) rs m + E0 (State stk (cf ctx) (csp ctx) pc' (tr_inputs ctx.(cf) tbl None rs) m) . (* Syntax and Semantics of symbolic internal states *) @@ -470,10 +470,10 @@ Definition sexec_final_sfv (i: final) (sis: sistate): sfval := Local Hint Constructors sem_sfval: core. -Lemma sexec_final_svf_correct ctx i sis t rs m s: +Lemma sexec_final_svf_correct ctx stk i sis t rs m s: sem_sistate ctx sis rs m -> - final_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s -> - sem_sfval ctx (sexec_final_sfv i sis) rs m t s. + final_step tr_inputs (cge ctx) stk (cf ctx) (csp ctx) rs m i t s -> + sem_sfval ctx stk (sexec_final_sfv i sis) rs m t s. Proof. intros (PRE&MEM®). destruct 1; subst; try_simplify_someHyps; simpl; intros; try autodestruct; eauto. @@ -493,10 +493,10 @@ Qed. Local Hint Constructors final_step: core. Local Hint Resolve seval_builtin_args_exact: core. -Lemma sexec_final_svf_exact ctx i sis t rs m s: +Lemma sexec_final_svf_exact ctx stk i sis t rs m s: sem_sistate ctx sis rs m -> - sem_sfval ctx (sexec_final_sfv i sis) rs m t s - -> final_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s. + sem_sfval ctx stk (sexec_final_sfv i sis) rs m t s + -> final_step tr_inputs (cge ctx) stk (cf ctx) (csp ctx) rs m i t s. Proof. intros (PRE&MEM®). destruct i; simpl; intros LAST; inv LAST; eauto. @@ -705,19 +705,61 @@ Inductive sstate := | Sabort . +(* outcome of a symbolic execution path *) +Record soutcome := sout { + so_sis: sistate; + so_svf: sfval; +}. + +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 + run_sem_isstate ctx (if b then ifso else ifnot) + | _ => None + end. + (* transition (t,s) produced by a sstate in initial context ctx *) -Inductive sem_sstate ctx t s: sstate -> Prop := +Inductive sem_sstate ctx stk t s: sstate -> Prop := | sem_Sfinal sis sfv rs m (SIS: sem_sistate ctx sis (str_regs (cf ctx) sfv rs) m) - (SFV: sem_sfval ctx sfv rs m t s) - : sem_sstate ctx t s (Sfinal sis sfv) + (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) - (SELECT: sem_sstate ctx t s (if b then ifso else ifnot)) - : sem_sstate ctx t s (Scond cond args sm ifso ifnot) + (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) (* NB: Sabort: fails to produce a transition *) . +Lemma sem_sstate_run ctx stk st t s: + sem_sstate ctx stk t s st -> + exists sis sfv rs m, + run_sem_isstate ctx st = Some (sout sis sfv) + /\ sem_sistate ctx sis (str_regs (cf ctx) sfv rs) m + /\ sem_sfval ctx stk sfv rs m t s + . +Proof. + induction 1; simpl; try_simplify_someHyps; do 4 eexists; intuition eauto. +Qed. + +Local Hint Resolve sem_Sfinal: core. + +Lemma run_sem_sstate ctx st sis sfv: + run_sem_isstate ctx st = Some (sout sis sfv) -> + forall rs m stk s t, + sem_sistate ctx sis (str_regs (cf ctx) sfv rs) m -> + sem_sfval ctx stk sfv rs m t s -> + sem_sstate ctx stk t s st + . +Proof. + induction st; simpl; try_simplify_someHyps. + autodestruct; intros; econstructor; eauto. + autodestruct; eauto. +Qed. + + (** * Idée de l'execution symbolique en Continuation Passing Style [k] ci-dessous est la continuation (c-a-d. la suite de la construction de l'arbre qu'on va appliquer dans chaque branche) @@ -755,14 +797,14 @@ Local Hint Constructors sem_sstate: core. Local Hint Resolve sexec_op_correct sexec_final_svf_correct tr_sis_regs_correct_aux tr_sis_regs_correct sexec_load_TRAP_correct sexec_store_correct sis_init_correct: core. -Lemma sexec_rec_correct ctx t s ib rs m rs1 m1 ofin +Lemma sexec_rec_correct ctx stk t s ib rs m rs1 m1 ofin (ISTEP: iblock_istep (cge ctx) (csp ctx) rs m ib rs1 m1 ofin): forall sis k (SIS: sem_sistate ctx sis rs m) (CONT: match ofin with - | None => forall sis', sem_sistate ctx sis' rs1 m1 -> sem_sstate ctx t s (k sis') - | Some fin => final_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs1 m1 fin t s + | None => forall sis', sem_sistate ctx sis' rs1 m1 -> sem_sstate ctx stk t s (k sis') + | Some fin => final_step tr_inputs (cge ctx) stk (cf ctx) (csp ctx) rs1 m1 fin t s end), - sem_sstate ctx t s (sexec_rec (cf ctx) ib sis k). + sem_sstate ctx stk t s (sexec_rec (cf ctx) ib sis k). Proof. induction ISTEP; simpl; try autodestruct; eauto. (* final value *) @@ -780,9 +822,9 @@ Qed. (* NB: each concrete execution can be executed on the symbolic state (produced from [sexec]) (sexec is a correct over-approximation) *) -Theorem sexec_correct ctx ib t s: - iblock_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s -> - sem_sstate ctx t s (sexec (cf ctx) ib). +Theorem sexec_correct ctx stk ib t s: + iblock_step tr_inputs (cge ctx) stk (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s -> + sem_sstate ctx stk t s (sexec (cf ctx) ib). Proof. destruct 1 as (rs' & m' & fin & ISTEP & FSTEP). eapply sexec_rec_correct; simpl; eauto. @@ -812,10 +854,10 @@ Qed. Local Hint Constructors equiv_stackframe list_forall2: core. Local Hint Resolve regmap_setres_eq equiv_stack_refl equiv_stack_refl: core. -Lemma sem_sfval_equiv rs1 rs2 ctx sfv m t s: - sem_sfval ctx sfv rs1 m t s -> +Lemma sem_sfval_equiv rs1 rs2 ctx stk sfv m t s: + sem_sfval ctx stk sfv rs1 m t s -> (forall r, (str_regs (cf ctx) sfv rs1)#r = (str_regs (cf ctx) sfv rs2)#r) -> - exists s', sem_sfval ctx sfv rs2 m t s' /\ equiv_state s s'. + exists s', sem_sfval ctx stk sfv rs2 m t s' /\ equiv_state s s'. Proof. unfold str_regs. destruct 1; simpl in *; intros; subst; eexists; split; econstructor; eauto; try congruence. @@ -877,9 +919,9 @@ Qed. Local Hint Resolve sexec_op_preserves_abort sexec_load_preserves_abort sexec_store_preserves_abort sem_sistate_tr_sis_exclude_abort: core. -Lemma sexec_exclude_abort ctx ib t s1: forall sis k - (SEXEC: sem_sstate ctx t s1 (sexec_rec (cf ctx) ib sis k)) - (CONT: forall sis', sem_sstate ctx t s1 (k sis') -> (abort_sistate ctx sis') -> False) +Lemma sexec_exclude_abort ctx stk ib t s1: forall sis k + (SEXEC: sem_sstate ctx stk t s1 (sexec_rec (cf ctx) ib sis k)) + (CONT: forall sis', sem_sstate ctx stk t s1 (k sis') -> (abort_sistate ctx sis') -> False) (ABORT: abort_sistate ctx sis), False. Proof. @@ -952,16 +994,16 @@ Qed. Local Hint Resolve sexec_op_abort sexec_load_TRAP_abort sexec_store_abort sexec_final_svf_exact: core. -Lemma sexec_rec_exact ctx ib t s1: forall sis k - (SEXEC: sem_sstate ctx t s1 (sexec_rec (cf ctx) ib sis k)) +Lemma sexec_rec_exact ctx stk ib t s1: forall sis k + (SEXEC: sem_sstate ctx stk t s1 (sexec_rec (cf ctx) ib sis k)) rs m (SIS: sem_sistate ctx sis rs m) - (CONT: forall sis', sem_sstate ctx t s1 (k sis') -> (abort_sistate ctx sis') -> False) + (CONT: forall sis', sem_sstate ctx stk t s1 (k sis') -> (abort_sistate ctx sis') -> False) , match iblock_istep_run (cge ctx) (csp ctx) ib rs m with | Some (out rs' m' (Some fin)) => - exists s2, final_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs' m' fin t s2 /\ equiv_state s1 s2 - | Some (out rs' m' None) => exists sis', (sem_sstate ctx t s1 (k sis')) /\ (sem_sistate ctx sis' rs' m') + exists s2, final_step tr_inputs (cge ctx) stk (cf ctx) (csp ctx) rs' m' fin t s2 /\ equiv_state s1 s2 + | Some (out rs' m' None) => exists sis', (sem_sstate ctx stk t s1 (k sis')) /\ (sem_sistate ctx sis' rs' m') | None => False end. Proof. @@ -1004,9 +1046,9 @@ Qed. (* NB: each execution of a symbolic state (produced from [sexec]) represents a concrete execution (sexec is exact). *) -Theorem sexec_exact ctx ib t s1: - sem_sstate ctx t s1 (sexec (cf ctx) ib) -> - exists s2, iblock_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s2 +Theorem sexec_exact ctx stk ib t s1: + sem_sstate ctx stk t s1 (sexec (cf ctx) ib) -> + exists s2, iblock_step tr_inputs (cge ctx) stk (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s2 /\ equiv_state s1 s2. Proof. intros; exploit sexec_rec_exact; eauto. @@ -1047,9 +1089,6 @@ 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; @@ -1057,24 +1096,69 @@ Record simu_proof_context {f1 f2: BTL.function} := Sctx { }. Arguments simu_proof_context: clear implicits. -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 bctx1 {f1 f2} (ctx: simu_proof_context f1 f2):= Bctx ctx.(sge1) f1 ctx.(ssp) ctx.(srs0) ctx.(sm0). +Definition bctx2 {f1 f2} (ctx: simu_proof_context f1 f2):= Bctx ctx.(sge2) f2 ctx.(ssp) ctx.(srs0) ctx.(sm0). + +(* NOTE: we need to mix semantical simulation and syntactic definition on [sfval] in order to abstract + the [match_states] of BTL_Schedulerproof. + Indeed, the [match_states] involves [match_function] in [match_stackframe]. + And, here, we aim to define a notion of simulation for defining [match_function]. -(* TODO: A REVOIR. L'approche suivie ne marche pas !!! + A syntactic definition of the simulation on [sfval] avoids the circularity issue. -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é ! +Inductive optsv_simu {f1 f2: function} (ctx: simu_proof_context f1 f2): (option sval) -> (option sval) -> Prop := + | Ssome_simu sv1 sv2: + eval_sval (bctx1 ctx) sv1 = eval_sval (bctx2 ctx) sv2 + -> optsv_simu ctx (Some sv1) (Some sv2) + | Snone_simu: optsv_simu ctx None None + . -Une solution: définir le match_function à l'aide d'un [iblock_step_simu] ? +Inductive svident_simu {f1 f2: function} (ctx: simu_proof_context f1 f2): (sval + ident) -> (sval + ident) -> Prop := + | Sleft_simu sv1 sv2: + eval_sval (bctx1 ctx) sv1 = eval_sval (bctx2 ctx) sv2 + -> svident_simu ctx (inl sv1) (inl sv2) + | Sright_simu id1 id2: + id1 = id2 + -> svident_simu ctx (inr id1) (inr id2) + . -Pas sûr que ça marche, on aura aussi la dépendance circulaire entre [simu_proof_context] et [match_function] ! +Definition bargs_simu {f1 f2: function} (ctx: simu_proof_context f1 f2) (args1 args2: list (builtin_arg sval)): Prop := + eval_list_builtin_sval (bctx1 ctx) args1 = eval_list_builtin_sval (bctx2 ctx) args2. + +Inductive sfv_simu {f1 f2} (ctx: simu_proof_context f1 f2): sfval -> sfval -> Prop := + | Sgoto_simu pc: sfv_simu ctx (Sgoto pc) (Sgoto pc) + | Scall_simu sig ros1 ros2 args1 args2 r pc + (SVID: svident_simu ctx ros1 ros2) + (ARGS:eval_list_sval (bctx1 ctx) args1 = eval_list_sval (bctx2 ctx) args2) + :sfv_simu ctx (Scall sig ros1 args1 r pc) (Scall sig ros2 args2 r pc) + | Stailcall_simu sig ros1 ros2 args1 args2 + (SVID: svident_simu ctx ros1 ros2) + (ARGS:eval_list_sval (bctx1 ctx) args1 = eval_list_sval (bctx2 ctx) args2) + :sfv_simu ctx (Stailcall sig ros1 args1) (Stailcall sig ros2 args2) + | Sbuiltin_simu ef lba1 lba2 br pc + (BARGS: bargs_simu ctx lba1 lba2) + :sfv_simu ctx (Sbuiltin ef lba1 br pc) (Sbuiltin ef lba2 br pc) + | Sjumptable_simu sv1 sv2 lpc + (VAL: eval_sval (bctx1 ctx) sv1 = eval_sval (bctx2 ctx) sv2) + :sfv_simu ctx (Sjumptable sv1 lpc) (Sjumptable sv2 lpc) + | simu_Sreturn osv1 osv2 + (OPT:optsv_simu ctx osv1 osv2) + :sfv_simu ctx (Sreturn osv1) (Sreturn osv2) +. -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): Prop := + forall sis1 sfv1, run_sem_isstate (bctx1 ctx) st1 = Some (sout sis1 sfv1) -> + exists sis2 sfv2, run_sem_isstate (bctx2 ctx) st2 = Some (sout sis2 sfv2) /\ sfv_simu ctx sfv1 sfv2 + . + +Definition symbolic_simu f1 f2 ib1 ib2: Prop := forall (ctx: simu_proof_context f1 f2), sstate_simu ctx (sexec f1 ib1) (sexec f2 ib2). +(* REM. L'approche suivie initialement ne marche pas !!! *) +(* 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. @@ -1095,4 +1179,99 @@ Proof. intros (s3 & STEP2 & EQ2). clear STEP1; eexists; split; eauto. eapply equiv_state_trans; eauto. -Qed. \ No newline at end of file +Qed. +*) + +(** * Preservation properties *) + +Section SymbValPreserved. + +Variable f1 f2: function. + +Hypothesis ctx: simu_proof_context f1 f2. +Local Hint Resolve sge_match: core. + +Lemma eval_sval_preserved sv: + eval_sval (bctx1 ctx) sv = eval_sval (bctx2 ctx) sv. +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. + destruct (eval_addressing _ _ _ _); 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 _ _ _ _); auto. + rewrite IHsv; clear IHsv. destruct (eval_smem _ _); auto. + rewrite IHsv1; auto. +Qed. + +Lemma list_sval_eval_preserved lsv: + eval_list_sval (bctx1 ctx) lsv = eval_list_sval (bctx2 ctx) 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 (bctx1 ctx) sm = eval_smem (bctx2 ctx) sm. +Proof. + induction sm; simpl; auto. + rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto. + erewrite eval_addressing_preserved; eauto. + destruct (eval_addressing _ _ _ _); auto. + rewrite IHsm; clear IHsm. destruct (eval_smem _ _); auto. + rewrite eval_sval_preserved; auto. +Qed. + +Lemma seval_condition_preserved cond lsv sm: + seval_condition (bctx1 ctx) cond lsv sm = seval_condition (bctx2 ctx) cond lsv sm. +Proof. + unfold seval_condition. + rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto. + rewrite smem_eval_preserved; auto. +Qed. + +Hypothesis senv_preserved_BTL: Senv.equiv (sge1 ctx) (sge2 ctx). + +Lemma senv_find_symbol_preserved id: + Senv.find_symbol (sge1 ctx) id = Senv.find_symbol (sge2 ctx) id. +Proof. + destruct senv_preserved_BTL as (A & B & C). congruence. +Qed. + +Lemma senv_symbol_address_preserved id ofs: + Senv.symbol_address (sge1 ctx) id ofs = Senv.symbol_address (sge2 ctx) id ofs. +Proof. + unfold Senv.symbol_address. rewrite senv_find_symbol_preserved. + reflexivity. +Qed. + +Lemma seval_builtin_arg_preserved m: forall bs varg, + seval_builtin_arg (bctx1 ctx) m bs varg -> + seval_builtin_arg (bctx2 ctx) 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 (bctx1 ctx) m lbs vargs -> + seval_builtin_args (bctx2 ctx) m lbs vargs. +Proof. + induction 1; constructor; eauto. + eapply seval_builtin_arg_preserved; auto. +Qed. + +End SymbValPreserved. + -- cgit From 79cca6a66cbad09f298e0d3b69974c47a8327fc0 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 2 Jun 2021 14:58:35 +0200 Subject: minor renaming --- scheduling/BTL_SEtheory.v | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index c437846e..7f00e46f 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -470,7 +470,7 @@ Definition sexec_final_sfv (i: final) (sis: sistate): sfval := Local Hint Constructors sem_sfval: core. -Lemma sexec_final_svf_correct ctx stk i sis t rs m s: +Lemma sexec_final_sfv_correct ctx stk i sis t rs m s: sem_sistate ctx sis rs m -> final_step tr_inputs (cge ctx) stk (cf ctx) (csp ctx) rs m i t s -> sem_sfval ctx stk (sexec_final_sfv i sis) rs m t s. @@ -493,7 +493,7 @@ Qed. Local Hint Constructors final_step: core. Local Hint Resolve seval_builtin_args_exact: core. -Lemma sexec_final_svf_exact ctx stk i sis t rs m s: +Lemma sexec_final_sfv_exact ctx stk i sis t rs m s: sem_sistate ctx sis rs m -> sem_sfval ctx stk (sexec_final_sfv i sis) rs m t s -> final_step tr_inputs (cge ctx) stk (cf ctx) (csp ctx) rs m i t s. @@ -677,8 +677,8 @@ Proof. econstructor; simpl; intuition eauto || congruence. Qed. -Definition poly_str {A} (tr: function -> list exit -> option reg -> A) f (svf: sfval): A := - match svf with +Definition poly_str {A} (tr: function -> list exit -> option reg -> A) f (sfv: sfval): A := + match sfv with | Sgoto pc => tr f [pc] None | Scall _ _ _ res pc => tr f [pc] (Some res) | Stailcall _ _ args => tr f [] None @@ -707,8 +707,8 @@ Inductive sstate := (* outcome of a symbolic execution path *) Record soutcome := sout { - so_sis: sistate; - so_svf: sfval; + _sis: sistate; + _sfv: sfval; }. Fixpoint run_sem_isstate ctx (st:sstate): option soutcome := @@ -717,7 +717,7 @@ Fixpoint run_sem_isstate ctx (st:sstate): option soutcome := | Scond cond args sm ifso ifnot => SOME b <- seval_condition ctx cond args sm IN run_sem_isstate ctx (if b then ifso else ifnot) - | _ => None + | Sabort => None end. (* transition (t,s) produced by a sstate in initial context ctx *) @@ -794,7 +794,7 @@ Fixpoint sexec_rec f ib sis (k: sistate -> sstate): sstate := Definition sexec f ib := sexec_rec f ib sis_init (fun _ => Sabort). Local Hint Constructors sem_sstate: core. -Local Hint Resolve sexec_op_correct sexec_final_svf_correct tr_sis_regs_correct_aux tr_sis_regs_correct +Local Hint Resolve sexec_op_correct sexec_final_sfv_correct tr_sis_regs_correct_aux tr_sis_regs_correct sexec_load_TRAP_correct sexec_store_correct sis_init_correct: core. Lemma sexec_rec_correct ctx stk t s ib rs m rs1 m1 ofin @@ -992,7 +992,7 @@ Proof. intros; rewrite REG; autodestruct; try_simplify_someHyps. Qed. -Local Hint Resolve sexec_op_abort sexec_load_TRAP_abort sexec_store_abort sexec_final_svf_exact: core. +Local Hint Resolve sexec_op_abort sexec_load_TRAP_abort sexec_store_abort sexec_final_sfv_exact: core. Lemma sexec_rec_exact ctx stk ib t s1: forall sis k (SEXEC: sem_sstate ctx stk t s1 (sexec_rec (cf ctx) ib sis k)) -- cgit