From 2932b531ceff2cd4573714aeaeb9b4e537d36af8 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 19 Jul 2015 09:29:45 +0200 Subject: 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. --- powerpc/ValueAOp.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'powerpc/ValueAOp.v') diff --git a/powerpc/ValueAOp.v b/powerpc/ValueAOp.v index a5a1db80..8cb29145 100644 --- a/powerpc/ValueAOp.v +++ b/powerpc/ValueAOp.v @@ -51,8 +51,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 | Oaddrsymbol id ofs, nil => Ptr (Gl id ofs) | Oaddrstack ofs, nil => Ptr (Stk ofs) | Ocast8signed, v1 :: nil => sign_ext 8 v1 -- cgit