UB not tracked data-flow-wise

[alivetoolkit]

UB not tracked data-flow-wise

[aqjune]

I find that better UB printing will be very helpful for correctly understanding counter examples; when an input program is too large, what I can do is to just guess which operation raised UB from the values of registers...
How costly will it be if we start to write a code for supporting this? What I immediately see is that there is no explicit mapping from instruction to its UB, which is needed to print the info.

[nunoplopes]

True, vcgen can take some time. The cost is basically track another expression per statement. Instead of just value & poison, we would need store UB as well.
I would wait a bit until we merge @kevindevos' patch, since this work conflicts with his.

[LebedevRI]

Still happens with master.

[nunoplopes]

The root cause of this is that we don't track UB in the data-flow, only in control-flow. This is fine for translation validation, but not sufficient for standalone alive.
With -root-only it verifies just fine, just not with the default per-register verification.

[regehr]

would it be bad to change the default to root-only, and make the other thing available as an option?

[nunoplopes]

I don't know what the overhead would be; didn't try it out.
An alternative to store this information is to repeat symbolic execution when printing a counterexample. Instead of assuming that all functions/optimizations are wrong, we just pay a small price when they are.
The bigger challenge is how to handle undefs. That's the biggest complication.

[aqjune]

If it is related with creation of a unique variable name, would it be helpful if the creation is done by alive2 rather than by Z3_mk_fresh_const?
But one concern that I have is that sometimes vcgen takes pretty long time, and printing counter examples will again take a time because it runs symbolic execution again.
For experiment, we have --succinct flag, so the cost can be hidden.