From d76f6a446a8c4866d7e89b1b5b13b24a20e6d1dc Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 26 May 2021 21:42:33 +0200 Subject: end of BTL_SEtheory w.r.t fsem --- scheduling/BTL_SEtheory.v | 331 +++++++++++++++++++++++----------------------- 1 file changed, 169 insertions(+), 162 deletions(-) (limited to 'scheduling/BTL_SEtheory.v') 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. + -- cgit