From ed7397533af0f850688256f07a2c5a22d6c58615 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 1 Jul 2021 16:25:05 +0200 Subject: red_PTree lemmas --- scheduling/BTL_SEimpl.v | 81 ++++++++++++++++++++++++++++++++++++++++------ scheduling/BTL_SEsimuref.v | 6 ++++ 2 files changed, 77 insertions(+), 10 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v index df8cc47f..b007a07e 100644 --- a/scheduling/BTL_SEimpl.v +++ b/scheduling/BTL_SEimpl.v @@ -258,21 +258,18 @@ Qed. Global Opaque hSstore. Local Hint Resolve hSstore_correct: wlp. -Definition hrs_sreg_eval ctx hrs r := eval_sval ctx (ris_sreg_get hrs r). - Definition hrs_sreg_get (hrs: ristate) r: ?? sval := match PTree.get r hrs with | None => if ris_input_init hrs then hSinput r else hSundef | Some sv => RET sv end. -Coercion hrs_sreg_get: ristate >-> Funclass. Lemma hrs_sreg_get_correct hrs r: WHEN hrs_sreg_get hrs r ~> sv THEN forall ctx (f: reg -> sval) - (RR: forall r, hrs_sreg_eval ctx hrs r = eval_sval ctx (f r)), + (RR: forall r, sval_refines ctx (hrs r) (f r)), sval_refines ctx sv (f r). Proof. - unfold hrs_sreg_eval, ris_sreg_get. wlp_simplify; rewrite <- RR; rewrite H; auto; + unfold ris_sreg_get; wlp_simplify; rewrite <- RR; rewrite H; auto; rewrite H0, H1; simpl; auto. Qed. Global Opaque hrs_sreg_get. @@ -289,7 +286,7 @@ Fixpoint hlist_args (hrs: ristate) (l: list reg): ?? list_sval := Lemma hlist_args_correct hrs l: WHEN hlist_args hrs l ~> lsv THEN forall ctx (f: reg -> sval) - (RR: forall r, hrs_sreg_eval ctx hrs r = eval_sval ctx (f r)), + (RR: forall r, sval_refines ctx (hrs r) (f r)), list_sval_refines ctx lsv (list_sval_inj (List.map f l)). Proof. induction l; wlp_simplify. @@ -333,7 +330,7 @@ with fsval_list_proj sl: ?? list_sval := Lemma fsval_proj_correct sv: WHEN fsval_proj sv ~> sv' THEN forall ctx, - eval_sval ctx sv = eval_sval ctx sv'. + sval_refines ctx sv sv'. Proof. induction sv using sval_mut with (P0 := fun lsv => @@ -349,7 +346,7 @@ Local Hint Resolve fsval_proj_correct: wlp. Lemma fsval_list_proj_correct lsv: WHEN fsval_list_proj lsv ~> lsv' THEN forall ctx, - eval_list_sval ctx lsv = eval_list_sval ctx lsv'. + list_sval_refines ctx lsv lsv'. Proof. induction lsv; wlp_simplify. erewrite H0, H1; eauto. @@ -495,13 +492,53 @@ Proof. wlp_simplify; inv REF. erewrite H0; eauto. - (* Rload *) destruct trap; wlp_simplify; inv REF. - + erewrite H0, H, MEM_EQ; eauto. + + erewrite H0; eauto. + erewrite H; [|eapply REG_EQ; eauto]. + erewrite MEM_EQ; eauto. repeat simplify_SOME z. * destruct (Memory.Mem.loadv _ _ _); try congruence. * rewrite H1 in OK1; congruence. + erewrite H0; eauto. Qed. +Definition red_PTree_set (r: reg) (sv: sval) (hrs: ristate): ristate := + let sreg := + match (ris_input_init hrs), sv with + | true, Sinput r' _ => + if Pos.eq_dec r r' + then PTree.remove r' hrs + else PTree.set r sv hrs + | false, Sundef _ => + PTree.remove r hrs + | _, _ => PTree.set r sv hrs + end in + ris_sreg_set hrs sreg. + +Lemma red_PTree_set_correct (r r0:reg) sv hrs ctx: + sval_refines ctx ((red_PTree_set r sv hrs) r0) ((ris_sreg_set hrs (PTree.set r sv hrs)) r0). +Proof. + unfold red_PTree_set, ris_sreg_set, ris_sreg_get; simpl. + destruct (ris_input_init hrs) eqn:Hinit, sv; simpl; auto. + 1: destruct (Pos.eq_dec r r1); auto; subst; + rename r1 into r. + all: destruct (Pos.eq_dec r r0); auto; + [ subst; rewrite PTree.grs, PTree.gss; simpl; auto | + rewrite PTree.gro, PTree.gso; simpl; auto]. +Qed. + +Lemma red_PTree_set_refines (r r0:reg) ctx hrs st sv1 sv2: + ris_refines ctx hrs st -> + sval_refines ctx sv1 sv2 -> + ris_ok ctx hrs -> + sval_refines ctx ((red_PTree_set r sv1 hrs) r0) (if Pos.eq_dec r r0 then sv2 else si_sreg st r0). +Proof. + intros REF SREF OK; rewrite red_PTree_set_correct. + unfold ris_sreg_set, ris_sreg_get. + destruct (Pos.eq_dec r r0). + - subst; simpl. rewrite PTree.gss; simpl; auto. + - inv REF; simpl. rewrite PTree.gso; simpl; eauto. +Qed. + Definition cbranch_expanse (prev: ristate) (cond: condition) (args: list reg): ?? (condition * list_sval) := (* TODO gourdinl match target_cbranch_expanse prev cond args with @@ -549,7 +586,31 @@ Proof. intros; rewrite PTree.gempty; eauto. Qed. -(* +Fixpoint hrexec_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 _ => RET (k ris) + | Bop op args res _ => + DO next <~ ris_sreg_set hrs 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 + + (* TODO to remove *) + | _ => RET (k ris) + end + . + Definition hrexec f ib := hrexec_rec f ib hris_init (fun _ => Rabort). Definition hsexec (f: function) (pc:node): ?? ristate := diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v index 66abe6e1..60c49e04 100644 --- a/scheduling/BTL_SEsimuref.v +++ b/scheduling/BTL_SEsimuref.v @@ -38,6 +38,12 @@ Definition ris_sreg_get (ris: ristate) r: sval := end. Coercion ris_sreg_get: ristate >-> Funclass. +Definition ris_sreg_set (ris: ristate) (sreg: PTree.t sval): ristate := + {| ris_smem := ris_smem ris; + ris_input_init := ris_input_init ris; + ok_rsval := ok_rsval ris; + ris_sreg := sreg |}. + Record ris_ok ctx (ris: ristate) : Prop := { OK_RMEM: (eval_smem ctx (ris_smem ris)) <> None; OK_RREG: forall sv, List.In sv (ok_rsval ris) -> eval_sval ctx sv <> None -- cgit