From 9e3940d183cb08cb9ed4b257f6dbe7a5aa05e9b6 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Mon, 7 Jun 2021 09:32:29 +0200 Subject: avancement ref de l'exe symbolique --- scheduling/BTL_SEsimuref.v | 321 ++++++++++++++++++++++++++++++++++++++++++--- scheduling/BTL_SEtheory.v | 11 +- 2 files changed, 306 insertions(+), 26 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v index 6d74ccf9..fdefe205 100644 --- a/scheduling/BTL_SEsimuref.v +++ b/scheduling/BTL_SEsimuref.v @@ -9,8 +9,6 @@ - Il faudra ensuite vérifier que l'exécution symbolique préserve ces relations de raffinement ! TODO: A REVOIR COMPLETEMENT. - - essayer de découper chaque relation de raffinement en une fonction "projection/abstraction" (à la "hsval_proj" à renommer en "hsval_abstract") - et une équivalence sur la représentation abstraite. - introduire "fake" hash-consed values (à renommer en "refined" plutôt que "fake"). *) @@ -48,7 +46,7 @@ Record ristate := 1) we store a list of sval evaluations 2) we encode the symbolic regset by a PTree + a boolean indicating the default sval *) ris_input_init: bool; - ris_ok_sval: list sval; + ok_rsval: list sval; ris_sreg:> PTree.t sval }. @@ -61,7 +59,7 @@ Coercion ris_sreg_get: ristate >-> Funclass. Record ris_ok ctx (ris: ristate) : Prop := { OK_RMEM: (eval_smem ctx (ris_smem ris)) <> None; - OK_RREG: forall sv, List.In sv (ris_ok_sval ris) -> eval_sval ctx sv <> None + OK_RREG: forall sv, List.In sv (ok_rsval ris) -> eval_sval ctx sv <> None }. Local Hint Resolve OK_RMEM OK_RREG: core. Local Hint Constructors ris_ok: core. @@ -77,7 +75,7 @@ Local Hint Resolve OK_EQUIV MEM_EQ REG_EQ VALID_PRESERV: core. Local Hint Constructors ris_refines: core. Record ris_simu ris1 ris2: Prop := { - SIMU_FAILS: forall sv, List.In sv ris2.(ris_ok_sval) -> List.In sv ris1.(ris_ok_sval); + SIMU_FAILS: forall sv, List.In sv ris2.(ok_rsval) -> List.In sv ris1.(ok_rsval); SIMU_MEM: ris1.(ris_smem) = ris2.(ris_smem); SIMU_REG: forall r, ris_sreg_get ris1 r = ris_sreg_get ris2 r }. @@ -307,7 +305,7 @@ Proof. destruct i; simpl; unfold sum_left_map; try autodestruct; eauto. Qed. -Definition ris_init: ristate := {| ris_smem:= Sinit; ris_input_init:=true; ris_ok_sval := nil; ris_sreg := PTree.empty _ |}. +Definition ris_init: ristate := {| ris_smem:= Sinit; ris_input_init:=true; ok_rsval := nil; ris_sreg := PTree.empty _ |}. Lemma ris_init_correct ctx: ris_refines ctx ris_init sis_init. @@ -323,11 +321,11 @@ Qed. Definition rset_smem rm (ris:ristate): ristate := {| ris_smem := rm; ris_input_init := ris.(ris_input_init); - ris_ok_sval := ris.(ris_ok_sval); + ok_rsval := ris.(ok_rsval); ris_sreg:= ris.(ris_sreg) |}. -Lemma sis_ok_set_mem ctx sm sis: +Lemma ok_set_mem ctx sm sis: sis_ok ctx (set_smem sm sis) <-> (sis_ok ctx sis /\ eval_smem ctx sm <> None). Proof. @@ -335,7 +333,7 @@ Proof. intuition eauto. Qed. -Lemma ris_ok_set_mem ctx rm (ris: ristate): +Lemma ok_rset_mem ctx rm (ris: ristate): (eval_smem ctx ris.(ris_smem) = None -> eval_smem ctx rm = None) -> ris_ok ctx (rset_smem rm ris) <-> (ris_ok ctx ris /\ eval_smem ctx rm <> None). @@ -343,7 +341,7 @@ Proof. split; destruct 1; econstructor; simpl in *; eauto. Qed. -Lemma rset_mem_refpreserv ctx rm sm ris sis: +Lemma rset_mem_correct ctx rm sm ris sis: (eval_smem ctx ris.(ris_smem) = None -> eval_smem ctx rm = None) -> (forall m b ofs, eval_smem ctx sm = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer (cm0 ctx) b ofs) -> ris_refines ctx ris sis -> @@ -352,23 +350,308 @@ Lemma rset_mem_refpreserv ctx rm sm ris sis: Proof. destruct 3; intros. econstructor; eauto. - + rewrite sis_ok_set_mem, ris_ok_set_mem; intuition congruence. - + rewrite ris_ok_set_mem; intuition eauto. - + rewrite ris_ok_set_mem; intuition eauto. + + rewrite ok_set_mem, ok_rset_mem; intuition congruence. + + rewrite ok_rset_mem; intuition eauto. + + rewrite ok_rset_mem; intuition eauto. Qed. -(** TODO: could be useful ? -Lemma seval_condition_valid_preserv ctx cond args sm b +Definition rexec_store chunk addr args src ris: ristate := + let args := list_sval_inj (List.map (ris_sreg_get ris) args) in + let src := ris_sreg_get ris src in + let rm := Sstore ris.(ris_smem) chunk addr args src in + rset_smem rm ris. + +Lemma rexec_store_correct ctx chunk addr args src ris sis: + ris_refines ctx ris sis -> + ris_refines ctx (rexec_store chunk addr args src ris) (sexec_store chunk addr args src sis). +Proof. + intros REF; eapply rset_mem_correct; simpl; eauto. + + intros X; rewrite X. repeat autodestruct; eauto. + + intros m b ofs; repeat autodestruct. + intros; erewrite <- Mem.storev_preserv_valid; [| eauto]. + eauto. + + intros OK; erewrite eval_list_sval_refpreserv, MEM_EQ, REG_EQ; eauto. +Qed. + +(* TODO: reintroduire le "root_apply" ? *) + +Definition rset_sreg r rsv (ris:ristate): ristate := + {| ris_smem := ris.(ris_smem); + ris_input_init := ris.(ris_input_init); + ok_rsval := rsv::ris.(ok_rsval); (* TODO: A CHANGER ? *) + ris_sreg:= PTree.set r rsv ris.(ris_sreg) (* TODO: A CHANGER *) + |}. + +Lemma ok_set_sreg ctx r sv sis: + sis_ok ctx (set_sreg r sv sis) + <-> (sis_ok ctx sis /\ eval_sval ctx sv <> None). +Proof. + unfold set_sreg; split. + + intros [(SVAL & PRE) SMEM SREG]; simpl in *; split. + - econstructor; eauto. + intros r0; generalize (SREG r0); destruct (Pos.eq_dec r r0); try congruence. + - generalize (SREG r); destruct (Pos.eq_dec r r); try congruence. + + intros ([PRE SMEM SREG] & SVAL). + econstructor; simpl; eauto. + intros r0; destruct (Pos.eq_dec r r0); try congruence. +Qed. + +Lemma ok_rset_sreg ctx r rsv ris: + ris_ok ctx (rset_sreg r rsv ris) + <-> (ris_ok ctx ris /\ eval_sval ctx rsv <> None). +Proof. + split; destruct 1; econstructor; simpl in *; eauto. + intuition subst; eauto. + exploit OK_RREG; eauto. +Qed. + +Lemma rset_reg_correct ctx r rsv sv ris sis: + ris_refines ctx ris sis -> + (ris_ok ctx ris -> eval_sval ctx rsv = eval_sval ctx sv) -> + ris_refines ctx (rset_sreg r rsv ris) (set_sreg r sv sis). +Proof. + destruct 1; intros. + econstructor; eauto. + + rewrite ok_set_sreg, ok_rset_sreg; intuition congruence. + + rewrite ok_rset_sreg; intuition eauto. + + rewrite ok_rset_sreg. intros; unfold rset_sreg, set_sreg, ris_sreg_get; simpl. intuition eauto. + destruct (Pos.eq_dec _ _). + * subst; rewrite PTree.gss; eauto. + * rewrite PTree.gso; eauto. +Qed. + +Definition rexec_op op args dst (ris:ristate): ristate := + let args := list_sval_inj (List.map ris args) in + rset_sreg dst (Sop op args Sinit) ris. + +Lemma rexec_op_correct ctx op args dst ris sis: + ris_refines ctx ris sis -> + ris_refines ctx (rexec_op op args dst ris) (sexec_op op args dst sis). +Proof. + intros REF; eapply rset_reg_correct; simpl; eauto. + intros OK; erewrite eval_list_sval_refpreserv; eauto. + do 2 autodestruct; auto. + + intros. erewrite <- op_valid_pointer_eq; eauto. + + erewrite <- MEM_EQ; eauto. + intros; exploit OK_RMEM; eauto. destruct 1. +Qed. + +Definition rexec_load trap chunk addr args dst (ris:ristate): ristate := + let args := list_sval_inj (List.map ris args) in + rset_sreg dst (Sload ris.(ris_smem) trap chunk addr args) ris. + +Lemma rexec_load_correct ctx trap chunk addr args dst ris sis: + ris_refines ctx ris sis -> + ris_refines ctx (rexec_load trap chunk addr args dst ris) (sexec_load trap chunk addr args dst sis). +Proof. + intros REF; eapply rset_reg_correct; simpl; eauto. + intros OK; erewrite eval_list_sval_refpreserv, MEM_EQ; eauto. +Qed. + +Lemma seval_condition_valid_preserv ctx cond args sm + (OK: eval_smem ctx sm <> None) (VALID_PRESERV: forall m b ofs, eval_smem ctx sm = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer (cm0 ctx) b ofs) - :seval_condition ctx cond args sm = Some b -> - seval_condition ctx cond args Sinit = Some b. + :seval_condition ctx cond args sm = seval_condition ctx cond args Sinit. Proof. unfold seval_condition; autodestruct; simpl; try congruence. intros EVAL_LIST. autodestruct; try congruence. - intros MEM COND. rewrite <- COND. + intros. eapply cond_valid_pointer_eq; intros. exploit VALID_PRESERV; eauto. Qed. -*) + +Lemma seval_condition_refpreserv ctx cond args ris sis: + ris_refines ctx ris sis -> + ris_ok ctx ris -> + seval_condition ctx cond (list_sval_inj (map ris args)) Sinit = + seval_condition ctx cond (list_sval_inj (map sis args)) Sinit. +Proof. + intros; unfold seval_condition. + erewrite eval_list_sval_refpreserv; eauto. +Qed. + + +(* transfer *) + +Definition rseto_sreg r rsv (ris:ristate): ristate := + {| ris_smem := ris.(ris_smem); + ris_input_init := ris.(ris_input_init); + ok_rsval := ris.(ok_rsval); + ris_sreg:= PTree.set r rsv ris.(ris_sreg) (* TODO: A CHANGER *) + |}. + +Lemma ok_rseto_sreg ctx r rsv ris: + ris_ok ctx (rseto_sreg r rsv ris) + <-> (ris_ok ctx ris). +Proof. + split; destruct 1; econstructor; simpl in *; eauto. +Qed. + +Lemma rseto_reg_correct ctx r rsv sv ris sis: + ris_refines ctx ris sis -> + (ris_ok ctx ris -> eval_sval ctx rsv <> None) -> + (ris_ok ctx ris -> eval_sval ctx rsv = eval_sval ctx sv) -> + ris_refines ctx (rseto_sreg r rsv ris) (set_sreg r sv sis). +Proof. + destruct 1; intros. + econstructor; eauto. + + rewrite ok_set_sreg, ok_rseto_sreg; intuition congruence. + + rewrite ok_rseto_sreg; intuition eauto. + + rewrite ok_rseto_sreg. intros; unfold rseto_sreg, set_sreg, ris_sreg_get; simpl. intuition eauto. + destruct (Pos.eq_dec _ _). + * subst; rewrite PTree.gss; eauto. + * rewrite PTree.gso; eauto. +Qed. + +Fixpoint transfer_ris (inputs: list reg) (ris:ristate): ristate := + match inputs with + | nil => {| ris_smem := ris.(ris_smem); + ris_input_init := false; + ok_rsval := ris.(ok_rsval); + ris_sreg:= PTree.empty _ + |} + | r::l => rseto_sreg r (ris_sreg_get ris r) (transfer_ris l ris) + end. + +Definition transfer_sis (inputs: list reg) (sis:sistate): sistate := + {| si_pre := fun ctx => (sis.(si_pre) ctx /\ forall r, eval_sval ctx (sis.(si_sreg) r) <> None); + si_sreg := transfer_sreg inputs sis; + si_smem := sis.(si_smem) |}. + +Lemma ok_transfer_sis ctx inputs sis: + sis_ok ctx (transfer_sis inputs sis) + <-> (sis_ok ctx sis). +Proof. + unfold transfer_sis. induction inputs as [|r l]; simpl. + + split; destruct 1; econstructor; simpl in *; intuition eauto. congruence. + + split. + * destruct 1; econstructor; simpl in *; intuition eauto. + * intros X; generalize X. rewrite <- IHl in X; clear IHl. + intros [PRE SMEM SREG]. + econstructor; simpl; eauto. + intros r0; destruct (Pos.eq_dec r r0); try congruence. + intros H; eapply OK_SREG; eauto. +Qed. + +Lemma ok_transfer_ris ctx inputs ris: + ris_ok ctx (transfer_ris inputs ris) + <-> (ris_ok ctx ris). +Proof. + induction inputs as [|r l]; simpl. + + split; destruct 1; econstructor; simpl in *; intuition eauto. + + rewrite ok_rseto_sreg. auto. +Qed. + +Lemma transfer_ris_correct ctx inputs ris sis: + ris_refines ctx ris sis -> + ris_refines ctx (transfer_ris inputs ris) (transfer_sis inputs sis). +Proof. + destruct 1; intros. + induction inputs as [|r l]. + + econstructor; eauto. + * erewrite ok_transfer_sis, ok_transfer_ris; eauto. + * erewrite ok_transfer_ris; eauto. + * erewrite ok_transfer_ris; simpl; unfold ris_sreg_get; simpl; eauto. + intros; rewrite PTree.gempty. simpl; auto. + + econstructor; eauto. + * erewrite ok_transfer_sis, ok_transfer_ris; eauto. + * erewrite ok_transfer_ris; simpl. + intros; erewrite MEM_EQ. 2: eauto. + - unfold transfer_sis; simpl; eauto. + - rewrite ok_transfer_ris; simpl; eauto. + * erewrite ok_transfer_ris; simpl. + intros H r0. + erewrite REG_EQ. 2: eapply rseto_reg_correct; eauto. + - unfold set_sreg; simpl; auto. + destruct (Pos.eq_dec _ _); simpl; auto. + - intros. rewrite REG_EQ0; auto. apply OK_SREG; tauto. + - rewrite ok_rseto_sreg, ok_transfer_ris. auto. +Qed. + +Definition alt_tr_sis := poly_tr (fun f tbl or => transfer_sis (Regset.elements (pre_inputs f tbl or))). + +Lemma tr_sis_alt_def f fi sis: + alt_tr_sis f fi sis = tr_sis f fi sis. +Proof. + unfold tr_sis, str_inputs. destruct fi; simpl; auto. +Qed. + +Definition tr_ris := poly_tr (fun f tbl or => transfer_ris (Regset.elements (pre_inputs f tbl or))). + +Local Hint Resolve transfer_ris_correct ok_transfer_ris: core. +Local Opaque transfer_ris. + +Lemma ok_tr_ris ctx f fi ris: + ris_ok ctx (tr_ris f fi ris) + <-> (ris_ok ctx ris). +Proof. + destruct fi; simpl; eauto. +Qed. + +Lemma ok_tr_ris_imp ctx f fi ris: + ris_ok ctx (tr_ris f fi ris) + -> (ris_ok ctx ris). +Proof. + rewrite ok_tr_ris; auto. +Qed. + + +Lemma tr_ris_correct ctx f fi ris sis: + ris_refines ctx ris sis -> + ris_refines ctx (tr_ris f fi ris) (tr_sis f fi sis). +Proof. + intros REF. rewrite <- tr_sis_alt_def. + destruct fi; simpl; eauto. +Qed. + +Fixpoint rexec_rec f ib ris (k: ristate -> rstate): rstate := + match ib with + | BF fin _ => Rfinal (tr_ris f fin ris) (sexec_final_sfv fin ris) + (* basic instructions *) + | Bnop _ => k ris + | Bop op args res _ => k (rexec_op op args res ris) + | Bload TRAP chunk addr args dst _ => k (rexec_load TRAP chunk addr args dst ris) + | Bload NOTRAP chunk addr args dst _ => Rabort + | Bstore chunk addr args src _ => k (rexec_store chunk addr args src ris) + (* composed instructions *) + | Bseq ib1 ib2 => + rexec_rec f ib1 ris (fun ris2 => rexec_rec f ib2 ris2 k) + | Bcond cond args ifso ifnot _ => + let args := list_sval_inj (List.map ris args) in + let ifso := rexec_rec f ifso ris k in + let ifnot := rexec_rec f ifnot ris k in + Rcond cond args ifso ifnot + end + . + +Local Hint Constructors rst_refines: core. +Local Hint Resolve ris_init_correct exec_final_refpreserv tr_ris_correct ok_tr_ris_imp + rexec_op_correct rexec_load_correct rexec_store_correct: core. + +Lemma rexec_rec_correct ctx f ib: + forall ris sis rk k + (CONT: forall rs ss, ris_refines ctx rs ss -> rst_refines ctx (rk rs) (k ss)) + (REF: ris_refines ctx ris sis) + (*OK: ris_ok ctx ris*) + , rst_refines ctx (rexec_rec f ib ris rk) (sexec_rec f ib sis k). +Proof. + induction ib; simpl; eauto. + - (* load *) autodestruct; eauto. + - intros. + econstructor; eauto. + symmetry. + erewrite seval_condition_valid_preserv; eauto. +Admitted. + +Definition rexec f ib := rexec_rec f ib ris_init (fun _ => Rabort). + +Lemma rexec_correct ctx f ib: + rst_refines ctx (rexec f ib) (sexec f ib). +Proof. + eapply rexec_rec_correct; eauto. + (* econstructor; simpl; auto. congruence. *) +Qed. + + diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index 4b4571e4..464bb0f0 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -630,7 +630,7 @@ Qed. 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 + | r1::l => fun r => if Pos.eq_dec r1 r 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 (pre_inputs f tbl or)). @@ -655,15 +655,12 @@ Definition tr_sis f (fi: final) (sis: sistate) := 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). + (forall r, eval_sval 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). + simpl. destruct 1 as (_ & _ & REG). destruct fin; simpl; eauto. Qed. @@ -842,7 +839,7 @@ Lemma sem_sistate_tr_sis_determ ctx sis rs1 m1 fi rs2 m2: Proof. intros H1 H2. lapply (tr_sis_regs_correct_aux ctx fi sis rs1 m1); eauto. - unfold sreg_eval; intros X. + intros X. destruct H1 as (_&MEM1®1). destruct H2 as (_&MEM2®2); simpl in *. intuition try congruence. -- cgit