Is this concept of UB as poison actually sound? It seems to me (and I apologize for not using real notation, as I can read a little bit of Lean but I’ve never tried writing it, and my experience writing optimizers is nonexistent):
Suppose we start when an SSA-style function with inputs x and y:
0
And we rewrite it as:
let z = x +nsw y --or anything else that is UB for some input
0
The original code is a function that takes x and y and returns an instance of iN {n}, namely bitvec 0.
The new code also takes any input to bitvec 0, although it may discard a poison value along the way. But this is UB in the C model!
I wonder whether this situation can be avoided by declaring that there is no control flow and that the program representation disallows discarding values. (And select would need to return poison if any argument is poison even if the selector says that the poison is not used.)
This kinda depends on how you model assignments. AFAIK in denotational semantics you usually express them a state update function, taking the previous state of the program and returning a new state with the value for that variable updated to the new one, or an error state if the expression evaluated to `poison`.
It does. But maybe someone should prove (in Lean?) that the lack of flow control is sufficient.
Without a constraint that values aren’t ignored, the lack of flow control is certainly not sufficient, so trying to do this right would require defining (in Lean!) what an expression is.
> Let’s say for moral reasons you choose to link none of LLVM’s libraries (thanks for caring about your users!)
For what moral reasons would I avoid linking LLVM? I’m not familiar.
Is this concept of UB as poison actually sound? It seems to me (and I apologize for not using real notation, as I can read a little bit of Lean but I’ve never tried writing it, and my experience writing optimizers is nonexistent):
Suppose we start when an SSA-style function with inputs x and y:
And we rewrite it as: The original code is a function that takes x and y and returns an instance of iN {n}, namely bitvec 0.The new code also takes any input to bitvec 0, although it may discard a poison value along the way. But this is UB in the C model!
I wonder whether this situation can be avoided by declaring that there is no control flow and that the program representation disallows discarding values. (And select would need to return poison if any argument is poison even if the selector says that the poison is not used.)
This kinda depends on how you model assignments. AFAIK in denotational semantics you usually express them a state update function, taking the previous state of the program and returning a new state with the value for that variable updated to the new one, or an error state if the expression evaluated to `poison`.
iiic the model assumes no flow control, only select.
It does. But maybe someone should prove (in Lean?) that the lack of flow control is sufficient.
Without a constraint that values aren’t ignored, the lack of flow control is certainly not sufficient, so trying to do this right would require defining (in Lean!) what an expression is.