diff options
| -rw-r--r-- | scheduling/BTL.v | 66 | ||||
| -rw-r--r-- | scheduling/BTL_SEtheory.v | 147 |
2 files changed, 132 insertions, 81 deletions
diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 954b4cb4..5f75231a 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -453,8 +453,8 @@ Definition inputs_exit (f:function) (tbl: list exit) (or: option reg): Regset.t | None => rs end. -Definition tr_inputs (f:function) (pc: list exit) (or:option reg): regset -> regset - := transfer_regs (Regset.elements (inputs_exit f pc or)). +Definition tr_inputs (f:function) (tbl: list exit) (or:option reg): regset -> regset + := transfer_regs (Regset.elements (inputs_exit f tbl or)). (* TODO: move this elsewhere *) Lemma SetoidList_InA_eq_equiv A (l: list A): forall x, @@ -465,38 +465,39 @@ Proof. - induction l; simpl; intuition. Qed. -Lemma tr_inputs_exit f pc or rs r: - Regset.In r (inputs_exit f pc or) -> (tr_inputs f pc or rs)#r = rs#r. +Lemma tr_inputs_exit f tbl or rs r: + Regset.In r (inputs_exit f tbl or) -> (tr_inputs f tbl or rs)#r = rs#r. Proof. intros; eapply transfer_regs_inputs. rewrite <- SetoidList_InA_eq_equiv. eapply Regset.elements_1; eauto. Qed. -Lemma tr_inputs_dead f pc or rs r: - ~(Regset.In r (inputs_exit f pc or)) -> (tr_inputs f pc or rs)#r = Vundef. +Lemma tr_inputs_dead f tbl or rs r: + ~(Regset.In r (inputs_exit f tbl or)) -> (tr_inputs f tbl or rs)#r = Vundef. Proof. intros X; eapply transfer_regs_dead; intuition eauto. eapply X. eapply Regset.elements_2. rewrite -> SetoidList_InA_eq_equiv; eauto. Qed. -Definition Regset_In_dec r rs: - { Regset.In r rs } + { ~(Regset.In r rs)}. +Local Hint Resolve tr_inputs_exit Regset.mem_2 Regset.mem_1: core. + +Lemma tr_inputs_get f tbl or rs r: + (tr_inputs f tbl or rs)#r = if Regset.mem r (inputs_exit f tbl or) then rs#r else Vundef. Proof. - destruct (Regset.mem r rs) eqn: IsIN. - + left. abstract (eapply Regset.mem_2; auto). - + right. - abstract (intro H; exploit Regset.mem_1; eauto; congruence). -Defined. + autodestruct; eauto. + intros; apply tr_inputs_dead; eauto. + intro X; exploit Regset.mem_1; eauto. + congruence. +Qed. -Lemma tr_inputs_ext f pc or rs1 rs2: - (forall r, Regset.In r (inputs_exit f pc or) -> rs1#r = rs2#r) -> - (forall r, (tr_inputs f pc or rs1)#r = (tr_inputs f pc or rs2)#r). +Lemma tr_inputs_ext f tbl or rs1 rs2: + (forall r, Regset.In r (inputs_exit f tbl or) -> rs1#r = rs2#r) -> + (forall r, (tr_inputs f tbl or rs1)#r = (tr_inputs f tbl or rs2)#r). Proof. - intros EQ r. destruct (Regset_In_dec r (inputs_exit f pc or)). - + rewrite! tr_inputs_exit; eauto. - + rewrite! tr_inputs_dead; eauto. + intros EQ r. rewrite !tr_inputs_get. + autodestruct; auto. Qed. Definition fsem (p: program) := @@ -507,16 +508,33 @@ Local Open Scope list_scope. Definition poly_tr {A} (tr: function -> list exit -> option reg -> A) f (i: final): A := match i with | Bgoto pc => tr f [pc] None - | Bcall sig ros args res pc => tr f [pc] (Some res) - | Btailcall sig ros args => tr f [] None - | Bbuiltin ef args res pc => tr f [pc] (reg_builtin_res res) - | Breturn or => tr f [] None - | Bjumptable reg tbl => tr f tbl None + | Bcall _ _ _ res pc => tr f [pc] (Some res) + | Btailcall _ _ args => tr f [] None + | Bbuiltin _ _ res pc => tr f [pc] (reg_builtin_res res) + | Breturn _ => tr f [] None + | Bjumptable _ tbl => tr f tbl None end. Definition tr_regs: function -> final -> regset -> regset := poly_tr tr_inputs. +Definition liveout: function -> final -> Regset.t := + poly_tr inputs_exit. + +Lemma tr_regs_liveout_equiv f fi : tr_regs f fi = transfer_regs (Regset.elements (liveout f fi)). +Proof. + destruct fi; simpl; auto. +Qed. + +Local Hint Resolve tr_inputs_get: core. + +Lemma tr_regs_get f fi rs r: (tr_regs f fi rs)#r = if Regset.mem r (liveout f fi) then rs#r else Vundef. +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" ? *) (** Matching BTL and RTL code 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. |