diff options
Diffstat (limited to 'scheduling/RTLpathSE_impl.v')
| -rw-r--r-- | scheduling/RTLpathSE_impl.v | 46 |
1 files changed, 16 insertions, 30 deletions
diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v index 1e36a558..ada0d308 100644 --- a/scheduling/RTLpathSE_impl.v +++ b/scheduling/RTLpathSE_impl.v @@ -1923,22 +1923,6 @@ Qed. Global Opaque PTree_frame_eq_check. Local Hint Resolve PTree_frame_eq_check_correct: wlp. -Definition hsilocal_simu_check hst1 hst2 : ?? unit := - DEBUG("? last check");; - phys_check (hsi_smem hst2) (hsi_smem hst1) "hsilocal_simu_check: hsi_smem sets aren't equiv";; - PTree_eq_check (hsi_sreg hst1) (hsi_sreg hst2);; - Sets.assert_list_incl mk_hash_params (hsi_ok_lsval hst2) (hsi_ok_lsval hst1);; - DEBUG("=> last check: OK"). - -Lemma hsilocal_simu_check_correct hst1 hst2: - WHEN hsilocal_simu_check hst1 hst2 ~> _ THEN - hsilocal_simu_spec None hst1 hst2. -Proof. - unfold hsilocal_simu_spec; wlp_simplify. -Qed. -Hint Resolve hsilocal_simu_check_correct: wlp. -Global Opaque hsilocal_simu_check. - Definition hsilocal_frame_simu_check frame hst1 hst2 : ?? unit := DEBUG("? frame check");; phys_check (hsi_smem hst2) (hsi_smem hst1) "hsilocal_frame_simu_check: hsi_smem sets aren't equiv";; @@ -1966,7 +1950,7 @@ Local Hint Resolve regset_elements_in: core. Lemma hsilocal_frame_simu_check_correct hst1 hst2 alive: WHEN hsilocal_frame_simu_check (Regset.elements alive) hst1 hst2 ~> _ THEN - hsilocal_simu_spec (Some alive) hst1 hst2. + hsilocal_simu_spec alive hst1 hst2. Proof. unfold hsilocal_simu_spec; wlp_simplify. symmetry; eauto. Qed. @@ -2020,13 +2004,13 @@ Qed. Hint Resolve hsiexits_simu_check_correct: wlp. Global Opaque hsiexits_simu_check. -Definition hsistate_simu_check (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsistate) := +Definition hsistate_simu_check (dm: PTree.t node) (f: RTLpath.function) outframe (hst1 hst2: hsistate) := hsiexits_simu_check dm f (hsi_exits hst1) (hsi_exits hst2);; - hsilocal_simu_check (hsi_local hst1) (hsi_local hst2). + hsilocal_frame_simu_check (Regset.elements outframe) (hsi_local hst1) (hsi_local hst2). -Lemma hsistate_simu_check_correct dm f hst1 hst2: - WHEN hsistate_simu_check dm f hst1 hst2 ~> _ THEN - hsistate_simu_spec dm f hst1 hst2. +Lemma hsistate_simu_check_correct dm f outframe hst1 hst2: + WHEN hsistate_simu_check dm f outframe hst1 hst2 ~> _ THEN + hsistate_simu_spec dm f outframe hst1 hst2. Proof. unfold hsistate_simu_spec; wlp_simplify. Qed. @@ -2160,18 +2144,18 @@ Qed. Hint Resolve sfval_simu_check_correct: wlp. Global Opaque sfval_simu_check. -Definition hsstate_simu_check (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) := - hsistate_simu_check dm f (hinternal hst1) (hinternal hst2);; +Definition hsstate_simu_check (dm: PTree.t node) (f: RTLpath.function) outframe (hst1 hst2: hsstate) := + hsistate_simu_check dm f outframe (hinternal hst1) (hinternal hst2);; sfval_simu_check dm f (hsi_pc hst1) (hsi_pc hst2) (hfinal hst1) (hfinal hst2). -Lemma hsstate_simu_check_correct dm f hst1 hst2: - WHEN hsstate_simu_check dm f hst1 hst2 ~> _ THEN - hsstate_simu_spec dm f hst1 hst2. +Lemma hsstate_simu_check_correct dm f outframe hst1 hst2: + WHEN hsstate_simu_check dm f outframe hst1 hst2 ~> _ THEN + hsstate_simu_spec dm f outframe hst1 hst2. Proof. unfold hsstate_simu_spec; wlp_simplify. Qed. Hint Resolve hsstate_simu_check_correct: wlp. -Global Opaque hsstate_simu_check. +Global Opaque hsstate_simu_check. Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) (m: node * node): ?? unit := let (pc2, pc1) := m in @@ -2185,8 +2169,10 @@ Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpa DO hst1 <~ hsexec f pc1;; XDEBUG pc2 (fun pc => DO name_pc <~ string_of_Z (Zpos pc);; RET ("entry-point of output superblock: " +; name_pc)%string);; DO hst2 <~ hsexec tf pc2;; + DO path <~ some_or_fail ((fn_path f)!pc1) "simu_check_single.internal_error.1";; + let outframe := path.(pre_output_regs) in (* comparing the executions *) - hsstate_simu_check dm f hst1 hst2. + hsstate_simu_check dm f outframe hst1 hst2. Lemma simu_check_single_correct dm tf f pc1 pc2: WHEN simu_check_single dm f tf (pc2, pc1) ~> _ THEN @@ -2197,7 +2183,7 @@ Proof. intros (st2 & SEXEC2 & REF2). try_simplify_someHyps. exploit H3; clear H3. 1-3: wlp_simplify. intros (st3 & SEXEC3 & REF3). try_simplify_someHyps. - eexists. split; eauto. + eexists. eexists. split; eauto. split; eauto. intros ctx. eapply hsstate_simu_spec_correct; eauto. Qed. |