diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-31 16:40:52 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-31 16:40:52 +0200 |
| commit | e52663259c93ee91a74c57df9ff554d799d42320 (patch) | |
| tree | c6eddddeae25eb44c25273ef22ee3c4480f27e40 /backend/Injectproof.v | |
| parent | e55776fd96f78518da49dfa9e856c3e070353fc9 (diff) | |
| download | compcert-kvx-e52663259c93ee91a74c57df9ff554d799d42320.tar.gz compcert-kvx-e52663259c93ee91a74c57df9ff554d799d42320.zip | |
jumptable
Diffstat (limited to 'backend/Injectproof.v')
| -rw-r--r-- | backend/Injectproof.v | 23 |
1 files changed, 22 insertions, 1 deletions
diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 11472c0e..7576fb30 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -1562,7 +1562,28 @@ Section INJECTOR. *** reflexivity. ** constructor; auto. - - admit. + - 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 := sp) (m := m) (trs := trs). + destruct SKIP as [trs' [MATCH PLUS]]. + econstructor; split. + * apply Smallstep.plus_one. + apply exec_Ijumptable with (arg := arg) (tbl := tbl) (n := n); trivial. + replace (trs # arg) with (hd Vundef (trs ## (instr_uses (Ijumptable arg tbl)))) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + eassumption. + * constructor; trivial. + + econstructor; split. + * apply Smallstep.plus_one. + apply exec_Ijumptable with (arg := arg) (tbl := tbl) (n := n); trivial. + rewrite transf_function_preserves with (f:=f); eauto. + eapply max_pc_function_sound; eauto. + replace (trs # arg) with (hd Vundef (trs ## (instr_uses (Ijumptable arg tbl)))) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + eassumption. + * constructor; trivial. - admit. - admit. - admit. |