diff options
Diffstat (limited to 'scheduling')
-rw-r--r-- | scheduling/RTLpathSchedulerproof.v | 45 |
1 files changed, 28 insertions, 17 deletions
diff --git a/scheduling/RTLpathSchedulerproof.v b/scheduling/RTLpathSchedulerproof.v index 8d2eff6d..2f917096 100644 --- a/scheduling/RTLpathSchedulerproof.v +++ b/scheduling/RTLpathSchedulerproof.v @@ -381,12 +381,16 @@ Proof. * econstructor; eauto. * econstructor; eauto. econstructor; eauto. + (* wf *) + generalize ICHK. + unfold inst_checker; simpl in *. + destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence. + destruct (list_mem _ _); try congruence. + destruct (reg_sum_mem _ _); try congruence. + intros EXIT. + exploit exit_checker_eqlive_ext1; eauto. + intros. destruct H as [p [PATH EQLIVE']]. econstructor; eauto. - - admit. (* wf *) - - intros; eapply eqlive_reg_update. - (* TODO: condition sur pre_output_regs a revoir *) - eapply eqlive_reg_monotonic; eauto; simpl. - admit. + (* Stailcall *) eexists; split. * econstructor; eauto. @@ -394,25 +398,32 @@ Proof. + (* Sbuiltin *) eexists; split. * econstructor; eauto. - * econstructor; eauto. - - admit. (* wf *) - - (* TODO: condition sur pre_output_regs a voir *) - (* NB: cas du [regmap_setres] à traiter *) - admit. + * (* wf *) + generalize ICHK. + unfold inst_checker; simpl in *. + destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence. + destruct (list_mem _ _); try congruence. + intros EXIT. + exploit exit_checker_eqlive_builtin_res; eauto. + intros. destruct H as [p [PATH EQLIVE']]. + econstructor; eauto. + (* Sjumptable *) eexists; split. * econstructor; eauto. - * econstructor; eauto. - - admit. (* wf *) - - (* TODO: condition sur pre_output_regs a revoir *) - eapply eqlive_reg_monotonic; eauto; simpl. - admit. + * (* wf *) + generalize ICHK. + unfold inst_checker; simpl in *. + destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence. + destruct (Regset.mem _ _); try congruence. + destruct (exit_list_checker _ _ _) eqn:EQL; try congruence. + exploit exit_list_checker_eqlive; eauto. + intros. destruct H as [p [PATH EQLIVE']]. + econstructor; eauto. + (* Sreturn *) eexists; split. * econstructor; eauto. * econstructor; eauto. -Admitted. - +Qed. (* The main theorem on simulation of symbolic states ! *) Theorem ssem_sstate_simu dm f f' pc0 path0 stk stk' sp st st' rs m t s: |