diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-06 23:46:15 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-06 23:46:15 +0200 |
commit | 75109076ec027675e297ff1273660fc6b5a5f239 (patch) | |
tree | 121a5ae341841599723c0dc9f8e1c033bbe72950 /x86 | |
parent | e64b9464fb6662bf63ac255eca94d17d572c9d81 (diff) | |
download | compcert-kvx-75109076ec027675e297ff1273660fc6b5a5f239.tar.gz compcert-kvx-75109076ec027675e297ff1273660fc6b5a5f239.zip |
for nontrap
Diffstat (limited to 'x86')
-rw-r--r-- | x86/Op.v | 28 |
1 files changed, 28 insertions, 0 deletions
@@ -1199,6 +1199,21 @@ Proof. unfold eval_addressing; intros. destruct Archi.ptr64; eauto using eval_addressing32_inj, eval_addressing64_inj. Qed. +Lemma eval_addressing_inj_none: + forall addr sp1 vl1 sp2 vl2, + (forall id ofs, + In id (globals_addressing addr) -> + Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> + Val.inject f sp1 sp2 -> + Val.inject_list f vl1 vl2 -> + eval_addressing ge1 sp1 addr vl1 = None -> + eval_addressing ge2 sp2 addr vl2 = None. +Proof. + intros until vl2. intros Hglobal Hinjsp Hinjvl. + destruct addr; simpl in *; + inv Hinjvl; trivial; try discriminate; inv H0; trivial; try discriminate; inv H2; trivial; try discriminate. +Qed. + Lemma eval_operation_inj: forall op sp1 vl1 sp2 vl2 v1, (forall id ofs, @@ -1425,6 +1440,19 @@ Proof. destruct H1 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto. Qed. +Lemma eval_addressing_lessdef_none: + forall sp addr vl1 vl2, + Val.lessdef_list vl1 vl2 -> + eval_addressing genv sp addr vl1 = None -> + eval_addressing genv sp addr vl2 = None. +Proof. + intros until vl2. intros Hlessdef Heval1. + destruct addr; simpl in *; + inv Hlessdef; trivial; try discriminate; + inv H0; trivial; try discriminate; + inv H2; trivial; try discriminate. +Qed. + End EVAL_LESSDEF. (** Compatibility of the evaluation functions with memory injections. *) |