diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-31 16:51:36 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-31 16:51:36 +0200 |
| commit | 501d6501b9de645843cfa1e1408ba3fe9318223f (patch) | |
| tree | 5bf267f1d08ae92c5548d84b36a0173c6a67e567 /backend/Injectproof.v | |
| parent | e52663259c93ee91a74c57df9ff554d799d42320 (diff) | |
| download | compcert-kvx-501d6501b9de645843cfa1e1408ba3fe9318223f.tar.gz compcert-kvx-501d6501b9de645843cfa1e1408ba3fe9318223f.zip | |
return
Diffstat (limited to 'backend/Injectproof.v')
| -rw-r--r-- | backend/Injectproof.v | 30 |
1 files changed, 29 insertions, 1 deletions
diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 7576fb30..013bc247 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -1584,7 +1584,35 @@ Section INJECTOR. rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. eassumption. * constructor; trivial. - - admit. + - (* return *) + destruct ((gen_injections f) ! pc) eqn:INJECTION. + + exploit transf_function_redirects; eauto. + { eapply max_pc_function_sound; eauto. } + intros [pc_inj [ALTER SKIP]]. + specialize SKIP with (ts := ts) (sp := (Vptr stk Ptrofs.zero)) (m := m) (trs := trs). + destruct SKIP as [trs' [MATCH PLUS]]. + econstructor; split. + * apply Smallstep.plus_one. + apply exec_Ireturn. + exact ALTER. + rewrite stacksize_preserved with (f:=f); eassumption. + * destruct or as [r | ]; simpl. + ** replace (trs # r) with (hd Vundef (trs ## (instr_uses (Ireturn (Some r))))) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + constructor; auto. + ** constructor; auto. + + econstructor; split. + * apply Smallstep.plus_one. + apply exec_Ireturn. + rewrite transf_function_preserves with (f:=f); eauto. + eapply max_pc_function_sound; eauto. + rewrite stacksize_preserved with (f:=f); eassumption. + * destruct or as [r | ]; simpl. + ** replace (trs # r) with (hd Vundef (trs ## (instr_uses (Ireturn (Some r))))) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + constructor; auto. + ** constructor; auto. + - admit. - admit. - admit. |