From 804339839051759c5c77e63232d0aec25bb3846d Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 5 Jul 2021 16:18:47 +0200 Subject: lemma on HC_set_reg --- scheduling/BTL_SEimpl.v | 206 +++++++++++++++++++++++++++++++++------------ scheduling/BTL_SEsimuref.v | 11 +++ 2 files changed, 165 insertions(+), 52 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v index b007a07e..6e86bebb 100644 --- a/scheduling/BTL_SEimpl.v +++ b/scheduling/BTL_SEimpl.v @@ -400,10 +400,10 @@ Definition root_happly (rsv: root_sval) (lr: list reg) (hrs: ristate): ?? sval : end. Lemma root_happly_correct (rsv: root_sval) lr hrs: - WHEN root_happly rsv lr hrs ~> sv THEN forall ctx st - (REF: ris_refines ctx hrs st) + WHEN root_happly rsv lr hrs ~> sv THEN forall ctx sis + (REF: ris_refines ctx hrs sis) (OK: ris_ok ctx hrs), - sval_refines ctx sv (rsv lr st). + sval_refines ctx sv (rsv lr sis). Proof. unfold root_apply, root_happly; destruct rsv; wlp_simplify; inv REF; erewrite H0, H; eauto. @@ -472,16 +472,16 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hrs: ristate): ?? sval := end*) end | Rload _ chunk addr => - DO lhsv <~ hlist_args hrs lr;; - hSload hrs NOTRAP chunk addr lhsv + DO lsv <~ hlist_args hrs lr;; + hSload hrs NOTRAP chunk addr lsv end. Lemma simplify_correct rsv lr hrs: - WHEN simplify rsv lr hrs ~> hv THEN forall ctx st - (REF: ris_refines ctx hrs st) + WHEN simplify rsv lr hrs ~> hv THEN forall ctx sis + (REF: ris_refines ctx hrs sis) (OK0: ris_ok ctx hrs) - (OK1: eval_sval ctx (rsv lr st) <> None), - sval_refines ctx hv (rsv lr st). + (OK1: eval_sval ctx (rsv lr sis) <> None), + sval_refines ctx hv (rsv lr sis). Proof. destruct rsv; simpl; auto. - (* Rop *) @@ -500,22 +500,22 @@ Proof. * rewrite H1 in OK1; congruence. + erewrite H0; eauto. Qed. +Global Opaque simplify. +Local Hint Resolve simplify_correct: wlp. + +Definition red_PTree_set (r: reg) (sv: sval) (hrs: ristate): PTree.t sval := + 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. -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). +Lemma red_PTree_set_correct (r r0:reg) sv (hrs: ristate) ctx: + sval_refines ctx ((ris_sreg_set hrs (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. @@ -526,11 +526,11 @@ Proof. 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 -> +Lemma red_PTree_set_refines (r r0:reg) ctx hrs sis sv1 sv2: + ris_refines ctx hrs sis -> 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). + sval_refines ctx (ris_sreg_set hrs (red_PTree_set r sv1 hrs) r0) (if Pos.eq_dec r r0 then sv2 else si_sreg sis r0). Proof. intros REF SREF OK; rewrite red_PTree_set_correct. unfold ris_sreg_set, ris_sreg_get. @@ -551,11 +551,11 @@ Definition cbranch_expanse (prev: ristate) (cond: condition) (args: list reg): ? (*end.*) Lemma cbranch_expanse_correct hrs c l: - WHEN cbranch_expanse hrs c l ~> r THEN forall ctx st - (REF : ris_refines ctx hrs st) + WHEN cbranch_expanse hrs c l ~> r THEN forall ctx sis + (REF : ris_refines ctx hrs sis) (OK: ris_ok ctx hrs), eval_scondition ctx (fst r) (snd r) = - eval_scondition ctx c (list_sval_inj (map (si_sreg st) l)). + eval_scondition ctx c (list_sval_inj (map (si_sreg sis) l)). Proof. unfold cbranch_expanse. wlp_simplify; inv REF. @@ -586,43 +586,145 @@ Proof. intros; rewrite PTree.gempty; eauto. Qed. -Fixpoint hrexec_rec f ib ris (k: ristate -> rstate): ?? rstate := +Definition hrset_sreg r lr rsv (hrs: ristate): ?? ristate := + DO ok_lsv <~ + (if may_trap rsv lr + then DO hv <~ root_happly rsv lr hrs;; + XDEBUG hv (fun hv => DO hv_name <~ string_of_hashcode (sval_get_hid hv);; RET ("-- insert undef behavior of hashcode:" +; (CamlStr hv_name))%string);; + RET (hv::(ok_rsval hrs)) + else RET (ok_rsval hrs));; + DO simp <~ simplify rsv lr hrs;; + RET {| ris_smem := hrs.(ris_smem); + ris_input_init := hrs.(ris_input_init); + ok_rsval := ok_lsv; + ris_sreg:= red_PTree_set r simp hrs |}. + +Lemma ok_hrset_sreg (rsv:root_sval) ctx (st: sistate) r lr: + si_ok ctx (set_sreg r (rsv lr st) st) + <-> (si_ok ctx st /\ eval_sval ctx (rsv lr st) <> None). +Proof. + unfold set_sreg; simpl; split. + - intros. destruct H as [[OK_SV OK_PRE] OK_SMEM OK_SREG]; simpl in *. + repeat (split; try tauto). + + intros r0; generalize (OK_SREG r0); clear OK_SREG; destruct (Pos.eq_dec r r0); try congruence. + + generalize (OK_SREG r); clear OK_SREG; destruct (Pos.eq_dec r r); try congruence. + - intros (OK & SEVAL). inv OK. + repeat (split; try tauto; eauto). + intros r0; destruct (Pos.eq_dec r r0) eqn:Heq; simpl; + rewrite Heq; eauto. +Qed. + +(* TODO gourdinl move this in BTL_SEtheory? *) +Lemma eval_list_sval_inj_not_none ctx st: forall l, + (forall r, List.In r l -> eval_sval ctx (si_sreg st r) = None -> False) -> + eval_list_sval ctx (list_sval_inj (map (si_sreg st) l)) = None -> False. +Proof. + induction l. + - intuition discriminate. + - intros ALLR. simpl. + inversion_SOME v. + + intro SVAL. inversion_SOME lv; [discriminate|]. + assert (forall r : reg, In r l -> eval_sval ctx (si_sreg st r) = None -> False). + { intros r INR. eapply ALLR. right. assumption. } + intro SVALLIST. intro. eapply IHl; eauto. + + intros. exploit (ALLR a); simpl; eauto. +Qed. + +Lemma hrset_sreg_correct r lr rsv hrs: + WHEN hrset_sreg r lr rsv hrs ~> hrs' THEN forall ctx sis + (REF: ris_refines ctx hrs sis), + ris_refines ctx hrs' (set_sreg r (rsv lr sis) sis). +Proof. + wlp_simplify; inversion REF. + - (* may_trap -> true *) + assert (X: si_ok ctx (set_sreg r (rsv lr sis) sis) <-> + ris_ok ctx {| ris_smem := hrs; + ris_input_init := ris_input_init hrs; + ok_rsval := exta :: ok_rsval hrs; + ris_sreg := red_PTree_set r exta0 hrs |}). + { + rewrite ok_hrset_sreg, OK_EQUIV. + split. + + intros (ROK & SEVAL); inv ROK. + assert (ROK: ris_ok ctx hrs) by (econstructor; eauto). + econstructor; eauto; simpl. + intuition (subst; eauto). + erewrite H0 in *; eauto. + + intros (OK_RMEM & OK_RREG); simpl in *. + assert (ROK: ris_ok ctx hrs) by (econstructor; eauto). + erewrite <- H0 in *; eauto. } + split; auto; rewrite <- X, ok_hrset_sreg. + + intuition eauto. + + intros (SOK & SEVAL) r0. + rewrite ris_sreg_set_access. + erewrite red_PTree_set_refines; intuition eauto. + - (* may_trap -> false *) + assert (X: si_ok ctx (set_sreg r (rsv lr sis) sis) <-> + ris_ok ctx {| ris_smem := hrs; + ris_input_init := ris_input_init hrs; + ok_rsval := ok_rsval hrs; + ris_sreg := red_PTree_set r exta hrs |}). + { + rewrite ok_hrset_sreg, OK_EQUIV. + split. + + intros (ROK & SEVAL); inv ROK. + econstructor; eauto. + + intros (OK_RMEM & OK_RREG). + assert (ROK: ris_ok ctx hrs) by (econstructor; eauto). + split; auto. + intros SNONE; exploit may_trap_correct; eauto. + * intros LNONE; eapply eval_list_sval_inj_not_none; eauto. + assert (SOK: si_ok ctx sis) by intuition. + inv SOK. intuition eauto. + * rewrite <- MEM_EQ; auto. } + split; auto; rewrite <- X, ok_hrset_sreg. + + intuition eauto. + + intros (SOK & SEVAL) r0. + rewrite ris_sreg_set_access. + erewrite red_PTree_set_refines; intuition eauto. +Qed. + +Fixpoint hrexec_rec f ib hrs (k: ristate -> ?? rstate): ?? rstate := match ib with - (*| BF fin _ => Rfinal (tr_ris f fin ris) (sexec_final_sfv fin ris)*) + | BF fin _ => RET (Rfinal (tr_ris f fin hrs) (sexec_final_sfv fin hrs)) (* 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) + | Bnop _ => k hrs + | Bop op args dst _ => + DO next <~ hrset_sreg dst args (Rop op) hrs;; + k next + | Bload TRAP chunk addr args dst _ => + DO next <~ hrset_sreg dst args (Rload TRAP chunk addr) hrs;; + k next + | Bload NOTRAP chunk addr args dst _ => RET Rabort + | Bstore chunk addr args src _ => + DO next <~ hrexec_store chunk addr args src hrs;; + k next (* composed instructions *) | Bseq ib1 ib2 => - rexec_rec f ib1 ris (fun ris2 => rexec_rec f ib2 ris2 k) + hrexec_rec f ib1 hrs (fun hrs2 => hrexec_rec f ib2 hrs2 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) + DO res <~ cbranch_expanse hrs cond args;; + let (cond, vargs) := res in + DO ifso <~ hrexec_rec f ifso hrs k;; + DO ifnot <~ hrexec_rec f ifnot hrs k;; + RET (Rcond cond vargs ifso ifnot) end . -Definition hrexec f ib := hrexec_rec f ib hris_init (fun _ => Rabort). +Definition hrexec f ib := + DO init <~ hris_init;; + hrexec_rec f ib init (fun _ => RET Rabort). -Definition hsexec (f: function) (pc:node): ?? ristate := +Definition hsexec (f: function) (pc:node): ?? rstate := DO path <~ some_or_fail ((fn_code f)!pc) "hsexec.internal_error.1";; - DO hinit <~ init_ristate;; - DO hst <~ hsiexec_path path.(psize) f hinit;; + (*DO hinit <~ init_ristate;;*) + DO hst <~ hrexec f f.(fn_entrypoint);; DO i <~ some_or_fail ((fn_code f)!(hst.(hsi_pc))) "hsexec.internal_error.2";; DO ohst <~ hsiexec_inst i hst;; match ohst with | Some hst' => RET {| hinternal := hst'; hfinal := HSnone |} | None => DO hsvf <~ hsexec_final i hst.(hsi_local);; RET {| hinternal := hst; hfinal := hsvf |} - end.*) + end. End CanonBuilding. diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v index 60c49e04..c812c607 100644 --- a/scheduling/BTL_SEsimuref.v +++ b/scheduling/BTL_SEsimuref.v @@ -44,6 +44,17 @@ Definition ris_sreg_set (ris: ristate) (sreg: PTree.t sval): ristate := ok_rsval := ok_rsval ris; ris_sreg := sreg |}. +Lemma ris_sreg_set_access (ris: ristate) (sreg: PTree.t sval) r smem rsval: + {| ris_smem := smem; + ris_input_init := ris_input_init ris; + ok_rsval := rsval; + ris_sreg := sreg |} r = + ris_sreg_set ris sreg r. +Proof. + unfold ris_sreg_set, ris_sreg_get; simpl. + reflexivity. +Qed. + 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