diff options
| -rw-r--r-- | scheduling/RTLpathSE_impl.v | 60 | ||||
| -rw-r--r-- | scheduling/RTLpathSE_simu_specs.v | 5 |
2 files changed, 23 insertions, 42 deletions
diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v index 87a064d5..38930a75 100644 --- a/scheduling/RTLpathSE_impl.v +++ b/scheduling/RTLpathSE_impl.v @@ -31,7 +31,7 @@ Definition DEBUG (s: pstring): ?? unit := XDEBUG tt (fun _ => RET s). Definition hsval_get_hid (hsv: hsval): hashcode := match hsv with | HSinput _ hid => hid - | HSop _ _ _ hid => hid + | HSop _ _ hid => hid | HSload _ _ _ _ _ hid => hid end. @@ -50,7 +50,7 @@ Definition hsmem_get_hid (hsm: hsmem): hashcode := Definition hsval_set_hid (hsv: hsval) (hid: hashcode): hsval := match hsv with | HSinput r _ => HSinput r hid - | HSop o lhsv hsm _ => HSop o lhsv hsm hid + | HSop o lhsv _ => HSop o lhsv hid | HSload hsm trap chunk addr lhsv _ => HSload hsm trap chunk addr lhsv hid end. @@ -104,10 +104,9 @@ Local Hint Resolve hsmem_set_hid_correct: core. Definition hsval_hash_eq (sv1 sv2: hsval): ?? bool := match sv1, sv2 with | HSinput r1 _, HSinput r2 _ => struct_eq r1 r2 (* NB: really need a struct_eq here ? *) - | HSop op1 lsv1 sm1 _, HSop op2 lsv2 sm2 _ => + | HSop op1 lsv1 _, HSop op2 lsv2 _ => DO b1 <~ phys_eq lsv1 lsv2;; - DO b2 <~ phys_eq sm1 sm2;; - if b1 && b2 + if b1 then struct_eq op1 op2 (* NB: really need a struct_eq here ? *) else RET false | HSload sm1 trap1 chk1 addr1 lsv1 _, HSload sm2 trap2 chk2 addr2 lsv2 _ => @@ -282,25 +281,27 @@ Qed. Global Opaque hSinput. Local Hint Resolve hSinput_correct: wlp. -Definition hSop_hcodes (op:operation) (lhsv: list_hsval) (hsm: hsmem) := +Definition hSop_hcodes (op:operation) (lhsv: list_hsval) := DO hc <~ hash op_hcode;; DO hv <~ hash op;; - RET [hc;hv;list_hsval_get_hid lhsv; hsmem_get_hid hsm]. + RET [hc;hv;list_hsval_get_hid lhsv]. Extraction Inline hSop_hcodes. -Definition hSop (op:operation) (lhsv: list_hsval) (hsm: hsmem): ?? hsval := - DO hv <~ hSop_hcodes op lhsv hsm;; - hC_hsval {| hdata:=HSop op lhsv hsm unknown_hid; hcodes :=hv |}. +Definition hSop (op:operation) (lhsv: list_hsval): ?? hsval := + DO hv <~ hSop_hcodes op lhsv;; + hC_hsval {| hdata:=HSop op lhsv unknown_hid; hcodes :=hv |}. -Lemma hSop_correct op lhsv hsm: - WHEN hSop op lhsv hsm ~> hv THEN forall ge sp rs0 m0 lsv sm - (LR: list_sval_refines ge sp rs0 m0 lhsv lsv) - (MR: smem_refines ge sp rs0 m0 hsm sm), - sval_refines ge sp rs0 m0 hv (Sop op lsv sm). +Lemma hSop_correct op lhsv: + WHEN hSop op lhsv ~> hv THEN forall ge sp rs0 m0 lsv sm m + (MEM: seval_smem ge sp sm rs0 m0 = Some m) + (MVALID: forall b ofs, Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) + (LR: list_sval_refines ge sp rs0 m0 lhsv lsv), + sval_refines ge sp rs0 m0 hv (Sop op lsv sm). Proof. wlp_simplify. - rewrite <- LR, <- MR. - auto. + rewrite <- H, MEM, LR. + destruct (seval_list_sval _ _ lsv _); try congruence. + eapply op_valid_pointer_eq; eauto. Qed. Global Opaque hSop. Local Hint Resolve hSop_correct: wlp. @@ -529,31 +530,10 @@ Definition root_apply (rsv: root_sval) (lr: list reg) (st: sistate_local): sval end. Coercion root_apply: root_sval >-> Funclass. -Definition hSop_hSinit (op:operation) (lhsv: list_hsval): ?? hsval := - DO hsi <~ hSinit ();; - hSop op lhsv hsi (** magically remove the dependency on sm ! *) - . - -Lemma hSop_hSinit_correct op lhsv: - WHEN hSop_hSinit op lhsv ~> hv THEN forall ge sp rs0 m0 lsv sm m - (MEM: seval_smem ge sp sm rs0 m0 = Some m) - (MVALID: forall b ofs, Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) - (LR: list_sval_refines ge sp rs0 m0 lhsv lsv), - sval_refines ge sp rs0 m0 hv (Sop op lsv sm). -Proof. - wlp_simplify. - erewrite H0; [ idtac | eauto | eauto ]. - rewrite H, MEM. - destruct (seval_list_sval _ _ lsv _); try congruence. - eapply op_valid_pointer_eq; eauto. -Qed. -Global Opaque hSop_hSinit. -Local Hint Resolve hSop_hSinit_correct: wlp. - Definition root_happly (rsv: root_sval) (lr: list reg) (hst: hsistate_local) : ?? hsval := DO lhsv <~ hlist_args hst lr;; match rsv with - | Rop op => hSop_hSinit op lhsv + | Rop op => hSop op lhsv | Rload trap chunk addr => hSload hst trap chunk addr lhsv end. @@ -624,7 +604,7 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hs | Some arg => hsi_sreg_get hst arg (** optimization of Omove *) | None => DO lhsv <~ hlist_args hst lr;; - hSop_hSinit op lhsv + hSop op lhsv end | Rload _ chunk addr => DO lhsv <~ hlist_args hst lr;; diff --git a/scheduling/RTLpathSE_simu_specs.v b/scheduling/RTLpathSE_simu_specs.v index 0c5ed3b8..48f5f65d 100644 --- a/scheduling/RTLpathSE_simu_specs.v +++ b/scheduling/RTLpathSE_simu_specs.v @@ -59,7 +59,7 @@ Definition siexits_simu (dm: PTree.t node) (f: RTLpath.function) (lse1 lse2: lis Inductive hsval := | HSinput (r: reg) (hid: hashcode) - | HSop (op: operation) (lhsv: list_hsval) (hsm: hsmem) (hid: hashcode) + | HSop (op: operation) (lhsv: list_hsval) (hid: hashcode) (** NB: does not depend on the memory ! *) | HSload (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval) (hid: hashcode) with list_hsval := | HSnil (hid: hashcode) @@ -86,10 +86,11 @@ Inductive hsfval := | HSreturn (res: option hsval) . +(** * gives the semantics of hash-consed symbolic values *) Fixpoint hsval_proj hsv := match hsv with | HSinput r _ => Sinput r - | HSop op hl hm _ => Sop op (hsval_list_proj hl) (hsmem_proj hm) + | HSop op hl _ => Sop op (hsval_list_proj hl) Sinit (** NB: use the initial memory of the path ! *) | HSload hm t chk addr hl _ => Sload (hsmem_proj hm) t chk addr (hsval_list_proj hl) end with hsval_list_proj hl := |