diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-01 08:27:57 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-01 08:27:57 +0200 |
| commit | 82c4699c8d5dd12e29b79045b6b8d2daf573ac91 (patch) | |
| tree | 28817dc1b0a5c19c1aab31acbd98d6aac2f042a9 /backend/Injectproof.v | |
| parent | 87a4d7e9f493876821e26548d379132f16a7a8ea (diff) | |
| download | compcert-kvx-82c4699c8d5dd12e29b79045b6b8d2daf573ac91.tar.gz compcert-kvx-82c4699c8d5dd12e29b79045b6b8d2daf573ac91.zip | |
now able to inject on Call
Diffstat (limited to 'backend/Injectproof.v')
| -rw-r--r-- | backend/Injectproof.v | 33 |
1 files changed, 15 insertions, 18 deletions
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]]. |