diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-26 21:42:33 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-27 09:46:24 +0200 |
commit | d76f6a446a8c4866d7e89b1b5b13b24a20e6d1dc (patch) | |
tree | 7b824d1c739f06d0692dc7790067495758c508aa /scheduling | |
parent | 47599a2ea88799d654ec644fe5ba9892087adb39 (diff) | |
download | compcert-kvx-d76f6a446a8c4866d7e89b1b5b13b24a20e6d1dc.tar.gz compcert-kvx-d76f6a446a8c4866d7e89b1b5b13b24a20e6d1dc.zip |
end of BTL_SEtheory w.r.t fsem
Diffstat (limited to 'scheduling')
-rw-r--r-- | scheduling/BTL.v | 9 | ||||
-rw-r--r-- | scheduling/BTL_SEtheory.v | 331 | ||||
-rw-r--r-- | scheduling/BTLroadmap.md | 36 |
3 files changed, 194 insertions, 182 deletions
diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 5f75231a..6f699cd0 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -391,10 +391,11 @@ Definition semantics (p: program) := (** The "functional" small-step semantics for a BTL program. at each exit, we only transfer register in "input_regs" (i.e. "alive" registers). *) - Definition transfer_regs (inputs: list reg) (rs: regset): regset := init_regs (rs##inputs) inputs. +(* TODO: LEMMA BELOW ON transfer_regs USEFUL ? *) + Lemma transfer_regs_inputs inputs rs r: List.In r inputs -> (transfer_regs inputs rs)#r = rs#r. Proof. @@ -456,6 +457,9 @@ Definition inputs_exit (f:function) (tbl: list exit) (or: option reg): Regset.t Definition tr_inputs (f:function) (tbl: list exit) (or:option reg): regset -> regset := transfer_regs (Regset.elements (inputs_exit f tbl or)). +(* TODO: BELOW, LEMMA on tr_inputs USEFUL ? *) + + (* TODO: move this elsewhere *) Lemma SetoidList_InA_eq_equiv A (l: list A): forall x, SetoidList.InA (fun x y => x = y) x l <-> List.In x l. @@ -518,6 +522,7 @@ Definition poly_tr {A} (tr: function -> list exit -> option reg -> A) f (i: fina Definition tr_regs: function -> final -> regset -> regset := poly_tr tr_inputs. +(* TODO: NOT USEFUL ? Definition liveout: function -> final -> Regset.t := poly_tr inputs_exit. @@ -533,7 +538,7 @@ Proof. Local Opaque inputs_exit. destruct fi; simpl; auto. Qed. - +*) (** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *) diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index a066626e..d6b4e741 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -401,57 +401,39 @@ Definition sfind_function ctx (svos : sval + ident): option fundef := Import ListNotations. Local Open Scope list_scope. -(** [sem_sfval] corresponds to [final_step tr_inputs] for symbolic final value. - - A main difference comes from [rsx] which observes the registers saved in the stackframe - of the returned state. - - Intuitively, only liveout registers are stored in the stack - (others will be associated to [Vundef] value). -*) -Inductive sem_sfval ctx (rsx: reg -> option val): sfval -> regset -> mem -> trace -> state -> Prop := - | exec_Sgoto pc rs rs' m: - rs' = tr_inputs ctx.(cf) [pc] None rs -> - (forall r, rsx r = Some rs'#r) -> - sem_sfval ctx rsx (Sgoto pc) rs m E0 (State (cstk ctx) (cf ctx) (csp ctx) pc rs' m) +Inductive sem_sfval ctx: 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' -> match osv with Some sv => eval_sval ctx sv | None => Some Vundef end = Some v -> - (forall r, rsx r = Some Vundef) -> - sem_sfval ctx rsx (Sreturn osv) rs m + sem_sfval ctx (Sreturn osv) rs m E0 (Returnstate (cstk ctx) v m') - | exec_Scall rs m sig svos lsv args res pc fd rs': + | 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 -> - rs' = tr_inputs ctx.(cf) [pc] (Some res) rs -> - (forall r, rsx r = Some rs'#r) -> - sem_sfval ctx rsx (Scall sig svos lsv res pc) rs m - E0 (Callstate ((Stackframe res (cf ctx) (csp ctx) pc rs')::cstk ctx) fd args m) + 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: 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' -> eval_list_sval ctx lsv = Some args -> - (forall r, rsx r = Some Vundef) -> - sem_sfval ctx rsx (Stailcall sig svos lsv) rs m + sem_sfval ctx (Stailcall sig svos lsv) rs m E0 (Callstate (cstk ctx) fd args m') - | exec_Sbuiltin m' rs m vres res pc t sargs ef vargs rs': + | 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' -> - rs' = tr_inputs (cf ctx) [pc] (reg_builtin_res res) rs -> - (forall r, rsx r = Some rs'#r) -> - sem_sfval ctx rsx (Sbuiltin ef sargs res pc) rs m - t (State (cstk ctx) (cf ctx) (csp ctx) pc (regmap_setres res vres rs') m') - | exec_Sjumptable sv tbl pc' n rs m rs': + 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') + | exec_Sjumptable sv tbl pc' n rs m: eval_sval ctx sv = Some (Vint n) -> list_nth_z tbl (Int.unsigned n) = Some pc' -> - rs' = tr_inputs ctx.(cf) tbl None rs -> - (forall r, rsx r = Some rs'#r) -> - sem_sfval ctx rsx (Sjumptable sv tbl) rs m - E0 (State (cstk ctx) (cf ctx) (csp ctx) pc' rs' m) + 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) . (** * Preservation properties *) @@ -564,59 +546,6 @@ Definition sem_sistate ctx (sis: sistate) (rs: regset) (m: mem): Prop := /\ forall (r:reg), eval_sval ctx (sis.(si_sreg) r) = Some (rs#r). (** * Symbolic execution of final step *) -Fixpoint transfer_sreg (inputs: list reg) (sreg: reg -> sval): reg -> sval := - match inputs with - | nil => fun r => Sundef - | r1::l => fun r => if Pos.eq_dec r r1 then sreg r1 else transfer_sreg l sreg r - end. - -Lemma transfer_sreg_inputs inputs sreg r: - List.In r inputs -> transfer_sreg inputs sreg r = sreg r. -Proof. - induction inputs; simpl; try autodestruct; intuition congruence. -Qed. - -Lemma transfer_sreg_dead inputs sreg r: - ~List.In r inputs -> transfer_sreg inputs sreg r = Sundef. -Proof. - induction inputs; simpl; try autodestruct; intuition congruence. -Qed. - -Definition str_inputs (f:function) (tbl: list exit) (or:option reg) := transfer_sreg (Regset.elements (inputs_exit f tbl or)). - -Lemma str_inputs_correct ctx sis rs tbl or r: - (forall r : reg, eval_sval ctx (si_sreg sis r) = Some rs # r) -> - eval_sval ctx (str_inputs (cf ctx) tbl or (si_sreg sis) r) = Some (tr_inputs (cf ctx) tbl or rs) # r. -Admitted. - -Local Hint Resolve str_inputs_correct: core. - -Definition tr_sis f (fi: final) (sis: sistate) := - {| si_pre := fun ctx => (sis.(si_pre) ctx /\ forall r, eval_sval ctx (sis.(si_sreg) r) <> None); - si_sreg := poly_tr str_inputs f fi sis.(si_sreg); - si_smem := sis.(si_smem) |}. - -Definition sreg_eval ctx (sis: sistate) (r: reg): option val := - eval_sval ctx (sis.(si_sreg) r). - -Lemma tr_sis_regs_correct_aux ctx fin sis rs m: - sem_sistate ctx sis rs m -> - (forall r, sreg_eval ctx (tr_sis (cf ctx) fin sis) r = Some (tr_regs (cf ctx) fin rs) # r). -Proof. - unfold sreg_eval; simpl. destruct 1 as (_ & _ & REG). - destruct fin; simpl; eauto. -Admitted. - -Lemma tr_sis_regs_correct ctx fin sis rs m: - sem_sistate ctx sis rs m -> - sem_sistate ctx (tr_sis (cf ctx) fin sis) (tr_regs (cf ctx) fin rs) m. -Proof. - intros H. - generalize (tr_sis_regs_correct_aux _ fin _ _ _ H). - destruct H as (PRE & MEM & REG). - econstructor; simpl; intuition eauto || congruence. -Qed. - Definition sexec_final_sfv (i: final) (sis: sistate): sfval := match i with | Bgoto pc => Sgoto pc @@ -644,9 +573,9 @@ Local Hint Constructors sem_sfval: core. Lemma sexec_final_svf_correct ctx 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 (sreg_eval ctx (tr_sis (cf ctx) i sis)) (sexec_final_sfv i sis) rs m t s. + sem_sfval ctx (sexec_final_sfv i sis) rs m t s. Proof. - unfold sreg_eval. intros (PRE&MEM®). + intros (PRE&MEM®). destruct 1; subst; try_simplify_someHyps; simpl; intros; try autodestruct; eauto. + (* Bcall *) intros; eapply exec_Scall; auto. - destruct ros; simpl in * |- *; auto. @@ -666,7 +595,7 @@ Local Hint Resolve seval_builtin_args_exact: core. Lemma sexec_final_svf_exact ctx i sis t rs m s: sem_sistate ctx sis rs m -> - sem_sfval ctx (sreg_eval ctx (tr_sis (cf ctx) i sis)) (sexec_final_sfv i sis) rs m t s + 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. Proof. intros (PRE&MEM®). @@ -797,6 +726,76 @@ Proof. erewrite MEM; auto. Qed. +(** * Compute sistate associated to final values *) +Fixpoint transfer_sreg (inputs: list reg) (sreg: reg -> sval): reg -> sval := + match inputs with + | nil => fun r => Sundef + | r1::l => fun r => if Pos.eq_dec r r1 then sreg r1 else transfer_sreg l sreg r + end. + +Definition str_inputs (f:function) (tbl: list exit) (or:option reg) := transfer_sreg (Regset.elements (inputs_exit f tbl or)). + +Lemma str_inputs_correct ctx sis rs tbl or r: + (forall r : reg, eval_sval ctx (si_sreg sis r) = Some rs # r) -> + eval_sval ctx (str_inputs (cf ctx) tbl or (si_sreg sis) r) = Some (tr_inputs (cf ctx) tbl or rs) # r. +Proof. + intros H. + unfold str_inputs, tr_inputs, transfer_regs. + induction (Regset.elements _) as [|x l]; simpl. + + rewrite Regmap.gi; auto. + + autodestruct; intros; subst. + * rewrite Regmap.gss; auto. + * rewrite Regmap.gso; eauto. +Qed. + +Local Hint Resolve str_inputs_correct: core. + +Definition tr_sis f (fi: final) (sis: sistate) := + {| si_pre := fun ctx => (sis.(si_pre) ctx /\ forall r, eval_sval ctx (sis.(si_sreg) r) <> None); + si_sreg := poly_tr str_inputs f fi sis.(si_sreg); + si_smem := sis.(si_smem) |}. + +Definition sreg_eval ctx (sis: sistate) (r: reg): option val := + eval_sval ctx (sis.(si_sreg) r). + +Lemma tr_sis_regs_correct_aux ctx fin sis rs m: + sem_sistate ctx sis rs m -> + (forall r, sreg_eval ctx (tr_sis (cf ctx) fin sis) r = Some (tr_regs (cf ctx) fin rs) # r). +Proof. + Local Opaque str_inputs. + unfold sreg_eval; simpl. destruct 1 as (_ & _ & REG). + destruct fin; simpl; eauto. +Qed. + +Lemma tr_sis_regs_correct ctx fin sis rs m: + sem_sistate ctx sis rs m -> + sem_sistate ctx (tr_sis (cf ctx) fin sis) (tr_regs (cf ctx) fin rs) m. +Proof. + intros H. + generalize (tr_sis_regs_correct_aux _ fin _ _ _ H). + destruct H as (PRE & MEM & REG). + econstructor; simpl; intuition eauto || congruence. +Qed. + +Definition poly_str {A} (tr: function -> list exit -> option reg -> A) f (svf: sfval): A := + match svf with + | Sgoto pc => tr f [pc] None + | Scall _ _ _ res pc => tr f [pc] (Some res) + | Stailcall _ _ args => tr f [] None + | Sbuiltin _ _ res pc => tr f [pc] (reg_builtin_res res) + | Sreturn _ => tr f [] None + | Sjumptable _ tbl => tr f tbl None + end. + +Definition str_regs: function -> sfval -> regset -> regset := + poly_str tr_inputs. + +Lemma str_tr_regs_equiv f fin sis: + str_regs f (sexec_final_sfv fin sis) = tr_regs f fin. +Proof. + destruct fin; simpl; auto. +Qed. + (** * symbolic execution of blocks *) (* symbolic state *) @@ -808,10 +807,9 @@ Inductive sstate := (* transition (t,s) produced by a sstate in initial context ctx *) Inductive sem_sstate ctx t s: sstate -> Prop := - | sem_Sfinal sis sfv rs rs' rsx m - (SIS: sem_sistate ctx sis rs' m) - (EXT: forall r, rsx r = Some (rs'#r)) - (SFV: sem_sfval ctx rsx sfv rs m t s) + | 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) | sem_Scond b cond args sm ifso ifnot (SEVAL: seval_condition ctx cond args sm = Some b) @@ -867,6 +865,9 @@ Lemma sexec_rec_correct ctx t s ib rs m rs1 m1 ofin sem_sstate ctx t s (sexec_rec (cf ctx) ib sis k). Proof. induction ISTEP; simpl; try autodestruct; eauto. + (* final value *) + intros; econstructor; eauto. + rewrite str_tr_regs_equiv; eauto. (* condition *) all: intros; eapply sem_Scond; eauto; [ @@ -875,6 +876,7 @@ Proof. try autodestruct; eauto ]. Qed. + (* NB: each concrete execution can be executed on the symbolic state (produced from [sexec]) (sexec is a correct over-approximation) *) @@ -886,6 +888,27 @@ Proof. eapply sexec_rec_correct; simpl; eauto. Qed. +(* Remark that we want to reason modulo "extensionality" wrt Regmap.get about regsets. + And, nothing in their representation as (val * PTree.t val) enforces that + (forall r, rs1#r = rs2#r) -> rs1 = rs2 +*) +Lemma sem_sistate_tr_sis_determ ctx sis rs1 m1 fi rs2 m2: + sem_sistate ctx sis rs1 m1 -> + sem_sistate ctx (tr_sis (cf ctx) fi sis) rs2 m2 -> + (forall r, rs2#r = (tr_regs (cf ctx) fi rs1)#r) + /\ m1 = m2. +Proof. + intros H1 H2. + lapply (tr_sis_regs_correct_aux ctx fi sis rs1 m1); eauto. + unfold sreg_eval; intros X. + destruct H1 as (_&MEM1®1). + destruct H2 as (_&MEM2®2); simpl in *. + intuition try congruence. + cut (Some rs2 # r = Some (tr_regs (cf ctx) fi rs1)#r). + { congruence. } + rewrite <- REG2, X. auto. +Qed. + (* TODO: déplacer les trucs sur equiv_stackframe -> regmap_setres_eq dans BTL! *) Inductive equiv_stackframe: stackframe -> stackframe -> Prop := @@ -958,38 +981,19 @@ Proof. - repeat (rewrite Regmap.gso); auto. Qed. -Local Hint Resolve tr_inputs_ext: core. +(* Local Hint Resolve tr_inputs_ext: core. *) +Local Hint Resolve regmap_setres_eq: core. -Definition poly_str {A} (tr: function -> list exit -> option reg -> A) f svf: A := - match svf with - | Sgoto pc => tr f [pc] None - | Scall _ _ _ res pc => tr f [pc] (Some res) - | Stailcall _ _ args => tr f [] None - | Sbuiltin _ _ res pc => tr f [pc] (reg_builtin_res res) - | Sreturn _ => tr f [] None - | Sjumptable _ tbl => tr f tbl None - end. - - -Lemma sem_sfval_inv1 rsx ctx sfv rs m t s: - sem_sfval ctx rsx sfv rs m t s -> - (forall r, rsx r = Some (poly_str tr_inputs (cf ctx) sfv rs)#r). -Proof. - destruct 1; simpl; subst; auto. -Admitted. - -Lemma sem_sfval_equivx rsx1 rsx2 ctx sfv rs m t s: - sem_sfval ctx rsx1 sfv rs m t s -> - (forall r, rsx1 r = rsx2 r) -> - exists s', equiv_state s s' /\ sem_sfval ctx rsx2 sfv rs m t s'. -Proof. - Local Hint Resolve equiv_stack_refl equiv_state_refl regmap_setres_eq: core. - Local Hint Constructors sem_sfval: core. - destruct 1; eexists; split; econstructor; eauto; try congruence. +Lemma sem_sfval_equiv rs1 rs2 ctx sfv m t s: + sem_sfval ctx 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'. +Proof. + unfold str_regs. + destruct 1; simpl in *; intros; subst; eexists; split; econstructor; eauto; try congruence. + constructor; eauto. Qed. - - Local Hint Resolve sexec_final_svf_exact: core. Definition abort_sistate ctx (sis: sistate): Prop := @@ -1123,39 +1127,6 @@ Qed. Local Hint Resolve sexec_op_abort sexec_load_TRAP_abort sexec_store_abort: core. -(* Remark that we need to reason modulo "extensionality" wrt Regmap.get about regsets. - And, nothing in their representation as (val * PTree.t val) enforces that - (forall r, rs1#r = rs2#r) -> rs1 = rs2 -*) -(* -Lemma sem_sistate_determ ctx sis rs1 m1 rs2 m2: - sem_sistate ctx sis rs1 m1 -> - sem_sistate ctx sis rs2 m2 -> - (forall r, rs1#r = rs2#r) /\ m1 = m2. -Proof. - intros (_&MEM1®1) (_&MEM2®2). - intuition try congruence. - generalize (REG1 r); rewrite REG2; congruence. -Qed. -*) - -Lemma sem_sistate_tr_sis_determ ctx sis rs1 m1 fi rs2 m2: - sem_sistate ctx sis rs1 m1 -> - sem_sistate ctx (tr_sis (cf ctx) fi sis) rs2 m2 -> - (forall r, rs2#r = (tr_regs (cf ctx) fi rs1)#r) - /\ m1 = m2. -Proof. - intros H1 H2. - lapply (tr_sis_regs_correct_aux ctx fi sis rs1 m1); eauto. - unfold sreg_eval; intros X. - destruct H1 as (_&MEM1®1). - destruct H2 as (_&MEM2®2); simpl in *. - intuition try congruence. - cut (Some rs2 # r = Some (tr_regs (cf ctx) fi rs1)#r). - { congruence. } - rewrite <- REG2, X. auto. -Qed. - Lemma sexec_rec_exact ctx ib t s1: forall sis k (SEXEC: sem_sstate ctx t s1 (sexec_rec (cf ctx) ib sis k)) rs m @@ -1172,14 +1143,11 @@ Proof. induction ib; simpl; intros; eauto. - (* final *) inv SEXEC. - exploit (sem_sistate_tr_sis_determ ctx sis rs m fi rs' m0); eauto. + exploit (sem_sistate_tr_sis_determ ctx sis rs m fi); eauto. intros (REG&MEM); subst. - exploit (sem_sfval_equivx rsx (sreg_eval ctx (tr_sis (cf ctx) fi sis)) ctx ); eauto. - + intros; rewrite EXT, REG. admit. - + intros (s2 & EQUIV & SFV'). admit. -(* eexists; split. - eapply sexec_final_svf_exact; eauto. -*) + exploit (sem_sfval_equiv rs0 rs); eauto. + * intros; rewrite REG, str_tr_regs_equiv; auto. + * intros (s2 & EQUIV & SFV'); eauto. - (* Bop *) autodestruct; eauto. - destruct trap; [| inv SEXEC ]. repeat autodestruct; eauto. @@ -1205,7 +1173,7 @@ Proof. destruct b. + exploit IHib1; eauto. + exploit IHib2; eauto. -Admitted. +Qed. (* NB: each execution of a symbolic state (produced from [sexec]) represents a concrete execution @@ -1227,3 +1195,42 @@ Proof. inversion SEXEC. Qed. +(** * High-Level specification of the symbolic simulation test as predicate [sstate_simu] *) + +Record simu_proof_context := 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; + sf1: BTL.function; + sf2: BTL.function; + ssp: val; + srs0: regset; + sm0: mem +}. + +Definition bctx1 (ctx: simu_proof_context):= Bctx ctx.(sge1) ctx.(sstk1) ctx.(sf1) ctx.(ssp) ctx.(srs0) ctx.(sm0). +Definition bctx2 (ctx: simu_proof_context):= Bctx ctx.(sge2) ctx.(sstk2) ctx.(sf2) ctx.(ssp) ctx.(srs0) ctx.(sm0). + +Definition sstate_simu (ctx: simu_proof_context) (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. + +Theorem sstate_simu_correct ctx ib1 ib2: + sstate_simu ctx (sexec (sf1 ctx) ib1) (sexec (sf2 ctx) ib2) -> + forall t s1, iblock_step tr_inputs (sge1 ctx) (sstk1 ctx) (sf1 ctx) (ssp ctx) (srs0 ctx) (sm0 ctx) ib1 t s1 -> + exists s2, iblock_step tr_inputs (sge2 ctx) (sstk2 ctx) (sf2 ctx) (ssp ctx) (srs0 ctx) (sm0 ctx) ib2 t s2 /\ equiv_state s1 s2. +Proof. + unfold sstate_simu. + intros SIMU t s1 STEP1. + exploit (sexec_correct (bctx1 ctx)); simpl; eauto. + intros; exploit SIMU; eauto. + intros (s2 & SEM1 & EQ1). + exploit (sexec_exact (bctx2 ctx)); simpl; eauto. + intros (s3 & STEP2 & EQ2). + clear STEP1; eexists; split; eauto. + eapply equiv_state_trans; eauto. +Qed. + diff --git a/scheduling/BTLroadmap.md b/scheduling/BTLroadmap.md index 6042803d..0cbcd7d6 100644 --- a/scheduling/BTLroadmap.md +++ b/scheduling/BTLroadmap.md @@ -117,37 +117,37 @@ partir du bloc d'entrée de la fonction. Ça semble complémentaire de l'analyse de "liveout". Mais utilisable uniquement dans le cadre d'une combinaison "exécution symbolique"+"value analysis" (donc pas tout de suite). -**IMPLEM PLAN** - -1. définir the "functional semantics" of BTL (dans un premier temps, avec uniquement Vundef en sortie de bloc). Rem: en pratique, la "functional semantics" est définie pour être une "concrétisation" de la sémantique symbolique. Les définitions des deux sémantiques (symbolique et "functional") se font donc en simultanée. -2. prouver la simulation BTL.FunctionalSemantics -> BTL.CFGSemantics (facile normalement: c'est du "less_undef lockstep"). -3. implémenter une passe BTL.CFGSemantics -> BTL.FunctionalSemantics. - en gros: on implémente un vérificateur des infos de liveness. - c'est la correction du "input_regs" qui garantit que la simulation est correct. - La preuve devrait normalement être très similaire à RTLpathLivegenproof. +Donc, dans un premier temps, la "functional semantics" encode/abstrait la notion de "liveout" pour le test d'exécution symbolique. +Les définitions des deux sémantiques (symbolique et "functional") se font donc en simultanée. **STATUS** 1. See [BTL.fsem] (Pour l'instant CFGSemantics => BTL.semantics et FunctionalSemantics => BTL.fsem) +**TODO** + +1. prouver la simulation BTL.FunctionalSemantics -> BTL.CFGSemantics (facile normalement: c'est du "less_undef lockstep"). +2. implémenter une passe BTL.CFGSemantics -> BTL.FunctionalSemantics. + en gros: on implémente un vérificateur des infos de liveness. + c'est la correction du "input_regs" qui garantit que la simulation est correct. + La preuve devrait normalement être très similaire à RTLpathLivegenproof. + ## "Basic" symbolic execution / symbolic simulation We will implement a "basic" (e.g without rewriting rules) simulation test for BTL.FunctionalSemantics. Dans un premier temps: pas besoin de "less_undef lockstep", on peut se contenter de tester l'égalité des registres de chaque côté: les registres hors liveout seront égaux à Vundef de chaque côté. -**IMPLEM NOTE** - -- use Continuation Passing Style for an easy recursive generation of "all execution paths". -- dans l'etat concret, prévoir un booleen qui indique la valeur symbolique par defaut des registres: deux cas, soit "Input" (valeur initiale du registre), soit "Sundef" (valeur Vundef). +**STATUS** -**CURRENT STATUS** +- BTL_SEtheory: DONE + - model of symbolic execution in Continuation-Passing Style for BTL with "correctness" and "completness" thms wrt BTL.fsem + - high-level specification [sstate_simu] of "symbolic simulation" over iblocks (wrt BTL.fsem). -- model of symbolic execution in Continuation-Passing Style for BTL with "correctness" and "completness" thms wrt BTL.semantics +**TODO** -**next steps** -- preservation proof w.r.t BTL.fsem. -- high-level specification of "symbolic simulation" -- ... +1. Verif du "scheduling" (aka analogue de RTLpathScheduler & RTLSchedulerproof). +2. raffinement intermediaire avant le hash-consing ? ça permettrait de décomposer encore davantage la preuve ? +Y a-t-il un moyen simple de faire le tests d'inclusion des fails potentiels à coût linéaire plutôt que quadratique (contrairement à RTLpath) ? ## Port of RTLpath optimizations to BTL |