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>
