aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--scheduling/BTL.v18
-rw-r--r--scheduling/RTLtoBTL.v2
-rw-r--r--scheduling/RTLtoBTLproof.v57
3 files changed, 35 insertions, 42 deletions
diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index d55a0415..10a000a8 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -833,21 +833,3 @@ Lemma expand_correct ib: forall k,
Proof.
induction ib; simpl; intros; try autodestruct; auto.
Qed.
-
-Lemma expand_None_correct ib:
- is_expand (expand ib None).
-Proof.
- apply expand_correct; simpl; auto.
-Qed.
-
-Definition expand_code (cfg: code): code :=
- (PTree.map (fun _ ib => {| entry:=expand ib.(entry) None; input_regs := ib.(input_regs) |}) cfg).
-
-Lemma expand_code_correct cfg pc ib :
- (expand_code cfg)!pc=Some ib -> is_expand (ib.(entry)).
-Proof.
- unfold expand_code.
- rewrite PTree.gmap.
- destruct (cfg!pc); simpl; intros; try_simplify_someHyps.
- apply expand_None_correct; auto.
-Qed.
diff --git a/scheduling/RTLtoBTL.v b/scheduling/RTLtoBTL.v
index 3617e691..e9319315 100644
--- a/scheduling/RTLtoBTL.v
+++ b/scheduling/RTLtoBTL.v
@@ -12,7 +12,7 @@ Local Open Scope error_monad_scope.
Definition transf_function (f: RTL.function) : res BTL.function :=
let (tcte, dupmap) := rtl2btl f in
let (tc, te) := tcte in
- let f' := BTL.mkfunction (RTL.fn_sig f) (RTL.fn_params f) (RTL.fn_stacksize f) (expand_code tc) te in
+ let f' := BTL.mkfunction (RTL.fn_sig f) (RTL.fn_params f) (RTL.fn_stacksize f) tc te in
do u <- verify_function dupmap f' f;
OK f'.
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index faf0b76c..633e1b8e 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -9,7 +9,6 @@ Require Import Linking.
Record match_function dupmap (f:RTL.function) (tf: BTL.function): Prop := {
dupmap_correct: match_cfg dupmap (fn_code tf) (RTL.fn_code f);
dupmap_entrypoint: dupmap!(fn_entrypoint tf) = Some (RTL.fn_entrypoint f);
- code_expand: forall pc ib, (fn_code tf)!pc=Some ib -> is_expand ib.(entry);
preserv_fnsig: fn_sig tf = RTL.fn_sig f;
preserv_fnparams: fn_params tf = RTL.fn_params f;
preserv_fnstacksize: fn_stacksize tf = RTL.fn_stacksize f
@@ -31,7 +30,6 @@ Lemma verify_function_correct dupmap f f' tt:
fn_sig f' = RTL.fn_sig f ->
fn_params f' = RTL.fn_params f ->
fn_stacksize f' = RTL.fn_stacksize f ->
- (forall pc ib, (fn_code f')!pc=Some ib -> is_expand ib.(entry)) ->
match_function dupmap f f'.
Proof.
unfold verify_function; intro VERIF. monadInv VERIF.
@@ -46,7 +44,6 @@ Proof.
unfold transf_function; unfold bind. repeat autodestruct.
intros H _ _ X. inversion X; subst; clear X.
eexists; eapply verify_function_correct; simpl; eauto.
- eapply expand_code_correct; eauto.
Qed.
Lemma transf_fundef_correct f f':
@@ -243,6 +240,18 @@ Proof.
destruct fi; trivial. inv H. inv H4.
Qed.
+Lemma expand_entry_isnt_goto dupmap f pc ib:
+ match_iblock dupmap (RTL.fn_code f) true pc (expand (entry ib) None) None ->
+ is_goto (expand (entry ib) None) = false.
+Proof.
+ destruct (is_goto (expand (entry ib) None))eqn:EQG.
+ - destruct (expand (entry ib) None);
+ try destruct fi; try discriminate; trivial.
+ intros; inv H; inv H4.
+ - destruct (expand (entry ib) None);
+ try destruct fi; try discriminate; trivial.
+Qed.
+
Lemma list_nth_z_rev_dupmap:
forall dupmap ln ln' (pc pc': node) val,
list_nth_z ln val = Some pc ->
@@ -498,10 +507,10 @@ Proof.
eexists; left; eexists; split.
+ repeat econstructor; eauto.
apply iblock_istep_run_equiv in BTL_RUN; eauto.
- + econstructor. econstructor; eauto.
- eapply code_expand; eauto.
- econstructor.
- eapply entry_isnt_goto; eauto.
+ + econstructor; apply expand_matchiblock_correct in MI.
+ econstructor; eauto. apply expand_correct; trivial.
+ econstructor. apply expand_preserves_iblock_istep_run.
+ eapply expand_entry_isnt_goto; eauto.
- (* Others *)
exists (Some ib2); right; split.
simpl; auto.
@@ -566,11 +575,10 @@ Proof.
pose symbols_preserved as SYMPRES.
eapply eval_builtin_args_preserved; eauto.
eapply external_call_symbols_preserved; eauto. eapply senv_preserved.
- * econstructor; eauto.
- { econstructor; eauto. eapply code_expand; eauto.
- apply star_refl. }
- inversion MI; subst; try_simplify_someHyps.
- inv H3; try_simplify_someHyps.
+ * econstructor; eauto; apply expand_matchiblock_correct in MI.
+ { econstructor; eauto. apply expand_correct; trivial.
+ apply star_refl. apply expand_preserves_iblock_istep_run. }
+ eapply expand_entry_isnt_goto; eauto.
+ (* Bjumptable *)
exploit list_nth_z_rev_dupmap; eauto.
intros (pc'0 & LNZ & DM).
@@ -582,11 +590,10 @@ Proof.
eexists; eexists; split.
eapply iblock_istep_run_equiv in BTL_RUN.
eapply BTL_RUN. econstructor; eauto.
- * econstructor; eauto.
- { econstructor; eauto. eapply code_expand; eauto.
- apply star_refl. }
- inversion MI; subst; try_simplify_someHyps.
- inv H4; try_simplify_someHyps.
+ * econstructor; eauto; apply expand_matchiblock_correct in MI.
+ { econstructor; eauto. apply expand_correct; trivial.
+ apply star_refl. apply expand_preserves_iblock_istep_run. }
+ eapply expand_entry_isnt_goto; eauto.
- (* mib_exit *)
discriminate.
- (* mib_seq *)
@@ -689,11 +696,13 @@ Proof.
eexists; left; eexists; split.
* eapply exec_function_internal.
erewrite preserv_fnstacksize; eauto.
- * econstructor. econstructor; eauto.
- eapply code_expand; eauto.
- 3: eapply entry_isnt_goto; eauto.
+ * apply expand_matchiblock_correct in MI.
+ econstructor. econstructor; eauto.
+ apply expand_correct; trivial.
+ 3: eapply expand_entry_isnt_goto; eauto.
all: erewrite preserv_fnparams; eauto.
constructor.
+ apply expand_preserves_iblock_istep_run.
+ (* External function *)
inv TRANSF.
eexists; left; eexists; split.
@@ -708,9 +717,11 @@ Proof.
apply DMC in DUPLIC as [ib [FNC MI]]; clear DMC.
eexists; left; eexists; split.
+ eapply exec_return.
- + econstructor. econstructor; eauto.
- eapply code_expand; eauto.
- constructor. eapply entry_isnt_goto; eauto.
+ + apply expand_matchiblock_correct in MI.
+ econstructor. econstructor; eauto.
+ apply expand_correct; trivial.
+ constructor. apply expand_preserves_iblock_istep_run.
+ eapply expand_entry_isnt_goto; eauto.
Qed.
Local Hint Resolve plus_one star_refl: core.
generated by cgit (git 2.34.1) at 2024-06-02 15:06:57 +0000