(** 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 Duplicate. Require Import RTLpathSE_theory RTLpathLivegenproof. Require Import Axioms. Local Open Scope error_monad_scope. Local Open Scope option_monad_scope. Require Export Impure.ImpHCons. Export Notations. Import HConsing. Local Open Scope impure. Import ListNotations. Local Open Scope list_scope. Ltac wlp_intro vname hname := apply wlp_unfold; intros vname hname. Ltac wlp_bind vname hname := apply wlp_bind; intros vname hname. Ltac wlp_ret vname := let H := fresh "H" vname in wlp_intro vname H; apply mayRet_ret in H; subst. Tactic Notation "wlp_intro" ident(v) ident(h) := wlp_intro v h. Tactic Notation "wlp_intro" ident(v) := let H := fresh "H" v in wlp_intro v H. Tactic Notation "wlp_bind" ident(v) ident(h) := wlp_bind v h. Tactic Notation "wlp_bind" ident(v) := let H := fresh "H" v in wlp_bind v H. Ltac wlp_absurd := match goal with | [ H : FAILWITH ?msg |- _ ] => eapply (_FAILWITH_correct _ _ (fun _ => False)) in H; inv H | [ H : DO r <~ fail ?msg;; RET ?expr ~~> ?exta |- _ ] => eapply (_FAILWITH_correct _ _ (fun _ => False)) in H; inv H end. Ltac wlp_hbind var := match goal with | [ H : DO _ <~ ?expr;; _ ~~> _ |- _ ] => let Hvar := fresh "H" var in (apply mayRet_bind in H; destruct H as (var & Hvar & H)) end. Ltac wlp_hret := match goal with | [ H : RET _ ~~> _ |- _ ] => apply mayRet_ret in H; subst; clear H end. (** * Implementation of Data-structure use in Hash-consing *) (** ** Implementation of symbolic values/symbolic memories with hash-consing data *) Inductive hsval := | HSinput (r: reg) (hid: hashcode) | HSop (op: operation) (lhsv: list_hsval) (hsm: hsmem) (hid: hashcode) | HSload (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval) (hid: hashcode) with list_hsval := | HSnil (hid: hashcode) | HScons (hsv: hsval) (lhsv: list_hsval) (hid: hashcode) with hsmem := | HSinit (hid: hashcode) | HSstore (hsm: hsmem) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval) (srce: hsval) (hid:hashcode). Scheme hsval_mut := Induction for hsval Sort Prop with list_hsval_mut := Induction for list_hsval Sort Prop with hsmem_mut := Induction for hsmem Sort Prop. 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 hsm _ => HSop o lhsv hsm 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. (** 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 sm1 _, HSop op2 lsv2 sm2 _ => DO b1 <~ phys_eq lsv1 lsv2;; DO b2 <~ phys_eq sm1 sm2;; if b1 && b2 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. 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. 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. 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 _ => RET () (* NB no log *) |}. Obligation 1. wlp_simplify. Qed. (** Symbolic final value -- from hash-consed values It does not seem useful to hash-consed these final values (because they are final). *) Inductive hsfval := | HSnone | HScall (sig: signature) (svos: hsval + ident) (lsv: list_hsval) (res: reg) (pc: node) | HStailcall (sig: signature) (svos: hsval + ident) (lsv: list_hsval) | HSbuiltin (ef: external_function) (sargs: list (builtin_arg hsval)) (res: builtin_res reg) (pc: node) | HSjumptable (sv: hsval) (tbl: list node) | HSreturn (res: option hsval) . (** ** Implementation of symbolic states *) (** name : Hash-consed Symbolic Internal state local. *) Record hsistate_local := { (** [hsi_smem] represents the current smem symbolic evaluations. (we can recover the previous one from smem) *) hsi_smem:> hsmem; (** For the values in registers: 1) we store a list of sval evaluations 2) we encode the symbolic regset by a PTree *) hsi_ok_lsval: list hsval; hsi_sreg:> PTree.t hsval }. (* Syntax and semantics of symbolic exit states *) Record hsistate_exit := mk_hsistate_exit { hsi_cond: condition; hsi_scondargs: list_hsval; hsi_elocal: hsistate_local; hsi_ifso: node }. (** ** Syntax and Semantics of symbolic internal state *) Record hsistate := { hsi_pc: node; hsi_exits: list hsistate_exit; hsi_local: hsistate_local }. (** ** Syntax and Semantics of symbolic state *) Record hsstate := { hinternal:> hsistate; hfinal: hsfval }. Fixpoint hsval_proj hsv := match hsv with | HSinput r _ => Sinput r | HSop op hl hm _ => Sop op (hsval_list_proj hl) (hsmem_proj hm) | HSload hm t chk addr hl _ => Sload (hsmem_proj hm) t chk addr (hsval_list_proj hl) end with hsval_list_proj hl := match hl with | HSnil _ => Snil | HScons hv hl _ => Scons (hsval_proj hv) (hsval_list_proj hl) end with hsmem_proj hm := match hm with | HSinit _ => Sinit | HSstore hm chk addr hl hv _ => Sstore (hsmem_proj hm) chk addr (hsval_list_proj hl) (hsval_proj hv) end. (** * Implementation of symbolic execution *) Section CanonBuilding. Variable hC_hsval: hashinfo hsval -> ?? hsval. (** FIXME - maybe it's not what we want ? *) Hypothesis hC_hsval_correct: forall hs rhsv, hC_hsval hs ~~> rhsv -> (hsval_proj (hdata hs)) = (hsval_proj rhsv). Local Hint Resolve hC_hsval_correct: wlp. Variable hC_list_hsval: hashinfo list_hsval -> ?? list_hsval. Hypothesis hC_list_hsval_correct: forall hs rhsv, hC_list_hsval hs ~~> rhsv -> (hsval_list_proj (hdata hs)) = (hsval_list_proj rhsv). Local Hint Resolve hC_list_hsval_correct: wlp. Variable hC_hsmem: hashinfo hsmem -> ?? hsmem. Hypothesis hC_hsmem_correct: forall hs rhsv, hC_hsmem hs ~~> rhsv -> (hsmem_proj (hdata hs)) = (hsmem_proj rhsv). Local Hint Resolve hC_hsmem_correct: wlp. (* 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; |}. Definition hSop_hcodes (op:operation) (lhsv: list_hsval) (hsm: hsmem) := DO hc <~ hash op_hcode;; DO hv <~ hash op;; RET [hc;hv;list_hsval_get_hid lhsv; hsmem_get_hid hsm]. Extraction Inline hSop_hcodes. Definition hSop (op:operation) (lhsv: list_hsval) (hsm: hsmem): ?? hsval := DO hv <~ hSop_hcodes op lhsv hsm;; hC_hsval {| hdata:=HSop op lhsv hsm unknown_hid; hcodes :=hv |}. Definition 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 |}. Definition hSnil (_: unit): ?? list_hsval := hC_list_hsval {| hdata := HSnil unknown_hid; hcodes := nil |}. 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] |}. Definition hSinit (_: unit): ?? hsmem := hC_hsmem {| hdata := HSinit unknown_hid; hcodes := nil |}. 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 |}. Definition hsi_sreg_get (hst: PTree.t hsval) r: ?? hsval := match PTree.get r hst with | None => hSinput r | Some sv => RET sv end. 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. (** ** Assignment of memory *) 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 {| hsi_smem := hm; hsi_ok_lsval := hsi_ok_lsval hst; hsi_sreg:= hsi_sreg hst |}. (** ** 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 |}. (** ** 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) (hst: hsistate_local) : ?? hsval := DO lhsv <~ hlist_args hst lr;; match rsv with | Rop op => hSop op lhsv hst | Rload trap chunk addr => hSload hst trap chunk addr lhsv end. 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. (** 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 => DO hsi <~ hSinit ();; DO lhsv <~ hlist_args hst lr;; hSop op lhsv hsi (** magically remove the dependency on sm ! *) end | Rload _ chunk addr => DO lhsv <~ hlist_args hst lr;; hSload hst NOTRAP chunk addr lhsv end. 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. 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_apply rsv lr hst;; 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) |}. (** ** Execution of one instruction *) 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 vargs <~ hlist_args prev args ;; 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 (* TODO jumptable ? *) end. 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 => DO i <~ some_or_fail ((fn_code f)!(hst.(hsi_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. 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. 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. 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. (** * The simulation test of 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. Lemma phys_check_correct {A} (a b: A) msg: WHEN phys_check a b msg ~> tt THEN a = b. Proof. wlp_simplify. Qed. Global Opaque phys_check. Hint Resolve phys_check_correct: wlp. 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 ~> tt 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. congruence. 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. 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. (** hsilocal_simu_check and properties *) Definition seval_hsval ge sp hsv rs0 m0 := seval_sval ge sp (hsval_proj hsv) rs0 m0. Definition seval_hsmem ge sp hsm rs0 m0 := seval_smem ge sp (hsmem_proj hsm) rs0 m0. Definition hsi_sreg_eval ge sp (hst: PTree.t hsval) r rs0 m0: option val := match PTree.get r hst with | None => Some (Regmap.get r rs0) | Some hsv => seval_hsval ge sp hsv rs0 m0 end. Lemma hsi_sreg_eval_correct ge sp hst r rs0 m0: WHEN hsi_sreg_get hst r ~> hv THEN hsi_sreg_eval ge sp hst r rs0 m0 = seval_hsval ge sp hv rs0 m0. Proof. wlp_simplify. - unfold hsi_sreg_eval. rewrite H. reflexivity. - unfold hsi_sreg_eval. rewrite H. eapply hC_hsval_correct in Hexta1. simpl in Hexta1. unfold seval_hsval. rewrite <- Hexta1. simpl. reflexivity. Qed. Hint Resolve hsi_sreg_eval_correct: wlp. Definition hsok_local ge sp rs0 m0 (hst: hsistate_local) : Prop := (forall hsv, List.In hsv (hsi_ok_lsval hst) -> seval_hsval ge sp hsv rs0 m0 <> None). (* refinement link between a (st: sistate_local) and (hst: hsistate_local) *) Definition hsilocal_refines ge sp rs0 m0 (hst: hsistate_local) (st: sistate_local) := (sok_local ge sp rs0 m0 st <-> hsok_local ge sp rs0 m0 hst) /\ (hsok_local ge sp rs0 m0 hst -> seval_hsmem ge sp (hsi_smem hst) rs0 m0 = seval_smem ge sp st.(si_smem) rs0 m0) /\ (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) /\ (forall r sv, hst ! r = Some sv -> In sv (hsi_ok_lsval hst)). Lemma ssem_local_sok ge sp rs0 m0 st rs m: ssem_local ge sp st rs0 m0 rs m -> sok_local ge sp rs0 m0 st. Proof. unfold sok_local, ssem_local. intuition congruence. Qed. Lemma ssem_local_refines_hok ge sp rs0 m0 hst st rs m: ssem_local ge sp st rs0 m0 rs m -> hsilocal_refines ge sp rs0 m0 hst st -> hsok_local ge sp rs0 m0 hst. Proof. intros H0 (H1 & _ & _). apply H1. eapply ssem_local_sok. eauto. Qed. Definition hsilocal_simu_core (oalive: option Regset.t) (hst1 hst2: hsistate_local) := incl (hsi_ok_lsval hst2) (hsi_ok_lsval hst1) /\ (forall r, (match oalive with Some alive => Regset.In r alive | _ => True end) -> (* hsi_sreg_get hst2 r = hsi_sreg_get hst1 r *) PTree.get r hst2 = PTree.get r hst1) /\ hsi_smem hst1 = hsi_smem hst2. Lemma hseval_preserved ge ge' rs0 m0 sp hsv: (forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s) -> seval_hsval ge sp hsv rs0 m0 = seval_hsval ge' sp hsv rs0 m0. Proof. intros. unfold seval_hsval. erewrite seval_preserved; eauto. Qed. Lemma hsmem_eval_preserved ge ge' rs0 m0 sp hsm: (forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s) -> seval_hsmem ge sp hsm rs0 m0 = seval_hsmem ge' sp hsm rs0 m0. Proof. intros. unfold seval_hsmem. erewrite smem_eval_preserved; eauto. Qed. Lemma hsilocal_simu_core_nofail ge1 ge2 of sp rs0 m0 hst1 hst2: hsilocal_simu_core of hst1 hst2 -> (forall s, Genv.find_symbol ge1 s = Genv.find_symbol ge2 s) -> hsok_local ge1 sp rs0 m0 hst1 -> hsok_local ge2 sp rs0 m0 hst2. Proof. intros (RSOK & _ & _) GFS OKV. intros sv INS. apply RSOK in INS. apply OKV in INS. erewrite hseval_preserved; eauto. Qed. Remark istate_simulive_reflexive dm is: istate_simulive (fun _ : Regset.elt => True) dm is is. Proof. unfold istate_simulive. repeat (constructor; auto). Qed. Definition seval_sval_partial ge sp rs0 m0 hsv := match seval_hsval ge sp hsv rs0 m0 with | Some v => v | None => Vundef end. Definition select_first (ox oy: option val) := match ox with | Some v => Some v | None => oy end. (** If the register was computed by hrs, evaluate the symbolic value from hrs. Else, take the value directly from rs0 *) Definition seval_partial_regset ge sp rs0 m0 hrs := let hrs_eval := PTree.map1 (seval_sval_partial ge sp rs0 m0) hrs in (fst rs0, PTree.combine select_first hrs_eval (snd rs0)). Lemma seval_partial_regset_get ge sp rs0 m0 hrs r: (seval_partial_regset ge sp rs0 m0 hrs) # r = match (hrs ! r) with Some sv => seval_sval_partial ge sp rs0 m0 sv | None => (rs0 # r) end. Proof. unfold seval_partial_regset. unfold Regmap.get. simpl. rewrite PTree.gcombine; [| simpl; reflexivity]. rewrite PTree.gmap1. destruct (hrs ! r); simpl; [reflexivity|]. destruct ((snd rs0) ! r); reflexivity. Qed. Theorem hsilocal_simu_core_correct hst1 hst2 of ge1 ge2 sp rs0 m0 rs m st1 st2: hsilocal_simu_core of hst1 hst2 -> hsilocal_refines ge1 sp rs0 m0 hst1 st1 -> hsilocal_refines ge2 sp rs0 m0 hst2 st2 -> (forall s, Genv.find_symbol ge1 s = Genv.find_symbol ge2 s) -> ssem_local ge1 sp st1 rs0 m0 rs m -> match of with | None => ssem_local ge2 sp st2 rs0 m0 rs m | Some alive => let rs' := seval_partial_regset ge2 sp rs0 m0 (hsi_sreg hst2) in ssem_local ge2 sp st2 rs0 m0 rs' m /\ eqlive_reg (fun r => Regset.In r alive) rs rs' end. Proof. intros CORE HREF1 HREF2 GFS SEML. refine (modusponens _ _ (ssem_local_refines_hok _ _ _ _ _ _ _ _ _ _) _); eauto. intro HOK1. refine (modusponens _ _ (hsilocal_simu_core_nofail _ _ _ _ _ _ _ _ _ _ _) _); eauto. intro HOK2. destruct SEML as (PRE & MEMEQ & RSEQ). assert (SIPRE: si_pre st2 ge2 sp rs0 m0). { destruct HREF2 as (OKEQ & _ & _). rewrite <- OKEQ in HOK2. apply HOK2. } assert (SMEMEVAL: seval_smem ge2 sp (si_smem st2) rs0 m0 = Some m). { destruct HREF2 as (_ & MEMEQ2 & _). destruct HREF1 as (_ & MEMEQ1 & _). destruct CORE as (_ & _ & MEMEQ3). rewrite <- MEMEQ2; auto. rewrite <- MEMEQ3. erewrite hsmem_eval_preserved; [| eapply GFS]. rewrite MEMEQ1; auto. } destruct of as [alive |]. - constructor. + constructor; [assumption | constructor; [assumption|]]. destruct HREF2 as (B & _ & A & PT). (** B, A and PT are used for the auto below *) assert (forall r : positive, hsi_sreg_eval ge2 sp hst2 r rs0 m0 = seval_sval ge2 sp (si_sreg st2 r) rs0 m0) by auto. intro r. rewrite <- H. clear H. rewrite seval_partial_regset_get. unfold hsi_sreg_eval. destruct (hst2 ! r) eqn:HST2; [| simpl; reflexivity]. unfold seval_sval_partial. assert (seval_hsval ge2 sp h rs0 m0 <> None) by eauto. destruct (seval_hsval ge2 sp h rs0 m0); [reflexivity | contradiction]. + intros r ALIVE. destruct HREF2 as (_ & _ & A & _). destruct HREF1 as (_ & _ & B & _). destruct CORE as (_ & C & _). rewrite seval_partial_regset_get. assert (OPT: forall (x y: val), Some x = Some y -> x = y) by congruence. destruct (hst2 ! r) eqn:HST2; apply OPT; clear OPT. ++ unfold seval_sval_partial. assert (seval_hsval ge2 sp h rs0 m0 = hsi_sreg_eval ge2 sp hst2 r rs0 m0). { unfold hsi_sreg_eval. rewrite HST2. reflexivity. } rewrite H. clear H. unfold hsi_sreg_eval. rewrite HST2. erewrite hseval_preserved; [| eapply GFS]. unfold hsi_sreg_eval in B. generalize (B HOK1 r); clear B; intro B. rewrite <- C in B; eauto. rewrite HST2 in B. rewrite B, RSEQ. reflexivity. ++ rewrite <- RSEQ. rewrite <- B; [|assumption]. unfold hsi_sreg_eval. rewrite <- C; [|assumption]. rewrite HST2. reflexivity. - constructor; [|constructor]. + destruct HREF2 as (OKEQ & _ & _). rewrite <- OKEQ in HOK2. apply HOK2. + destruct HREF2 as (_ & MEMEQ2 & _). destruct HREF1 as (_ & MEMEQ1 & _). destruct CORE as (_ & _ & MEMEQ3). rewrite <- MEMEQ2; auto. rewrite <- MEMEQ3. erewrite hsmem_eval_preserved; [| eapply GFS]. rewrite MEMEQ1; auto. + intro r. destruct HREF2 as (_ & _ & A & _). destruct HREF1 as (_ & _ & B & _). destruct CORE as (_ & C & _). rewrite <- A; auto. unfold hsi_sreg_eval. destruct (hst2 ! r) eqn:HST2. ++ assert (seval_hsval ge2 sp h rs0 m0 = hsi_sreg_eval ge2 sp hst2 r rs0 m0). { unfold hsi_sreg_eval. rewrite HST2. reflexivity. } rewrite H. clear H. unfold hsi_sreg_eval. rewrite HST2. erewrite hseval_preserved; [| eapply GFS]. unfold hsi_sreg_eval in B. generalize (B HOK1 r); clear B; intro B. rewrite <- C in B; eauto. rewrite HST2 in B. rewrite B, RSEQ. reflexivity. ++ rewrite <- RSEQ. rewrite <- B; [|assumption]. unfold hsi_sreg_eval. rewrite <- C; [|auto]. rewrite HST2. reflexivity. Qed. Definition hsilocal_simu_check hst1 hst2 : ?? unit := phys_check (hsi_smem hst2) (hsi_smem hst1) "hsilocal_simu_check: hsi_smem sets aren't equiv";; Sets.assert_list_incl mk_hash_params (hsi_ok_lsval hst2) (hsi_ok_lsval hst1);; PTree_eq_check (hsi_sreg hst1) (hsi_sreg hst2). Theorem hsilocal_simu_check_correct hst1 hst2: WHEN hsilocal_simu_check hst1 hst2 ~> tt THEN hsilocal_simu_core None hst1 hst2. Proof. wlp_simplify. constructor; [|constructor]; [assumption | | congruence]. intros. unfold hsi_sreg_get. rewrite (PTree_eq_check_correct _ hst1 hst2); [|eassumption]. reflexivity. Qed. Hint Resolve hsilocal_simu_check_correct: wlp. Global Opaque hsilocal_simu_check. Definition hsilocal_frame_simu_check frame hst1 hst2 : ?? unit := phys_check (hsi_smem hst2) (hsi_smem hst1) "hsilocal_frame_simu_check: hsi_smem sets aren't equiv";; Sets.assert_list_incl mk_hash_params (hsi_ok_lsval hst2) (hsi_ok_lsval hst1);; PTree_frame_eq_check frame (hsi_sreg hst1) (hsi_sreg hst2). 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 PTree_frame_eq_check_correct: wlp. Local Hint Resolve regset_elements_in: core. Theorem hsilocal_frame_simu_check_correct hst1 hst2 alive: WHEN hsilocal_frame_simu_check (Regset.elements alive) hst1 hst2 ~> tt THEN hsilocal_simu_core (Some alive) hst1 hst2. Proof. wlp_simplify. constructor; [|constructor]; [assumption | | congruence]. intros. symmetry. eauto. (* rewrite (PTree_frame_eq_check_correct _ (Regset.elements alive) hst1 hst2); [reflexivity | eassumption | ]. apply regset_elements_in. assumption. *) Qed. Hint Resolve hsilocal_frame_simu_check_correct: wlp. Global Opaque hsilocal_frame_simu_check. Definition init_hsistate_local (_:unit): ?? hsistate_local := DO hm <~ hSinit ();; RET {| hsi_smem := hm; hsi_ok_lsval := nil; hsi_sreg := PTree.empty hsval |}. Remark hsinit_seval_hsmem ge sp rs0 m0: WHEN hSinit () ~> init THEN seval_hsmem ge sp init rs0 m0 = Some m0. Proof. wlp_simplify. unfold hSinit in Hexta. apply hC_hsmem_correct in Hexta. simpl in Hexta. unfold seval_hsmem. rewrite <- Hexta. simpl. reflexivity. Qed. Remark init_hsistate_local_correct ge sp rs0 m0: WHEN init_hsistate_local () ~> hsl THEN hsilocal_refines ge sp rs0 m0 hsl init_sistate_local. Proof. wlp_simplify. constructor; constructor; simpl. - intro. destruct H as (_ & SMEM & SVAL). unfold hsok_local. simpl. contradiction. - intro. constructor; [simpl; auto|]. constructor; simpl; discriminate. - unfold hsok_local. simpl. intros; simpl. apply hsinit_seval_hsmem. assumption. - constructor. + intros. simpl. unfold hsi_sreg_eval. rewrite PTree.gempty. reflexivity. + intros r sv. rewrite PTree.gempty. discriminate. Qed. (** Simulation of exits *) Definition hsiexit_simu_core dm f (hse1 hse2: hsistate_exit) := (exists path, (fn_path f) ! (hsi_ifso hse1) = Some path /\ hsilocal_simu_core (Some path.(input_regs)) (hsi_elocal hse1) (hsi_elocal hse2)) /\ dm ! (hsi_ifso hse2) = Some (hsi_ifso hse1) /\ hsi_cond hse1 = hsi_cond hse2 /\ hsi_scondargs hse1 = hsi_scondargs hse2 (* FIXME - should there be something about okvals ? *). (** NB: we split the refinement relation between a "static" part -- independendent of the initial context and a "dynamic" part -- that depends on it *) Definition hsiexit_refines_stat (hext: hsistate_exit) (ext: sistate_exit): Prop := hsi_ifso hext = si_ifso ext. Definition hsok_exit ge sp rs m hse := hsok_local ge sp rs m (hsi_elocal hse). Definition hseval_condition ge sp cond hcondargs hmem rs0 m0 := seval_condition ge sp cond (hsval_list_proj hcondargs) (hsmem_proj hmem) rs0 m0. Lemma hseval_condition_preserved ge ge' sp cond args mem rs0 m0: (forall s : ident, Genv.find_symbol ge' s = Genv.find_symbol ge s) -> hseval_condition ge sp cond args mem rs0 m0 = hseval_condition ge' sp cond args mem rs0 m0. Proof. intros. unfold hseval_condition. erewrite seval_condition_preserved; [|eapply H]. reflexivity. Qed. Definition hsiexit_refines_dyn ge sp rs0 m0 (hext: hsistate_exit) (ext: sistate_exit): Prop := hsilocal_refines ge sp rs0 m0 (hsi_elocal hext) (si_elocal ext) /\ (hsok_local ge sp rs0 m0 (hsi_elocal hext) -> hseval_condition ge sp (hsi_cond hext) (hsi_scondargs hext) (hsi_smem (hsi_elocal hext)) rs0 m0 = seval_condition ge sp (si_cond ext) (si_scondargs ext) (si_smem (si_elocal ext)) rs0 m0). Definition hsiexit_simu dm f (ctx: simu_proof_context f) hse1 hse2: Prop := forall se1 se2, hsiexit_refines_stat hse1 se1 -> hsiexit_refines_stat hse2 se2 -> hsiexit_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1 se1 -> hsiexit_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse2 se2 -> siexit_simu dm f ctx se1 se2. Lemma hsiexit_simu_core_nofail dm f hse1 hse2 ge1 ge2 sp rs m: hsiexit_simu_core dm f hse1 hse2 -> (forall s, Genv.find_symbol ge1 s = Genv.find_symbol ge2 s) -> hsok_exit ge1 sp rs m hse1 -> hsok_exit ge2 sp rs m hse2. Proof. intros CORE GFS HOK1. destruct CORE as ((p & _ & CORE') & _ & _ & _). eapply hsilocal_simu_core_nofail; eauto. Qed. Theorem hsiexit_simu_core_correct dm f hse1 hse2 ctx: hsiexit_simu_core dm f hse1 hse2 -> hsiexit_simu dm f ctx hse1 hse2. Proof. intros SIMUC st1 st2 HREF1 HREF2 HDYN1 HDYN2. assert (SEVALC: sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal st1) -> (seval_condition (the_ge1 ctx) (the_sp ctx) (si_cond st1) (si_scondargs st1) (si_smem (si_elocal st1)) (the_rs0 ctx) (the_m0 ctx)) = (seval_condition (the_ge2 ctx) (the_sp ctx) (si_cond st2) (si_scondargs st2) (si_smem (si_elocal st2)) (the_rs0 ctx) (the_m0 ctx))). { destruct HDYN1 as ((OKEQ1 & _) & SCOND1). rewrite OKEQ1; intro OK1. rewrite <- SCOND1 by assumption. clear SCOND1. generalize (genv_match ctx). intro GFS; refine (modusponens _ _ (hsiexit_simu_core_nofail _ _ _ _ _ _ _ _ _ _ _ _) _); eauto. destruct HDYN2 as (_ & SCOND2). intro OK2. rewrite <- SCOND2 by assumption. clear OK1 OK2 SCOND2. destruct SIMUC as ((path & _ & LSIMU) & _ & CONDEQ & ARGSEQ). destruct LSIMU as (_ & _ & MEMEQ). rewrite CONDEQ. rewrite ARGSEQ. rewrite MEMEQ. erewrite <- hseval_condition_preserved; eauto. } constructor; [assumption|]. intros is1 ICONT SSEME. assert (OK1: sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal st1)). { destruct SSEME as (_ & SSEML & _). eapply ssem_local_sok; eauto. } assert (HOK1: hsok_exit (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1). { unfold hsok_exit. destruct HDYN1 as (LREF & _). destruct LREF as (OKEQ & _ & _). rewrite <- OKEQ. assumption. } refine (modusponens _ _ (hsiexit_simu_core_nofail _ _ _ _ _ _ _ _ _ _ _ _) _). 2: eapply ctx. all: eauto. intro HOK2. destruct SSEME as (SCOND & SLOC & PCEQ). destruct SIMUC as ((path & PATH & LSIMU) & REVEQ & _ & _); eauto. destruct HDYN1 as (LREF1 & _). destruct HDYN2 as (LREF2 & _). exploit hsilocal_simu_core_correct; eauto; [apply ctx|]. simpl. intros (SSEML & EQREG). eexists (mk_istate (icontinue is1) (si_ifso st2) _ (imem is1)). simpl. constructor. - constructor; intuition congruence || eauto. - unfold istate_simu. rewrite ICONT. simpl. assert (PCEQ': hsi_ifso hse1 = ipc is1) by congruence. exists path. constructor; [|constructor]; [congruence| |congruence]. constructor; [|constructor]; simpl; auto. Qed. Remark hsiexit_simu_siexit dm f ctx hse1 hse2 se1 se2: hsiexit_simu dm f ctx hse1 hse2 -> hsiexit_refines_stat hse1 se1 -> hsiexit_refines_stat hse2 se2 -> hsiexit_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1 se1 -> hsiexit_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse2 se2 -> siexit_simu dm f ctx se1 se2. Proof. auto. Qed. 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 ~> tt 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). Theorem hsiexit_simu_check_correct dm f hse1 hse2: WHEN hsiexit_simu_check dm f hse1 hse2 ~> tt THEN hsiexit_simu_core dm f hse1 hse2. Proof. wlp_simplify. constructor; [| constructor; [| constructor]]. 2-4: assumption. exists a. constructor. 1-2: assumption. Qed. Hint Resolve hsiexit_simu_check_correct: wlp. Global Opaque hsiexit_simu_check. Definition hsiexits_simu dm f (ctx: simu_proof_context f) lhse1 lhse2: Prop := list_forall2 (hsiexit_simu dm f ctx) lhse1 lhse2. Definition hsiexits_simu_core dm f lhse1 lhse2: Prop := list_forall2 (hsiexit_simu_core dm f) lhse1 lhse2. Theorem hsiexits_simu_core_correct dm f lhse1 lhse2 ctx: hsiexits_simu_core dm f lhse1 lhse2 -> hsiexits_simu dm f ctx lhse1 lhse2. Proof. induction 1; [constructor|]. constructor; [|apply IHlist_forall2; assumption]. apply hsiexit_simu_core_correct; assumption. Qed. Definition hsiexits_refines_stat lhse lse := list_forall2 hsiexit_refines_stat lhse lse. Definition hsiexits_refines_dyn ge sp rs0 m0 lhse se := list_forall2 (hsiexit_refines_dyn ge sp rs0 m0) lhse se. 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. Theorem hsiexits_simu_check_correct dm f: forall le1 le2, WHEN hsiexits_simu_check dm f le1 le2 ~> tt THEN hsiexits_simu_core dm f le1 le2. Proof. induction le1; simpl. - destruct le2; wlp_simplify. constructor. - destruct le2; wlp_simplify. constructor; [assumption|]. eapply IHle1. eassumption. Qed. Hint Resolve hsiexits_simu_check_correct: wlp. Global Opaque hsiexits_simu_check. Definition hsistate_simu_core dm f (hse1 hse2: hsistate) := dm ! (hsi_pc hse2) = Some (hsi_pc hse1) /\ list_forall2 (hsiexit_simu_core dm f) (hsi_exits hse1) (hsi_exits hse2) /\ hsilocal_simu_core None (hsi_local hse1) (hsi_local hse2). Definition hsistate_refines_stat (hst: hsistate) (st:sistate): Prop := hsi_pc hst = si_pc st /\ hsiexits_refines_stat (hsi_exits hst) (si_exits st). Inductive nested_sok ge sp rs0 m0: sistate_local -> list sistate_exit -> Prop := nsok_nil st: nested_sok ge sp rs0 m0 st nil | nsok_cons st se lse: (sok_local ge sp rs0 m0 st -> sok_local ge sp rs0 m0 (si_elocal se)) -> nested_sok ge sp rs0 m0 (si_elocal se) lse -> nested_sok ge sp rs0 m0 st (se::lse). Lemma nested_sok_prop ge sp st sle rs0 m0: nested_sok ge sp rs0 m0 st sle -> sok_local ge sp rs0 m0 st -> forall se, In se sle -> sok_local ge sp rs0 m0 (si_elocal se). Proof. induction 1; simpl; intuition (subst; eauto). Qed. Lemma nested_sok_elocal ge sp rs0 m0 st2 exits: nested_sok ge sp rs0 m0 st2 exits -> forall st1, (sok_local ge sp rs0 m0 st1 -> sok_local ge sp rs0 m0 st2) -> nested_sok ge sp rs0 m0 st1 exits. Proof. induction 1; [intros; constructor|]. intros. constructor; auto. Qed. Lemma nested_sok_tail ge sp rs0 m0 st lx exits: is_tail lx exits -> nested_sok ge sp rs0 m0 st exits -> nested_sok ge sp rs0 m0 st lx. Proof. induction 1; [auto|]. intros. inv H0. eapply IHis_tail. eapply nested_sok_elocal; eauto. Qed. Definition hsistate_refines_dyn ge sp rs0 m0 (hst: hsistate) (st:sistate): Prop := hsiexits_refines_dyn ge sp rs0 m0 (hsi_exits hst) (si_exits st) /\ hsilocal_refines ge sp rs0 m0 (hsi_local hst) (si_local st) /\ nested_sok ge sp rs0 m0 (si_local st) (si_exits st). Definition hsistate_simu dm f (hst1 hst2: hsistate) (ctx: simu_proof_context f): Prop := forall st1 st2, hsistate_refines_stat hst1 st1 -> hsistate_refines_stat hst2 st2 -> hsistate_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst1 st1 -> hsistate_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst2 st2 -> sistate_simu dm f st1 st2 ctx. Definition init_hsistate pc: ?? hsistate := DO hst <~ init_hsistate_local ();; RET {| hsi_pc := pc; hsi_exits := nil; hsi_local := hst |}. Remark init_hsistate_correct_stat pc: WHEN init_hsistate pc ~> hst THEN hsistate_refines_stat hst (init_sistate pc). Proof. wlp_simplify. constructor; constructor; simpl; auto. Qed. Hint Resolve init_hsistate_correct_stat: wlp. Remark init_hsistate_correct_dyn ge sp rs0 m0 pc: WHEN init_hsistate pc ~> hst THEN hsistate_refines_dyn ge sp rs0 m0 hst (init_sistate pc). Proof. unfold init_hsistate. wlp_bind hst. wlp_simplify. constructor; simpl; auto; [|constructor]. - apply list_forall2_nil. - apply init_hsistate_local_correct. assumption. - constructor. Qed. Lemma siexits_simu_all_fallthrough dm f ctx: forall lse1 lse2, siexits_simu dm f lse1 lse2 ctx -> all_fallthrough (the_ge1 ctx) (the_sp ctx) lse1 (the_rs0 ctx) (the_m0 ctx) -> (forall se1, In se1 lse1 -> sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal se1)) -> all_fallthrough (the_ge2 ctx) (the_sp ctx) lse2 (the_rs0 ctx) (the_m0 ctx). Proof. induction 1; [unfold all_fallthrough; contradiction|]; simpl. intros X OK ext INEXT. eapply all_fallthrough_revcons in X. destruct X as (SEVAL & ALLFU). apply IHlist_forall2 in ALLFU. - destruct H as (CONDSIMU & _). inv INEXT; [|eauto]. erewrite <- CONDSIMU; eauto. - intros; intuition. Qed. Lemma hsiexits_simu_siexits dm f ctx lhse1 lhse2: hsiexits_simu dm f ctx lhse1 lhse2 -> forall lse1 lse2, hsiexits_refines_stat lhse1 lse1 -> hsiexits_refines_stat lhse2 lse2 -> hsiexits_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) lhse1 lse1 -> hsiexits_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) lhse2 lse2 -> siexits_simu dm f lse1 lse2 ctx. Proof. induction 1. - intros. inv H. inv H0. constructor. - intros lse1 lse2 SREF1 SREF2 DREF1 DREF2. inv SREF1. inv SREF2. inv DREF1. inv DREF2. constructor; [| eapply IHlist_forall2; eauto]. eapply hsiexit_simu_siexit; eauto. Qed. Lemma siexits_simu_all_fallthrough_upto dm f ctx lse1 lse2: siexits_simu dm f lse1 lse2 ctx -> forall ext1 lx1, (forall se1, In se1 lx1 -> sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal se1)) -> all_fallthrough_upto_exit (the_ge1 ctx) (the_sp ctx) ext1 lx1 lse1 (the_rs0 ctx) (the_m0 ctx) -> exists ext2 lx2, all_fallthrough_upto_exit (the_ge2 ctx) (the_sp ctx) ext2 lx2 lse2 (the_rs0 ctx) (the_m0 ctx) /\ length lx1 = length lx2. Proof. induction 1. - intros ext lx1. intros OK H. destruct H as (ITAIL & ALLFU). eapply is_tail_false in ITAIL. contradiction. - simpl; intros ext lx1 OK ALLFUE. destruct ALLFUE as (ITAIL & ALLFU). inv ITAIL. + eexists; eexists. constructor; [| eapply list_forall2_length; eauto]. constructor; [econstructor | eapply siexits_simu_all_fallthrough; eauto]. + exploit IHlist_forall2. * intuition. apply OK. eassumption. * constructor; eauto. * intros (ext2 & lx2 & ALLFUE2 & LENEQ). eexists; eexists. constructor; eauto. eapply all_fallthrough_upto_exit_cons; eauto. Qed. Lemma list_forall2_nth_error {A} (l1 l2: list A) P: list_forall2 P l1 l2 -> forall x1 x2 n, nth_error l1 n = Some x1 -> nth_error l2 n = Some x2 -> P x1 x2. Proof. induction 1. - intros. rewrite nth_error_nil in H. discriminate. - intros x1 x2 n. destruct n as [|n]; simpl. + intros. inv H1. inv H2. assumption. + apply IHlist_forall2. Qed. Lemma is_tail_length {A} (l1 l2: list A): is_tail l1 l2 -> (length l1 <= length l2)%nat. Proof. induction l2. - intro. destruct l1; auto. apply is_tail_false in H. contradiction. - intros ITAIL. inv ITAIL; auto. apply IHl2 in H1. clear IHl2. simpl. omega. Qed. Lemma is_tail_nth_error {A} (l1 l2: list A) x: is_tail (x::l1) l2 -> nth_error l2 ((length l2) - length l1 - 1) = Some x. Proof. induction l2. - intro ITAIL. apply is_tail_false in ITAIL. contradiction. - intros ITAIL. assert (length (a::l2) = S (length l2)) by auto. rewrite H. clear H. assert (forall n n', ((S n) - n' - 1)%nat = (n - n')%nat) by (intros; omega). rewrite H. clear H. inv ITAIL. + assert (forall n, (n - n)%nat = 0%nat) by (intro; omega). rewrite H. simpl. reflexivity. + exploit IHl2; eauto. intros. clear IHl2. assert (forall n n', (n > n')%nat -> (n - n')%nat = S (n - n' - 1)%nat) by (intros; omega). exploit (is_tail_length (x::l1)); eauto. intro. simpl in H2. assert ((length l2 > length l1)%nat) by omega. clear H2. rewrite H0; auto. Qed. Theorem hsistate_simu_core_correct dm f hst1 hst2 ctx: hsistate_simu_core dm f hst1 hst2 -> hsistate_simu dm f hst1 hst2 ctx. Proof. intros SIMUC st1 st2 HREF1 HREF2 DREF1 DREF2 is1 SEMI. destruct HREF1 as (PCREF1 & EREF1). destruct HREF2 as (PCREF2 & EREF2). destruct DREF1 as (DEREF1 & LREF1 & NESTED). destruct DREF2 as (DEREF2 & LREF2 & _). destruct SIMUC as (PCSIMU & ESIMU & LSIMU). exploit hsiexits_simu_core_correct; eauto. intro HESIMU. unfold ssem_internal in SEMI. destruct (icontinue _) eqn:ICONT. - destruct SEMI as (SSEML & PCEQ & ALLFU). exploit hsilocal_simu_core_correct; eauto; [apply ctx|]. simpl. intro SSEML2. exists (mk_istate (icontinue is1) (si_pc st2) (irs is1) (imem is1)). constructor. + unfold ssem_internal. simpl. rewrite ICONT. constructor; [assumption | constructor; [reflexivity |]]. eapply siexits_simu_all_fallthrough; eauto. * eapply hsiexits_simu_siexits; eauto. * eapply nested_sok_prop; eauto. eapply ssem_local_sok; eauto. + unfold istate_simu. rewrite ICONT. constructor; [simpl; assumption | constructor; [| reflexivity]]. constructor. - destruct SEMI as (ext & lx & SSEME & ALLFU). assert (SESIMU: siexits_simu dm f (si_exits st1) (si_exits st2) ctx) by (eapply hsiexits_simu_siexits; eauto). exploit siexits_simu_all_fallthrough_upto; eauto. * destruct ALLFU as (ITAIL & ALLF). exploit nested_sok_tail; eauto. intros NESTED2. inv NESTED2. destruct SSEME as (_ & SSEML & _). eapply ssem_local_sok in SSEML. eapply nested_sok_prop; eauto. * intros (ext2 & lx2 & ALLFU2 & LENEQ). assert (EXTSIMU: siexit_simu dm f ctx ext ext2). { eapply list_forall2_nth_error; eauto. - destruct ALLFU as (ITAIL & _). eapply is_tail_nth_error; eauto. - destruct ALLFU2 as (ITAIL & _). eapply is_tail_nth_error in ITAIL. assert (LENEQ': length (si_exits st1) = length (si_exits st2)) by (eapply list_forall2_length; eauto). congruence. } destruct EXTSIMU as (CONDEVAL & EXTSIMU). apply EXTSIMU in SSEME; [|assumption]. clear EXTSIMU. destruct SSEME as (is2 & SSEME2 & ISIMU). exists (mk_istate (icontinue is1) (ipc is2) (irs is2) (imem is2)). constructor. + unfold ssem_internal. simpl. rewrite ICONT. exists ext2, lx2. constructor; assumption. + unfold istate_simu in *. rewrite ICONT in *. destruct ISIMU as (path & PATHEQ & ISIMULIVE & DMEQ). destruct ISIMULIVE as (CONTEQ & REGEQ & MEMEQ). exists path. repeat (constructor; auto). Qed. Definition hsistate_simu_check (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsistate) := revmap_check_single dm (hsi_pc hst1) (hsi_pc hst2);; hsilocal_simu_check (hsi_local hst1) (hsi_local hst2);; hsiexits_simu_check dm f (hsi_exits hst1) (hsi_exits hst2). Theorem hsistate_simu_check_correct dm f hst1 hst2: WHEN hsistate_simu_check dm f hst1 hst2 ~> tt THEN hsistate_simu_core dm f hst1 hst2. Proof. wlp_simplify. constructor; [|constructor]. 1-3: assumption. Qed. Hint Resolve hsistate_simu_check_correct: wlp. Global Opaque hsistate_simu_check. Definition hsi_proj (hsi: hsval + ident) := match hsi with | inl hv => inl (hsval_proj hv) | inr id => inr id end. Fixpoint barg_proj (bhv: builtin_arg hsval) := match bhv with | BA hv => BA (hsval_proj hv) | BA_splitlong ba1 ba2 => BA_splitlong (barg_proj ba1) (barg_proj ba2) | BA_addptr ba1 ba2 => BA_addptr (barg_proj ba1) (barg_proj ba2) | BA_int i => BA_int i | BA_long i => BA_long i | BA_float f => BA_float f | BA_single f32 => BA_single f32 | BA_loadstack m p => BA_loadstack m p | BA_addrstack p => BA_addrstack p | BA_loadglobal c i p => BA_loadglobal c i p | BA_addrglobal i p => BA_addrglobal i p end. Fixpoint barg_list_proj lbh := match lbh with | [] => [] | bh::lbh => (barg_proj bh) :: (barg_list_proj lbh) end. Definition option_hsval_proj oh := match oh with None => None | Some h => Some (hsval_proj h) end. Definition hfinal_proj hfv := match hfv with | HSnone => Snone | HScall s hvi hlv r pc => Scall s (hsi_proj hvi) (hsval_list_proj hlv) r pc | HStailcall s hvi hlv => Stailcall s (hsi_proj hvi) (hsval_list_proj hlv) | HSbuiltin ef lbh br pc => Sbuiltin ef (barg_list_proj lbh) br pc | HSjumptable hv ln => Sjumptable (hsval_proj hv) ln | HSreturn oh => Sreturn (option_hsval_proj oh) end. Section HFINAL_REFINES. Variable ge: RTL.genv. Variable sp: val. Variable rs0: regset. Variable m0: mem. Definition sval_refines (hv: hsval) (sv: sval) := seval_hsval ge sp hv rs0 m0 = seval_sval ge sp sv rs0 m0. Definition sum_refines (hsi: hsval + ident) (si: sval + ident) := match hsi, si with | inl hv, inl sv => sval_refines hv sv | inr id, inr id' => id = id' | _, _ => False end. Inductive list_refines: list_hsval -> list_sval -> Prop := | hsnil_ref: forall h, list_refines (HSnil h) Snil | hscons_ref: forall lhv lsv hv sv h, list_refines lhv lsv -> sval_refines hv sv -> list_refines (HScons hv lhv h) (Scons sv lsv). Inductive barg_refines: builtin_arg hsval -> builtin_arg sval -> Prop := | hba_ref: forall hsv sv, sval_refines hsv sv -> barg_refines (BA hsv) (BA sv) | hba_splitlong: forall bha1 bha2 ba1 ba2, barg_refines bha1 ba1 -> barg_refines bha2 ba2 -> barg_refines (BA_splitlong bha1 bha2) (BA_splitlong ba1 ba2) | hba_addptr: forall bha1 bha2 ba1 ba2, barg_refines bha1 ba1 -> barg_refines bha2 ba2 -> barg_refines (BA_addptr bha1 bha2) (BA_addptr ba1 ba2) | hba_int: forall i, barg_refines (BA_int i) (BA_int i) | hba_long: forall l, barg_refines (BA_long l) (BA_long l) | hba_float: forall f, barg_refines (BA_float f) (BA_float f) | hba_single: forall s, barg_refines (BA_single s) (BA_single s) | hba_loadstack: forall chk ptr, barg_refines (BA_loadstack chk ptr) (BA_loadstack chk ptr) | hba_addrstack: forall ptr, barg_refines (BA_addrstack ptr) (BA_addrstack ptr) | hba_loadglobal: forall chk id ptr, barg_refines (BA_loadglobal chk id ptr) (BA_loadglobal chk id ptr) | hba_addrglobal: forall id ptr, barg_refines (BA_addrglobal id ptr) (BA_addrglobal id ptr). Definition option_refines ohsv osv := match ohsv, osv with | Some hsv, Some sv => sval_refines hsv sv | None, None => True | _, _ => False end. Inductive hfinal_refines: hsfval -> sfval -> Prop := | hsnone_ref: hfinal_refines HSnone Snone | hscall_ref: forall hros ros hargs args s r pc, sum_refines hros ros -> list_refines hargs args -> hfinal_refines (HScall s hros hargs r pc) (Scall s ros args r pc) | hstailcall_ref: forall hros ros hargs args s, sum_refines hros ros -> list_refines hargs args -> hfinal_refines (HStailcall s hros hargs) (Stailcall s ros args) | hsbuiltin_ref: forall ef lbha lba br pc, list_forall2 barg_refines lbha lba -> hfinal_refines (HSbuiltin ef lbha br pc) (Sbuiltin ef lba br pc) | hsjumptable_ref: forall hsv sv lpc, sval_refines hsv sv -> hfinal_refines (HSjumptable hsv lpc) (Sjumptable sv lpc) | hsreturn_ref: forall ohsv osv, option_refines ohsv osv -> hfinal_refines (HSreturn ohsv) (Sreturn osv). Remark hfinal_refines_snone: hfinal_refines HSnone Snone. Proof. constructor. Qed. End HFINAL_REFINES. Lemma list_proj_refines_eq ge ge' sp rs0 m0: forall lsv lhsv, (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) -> list_refines ge sp rs0 m0 lhsv lsv -> forall lhsv' lsv', list_refines ge' sp rs0 m0 lhsv' lsv' -> hsval_list_proj lhsv = hsval_list_proj lhsv' -> seval_list_sval ge sp lsv rs0 m0 = seval_list_sval ge' sp lsv' rs0 m0. Proof. induction 2; rename H into GFS. - simpl. intros. destruct lhsv'; try discriminate. clear H0. inv H. simpl. reflexivity. - simpl. intros. destruct lhsv'; try discriminate. simpl in H2. inv H2. destruct lsv'; [inv H|]. inv H. simpl. assert (SVALEQ: seval_sval ge sp sv rs0 m0 = seval_sval ge' sp sv0 rs0 m0). { rewrite <- H10. rewrite <- H1. unfold seval_hsval. erewrite <- seval_preserved; [| eapply GFS]. congruence. } rewrite SVALEQ. erewrite IHlist_refines; eauto. Qed. Lemma sval_refines_proj ge ge' sp rs m hsv sv hsv' sv': (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) -> sval_refines ge sp rs m hsv sv -> sval_refines ge' sp rs m hsv' sv' -> hsval_proj hsv = hsval_proj hsv' -> seval_sval ge sp sv rs m = seval_sval ge' sp sv' rs m. Proof. intros GFS REF REF' PROJ. rewrite <- REF. rewrite <- REF'. unfold seval_hsval. erewrite <- seval_preserved; [| eapply GFS]. congruence. Qed. Lemma barg_proj_refines_eq_single ge ge' sp rs0 m0: (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) -> forall hsv sv, barg_refines ge sp rs0 m0 hsv sv -> forall hsv' sv', barg_refines ge' sp rs0 m0 hsv' sv' -> barg_proj hsv = barg_proj hsv' -> seval_builtin_sval ge sp sv rs0 m0 = seval_builtin_sval ge' sp sv' rs0 m0. Proof. intro GFS. induction 1. all: try (simpl; intros hsv' sv' BREF' BPROJ'; destruct hsv'; simpl in BPROJ'; try discriminate; inv BPROJ'; inv BREF'; simpl; try reflexivity; erewrite sval_refines_proj; eauto). (* BA_splitlong *) - simpl. intros hsv' sv' BREF' BPROJ'. destruct hsv'; simpl in BPROJ'; try discriminate. inv BPROJ'. inv BREF'. simpl. erewrite IHbarg_refines2; eauto. erewrite IHbarg_refines1. 2: eapply H5. all: eauto. (* BA_addptr *) - simpl. intros hsv' sv' BREF' BPROJ'. destruct hsv'; simpl in BPROJ'; try discriminate. inv BPROJ'. inv BREF'. simpl. erewrite IHbarg_refines2; eauto. erewrite IHbarg_refines1. 2: eapply H5. all: eauto. Qed. Lemma barg_proj_refines_eq ge ge' sp rs0 m0: forall lsv lhsv, (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) -> list_forall2 (barg_refines ge sp rs0 m0) lhsv lsv -> forall lhsv' lsv', list_forall2 (barg_refines ge' sp rs0 m0) lhsv' lsv' -> barg_list_proj lhsv = barg_list_proj lhsv' -> seval_list_builtin_sval ge sp lsv rs0 m0 = seval_list_builtin_sval ge' sp lsv' rs0 m0. Proof. induction 2; rename H into GFS. - simpl. intros. destruct lhsv'; try discriminate. clear H0. inv H. simpl. reflexivity. - simpl. intros. destruct lhsv'; try discriminate. simpl in H2. inv H2. destruct lsv'; [inv H|]. inv H. simpl. erewrite barg_proj_refines_eq_single; eauto. erewrite IHlist_forall2; eauto. Qed. Definition final_simu_core (dm: PTree.t node) (f: RTLpath.function) (pc1 pc2: node) (f1 f2: sfval): Prop := match f1 with | Scall sig1 svos1 lsv1 res1 pc1 => match f2 with | Scall sig2 svos2 lsv2 res2 pc2 => dm ! pc2 = Some pc1 /\ sig1 = sig2 /\ svos1 = svos2 /\ lsv1 = lsv2 /\ res1 = res2 | _ => False end | Sbuiltin ef1 lbs1 br1 pc1 => match f2 with | Sbuiltin ef2 lbs2 br2 pc2 => dm ! pc2 = Some pc1 /\ ef1 = ef2 /\ lbs1 = lbs2 /\ br1 = br2 | _ => False end | Sjumptable sv1 lpc1 => match f2 with | Sjumptable sv2 lpc2 => ptree_get_list dm lpc2 = Some lpc1 /\ sv1 = sv2 | _ => False end | Snone => match f2 with | Snone => dm ! pc2 = Some pc1 | _ => False end (* Stailcall, Sreturn *) | _ => f1 = f2 end. Definition hfinal_simu_core (dm: PTree.t node) (f: RTLpath.function) (pc1 pc2: node) (hf1 hf2: hsfval): Prop := final_simu_core dm f pc1 pc2 (hfinal_proj hf1) (hfinal_proj hf2). Lemma svident_simu_refl f ctx s: svident_simu f ctx s s. Proof. destruct s; constructor; [| reflexivity]. erewrite <- seval_preserved; [| eapply ctx]. constructor. Qed. Theorem hfinal_simu_core_correct dm f ctx opc1 opc2 hf1 hf2 f1 f2: hfinal_simu_core dm f opc1 opc2 hf1 hf2 -> hfinal_refines (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hf1 f1 -> hfinal_refines (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hf2 f2 -> sfval_simu dm f opc1 opc2 ctx f1 f2. Proof. assert (GFS: forall s : ident, Genv.find_symbol (the_ge1 ctx) s = Genv.find_symbol (the_ge2 ctx) s) by apply ctx. intros CORE FREF1 FREF2. destruct hf1; inv FREF1. (* Snone *) - destruct hf2; try contradiction. inv FREF2. inv CORE. constructor. assumption. (* Scall *) - rename H5 into SREF1. rename H6 into LREF1. destruct hf2; try contradiction. inv FREF2. rename H5 into SREF2. rename H6 into LREF2. destruct CORE as (PCEQ & ? & ? & ? & ?). subst. rename H0 into SVOSEQ. rename H1 into LSVEQ. constructor; [assumption | |]. + destruct svos. * destruct svos0; try discriminate. destruct ros; try contradiction. destruct ros0; try contradiction. constructor. simpl in SVOSEQ. inv SVOSEQ. simpl in SREF1. simpl in SREF2. rewrite <- SREF1. rewrite <- SREF2. unfold seval_hsval. erewrite <- seval_preserved; [| eapply GFS]. congruence. * destruct svos0; try discriminate. destruct ros; try contradiction. destruct ros0; try contradiction. constructor. simpl in SVOSEQ. inv SVOSEQ. congruence. + erewrite list_proj_refines_eq; eauto. constructor. (* Stailcall *) - rename H3 into SREF1. rename H4 into LREF1. destruct hf2; try (inv CORE; fail). inv FREF2. rename H4 into LREF2. rename H3 into SREF2. inv CORE. rename H1 into SVOSEQ. rename H2 into LSVEQ. constructor. + destruct svos. (** Copy-paste from Scall *) * destruct svos0; try discriminate. destruct ros; try contradiction. destruct ros0; try contradiction. constructor. simpl in SVOSEQ. inv SVOSEQ. simpl in SREF1. simpl in SREF2. rewrite <- SREF1. rewrite <- SREF2. unfold seval_hsval. erewrite <- seval_preserved; [| eapply GFS]. congruence. * destruct svos0; try discriminate. destruct ros; try contradiction. destruct ros0; try contradiction. constructor. simpl in SVOSEQ. inv SVOSEQ. congruence. + erewrite list_proj_refines_eq; eauto. constructor. (* Sbuiltin *) - rename H4 into BREF1. destruct hf2; try (inv CORE; fail). inv FREF2. rename H4 into BREF2. inv CORE. destruct H0 as (? & ? & ?). subst. rename H into PCEQ. rename H1 into ARGSEQ. constructor; [assumption|]. erewrite barg_proj_refines_eq; eauto. constructor. (* Sjumptable *) - rename H2 into SREF1. destruct hf2; try contradiction. inv FREF2. rename H2 into SREF2. destruct CORE as (A & B). constructor; [assumption|]. erewrite sval_refines_proj; eauto. constructor. (* Sreturn *) - rename H0 into SREF1. destruct hf2; try discriminate. inv CORE. inv FREF2. destruct osv; destruct res; inv SREF1. + destruct res0; try discriminate. destruct osv0; inv H1. constructor. simpl in H0. inv H0. erewrite sval_refines_proj; eauto. constructor. + destruct res0; try discriminate. destruct osv0; inv H1. constructor. Qed. 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 sval_refines_local_get ge sp rs0 m0 hsl sl r: hsok_local ge sp rs0 m0 hsl -> hsilocal_refines ge sp rs0 m0 hsl sl -> WHEN hsi_sreg_get hsl r ~> hsv THEN sval_refines ge sp rs0 m0 hsv (si_sreg sl r). Proof. intros HOK HREF. wlp_intro hsv. unfold sval_refines. erewrite <- hsi_sreg_eval_correct; eauto. destruct HREF as (_ & _ & A & _). rewrite <- A; [| assumption]. reflexivity. Qed. Lemma hsum_left_correct ge sp rs0 m0 hsl sl ros: hsok_local ge sp rs0 m0 hsl -> hsilocal_refines ge sp rs0 m0 hsl sl -> WHEN hsum_left hsl ros ~> svos THEN sum_refines ge sp rs0 m0 svos (sum_left_map (si_sreg sl) ros). Proof. intros HOK HREF. destruct ros; [| wlp_simplify]. wlp_bind hr. wlp_simplify. unfold sval_refines. rewrite sval_refines_local_get; eauto. Qed. Lemma hSnil_correct: WHEN hSnil () ~> shv THEN hsval_list_proj shv = Snil. Proof. wlp_simplify. unfold hSnil in Hexta. apply hC_list_hsval_correct in Hexta. simpl in *. symmetry. assumption. Qed. Global Opaque hSnil. Hint Resolve hSnil_correct: wlp. Lemma hScons_correct: forall lhsv hsv, WHEN hScons hsv lhsv ~> lhsv' THEN hsval_list_proj lhsv' = Scons (hsval_proj hsv) (hsval_list_proj lhsv). Proof. destruct lhsv; wlp_simplify. - unfold hScons in Hexta. apply hC_list_hsval_correct in Hexta. simpl in *. congruence. - unfold hScons in Hexta. apply hC_list_hsval_correct in Hexta. simpl in *. congruence. Qed. Global Opaque hScons. Hint Resolve hScons_correct: wlp. Lemma hsi_sreg_get_refines ge sp rs0 m0 hsl sl r: hsok_local ge sp rs0 m0 hsl -> hsilocal_refines ge sp rs0 m0 hsl sl -> WHEN hsi_sreg_get hsl r ~> hsv THEN sval_refines ge sp rs0 m0 hsv (si_sreg sl r). Proof. intros HOK HREF. wlp_intro hsv. destruct HREF as (_ & _ & A & _). unfold sval_refines. erewrite <- hsi_sreg_eval_correct by eassumption. rewrite A by assumption. reflexivity. Qed. Lemma hsval_list_proj_correct ge sp rs m lsv: forall lhsv, list_refines ge sp rs m lhsv lsv -> forall lhsv', hsval_list_proj lhsv' = hsval_list_proj lhsv -> list_refines ge sp rs m lhsv' lsv. Proof. induction 1. - intro. simpl. intros. destruct lhsv'; try discriminate. constructor. - intros. simpl in H1. destruct lhsv'; try discriminate. simpl in H1. inv H1. apply IHlist_refines in H4. constructor; [assumption|]. unfold sval_refines. unfold seval_hsval. rewrite H3. assumption. Qed. Hint Resolve hsval_list_proj_correct: wlp. Lemma hsval_proj_correct ge sp rs0 m0 hsl sl hsv r: hsok_local ge sp rs0 m0 hsl -> hsilocal_refines ge sp rs0 m0 hsl sl -> WHEN hsi_sreg_get hsl r ~> hsv' THEN hsval_proj hsv = hsval_proj hsv' -> sval_refines ge sp rs0 m0 hsv (si_sreg sl r). Proof. intros HOK HREF. wlp_intro hsv'. intros PROJ. unfold sval_refines. unfold seval_hsval. rewrite PROJ. enough (seval_sval ge sp (hsval_proj hsv') rs0 m0 = seval_hsval ge sp hsv' rs0 m0) as ->; [|reflexivity]. erewrite hsi_sreg_get_refines; eauto. Qed. Hint Resolve hsval_proj_correct: wlp. Lemma hlist_args_correct ge sp rs0 m0 hsl sl: hsok_local ge sp rs0 m0 hsl -> hsilocal_refines ge sp rs0 m0 hsl sl -> forall lr, WHEN hlist_args hsl lr ~> shv THEN list_refines ge sp rs0 m0 shv (list_sval_inj (List.map (si_sreg sl) lr)). Proof. intros HOK HREF. induction lr. - simpl. wlp_simplify. destruct exta; try discriminate. constructor. - simpl. wlp_bind v. wlp_bind lhsv. wlp_simplify. apply IHlr in Hlhsv. clear IHlr. destruct exta; try discriminate. simpl in H. inv H. constructor. + eapply hsval_list_proj_correct; eauto. + eapply hsval_proj_correct; eauto. Qed. Global Opaque hlist_args. Hint Resolve hlist_args_correct: wlp. Lemma hbuiltin_arg_correct ge sp rs0 m0 hsl sl: hsok_local ge sp rs0 m0 hsl -> hsilocal_refines ge sp rs0 m0 hsl sl -> forall br, WHEN hbuiltin_arg hsl br ~> bhsv THEN barg_refines ge sp rs0 m0 bhsv (builtin_arg_map (si_sreg sl) br). Proof. intros HOK HREF. induction br. all: try (wlp_simplify; constructor; auto; fail). (* BA *) - simpl. wlp_bind hsv. wlp_simplify. constructor. eapply hsi_sreg_get_refines; eauto. Qed. Lemma hbuiltin_args_correct ge sp rs0 m0 hsl sl: hsok_local ge sp rs0 m0 hsl -> hsilocal_refines ge sp rs0 m0 hsl sl -> forall lbr, WHEN hbuiltin_args hsl lbr ~> lbhsv THEN list_forall2 (barg_refines ge sp rs0 m0) lbhsv (List.map (builtin_arg_map (si_sreg sl)) lbr). Proof. intros HOK HREF. induction lbr; [wlp_simplify; constructor|]. simpl. wlp_bind ha. wlp_bind hl. wlp_simplify. constructor; [|auto]. eapply hbuiltin_arg_correct; eauto. Qed. Lemma hsexec_final_correct ge sp rs0 m0 hsl sl i: hsok_local ge sp rs0 m0 hsl -> hsilocal_refines ge sp rs0 m0 hsl sl -> WHEN hsexec_final i hsl ~> hsf THEN hfinal_refines ge sp rs0 m0 hsf (sexec_final i sl). Proof. intro HOK. destruct i; simpl; intros HLREF; try (wlp_simplify; apply hfinal_refines_snone). (* Scall *) - wlp_bind svos. wlp_bind sargs. wlp_simplify. constructor. + eapply hsum_left_correct; eauto. + eapply hlist_args_correct; eauto. (* Stailcall *) - wlp_bind svos. wlp_bind sargs. wlp_simplify. constructor. + eapply hsum_left_correct; eauto. + eapply hlist_args_correct; eauto. (* Sbuiltin *) - wlp_simplify. constructor. eapply hbuiltin_args_correct; eauto. (* Sjumptable *) - wlp_bind sv. wlp_simplify. constructor. eapply hsi_sreg_get_refines; eauto. (* Sreturn *) - destruct o. -- wlp_bind sv. wlp_simplify. constructor. simpl. eapply hsi_sreg_get_refines; eauto. -- wlp_simplify. repeat constructor. Qed. 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' ~> tt THEN ptree_get_list dm lpc' = Some lpc. Proof. induction lpc. - destruct lpc'; wlp_simplify. - destruct lpc'; wlp_simplify. rewrite H. rewrite H0. reflexivity. 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 ~> tt THEN svos1 = svos2. Proof. destruct svos1; destruct svos2; wlp_simplify; try wlp_absurd. all: congruence. 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 ~> tt THEN barg_proj bs1 = barg_proj bs2. Proof. induction bs1. all: try (intros; simpl; wlp_simplify; subst; reflexivity). (* BA *) - destruct bs2; wlp_simplify; try wlp_absurd. congruence. (* BA_splitlong *) - destruct bs2; try (wlp_simplify; wlp_absurd). simpl. wlp_bind b1. wlp_intro b2. rewrite IHbs1_1 by eassumption. rewrite IHbs1_2 by eassumption. reflexivity. (* BA_addptr *) - destruct bs2; try (wlp_simplify; wlp_absurd). simpl. wlp_bind b1. wlp_intro b2. rewrite IHbs1_1 by eassumption. rewrite IHbs1_2 by eassumption. reflexivity. 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 ~> tt THEN barg_list_proj lbs1 = barg_list_proj lbs2. Proof. induction lbs1. - wlp_simplify. destruct lbs2; [simpl; reflexivity|]. simpl in Hexta. wlp_absurd. - destruct lbs2; wlp_simplify; try wlp_absurd. 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) (opc1 opc2: node) (fv1 fv2: hsfval) := match fv1, fv2 with | HSnone, HSnone => revmap_check_single dm opc1 opc2 | 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. Theorem sfval_simu_check_correct dm f opc1 opc2 fv1 fv2: WHEN sfval_simu_check dm f opc1 opc2 fv1 fv2 ~> tt THEN hfinal_simu_core dm f opc1 opc2 fv1 fv2. Proof. destruct fv1; destruct fv2; try (wlp_simplify; simpl in Hexta; wlp_absurd). (* HScall *) - simpl. wlp_bind u1 REVMAP. wlp_bind u2 SIG. wlp_bind u3 RES. wlp_bind u4 SVOS. wlp_intro u5 LSV. apply phys_check_correct in SIG. apply phys_check_correct in RES. apply revmap_check_single_correct in REVMAP. apply phys_check_correct in LSV. apply svos_simu_check_correct in SVOS. subst. repeat (constructor; auto). (* HStailcall *) - simpl. wlp_bind u1 SIG. wlp_bind u2 SVOS. wlp_intro u3 LSV. apply phys_check_correct in SIG. apply phys_check_correct in LSV. apply svos_simu_check_correct in SVOS. subst. repeat (constructor; auto). (* HSbuiltin *) - simpl. wlp_bind u1 RMAP. wlp_bind u2 EF. wlp_bind u3 RES. wlp_intro u4 SARGS. apply phys_check_correct in EF. apply phys_check_correct in RES. apply list_builtin_arg_simu_check_correct in SARGS. apply revmap_check_single_correct in RMAP. subst. repeat (constructor; auto). (* HSjumptable *) - simpl. wlp_simplify. subst. constructor; auto. (* HSreturn *) - wlp_simplify. subst. reflexivity. Qed. Hint Resolve sfval_simu_check_correct: wlp. Global Opaque hfinal_simu_core. Definition hsstate_refines (hst: hsstate) (st:sstate): Prop := hsistate_refines_stat (hinternal hst) (internal st) /\ (forall ge sp rs0 m0, hsistate_refines_dyn ge sp rs0 m0 (hinternal hst) (internal st) /\ hfinal_refines ge sp rs0 m0 (hfinal hst) (final st)) . Definition hsstate_simu_core (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) := hsistate_simu_core dm f (hinternal hst1) (hinternal hst2) /\ hfinal_simu_core dm f (hsi_pc (hinternal hst1)) (hsi_pc (hinternal hst2)) (hfinal hst1) (hfinal hst2). Definition hsstate_simu dm f (hst1 hst2: hsstate) ctx: Prop := forall st1 st2, hsstate_refines hst1 st1 -> hsstate_refines hst2 st2 -> sstate_simu dm f st1 st2 ctx. Theorem hsstate_simu_core_correct dm f ctx hst1 hst2: hsstate_simu_core dm f hst1 hst2 -> hsstate_simu dm f hst1 hst2 ctx. Proof. intros (SCORE & FSIMU). intros st1 st2 HREF1 HREF2. destruct HREF1 as (SREF1 & DREF1 & FREF1). destruct HREF2 as (SREF2 & DREF2 & FREF2). assert (PCEQ: dm ! (hsi_pc hst2) = Some (hsi_pc hst1)) by apply SCORE. eapply hsistate_simu_core_correct in SCORE. eapply hfinal_simu_core_correct in FSIMU; eauto. constructor; [apply SCORE; auto|]. 1-2: eassumption. destruct SREF1 as (PC1 & _). destruct SREF2 as (PC2 & _). rewrite <- PC1. rewrite <- PC2. eapply FSIMU. Qed. Definition hsstate_simu_check (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) := hsistate_simu_check dm f (hinternal hst1) (hinternal hst2);; sfval_simu_check dm f (hsi_pc hst1) (hsi_pc hst2) (hfinal hst1) (hfinal hst2). Theorem hsstate_simu_check_correct dm f hst1 hst2: WHEN hsstate_simu_check dm f hst1 hst2 ~> tt THEN hsstate_simu_core dm f hst1 hst2. Proof. wlp_simplify. constructor. 1-2: assumption. Qed. Hint Resolve hsstate_simu_check_correct: wlp. Global Opaque hsstate_simu_core. Definition seval_list_hsval ge sp lhsv rs m := seval_list_sval ge sp (hsval_list_proj lhsv) rs m. Definition hok_args ge sp rs0 m0 hst lr := WHEN hlist_args (hsi_sreg hst) lr ~> lhsv THEN hsok_local ge sp rs0 m0 hst -> (seval_list_hsval ge sp lhsv rs0 m0 <> None). 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. (* Completely lost on that one *) (* Lemma hsok_local_set_sreg ge sp rs0 m0 hst r (rsv:root_sval) lr: WHEN hslocal_set_sreg hst r rsv lr ~> hst' THEN hok_args ge sp rs0 m0 hst lr -> hsok_local ge sp rs0 m0 hst' <-> (hsok_local ge sp rs0 m0 hst /\ (WHEN root_apply rsv lr hst ~> hsv THEN seval_hsval ge sp hsv rs0 m0 <> None)). Proof. unfold hslocal_set_sreg. wlp_bind lhsvok. wlp_bind hsv. wlp_ret hst'. intros HOK. destruct may_trap eqn: MAYTRAP. - wlp_hbind hv. wlp_hret. constructor. + unfold hsok_local. simpl. intro. constructor. * intros. apply H. right. assumption. * wlp_intro hsv'. apply H. unfold hok_args, hsok_local. simpl. unfold hslocal_set_sreg, ok_args, hsok_local; simpl. destruct may_trap eqn: MAYTRAP; simpl; intuition (subst; eauto). eapply may_trap_correct; eauto. Qed. *) Lemma seval_list_sval_proj ge sp rs0 m0: forall lhsv lsv, list_refines ge sp rs0 m0 lhsv lsv -> seval_list_sval ge sp (hsval_list_proj lhsv) rs0 m0 = seval_list_sval ge sp lsv rs0 m0. Proof. induction lhsv. - destruct lsv; simpl; intros H; [reflexivity | inv H]. - destruct lsv; [intro H; inv H|]. intros. inv H. simpl. erewrite IHlhsv; eauto. rewrite H6. reflexivity. Qed. Lemma hSop_correct ge sp rs0 m0 op lhsv lsv hst st: WHEN hSop op lhsv (hsi_smem hst) ~> hsv THEN hsok_local ge sp rs0 m0 hst -> list_refines ge sp rs0 m0 lhsv lsv -> hsilocal_refines ge sp rs0 m0 hst st -> seval_hsval ge sp hsv rs0 m0 = seval_sval ge sp (Sop op lsv (si_smem st)) rs0 m0. Proof. wlp_simplify. apply hC_hsval_correct in Hexta1. simpl in *. unfold seval_hsval. rewrite <- Hexta1. simpl. clear Hexta1. erewrite seval_list_sval_proj; eauto. clear H0. destruct H1 as (A & B & C & D). rewrite <- B; eauto. Qed. (** Version of hSop_correct with weaker hypothesis *) Lemma hSop_correct_mem ge sp rs0 m0 op lhsv lsv hsm sm: WHEN hSop op lhsv hsm ~> hsv THEN seval_hsmem ge sp hsm rs0 m0 = seval_smem ge sp sm rs0 m0 -> list_refines ge sp rs0 m0 lhsv lsv -> seval_hsval ge sp hsv rs0 m0 = seval_sval ge sp (Sop op lsv sm) rs0 m0. Proof. wlp_simplify. apply hC_hsval_correct in Hexta1. simpl in *. unfold seval_hsval. rewrite <- Hexta1. simpl. clear Hexta1. erewrite seval_list_sval_proj; eauto. clear H0. rewrite <- H. eauto. Qed. Lemma hSload_correct ge sp rs0 m0 lhsv lsv hst st trap addr chunk: WHEN hSload (hsi_smem hst) trap chunk addr lhsv ~> hsv THEN hsok_local ge sp rs0 m0 hst -> list_refines ge sp rs0 m0 lhsv lsv -> hsilocal_refines ge sp rs0 m0 hst st -> seval_hsval ge sp hsv rs0 m0 = seval_sval ge sp (Sload (si_smem st) trap chunk addr lsv) rs0 m0. Proof. wlp_simplify. apply hC_hsval_correct in Hexta3. simpl in *. unfold seval_hsval. rewrite <- Hexta3. simpl. clear Hexta3. erewrite seval_list_sval_proj; eauto. clear H0. destruct H1 as (A & B & C & D). rewrite <- B; eauto. Qed. Lemma hsinit_sinit ge sp rs0 m0: WHEN hSinit () ~> init THEN seval_hsmem ge sp init rs0 m0 = seval_smem ge sp Sinit rs0 m0. Proof. wlp_intro init. eapply hsinit_seval_hsmem in Hinit; eauto. Qed. Lemma simplify_correct (rsv: root_sval) lr (ge: RTL.genv) (sp: val) rs0 m0 v hst st: WHEN root_apply rsv lr hst ~> hsv THEN hsok_local ge sp rs0 m0 hst -> hsilocal_refines ge sp rs0 m0 hst st -> seval_hsval ge sp hsv rs0 m0 = Some v -> WHEN simplify rsv lr hst ~> hsv' THEN seval_hsval ge sp hsv' rs0 m0 = Some v. Proof. wlp_bind lhsv. wlp_intro hsv. intros HOK HREF HEVAL. eapply hlist_args_correct in Hlhsv; eauto. destruct rsv; simpl. (* Rop *) - exploit hSop_correct; eauto. intros EVALMOV. clear Hlhsv. clear Hhsv. destruct (is_move_operation _ _) eqn:IMOVE. + apply is_move_operation_correct in IMOVE. inv IMOVE. rewrite <- HEVAL. rewrite EVALMOV. wlp_intro hsv'. simpl. destruct HREF as (A & B & C & D). rewrite <- C; eauto. rewrite hsi_sreg_eval_correct; eauto. destruct (seval_hsval ge sp hsv' rs0 m0); [|reflexivity]. apply A in HOK. destruct HOK as (_ & MOK & _). destruct (seval_smem _ _ _ _ _); [reflexivity|contradiction]. + clear IMOVE. wlp_bind hsm. wlp_bind lhsv'. wlp_intro hsv'. eapply hlist_args_correct in Hlhsv'; eauto. rewrite hSop_correct_mem; eauto; [|eapply hsinit_sinit; eauto]. clear Hlhsv'. clear Hhsv'. rewrite <- HEVAL. rewrite EVALMOV. admit. (** Voir avec Sylvain - je ne sais plus où on en est sur les dépendances mémoires avec les op *) (* Rload *) - exploit hSload_correct; eauto. intros EVALLOAD. wlp_bind lhsv'. wlp_intro hsv'. eapply hlist_args_correct in Hlhsv'; eauto. rewrite hSload_correct; eauto. rewrite EVALLOAD in HEVAL. destruct trap; simpl; auto. simpl in HEVAL. 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. rewrite HEVAL. reflexivity. Admitted. Lemma hsok_local_set_sreg ge sp rs0 m0 hst r (rsv:root_sval) lr: hok_args ge sp rs0 m0 hst lr -> WHEN hslocal_set_sreg hst r rsv lr ~> hst' THEN hsok_local ge sp rs0 m0 hst' <-> (hsok_local ge sp rs0 m0 hst /\ (WHEN root_apply rsv lr hst ~> hsv' THEN seval_hsval ge sp hsv' rs0 m0 <> None)). Proof. (* unfold hslocal_set_sreg, ok_args, hsok_local; simpl. destruct may_trap eqn: MAYTRAP; simpl; intuition (subst; eauto). eapply may_trap_correct; eauto. *) Admitted. Lemma slocal_set_sreg_preserves_sok ge sp rs m st r sv: sok_local ge sp rs m st <-> sok_local ge sp rs m (slocal_set_sreg st r sv). Proof. Admitted. Lemma root_apply_none ge sp rsv rs m hst lr: hsok_local ge sp rs m hst -> WHEN root_apply rsv lr hst ~> hsv THEN seval_hsval ge sp hsv rs m <> None. Proof. Admitted. Lemma hslocal_set_sreg_preserves_smem ge sp hst rs0 m0 r rsv lr: WHEN hslocal_set_sreg hst r rsv lr ~> hst' THEN seval_hsmem ge sp hst' rs0 m0 = seval_hsmem ge sp hst rs0 m0. Proof. Admitted. Lemma hslocal_set_sreg_preserves_hsok ge sp rs m hst r rsv lr: WHEN hslocal_set_sreg hst r rsv lr ~> hst' THEN hsok_local ge sp rs m hst <-> hsok_local ge sp rs m hst'. Proof. Admitted. Lemma red_PTree_set_correct (r r0:reg) (hsv: hsval) (hst: PTree.t hsval) 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. destruct (Pos.eq_dec r0 r1); auto. - subst; rewrite PTree.grs, PTree.gss; simpl; auto. - rewrite PTree.gro, PTree.gso; simpl; auto. Qed. (** TODO - express some lemma about root_apply_correct and simplify_correct * Figure out how to prove this stuff *) Lemma hslocal_set_sreg_correct ge sp rs0 m0 hst st r (rsv:root_sval) lr sv': hsilocal_refines ge sp rs0 m0 hst st -> hok_args ge sp rs0 m0 hst lr -> ( hsok_local ge sp rs0 m0 hst -> WHEN root_apply rsv lr hst ~> hsv THEN seval_sval ge sp sv' rs0 m0 = seval_hsval ge sp hsv rs0 m0) -> WHEN hslocal_set_sreg hst r rsv lr ~> hst' THEN hsilocal_refines ge sp rs0 m0 hst' (slocal_set_sreg st r sv'). Proof. intros HREF HOK REVAL. wlp_intro hst'. unfold hsilocal_refines. split; [|split; [|split]]. + symmetry. eapply iff_trans. eapply hsok_local_set_sreg; eauto. constructor. * intros (HOKL & REVAL'). apply slocal_set_sreg_preserves_sok. destruct HREF as (A & _). apply A in HOKL. assumption. * intros SOKL. rewrite <- slocal_set_sreg_preserves_sok in SOKL. destruct HREF as (A & _). apply A in SOKL. split; [assumption|]. eapply root_apply_none; eauto. + intros HOKL. simpl. rewrite hslocal_set_sreg_preserves_smem; eauto. destruct HREF as (_ & A & _). rewrite A; auto. eapply hslocal_set_sreg_preserves_hsok; eauto. + intros HOKL. simpl. intro r0. unfold hslocal_set_sreg in Hhst'. wlp_hbind ok_lhsv. wlp_hbind hsv'. wlp_hret. simpl. rewrite red_PTree_set_correct. unfold hsi_sreg_eval. destruct (Pos.eq_dec r r0). * subst. rewrite PTree.gss. (* Something about simplify_correct ? *) admit. * admit. + admit. (* intros (ROK & RMEM & RVAL) OKA RSV. unfold hsilocal_refines; simpl. rewrite! hsok_local_set_sreg; eauto. split. + rewrite <- ROK in RSV; rewrite sok_local_set_sreg; eauto. intuition congruence. + split; try tauto. intros (HOKL & RSV2) r0. rewrite red_PTree_set_correct. rewrite hsi_sreg_eval_correct. unfold hsi_sreg_get. destruct (Pos.eq_dec r r0). * subst. rewrite PTree.gss, RSV; auto. destruct (seval_sval ge sp (rsv lsv (hsi_smem hst))) eqn: RSV3; simpl; try congruence. eapply simplify_correct; eauto. * intros; rewrite PTree.gso; auto. rewrite <- RVAL, hsi_sreg_eval_correct; auto. *) Admitted. Lemma seval_list_hsval_refines ge sp rs0 m0 hst st lr: hsok_local ge sp rs0 m0 hst -> hsilocal_refines ge sp rs0 m0 hst st -> WHEN hlist_args hst lr ~> lhsv THEN seval_list_hsval ge sp lhsv rs0 m0 = seval_list_sval ge sp (list_sval_inj (List.map (si_sreg st) lr)) rs0 m0. Proof. intros OKL HLREF. wlp_simplify. destruct lr. - simpl in *. inv H. reflexivity. - inv H. simpl. unfold seval_list_hsval. simpl. rewrite H4. erewrite seval_list_sval_proj; eauto. Qed. Lemma seval_list_sval_none ge sp (srs: reg -> sval) rs0 m0: forall lr, (forall r, seval_sval ge sp (srs r) rs0 m0 <> None) -> seval_list_sval ge sp (list_sval_inj (List.map srs lr)) rs0 m0 <> None. Proof. induction lr. - simpl. discriminate. - intro SR. simpl. destruct (seval_sval _ _ _ _ _) eqn:V. 2: { apply SR in V. inv V. } destruct (seval_list_sval _ _ _ _ _) eqn:LV. 2: { apply IHlr in SR. assumption. } discriminate. Qed. Lemma refines_okargs ge sp rs0 m0 hst st lr: hsistate_refines_dyn ge sp rs0 m0 hst st -> hok_args ge sp rs0 m0 (hsi_local hst) lr. Proof. unfold hok_args. intros (_ & HLREF & _). wlp_intro lhsv LHSV. intros OK. exploit hlist_args_correct; eauto. intro LREF. erewrite seval_list_hsval_refines; eauto. destruct HLREF as (OKEQ & _ & _). rewrite <- OKEQ in OK. destruct OK as (_ & _ & OK). apply seval_list_sval_none. assumption. Qed. (* Local Hint Resolve refines_okargs: core. *) Lemma hsiexec_inst_correct_dyn ge sp rs0 m0 i hst st hst' st': WHEN hsiexec_inst i hst ~> ohst' THEN ohst' = Some hst' -> siexec_inst i st = Some st' -> hsistate_refines_dyn ge sp rs0 m0 hst st -> hsistate_refines_dyn ge sp rs0 m0 hst' st'. Proof. destruct i. (* Inop *) - wlp_simplify. inv H. inv H0. auto. (* Iop *) - simpl. wlp_bind next NEXT. wlp_simplify. inv H. inv H0. eapply hsist_set_local_correct_dyn; eauto. + destruct H1 as (A & B & C). eapply hslocal_set_sreg_correct; eauto. { eapply refines_okargs. repeat (econstructor; eauto). } simpl. intro HOK. unfold root_apply. wlp_bind lhsv LHSV. wlp_intro hsv HSV. eapply hlist_args_correct in LHSV; eauto. erewrite hSop_correct; eauto. simpl. reflexivity. + unfold sok_local; simpl; intros (PRE & MEM & REG). intuition. generalize (REG r0); clear REG. destruct (Pos.eq_dec r r0); simpl; intuition (subst; eauto). (* Iload *) - simpl. wlp_bind next NEXT. wlp_simplify. inv H. inv H0. eapply hsist_set_local_correct_dyn; eauto. + destruct H1 as (A & B & C). eapply hslocal_set_sreg_correct; eauto. { eapply refines_okargs. repeat (econstructor; eauto). } simpl. intro HOK. unfold root_apply. wlp_bind lhsv LHSV. wlp_intro hsv HSV. eapply hlist_args_correct in LHSV; eauto. erewrite hSload_correct; eauto. simpl. reflexivity. + unfold sok_local; simpl; intros (PRE & MEM & REG). intuition. generalize (REG r0); clear REG. destruct (Pos.eq_dec r r0); simpl; intuition (subst; eauto). (* Istore *) - simpl. wlp_bind next NEXT. wlp_simplify. inv H. inv H0. eapply hsist_set_local_correct_dyn; eauto. + admit. (** TODO - port hslocal_set_smem_correct *) + unfold sok_local; simpl; intuition. (* Icall *) - admit. (* Itailcall *) - admit. (* Ibuiltin *) - admit. (* Icond *) - admit. (* Ijumptable *) - admit. (* Ireturn *) - admit. Admitted. (* PROOF from RTLpathSE_impl.v destruct i; simpl; intros STEP1 STEP2; inversion_clear STEP1; inversion_clear STEP2; discriminate || (intro REF; eauto). - (* Iop *) eapply hsist_set_local_correct_dyn; eauto. + eapply hslocal_set_sreg_correct; eauto. simpl; intros. erewrite seval_list_sval_refines; eauto. erewrite seval_smem_refines; eauto. + unfold sok_local; simpl; intros (PRE & MEM & REG). intuition. generalize (REG r0); clear REG. destruct (Pos.eq_dec r r0); simpl; intuition (subst; eauto). - (* Iload *) eapply hsist_set_local_correct_dyn; eauto. + eapply hslocal_set_sreg_correct; eauto. simpl; intros. erewrite seval_list_sval_refines; eauto. erewrite seval_smem_refines; eauto. + unfold sok_local; simpl; intros (PRE & MEM & REG). intuition. generalize (REG r0); clear REG. destruct (Pos.eq_dec r r0); simpl; intuition (subst; eauto). - (* Istore *) eapply hsist_set_local_correct_dyn; eauto. + eapply hslocal_set_mem_correct; eauto. * simpl. simplify_SOME x. * intros. simpl. erewrite seval_list_sval_refines; eauto. erewrite seval_smem_refines; eauto. erewrite seval_sval_refines; eauto. + unfold sok_local; simpl; intuition. - (* Icond *) destruct REF as (EXREF & LREF & NEST). split. + constructor; simpl; auto. constructor; simpl; auto. intros; erewrite seval_condition_refines; eauto. unfold seval_condition. erewrite seval_list_sval_refines; eauto. + split; simpl; auto. destruct NEST as [|st0 se lse TOP NEST]; econstructor; simpl; auto; constructor; auto. Qed. *) 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. (** * init_hsistate_correct_stat : OK * init_hsistate_correct_dyn : OK * hsexec_final_correct : OK * hsiexec_inst_correct_dyn : TODO * hsiexec_path_correct_dyn : TODO * hfinal_refines_snone : OK *) (* Local Hint Resolve init_hsistate_correct_stat init_hsistate_correct_dyn hsexec_final_correct hsiexec_inst_correct_dyn hsiexec_path_correct_dyn hfinal_refines_snone: core. *) Lemma hsexec_correct f pc: WHEN hsexec f pc ~> hst THEN exists st, sexec f pc = Some st /\ hsstate_refines hst st. Proof. Admitted. (* unfold hsexec. intro. explore_hyp. unfold sexec. rewrite EQ. exploit hsiexec_path_correct_stat; eauto. intros (st0 & SPATH & REF0). generalize REF0; intros (PC0 & XREF0). rewrite SPATH. erewrite <- PC0. rewrite EQ1. destruct (hsiexec_inst i h) eqn:HINST. + exploit hsiexec_inst_correct_stat; eauto. intros (st1 & EQ2 & PC2 & REF2). - split; eauto. - rewrite EQ2. repeat (econstructor; simpl; eauto). + erewrite hsiexec_inst_correct_None; eauto. repeat (econstructor; simpl; eauto). unfold hfinal_refines. simpl; eauto. Qed. *) End CanonBuilding. 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 *) DO hst1 <~ hsexec f pc1;; DO hst2 <~ hsexec tf pc2;; (* comparing the executions *) hsstate_simu_check dm f 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 simu_check_single. wlp_bind hC_sval HSVAL. wlp_bind hC_list_hsval HLSVAL. wlp_bind hC_hsmem HSMEM. wlp_bind hst1 HSEXEC1. wlp_bind hst2 HSEXEC2. wlp_intro u HSIMU. unfold sexec_simu. intros st1 SEXEC. explore. assert (TODO1: forall hs rhsv, hC hC_sval hs ~~> rhsv -> hsval_proj (hdata hs) = hsval_proj rhsv) by admit. assert (TODO2: forall hs rhsv, hC hC_list_hsval hs ~~> rhsv -> hsval_list_proj (hdata hs) = hsval_list_proj rhsv) by admit. assert (TODO3: forall hs rhsv, hC hC_hsmem hs ~~> rhsv -> hsmem_proj (hdata hs) = hsmem_proj rhsv) by admit. exploit hsexec_correct; eauto. intros (st2 & SEXEC2 & REF2). exploit hsexec_correct. 4: eapply HSEXEC1. all: eauto. intros (st0 & SEXEC1 & REF1). rewrite SEXEC1 in SEXEC. inv SEXEC. eexists. split; eauto. intros ctx. eapply hsstate_simu_check_correct in HSIMU; eauto. eapply hsstate_simu_core_correct; eauto. Admitted. 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);; println("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.