diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-31 19:02:02 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-31 19:02:02 +0200 |
commit | e4c053f3ddfb8fbea125ba5100293e013900d0b1 (patch) | |
tree | 2c5f041ffb09617a3e377158f801c6e3fc8a8927 /backend | |
parent | 031b1525ad7f27fa67f48ae83b101b5c2b969af7 (diff) | |
download | compcert-kvx-e4c053f3ddfb8fbea125ba5100293e013900d0b1.tar.gz compcert-kvx-e4c053f3ddfb8fbea125ba5100293e013900d0b1.zip |
resolved an "admit"
Diffstat (limited to 'backend')
-rw-r--r-- | backend/Injectproof.v | 23 |
1 files changed, 20 insertions, 3 deletions
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. |