diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-15 11:16:05 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-15 11:16:05 +0100 |
| commit | 7209e1ba8c6ae100922601b88a9faba5a7ce752f (patch) | |
| tree | 88b3dae29557108ed8216419210cbc6b51d0a20c /scheduling | |
| parent | 6099970964c478fae9672178c750623369c84e31 (diff) | |
| download | compcert-kvx-7209e1ba8c6ae100922601b88a9faba5a7ce752f.tar.gz compcert-kvx-7209e1ba8c6ae100922601b88a9faba5a7ce752f.zip | |
[Broken version] Intermediate local commit: pre_output_regs_correct proved
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: |