Undef/poison semantics


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?