From f1a409ffe3a84f1eb6e4027a46d366a7942be0ae Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 14 Mar 2020 06:39:49 +0100 Subject: Icall --- backend/CSE3proof.v | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) (limited to 'backend/CSE3proof.v') diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 9ddd6ba2..54c96cbf 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -592,7 +592,19 @@ Proof. + eapply exec_Icall; try eassumption. * TR_AT. reflexivity. * apply sig_preserved; auto. - + admit. + + rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial. + assert (wt_instr f tenv (Icall (funsig fd) ros args res pc')) as WTcall by eauto with wt. + inv WTcall. + constructor; trivial. + * econstructor; eauto. + ** rewrite sig_preserved with (f:=fd); assumption. + ** intros. + IND_STEP. + apply kill_reg_sound; eauto with cse3. + eapply kill_mem_sound; eauto with cse3. + * rewrite sig_preserved with (f:=fd) by trivial. + rewrite <- H7. + apply wt_regset_list; auto. - (* Itailcall *) destruct (find_function_translated ros rs fd H0) as [tfd [HTFD1 HTFD2]]. econstructor. split. -- cgit