From 47599a2ea88799d654ec644fe5ba9892087adb39 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 26 May 2021 16:27:21 +0200 Subject: fix tr_sis definition --- scheduling/BTL_SEtheory.v | 147 ++++++++++++++++++++++++++++------------------ 1 file changed, 90 insertions(+), 57 deletions(-) (limited to 'scheduling/BTL_SEtheory.v') diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index d682f776..a066626e 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -563,20 +563,6 @@ Definition sem_sistate ctx (sis: sistate) (rs: regset) (m: mem): Prop := /\ eval_smem ctx sis.(si_smem) = Some m /\ forall (r:reg), eval_sval ctx (sis.(si_sreg) r) = Some (rs#r). -(* 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. - (** * Symbolic execution of final step *) Fixpoint transfer_sreg (inputs: list reg) (sreg: reg -> sval): reg -> sval := match inputs with @@ -598,29 +584,28 @@ Qed. Definition str_inputs (f:function) (tbl: list exit) (or:option reg) := transfer_sreg (Regset.elements (inputs_exit f tbl or)). -Definition transfer_sis (f:function) (tbl: list exit) (or:option reg) (sis: sistate) := - {| si_pre := sis.(si_pre); si_sreg := str_inputs f tbl or 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 transfer_sis_correct ctx sis rs tbl or r: +Lemma str_inputs_correct ctx sis rs tbl or r: (forall r : reg, eval_sval ctx (si_sreg sis r) = Some rs # r) -> - sreg_eval ctx (transfer_sis (cf ctx) tbl or sis) r = Some (tr_inputs (cf ctx) tbl or 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 transfer_sis_correct: core. +Local Hint Resolve str_inputs_correct: core. -Definition tr_sis: function -> final -> sistate -> sistate := - poly_tr transfer_sis. +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. - destruct 1 as (_ & _ & REG). + unfold sreg_eval; simpl. destruct 1 as (_ & _ & REG). destruct fin; simpl; eauto. -Qed. +Admitted. Lemma tr_sis_regs_correct ctx fin sis rs m: sem_sistate ctx sis rs m -> @@ -629,7 +614,7 @@ Proof. intros H. generalize (tr_sis_regs_correct_aux _ fin _ _ _ H). destruct H as (PRE & MEM & REG). - destruct fin; simpl; econstructor; simpl; intuition eauto. + econstructor; simpl; intuition eauto || congruence. Qed. Definition sexec_final_sfv (i: final) (sis: sistate): sfval := @@ -661,7 +646,7 @@ Lemma sexec_final_svf_correct ctx i sis t rs m s: 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. Proof. - intros (PRE&MEM®). + unfold sreg_eval. 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. @@ -975,18 +960,35 @@ Qed. Local Hint Resolve tr_inputs_ext: core. -(* TODO -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'. +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. - econstructor; eauto. + destruct 1; eexists; split; econstructor; eauto; try congruence. Qed. -*) + + Local Hint Resolve sexec_final_svf_exact: core. @@ -995,17 +997,6 @@ Definition abort_sistate ctx (sis: sistate): Prop := \/ 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). @@ -1045,8 +1036,17 @@ Proof. intros; eapply set_smem_preserves_abort; eauto. Qed. +Lemma sem_sistate_tr_sis_exclude_abort ctx sis fi rs m: + sem_sistate ctx (tr_sis (cf ctx) fi sis) rs m -> + abort_sistate ctx sis -> + False. +Proof. + intros ((PRE1 & PRE2) & MEM & REG); simpl in *. + intros [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; try congruence. +Qed. + Local Hint Resolve sexec_op_preserves_abort sexec_load_preserves_abort - sexec_store_preserves_abort: core. + 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)) @@ -1056,7 +1056,6 @@ Lemma sexec_exclude_abort ctx ib t s1: forall sis k Proof. induction ib; simpl; intros; eauto. - (* final *) inversion SEXEC; subst; eauto. - admit. - (* load *) destruct trap; eauto. inversion SEXEC. - (* seq *) @@ -1065,7 +1064,7 @@ Proof. - (* cond *) inversion SEXEC; subst; eauto. clear SEXEC. destruct b; eauto. -Admitted. +Qed. Lemma set_sreg_abort ctx dst sv sis rs m: sem_sistate ctx sis rs m -> @@ -1124,6 +1123,39 @@ 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 @@ -1140,13 +1172,14 @@ Proof. induction ib; simpl; intros; eauto. - (* final *) inv SEXEC. - admit. - (* TODO - exploit (sem_sistate_determ ctx sis rs m rs0 m0); eauto. + exploit (sem_sistate_tr_sis_determ ctx sis rs m fi rs' m0); eauto. intros (REG&MEM); subst. - exploit (sem_sfval_equiv rs0 rs); eauto. - intros (s2 & EQUIV & SFV'). - eexists; split; eauto. *) + 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. +*) - (* Bop *) autodestruct; eauto. - destruct trap; [| inv SEXEC ]. repeat autodestruct; eauto. -- cgit