diff options
Diffstat (limited to 'scheduling/RTLpathSchedulerproof.v')
| -rw-r--r-- | scheduling/RTLpathSchedulerproof.v | 35 |
1 files changed, 26 insertions, 9 deletions
diff --git a/scheduling/RTLpathSchedulerproof.v b/scheduling/RTLpathSchedulerproof.v index a9c2fa76..03554f9c 100644 --- a/scheduling/RTLpathSchedulerproof.v +++ b/scheduling/RTLpathSchedulerproof.v @@ -281,6 +281,7 @@ Proof. unfold inst_checker. destruct i; simpl in *; unfold exit_checker; try discriminate. all: + try destruct Pos.eq_dec; simpl; try destruct (list_mem _ _); simpl; try (destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence; fail). 4,5: @@ -302,17 +303,27 @@ Proof. inversion_SOME p. 2: { destruct (Regset.subset _ _) eqn:?; try congruence. } destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence. - 2: { destruct (Regset.subset (pre_output_regs path0) alive) eqn:?; try congruence. } - simpl. + 2: { + destruct (Regset.subset (pre_output_regs path0) alive) eqn:?; try congruence; + destruct ((fn_path f) ! n); intros; try discriminate. + all: inversion SIEXEC; simpl; auto. + all: destruct Regset.subset in ICHK0; try discriminate; + destruct Regset.subset in ICHK0; try discriminate; + simpl in ICHK0. + all: destruct PTree.get eqn:GET in ICHK0; try discriminate. + all: destruct Regset.subset eqn:SUBS_PATH0 in ICHK0; try discriminate. + all: econstructor; eauto. + all: eapply eqlive_reg_monotonic; eauto. + all: destruct (Regset.subset (input_regs p0) (pre_output_regs path0)) eqn:SUB_PATH; try congruence. + all: intros; apply Regset.subset_2 in SUB_PATH. + all: unfold Regset.Subset in SUB_PATH; apply SUB_PATH in H; auto. } + intros; simpl. destruct (Regset.subset (pre_output_regs path0) alive) eqn:SUB_ALIVE'; try congruence. - inversion_SOME p'. - destruct (Regset.subset (input_regs p') (pre_output_regs path0)) eqn:SUB_PATH; try congruence. - intros NPATH NPATH' _. econstructor; eauto. - instantiate (1:=p'). rewrite <- NPC; auto. - eapply eqlive_reg_monotonic; eauto; simpl. - intros. apply Regset.subset_2 in SUB_PATH. + destruct (Regset.subset (input_regs p) (pre_output_regs path0)) eqn:SUB_PATH; try congruence. + apply Regset.subset_2 in SUB_PATH. unfold Regset.Subset in SUB_PATH. - apply SUB_PATH in H; auto. + econstructor; eauto. { rewrite <- NPC; eauto. } + eapply eqlive_reg_monotonic; eauto. Qed. Lemma pre_output_regs_correct f pc0 path0 stk stk' sp (st:sstate) rs0 m0 t s is rs': @@ -376,6 +387,12 @@ Proof. exploit exit_checker_eqlive_builtin_res; eauto. intros. destruct H as [p [PATH EQLIVE']]. econstructor; eauto. + + (* Icond *) + eexists; split. + * econstructor. + * generalize ICHK. + unfold inst_checker; simpl in *. + destruct Pos.eq_dec; destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence. + (* Sjumptable *) eexists; split. * econstructor; eauto. |