diff options
Diffstat (limited to 'scheduling/RTLpath.v')
| -rw-r--r-- | scheduling/RTLpath.v | 25 |
1 files changed, 16 insertions, 9 deletions
diff --git a/scheduling/RTLpath.v b/scheduling/RTLpath.v index b29a7759..97187ca8 100644 --- a/scheduling/RTLpath.v +++ b/scheduling/RTLpath.v @@ -54,7 +54,9 @@ Definition default_succ (i: instruction): option node := Definition early_exit (i: instruction): option node := (* FIXME: for jumptable, replace [node] by [list node] *) match i with - | Icond cond args ifso ifnot _ => Some ifso + | Icond cond args ifso ifnot _ => + if Pos.eq_dec ifso ifnot then None + else Some ifso | _ => None end. @@ -170,7 +172,10 @@ Definition istep (ge: RTL.genv) (i: instruction) (sp: val) (rs: regset) (m: mem) Some (mk_istate true pc' rs m') | Icond cond args ifso ifnot _ => SOME b <- eval_condition cond rs##args m IN - Some (mk_istate (negb b) (if b then ifso else ifnot) rs m) + if Pos.eq_dec ifso ifnot then + Some (mk_istate true (if b then ifso else ifnot) rs m) + else + Some (mk_istate (negb b) (if b then ifso else ifnot) rs m) | _ => None (* TODO jumptable ? *) end. @@ -398,8 +403,8 @@ Lemma istep_correct ge i stack (f:function) sp rs m st : forall pc, (fn_code f)!pc = Some i -> RTL.step ge (State stack f sp pc rs m) E0 (State stack f sp st.(ipc) st.(irs) st.(imem)). Proof. - destruct i; simpl; try congruence; simplify_SOME x. - 1-3: explore_destruct; simplify_SOME x. + destruct i; simpl; try congruence; simplify_SOME x; + try (explore_destruct; simplify_SOME x). Qed. Local Hint Resolve star_refl: core. @@ -648,6 +653,7 @@ Lemma istep_normal_exit ge i sp rs m st: Proof. destruct i; simpl; try congruence; simplify_SOME x. all: explore_destruct; simplify_SOME x. + discriminate. Qed. Lemma isteps_normal_exit ge path f sp: forall rs m pc st, @@ -728,7 +734,7 @@ Qed. (* FIXME - add prediction *) Inductive is_early_exit pc: instruction -> Prop := | Icond_early_exit cond args ifnot predict: - is_early_exit pc (Icond cond args pc ifnot predict) + pc <> ifnot -> is_early_exit pc (Icond cond args pc ifnot predict) . (* TODO add jumptable here ? *) Lemma istep_early_exit ge i sp rs m st : @@ -826,8 +832,7 @@ Lemma istep_complete t i stack f sp rs m pc s': t = E0 /\ exists st, istep ge i sp rs m = Some st /\ s'=(State stack f sp st.(ipc) st.(irs) st.(imem)). Proof. intros H X; inversion H; simpl; subst; try rewrite X in * |-; clear X; simplify_someHyps; try congruence; - (split; auto); simplify_someHyps; eexists; split; simplify_someHyps; eauto. - all: explore_destruct; simplify_SOME a. + (split; auto); simplify_someHyps; intros; explore_destruct; eexists; split; simplify_someHyps; eauto. Qed. Lemma stuttering path idx stack f sp rs m pc st t s1': @@ -958,8 +963,10 @@ Proof. unfold nth_default_succ_inst in Hi'. erewrite isteps_normal_exit in Hi'; eauto. clear pc' Hpc' STEP0 PSTEP0 BOUND0; try_simplify_someHyps; intros. - destruct EARLY_EXIT as [cond args ifnot]; simpl in ENTRY; - destruct (initialize_path (*fn_code f*) (fn_path f) pc0); eauto. + destruct EARLY_EXIT as [cond args ifnot]; simpl in ENTRY. + destruct Pos.eq_dec in ENTRY. + - contradiction. + - destruct (initialize_path (*fn_code f*) (fn_path f) pc0); eauto. } destruct HPATH0 as (path1 & Hpath1). destruct (path1.(psize)) as [|ps] eqn:Hpath1size. |