diff options
Diffstat (limited to 'scheduling/RTLpathSE_impl.v')
| -rw-r--r-- | scheduling/RTLpathSE_impl.v | 1650 |
1 files changed, 0 insertions, 1650 deletions
diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v deleted file mode 100644 index cda1c079..00000000 --- a/scheduling/RTLpathSE_impl.v +++ /dev/null @@ -1,1650 +0,0 @@ -(** 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 *) - -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. |