From f03d8bc434ea992bd390b949c1e0ce7dd99d2ddc Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 30 Jun 2021 14:57:48 +0200 Subject: some advance --- scheduling/BTL_SEimpl.v | 168 ++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 154 insertions(+), 14 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v index 5c974efd..bf47b6da 100644 --- a/scheduling/BTL_SEimpl.v +++ b/scheduling/BTL_SEimpl.v @@ -1,4 +1,4 @@ -Require Import AST Maps. +Require Import Coqlib AST Maps. Require Import Op Registers. Require Import RTL BTL. Require Import BTL_SEsimuref BTL_SEtheory OptionMonad. @@ -13,6 +13,10 @@ Local Open Scope impure. Import ListNotations. Local Open Scope list_scope. +(** Tactics *) + +Ltac simplify_SOME x := repeat inversion_SOME x; try_simplify_someHyps. + (** Notations to make lemmas more readable *) Notation "'sval_refines' ctx sv1 sv2" := (eval_sval ctx sv1 = eval_sval ctx sv2) (only parsing, at level 0, ctx at next level, sv1 at next level, sv2 at next level): hse. @@ -160,10 +164,10 @@ Definition hSload (sm: smem) (trap: trapping_mode) (chunk: memory_chunk) (addr: hC_sval {| hdata := Sload sm trap chunk addr lsv unknown_hid; hcodes := hv |}. Lemma hSload_correct sm1 trap chunk addr lsv1: - WHEN hSload sm1 trap chunk addr lsv1 ~> hv THEN forall ctx lsv2 sm2 hid + WHEN hSload sm1 trap chunk addr lsv1 ~> hv THEN forall ctx lsv2 sm2 (LR: list_sval_refines ctx lsv1 lsv2) (MR: smem_refines ctx sm1 sm2), - sval_refines ctx hv (Sload sm2 trap chunk addr lsv2 hid). + sval_refines ctx hv (Sload sm2 trap chunk addr lsv2 unknown_hid). Proof. wlp_simplify. rewrite <- LR, <- MR. @@ -254,25 +258,161 @@ Qed. Global Opaque hSstore. Local Hint Resolve hSstore_correct: wlp. -Definition hris_sreg_eval ctx hris r := eval_sval ctx (ris_sreg_get hris r). +Definition hrs_sreg_eval ctx hrs r := eval_sval ctx (ris_sreg_get hrs r). -Definition hris_sreg_get (hris: ristate) r: ?? sval := - match PTree.get r hris with - | None => if ris_input_init hris then hSinput r else hSundef +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 hris_sreg_get: ristate >-> Funclass. +Coercion hrs_sreg_get: ristate >-> Funclass. -Lemma hris_sreg_get_correct hris r: - WHEN hris_sreg_get hris r ~> sv THEN forall ctx (f: reg -> sval) - (RR: forall r, hris_sreg_eval ctx hris r = eval_sval ctx (f r)), +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)), sval_refines ctx sv (f r). Proof. - unfold hris_sreg_eval, ris_sreg_get. wlp_simplify; rewrite <- RR; rewrite H; auto; + unfold hrs_sreg_eval, ris_sreg_get. wlp_simplify; rewrite <- RR; rewrite H; auto; rewrite H0, H1; simpl; auto. Qed. -Global Opaque hris_sreg_get. -Local Hint Resolve hris_sreg_get_correct: wlp. +Global Opaque hrs_sreg_get. +Local Hint Resolve hrs_sreg_get_correct: wlp. + +Fixpoint hlist_args (hrs: ristate) (l: list reg): ?? list_sval := + match l with + | nil => hSnil() + | r::l => + DO v <~ hrs_sreg_get hrs r;; + DO lsv <~ hlist_args hrs l;; + hScons v lsv + end. + +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)), + list_sval_refines ctx lsv (list_sval_inj (List.map f l)). +Proof. + induction l; wlp_simplify. +Qed. +Global Opaque hlist_args. +Local Hint Resolve hlist_args_correct: wlp. + +(** Convert a "fake" hash-consed term into a "real" hash-consed term *) + +Fixpoint fsval_proj sv: ?? sval := + match sv with + | Sundef hc => + DO b <~ phys_eq hc unknown_hid;; + if b then hSundef else RET sv + | Sinput r hc => + DO b <~ phys_eq hc unknown_hid;; + if b then hSinput r (* was not yet really hash-consed *) + else RET sv (* already hash-consed *) + | Sop op hl hc => + DO b <~ phys_eq hc unknown_hid;; + if b then (* was not yet really hash-consed *) + DO hl' <~ fsval_list_proj hl;; + hSop op hl' + else RET sv (* already hash-consed *) + | Sload hm t chk addr hl _ => RET sv (* FIXME TODO gourdinl ? *) + end +with fsval_list_proj sl: ?? list_sval := + match sl with + | Snil hc => + DO b <~ phys_eq hc unknown_hid;; + if b then hSnil() (* was not yet really hash-consed *) + else RET sl (* already hash-consed *) + | Scons hv hl hc => + DO b <~ phys_eq hc unknown_hid;; + if b then (* was not yet really hash-consed *) + DO hv' <~ fsval_proj hv;; + DO hl' <~ fsval_list_proj hl;; + hScons hv' hl' + else RET sl (* already hash-consed *) + end. + +Lemma fsval_proj_correct sv: + WHEN fsval_proj sv ~> sv' THEN forall ctx, + eval_sval ctx sv = eval_sval ctx sv'. +Proof. + induction sv using sval_mut + with (P0 := fun lsv => + WHEN fsval_list_proj lsv ~> lsv' THEN forall ctx, + eval_list_sval ctx lsv = eval_list_sval ctx lsv') + (P1 := fun sm => True); try (wlp_simplify; tauto). + - wlp_xsimplify ltac:(intuition eauto with wlp_raw wlp). + rewrite H, H0; auto. + - wlp_simplify; erewrite H0, H1; eauto. +Qed. +Global Opaque fsval_proj. +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'. +Proof. + induction lsv; wlp_simplify. + erewrite H0, H1; eauto. +Qed. +Global Opaque fsval_list_proj. +Local Hint Resolve fsval_list_proj_correct: wlp. + +(** ** Assignment of memory *) + +Definition hrexec_store chunk addr args src hrs: ?? ristate := + DO hargs <~ hlist_args hrs args;; + DO hsrc <~ hrs_sreg_get hrs src;; + DO hm <~ hSstore hrs.(ris_smem) chunk addr hargs hsrc;; + RET (rset_smem hm hrs). + +Lemma hrexec_store_correct chunk addr args src hrs: + WHEN hrexec_store chunk addr args src hrs ~> hrs' THEN forall ctx sis + (REF: ris_refines ctx hrs sis), + ris_refines ctx hrs' (sexec_store chunk addr args src sis). +Proof. + wlp_simplify. + eapply rset_mem_correct; simpl; eauto. + - intros X; erewrite H1; eauto. + rewrite X. simplify_SOME z. + - intros X; inversion REF. + erewrite H1; eauto. +Qed. + +(** ** Assignment of registers *) + +(** locally new symbolic values during symbolic execution *) +Inductive root_sval: Type := +| Rop (op: operation) +| Rload (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) +. + +Definition root_apply (rsv: root_sval) (lr: list reg) (st: sistate): sval := + let lsv := list_sval_inj (List.map (si_sreg st) lr) in + let sm := si_smem st in + match rsv with + | Rop op => fSop op lsv + | Rload trap chunk addr => fSload sm trap chunk addr lsv + end. +Coercion root_apply: root_sval >-> Funclass. + +Definition root_happly (rsv: root_sval) (lr: list reg) (hrs: ristate): ?? sval := + DO lsv <~ hlist_args hrs lr;; + match rsv with + | Rop op => hSop op lsv + | Rload trap chunk addr => hSload hrs.(ris_smem) trap chunk addr lsv + 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) + (OK: ris_ok ctx hrs), + sval_refines ctx sv (rsv lr st). +Proof. + unfold root_apply, root_happly; destruct rsv; wlp_simplify; inv REF; + erewrite H0, H; eauto. +Qed. +Global Opaque root_happly. +Hint Resolve root_happly_correct: wlp. Definition some_or_fail {A} (o: option A) (msg: pstring): ?? A := match o with -- cgit