diff options
Diffstat (limited to 'scheduling/RTLpathSE_impl.v')
| -rw-r--r-- | scheduling/RTLpathSE_impl.v | 1664 |
1 files changed, 1664 insertions, 0 deletions
diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v new file mode 100644 index 00000000..e21d7cd1 --- /dev/null +++ b/scheduling/RTLpathSE_impl.v @@ -0,0 +1,1664 @@ +(** Implementation and refinement of the symbolic execution *) + +Require Import Coqlib Maps Floats. +Require Import AST Integers Values Events Memory Globalenvs Smallstep. +Require Import Op Registers. +Require Import RTL RTLpath. +Require Import Errors. +Require Import RTLpathSE_theory RTLpathLivegenproof. +Require Import Axioms RTLpathSE_simu_specs. +Require Import RTLpathSE_simplify. + +Local Open Scope error_monad_scope. +Local Open Scope option_monad_scope. + +Require Import Impure.ImpHCons. +Import Notations. +Import HConsing. + +Local Open Scope impure. +Local Open Scope hse. + +Import ListNotations. +Local Open Scope list_scope. + +Definition XDEBUG {A} (x:A) (k: A -> ?? pstring): ?? unit := RET tt. (* TO REMOVE DEBUG INFO *) +(*Definition XDEBUG {A} (x:A) (k: A -> ?? pstring): ?? unit := DO s <~ k x;; println ("DEBUG simu_check:" +; s). (* TO INSERT DEBUG INFO *)*) + +Definition DEBUG (s: pstring): ?? unit := XDEBUG tt (fun _ => RET s). + +(** * Implementation of Data-structure use in Hash-consing *) + +Definition hsval_get_hid (hsv: hsval): hashcode := + match hsv with + | HSinput _ hid => hid + | HSop _ _ hid => hid + | HSload _ _ _ _ _ hid => hid + end. + +Definition list_hsval_get_hid (lhsv: list_hsval): hashcode := + match lhsv with + | HSnil hid => hid + | HScons _ _ hid => hid + end. + +Definition hsmem_get_hid (hsm: hsmem): hashcode := + match hsm with + | HSinit hid => hid + | HSstore _ _ _ _ _ hid => hid + end. + +Definition hsval_set_hid (hsv: hsval) (hid: hashcode): hsval := + match hsv with + | HSinput r _ => HSinput r hid + | HSop o lhsv _ => HSop o lhsv hid + | HSload hsm trap chunk addr lhsv _ => HSload hsm trap chunk addr lhsv hid + end. + +Definition list_hsval_set_hid (lhsv: list_hsval) (hid: hashcode): list_hsval := + match lhsv with + | HSnil _ => HSnil hid + | HScons hsv lhsv _ => HScons hsv lhsv hid + end. + +Definition hsmem_set_hid (hsm: hsmem) (hid: hashcode): hsmem := + match hsm with + | HSinit _ => HSinit hid + | HSstore hsm chunk addr lhsv srce _ => HSstore hsm chunk addr lhsv srce hid + end. + + +Lemma hsval_set_hid_correct x y ge sp rs0 m0: + hsval_set_hid x unknown_hid = hsval_set_hid y unknown_hid -> + seval_hsval ge sp x rs0 m0 = seval_hsval ge sp y rs0 m0. +Proof. + destruct x, y; intro H; inversion H; subst; simpl; auto. +Qed. +Local Hint Resolve hsval_set_hid_correct: core. + +Lemma list_hsval_set_hid_correct x y ge sp rs0 m0: + list_hsval_set_hid x unknown_hid = list_hsval_set_hid y unknown_hid -> + seval_list_hsval ge sp x rs0 m0 = seval_list_hsval ge sp y rs0 m0. +Proof. + destruct x, y; intro H; inversion H; subst; simpl; auto. +Qed. +Local Hint Resolve list_hsval_set_hid_correct: core. + +Lemma hsmem_set_hid_correct x y ge sp rs0 m0: + hsmem_set_hid x unknown_hid = hsmem_set_hid y unknown_hid -> + seval_hsmem ge sp x rs0 m0 = seval_hsmem ge sp y rs0 m0. +Proof. + destruct x, y; intro H; inversion H; subst; simpl; auto. +Qed. +Local Hint Resolve hsmem_set_hid_correct: core. + +(** Now, we build the hash-Cons value from a "hash_eq". + + Informal specification: + [hash_eq] must be consistent with the "hashed" constructors defined above. + + We expect that hashinfo values in the code of these "hashed" constructors verify: + (hash_eq (hdata x) (hdata y) ~> true) <-> (hcodes x)=(hcodes y) +*) + + +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 _, HSop op2 lsv2 _ => + DO b1 <~ phys_eq lsv1 lsv2;; + 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 _ => + DO b1 <~ phys_eq lsv1 lsv2;; + DO b2 <~ phys_eq sm1 sm2;; + DO b3 <~ struct_eq trap1 trap2;; + DO b4 <~ struct_eq chk1 chk2;; + if b1 && b2 && b3 && b4 + then struct_eq addr1 addr2 + else RET false + | _,_ => RET false + end. + + +Lemma and_true_split a b: a && b = true <-> a = true /\ b = true. +Proof. + destruct a; simpl; intuition. +Qed. + +Lemma hsval_hash_eq_correct x y: + WHEN hsval_hash_eq x y ~> b THEN + b = true -> hsval_set_hid x unknown_hid = hsval_set_hid y unknown_hid. +Proof. + destruct x, y; wlp_simplify; try (rewrite !and_true_split in *); intuition; subst; try congruence. +Qed. +Global Opaque hsval_hash_eq. +Local Hint Resolve hsval_hash_eq_correct: wlp. + +Definition list_hsval_hash_eq (lsv1 lsv2: list_hsval): ?? bool := + match lsv1, lsv2 with + | HSnil _, HSnil _ => RET true + | HScons sv1 lsv1' _, HScons sv2 lsv2' _ => + DO b <~ phys_eq lsv1' lsv2';; + if b + then phys_eq sv1 sv2 + else RET false + | _,_ => RET false + end. + +Lemma list_hsval_hash_eq_correct x y: + WHEN list_hsval_hash_eq x y ~> b THEN + b = true -> list_hsval_set_hid x unknown_hid = list_hsval_set_hid y unknown_hid. +Proof. + destruct x, y; wlp_simplify; try (rewrite !and_true_split in *); intuition; subst; try congruence. +Qed. +Global Opaque list_hsval_hash_eq. +Local Hint Resolve list_hsval_hash_eq_correct: wlp. + +Definition hsmem_hash_eq (sm1 sm2: hsmem): ?? bool := + match sm1, sm2 with + | HSinit _, HSinit _ => RET true + | HSstore sm1 chk1 addr1 lsv1 sv1 _, HSstore sm2 chk2 addr2 lsv2 sv2 _ => + DO b1 <~ phys_eq lsv1 lsv2;; + DO b2 <~ phys_eq sm1 sm2;; + DO b3 <~ phys_eq sv1 sv2;; + DO b4 <~ struct_eq chk1 chk2;; + if b1 && b2 && b3 && b4 + then struct_eq addr1 addr2 + else RET false + | _,_ => RET false + end. + +Lemma hsmem_hash_eq_correct x y: + WHEN hsmem_hash_eq x y ~> b THEN + b = true -> hsmem_set_hid x unknown_hid = hsmem_set_hid y unknown_hid. +Proof. + destruct x, y; wlp_simplify; try (rewrite !and_true_split in *); intuition; subst; try congruence. +Qed. +Global Opaque hsmem_hash_eq. +Local Hint Resolve hsmem_hash_eq_correct: wlp. + + +Definition hSVAL: hashP hsval := {| hash_eq := hsval_hash_eq; get_hid:=hsval_get_hid; set_hid:=hsval_set_hid |}. +Definition hLSVAL: hashP list_hsval := {| hash_eq := list_hsval_hash_eq; get_hid:= list_hsval_get_hid; set_hid:= list_hsval_set_hid |}. +Definition hSMEM: hashP hsmem := {| hash_eq := hsmem_hash_eq; get_hid:= hsmem_get_hid; set_hid:= hsmem_set_hid |}. + +Program Definition mk_hash_params: Dict.hash_params hsval := + {| + Dict.test_eq := phys_eq; + Dict.hashing := fun (ht: hsval) => RET (hsval_get_hid ht); + Dict.log := fun hv => + DO hv_name <~ string_of_hashcode (hsval_get_hid hv);; + println ("unexpected undef behavior of hashcode:" +; (CamlStr hv_name)) |}. +Obligation 1. + wlp_simplify. +Qed. + +(** ** various auxiliary (trivial lemmas) *) +Lemma hsilocal_refines_sreg ge sp rs0 m0 hst st: + hsilocal_refines ge sp rs0 m0 hst st -> hsok_local ge sp rs0 m0 hst -> forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (si_sreg st r) rs0 m0. +Proof. + unfold hsilocal_refines; intuition. +Qed. +Local Hint Resolve hsilocal_refines_sreg: core. + +Lemma hsilocal_refines_valid_pointer ge sp rs0 m0 hst st: + hsilocal_refines ge sp rs0 m0 hst st -> forall m b ofs, seval_smem ge sp st.(si_smem) rs0 m0 = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs. +Proof. + unfold hsilocal_refines; intuition. +Qed. +Local Hint Resolve hsilocal_refines_valid_pointer: core. + +Lemma hsilocal_refines_smem_refines ge sp rs0 m0 hst st: + hsilocal_refines ge sp rs0 m0 hst st -> hsok_local ge sp rs0 m0 hst -> smem_refines ge sp rs0 m0 (hsi_smem hst) (st.(si_smem)). +Proof. + unfold hsilocal_refines; intuition. +Qed. +Local Hint Resolve hsilocal_refines_smem_refines: core. + +Lemma hsistate_refines_dyn_exits ge sp rs0 m0 hst st: + hsistate_refines_dyn ge sp rs0 m0 hst st -> hsiexits_refines_dyn ge sp rs0 m0 (hsi_exits hst) (si_exits st). +Proof. + unfold hsistate_refines_dyn; intuition. +Qed. +Local Hint Resolve hsistate_refines_dyn_exits: core. + +Lemma hsistate_refines_dyn_local ge sp rs0 m0 hst st: + hsistate_refines_dyn ge sp rs0 m0 hst st -> hsilocal_refines ge sp rs0 m0 (hsi_local hst) (si_local st). +Proof. + unfold hsistate_refines_dyn; intuition. +Qed. +Local Hint Resolve hsistate_refines_dyn_local: core. + +Lemma hsistate_refines_dyn_nested ge sp rs0 m0 hst st: + hsistate_refines_dyn ge sp rs0 m0 hst st -> nested_sok ge sp rs0 m0 (si_local st) (si_exits st). +Proof. + unfold hsistate_refines_dyn; intuition. +Qed. +Local Hint Resolve hsistate_refines_dyn_nested: core. + +(** * Implementation of symbolic execution *) +Section CanonBuilding. + +Variable hC_hsval: hashinfo hsval -> ?? hsval. + +Hypothesis hC_hsval_correct: forall hs, + WHEN hC_hsval hs ~> hs' THEN forall ge sp rs0 m0, + seval_hsval ge sp (hdata hs) rs0 m0 = seval_hsval ge sp hs' rs0 m0. + +Variable hC_list_hsval: hashinfo list_hsval -> ?? list_hsval. +Hypothesis hC_list_hsval_correct: forall lh, + WHEN hC_list_hsval lh ~> lh' THEN forall ge sp rs0 m0, + seval_list_hsval ge sp (hdata lh) rs0 m0 = seval_list_hsval ge sp lh' rs0 m0. + +Variable hC_hsmem: hashinfo hsmem -> ?? hsmem. +Hypothesis hC_hsmem_correct: forall hm, + WHEN hC_hsmem hm ~> hm' THEN forall ge sp rs0 m0, + seval_hsmem ge sp (hdata hm) rs0 m0 = seval_hsmem ge sp hm' rs0 m0. + +(* First, we wrap constructors for hashed values !*) + +Definition reg_hcode := 1. +Definition op_hcode := 2. +Definition load_hcode := 3. + +Definition hSinput_hcodes (r: reg) := + DO hc <~ hash reg_hcode;; + DO hv <~ hash r;; + RET [hc;hv]. +Extraction Inline hSinput_hcodes. + +Definition hSinput (r:reg): ?? hsval := + DO hv <~ hSinput_hcodes r;; + hC_hsval {| hdata:=HSinput r unknown_hid; hcodes :=hv; |}. + +Lemma hSinput_correct r: + WHEN hSinput r ~> hv THEN forall ge sp rs0 m0, + sval_refines ge sp rs0 m0 hv (Sinput r). +Proof. + wlp_simplify. +Qed. +Global Opaque hSinput. +Local Hint Resolve hSinput_correct: wlp. + +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]. +Extraction Inline hSop_hcodes. + +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_fSop_correct op lhsv: + WHEN hSop op lhsv ~> hv THEN forall ge sp rs0 m0, + seval_hsval ge sp hv rs0 m0 = seval_hsval ge sp (fSop op lhsv) rs0 m0. +Proof. + wlp_simplify. +Qed. +Global Opaque hSop. +Local Hint Resolve hSop_fSop_correct: wlp_raw. + +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. + generalize fSop_correct; simpl. + intros X. + wlp_xsimplify ltac:(intuition eauto with wlp wlp_raw). + erewrite H, X; eauto. +Qed. +Local Hint Resolve hSop_correct: wlp. + +Definition hSload_hcodes (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval):= + DO hc <~ hash load_hcode;; + DO hv1 <~ hash trap;; + DO hv2 <~ hash chunk;; + DO hv3 <~ hash addr;; + RET [hc; hsmem_get_hid hsm; hv1; hv2; hv3; list_hsval_get_hid lhsv]. +Extraction Inline hSload_hcodes. + +Definition hSload (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval): ?? hsval := + DO hv <~ hSload_hcodes hsm trap chunk addr lhsv;; + hC_hsval {| hdata := HSload hsm trap chunk addr lhsv unknown_hid; hcodes := hv |}. + +Lemma hSload_correct hsm trap chunk addr lhsv: + WHEN hSload hsm trap chunk addr lhsv ~> 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 (Sload sm trap chunk addr lsv). +Proof. + wlp_simplify. + rewrite <- LR, <- MR. + auto. +Qed. +Global Opaque hSload. +Local Hint Resolve hSload_correct: wlp. + +Definition hSnil (_: unit): ?? list_hsval := + hC_list_hsval {| hdata := HSnil unknown_hid; hcodes := nil |}. + +Lemma hSnil_correct: + WHEN hSnil() ~> hv THEN forall ge sp rs0 m0, + list_sval_refines ge sp rs0 m0 hv Snil. +Proof. + wlp_simplify. +Qed. +Global Opaque hSnil. +Local Hint Resolve hSnil_correct: wlp. + +Definition hScons (hsv: hsval) (lhsv: list_hsval): ?? list_hsval := + hC_list_hsval {| hdata := HScons hsv lhsv unknown_hid; hcodes := [hsval_get_hid hsv; list_hsval_get_hid lhsv] |}. + +Lemma hScons_correct hsv lhsv: + WHEN hScons hsv lhsv ~> lhsv' THEN forall ge sp rs0 m0 sv lsv + (VR: sval_refines ge sp rs0 m0 hsv sv) + (LR: list_sval_refines ge sp rs0 m0 lhsv lsv), + list_sval_refines ge sp rs0 m0 lhsv' (Scons sv lsv). +Proof. + wlp_simplify. + rewrite <- VR, <- LR. + auto. +Qed. +Global Opaque hScons. +Local Hint Resolve hScons_correct: wlp. + +Definition hSinit (_: unit): ?? hsmem := + hC_hsmem {| hdata := HSinit unknown_hid; hcodes := nil |}. + +Lemma hSinit_correct: + WHEN hSinit() ~> hm THEN forall ge sp rs0 m0, + smem_refines ge sp rs0 m0 hm Sinit. +Proof. + wlp_simplify. +Qed. +Global Opaque hSinit. +Local Hint Resolve hSinit_correct: wlp. + +Definition hSstore_hcodes (hsm: hsmem) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval) (srce: hsval):= + DO hv1 <~ hash chunk;; + DO hv2 <~ hash addr;; + RET [hsmem_get_hid hsm; hv1; hv2; list_hsval_get_hid lhsv; hsval_get_hid srce]. +Extraction Inline hSstore_hcodes. + +Definition hSstore (hsm: hsmem) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval) (srce: hsval): ?? hsmem := + DO hv <~ hSstore_hcodes hsm chunk addr lhsv srce;; + hC_hsmem {| hdata := HSstore hsm chunk addr lhsv srce unknown_hid; hcodes := hv |}. + +Lemma hSstore_correct hsm chunk addr lhsv hsv: + WHEN hSstore hsm chunk addr lhsv hsv ~> hsm' THEN forall ge sp rs0 m0 lsv sm sv + (LR: list_sval_refines ge sp rs0 m0 lhsv lsv) + (MR: smem_refines ge sp rs0 m0 hsm sm) + (VR: sval_refines ge sp rs0 m0 hsv sv), + smem_refines ge sp rs0 m0 hsm' (Sstore sm chunk addr lsv sv). +Proof. + wlp_simplify. + rewrite <- LR, <- MR, <- VR. + auto. +Qed. +Global Opaque hSstore. +Local Hint Resolve hSstore_correct: wlp. + +Definition hsi_sreg_get (hst: PTree.t hsval) r: ?? hsval := + match PTree.get r hst with + | None => hSinput r + | Some sv => RET sv + end. + +Lemma hsi_sreg_get_correct hst r: + WHEN hsi_sreg_get hst r ~> hsv THEN forall ge sp rs0 m0 (f: reg -> sval) + (RR: forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0), + sval_refines ge sp rs0 m0 hsv (f r). +Proof. + unfold hsi_sreg_eval, hsi_sreg_proj; wlp_simplify; rewrite <- RR; try_simplify_someHyps. +Qed. +Global Opaque hsi_sreg_get. +Local Hint Resolve hsi_sreg_get_correct: wlp. + +Fixpoint hlist_args (hst: PTree.t hsval) (l: list reg): ?? list_hsval := + match l with + | nil => hSnil() + | r::l => + DO v <~ hsi_sreg_get hst r;; + DO lhsv <~ hlist_args hst l;; + hScons v lhsv + end. + +Lemma hlist_args_correct hst l: + WHEN hlist_args hst l ~> lhsv THEN forall ge sp rs0 m0 (f: reg -> sval) + (RR: forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0), + list_sval_refines ge sp rs0 m0 lhsv (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 hsv: ?? hsval := + match hsv with + | HSinput r hc => + DO b <~ phys_eq hc unknown_hid;; + if b + then hSinput r (* was not yet really hash-consed *) + else RET hsv (* already hash-consed *) + | HSop 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 hsv (* already hash-consed *) + | HSload hm t chk addr hl _ => RET hsv (* FIXME ? *) + end +with fsval_list_proj hsl: ?? list_hsval := + match hsl with + | HSnil hc => + DO b <~ phys_eq hc unknown_hid;; + if b + then hSnil() (* was not yet really hash-consed *) + else RET hsl (* already hash-consed *) + | HScons 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 hsl (* already hash-consed *) + end. + +Lemma fsval_proj_correct hsv: + WHEN fsval_proj hsv ~> hsv' THEN forall ge sp rs0 m0, + seval_hsval ge sp hsv rs0 m0 = seval_hsval ge sp hsv' rs0 m0. +Proof. + induction hsv using hsval_mut + with (P0 := fun lhsv => + WHEN fsval_list_proj lhsv ~> lhsv' THEN forall ge sp rs0 m0, + seval_list_hsval ge sp lhsv rs0 m0 = seval_list_hsval ge sp lhsv' rs0 m0) + (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 lhsv: + WHEN fsval_list_proj lhsv ~> lhsv' THEN forall ge sp rs0 m0, + seval_list_hsval ge sp lhsv rs0 m0 = seval_list_hsval ge sp lhsv' rs0 m0. +Proof. + induction lhsv; wlp_simplify. + erewrite H0, H1; eauto. +Qed. +Global Opaque fsval_list_proj. +Local Hint Resolve fsval_list_proj_correct: wlp. + + +(** ** Assignment of memory *) +Definition hslocal_set_smem (hst:hsistate_local) hm := + {| hsi_smem := hm; + hsi_ok_lsval := hsi_ok_lsval hst; + hsi_sreg:= hsi_sreg hst + |}. + +Lemma sok_local_set_mem ge sp rs0 m0 st sm: + sok_local ge sp rs0 m0 (slocal_set_smem st sm) + <-> (sok_local ge sp rs0 m0 st /\ seval_smem ge sp sm rs0 m0 <> None). +Proof. + unfold slocal_set_smem, sok_local; simpl; intuition (subst; eauto). +Qed. + +Lemma hsok_local_set_mem ge sp rs0 m0 hst hsm: + (seval_hsmem ge sp (hsi_smem hst) rs0 m0 = None -> seval_hsmem ge sp hsm rs0 m0 = None) -> + hsok_local ge sp rs0 m0 (hslocal_set_smem hst hsm) + <-> (hsok_local ge sp rs0 m0 hst /\ seval_hsmem ge sp hsm rs0 m0 <> None). +Proof. + unfold hslocal_set_smem, hsok_local; simpl; intuition. +Qed. + +Lemma hslocal_set_mem_correct ge sp rs0 m0 hst st hsm sm: + (seval_hsmem ge sp (hsi_smem hst) rs0 m0 = None -> seval_hsmem ge sp hsm rs0 m0 = None) -> + (forall m b ofs, seval_smem ge sp sm rs0 m0 = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) -> + hsilocal_refines ge sp rs0 m0 hst st -> + (hsok_local ge sp rs0 m0 hst -> smem_refines ge sp rs0 m0 hsm sm) -> + hsilocal_refines ge sp rs0 m0 (hslocal_set_smem hst hsm) (slocal_set_smem st sm). +Proof. + intros PRESERV SMVALID (OKEQ & SMEMEQ' & REGEQ & MVALID) SMEMEQ. + split; rewrite! hsok_local_set_mem; simpl; eauto; try tauto. + rewrite sok_local_set_mem. + intuition congruence. +Qed. + +Definition hslocal_store (hst: hsistate_local) chunk addr args src: ?? hsistate_local := + let pt := hst.(hsi_sreg) in + DO hargs <~ hlist_args pt args;; + DO hsrc <~ hsi_sreg_get pt src;; + DO hm <~ hSstore hst chunk addr hargs hsrc;; + RET (hslocal_set_smem hst hm). + +Lemma hslocal_store_correct hst chunk addr args src: + WHEN hslocal_store hst chunk addr args src ~> hst' THEN forall ge sp rs0 m0 st + (REF: hsilocal_refines ge sp rs0 m0 hst st), + hsilocal_refines ge sp rs0 m0 hst' (slocal_store st chunk addr args src). +Proof. + wlp_simplify. + eapply hslocal_set_mem_correct; simpl; eauto. + + intros X; erewrite H1; eauto. + rewrite X. simplify_SOME z. + + unfold hsilocal_refines in *; + simplify_SOME z; intuition. + erewrite <- Mem.storev_preserv_valid; [| eauto]. + eauto. + + unfold hsilocal_refines in *; intuition eauto. +Qed. +Global Opaque hslocal_store. +Local Hint Resolve hslocal_store_correct: wlp. + +(** ** Assignment of local state *) + +Definition hsist_set_local (hst: hsistate) (pc: node) (hnxt: hsistate_local): hsistate := + {| hsi_pc := pc; hsi_exits := hst.(hsi_exits); hsi_local:= hnxt |}. + +Lemma hsist_set_local_correct_stat hst st pc hnxt nxt: + hsistate_refines_stat hst st -> + hsistate_refines_stat (hsist_set_local hst pc hnxt) (sist_set_local st pc nxt). +Proof. + unfold hsistate_refines_stat; simpl; intuition. +Qed. + +Lemma hsist_set_local_correct_dyn ge sp rs0 m0 hst st pc hnxt nxt: + hsistate_refines_dyn ge sp rs0 m0 hst st -> + hsilocal_refines ge sp rs0 m0 hnxt nxt -> + (sok_local ge sp rs0 m0 nxt -> sok_local ge sp rs0 m0 (si_local st)) -> + hsistate_refines_dyn ge sp rs0 m0 (hsist_set_local hst pc hnxt) (sist_set_local st pc nxt). +Proof. + unfold hsistate_refines_dyn; simpl. + intros (EREF & LREF & NESTED) LREFN SOK; intuition. + destruct NESTED as [|st0 se lse TOP NEST]; econstructor; simpl; auto. +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_local): sval := + let lsv := list_sval_inj (List.map (si_sreg st) lr) in + let sm := si_smem st in + match rsv with + | Rop op => Sop op lsv sm + | Rload trap chunk addr => Sload sm trap chunk addr lsv + end. +Coercion root_apply: root_sval >-> Funclass. + +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 op lhsv + | Rload trap chunk addr => hSload hst trap chunk addr lhsv + end. + +Lemma root_happly_correct (rsv: root_sval) lr hst: + WHEN root_happly rsv lr hst ~> hv' THEN forall ge sp rs0 m0 st + (REF:hsilocal_refines ge sp rs0 m0 hst st) + (OK:hsok_local ge sp rs0 m0 hst), + sval_refines ge sp rs0 m0 hv' (rsv lr st). +Proof. + unfold hsilocal_refines, root_apply, root_happly; destruct rsv; wlp_simplify. + unfold sok_local in *. + generalize (H0 ge sp rs0 m0 (list_sval_inj (map (si_sreg st) lr)) (si_smem st)); clear H0. + destruct (seval_smem ge sp (si_smem st) rs0 m0) as [m|] eqn:X; eauto. + intuition congruence. +Qed. +Global Opaque root_happly. +Hint Resolve root_happly_correct: wlp. + +Local Open Scope lazy_bool_scope. + +(* NB: return [false] if the rsv cannot fail *) +Definition may_trap (rsv: root_sval) (lr: list reg): bool := + match rsv with + | Rop op => is_trapping_op op ||| negb (Nat.eqb (length lr) (args_of_operation op)) (* cf. lemma is_trapping_op_sound *) + | Rload TRAP _ _ => true + | _ => false + end. + +Lemma lazy_orb_negb_false (b1 b2:bool): + (b1 ||| negb b2) = false <-> (b1 = false /\ b2 = true). +Proof. + unfold negb; explore; simpl; intuition (try congruence). +Qed. + +Lemma seval_list_sval_length ge sp rs0 m0 (f: reg -> sval) (l:list reg): + forall l', seval_list_sval ge sp (list_sval_inj (List.map f l)) rs0 m0 = Some l' -> + Datatypes.length l = Datatypes.length l'. +Proof. + induction l. + - simpl. intros. inv H. reflexivity. + - simpl. intros. destruct (seval_sval _ _ _ _ _); [|discriminate]. + destruct (seval_list_sval _ _ _ _ _) eqn:SLS; [|discriminate]. inv H. simpl. + erewrite IHl; eauto. +Qed. + +Lemma may_trap_correct (ge: RTL.genv) (sp:val) (rsv: root_sval) (rs0: regset) (m0: mem) (lr: list reg) st: + may_trap rsv lr = false -> + seval_list_sval ge sp (list_sval_inj (List.map (si_sreg st) lr)) rs0 m0 <> None -> + seval_smem ge sp (si_smem st) rs0 m0 <> None -> + seval_sval ge sp (rsv lr st) rs0 m0 <> None. +Proof. + destruct rsv; simpl; try congruence. + - rewrite lazy_orb_negb_false. intros (TRAP1 & TRAP2) OK1 OK2. + explore; try congruence. + eapply is_trapping_op_sound; eauto. + erewrite <- seval_list_sval_length; eauto. + apply Nat.eqb_eq in TRAP2. + assumption. + - intros X OK1 OK2. + explore; try congruence. +Qed. + +(** simplify a symbolic value before assignment to a register *) +Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hsval := + match rsv with + | Rop op => + match is_move_operation op lr with + | Some arg => hsi_sreg_get hst arg (* optimization of Omove *) + | None => + match target_op_simplify op lr hst with + | Some fhv => fsval_proj fhv + | None => + DO lhsv <~ hlist_args hst lr;; + hSop op lhsv + end + end + | Rload _ chunk addr => + DO lhsv <~ hlist_args hst lr;; + hSload hst NOTRAP chunk addr lhsv + end. + +Lemma simplify_correct rsv lr hst: + WHEN simplify rsv lr hst ~> hv THEN forall ge sp rs0 m0 st + (REF: hsilocal_refines ge sp rs0 m0 hst st) + (OK0: hsok_local ge sp rs0 m0 hst) + (OK1: seval_sval ge sp (rsv lr st) rs0 m0 <> None), + sval_refines ge sp rs0 m0 hv (rsv lr st). +Proof. + destruct rsv; simpl; auto. + - (* Rop *) + destruct (is_move_operation _ _) eqn: Hmove. + { wlp_simplify; exploit is_move_operation_correct; eauto. + intros (Hop & Hlsv); subst; simpl in *. + simplify_SOME z. + * erewrite H; eauto. + * try_simplify_someHyps; congruence. + * congruence. } + destruct (target_op_simplify _ _ _) eqn: Htarget_op_simp; wlp_simplify. + { destruct (seval_list_sval _ _ _) eqn: OKlist; try congruence. + destruct (seval_smem _ _ _ _ _) eqn: OKmem; try congruence. + rewrite <- H; exploit target_op_simplify_correct; eauto. } + clear Htarget_op_simp. + generalize (H0 ge sp rs0 m0 (list_sval_inj (map (si_sreg st) lr)) (si_smem st)); clear H0. + destruct (seval_smem ge sp (si_smem st) rs0 m0) as [m|] eqn:X; eauto. + intro H0; clear H0; simplify_SOME z; congruence. (* absurd case *) + - (* Rload *) + destruct trap; wlp_simplify. + erewrite H0; eauto. + erewrite H; eauto. + erewrite hsilocal_refines_smem_refines; eauto. + destruct (seval_list_sval _ _ _ _) as [args|] eqn: Hargs; try congruence. + destruct (eval_addressing _ _ _ _) as [a|] eqn: Ha; try congruence. + destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence. + destruct (Mem.loadv _ _ _); try congruence. +Qed. +Global Opaque simplify. +Local Hint Resolve simplify_correct: wlp. + +Definition red_PTree_set (r: reg) (hsv: hsval) (hst: PTree.t hsval): PTree.t hsval := + match hsv with + | HSinput r' _ => + if Pos.eq_dec r r' + then PTree.remove r' hst + else PTree.set r hsv hst + | _ => PTree.set r hsv hst + end. + +Lemma red_PTree_set_correct (r r0:reg) hsv hst ge sp rs0 m0: + hsi_sreg_eval ge sp (red_PTree_set r hsv hst) r0 rs0 m0 = hsi_sreg_eval ge sp (PTree.set r hsv hst) r0 rs0 m0. +Proof. + destruct hsv; simpl; auto. + destruct (Pos.eq_dec r r1); auto. + subst; unfold hsi_sreg_eval, hsi_sreg_proj. + destruct (Pos.eq_dec r0 r1); 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) hsv hst sv st ge sp rs0 m0: + hsilocal_refines ge sp rs0 m0 hst st -> + sval_refines ge sp rs0 m0 hsv sv -> + hsok_local ge sp rs0 m0 hst -> + hsi_sreg_eval ge sp (red_PTree_set r hsv hst) r0 rs0 m0 = seval_sval ge sp (if Pos.eq_dec r r0 then sv else si_sreg st r0) rs0 m0. +Proof. + intros; rewrite red_PTree_set_correct. + exploit hsilocal_refines_sreg; eauto. + unfold hsi_sreg_eval, hsi_sreg_proj. + destruct (Pos.eq_dec r r0); auto. + - subst. rewrite PTree.gss; simpl; auto. + - rewrite PTree.gso; simpl; eauto. +Qed. + +Lemma sok_local_set_sreg (rsv:root_sval) ge sp rs0 m0 st r lr: + sok_local ge sp rs0 m0 (slocal_set_sreg st r (rsv lr st)) + <-> (sok_local ge sp rs0 m0 st /\ seval_sval ge sp (rsv lr st) rs0 m0 <> None). +Proof. + unfold slocal_set_sreg, sok_local; simpl; split. + + intros ((SVAL0 & PRE) & SMEM & SVAL). + repeat (split; try tauto). + - intros r0; generalize (SVAL r0); clear SVAL; destruct (Pos.eq_dec r r0); try congruence. + - generalize (SVAL r); clear SVAL; destruct (Pos.eq_dec r r); try congruence. + + intros ((PRE & SMEM & SVAL0) & SVAL). + repeat (split; try tauto; eauto). + intros r0; destruct (Pos.eq_dec r r0); try congruence. +Qed. + +Definition hslocal_set_sreg (hst: hsistate_local) (r: reg) (rsv: root_sval) (lr: list reg): ?? hsistate_local := + DO ok_lhsv <~ + (if may_trap rsv lr + then DO hv <~ root_happly rsv lr hst;; + XDEBUG hv (fun hv => DO hv_name <~ string_of_hashcode (hsval_get_hid hv);; RET ("-- insert undef behavior of hashcode:" +; (CamlStr hv_name))%string);; + RET (hv::(hsi_ok_lsval hst)) + else RET (hsi_ok_lsval hst));; + DO simp <~ simplify rsv lr hst;; + RET {| hsi_smem := hst; + hsi_ok_lsval := ok_lhsv; + hsi_sreg := red_PTree_set r simp (hsi_sreg hst) |}. + +Lemma hslocal_set_sreg_correct hst r rsv lr: + WHEN hslocal_set_sreg hst r rsv lr ~> hst' THEN forall ge sp rs0 m0 st + (REF: hsilocal_refines ge sp rs0 m0 hst st), + hsilocal_refines ge sp rs0 m0 hst' (slocal_set_sreg st r (rsv lr st)). +Proof. + wlp_simplify. + + (* may_trap ~> true *) + assert (X: sok_local ge sp rs0 m0 (slocal_set_sreg st r (rsv lr st)) <-> + hsok_local ge sp rs0 m0 {| hsi_smem := hst; hsi_ok_lsval := exta :: hsi_ok_lsval hst; hsi_sreg := red_PTree_set r exta0 hst |}). + { rewrite sok_local_set_sreg; generalize REF. + intros (OKeq & MEM & REG & MVALID); rewrite OKeq; clear OKeq. + unfold hsok_local; simpl; intuition (subst; eauto); + erewrite <- H0 in *; eauto; unfold hsok_local; simpl; intuition eauto. + } + unfold hsilocal_refines; simpl; split; auto. + rewrite <- X, sok_local_set_sreg. intuition eauto. + - destruct REF; intuition eauto. + - generalize REF; intros (OKEQ & _). rewrite OKEQ in * |-; erewrite red_PTree_set_refines; eauto. + + (* may_trap ~> false *) + assert (X: sok_local ge sp rs0 m0 (slocal_set_sreg st r (rsv lr st)) <-> + hsok_local ge sp rs0 m0 {| hsi_smem := hst; hsi_ok_lsval := hsi_ok_lsval hst; hsi_sreg := red_PTree_set r exta hst |}). + { + rewrite sok_local_set_sreg; generalize REF. + intros (OKeq & MEM & REG & MVALID); rewrite OKeq. + unfold hsok_local; simpl; intuition (subst; eauto). + assert (X0:hsok_local ge sp rs0 m0 hst). { unfold hsok_local; intuition. } + exploit may_trap_correct; eauto. + * intro X1; eapply seval_list_sval_inj_not_none; eauto. + assert (X2: sok_local ge sp rs0 m0 st). { intuition. } + unfold sok_local in X2; intuition eauto. + * rewrite <- MEM; eauto. + } + unfold hsilocal_refines; simpl; split; auto. + rewrite <- X, sok_local_set_sreg. intuition eauto. + - destruct REF; intuition eauto. + - generalize REF; intros (OKEQ & _). rewrite OKEQ in * |-; erewrite red_PTree_set_refines; eauto. +Qed. +Global Opaque hslocal_set_sreg. +Local Hint Resolve hslocal_set_sreg_correct: wlp. + +(** ** Execution of one instruction *) + +(* TODO gourdinl + * This is just useful for debugging fake values hashcode projection *) +Fixpoint check_no_uhid lhsv := + match lhsv with + | HSnil hc => + DO b <~ phys_eq hc unknown_hid;; + assert_b (negb b) "fail no uhid";; + RET tt + | HScons hsv lhsv' hc => + DO b <~ phys_eq hc unknown_hid;; + assert_b (negb b) "fail no uhid";; + check_no_uhid lhsv' + end. + +Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg): ?? (condition * list_hsval) := + match target_cbranch_expanse prev cond args with + | Some (cond', vargs) => + DO vargs' <~ fsval_list_proj vargs;; + RET (cond', vargs') + | None => + DO vargs <~ hlist_args prev args ;; + RET (cond, vargs) + end. + +Lemma cbranch_expanse_correct hst c l: + WHEN cbranch_expanse hst c l ~> r THEN forall ge sp rs0 m0 st + (LREF : hsilocal_refines ge sp rs0 m0 hst st) + (OK: hsok_local ge sp rs0 m0 hst), + seval_condition ge sp (fst r) (hsval_list_proj (snd r)) (si_smem st) rs0 m0 = + seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0. +Proof. + unfold cbranch_expanse. + destruct (target_cbranch_expanse _ _ _) eqn: TARGET; wlp_simplify; + unfold seval_condition; erewrite <- H; eauto. + destruct p as [c' l']; simpl. + exploit target_cbranch_expanse_correct; eauto. +Qed. +Local Hint Resolve cbranch_expanse_correct: wlp. +Global Opaque cbranch_expanse. + +Definition hsiexec_inst (i: instruction) (hst: hsistate): ?? (option hsistate) := + match i with + | Inop pc' => + RET (Some (hsist_set_local hst pc' hst.(hsi_local))) + | Iop op args dst pc' => + DO next <~ hslocal_set_sreg hst.(hsi_local) dst (Rop op) args;; + RET (Some (hsist_set_local hst pc' next)) + | Iload trap chunk addr args dst pc' => + DO next <~ hslocal_set_sreg hst.(hsi_local) dst (Rload trap chunk addr) args;; + RET (Some (hsist_set_local hst pc' next)) + | Istore chunk addr args src pc' => + DO next <~ hslocal_store hst.(hsi_local) chunk addr args src;; + RET (Some (hsist_set_local hst pc' next)) + | Icond cond args ifso ifnot _ => + let prev := hst.(hsi_local) in + DO res <~ cbranch_expanse prev cond args;; + let (cond, vargs) := res in + let ex := {| hsi_cond:=cond; hsi_scondargs:=vargs; hsi_elocal := prev; hsi_ifso := ifso |} in + RET (Some {| hsi_pc := ifnot; hsi_exits := ex::hst.(hsi_exits); hsi_local := prev |}) + | _ => RET None + end. + +Remark hsiexec_inst_None_correct i hst: + WHEN hsiexec_inst i hst ~> o THEN forall st, o = None -> siexec_inst i st = None. +Proof. + destruct i; wlp_simplify; congruence. +Qed. + +Lemma seval_condition_refines hst st ge sp cond hargs args rs m: + hsok_local ge sp rs m hst -> + hsilocal_refines ge sp rs m hst st -> + list_sval_refines ge sp rs m hargs args -> + hseval_condition ge sp cond hargs (hsi_smem hst) rs m + = seval_condition ge sp cond args (si_smem st) rs m. + Proof. + intros HOK (_ & MEMEQ & _) LR. unfold hseval_condition, seval_condition. + rewrite LR, <- MEMEQ; auto. +Qed. + +Lemma sok_local_set_sreg_simp (rsv:root_sval) ge sp rs0 m0 st r lr: + sok_local ge sp rs0 m0 (slocal_set_sreg st r (rsv lr st)) + -> sok_local ge sp rs0 m0 st. +Proof. + rewrite sok_local_set_sreg; intuition. +Qed. + +Local Hint Resolve hsist_set_local_correct_stat: core. + +Lemma hsiexec_cond_noexp (hst: hsistate): forall l c0 n n0, + WHEN DO res <~ + (DO vargs <~ hlist_args (hsi_local hst) l;; RET ((c0, vargs)));; + (let (cond, vargs) := res in + RET (Some + {| + hsi_pc := n0; + hsi_exits := {| + hsi_cond := cond; + hsi_scondargs := vargs; + hsi_elocal := hsi_local hst; + hsi_ifso := n |} :: hsi_exits hst; + hsi_local := hsi_local hst |})) ~> o0 + THEN (forall (hst' : hsistate) (st : sistate), + o0 = Some hst' -> + exists st' : sistate, + Some + {| + si_pc := n0; + si_exits := {| + si_cond := c0; + si_scondargs := list_sval_inj + (map (si_sreg (si_local st)) l); + si_elocal := si_local st; + si_ifso := n |} :: si_exits st; + si_local := si_local st |} = Some st' /\ + (hsistate_refines_stat hst st -> hsistate_refines_stat hst' st') /\ + (forall (ge : RTL.genv) (sp : val) (rs0 : regset) (m0 : mem), + hsistate_refines_dyn ge sp rs0 m0 hst st -> + hsistate_refines_dyn ge sp rs0 m0 hst' st')). +Proof. + intros. + wlp_simplify; try_simplify_someHyps; eexists; intuition eauto. + - unfold hsistate_refines_stat, hsiexits_refines_stat in *; simpl; intuition. + constructor; simpl; eauto. + constructor. + - destruct H0 as (EXREF & LREF & NEST). + split. + + constructor; simpl; auto. + constructor; simpl; auto. + intros; erewrite seval_condition_refines; eauto. + + split; simpl; auto. + destruct NEST as [|st0 se lse TOP NEST]; + econstructor; simpl; auto; constructor; auto. +Qed. + +Lemma hsiexec_inst_correct i hst: + WHEN hsiexec_inst i hst ~> o THEN forall hst' st, + o = Some hst' -> + exists st', siexec_inst i st = Some st' + /\ (forall (REF:hsistate_refines_stat hst st), hsistate_refines_stat hst' st') + /\ (forall ge sp rs0 m0 (REF:hsistate_refines_dyn ge sp rs0 m0 hst st), hsistate_refines_dyn ge sp rs0 m0 hst' st'). +Proof. + destruct i; simpl; + try (wlp_simplify; try_simplify_someHyps; eexists; intuition eauto; fail). + - (* refines_dyn Iop *) + wlp_simplify; try_simplify_someHyps; eexists; intuition eauto. + eapply hsist_set_local_correct_dyn; eauto. + generalize (sok_local_set_sreg_simp (Rop o)); simpl; eauto. + - (* refines_dyn Iload *) + wlp_simplify; try_simplify_someHyps; eexists; intuition eauto. + eapply hsist_set_local_correct_dyn; eauto. + generalize (sok_local_set_sreg_simp (Rload t0 m a)); simpl; eauto. + - (* refines_dyn Istore *) + wlp_simplify; try_simplify_someHyps; eexists; intuition eauto. + eapply hsist_set_local_correct_dyn; eauto. + unfold sok_local; simpl; intuition. + - (* refines_stat Icond *) + wlp_simplify; try_simplify_someHyps; eexists; intuition eauto. + + unfold hsistate_refines_stat, hsiexits_refines_stat in *; simpl; intuition. + constructor; simpl; eauto. + constructor. + + destruct REF as (EXREF & LREF & NEST). + split. + * constructor; simpl; auto. + constructor; simpl; auto. + intros; erewrite seval_condition_refines; eauto. + * split; simpl; auto. + destruct NEST as [|st0 se lse TOP NEST]; + econstructor; simpl; auto; constructor; auto. +Qed. +Global Opaque hsiexec_inst. +Local Hint Resolve hsiexec_inst_correct: wlp. + + +Definition some_or_fail {A} (o: option A) (msg: pstring): ?? A := + match o with + | Some x => RET x + | None => FAILWITH msg + end. + +Fixpoint hsiexec_path (path:nat) (f: function) (hst: hsistate): ?? hsistate := + match path with + | O => RET hst + | S p => + let pc := hst.(hsi_pc) in + XDEBUG pc (fun pc => DO name_pc <~ string_of_Z (Zpos pc);; RET ("- sym exec node: " +; name_pc)%string);; + DO i <~ some_or_fail ((fn_code f)!pc) "hsiexec_path.internal_error.1";; + DO ohst1 <~ hsiexec_inst i hst;; + DO hst1 <~ some_or_fail ohst1 "hsiexec_path.internal_error.2";; + hsiexec_path p f hst1 + end. + +Lemma hsiexec_path_correct path f: forall hst, + WHEN hsiexec_path path f hst ~> hst' THEN forall st + (RSTAT:hsistate_refines_stat hst st), + exists st', siexec_path path f st = Some st' + /\ hsistate_refines_stat hst' st' + /\ (forall ge sp rs0 m0 (REF:hsistate_refines_dyn ge sp rs0 m0 hst st), hsistate_refines_dyn ge sp rs0 m0 hst' st'). +Proof. + induction path; wlp_simplify; try_simplify_someHyps. clear IHpath. + generalize RSTAT; intros (PCEQ & _) INSTEQ. + rewrite <- PCEQ, INSTEQ; simpl. + exploit H0; eauto. clear H0. + intros (st0 & SINST & ISTAT & IDYN); erewrite SINST. + exploit H1; eauto. clear H1. + intros (st' & SPATH & PSTAT & PDYN). + eexists; intuition eauto. +Qed. +Global Opaque hsiexec_path. +Local Hint Resolve hsiexec_path_correct: wlp. + +Fixpoint hbuiltin_arg (hst: PTree.t hsval) (arg : builtin_arg reg): ?? builtin_arg hsval := + match arg with + | BA r => + DO v <~ hsi_sreg_get hst r;; + RET (BA v) + | BA_int n => RET (BA_int n) + | BA_long n => RET (BA_long n) + | BA_float f0 => RET (BA_float f0) + | BA_single s => RET (BA_single s) + | BA_loadstack chunk ptr => RET (BA_loadstack chunk ptr) + | BA_addrstack ptr => RET (BA_addrstack ptr) + | BA_loadglobal chunk id ptr => RET (BA_loadglobal chunk id ptr) + | BA_addrglobal id ptr => RET (BA_addrglobal id ptr) + | BA_splitlong ba1 ba2 => + DO v1 <~ hbuiltin_arg hst ba1;; + DO v2 <~ hbuiltin_arg hst ba2;; + RET (BA_splitlong v1 v2) + | BA_addptr ba1 ba2 => + DO v1 <~ hbuiltin_arg hst ba1;; + DO v2 <~ hbuiltin_arg hst ba2;; + RET (BA_addptr v1 v2) + end. + +Lemma hbuiltin_arg_correct hst arg: + WHEN hbuiltin_arg hst arg ~> hargs THEN forall ge sp rs0 m0 (f: reg -> sval) + (RR: forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0), + seval_builtin_sval ge sp (builtin_arg_map hsval_proj hargs) rs0 m0 = seval_builtin_sval ge sp (builtin_arg_map f arg) rs0 m0. +Proof. + induction arg; wlp_simplify. + + erewrite H; eauto. + + erewrite H; eauto. + erewrite H0; eauto. + + erewrite H; eauto. + erewrite H0; eauto. +Qed. +Global Opaque hbuiltin_arg. +Local Hint Resolve hbuiltin_arg_correct: wlp. + +Fixpoint hbuiltin_args (hst: PTree.t hsval) (args: list (builtin_arg reg)): ?? list (builtin_arg hsval) := + match args with + | nil => RET nil + | a::l => + DO ha <~ hbuiltin_arg hst a;; + DO hl <~ hbuiltin_args hst l;; + RET (ha::hl) + end. + +Lemma hbuiltin_args_correct hst args: + WHEN hbuiltin_args hst args ~> hargs THEN forall ge sp rs0 m0 (f: reg -> sval) + (RR: forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0), + bargs_refines ge sp rs0 m0 hargs (List.map (builtin_arg_map f) args). +Proof. + unfold bargs_refines, seval_builtin_args; induction args; wlp_simplify. + erewrite H; eauto. + erewrite H0; eauto. +Qed. +Global Opaque hbuiltin_args. +Local Hint Resolve hbuiltin_args_correct: wlp. + +Definition hsum_left (hst: PTree.t hsval) (ros: reg + ident): ?? (hsval + ident) := + match ros with + | inl r => DO hr <~ hsi_sreg_get hst r;; RET (inl hr) + | inr s => RET (inr s) + end. + +Lemma hsum_left_correct hst ros: + WHEN hsum_left hst ros ~> hsi THEN forall ge sp rs0 m0 (f: reg -> sval) + (RR: forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0), + sum_refines ge sp rs0 m0 hsi (sum_left_map f ros). +Proof. + unfold sum_refines; destruct ros; wlp_simplify. +Qed. +Global Opaque hsum_left. +Local Hint Resolve hsum_left_correct: wlp. + +Definition hsexec_final (i: instruction) (hst: PTree.t hsval): ?? hsfval := + match i with + | Icall sig ros args res pc => + DO svos <~ hsum_left hst ros;; + DO sargs <~ hlist_args hst args;; + RET (HScall sig svos sargs res pc) + | Itailcall sig ros args => + DO svos <~ hsum_left hst ros;; + DO sargs <~ hlist_args hst args;; + RET (HStailcall sig svos sargs) + | Ibuiltin ef args res pc => + DO sargs <~ hbuiltin_args hst args;; + RET (HSbuiltin ef sargs res pc) + | Ijumptable reg tbl => + DO sv <~ hsi_sreg_get hst reg;; + RET (HSjumptable sv tbl) + | Ireturn or => + match or with + | Some r => DO hr <~ hsi_sreg_get hst r;; RET (HSreturn (Some hr)) + | None => RET (HSreturn None) + end + | _ => RET (HSnone) + end. + +Lemma hsexec_final_correct (hsl: hsistate_local) i: + WHEN hsexec_final i hsl ~> hsf THEN forall ge sp rs0 m0 sl + (OK: hsok_local ge sp rs0 m0 hsl) + (REF: hsilocal_refines ge sp rs0 m0 hsl sl), + hfinal_refines ge sp rs0 m0 hsf (sexec_final i sl). +Proof. + destruct i; wlp_simplify; try econstructor; simpl; eauto. +Qed. +Global Opaque hsexec_final. +Local Hint Resolve hsexec_final_correct: wlp. + +Definition init_hsistate_local (_:unit): ?? hsistate_local + := DO hm <~ hSinit ();; + RET {| hsi_smem := hm; hsi_ok_lsval := nil; hsi_sreg := PTree.empty hsval |}. + +Lemma init_hsistate_local_correct: + WHEN init_hsistate_local () ~> hsl THEN forall ge sp rs0 m0, + hsilocal_refines ge sp rs0 m0 hsl init_sistate_local. +Proof. + unfold hsilocal_refines; wlp_simplify. + - unfold hsok_local; simpl; intuition. erewrite H in *; congruence. + - unfold hsok_local, sok_local; simpl in *; intuition; try congruence. + - unfold hsi_sreg_eval, hsi_sreg_proj. rewrite PTree.gempty. reflexivity. + - try_simplify_someHyps. +Qed. +Global Opaque init_hsistate_local. +Local Hint Resolve init_hsistate_local_correct: wlp. + +Definition init_hsistate pc: ?? hsistate + := DO hst <~ init_hsistate_local ();; + RET {| hsi_pc := pc; hsi_exits := nil; hsi_local := hst |}. + +Lemma init_hsistate_correct pc: + WHEN init_hsistate pc ~> hst THEN + hsistate_refines_stat hst (init_sistate pc) + /\ forall ge sp rs0 m0, hsistate_refines_dyn ge sp rs0 m0 hst (init_sistate pc). +Proof. + unfold hsistate_refines_stat, hsistate_refines_dyn, hsiexits_refines_dyn; wlp_simplify; constructor. +Qed. +Global Opaque init_hsistate. +Local Hint Resolve init_hsistate_correct: wlp. + +Definition hsexec (f: function) (pc:node): ?? hsstate := + DO path <~ some_or_fail ((fn_path f)!pc) "hsexec.internal_error.1";; + DO hinit <~ init_hsistate pc;; + DO hst <~ hsiexec_path path.(psize) f hinit;; + 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. + +Lemma hsexec_correct_aux f pc: + WHEN hsexec f pc ~> hst THEN + exists st, sexec f pc = Some st /\ hsstate_refines hst st. +Proof. + unfold hsstate_refines, sexec; wlp_simplify. + - (* Some *) + rewrite H; clear H. + exploit H0; clear H0; eauto. + intros (st0 & EXECPATH & SREF & DREF). + rewrite EXECPATH; clear EXECPATH. + generalize SREF. intros (EQPC & _). + rewrite <- EQPC, H3; clear H3. + exploit H4; clear H4; eauto. + intros (st' & EXECL & SREF' & DREF'). + try_simplify_someHyps. + eexists; intuition (simpl; eauto). + constructor. + - (* None *) + rewrite H; clear H H4. + exploit H0; clear H0; eauto. + intros (st0 & EXECPATH & SREF & DREF). + rewrite EXECPATH; clear EXECPATH. + generalize SREF. intros (EQPC & _). + rewrite <- EQPC, H3; clear H3. + erewrite hsiexec_inst_None_correct; eauto. + eexists; intuition (simpl; eauto). +Qed. + +Global Opaque hsexec. + +End CanonBuilding. + +(** Correction of concrete symbolic execution wrt abstract symbolic execution *) +Theorem hsexec_correct + (hC_hsval : hashinfo hsval -> ?? hsval) + (hC_list_hsval : hashinfo list_hsval -> ?? list_hsval) + (hC_hsmem : hashinfo hsmem -> ?? hsmem) + (f : function) + (pc : node): + WHEN hsexec hC_hsval hC_list_hsval hC_hsmem f pc ~> hst THEN forall + (hC_hsval_correct: forall hs, + WHEN hC_hsval hs ~> hs' THEN forall ge sp rs0 m0, + seval_sval ge sp (hsval_proj (hdata hs)) rs0 m0 = + seval_sval ge sp (hsval_proj hs') rs0 m0) + (hC_list_hsval_correct: forall lh, + WHEN hC_list_hsval lh ~> lh' THEN forall ge sp rs0 m0, + seval_list_sval ge sp (hsval_list_proj (hdata lh)) rs0 m0 = + seval_list_sval ge sp (hsval_list_proj lh') rs0 m0) + (hC_hsmem_correct: forall hm, + WHEN hC_hsmem hm ~> hm' THEN forall ge sp rs0 m0, + seval_smem ge sp (hsmem_proj (hdata hm)) rs0 m0 = + seval_smem ge sp (hsmem_proj hm') rs0 m0), + exists st : sstate, sexec f pc = Some st /\ hsstate_refines hst st. +Proof. + wlp_simplify. + eapply hsexec_correct_aux; eauto. +Qed. +Local Hint Resolve hsexec_correct: wlp. + +(** * Implementing the simulation test with concrete hash-consed symbolic execution *) + +Definition phys_check {A} (x y:A) (msg: pstring): ?? unit := + DO b <~ phys_eq x y;; + assert_b b msg;; + RET tt. + +Definition struct_check {A} (x y: A) (msg: pstring): ?? unit := + DO b <~ struct_eq x y;; + assert_b b msg;; + RET tt. + +Lemma struct_check_correct {A} (a b: A) msg: + WHEN struct_check a b msg ~> _ THEN + a = b. +Proof. wlp_simplify. Qed. +Global Opaque struct_check. +Hint Resolve struct_check_correct: wlp. + +Definition option_eq_check {A} (o1 o2: option A): ?? unit := + match o1, o2 with + | Some x1, Some x2 => phys_check x1 x2 "option_eq_check: data physically differ" + | None, None => RET tt + | _, _ => FAILWITH "option_eq_check: structure differs" + end. + +Lemma option_eq_check_correct A (o1 o2: option A): WHEN option_eq_check o1 o2 ~> _ THEN o1=o2. +Proof. + wlp_simplify. +Qed. +Global Opaque option_eq_check. +Hint Resolve option_eq_check_correct:wlp. + +Import PTree. + +Fixpoint PTree_eq_check {A} (d1 d2: PTree.t A): ?? unit := + match d1, d2 with + | Leaf, Leaf => RET tt + | Node l1 o1 r1, Node l2 o2 r2 => + option_eq_check o1 o2;; + PTree_eq_check l1 l2;; + PTree_eq_check r1 r2 + | _, _ => FAILWITH "PTree_eq_check: some key is absent" + end. + +Lemma PTree_eq_check_correct A d1: forall (d2: t A), + WHEN PTree_eq_check d1 d2 ~> _ THEN forall x, PTree.get x d1 = PTree.get x d2. +Proof. + induction d1 as [|l1 Hl1 o1 r1 Hr1]; destruct d2 as [|l2 o2 r2]; simpl; + wlp_simplify. destruct x; simpl; auto. +Qed. +Global Opaque PTree_eq_check. +Local Hint Resolve PTree_eq_check_correct: wlp. + +Fixpoint PTree_frame_eq_check {A} (frame: list positive) (d1 d2: PTree.t A): ?? unit := + match frame with + | nil => RET tt + | k::l => + option_eq_check (PTree.get k d1) (PTree.get k d2);; + PTree_frame_eq_check l d1 d2 + end. + +Lemma PTree_frame_eq_check_correct A l (d1 d2: t A): + WHEN PTree_frame_eq_check l d1 d2 ~> _ THEN forall x, List.In x l -> PTree.get x d1 = PTree.get x d2. +Proof. + induction l as [|k l]; simpl; wlp_simplify. + subst; auto. +Qed. +Global Opaque PTree_frame_eq_check. +Local Hint Resolve PTree_frame_eq_check_correct: wlp. + +Definition hsilocal_frame_simu_check frame hst1 hst2 : ?? unit := + DEBUG("? frame check");; + phys_check (hsi_smem hst2) (hsi_smem hst1) "hsilocal_frame_simu_check: hsi_smem sets aren't equiv";; + PTree_frame_eq_check frame (hsi_sreg hst1) (hsi_sreg hst2);; + Sets.assert_list_incl mk_hash_params (hsi_ok_lsval hst2) (hsi_ok_lsval hst1);; + DEBUG("=> frame check: OK"). + +Lemma setoid_in {A: Type} (a: A): forall l, + SetoidList.InA (fun x y => x = y) a l -> + In a l. +Proof. + induction l; intros; inv H. + - constructor. reflexivity. + - right. auto. +Qed. + +Lemma regset_elements_in r rs: + Regset.In r rs -> + In r (Regset.elements rs). +Proof. + intros. exploit Regset.elements_1; eauto. intro SIN. + apply setoid_in. assumption. +Qed. +Local Hint Resolve regset_elements_in: core. + +Lemma hsilocal_frame_simu_check_correct hst1 hst2 alive: + WHEN hsilocal_frame_simu_check (Regset.elements alive) hst1 hst2 ~> _ THEN + hsilocal_simu_spec alive hst1 hst2. +Proof. + unfold hsilocal_simu_spec; wlp_simplify. symmetry; eauto. +Qed. +Hint Resolve hsilocal_frame_simu_check_correct: wlp. +Global Opaque hsilocal_frame_simu_check. + +Definition revmap_check_single (dm: PTree.t node) (n tn: node) : ?? unit := + DO res <~ some_or_fail (dm ! tn) "revmap_check_single: no mapping for tn";; + struct_check n res "revmap_check_single: n and res are physically different". + +Lemma revmap_check_single_correct dm pc1 pc2: + WHEN revmap_check_single dm pc1 pc2 ~> _ THEN + dm ! pc2 = Some pc1. +Proof. + wlp_simplify. congruence. +Qed. +Hint Resolve revmap_check_single_correct: wlp. +Global Opaque revmap_check_single. + +Definition hsiexit_simu_check (dm: PTree.t node) (f: RTLpath.function) (hse1 hse2: hsistate_exit): ?? unit := + struct_check (hsi_cond hse1) (hsi_cond hse2) "hsiexit_simu_check: conditions do not match";; + phys_check (hsi_scondargs hse1) (hsi_scondargs hse2) "hsiexit_simu_check: args do not match";; + revmap_check_single dm (hsi_ifso hse1) (hsi_ifso hse2);; + DO path <~ some_or_fail ((fn_path f) ! (hsi_ifso hse1)) "hsiexit_simu_check: internal error";; + hsilocal_frame_simu_check (Regset.elements path.(input_regs)) (hsi_elocal hse1) (hsi_elocal hse2). + +Lemma hsiexit_simu_check_correct dm f hse1 hse2: + WHEN hsiexit_simu_check dm f hse1 hse2 ~> _ THEN + hsiexit_simu_spec dm f hse1 hse2. +Proof. + unfold hsiexit_simu_spec; wlp_simplify. +Qed. +Hint Resolve hsiexit_simu_check_correct: wlp. +Global Opaque hsiexit_simu_check. + +Fixpoint hsiexits_simu_check (dm: PTree.t node) (f: RTLpath.function) (lhse1 lhse2: list hsistate_exit) := + match lhse1,lhse2 with + | nil, nil => RET tt + | hse1 :: lhse1, hse2 :: lhse2 => + hsiexit_simu_check dm f hse1 hse2;; + hsiexits_simu_check dm f lhse1 lhse2 + | _, _ => FAILWITH "siexists_simu_check: lengths do not match" + end. + +Lemma hsiexits_simu_check_correct dm f: forall le1 le2, + WHEN hsiexits_simu_check dm f le1 le2 ~> _ THEN + hsiexits_simu_spec dm f le1 le2. +Proof. + unfold hsiexits_simu_spec; induction le1; simpl; destruct le2; wlp_simplify; constructor; eauto. +Qed. +Hint Resolve hsiexits_simu_check_correct: wlp. +Global Opaque hsiexits_simu_check. + +Definition hsistate_simu_check (dm: PTree.t node) (f: RTLpath.function) outframe (hst1 hst2: hsistate) := + hsiexits_simu_check dm f (hsi_exits hst1) (hsi_exits hst2);; + hsilocal_frame_simu_check (Regset.elements outframe) (hsi_local hst1) (hsi_local hst2). + +Lemma hsistate_simu_check_correct dm f outframe hst1 hst2: + WHEN hsistate_simu_check dm f outframe hst1 hst2 ~> _ THEN + hsistate_simu_spec dm f outframe hst1 hst2. +Proof. + unfold hsistate_simu_spec; wlp_simplify. +Qed. +Hint Resolve hsistate_simu_check_correct: wlp. +Global Opaque hsistate_simu_check. + + +Fixpoint revmap_check_list (dm: PTree.t node) (ln ln': list node): ?? unit := + match ln, ln' with + | nil, nil => RET tt + | n::ln, n'::ln' => + revmap_check_single dm n n';; + revmap_check_list dm ln ln' + | _, _ => FAILWITH "revmap_check_list: lists have different lengths" + end. + +Lemma revmap_check_list_correct dm: forall lpc lpc', + WHEN revmap_check_list dm lpc lpc' ~> _ THEN + ptree_get_list dm lpc' = Some lpc. +Proof. + induction lpc. + - destruct lpc'; wlp_simplify. + - destruct lpc'; wlp_simplify. try_simplify_someHyps. +Qed. +Global Opaque revmap_check_list. +Hint Resolve revmap_check_list_correct: wlp. + + +Definition svos_simu_check (svos1 svos2: hsval + ident) := + match svos1, svos2 with + | inl sv1, inl sv2 => phys_check sv1 sv2 "svos_simu_check: sval mismatch" + | inr id1, inr id2 => phys_check id1 id2 "svos_simu_check: symbol mismatch" + | _, _ => FAILWITH "svos_simu_check: type mismatch" + end. + +Lemma svos_simu_check_correct svos1 svos2: + WHEN svos_simu_check svos1 svos2 ~> _ THEN + svos1 = svos2. +Proof. + destruct svos1; destruct svos2; wlp_simplify. +Qed. +Global Opaque svos_simu_check. +Hint Resolve svos_simu_check_correct: wlp. + + +Fixpoint builtin_arg_simu_check (bs bs': builtin_arg hsval) := + match bs with + | BA sv => + match bs' with + | BA sv' => phys_check sv sv' "builtin_arg_simu_check: sval mismatch" + | _ => FAILWITH "builtin_arg_simu_check: BA mismatch" + end + | BA_splitlong lo hi => + match bs' with + | BA_splitlong lo' hi' => + builtin_arg_simu_check lo lo';; + builtin_arg_simu_check hi hi' + | _ => FAILWITH "builtin_arg_simu_check: BA_splitlong mismatch" + end + | BA_addptr b1 b2 => + match bs' with + | BA_addptr b1' b2' => + builtin_arg_simu_check b1 b1';; + builtin_arg_simu_check b2 b2' + | _ => FAILWITH "builtin_arg_simu_check: BA_addptr mismatch" + end + | bs => struct_check bs bs' "builtin_arg_simu_check: basic mismatch" + end. + +Lemma builtin_arg_simu_check_correct: forall bs1 bs2, + WHEN builtin_arg_simu_check bs1 bs2 ~> _ THEN + builtin_arg_map hsval_proj bs1 = builtin_arg_map hsval_proj bs2. +Proof. + induction bs1. + all: try (wlp_simplify; subst; reflexivity). + all: destruct bs2; wlp_simplify; congruence. +Qed. +Global Opaque builtin_arg_simu_check. +Hint Resolve builtin_arg_simu_check_correct: wlp. + +Fixpoint list_builtin_arg_simu_check lbs1 lbs2 := + match lbs1, lbs2 with + | nil, nil => RET tt + | bs1::lbs1, bs2::lbs2 => + builtin_arg_simu_check bs1 bs2;; + list_builtin_arg_simu_check lbs1 lbs2 + | _, _ => FAILWITH "list_builtin_arg_simu_check: length mismatch" + end. + +Lemma list_builtin_arg_simu_check_correct: forall lbs1 lbs2, + WHEN list_builtin_arg_simu_check lbs1 lbs2 ~> _ THEN + List.map (builtin_arg_map hsval_proj) lbs1 = List.map (builtin_arg_map hsval_proj) lbs2. +Proof. + induction lbs1; destruct lbs2; wlp_simplify. congruence. +Qed. +Global Opaque list_builtin_arg_simu_check. +Hint Resolve list_builtin_arg_simu_check_correct: wlp. + +Definition sfval_simu_check (dm: PTree.t node) (f: RTLpath.function) (pc1 pc2: node) (fv1 fv2: hsfval) := + match fv1, fv2 with + | HSnone, HSnone => revmap_check_single dm pc1 pc2 + | HScall sig1 svos1 lsv1 res1 pc1, HScall sig2 svos2 lsv2 res2 pc2 => + revmap_check_single dm pc1 pc2;; + phys_check sig1 sig2 "sfval_simu_check: Scall different signatures";; + phys_check res1 res2 "sfval_simu_check: Scall res do not match";; + svos_simu_check svos1 svos2;; + phys_check lsv1 lsv2 "sfval_simu_check: Scall args do not match" + | HStailcall sig1 svos1 lsv1, HStailcall sig2 svos2 lsv2 => + phys_check sig1 sig2 "sfval_simu_check: Stailcall different signatures";; + svos_simu_check svos1 svos2;; + phys_check lsv1 lsv2 "sfval_simu_check: Stailcall args do not match" + | HSbuiltin ef1 lbs1 br1 pc1, HSbuiltin ef2 lbs2 br2 pc2 => + revmap_check_single dm pc1 pc2;; + phys_check ef1 ef2 "sfval_simu_check: builtin ef do not match";; + phys_check br1 br2 "sfval_simu_check: builtin br do not match";; + list_builtin_arg_simu_check lbs1 lbs2 + | HSjumptable sv ln, HSjumptable sv' ln' => + revmap_check_list dm ln ln';; + phys_check sv sv' "sfval_simu_check: Sjumptable sval do not match" + | HSreturn osv1, HSreturn osv2 => + option_eq_check osv1 osv2 + | _, _ => FAILWITH "sfval_simu_check: structure mismatch" + end. + +Lemma sfval_simu_check_correct dm f opc1 opc2 fv1 fv2: + WHEN sfval_simu_check dm f opc1 opc2 fv1 fv2 ~> _ THEN + hfinal_simu_spec dm f opc1 opc2 fv1 fv2. +Proof. + unfold hfinal_simu_spec; destruct fv1; destruct fv2; wlp_simplify; try congruence. +Qed. +Hint Resolve sfval_simu_check_correct: wlp. +Global Opaque sfval_simu_check. + +Definition hsstate_simu_check (dm: PTree.t node) (f: RTLpath.function) outframe (hst1 hst2: hsstate) := + hsistate_simu_check dm f outframe (hinternal hst1) (hinternal hst2);; + sfval_simu_check dm f (hsi_pc hst1) (hsi_pc hst2) (hfinal hst1) (hfinal hst2). + +Lemma hsstate_simu_check_correct dm f outframe hst1 hst2: + WHEN hsstate_simu_check dm f outframe hst1 hst2 ~> _ THEN + hsstate_simu_spec dm f outframe hst1 hst2. +Proof. + unfold hsstate_simu_spec; wlp_simplify. +Qed. +Hint Resolve hsstate_simu_check_correct: wlp. +Global Opaque hsstate_simu_check. + +Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) (m: node * node): ?? unit := + let (pc2, pc1) := m in + (* creating the hash-consing tables *) + DO hC_sval <~ hCons hSVAL;; + DO hC_list_hsval <~ hCons hLSVAL;; + DO hC_hsmem <~ hCons hSMEM;; + let hsexec := hsexec hC_sval.(hC) hC_list_hsval.(hC) hC_hsmem.(hC) in + (* performing the hash-consed executions *) + XDEBUG pc1 (fun pc => DO name_pc <~ string_of_Z (Zpos pc);; RET ("entry-point of input superblock: " +; name_pc)%string);; + DO hst1 <~ hsexec f pc1;; + XDEBUG pc2 (fun pc => DO name_pc <~ string_of_Z (Zpos pc);; RET ("entry-point of output superblock: " +; name_pc)%string);; + DO hst2 <~ hsexec tf pc2;; + DO path <~ some_or_fail ((fn_path f)!pc1) "simu_check_single.internal_error.1";; + let outframe := path.(pre_output_regs) in + (* comparing the executions *) + hsstate_simu_check dm f outframe hst1 hst2. + +Lemma simu_check_single_correct dm tf f pc1 pc2: + WHEN simu_check_single dm f tf (pc2, pc1) ~> _ THEN + sexec_simu dm f tf pc1 pc2. +Proof. + unfold sexec_simu; wlp_simplify. + exploit H2; clear H2. 1-3: wlp_simplify. + intros (st2 & SEXEC2 & REF2). try_simplify_someHyps. + exploit H3; clear H3. 1-3: wlp_simplify. + intros (st3 & SEXEC3 & REF3). try_simplify_someHyps. + eexists. eexists. split; eauto. split; eauto. + intros ctx. + eapply hsstate_simu_spec_correct; eauto. +Qed. +Global Opaque simu_check_single. +Global Hint Resolve simu_check_single_correct: wlp. + +Fixpoint simu_check_rec (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) lm : ?? unit := + match lm with + | nil => RET tt + | m :: lm => + simu_check_single dm f tf m;; + simu_check_rec dm f tf lm + end. + +Lemma simu_check_rec_correct dm f tf lm: + WHEN simu_check_rec dm f tf lm ~> _ THEN + forall pc1 pc2, In (pc2, pc1) lm -> sexec_simu dm f tf pc1 pc2. +Proof. + induction lm; wlp_simplify. + match goal with + | X: (_,_) = (_,_) |- _ => inversion X; subst + end. + subst; eauto. +Qed. +Global Opaque simu_check_rec. +Global Hint Resolve simu_check_rec_correct: wlp. + +Definition imp_simu_check (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function): ?? unit := + simu_check_rec dm f tf (PTree.elements dm);; + DEBUG("simu_check OK!"). + +Local Hint Resolve PTree.elements_correct: core. +Lemma imp_simu_check_correct dm f tf: + WHEN imp_simu_check dm f tf ~> _ THEN + forall pc1 pc2, dm ! pc2 = Some pc1 -> sexec_simu dm f tf pc1 pc2. +Proof. + wlp_simplify. +Qed. +Global Opaque imp_simu_check. +Global Hint Resolve imp_simu_check_correct: wlp. + +Program Definition aux_simu_check (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function): ?? bool := + DO r <~ + (TRY + imp_simu_check dm f tf;; + RET true + CATCH_FAIL s, _ => + println ("simu_check_failure:" +; s);; + RET false + ENSURE (fun b => b=true -> forall pc1 pc2, dm ! pc2 = Some pc1 -> sexec_simu dm f tf pc1 pc2));; + RET (`r). +Obligation 1. + split; wlp_simplify. discriminate. +Qed. + +Lemma aux_simu_check_correct dm f tf: + WHEN aux_simu_check dm f tf ~> b THEN + b=true -> forall pc1 pc2, dm ! pc2 = Some pc1 -> sexec_simu dm f tf pc1 pc2. +Proof. + unfold aux_simu_check; wlp_simplify. + destruct exta; simpl; auto. +Qed. + +(* Coerce aux_simu_check into a pure function (this is a little unsafe like all oracles in CompCert). *) + +Import UnsafeImpure. + +Definition simu_check (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) : res unit := + match unsafe_coerce (aux_simu_check dm f tf) with + | Some true => OK tt + | _ => Error (msg "simu_check has failed") + end. + +Lemma simu_check_correct dm f tf: + simu_check dm f tf = OK tt -> + forall pc1 pc2, dm ! pc2 = Some pc1 -> + sexec_simu dm f tf pc1 pc2. +Proof. + unfold simu_check. + destruct (unsafe_coerce (aux_simu_check dm f tf)) as [[|]|] eqn:Hres; simpl; try discriminate. + intros; eapply aux_simu_check_correct; eauto. + eapply unsafe_coerce_not_really_correct; eauto. +Qed. |