diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-31 18:56:17 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-31 18:56:17 +0200 |
| commit | 031b1525ad7f27fa67f48ae83b101b5c2b969af7 (patch) | |
| tree | 643d92de983a41a47e14f2202deeb9d7010d20de /backend/Injectproof.v | |
| parent | cc2d5def041128ae6dcbf46455db3341e74e995c (diff) | |
| download | compcert-kvx-031b1525ad7f27fa67f48ae83b101b5c2b969af7.tar.gz compcert-kvx-031b1525ad7f27fa67f48ae83b101b5c2b969af7.zip | |
more about builtin args
Diffstat (limited to 'backend/Injectproof.v')
| -rw-r--r-- | backend/Injectproof.v | 84 |
1 files changed, 83 insertions, 1 deletions
diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 2bfd9701..93cbdc10 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -1094,6 +1094,87 @@ Section INJECTOR. apply SAME. right. assumption. Qed. + (* + Lemma transf_function_preserves_builtin_arg: + forall rs trs ef res sp m pc' + (arg : builtin_arg reg) + (SAME : (forall r, + In r (instr_uses (Ibuiltin ef args res pc')) -> + trs # r = rs # r) ) + varg + (EVAL : eval_builtin_arg ge (fun r => rs#r) sp m arg varg), + eval_builtin_arg ge (fun r => trs#r) sp m arg varg. + Proof. + *) + + Lemma transf_function_preserves_builtin_args_rec: + forall rs trs ef res sp m pc' + (args : list (builtin_arg reg)) + (SAME : (forall r, + In r (instr_uses (Ibuiltin ef args res pc')) -> + trs # r = rs # r) ) + (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. + unfold eval_builtin_args. + induction args; intros; inv EVAL. + - constructor. + - constructor. + + induction H1. + all: try (constructor; auto; fail). + * rewrite <- SAME. + apply eval_BA. + simpl. + left. reflexivity. + * constructor. + ** apply IHeval_builtin_arg1. + intros r INr. + apply SAME. + simpl. + simpl in INr. + rewrite in_app in INr. + rewrite in_app. + rewrite in_app. + tauto. + ** apply IHeval_builtin_arg2. + intros r INr. + apply SAME. + simpl. + simpl in INr. + rewrite in_app in INr. + rewrite in_app. + rewrite in_app. + tauto. + * constructor. + ** apply IHeval_builtin_arg1. + intros r INr. + apply SAME. + simpl. + simpl in INr. + rewrite in_app in INr. + rewrite in_app. + rewrite in_app. + tauto. + ** apply IHeval_builtin_arg2. + intros r INr. + apply SAME. + simpl. + simpl in INr. + rewrite in_app in INr. + rewrite in_app. + rewrite in_app. + tauto. + + apply IHargs. + 2: assumption. + intros r INr. + apply SAME. + simpl. + apply in_or_app. + right. + exact INr. + Qed. + Lemma match_regs_write: forall f rs trs res v (MATCH : match_regs f rs trs), @@ -1488,7 +1569,8 @@ Section INJECTOR. *** exact ALTER. *** apply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. - admit. + Compute (instr_uses (Ibuiltin ef args res pc')). + (instr_uses *** eapply external_call_symbols_preserved; eauto. apply senv_preserved. ** apply Smallstep.plus_star. exact PLUS. |