[llvm-dev] Undef/poison semantics

[Joe Hendrix via llvm-dev]

Hi,

I'm new to the LLVM mailing list, but I've been working on tools for symbolic execution/formal modeling of LLVM off and on for a while.

I’m trying to understand the current status of the LLVM undef/poison semantics from a frontend/verification perspective.  I saw there was a lot of interest in a proposed semantics in late 2016 and mid-2017.  Perhaps this was due to the “Taming Undefined..."  PLDI paper, which seemed like a nice writeup.  I'd like to formalize this in a theorem prover or Cryptol.

Since the mid 2017 discussion, is there an emerging consensus of the semantics of undef/poison?  If so, is there a newer writeup than the PLDI paper?

The paper semantics in Section 4 on bitvector types "isz” seem reasonable to me.  However, I was surprised by the pointer semantics. I expected each non-poison pointer to be represented by an (allocation id, offset) pair rather than a single bitvector value. My understanding is that LLVM does not define pointer arithmetic between allocations.

I also saw discussion around whether there was a single poison value or whether each bit was potentially poison/non-poison and bitwise operations modeled the more precise behavior.  Is that resolved one way or another?

Regards,
Joe

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: Message signed with OpenPGP
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20180220/d72d443c/attachment.sig>