From e4c053f3ddfb8fbea125ba5100293e013900d0b1 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 31 Mar 2020 19:02:02 +0200 Subject: resolved an "admit" --- backend/Injectproof.v | 23 ++++++++++++++++++++--- 1 file changed, 20 insertions(+), 3 deletions(-) (limited to 'backend/Injectproof.v') diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 93cbdc10..0a53dc9f 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -1174,7 +1174,25 @@ Section INJECTOR. right. exact INr. Qed. - + + Lemma transf_function_preserves_builtin_args: + forall f tf pc rs trs ef res sp m pc' + (args : list (builtin_arg reg)) + (FUN : transf_function gen_injections f = OK tf) + (MATCH : match_regs f rs trs) + (INSTR : (fn_code f) ! pc = Some (Ibuiltin ef args res pc')) + (vargs : list val) + (EVAL : eval_builtin_args ge (fun r => rs#r) sp m args vargs), + eval_builtin_args ge (fun r => trs#r) sp m args vargs. + Proof. + intros. + apply transf_function_preserves_builtin_args_rec with (rs := rs) (ef := ef) (res := res) (pc' := pc'). + intros r INr. + apply MATCH. + apply (max_reg_function_use f pc (Ibuiltin ef args res pc')). + all: auto. + Qed. + Lemma match_regs_write: forall f rs trs res v (MATCH : match_regs f rs trs), @@ -1569,8 +1587,7 @@ Section INJECTOR. *** exact ALTER. *** apply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. - Compute (instr_uses (Ibuiltin ef args res pc')). - (instr_uses + apply transf_function_preserves_builtin_args with (f:=f) (tf:=tf) (pc:=pc) (rs:=rs) (ef:=ef) (res0:=res) (pc':=pc'); auto. *** eapply external_call_symbols_preserved; eauto. apply senv_preserved. ** apply Smallstep.plus_star. exact PLUS. -- cgit