Value analysis: keep track of pointer values that leak through arithmetic operations with undefined behaviors.

Consider (x ^ 1) ^ 1 where x is a intptr_t containing a pointer value.  "x ^ 1" evaluates to Vundef in the CompCert semantics, hence the value analysis, in strict mode, gives abstract result Ifptr Pbot (= any number but not a pointer).  In relaxed mode, we now give abstract result Ifptr (poffset p) where p is the abstraction of the pointer, thus keeping track of the actual leak of the pointer value.

1 files changed, 3 insertions, 3 deletions

diff --git a/ia32/ValueAOp.v b/ia32/ValueAOp.v
index 53013337..93fd8954 100644
--- a/ia32/ValueAOp.v
+++ b/ia32/ValueAOp.v
@@ -56,8 +56,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   match op, vl with
   | Omove, v1::nil => v1
   | Ointconst n, nil => I n
-  | Ofloatconst n, nil => if propagate_float_constants tt then F n else ftop
-  | Osingleconst n, nil => if propagate_float_constants tt then FS n else ftop
+  | Ofloatconst n, nil => if propagate_float_constants tt then F n else ntop
+  | Osingleconst n, nil => if propagate_float_constants tt then FS n else ntop
   | Oindirectsymbol id, nil => Ifptr (Gl id Int.zero)
   | Ocast8signed, v1 :: nil => sign_ext 8 v1
   | Ocast8unsigned, v1 :: nil => zero_ext 8 v1
@@ -132,7 +132,7 @@ Proof.
   inv VM.
   destruct cond; auto with va.
   inv H0.
-  destruct cond; simpl; eauto with va.
+  destruct cond; simpl; eauto with va.  
   inv H2.
   destruct cond; simpl; eauto with va.
   destruct cond; auto with va.