From 95b6814a1cff386150a7573cb30e9cb68a18052c Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Mon, 10 May 2021 20:07:29 +0200 Subject: prove sexec_exact --- scheduling/BTL_SEtheory.v | 334 ++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 323 insertions(+), 11 deletions(-) (limited to 'scheduling/BTL_SEtheory.v') diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index 0a2c0a04..5f7ecb1b 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -13,6 +13,22 @@ Require Import RTL BTL OptionMonad. Ltac inversion_SOME := fail. (* deprecated tactic of OptionMonad: use autodestruct instead *) Ltac inversion_ASSERT := fail. (* deprecated tactic of OptionMonad: use autodestruct instead *) + +Ltac depmatch exp := + match exp with + | context f [match ?expr with | _ => _ end] => ltac: (depmatch expr) + | _ => exp + end. + +Ltac autodestruct := + let EQ := fresh "EQ" in + match goal with + | |- context f [match ?expr with | _ => _ end] => + let t := ltac: (depmatch expr) in + destruct t eqn:EQ; generalize EQ; clear EQ; congruence || trivial + end. + + Record iblock_exec_context := Bctx { cge: BTL.genv; cstk: list stackframe; @@ -206,7 +222,7 @@ Proof. eapply seval_builtin_arg_correct; eauto. Qed. -Lemma seval_builtin_arg_complete ctx rs m sreg: forall arg varg, +Lemma seval_builtin_arg_exact ctx rs m sreg: forall arg varg, (forall r, eval_sval ctx (sreg r) = Some rs # r) -> seval_builtin_arg ctx m (builtin_arg_map sreg arg) varg -> eval_builtin_arg (cge ctx) (fun r => rs # r) (csp ctx) m arg varg. @@ -220,7 +236,7 @@ Proof. eapply IHarg1; eauto. eapply IHarg2; eauto. Qed. -Lemma seval_builtin_args_complete ctx rs m sreg: forall args vargs, +Lemma seval_builtin_args_exact ctx rs m sreg: forall args vargs, (forall r, eval_sval ctx (sreg r) = Some rs # r) -> seval_builtin_args ctx m (map (builtin_arg_map sreg) args) vargs -> eval_builtin_args (cge ctx) (fun r => rs # r) (csp ctx) m args vargs. @@ -229,7 +245,7 @@ Proof. - simpl. intros. inv H0. constructor. - intros vargs SEVAL BARG. simpl in BARG. inv BARG. constructor; [| eapply IHargs; eauto]. - eapply seval_builtin_arg_complete; eauto. + eapply seval_builtin_arg_exact; eauto. Qed. Fixpoint seval_builtin_sval ctx bsv := @@ -539,10 +555,19 @@ Definition sem_sistate ctx (st: sistate) (rs: regset) (m: mem): Prop := /\ eval_smem ctx st.(si_smem) = Some m /\ forall (r:reg), eval_sval ctx (st.(si_sreg) r) = Some (rs#r). -Definition abort_sistate ctx (st: sistate): Prop := - ~(st.(si_pre) ctx) - \/ eval_smem ctx st.(si_smem) = None - \/ exists (r: reg), eval_sval ctx (st.(si_sreg) r) = None. +(* 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 st rs1 m1 rs2 m2: + sem_sistate ctx st rs1 m1 -> + sem_sistate ctx st 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. (** * Symbolic execution of final step *) Definition sexec_final_sfv (i: final) (sis: sistate): sfval := @@ -590,9 +615,9 @@ Proof. Qed. Local Hint Constructors final_step: core. -Local Hint Resolve seval_builtin_args_complete: core. +Local Hint Resolve seval_builtin_args_exact: core. -Lemma sexec_final_svf_complete ctx i sis t rs m s: +Lemma sexec_final_svf_exact ctx 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 (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s. @@ -640,7 +665,7 @@ Lemma set_sreg_correct ctx dst sv sis (rs rs': regset) m: sem_sistate ctx (set_sreg dst sv sis) rs' m. Proof. intros (PRE&MEM®) NEW OLD. - unfold sem_sistate, set_sreg; simpl. + unfold sem_sistate; simpl. intuition. - rewrite REG in *; congruence. - destruct (Pos.eq_dec dst r); simpl; subst; eauto. @@ -658,7 +683,7 @@ Lemma set_smem_correct ctx sm sis rs m m': sem_sistate ctx (set_smem sm sis) rs m'. Proof. intros (PRE&MEM®) NEW. - unfold sem_sistate, set_smem; simpl. + unfold sem_sistate; simpl. intuition. rewrite MEM in *; congruence. Qed. @@ -813,3 +838,290 @@ Proof. destruct 1 as (rs' & m' & fin & ISTEP & FSTEP). eapply sexec_rec_correct; simpl; eauto. Qed. + + +(* TODO: déplacer les trucs sur equiv_stackframe -> regmap_setres_eq dans BTL! *) +Inductive equiv_stackframe: stackframe -> stackframe -> Prop := + | equiv_stackframe_intro res f sp pc rs1 rs2 + (EQUIV: forall r : positive, rs1 !! r = rs2 !! r): + equiv_stackframe (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2) + . + +Inductive equiv_state: state -> state -> Prop := + | State_equiv stack f sp pc rs1 m rs2 + (EQUIV: forall r, rs1#r = rs2#r): + equiv_state (State stack f sp pc rs1 m) (State stack f sp pc rs2 m) + | Call_equiv stk stk' f args m + (STACKS: list_forall2 equiv_stackframe stk stk'): + equiv_state (Callstate stk f args m) (Callstate stk' f args m) + | Return_equiv stk stk' v m + (STACKS: list_forall2 equiv_stackframe stk stk'): + equiv_state (Returnstate stk v m) (Returnstate stk' v m) + . + +Local Hint Constructors equiv_stackframe equiv_state: core. + +Lemma equiv_stackframe_refl stf: equiv_stackframe stf stf. +Proof. + destruct stf; eauto. +Qed. + +Lemma equiv_stack_refl stk: list_forall2 equiv_stackframe stk stk. +Proof. + Local Hint Resolve equiv_stackframe_refl: core. + induction stk; simpl; constructor; auto. +Qed. + +Lemma equiv_state_refl s: equiv_state s s. +Proof. + Local Hint Resolve equiv_stack_refl: core. + induction s; simpl; constructor; auto. +Qed. + +Lemma equiv_stackframe_trans stf1 stf2 stf3: + equiv_stackframe stf1 stf2 -> equiv_stackframe stf2 stf3 -> equiv_stackframe stf1 stf3. +Proof. + destruct 1; intros EQ; inv EQ; try econstructor; eauto. + intros; eapply eq_trans; eauto. +Qed. + +Lemma equiv_stack_trans stk1 stk2: + list_forall2 equiv_stackframe stk1 stk2 -> + forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> + list_forall2 equiv_stackframe stk1 stk3. +Proof. + Local Hint Resolve equiv_stackframe_trans: core. + induction 1; intros stk3 EQ; inv EQ; econstructor; eauto. +Qed. + +Lemma equiv_state_trans s1 s2 s3: equiv_state s1 s2 -> equiv_state s2 s3 -> equiv_state s1 s3. +Proof. + Local Hint Resolve equiv_stack_trans: core. + destruct 1; intros EQ; inv EQ; econstructor; eauto. + intros; eapply eq_trans; eauto. +Qed. + +Lemma regmap_setres_eq (rs rs': regset) res vres: + (forall r, rs # r = rs' # r) -> + forall r, (regmap_setres res vres rs) # r = (regmap_setres res vres rs') # r. +Proof. + intros RSEQ r. destruct res; simpl; try congruence. + destruct (peq x r). + - subst. repeat (rewrite Regmap.gss). reflexivity. + - repeat (rewrite Regmap.gso); auto. +Qed. + +Lemma sem_sfval_equiv rs1 rs2 ctx sfv m t s: + sem_sfval ctx sfv rs1 m t s -> + (forall r, rs1#r = rs2#r) -> + exists s', equiv_state s s' /\ sem_sfval ctx sfv rs2 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. + econstructor; eauto. +Qed. + +Local Hint Resolve sexec_final_svf_exact: core. + +Definition abort_sistate ctx (sis: sistate): Prop := + ~(sis.(si_pre) ctx) + \/ eval_smem ctx sis.(si_smem) = None + \/ exists (r: reg), eval_sval ctx (sis.(si_sreg) r) = None. + +Lemma sem_sistate_exclude_abort ctx sis rs m: + sem_sistate ctx sis rs m -> + abort_sistate ctx sis -> + False. +Proof. + intros SIS ABORT. inv SIS. destruct H0 as (H0 & H0'). + inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; congruence. +Qed. + +Local Hint Resolve sem_sistate_exclude_abort: core. + +Lemma set_sreg_preserves_abort ctx sv dst sis: + abort_sistate ctx sis -> + abort_sistate ctx (set_sreg dst sv sis). +Proof. + unfold abort_sistate; simpl; intros [PRE|[MEM|REG]]; try tauto. + destruct REG as [r REG]. + destruct (Pos.eq_dec dst r) as [TEST|TEST] eqn: HTEST. + - subst; rewrite REG; tauto. + - right. right. eexists; rewrite HTEST. auto. +Qed. + +Lemma sexec_op_preserves_abort ctx op args dest sis: + abort_sistate ctx sis + -> abort_sistate ctx (sexec_op op args dest sis). +Proof. + intros; eapply set_sreg_preserves_abort; eauto. +Qed. + +Lemma sexec_load_preserves_abort ctx chunk addr args dest sis: + abort_sistate ctx sis + -> abort_sistate ctx (sexec_load TRAP chunk addr args dest sis). +Proof. + intros; eapply set_sreg_preserves_abort; eauto. +Qed. + +Lemma set_smem_preserves_abort ctx sm sis: + abort_sistate ctx sis -> + abort_sistate ctx (set_smem sm sis). +Proof. + unfold abort_sistate; simpl; try tauto. +Qed. + +Lemma sexec_store_preserves_abort ctx chunk addr args src sis: + abort_sistate ctx sis + -> abort_sistate ctx (sexec_store chunk addr args src sis). +Proof. + intros; eapply set_smem_preserves_abort; eauto. +Qed. + +Local Hint Resolve sexec_op_preserves_abort sexec_load_preserves_abort + sexec_store_preserves_abort: core. + +Lemma sexec_exclude_abort ctx ib t s1: forall sis k + (SEXEC: sem_sstate ctx t s1 (sexec_rec ib sis k)) + (CONT: forall sis', sem_sstate ctx t s1 (k sis') -> (abort_sistate ctx sis') -> False) + (ABORT: abort_sistate ctx sis), + False. +Proof. + induction ib; simpl; intros; eauto. + - (* final *) inversion SEXEC; subst; eauto. + - (* load *) destruct trap; eauto. + inversion SEXEC. + - (* seq *) + eapply IHib1; eauto. + simpl. eauto. + - (* cond *) + inversion SEXEC; subst; eauto. clear SEXEC. + destruct b; eauto. +Qed. + +Lemma set_sreg_abort ctx dst sv sis rs m: + sem_sistate ctx sis rs m -> + (eval_sval ctx sv = None) -> + abort_sistate ctx (set_sreg dst sv sis). +Proof. + intros (PRE&MEM®) NEW. + unfold sem_sistate, abort_sistate; simpl. + right; right. + exists dst; destruct (Pos.eq_dec dst dst); simpl; try congruence. +Qed. + +Lemma sexec_op_abort ctx sis op args dest rs m + (EVAL: eval_operation (cge ctx) (csp ctx) op rs ## args m = None) + (SIS: sem_sistate ctx sis rs m) + : abort_sistate ctx (sexec_op op args dest sis). +Proof. + eapply set_sreg_abort; eauto. + simpl. destruct SIS as (PRE&MEM®). + erewrite eval_list_sval_inj; simpl; auto. + try_simplify_someHyps. +Qed. + +Lemma sexec_load_TRAP_abort ctx chunk addr args dst sis rs m + (EVAL: forall a, eval_addressing (cge ctx) (csp ctx) addr rs ## args = Some a -> Mem.loadv chunk m a = None) + (SIS: sem_sistate ctx sis rs m) + : abort_sistate ctx (sexec_load TRAP chunk addr args dst sis). +Proof. + eapply set_sreg_abort; eauto. + simpl. destruct SIS as (PRE&MEM®). + erewrite eval_list_sval_inj; simpl; auto. + intros; autodestruct; try_simplify_someHyps. +Qed. + +Lemma set_smem_abort ctx sm sis rs m: + sem_sistate ctx sis rs m -> + eval_smem ctx sm = None -> + abort_sistate ctx (set_smem sm sis). +Proof. + intros (PRE&MEM®) NEW. + unfold abort_sistate; simpl. + tauto. +Qed. + +Lemma sexec_store_abort ctx chunk addr args src sis rs m + (EVAL: forall a, eval_addressing (cge ctx) (csp ctx) addr rs ## args = Some a -> Mem.storev chunk m a (rs # src) = None) + (SIS: sem_sistate ctx sis rs m) + :abort_sistate ctx (sexec_store chunk addr args src sis). +Proof. + eapply set_smem_abort; eauto. + simpl. destruct SIS as (PRE&MEM®). + erewrite eval_list_sval_inj; simpl; auto. + try_simplify_someHyps. + intros; rewrite REG; autodestruct; try_simplify_someHyps. +Qed. + +Local Hint Resolve sexec_op_abort sexec_load_TRAP_abort sexec_store_abort: core. + +Lemma sexec_rec_exact ctx ib t s1: forall sis k + (SEXEC: sem_sstate ctx t s1 (sexec_rec 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) + , + match iblock_istep_run (cge ctx) (csp ctx) ib rs m with + | Some (out rs' m' (Some fin)) => + exists s2, final_step (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') + | None => False + end. +Proof. + induction ib; simpl; intros; eauto. + - (* final *) + inv SEXEC. + exploit (sem_sistate_determ ctx sis rs m rs0 m0); eauto. + intros (REG&MEM); subst. + exploit (sem_sfval_equiv rs0 rs); eauto. + intros (s2 & EQUIV & SFV'). + eexists; split; eauto. + - (* Bop *) autodestruct; eauto. + - destruct trap; [| inv SEXEC ]. + repeat autodestruct; eauto. + all: intros; eapply CONT; eauto; + eapply sexec_load_TRAP_abort; eauto; + intros; try_simplify_someHyps. + - repeat autodestruct; eauto. + all: intros; eapply CONT; eauto; + eapply sexec_store_abort; eauto; + intros; try_simplify_someHyps. + - (* Bseq *) + exploit IHib1; eauto. clear sis SEXEC SIS. + { simpl; intros; eapply sexec_exclude_abort; eauto. } + destruct (iblock_istep_run _ _ _ _ _) eqn: ISTEP; auto. + destruct o. + destruct _fin eqn: OFIN; simpl; eauto. + intros (sis1 & SEXEC1 & SIS1). + exploit IHib2; eauto. + - (* Bcond *) + inv SEXEC. + erewrite seval_condition_eq in SEVAL; eauto. + rewrite SEVAL. + destruct b. + + exploit IHib1; eauto. + + exploit IHib2; eauto. +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 ib) -> + exists s2, iblock_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s2 + /\ equiv_state s1 s2. +Proof. + intros; exploit sexec_rec_exact; eauto. + { intros sis' SEXEC; inversion SEXEC. } + repeat autodestruct; simpl; try tauto. + - intros D1 D2 ISTEP (s2 & FSTEP & EQSTEP); subst. + eexists; split; eauto. + repeat eexists; eauto. + erewrite iblock_istep_run_equiv; eauto. + - intros D1 D2 ISTEP (sis & SEXEC & _); subst. + inversion SEXEC. +Qed. + -- cgit