diff options
Diffstat (limited to 'scheduling/RTLpathSE_simu_specs.v')
| -rw-r--r-- | scheduling/RTLpathSE_simu_specs.v | 937 |
1 files changed, 0 insertions, 937 deletions
diff --git a/scheduling/RTLpathSE_simu_specs.v b/scheduling/RTLpathSE_simu_specs.v deleted file mode 100644 index 5051d805..00000000 --- a/scheduling/RTLpathSE_simu_specs.v +++ /dev/null @@ -1,937 +0,0 @@ -(** Low-level specifications of the simulation tests by symbolic execution with hash-consing *) - -Require Import Coqlib Maps Floats. -Require Import AST Integers Values Events Memory Globalenvs Smallstep. -Require Import Op Registers. -Require Import RTL RTLpath. -Require Import Errors. -Require Import RTLpathSE_theory RTLpathLivegenproof. -Require Import Axioms. -Require Import Lia. - -Local Open Scope error_monad_scope. -Local Open Scope option_monad_scope. - -Require Export Impure.ImpHCons. -Import HConsing. - -Import ListNotations. -Local Open Scope list_scope. - -(** * Auxilary notions on simulation tests *) - -Definition silocal_simu (dm: PTree.t node) (f: RTLpath.function) outframe (sl1 sl2: sistate_local) (ctx: simu_proof_context f): Prop := - forall is1, ssem_local (the_ge1 ctx) (the_sp ctx) sl1 (the_rs0 ctx) (the_m0 ctx) (irs is1) (imem is1) -> - exists is2, ssem_local (the_ge2 ctx) (the_sp ctx) sl2 (the_rs0 ctx) (the_m0 ctx) (irs is2) (imem is2) - /\ istate_simu f dm outframe is1 is2. - -(* a kind of negation of sabort_local *) -Definition sok_local (ge: RTL.genv) (sp:val) (rs0: regset) (m0: mem) (st: sistate_local): Prop := - (st.(si_pre) ge sp rs0 m0) - /\ seval_smem ge sp st.(si_smem) rs0 m0 <> None - /\ forall (r: reg), seval_sval ge sp (si_sreg st r) rs0 m0 <> None. - -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. - -Definition siexit_simu (dm: PTree.t node) (f: RTLpath.function) outframe (ctx: simu_proof_context f) (se1 se2: sistate_exit) := - (sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal se1) -> - (seval_condition (the_ge1 ctx) (the_sp ctx) (si_cond se1) (si_scondargs se1) - (si_smem (si_elocal se1)) (the_rs0 ctx) (the_m0 ctx)) = - (seval_condition (the_ge2 ctx) (the_sp ctx) (si_cond se2) (si_scondargs se2) - (si_smem (si_elocal se2)) (the_rs0 ctx) (the_m0 ctx))) - /\ forall is1, - icontinue is1 = false -> - ssem_exit (the_ge1 ctx) (the_sp ctx) se1 (the_rs0 ctx) (the_m0 ctx) (irs is1) (imem is1) (ipc is1) -> - exists is2, - ssem_exit (the_ge2 ctx) (the_sp ctx) se2 (the_rs0 ctx) (the_m0 ctx) (irs is2) (imem is2) (ipc is2) - /\ istate_simu f dm outframe is1 is2. - -Definition siexits_simu (dm: PTree.t node) (f: RTLpath.function) outframe (lse1 lse2: list sistate_exit) (ctx: simu_proof_context f) := - list_forall2 (siexit_simu dm f outframe ctx) lse1 lse2. - - -(** * 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) (hid: hashcode) (** NB: does not depend on the memory ! *) - | HSload (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval) (hid: hashcode) -with list_hsval := - | HSnil (hid: hashcode) - | 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. - - - -(** 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) -. - -(** * gives the semantics of hash-consed symbolic values *) -Fixpoint hsval_proj hsv := - match hsv with - | HSinput r _ => Sinput r - | HSop op hl _ => Sop op (hsval_list_proj hl) Sinit (** NB: use the initial memory of the path ! *) - | HSload hm t chk addr hl _ => Sload (hsmem_proj hm) t chk addr (hsval_list_proj hl) - end -with hsval_list_proj hl := - 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. - -(** We use a Notation instead a Definition, in order to get more automation "for free" *) -Notation "'seval_hsval' ge sp hsv" := (seval_sval ge sp (hsval_proj hsv)) - (only parsing, at level 0, ge at next level, sp at next level, hsv at next level): hse. - -Local Open Scope hse. - -Notation "'seval_list_hsval' ge sp lhv" := (seval_list_sval ge sp (hsval_list_proj lhv)) - (only parsing, at level 0, ge at next level, sp at next level, lhv at next level): hse. -Notation "'seval_hsmem' ge sp hsm" := (seval_smem ge sp (hsmem_proj hsm)) - (only parsing, at level 0, ge at next level, sp at next level, hsm at next level): hse. - -Notation "'sval_refines' ge sp rs0 m0 hv sv" := (seval_hsval ge sp hv rs0 m0 = seval_sval ge sp sv rs0 m0) - (only parsing, at level 0, ge at next level, sp at next level, rs0 at next level, m0 at next level, hv at next level, sv at next level): hse. -Notation "'list_sval_refines' ge sp rs0 m0 lhv lsv" := (seval_list_hsval ge sp lhv rs0 m0 = seval_list_sval ge sp lsv rs0 m0) - (only parsing, at level 0, ge at next level, sp at next level, rs0 at next level, m0 at next level, lhv at next level, lsv at next level): hse. -Notation "'smem_refines' ge sp rs0 m0 hm sm" := (seval_hsmem ge sp hm rs0 m0 = seval_smem ge sp sm rs0 m0) - (only parsing, at level 0, ge at next level, sp at next level, rs0 at next level, m0 at next level, hm at next level, sm at next level): hse. - - -(** ** Implementation of symbolic states (with hash-consing) *) - -(** *** Syntax and semantics of symbolic internal local states - -The semantics is given by the refinement relation [hsilocal_refines] wrt to (abstract) symbolic internal local states - -*) - -(* NB: "h" stands for hash-consing *) -Record hsistate_local := - { - (** [hsi_smem] represents the current smem symbolic evaluations. - (we also recover the history of smem in hsi_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 - }. - -Definition hsi_sreg_proj (hst: PTree.t hsval) r: sval := - match PTree.get r hst with - | None => Sinput r - | Some hsv => hsval_proj hsv - end. - -Definition hsi_sreg_eval ge sp hst r := seval_sval ge sp (hsi_sreg_proj hst r). - -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) - /\ (seval_hsmem ge sp (hst.(hsi_smem)) 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 -> smem_refines ge sp rs0 m0 (hsi_smem hst) (st.(si_smem))) - /\ (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) - /\ (* the below invariant allows to evaluate operations in the initial memory of the path instead of the current memory *) - (forall m b ofs, seval_smem ge sp st.(si_smem) rs0 m0 = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) - . - -(** *** 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 }. - -(** 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 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 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. - - -(** *** Syntax and Semantics of symbolic internal state *) - -Record hsistate := { hsi_pc: node; hsi_exits: list hsistate_exit; hsi_local: hsistate_local }. - -(* expresses the "monotony" of sok_local along sequences *) -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_stat (hst: hsistate) (st:sistate): Prop := - hsi_pc hst = si_pc st - /\ hsiexits_refines_stat (hsi_exits hst) (si_exits st). - -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) (* invariant necessary to prove "monotony" of sok_local along execution *) - . - -(** *** Syntax and Semantics of symbolic state *) - -Definition hfinal_proj (hfv: hsfval) : sfval := - match hfv with - | HSnone => Snone - | HScall s hvi hlv r pc => Scall s (sum_left_map hsval_proj hvi) (hsval_list_proj hlv) r pc - | HStailcall s hvi hlv => Stailcall s (sum_left_map hsval_proj hvi) (hsval_list_proj hlv) - | HSbuiltin ef lbh br pc => Sbuiltin ef (List.map (builtin_arg_map hsval_proj) lbh) br pc - | HSjumptable hv ln => Sjumptable (hsval_proj hv) ln - | HSreturn oh => Sreturn (option_map hsval_proj oh) - end. - -Section HFINAL_REFINES. - -Variable ge: RTL.genv. -Variable sp: val. -Variable rs0: regset. -Variable m0: mem. - -Definition option_refines (ohsv: option hsval) (osv: option sval) := - match ohsv, osv with - | Some hsv, Some sv => sval_refines ge sp rs0 m0 hsv sv - | None, None => True - | _, _ => False - end. - -Definition sum_refines (hsi: hsval + ident) (si: sval + ident) := - match hsi, si with - | inl hv, inl sv => sval_refines ge sp rs0 m0 hv sv - | inr id, inr id' => id = id' - | _, _ => False - end. - -Definition bargs_refines (hargs: list (builtin_arg hsval)) (args: list (builtin_arg sval)): Prop := - seval_list_builtin_sval ge sp (List.map (builtin_arg_map hsval_proj) hargs) rs0 m0 = seval_list_builtin_sval ge sp args rs0 m0. - -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_sval_refines ge sp rs0 m0 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_sval_refines ge sp rs0 m0 hargs args -> - hfinal_refines (HStailcall s hros hargs) (Stailcall s ros args) - | hsbuiltin_ref: forall ef lbha lba br pc, - bargs_refines lbha lba -> - hfinal_refines (HSbuiltin ef lbha br pc) (Sbuiltin ef lba br pc) - | hsjumptable_ref: forall hsv sv lpc, - sval_refines ge sp rs0 m0 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). - -End HFINAL_REFINES. - -(* TODO gourdinl Leave this here ? *) -Section FAKE_HSVAL. -(* BEGIN "fake" hsval without real hash-consing *) -(* TODO: - 2) reuse these definitions in hSinput, hSop, etc - in order to factorize proofs ? -*) - -Definition fSinput (r: reg): hsval := - HSinput r unknown_hid. - -Lemma fSinput_correct r ge sp rs0 m0: (* useless trivial lemma ? *) - sval_refines ge sp rs0 m0 (fSinput r) (Sinput r). -Proof. - auto. -Qed. - -Definition fSop (op:operation) (lhsv: list_hsval): hsval := - HSop op lhsv unknown_hid. - -Lemma fSop_correct op lhsv ge sp rs0 m0 lsv sm m: forall - (MEM: seval_smem ge sp sm rs0 m0 = Some m) - (MVALID: forall b ofs, Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) - (LR: list_sval_refines ge sp rs0 m0 lhsv lsv), - sval_refines ge sp rs0 m0 (fSop op lhsv) (Sop op lsv sm). -Proof. - intros; simpl. rewrite <- LR, MEM. - destruct (seval_list_sval _ _ _ _); try congruence. - eapply op_valid_pointer_eq; eauto. -Qed. - -Definition fsi_sreg_get (hst: PTree.t hsval) r: hsval := - match PTree.get r hst with - | None => fSinput r - | Some sv => sv - end. - -Lemma fsi_sreg_get_correct hst r ge sp rs0 m0 (f: reg -> sval): forall - (RR: forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0), - sval_refines ge sp rs0 m0 (fsi_sreg_get hst r) (f r). -Proof. - unfold hsi_sreg_eval, hsi_sreg_proj, fsi_sreg_get; intros; simpl. - rewrite <- RR. destruct (hst ! r); simpl; auto. -Qed. - -Definition fSnil: list_hsval := - HSnil unknown_hid. - -(* TODO: Lemma fSnil_correct *) - -Definition fScons (hsv: hsval) (lhsv: list_hsval): list_hsval := - HScons hsv lhsv unknown_hid. - -(* TODO: Lemma fScons_correct *) - -(* END "fake" hsval ... *) - -End FAKE_HSVAL. - - -Record hsstate := { hinternal:> hsistate; hfinal: hsfval }. - -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)) - /\ (forall ge sp rs0 m0, hsok_local ge sp rs0 m0 (hsi_local (hinternal hst)) -> hfinal_refines ge sp rs0 m0 (hfinal hst) (final st)) - . - -(** * Intermediate specifications of the simulation tests *) - -(** ** Specification of the simulation test on [hsistate_local]. - It is motivated by [hsilocal_simu_spec_correct theorem] below -*) -Definition hsilocal_simu_spec (alive: Regset.t) (hst1 hst2: hsistate_local) := - List.incl (hsi_ok_lsval hst2) (hsi_ok_lsval hst1) - /\ (forall r, Regset.In r alive -> PTree.get r hst2 = PTree.get r hst1) - /\ hsi_smem hst1 = hsi_smem hst2. - -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. - -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. - -Lemma hsilocal_simu_spec_nofail ge1 ge2 of sp rs0 m0 hst1 hst2: - hsilocal_simu_spec 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 & _ & MEMOK) GFS (OKV & OKM). constructor. - - intros sv INS. apply RSOK in INS. apply OKV in INS. erewrite seval_preserved; eauto. - - erewrite MEMOK in OKM. erewrite smem_eval_preserved; eauto. -Qed. - -Theorem hsilocal_simu_spec_correct hst1 hst2 alive ge1 ge2 sp rs0 m0 rs m st1 st2: - hsilocal_simu_spec alive 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 -> - 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'. -Proof. - intros CORE HREF1 HREF2 GFS SEML. - refine (modusponens _ _ (ssem_local_refines_hok _ _ _ _ _ _ _ _ _ _) _); eauto. - intro HOK1. - refine (modusponens _ _ (hsilocal_simu_spec_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 smem_eval_preserved; [| eapply GFS]. - rewrite MEMEQ1; auto. } - constructor. - + constructor; [assumption | constructor; [assumption|]]. - destruct HREF2 as (B & _ & A & _). - (** B is 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. - generalize (A HOK2 r). unfold hsi_sreg_eval. - rewrite seval_partial_regset_get. - unfold hsi_sreg_proj. - destruct (hst2 ! r) eqn:HST2; [| simpl; reflexivity]. - unfold seval_sval_partial. generalize HOK2; rewrite <- B; intros (_ & _ & C) D. - assert (seval_sval ge2 sp (hsval_proj h) rs0 m0 <> None) by congruence. - destruct (seval_sval ge2 sp _ 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_sval ge2 sp (hsval_proj h) rs0 m0 = hsi_sreg_eval ge2 sp hst2 r rs0 m0). { - unfold hsi_sreg_eval, hsi_sreg_proj. rewrite HST2. reflexivity. } - rewrite H. clear H. unfold hsi_sreg_eval, hsi_sreg_proj. rewrite C; [|assumption]. - erewrite seval_preserved; [| eapply GFS]. - unfold hsi_sreg_eval, hsi_sreg_proj in B; rewrite B; [|assumption]. rewrite RSEQ. reflexivity. - ++ rewrite <- RSEQ. rewrite <- B; [|assumption]. unfold hsi_sreg_eval, hsi_sreg_proj. - rewrite <- C; [|assumption]. rewrite HST2. reflexivity. -Qed. - -(** ** Specification of the simulation test on [hsistate_exit]. - It is motivated by [hsiexit_simu_spec_correct theorem] below -*) -Definition hsiexit_simu_spec dm f (hse1 hse2: hsistate_exit) := - (exists path, (fn_path f) ! (hsi_ifso hse1) = Some path - /\ hsilocal_simu_spec 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. - -Definition hsiexit_simu dm f outframe (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 outframe ctx se1 se2. - -Lemma hsiexit_simu_spec_nofail dm f hse1 hse2 ge1 ge2 sp rs m: - hsiexit_simu_spec dm f hse1 hse2 -> - (forall s, Genv.find_symbol ge1 s = Genv.find_symbol ge2 s) -> - hsok_local ge1 sp rs m (hsi_elocal hse1) -> - hsok_local ge2 sp rs m (hsi_elocal hse2). -Proof. - intros CORE GFS HOK1. - destruct CORE as ((p & _ & CORE') & _ & _ & _). - eapply hsilocal_simu_spec_nofail; eauto. -Qed. - -Theorem hsiexit_simu_spec_correct dm f outframe hse1 hse2 ctx: - hsiexit_simu_spec dm f hse1 hse2 -> - hsiexit_simu dm f outframe 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; exploit hsiexit_simu_spec_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_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (hsi_elocal hse1)). { - destruct HDYN1 as (LREF & _). destruct LREF as (OKEQ & _ & _). rewrite <- OKEQ. assumption. } - exploit hsiexit_simu_spec_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_spec_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 outframe ctx hse1 hse2 se1 se2: - hsiexit_simu dm f outframe 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 outframe ctx se1 se2. -Proof. - auto. -Qed. - -(** ** Specification of the simulation test on [list hsistate_exit]. - It is motivated by [hsiexit_simu_spec_correct theorem] below -*) - -Definition hsiexits_simu dm f outframe (ctx: simu_proof_context f) (lhse1 lhse2: list hsistate_exit): Prop := - list_forall2 (hsiexit_simu dm f outframe ctx) lhse1 lhse2. - -Definition hsiexits_simu_spec dm f lhse1 lhse2: Prop := - list_forall2 (hsiexit_simu_spec dm f) lhse1 lhse2. - -Theorem hsiexits_simu_spec_correct dm f outframe lhse1 lhse2 ctx: - hsiexits_simu_spec dm f lhse1 lhse2 -> - hsiexits_simu dm f outframe ctx lhse1 lhse2. -Proof. - induction 1; [constructor|]. - constructor; [|apply IHlist_forall2; assumption]. - apply hsiexit_simu_spec_correct; assumption. -Qed. - - -Lemma siexits_simu_all_fallthrough dm f outframe ctx: forall lse1 lse2, - siexits_simu dm f outframe 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 siexits_simu_all_fallthrough_upto dm f outframe ctx lse1 lse2: - siexits_simu dm f outframe 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 hsiexits_simu_siexits dm f outframe ctx lhse1 lhse2: - hsiexits_simu dm f outframe 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 outframe 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. - - -(** ** Specification of the simulation test on [hsistate]. - It is motivated by [hsistate_simu_spec_correct theorem] below -*) - -Definition hsistate_simu_spec dm f outframe (hse1 hse2: hsistate) := - list_forall2 (hsiexit_simu_spec dm f) (hsi_exits hse1) (hsi_exits hse2) - /\ hsilocal_simu_spec outframe (hsi_local hse1) (hsi_local hse2). - -Definition hsistate_simu dm f outframe (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 outframe st1 st2 ctx. - -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. lia. -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; lia). rewrite H. clear H. - inv ITAIL. - + assert (forall n, (n - n)%nat = 0%nat) by (intro; lia). 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; lia). - exploit (is_tail_length (x::l1)); eauto. intro. simpl in H2. - assert ((length l2 > length l1)%nat) by lia. clear H2. - rewrite H0; auto. -Qed. - -Theorem hsistate_simu_spec_correct dm f outframe hst1 hst2 ctx: - hsistate_simu_spec dm f outframe hst1 hst2 -> - hsistate_simu dm f outframe hst1 hst2 ctx. -Proof. - intros (ESIMU & LSIMU) st1 st2 (PCREF1 & EREF1) (PCREF2 & EREF2) DREF1 DREF2 is1 SEMI. - destruct DREF1 as (DEREF1 & LREF1 & NESTED). destruct DREF2 as (DEREF2 & LREF2 & _). - exploit hsiexits_simu_spec_correct; eauto. intro HESIMU. - unfold ssem_internal in SEMI. destruct (icontinue _) eqn:ICONT. - - destruct SEMI as (SSEML & PCEQ & ALLFU). - exploit hsilocal_simu_spec_correct; eauto; [apply ctx|]. simpl. intro SSEML2. - exists (mk_istate (icontinue is1) (si_pc st2) (seval_partial_regset (the_ge2 ctx) (the_sp ctx) - (the_rs0 ctx) (the_m0 ctx) (hsi_local hst2)) (imem is1)). constructor. - + unfold ssem_internal. simpl. rewrite ICONT. - destruct SSEML2 as [SSEMLP EQLIVE]. - 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. - destruct SSEML2 as [SSEMLP EQLIVE]. - constructor; simpl; auto. - - destruct SEMI as (ext & lx & SSEME & ALLFU). - assert (SESIMU: siexits_simu dm f outframe (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 outframe 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. - - -(** ** Specification of the simulation test on [sfval]. - It is motivated by [hfinal_simu_spec_correct theorem] below -*) - - -Definition final_simu_spec (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_spec (dm: PTree.t node) (f: RTLpath.function) (pc1 pc2: node) (hf1 hf2: hsfval): Prop := - final_simu_spec 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. - -Lemma list_proj_refines_eq ge ge' sp rs0 m0 lsv lhsv: - (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) -> - list_sval_refines ge sp rs0 m0 lhsv lsv -> - forall lhsv' lsv', - list_sval_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. - intros GFS H lhsv' lsv' H' H0. - erewrite <- H, H0. - erewrite list_sval_eval_preserved; eauto. -Qed. - -Lemma seval_builtin_sval_preserved ge ge' sp sv rs0 m0: - (forall s : ident, Genv.find_symbol ge' s = Genv.find_symbol ge s) -> - seval_builtin_sval ge sp sv rs0 m0 = - seval_builtin_sval ge' sp sv rs0 m0. -Proof. - induction sv; intro FIND; cbn. - all: try (erewrite seval_preserved by eauto); trivial. - all: erewrite IHsv1 by eauto; erewrite IHsv2 by eauto; reflexivity. -Qed. - -Lemma seval_list_builtin_sval_preserved ge ge' sp lsv rs0 m0: - (forall s : ident, Genv.find_symbol ge' s = Genv.find_symbol ge s) -> - seval_list_builtin_sval ge sp lsv rs0 m0 = - seval_list_builtin_sval ge' sp lsv rs0 m0. -Proof. - induction lsv; intro FIND; cbn. { trivial. } - erewrite seval_builtin_sval_preserved by eauto. - erewrite IHlsv by eauto. - reflexivity. -Qed. - -Lemma barg_proj_refines_eq ge ge' sp rs0 m0: - (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) -> - forall lhsv lsv, bargs_refines ge sp rs0 m0 lhsv lsv -> - forall lhsv' lsv', bargs_refines ge' sp rs0 m0 lhsv' lsv' -> - List.map (builtin_arg_map hsval_proj) lhsv = List.map (builtin_arg_map hsval_proj) lhsv' -> - seval_list_builtin_sval ge sp lsv rs0 m0 = seval_list_builtin_sval ge' sp lsv' rs0 m0. -Proof. - unfold bargs_refines; intros GFS lhsv lsv H lhsv' lsv' H' H0. - erewrite <- H, H0. - erewrite seval_list_builtin_sval_preserved; 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, PROJ. - erewrite <- seval_preserved; eauto. -Qed. - -Theorem hfinal_simu_spec_correct dm f ctx opc1 opc2 hf1 hf2 f1 f2: - hfinal_simu_spec 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. - 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. - (* 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. - 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. - (* 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. - (* 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. - + destruct res0; try discriminate. destruct osv0; inv H1. constructor. -Qed. - - -(** ** Specification of the simulation test on [hsstate]. - It is motivated by [hsstate_simu_spec_correct theorem] below -*) - -Definition hsstate_simu_spec (dm: PTree.t node) (f: RTLpath.function) outframe (hst1 hst2: hsstate) := - hsistate_simu_spec dm f outframe (hinternal hst1) (hinternal hst2) - /\ hfinal_simu_spec dm f (hsi_pc (hinternal hst1)) (hsi_pc (hinternal hst2)) (hfinal hst1) (hfinal hst2). - -Definition hsstate_simu dm f outframe (hst1 hst2: hsstate) ctx: Prop := - forall st1 st2, - hsstate_refines hst1 st1 -> - hsstate_refines hst2 st2 -> sstate_simu dm f outframe st1 st2 ctx. - -Theorem hsstate_simu_spec_correct dm f outframe ctx hst1 hst2: - hsstate_simu_spec dm f outframe hst1 hst2 -> - hsstate_simu dm f outframe hst1 hst2 ctx. -Proof. - intros (SCORE & FSIMU) st1 st2 (SREF1 & DREF1 & FREF1) (SREF2 & DREF2 & FREF2). - generalize SCORE. intro SIMU; eapply hsistate_simu_spec_correct in SIMU; eauto. - constructor; auto. - intros is1 SEM1 CONT1. - unfold hsistate_simu in SIMU. exploit SIMU; clear SIMU; eauto. - unfold istate_simu, ssem_internal in *; intros (is2 & SEM2 & SIMU). - rewrite! CONT1 in *. destruct SIMU as (CONT2 & _). - rewrite! CONT1, <- CONT2 in *. - destruct SEM1 as (SEM1 & _ & _). - destruct SEM2 as (SEM2 & _ & _). - eapply hfinal_simu_spec_correct in FSIMU; eauto. - - destruct SREF1 as (PC1 & _). destruct SREF2 as (PC2 & _). rewrite <- PC1. rewrite <- PC2. - eapply FSIMU. - - eapply FREF1. exploit DREF1. intros (_ & (OK & _) & _). rewrite <- OK. eapply ssem_local_sok; eauto. - - eapply FREF2. exploit DREF2. intros (_ & (OK & _) & _). rewrite <- OK. eapply ssem_local_sok; eauto. -Qed. |