diff options
| -rw-r--r-- | backend/CSEproof.v | 2 | ||||
| -rw-r--r-- | backend/ValueDomain.v | 18 |
2 files changed, 14 insertions, 6 deletions
diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 74e3ceca..b59078d4 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -696,7 +696,7 @@ Proof. rs#r = Vptr b o -> aaddr approx r = Stk i -> b = sp /\ i = o). { intros until i. unfold aaddr; subst approx. intros. - specialize (H5 r). rewrite H6 in H5. rewrite match_aptr_of_aval in H5. + specialize (H5 r). rewrite H6 in H5. apply match_aptr_of_aval in H5. rewrite H10 in H5. inv H5. split; auto. eapply bc_stack; eauto. } exploit (A rsrc); eauto. intros [P Q]. diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index dbdc6352..626ab526 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -971,20 +971,28 @@ Proof. intros. rewrite vlub_comm. apply vmatch_lub_l; auto. Qed. +(** In the CompCert semantics, a memory load or store succeeds only + if the address is a pointer value. Hence, in strict mode, + [aptr_of_aval x] returns [Pbot] (no pointer value) if [x] + denotes a number or [Vundef]. However, in real code, memory + addresses are sometimes synthesized from integers, e.g. an absolute + address for a hardware device. It is a reasonable assumption + that these absolute addresses do not point within the stack block, + however. Therefore, in relaxed mode, [aptr_of_aval x] returns + [Nonstack] (any pointer outside the stack) when [x] denotes a number. *) + Definition aptr_of_aval (v: aval) : aptr := match v with | Ptr p => p | Ifptr p => p - | _ => Pbot + | _ => if va_strict tt then Pbot else Nonstack end. Lemma match_aptr_of_aval: forall b ofs av, - vmatch (Vptr b ofs) av <-> pmatch b ofs (aptr_of_aval av). + vmatch (Vptr b ofs) av -> pmatch b ofs (aptr_of_aval av). Proof. - unfold aptr_of_aval; intros; split; intros. -- inv H; auto. -- destruct av; ((constructor; assumption) || inv H). + unfold aptr_of_aval; intros. inv H; auto. Qed. Definition vplub (v: aval) (p: aptr) : aptr := |