From 7209e1ba8c6ae100922601b88a9faba5a7ce752f Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 15 Feb 2021 11:16:05 +0100 Subject: [Broken version] Intermediate local commit: pre_output_regs_correct proved --- scheduling/RTLpathSchedulerproof.v | 45 ++++++++++++++++++++++++-------------- 1 file changed, 28 insertions(+), 17 deletions(-) (limited to 'scheduling') 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: -- cgit