diff options
Diffstat (limited to 'scheduling/RTLpathSE_simu_specs.v')
| -rw-r--r-- | scheduling/RTLpathSE_simu_specs.v | 22 |
1 files changed, 6 insertions, 16 deletions
diff --git a/scheduling/RTLpathSE_simu_specs.v b/scheduling/RTLpathSE_simu_specs.v index c93c1343..5051d805 100644 --- a/scheduling/RTLpathSE_simu_specs.v +++ b/scheduling/RTLpathSE_simu_specs.v @@ -74,11 +74,7 @@ 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. -Record hscond := - { cond : condition - ; lhsv : list_hsval - ; hscond_hid : hashcode - (** NB: Like HSop, does also not depend on the memory! *) }. + (** Symbolic final value -- from hash-consed values It does not seem useful to hash-consed these final values (because they are final). @@ -120,8 +116,6 @@ Notation "'seval_list_hsval' ge sp lhv" := (seval_list_sval ge sp (hsval_list_pr (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 "'seval_hscond' ge sp hsc" := (seval_condition ge sp hsc.(cond) (hsval_list_proj hsc.(lhsv)) Sinit) - (only parsing, at level 0, ge at next level, sp at next level, hsc 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. @@ -145,7 +139,6 @@ Record hsistate_local := (** [hsi_smem] represents the current smem symbolic evaluations. (we also recover the history of smem in hsi_smem) *) hsi_smem:> hsmem; - hsi_ok_lscond: list hscond; (** For the values in registers: 1) we store a list of sval evaluations 2) we encode the symbolic regset by a PTree *) @@ -163,7 +156,6 @@ 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) - /\ (forall hsc, List.In hsc (hsi_ok_lscond hst) -> seval_hscond ge sp hsc rs0 m0 <> None) /\ (seval_hsmem ge sp (hst.(hsi_smem)) rs0 m0 <> None). (* refinement link between a (st: sistate_local) and (hst: hsistate_local) *) @@ -388,7 +380,6 @@ Definition hsstate_refines (hst: hsstate) (st:sstate): Prop := *) Definition hsilocal_simu_spec (alive: Regset.t) (hst1 hst2: hsistate_local) := List.incl (hsi_ok_lsval hst2) (hsi_ok_lsval hst1) - /\ List.incl (hsi_ok_lscond hst2) (hsi_ok_lscond hst1) /\ (forall r, Regset.In r alive -> PTree.get r hst2 = PTree.get r hst1) /\ hsi_smem hst1 = hsi_smem hst2. @@ -432,9 +423,8 @@ Lemma hsilocal_simu_spec_nofail ge1 ge2 of sp rs0 m0 hst1 hst2: hsok_local ge1 sp rs0 m0 hst1 -> hsok_local ge2 sp rs0 m0 hst2. Proof. - intros (RSOK & CONDOK & _ & MEMOK) GFS (OKV & OKC & OKM). repeat constructor. + intros (RSOK & _ & MEMOK) GFS (OKV & OKM). constructor. - intros sv INS. apply RSOK in INS. apply OKV in INS. erewrite seval_preserved; eauto. - - intros sc INS. apply CONDOK in INS. apply OKC in INS. erewrite seval_condition_preserved; eauto. - erewrite MEMOK in OKM. erewrite smem_eval_preserved; eauto. Qed. @@ -456,7 +446,7 @@ Proof. 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). + destruct CORE as (_ & _ & MEMEQ3). rewrite <- MEMEQ2; auto. rewrite <- MEMEQ3. erewrite smem_eval_preserved; [| eapply GFS]. rewrite MEMEQ1; auto. } @@ -474,7 +464,7 @@ Proof. 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. + 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. @@ -531,7 +521,7 @@ Proof. 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). + 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. @@ -820,7 +810,7 @@ Proof. erewrite seval_builtin_sval_preserved by eauto. erewrite IHlsv by eauto. reflexivity. -Qed. +Qed. Lemma barg_proj_refines_eq ge ge' sp rs0 m0: (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) -> |