From a345b9ff0ff90a3b90b20c13c472d52361ddcea6 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 4 May 2021 13:06:52 +0200 Subject: builtin case OK, call and tailcall started but not finished --- scheduling/BTLtoRTLproof.v | 30 +++++++++++++++++++++++++++++- 1 file changed, 29 insertions(+), 1 deletion(-) (limited to 'scheduling/BTLtoRTLproof.v') diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 94ec84bf..4595eb83 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -226,6 +226,7 @@ Proof. + inv STAR; try discriminate. eexists; split. eauto. econstructor; eauto. + - inv MI. inv STAR. + inv H5. eexists; split. @@ -237,8 +238,35 @@ Proof. eapply plus_one. eapply exec_Ireturn; eauto. erewrite <- preserv_fnstacksize; eauto. eauto. econstructor; eauto. + - inv MI. + inv STAR. + + inv H5. + pose symbols_preserved as SYMPRES. + destruct ros. + * simpl in H. apply functions_translated in H. + destruct H as (tf & cunit & TFUN & GFIND & LO). + eexists; split. + eapply plus_one. eapply exec_Icall; eauto. + apply function_sig_translated. assumption. + admit. + (* TODO ?? *) + * admit. + + admit. - admit. - - admit. + - inv MI. pose symbols_preserved as SYMPRES. + inv STAR. + + inv H5. eexists; split. + eapply plus_one. eapply exec_Ibuiltin; eauto. + eapply eval_builtin_args_preserved; eauto. + eapply external_call_symbols_preserved; eauto. eapply senv_preserved. + econstructor; eauto. + + inv H5. eexists; split. + eapply plus_trans. eauto. + eapply plus_one. eapply exec_Ibuiltin; eauto. + eapply eval_builtin_args_preserved; eauto. + eapply external_call_symbols_preserved; eauto. eapply senv_preserved. + eauto. econstructor; eauto. +(* Icond *) - admit. - admit. Admitted. -- cgit