diff options
Diffstat (limited to 'scheduling/BTL_SEimpl.v')
| -rw-r--r-- | scheduling/BTL_SEimpl.v | 1508 |
1 files changed, 1508 insertions, 0 deletions
diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v new file mode 100644 index 00000000..65d16d01 --- /dev/null +++ b/scheduling/BTL_SEimpl.v @@ -0,0 +1,1508 @@ +Require Import Coqlib AST Maps. +Require Import Op Registers. +Require Import RTL BTL Errors. +Require Import BTL_SEsimuref BTL_SEtheory OptionMonad. +Require Import BTL_SEsimplify. + +Require Import Impure.ImpHCons. +Import Notations. +Import HConsing. + +Local Open Scope option_monad_scope. +Local Open Scope impure. + +Import ListNotations. +Local Open Scope list_scope. + +(** Tactics *) + +Ltac simplify_SOME x := repeat inversion_SOME x; try_simplify_someHyps. + +(** Notations to make lemmas more readable *) +Notation "'sval_refines' ctx sv1 sv2" := (eval_sval ctx sv1 = eval_sval ctx sv2) + (only parsing, at level 0, ctx at next level, sv1 at next level, sv2 at next level): hse. + +Local Open Scope hse. + +Notation "'list_sval_refines' ctx lsv1 lsv2" := (eval_list_sval ctx lsv1 = eval_list_sval ctx lsv2) + (only parsing, at level 0, ctx at next level, lsv1 at next level, lsv2 at next level): hse. + +Notation "'smem_refines' ctx sm1 sm2" := (eval_smem ctx sm1 = eval_smem ctx sm2) + (only parsing, at level 0, ctx at next level, sm1 at next level, sm2 at next level): hse. + +(** Debug printer *) +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 sval_get_hid (sv: sval): hashcode := + match sv with + | Sundef hid => hid + | Sinput _ hid => hid + | Sop _ _ hid => hid + | Sload _ _ _ _ _ hid => hid + end. + +Definition list_sval_get_hid (lsv: list_sval): hashcode := + match lsv with + | Snil hid => hid + | Scons _ _ hid => hid + end. + +Definition smem_get_hid (sm: smem): hashcode := + match sm with + | Sinit hid => hid + | Sstore _ _ _ _ _ hid => hid + end. + +Definition sval_set_hid (sv: sval) (hid: hashcode): sval := + match sv with + | Sundef _ => Sundef hid + | Sinput r _ => Sinput r hid + | Sop o lsv _ => Sop o lsv hid + | Sload sm trap chunk addr lsv _ => Sload sm trap chunk addr lsv hid + end. + +Definition list_sval_set_hid (lsv: list_sval) (hid: hashcode): list_sval := + match lsv with + | Snil _ => Snil hid + | Scons sv lsv _ => Scons sv lsv hid + end. + +Definition smem_set_hid (sm: smem) (hid: hashcode): smem := + match sm with + | Sinit _ => Sinit hid + | Sstore sm chunk addr lsv srce _ => Sstore sm chunk addr lsv srce hid + end. + +Lemma sval_set_hid_correct ctx x y: + sval_set_hid x unknown_hid = sval_set_hid y unknown_hid -> + sval_refines ctx x y. +Proof. + destruct x, y; intro H; inversion H; subst; simpl; auto. +Qed. +Local Hint Resolve sval_set_hid_correct: core. + +Lemma list_sval_set_hid_correct ctx x y: + list_sval_set_hid x unknown_hid = list_sval_set_hid y unknown_hid -> + list_sval_refines ctx x y. +Proof. + destruct x, y; intro H; inversion H; subst; simpl; auto. +Qed. +Local Hint Resolve list_sval_set_hid_correct: core. + +Lemma smem_set_hid_correct ctx x y: + smem_set_hid x unknown_hid = smem_set_hid y unknown_hid -> + smem_refines ctx x y. +Proof. + destruct x, y; intro H; inversion H; subst; simpl; auto. +Qed. +Local Hint Resolve smem_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 sval_hash_eq (sv1 sv2: sval): ?? bool := + match sv1, sv2 with + | Sinput r1 _, Sinput r2 _ => struct_eq r1 r2 (* NB: really need a struct_eq here ? *) + | Sop op1 lsv1 _, Sop 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 + | Sload sm1 trap1 chk1 addr1 lsv1 _, Sload 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 sval_hash_eq_correct x y: + WHEN sval_hash_eq x y ~> b THEN + b = true -> sval_set_hid x unknown_hid = sval_set_hid y unknown_hid. +Proof. + destruct x, y; wlp_simplify; try (rewrite !and_true_split in *); intuition; subst; try congruence. +Qed. +Global Opaque sval_hash_eq. +Local Hint Resolve sval_hash_eq_correct: wlp. + +Definition list_sval_hash_eq (lsv1 lsv2: list_sval): ?? bool := + match lsv1, lsv2 with + | Snil _, Snil _ => RET true + | Scons sv1 lsv1' _, Scons sv2 lsv2' _ => + DO b <~ phys_eq lsv1' lsv2';; + if b + then phys_eq sv1 sv2 + else RET false + | _,_ => RET false + end. + +Lemma list_sval_hash_eq_correct x y: + WHEN list_sval_hash_eq x y ~> b THEN + b = true -> list_sval_set_hid x unknown_hid = list_sval_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_sval_hash_eq. +Local Hint Resolve list_sval_hash_eq_correct: wlp. + +Definition smem_hash_eq (sm1 sm2: smem): ?? bool := + match sm1, sm2 with + | Sinit _, Sinit _ => RET true + | Sstore sm1 chk1 addr1 lsv1 sv1 _, Sstore 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 smem_hash_eq_correct x y: + WHEN smem_hash_eq x y ~> b THEN + b = true -> smem_set_hid x unknown_hid = smem_set_hid y unknown_hid. +Proof. + destruct x, y; wlp_simplify; try (rewrite !and_true_split in *); intuition; subst; try congruence. +Qed. +Global Opaque smem_hash_eq. +Local Hint Resolve smem_hash_eq_correct: wlp. + +Definition hSVAL: hashP sval := {| hash_eq := sval_hash_eq; get_hid:=sval_get_hid; set_hid:=sval_set_hid |}. +Definition hLSVAL: hashP list_sval := {| hash_eq := list_sval_hash_eq; get_hid:= list_sval_get_hid; set_hid:= list_sval_set_hid |}. +Definition hSMEM: hashP smem := {| hash_eq := smem_hash_eq; get_hid:= smem_get_hid; set_hid:= smem_set_hid |}. + +Program Definition mk_hash_params: Dict.hash_params sval := + {| + Dict.test_eq := phys_eq; + Dict.hashing := fun (sv: sval) => RET (sval_get_hid sv); + Dict.log := fun sv => + DO sv_name <~ string_of_hashcode (sval_get_hid sv);; + println ("unexpected undef behavior of hashcode:" +; (CamlStr sv_name)) |}. +Obligation 1. + wlp_simplify. +Qed. + +(** * Implementation of symbolic execution *) +Section CanonBuilding. + +Variable hC_sval: hashinfo sval -> ?? sval. + +Hypothesis hC_sval_correct: forall s, + WHEN hC_sval s ~> s' THEN forall ctx, + sval_refines ctx (hdata s) s'. + +Variable hC_list_sval: hashinfo list_sval -> ?? list_sval. +Hypothesis hC_list_sval_correct: forall lh, + WHEN hC_list_sval lh ~> lh' THEN forall ctx, + list_sval_refines ctx (hdata lh) lh'. + +Variable hC_smem: hashinfo smem -> ?? smem. +Hypothesis hC_smem_correct: forall hm, + WHEN hC_smem hm ~> hm' THEN forall ctx, + smem_refines ctx (hdata hm) hm'. + +(* First, we wrap constructors for hashed values !*) + +Definition reg_hcode := 1. +Definition op_hcode := 2. +Definition load_hcode := 3. +Definition undef_code := 4. + +Definition hSinput_hcodes (r: reg) := + DO hc <~ hash reg_hcode;; + DO sv <~ hash r;; + RET [hc;sv]. +Extraction Inline hSinput_hcodes. + +Definition hSinput (r:reg): ?? sval := + DO sv <~ hSinput_hcodes r;; + hC_sval {| hdata:=Sinput r unknown_hid; hcodes :=sv; |}. + +Lemma hSinput_correct r: + WHEN hSinput r ~> sv THEN forall ctx, + sval_refines ctx sv (Sinput r unknown_hid). +Proof. + wlp_simplify. +Qed. +Global Opaque hSinput. +Local Hint Resolve hSinput_correct: wlp. + +Definition hSop_hcodes (op:operation) (lsv: list_sval) := + DO hc <~ hash op_hcode;; + DO sv <~ hash op;; + RET [hc;sv;list_sval_get_hid lsv]. +Extraction Inline hSop_hcodes. + +Definition hSop (op:operation) (lsv: list_sval): ?? sval := + DO sv <~ hSop_hcodes op lsv;; + hC_sval {| hdata:=Sop op lsv unknown_hid; hcodes :=sv |}. + +Lemma hSop_fSop_correct op lsv: + WHEN hSop op lsv ~> sv THEN forall ctx, + sval_refines ctx sv (fSop op lsv). +Proof. + wlp_simplify. +Qed. +Global Opaque hSop. +Local Hint Resolve hSop_fSop_correct: wlp_raw. + +Lemma hSop_correct op lsv1: + WHEN hSop op lsv1 ~> sv THEN forall ctx lsv2 + (LR: list_sval_refines ctx lsv1 lsv2), + sval_refines ctx sv (Sop op lsv2 unknown_hid). +Proof. + wlp_xsimplify ltac:(intuition eauto with wlp wlp_raw). + rewrite <- LR. erewrite H; eauto. +Qed. +Local Hint Resolve hSop_correct: wlp. + +Definition hSload_hcodes (sm: smem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval):= + DO hc <~ hash load_hcode;; + DO sv1 <~ hash trap;; + DO sv2 <~ hash chunk;; + DO sv3 <~ hash addr;; + RET [hc; smem_get_hid sm; sv1; sv2; sv3; list_sval_get_hid lsv]. +Extraction Inline hSload_hcodes. + +Definition hSload (sm: smem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval): ?? sval := + DO sv <~ hSload_hcodes sm trap chunk addr lsv;; + hC_sval {| hdata := Sload sm trap chunk addr lsv unknown_hid; hcodes := sv |}. + +Lemma hSload_correct sm1 trap chunk addr lsv1: + WHEN hSload sm1 trap chunk addr lsv1 ~> sv THEN forall ctx lsv2 sm2 + (LR: list_sval_refines ctx lsv1 lsv2) + (MR: smem_refines ctx sm1 sm2), + sval_refines ctx sv (Sload sm2 trap chunk addr lsv2 unknown_hid). +Proof. + wlp_simplify. + rewrite <- LR, <- MR. + auto. +Qed. +Global Opaque hSload. +Local Hint Resolve hSload_correct: wlp. + +Definition hSundef_hcodes := + DO hc <~ hash undef_code;; + RET [hc]. +Extraction Inline hSundef_hcodes. + +Definition hSundef : ?? sval := + DO sv <~ hSundef_hcodes;; + hC_sval {| hdata:=Sundef unknown_hid; hcodes :=sv; |}. + +Lemma hSundef_correct: + WHEN hSundef ~> sv THEN forall ctx, + sval_refines ctx sv (Sundef unknown_hid). +Proof. + wlp_simplify. +Qed. +Global Opaque hSundef. +Local Hint Resolve hSundef_correct: wlp. + +Definition hSnil (_: unit): ?? list_sval := + hC_list_sval {| hdata := Snil unknown_hid; hcodes := nil |}. + +Lemma hSnil_correct: + WHEN hSnil() ~> sv THEN forall ctx, + list_sval_refines ctx sv (Snil unknown_hid). +Proof. + wlp_simplify. +Qed. +Global Opaque hSnil. +Local Hint Resolve hSnil_correct: wlp. + +Definition hScons (sv: sval) (lsv: list_sval): ?? list_sval := + hC_list_sval {| hdata := Scons sv lsv unknown_hid; hcodes := [sval_get_hid sv; list_sval_get_hid lsv] |}. + +Lemma hScons_correct sv1 lsv1: + WHEN hScons sv1 lsv1 ~> lsv1' THEN forall ctx sv2 lsv2 + (VR: sval_refines ctx sv1 sv2) + (LR: list_sval_refines ctx lsv1 lsv2), + list_sval_refines ctx lsv1' (Scons sv2 lsv2 unknown_hid). +Proof. + wlp_simplify. + rewrite <- VR, <- LR. + auto. +Qed. +Global Opaque hScons. +Local Hint Resolve hScons_correct: wlp. + +Definition hSinit (_: unit): ?? smem := + hC_smem {| hdata := Sinit unknown_hid; hcodes := nil |}. + +Lemma hSinit_correct: + WHEN hSinit() ~> hm THEN forall ctx, + smem_refines ctx hm (Sinit unknown_hid). +Proof. + wlp_simplify. +Qed. +Global Opaque hSinit. +Local Hint Resolve hSinit_correct: wlp. + +Definition hSstore_hcodes (sm: smem) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval) (srce: sval):= + DO sv1 <~ hash chunk;; + DO sv2 <~ hash addr;; + RET [smem_get_hid sm; sv1; sv2; list_sval_get_hid lsv; sval_get_hid srce]. +Extraction Inline hSstore_hcodes. + +Definition hSstore (sm: smem) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval) (srce: sval): ?? smem := + DO sv <~ hSstore_hcodes sm chunk addr lsv srce;; + hC_smem {| hdata := Sstore sm chunk addr lsv srce unknown_hid; hcodes := sv |}. + +Lemma hSstore_correct sm1 chunk addr lsv1 sv1: + WHEN hSstore sm1 chunk addr lsv1 sv1 ~> sm1' THEN forall ctx lsv2 sm2 sv2 + (LR: list_sval_refines ctx lsv1 lsv2) + (MR: smem_refines ctx sm1 sm2) + (VR: sval_refines ctx sv1 sv2), + smem_refines ctx sm1' (Sstore sm2 chunk addr lsv2 sv2 unknown_hid). +Proof. + wlp_simplify. + rewrite <- LR, <- MR, <- VR. + auto. +Qed. +Global Opaque hSstore. +Local Hint Resolve hSstore_correct: wlp. + +Definition hrs_sreg_get (hrs: ristate) r: ?? sval := + match PTree.get r hrs with + | None => if ris_input_init hrs then hSinput r else hSundef + | Some sv => RET sv + end. + +Lemma hrs_sreg_get_correct hrs r: + WHEN hrs_sreg_get hrs r ~> sv THEN forall ctx (f: reg -> sval) + (RR: forall r, sval_refines ctx (hrs r) (f r)), + sval_refines ctx sv (f r). +Proof. + unfold ris_sreg_get; wlp_simplify; rewrite <- RR; rewrite H; auto; + rewrite H0, H1; simpl; auto. +Qed. +Global Opaque hrs_sreg_get. +Local Hint Resolve hrs_sreg_get_correct: wlp. + +Fixpoint hlist_args (hrs: ristate) (l: list reg): ?? list_sval := + match l with + | nil => hSnil() + | r::l => + DO v <~ hrs_sreg_get hrs r;; + DO lsv <~ hlist_args hrs l;; + hScons v lsv + end. + +Lemma hlist_args_correct hrs l: + WHEN hlist_args hrs l ~> lsv THEN forall ctx (f: reg -> sval) + (RR: forall r, sval_refines ctx (hrs r) (f r)), + list_sval_refines ctx lsv (list_sval_inj (List.map f l)). +Proof. + induction l; wlp_simplify. +Qed. +Global Opaque hlist_args. +Local Hint Resolve hlist_args_correct: wlp. + +(** Convert a "fake" hash-consed term into a "real" hash-consed term *) + +Fixpoint fsval_proj sv: ?? sval := + match sv with + | Sundef hc => + DO b <~ phys_eq hc unknown_hid;; + if b then hSundef else RET sv + | Sinput r hc => + DO b <~ phys_eq hc unknown_hid;; + if b then hSinput r (* was not yet really hash-consed *) + else RET sv (* already hash-consed *) + | Sop op hl hc => + DO b <~ phys_eq hc unknown_hid;; + if b then (* was not yet really hash-consed *) + DO hl' <~ fsval_list_proj hl;; + hSop op hl' + else RET sv (* already hash-consed *) + | Sload hm t chk addr hl _ => RET sv (* FIXME TODO gourdinl ? *) + end +with fsval_list_proj sl: ?? list_sval := + match sl with + | Snil hc => + DO b <~ phys_eq hc unknown_hid;; + if b then hSnil() (* was not yet really hash-consed *) + else RET sl (* already hash-consed *) + | Scons sv hl hc => + DO b <~ phys_eq hc unknown_hid;; + if b then (* was not yet really hash-consed *) + DO sv' <~ fsval_proj sv;; + DO hl' <~ fsval_list_proj hl;; + hScons sv' hl' + else RET sl (* already hash-consed *) + end. + +Lemma fsval_proj_correct sv: + WHEN fsval_proj sv ~> sv' THEN forall ctx, + sval_refines ctx sv sv'. +Proof. + induction sv using sval_mut + with (P0 := fun lsv => + WHEN fsval_list_proj lsv ~> lsv' THEN forall ctx, + eval_list_sval ctx lsv = eval_list_sval ctx lsv') + (P1 := fun sm => True); try (wlp_simplify; tauto). + - wlp_xsimplify ltac:(intuition eauto with wlp_raw wlp). + rewrite H, H0; auto. + - wlp_simplify; erewrite H0, H1; eauto. +Qed. +Global Opaque fsval_proj. +Local Hint Resolve fsval_proj_correct: wlp. + +Lemma fsval_list_proj_correct lsv: + WHEN fsval_list_proj lsv ~> lsv' THEN forall ctx, + list_sval_refines ctx lsv lsv'. +Proof. + induction lsv; wlp_simplify. + erewrite H0, H1; eauto. +Qed. +Global Opaque fsval_list_proj. +Local Hint Resolve fsval_list_proj_correct: wlp. + +(** ** Assignment of memory *) + +Definition hrexec_store chunk addr args src hrs: ?? ristate := + DO hargs <~ hlist_args hrs args;; + DO hsrc <~ hrs_sreg_get hrs src;; + DO hm <~ hSstore hrs chunk addr hargs hsrc;; + RET (rset_smem hm hrs). + +Lemma hrexec_store_correct chunk addr args src hrs: + WHEN hrexec_store chunk addr args src hrs ~> hrs' THEN forall ctx sis + (REF: ris_refines ctx hrs sis), + ris_refines ctx hrs' (sexec_store chunk addr args src sis). +Proof. + wlp_simplify. + eapply rset_mem_correct; simpl; eauto. + - intros X; erewrite H1; eauto. + rewrite X. simplify_SOME z. + - intros X; inversion REF. + erewrite H1; eauto. +Qed. +Local Hint Resolve hrexec_store_correct: wlp. + +(** ** Assignment of registers *) + +(** locally new symbolic values during symbolic execution *) +Inductive root_sval: Type := +| Rop (op: operation) +| Rload (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) +. + +Definition root_apply (rsv: root_sval) (lr: list reg) (st: sistate): sval := + let lsv := list_sval_inj (List.map (si_sreg st) lr) in + let sm := si_smem st in + match rsv with + | Rop op => fSop op lsv + | Rload trap chunk addr => fSload sm trap chunk addr lsv + end. +Coercion root_apply: root_sval >-> Funclass. + +Definition root_happly (rsv: root_sval) (lr: list reg) (hrs: ristate): ?? sval := + DO lsv <~ hlist_args hrs lr;; + match rsv with + | Rop op => hSop op lsv + | Rload trap chunk addr => hSload hrs trap chunk addr lsv + end. + +Lemma root_happly_correct (rsv: root_sval) lr hrs: + WHEN root_happly rsv lr hrs ~> sv THEN forall ctx sis + (REF: ris_refines ctx hrs sis) + (OK: ris_ok ctx hrs), + sval_refines ctx sv (rsv lr sis). +Proof. + unfold root_apply, root_happly; destruct rsv; wlp_simplify; inv REF; + erewrite H0, H; eauto. +Qed. +Global Opaque root_happly. +Hint Resolve root_happly_correct: wlp. + +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. repeat autodestruct; simpl; intuition (try congruence). +Qed. + +Lemma eval_list_sval_length ctx (f: reg -> sval) (l:list reg): + forall l', eval_list_sval ctx (list_sval_inj (List.map f l)) = Some l' -> + Datatypes.length l = Datatypes.length l'. +Proof. + induction l. + - simpl. intros. inv H. reflexivity. + - simpl. intros. destruct (eval_sval _ _); [|discriminate]. + destruct (eval_list_sval _ _) eqn:SLS; [|discriminate]. inv H. simpl. + erewrite IHl; eauto. +Qed. + +Lemma may_trap_correct ctx (rsv: root_sval) (lr: list reg) st: + may_trap rsv lr = false -> + eval_list_sval ctx (list_sval_inj (List.map (si_sreg st) lr)) <> None -> + eval_smem ctx (si_smem st) <> None -> + eval_sval ctx (rsv lr st) <> None. +Proof. + destruct rsv; simpl; try congruence. + - rewrite lazy_orb_negb_false. intros (TRAP1 & LEN) OK1 OK2. + autodestruct; try congruence. intros. + eapply is_trapping_op_sound; eauto. + erewrite <- eval_list_sval_length; eauto. + apply Nat.eqb_eq in LEN. + assumption. + - intros X OK1 OK2. + repeat autodestruct; try congruence. +Qed. + +(** simplify a symbolic value before assignment to a register *) +Definition simplify (rsv: root_sval) (lr: list reg) (hrs: ristate): ?? sval := + match rsv with + | Rop op => + match is_move_operation op lr with + | Some arg => hrs_sreg_get hrs arg (* optimization of Omove *) + | None => + match target_op_simplify op lr hrs with + | Some fsv => fsval_proj fsv + | None => + DO lhsv <~ hlist_args hrs lr;; + hSop op lhsv + end + end + | Rload _ chunk addr => + DO lsv <~ hlist_args hrs lr;; + hSload hrs NOTRAP chunk addr lsv + end. + +Lemma simplify_correct rsv lr hrs: + WHEN simplify rsv lr hrs ~> sv THEN forall ctx sis + (REF: ris_refines ctx hrs sis) + (OK0: ris_ok ctx hrs) + (OK1: eval_sval ctx (rsv lr sis) <> None), + sval_refines ctx sv (rsv lr sis). +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 *. inv REF. + simplify_SOME z; erewrite H; eauto. } + destruct (target_op_simplify _ _ _) eqn: Htarget_op_simp; wlp_simplify. + { destruct (eval_list_sval _ _) eqn: OKlist; try congruence. + rewrite <- H; exploit target_op_simplify_correct; eauto. } + inv REF; clear Htarget_op_simp. + intuition eauto. + - (* Rload *) + destruct trap; wlp_simplify; inv REF. + + erewrite H0; eauto. + erewrite H; [|eapply REG_EQ; eauto]. + erewrite MEM_EQ; eauto. + repeat simplify_SOME z. + * destruct (Memory.Mem.loadv _ _ _); try congruence. + * rewrite H1 in OK1; congruence. + + erewrite H0; eauto. +Qed. +Global Opaque simplify. +Local Hint Resolve simplify_correct: wlp. + +Definition red_PTree_set (r: reg) (sv: sval) (hrs: ristate): PTree.t sval := + match (ris_input_init hrs), sv with + | true, Sinput r' _ => + if Pos.eq_dec r r' + then PTree.remove r' hrs + else PTree.set r sv hrs + | false, Sundef _ => + PTree.remove r hrs + | _, _ => PTree.set r sv hrs + end. + +Lemma red_PTree_set_correct (r r0:reg) sv (hrs: ristate) ctx: + sval_refines ctx ((ris_sreg_set hrs (red_PTree_set r sv hrs)) r0) ((ris_sreg_set hrs (PTree.set r sv hrs)) r0). +Proof. + unfold red_PTree_set, ris_sreg_set, ris_sreg_get; simpl. + destruct (ris_input_init hrs) eqn:Hinit, sv; simpl; auto. + 1: destruct (Pos.eq_dec r r1); auto; subst; + rename r1 into r. + all: destruct (Pos.eq_dec r r0); 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) ctx hrs sis sv1 sv2: + ris_refines ctx hrs sis -> + sval_refines ctx sv1 sv2 -> + ris_ok ctx hrs -> + sval_refines ctx (ris_sreg_set hrs (red_PTree_set r sv1 hrs) r0) (if Pos.eq_dec r r0 then sv2 else si_sreg sis r0). +Proof. + intros REF SREF OK; rewrite red_PTree_set_correct. + unfold ris_sreg_set, ris_sreg_get. + destruct (Pos.eq_dec r r0). + - subst; simpl. rewrite PTree.gss; simpl; auto. + - inv REF; simpl. rewrite PTree.gso; simpl; eauto. +Qed. + +Definition cbranch_expanse (prev: ristate) (cond: condition) (args: list reg): ?? (condition * list_sval) := + 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 hrs c l: + WHEN cbranch_expanse hrs c l ~> r THEN forall ctx sis + (REF : ris_refines ctx hrs sis) + (OK: ris_ok ctx hrs), + eval_scondition ctx (fst r) (snd r) = + eval_scondition ctx c (list_sval_inj (map (si_sreg sis) l)). +Proof. + unfold cbranch_expanse. + destruct (target_cbranch_expanse _ _ _) eqn: TARGET; wlp_simplify; + unfold eval_scondition; try erewrite <- H; inversion REF; 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 some_or_fail {A} (o: option A) (msg: pstring): ?? A := + match o with + | Some x => RET x + | None => FAILWITH msg + end. + +Definition hrs_init: ?? ristate + := DO hm <~ hSinit ();; + RET {| ris_smem := hm; ris_input_init := true; ok_rsval := nil; ris_sreg := PTree.empty _ |}. + +Lemma hrs_init_correct: + WHEN hrs_init ~> hrs THEN + forall ctx, ris_refines ctx hrs sis_init. +Proof. + unfold hrs_init, sis_init; wlp_simplify. + econstructor; simpl in *; eauto. + + split; destruct 1; econstructor; simpl in *; + try rewrite H; try congruence; trivial. + + destruct 1; simpl in *. unfold ris_sreg_get; simpl. + intros; rewrite PTree.gempty; eauto. +Qed. +Local Hint Resolve hrs_init_correct: wlp. +Global Opaque hrs_init. + +Definition hrs_sreg_set r lr rsv (hrs: ristate): ?? ristate := + DO ok_lsv <~ + (if may_trap rsv lr + then DO sv <~ root_happly rsv lr hrs;; + XDEBUG sv (fun sv => DO sv_name <~ string_of_hashcode (sval_get_hid sv);; RET ("-- insert undef behavior of hashcode:" +; (CamlStr sv_name))%string);; + RET (sv::(ok_rsval hrs)) + else RET (ok_rsval hrs));; + DO simp <~ simplify rsv lr hrs;; + RET {| ris_smem := hrs.(ris_smem); + ris_input_init := hrs.(ris_input_init); + ok_rsval := ok_lsv; + ris_sreg:= red_PTree_set r simp hrs |}. + +Lemma ok_hrset_sreg (rsv:root_sval) ctx (st: sistate) r lr: + si_ok ctx (set_sreg r (rsv lr st) st) + <-> (si_ok ctx st /\ eval_sval ctx (rsv lr st) <> None). +Proof. + unfold set_sreg; simpl; split. + - intros. destruct H as [[OK_SV OK_PRE] OK_SMEM OK_SREG]; simpl in *. + repeat (split; try tauto). + + intros r0; generalize (OK_SREG r0); clear OK_SREG; destruct (Pos.eq_dec r r0); try congruence. + + generalize (OK_SREG r); clear OK_SREG; destruct (Pos.eq_dec r r); try congruence. + - intros (OK & SEVAL). inv OK. + repeat (split; try tauto; eauto). + intros r0; destruct (Pos.eq_dec r r0) eqn:Heq; simpl; + rewrite Heq; eauto. +Qed. + +Lemma eval_list_sval_inj_not_none ctx st: forall l, + (forall r, List.In r l -> eval_sval ctx (si_sreg st r) = None -> False) -> + eval_list_sval ctx (list_sval_inj (map (si_sreg st) l)) = None -> False. +Proof. + induction l. + - intuition discriminate. + - intros ALLR. simpl. + inversion_SOME v. + + intro SVAL. inversion_SOME lv; [discriminate|]. + assert (forall r : reg, In r l -> eval_sval ctx (si_sreg st r) = None -> False). + { intros r INR. eapply ALLR. right. assumption. } + intro SVALLIST. intro. eapply IHl; eauto. + + intros. exploit (ALLR a); simpl; eauto. +Qed. + +Lemma hrs_sreg_set_correct r lr rsv hrs: + WHEN hrs_sreg_set r lr rsv hrs ~> hrs' THEN forall ctx sis + (REF: ris_refines ctx hrs sis), + ris_refines ctx hrs' (set_sreg r (rsv lr sis) sis). +Proof. + wlp_simplify; inversion REF. + - (* may_trap -> true *) + assert (X: si_ok ctx (set_sreg r (rsv lr sis) sis) <-> + ris_ok ctx {| ris_smem := hrs; + ris_input_init := ris_input_init hrs; + ok_rsval := exta :: ok_rsval hrs; + ris_sreg := red_PTree_set r exta0 hrs |}). + { + rewrite ok_hrset_sreg, OK_EQUIV. + split. + + intros (ROK & SEVAL); inv ROK. + assert (ROK: ris_ok ctx hrs) by (econstructor; eauto). + econstructor; eauto; simpl. + intuition (subst; eauto). + erewrite H0 in *; eauto. + + intros (OK_RMEM & OK_RREG); simpl in *. + assert (ROK: ris_ok ctx hrs) by (econstructor; eauto). + erewrite <- H0 in *; eauto. } + split; auto; rewrite <- X, ok_hrset_sreg. + + intuition eauto. + + intros (SOK & SEVAL) r0. + rewrite ris_sreg_set_access. + erewrite red_PTree_set_refines; intuition eauto. + - (* may_trap -> false *) + assert (X: si_ok ctx (set_sreg r (rsv lr sis) sis) <-> + ris_ok ctx {| ris_smem := hrs; + ris_input_init := ris_input_init hrs; + ok_rsval := ok_rsval hrs; + ris_sreg := red_PTree_set r exta hrs |}). + { + rewrite ok_hrset_sreg, OK_EQUIV. + split. + + intros (ROK & SEVAL); inv ROK. + econstructor; eauto. + + intros (OK_RMEM & OK_RREG). + assert (ROK: ris_ok ctx hrs) by (econstructor; eauto). + split; auto. + intros SNONE; exploit may_trap_correct; eauto. + * intros LNONE; eapply eval_list_sval_inj_not_none; eauto. + assert (SOK: si_ok ctx sis) by intuition. + inv SOK. intuition eauto. + * rewrite <- MEM_EQ; auto. } + split; auto; rewrite <- X, ok_hrset_sreg. + + intuition eauto. + + intros (SOK & SEVAL) r0. + rewrite ris_sreg_set_access. + erewrite red_PTree_set_refines; intuition eauto. +Qed. + +Lemma hrs_ok_op_okpreserv ctx op args dest hrs: + WHEN hrs_sreg_set dest args (Rop op) hrs ~> rst THEN + ris_ok ctx rst -> ris_ok ctx hrs. +Proof. + wlp_simplify; inv H2 || inv H1; + simpl in *; econstructor; eauto. +Qed. + +Lemma hrs_ok_load_okpreserv ctx chunk addr args dest hrs trap: + WHEN hrs_sreg_set dest args (Rload trap chunk addr) hrs ~> rst THEN + ris_ok ctx rst -> ris_ok ctx hrs. +Proof. + wlp_simplify; inv H2 || inv H1; + simpl in *; econstructor; eauto. +Qed. + +Lemma hrs_ok_store_okpreserv ctx chunk addr args src hrs: + WHEN hrexec_store chunk addr args src hrs ~> rst THEN + ris_ok ctx rst -> ris_ok ctx hrs. +Proof. + unfold hrexec_store; wlp_simplify. + generalize H2. erewrite ok_rset_mem; intuition. + specialize H1 with (sm2 := hrs). + erewrite H1; eauto. rewrite H3. repeat autodestruct. +Qed. + +Global Opaque hrs_sreg_set hrexec_store. +Local Hint Resolve hrs_sreg_set_correct: wlp. + +(* transfer *) + +Lemma ok_hrset_red_sreg ctx r rsv hrs: + ris_ok ctx (ris_sreg_set hrs (red_PTree_set r rsv hrs)) + <-> (ris_ok ctx hrs). +Proof. + split; destruct 1; econstructor; simpl in *; eauto. +Qed. + +Fixpoint transfer_hrs (inputs: list reg) (hrs: ristate): ?? ristate := + match inputs with + | nil => RET {| ris_smem := hrs.(ris_smem); + ris_input_init := false; + ok_rsval := hrs.(ok_rsval); + ris_sreg:= PTree.empty _ + |} + | r::l => + DO hrs' <~ transfer_hrs l hrs;; + DO sv <~ hrs_sreg_get hrs r;; + RET (ris_sreg_set hrs' (red_PTree_set r sv hrs')) + end. + +Lemma ok_transfer_hrs ctx inputs hrs: + WHEN transfer_hrs inputs hrs ~> hrs' THEN + ris_ok ctx hrs' + <-> (ris_ok ctx hrs). +Proof. + induction inputs as [|r l]; simpl; wlp_simplify; + try (inv H; econstructor; eauto; fail). + + apply H0; rewrite <- ok_hrset_red_sreg; eauto. + + rewrite ok_hrset_red_sreg; auto. +Qed. +Local Hint Resolve ok_transfer_hrs: wlp. + +Lemma transfer_hrs_correct ctx inputs hrs sis: + WHEN transfer_hrs inputs hrs ~> hrs' THEN + ris_refines ctx hrs sis -> + ris_refines ctx hrs' (transfer_sis inputs sis). +Proof. + unfold transfer_hrs; + induction inputs as [|r l]; wlp_simplify. + inversion H. + + constructor. + * erewrite ok_transfer_sis; split; intros X. + - constructor; simpl; rewrite OK_EQUIV in X; inv X; assumption. + - rewrite OK_EQUIV; constructor; inv X; assumption. + * intros X; inv X; simpl; apply MEM_EQ; constructor; auto. + * simpl. unfold ris_sreg_get. + intros;rewrite PTree.gempty. simpl; auto. + + constructor. + * erewrite ok_hrset_red_sreg; eauto. + inv H2. rewrite <- OK_EQUIV. + erewrite !ok_transfer_sis; reflexivity. + * intros X; inversion X; simpl in *. + rewrite ok_hrset_red_sreg in X. + inv H2; rewrite MEM_EQ; auto. + * simpl; intros X r0. inversion H2. + rewrite ok_hrset_red_sreg in X. + erewrite red_PTree_set_refines; eauto. + destruct (Pos.eq_dec); auto. + inv H1. rewrite ok_transfer_sis in OK_EQUIV. + rewrite <- OK_EQUIV, OK_EQUIV0 in X. + erewrite H0; eauto. +Qed. + +Definition tr_hrs := poly_tr (fun f tbl or => transfer_hrs (Regset.elements (pre_inputs f tbl or))). + +Local Hint Resolve transfer_hrs_correct ok_transfer_hrs: core. +Local Opaque transfer_hrs. + +Lemma ok_tr_hrs ctx fi hrs: + WHEN tr_hrs (cf ctx) fi hrs ~> hrs' THEN + ris_ok ctx hrs' + <-> (ris_ok ctx hrs). +Proof. + destruct fi; simpl; eauto. +Qed. + +Lemma tr_hrs_correct ctx fi hrs sis: + WHEN tr_hrs (cf ctx) fi hrs ~> hrs' THEN + ris_refines ctx hrs sis -> + ris_refines ctx hrs' (tr_sis (cf ctx) fi sis). +Proof. + unfold tr_hrs, poly_tr; destruct fi; wlp_simplify; + exploit transfer_hrs_correct; eauto. + Unshelve. all: auto. +Qed. + +Fixpoint hbuiltin_arg (hrs: ristate) (arg : builtin_arg reg): ?? builtin_arg sval := + match arg with + | BA r => + DO v <~ hrs_sreg_get hrs 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 hrs ba1;; + DO v2 <~ hbuiltin_arg hrs ba2;; + RET (BA_splitlong v1 v2) + | BA_addptr ba1 ba2 => + DO v1 <~ hbuiltin_arg hrs ba1;; + DO v2 <~ hbuiltin_arg hrs ba2;; + RET (BA_addptr v1 v2) + end. + +Lemma hbuiltin_arg_correct hrs arg: + WHEN hbuiltin_arg hrs arg ~> hargs THEN forall ctx (f: reg -> sval) + (RR: forall r, sval_refines ctx (hrs r) (f r)), + eval_builtin_sval ctx hargs = eval_builtin_sval ctx (builtin_arg_map f arg). +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 hrs (args: list (builtin_arg reg)): ?? list (builtin_arg sval) := + match args with + | nil => RET nil + | a::l => + DO ha <~ hbuiltin_arg hrs a;; + DO hl <~ hbuiltin_args hrs l;; + RET (ha::hl) + end. + +Lemma hbuiltin_args_correct hrs args: + WHEN hbuiltin_args hrs args ~> hargs THEN forall ctx (f: reg -> sval) + (RR: forall r, sval_refines ctx (hrs r) (f r)), + bargs_refines ctx hargs (List.map (builtin_arg_map f) args). +Proof. + unfold bargs_refines; 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 hrs (ros: reg + ident): ?? (sval + ident) := + match ros with + | inl r => DO hr <~ hrs_sreg_get hrs r;; RET (inl hr) + | inr s => RET (inr s) + end. + +Lemma hsum_left_correct hrs ros: + WHEN hsum_left hrs ros ~> hsi THEN forall ctx (f: reg -> sval) + (RR: forall r, sval_refines ctx (hrs r) (f r)), + rsvident_refines ctx hsi (sum_left_map f ros). +Proof. + destruct ros; wlp_simplify; + econstructor; eauto. +Qed. +Global Opaque hsum_left. +Local Hint Resolve hsum_left_correct: wlp. + +(** * Symbolic execution of final step *) +Definition hrexec_final_sfv (i: final) hrs: ?? sfval := + match i with + | Bgoto pc => RET (Sgoto pc) + | Bcall sig ros args res pc => + DO svos <~ hsum_left hrs ros;; + DO sargs <~ hlist_args hrs args;; + RET (Scall sig svos sargs res pc) + | Btailcall sig ros args => + DO svos <~ hsum_left hrs ros;; + DO sargs <~ hlist_args hrs args;; + RET (Stailcall sig svos sargs) + | Bbuiltin ef args res pc => + DO sargs <~ hbuiltin_args hrs args;; + RET (Sbuiltin ef sargs res pc) + | Breturn or => + match or with + | Some r => DO hr <~ hrs_sreg_get hrs r;; RET (Sreturn (Some hr)) + | None => RET (Sreturn None) + end + | Bjumptable reg tbl => + DO sv <~ hrs_sreg_get hrs reg;; + RET (Sjumptable sv tbl) + end. + +Lemma hrexec_final_sfv_correct ctx fi hrs sis: + WHEN hrexec_final_sfv fi hrs ~> hrs' THEN forall + (REF: ris_refines ctx hrs sis) + (OK: ris_ok ctx hrs), + rfv_refines ctx hrs' (sexec_final_sfv fi sis). +Proof. + destruct fi; simpl; wlp_simplify; repeat econstructor; + try inversion REF; try erewrite H; eauto. +Qed. + +Fixpoint hrexec_rec f ib hrs (k: ristate -> ?? rstate): ?? rstate := + match ib with + | BF fin _ => + DO sfv <~ hrexec_final_sfv fin hrs;; + DO hrs' <~ tr_hrs f fin hrs;; + RET (Rfinal hrs' sfv) + (* basic instructions *) + | Bnop _ => k hrs + | Bop op args dst _ => + DO next <~ hrs_sreg_set dst args (Rop op) hrs;; + k next + | Bload trap chunk addr args dst _ => + DO next <~ hrs_sreg_set dst args (Rload trap chunk addr) hrs;; + k next + | Bstore chunk addr args src _ => + DO next <~ hrexec_store chunk addr args src hrs;; + k next + (* composed instructions *) + | Bseq ib1 ib2 => + hrexec_rec f ib1 hrs (fun hrs2 => hrexec_rec f ib2 hrs2 k) + | Bcond cond args ifso ifnot _ => + DO res <~ cbranch_expanse hrs cond args;; + let (cond, vargs) := res in + DO ifso <~ hrexec_rec f ifso hrs k;; + DO ifnot <~ hrexec_rec f ifnot hrs k;; + RET (Rcond cond vargs ifso ifnot) + end + . + +Definition hrexec f ib := + DO init <~ hrs_init;; + hrexec_rec f ib init (fun _ => RET Rabort). + +Local Hint Resolve exec_final_refpreserv ok_tr_hrs: core. +Local Hint Constructors rst_refines: core. + +Lemma hrexec_rec_correct1 ctx ib: + forall rk k + (CONTh: forall sis lsis sfv, get_soutcome ctx (k sis) = Some (sout lsis sfv) -> si_ok ctx lsis -> si_ok ctx sis) + (CONT: forall hrs sis lsis sfv st, + ris_refines ctx hrs sis -> + k sis = st -> + get_soutcome ctx (k sis) = Some (sout lsis sfv) -> + si_ok ctx lsis -> + WHEN rk hrs ~> rst THEN + rst_refines ctx rst (k sis)) + hrs sis lsis sfv st + (REF: ris_refines ctx hrs sis) + (EXEC: sexec_rec (cf ctx) ib sis k = st) + (SOUT: get_soutcome ctx st = Some (sout lsis sfv)) + (OK: si_ok ctx lsis), + WHEN hrexec_rec (cf ctx) ib hrs rk ~> rst THEN + rst_refines ctx rst st. +Proof. + induction ib; try (wlp_simplify; fail). + - (* BF *) + wlp_simplify; exploit tr_hrs_correct; eauto. + intros; constructor; auto. + intros X; apply H0 in X. + exploit hrexec_final_sfv_correct; eauto. + - (* Bnop *) wlp_simplify; eapply CONT; eauto. + - (* Bseq *) + wlp_simplify. + eapply IHib1. 3-7: eauto. + + simpl. eapply sexec_rec_okpreserv; eauto. + + intros; eapply IHib2; eauto. + - (* Bcond *) + simpl; intros; wlp_simplify. + assert (rOK: ris_ok ctx hrs). { + erewrite <- OK_EQUIV. 2: eauto. + eapply sexec_rec_okpreserv with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto. + } + exploit (Refcond ctx (fst exta) cond (snd exta) (list_sval_inj (map sis args)) exta0 exta1 + (sexec_rec (cf ctx) ib1 sis k) (sexec_rec (cf ctx) ib2 sis k)); + exploit H; eauto; intros SEVAL; auto. + all: + simpl in SOUT; generalize SOUT; clear SOUT; + inversion_SOME b0; try_simplify_someHyps. + + intros; eapply IHib1; eauto. + + intros; eapply IHib2; eauto. +Qed. + +Lemma hrexec_correct1 ctx ib sis sfv: + get_soutcome ctx (sexec (cf ctx) ib) = Some (sout sis sfv) -> + (si_ok ctx sis) -> + WHEN hrexec (cf ctx) ib ~> rst THEN + rst_refines ctx rst (sexec (cf ctx) ib). +Proof. + unfold sexec; intros; wlp_simplify. + eapply hrexec_rec_correct1; eauto; simpl; congruence. +Qed. + +Lemma hrexec_rec_okpreserv ctx ib: + forall k + (CONT: forall hrs lhrs rfv, + WHEN k hrs ~> rst THEN + get_routcome ctx rst = Some (rout lhrs rfv) -> + ris_ok ctx lhrs -> + ris_ok ctx hrs) + hrs lhrs rfv, + WHEN hrexec_rec (cf ctx) ib hrs k ~> rst THEN + get_routcome ctx rst = Some (rout lhrs rfv) -> + ris_ok ctx lhrs -> + ris_ok ctx hrs. +Proof. + induction ib; simpl; try (wlp_simplify; try_simplify_someHyps; fail). + - (* Bop *) + wlp_simplify; exploit hrs_ok_op_okpreserv; eauto. + - (* Bload *) + destruct trap; wlp_simplify; try_simplify_someHyps; + exploit hrs_ok_load_okpreserv; eauto. + - (* Bstore *) + wlp_simplify; exploit hrs_ok_store_okpreserv; eauto. + - (* Bcond *) + wlp_simplify; generalize H2; clear H2; inversion_SOME b; destruct b; try_simplify_someHyps. +Qed. +Local Hint Resolve hrexec_rec_okpreserv: wlp. + +Lemma hrexec_rec_correct2 ctx ib: + forall rk k + (CONTh: forall hrs lhrs rfv, + WHEN rk hrs ~> rst THEN + get_routcome ctx rst = Some (rout lhrs rfv) -> + ris_ok ctx lhrs -> + ris_ok ctx hrs) + (CONT: forall hrs sis lhrs rfv, + ris_refines ctx hrs sis -> + WHEN rk hrs ~> rst THEN + get_routcome ctx rst = Some (rout lhrs rfv) -> + ris_ok ctx lhrs -> + rst_refines ctx rst (k sis)) + hrs sis lhrs rfv + (REF: ris_refines ctx hrs sis), + WHEN hrexec_rec (cf ctx) ib hrs rk ~> rst THEN + get_routcome ctx rst = Some (rout lhrs rfv) -> + ris_ok ctx lhrs -> + rst_refines ctx rst (sexec_rec (cf ctx) ib sis k). +Proof. + induction ib; try (wlp_simplify; fail). + - (* BF *) + wlp_simplify; exploit tr_hrs_correct; eauto. + intros; constructor; auto. + intros X; apply H0 in X. + exploit hrexec_final_sfv_correct; eauto. + - (* Bnop *) wlp_simplify; eapply CONT; eauto. + - (* Bseq *) + wlp_simplify. + eapply IHib1. 3-6: eauto. + + simpl; eapply hrexec_rec_okpreserv; eauto. + + intros; eapply IHib2; eauto. + - (* Bcond *) + simpl; intros; wlp_simplify. + assert (rOK: ris_ok ctx hrs). { + simpl in H2; generalize H2; inversion_SOME b0; destruct b0; try_simplify_someHyps. + } + exploit (Refcond ctx (fst exta) cond (snd exta) (list_sval_inj (map sis args)) exta0 exta1 + (sexec_rec (cf ctx) ib1 sis k) (sexec_rec (cf ctx) ib2 sis k)); + exploit H; eauto; intros SEVAL; auto. + all: + simpl in H2; generalize H2; clear H2; + inversion_SOME b0; try_simplify_someHyps. + + intros; eapply IHib1; eauto. + + intros; eapply IHib2; eauto. + Unshelve. all: auto. +Qed. + +Lemma hrexec_correct2 ctx ib hrs rfv: + WHEN hrexec (cf ctx) ib ~> rst THEN + get_routcome ctx rst = Some (rout hrs rfv) -> + (ris_ok ctx hrs) -> + rst_refines ctx rst (sexec (cf ctx) ib). +Proof. + unfold hrexec; intros; wlp_simplify. + eapply hrexec_rec_correct2; eauto; simpl; + wlp_simplify; congruence. +Qed. + +Global Opaque hrexec. + +End CanonBuilding. + +(** * 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. + +Definition hrs_simu_check (hrs1 hrs2: ristate) : ?? unit := + DEBUG("? hrs_simu_check");; + phys_check (ris_smem hrs1) (ris_smem hrs2) "hrs_simu_check: ris_smem sets aren't equiv";; + phys_check (ris_input_init hrs1) (ris_input_init hrs2) "hrs_simu_check: ris_input_init bools aren't equiv";; + PTree_eq_check (ris_sreg hrs1) (ris_sreg hrs2);; + Sets.assert_list_incl mk_hash_params (ok_rsval hrs2) (ok_rsval hrs1);; + DEBUG("=> hrs_simu_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 hrs_simu_check_correct hrs1 hrs2: + WHEN hrs_simu_check hrs1 hrs2 ~> _ THEN + ris_simu hrs1 hrs2. +Proof. + wlp_simplify; constructor; auto. + unfold ris_sreg_get; intros r; rewrite H, H1; reflexivity. +Qed. +Hint Resolve hrs_simu_check_correct: wlp. +Global Opaque hrs_simu_check. + +Definition svos_simu_check (svos1 svos2: sval + 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 sval) := + 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 + bs1 = 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 + lbs1 = 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 (sfv1 sfv2: sfval): ?? unit := + match sfv1, sfv2 with + | Sgoto e1, Sgoto e2 => + phys_check e1 e2 "sfval_simu_check: Sgoto successors do not match" + | Scall sig1 svos1 lsv1 res1 e1, Scall sig2 svos2 lsv2 res2 e2 => + phys_check e1 e2 "sfval_simu_check: Scall successors do not match";; + 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" + | Stailcall sig1 svos1 lsv1, Stailcall 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" + | Sbuiltin ef1 lbs1 br1 e1, Sbuiltin ef2 lbs2 br2 e2 => + phys_check e1 e2 "sfval_simu_check: Sbuiltin successors do not match";; + phys_check ef1 ef2 "sfval_simu_check: Sbuiltin ef do not match";; + phys_check br1 br2 "sfval_simu_check: Sbuiltin br do not match";; + list_builtin_arg_simu_check lbs1 lbs2 + | Sjumptable sv1 le1, Sjumptable sv2 le2 => + phys_check le1 le2 "sfval_simu_check: Sjumptable successors do not match";; + phys_check sv1 sv2 "sfval_simu_check: Sjumptable sval do not match" + | Sreturn osv1, Sreturn osv2 => + option_eq_check osv1 osv2 + | _, _ => FAILWITH "sfval_simu_check: structure mismatch" + end. + +Lemma sfval_simu_check_correct sfv1 sfv2: + WHEN sfval_simu_check sfv1 sfv2 ~> _ THEN + rfv_simu sfv1 sfv2. +Proof. + destruct sfv1; destruct sfv2; simpl; wlp_simplify; try congruence. +Qed. +Hint Resolve sfval_simu_check_correct: wlp. +Global Opaque sfval_simu_check. + +Fixpoint rst_simu_check (rst1 rst2: rstate) {struct rst1} := + match rst1, rst2 with + | Rfinal hrs1 sfv1, Rfinal hrs2 sfv2 => + hrs_simu_check hrs1 hrs2;; + sfval_simu_check sfv1 sfv2 + | Rcond cond1 lsv1 rsL1 rsR1, Rcond cond2 lsv2 rsL2 rsR2 => + struct_check cond1 cond2 "rst_simu_check: conditions do not match";; + phys_check lsv1 lsv2 "rst_simu_check: args do not match";; + rst_simu_check rsL1 rsL2;; + rst_simu_check rsR1 rsR2 + | _, _ => FAILWITH "rst_simu_check: simu_check failed" + end. + +Lemma rst_simu_check_correct rst1: forall rst2, + WHEN rst_simu_check rst1 rst2 ~> _ THEN + rst_simu rst1 rst2. +Proof. + induction rst1; destruct rst2; + wlp_simplify; constructor; auto. +Qed. +Hint Resolve rst_simu_check_correct: wlp. +Global Opaque rst_simu_check. + +Definition simu_check_single (f1 f2: function) (ibf1 ibf2: iblock_info): ?? unit := + (* creating the hash-consing tables *) + DO hC_sval <~ hCons hSVAL;; + DO hC_list_hsval <~ hCons hLSVAL;; + DO hC_hsmem <~ hCons hSMEM;; + let hrexec := hrexec hC_sval.(hC) hC_list_hsval.(hC) hC_hsmem.(hC) in + (* performing the hash-consed executions *) + DO hst1 <~ hrexec f1 ibf1.(entry);; + DO hst2 <~ hrexec f2 ibf2.(entry);; + (* comparing the executions *) + rst_simu_check hst1 hst2. + +Lemma simu_check_single_correct (f1 f2: function) (ibf1 ibf2: iblock_info): + WHEN simu_check_single f1 f2 ibf1 ibf2 ~> _ THEN + symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry). +Proof. + unfold symbolic_simu; wlp_simplify. + eapply rst_simu_correct; eauto. + + intros; eapply hrexec_correct1; eauto; wlp_simplify. + + intros; eapply hrexec_correct2; eauto; wlp_simplify. +Qed. +Global Opaque simu_check_single. +Global Hint Resolve simu_check_single_correct: wlp. + +Program Definition aux_simu_check (f1 f2: function) (ibf1 ibf2: iblock_info): ?? bool := + DO r <~ + (TRY + simu_check_single f1 f2 ibf1 ibf2;; + RET true + CATCH_FAIL s, _ => + println ("simu_check_failure:" +; s);; + RET false + ENSURE (fun b => b=true -> symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry)));; + RET (`r). +Obligation 1. + split; wlp_simplify. discriminate. +Qed. + +Lemma aux_simu_check_correct (f1 f2: function) (ibf1 ibf2: iblock_info): + WHEN aux_simu_check f1 f2 ibf1 ibf2 ~> b THEN + b=true -> symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry). +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 (f1 f2: function) (ibf1 ibf2: iblock_info): res unit := + match unsafe_coerce (aux_simu_check f1 f2 ibf1 ibf2) with + | Some true => OK tt + | _ => Error (msg "simu_check has failed") + end. + +Lemma simu_check_correct f1 f2 ibf1 ibf2: + simu_check f1 f2 ibf1 ibf2 = OK tt -> + symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry). +Proof. + unfold simu_check. + destruct (unsafe_coerce (aux_simu_check f1 f2 ibf1 ibf2)) as [[|]|] eqn:Hres; simpl; try discriminate. + intros; eapply aux_simu_check_correct; eauto. + eapply unsafe_coerce_not_really_correct; eauto. +Qed. |