From 82c4699c8d5dd12e29b79045b6b8d2daf573ac91 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 Apr 2020 08:27:57 +0200 Subject: now able to inject on Call --- backend/Injectproof.v | 33 +++++++++++++++------------------ 1 file changed, 15 insertions(+), 18 deletions(-) (limited to 'backend/Injectproof.v') diff --git a/backend/Injectproof.v b/backend/Injectproof.v index dfecbac7..1dd26a24 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -1527,22 +1527,22 @@ Section INJECTOR. constructor; auto. constructor; auto. - (* FIXME *) intros. - exists trs1. split. - apply match_regs_refl. - constructor. + destruct (SKIP ts0 sp m0 trs1) as [trs2 [MATCH PLUS]]. + exists trs2. split. assumption. + apply Smallstep.plus_star. exact PLUS. ** replace (trs ## args) with (trs ## (instr_uses (Icall (funsig fd) (inr id) args res pc'))) by reflexivity. rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. apply match_states_call; auto. constructor; auto. constructor; auto. - (* FIXME *) + intros. - exists trs1. split. - apply match_regs_refl. - constructor. + destruct (SKIP ts0 sp m0 trs1) as [trs2 [MATCH PLUS]]. + exists trs2. split. assumption. + apply Smallstep.plus_star. exact PLUS. + + econstructor; split. * eapply Smallstep.plus_one. apply exec_Icall with (args := args) (sig := (funsig fd)) (ros := ros). @@ -1556,21 +1556,18 @@ Section INJECTOR. apply match_states_call; auto. constructor; auto. constructor; auto. - (* FIXME *) - intros. - exists trs1. split. - apply match_regs_refl. - constructor. + + intros. exists trs1. split. + apply match_regs_refl. constructor. + ** replace (trs ## args) with (trs ## (instr_uses (Icall (funsig fd) (inr id) args res pc'))) by reflexivity. rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. apply match_states_call; auto. constructor; auto. constructor; auto. - (* FIXME *) - intros. - exists trs1. split. - apply match_regs_refl. - constructor. + + intros. exists trs1. split. + apply match_regs_refl. constructor. - (* tailcall *) destruct (transf_function_preserves_ros_tail f tf pc rs trs ros args fd (funsig fd) FUN REGS H H0) as [tfd [TFD1 TFD2]]. -- cgit