ValueDomain.aptr_of_aval: be more conservative with pointers synthesized from numbers.

For example: *((int *) 0x10000) = 0.  This write used to be treated as not interfering with any load.  With this change, in relaxed value analysis mode, it is treated as interfering with any load except those from the current stack frame.

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 :=