Infer nsw/nuw/etc attributes in tgt

[nunoplopes]

#962 is a simple implementation that does 1 query per flag.
It should be implemented in a more generic way, with some abstraction for instructions to advertise the flags they support so we can have a generic flag inference machinery.

cc @dtcxzyw

[dtcxzyw]

Thank you for the comment!
I believe it is a useful feature for LLVM developers to reduce information loss during transformations.
I am willing to implement it. Could you please explain further about how to do it in a "more generic" way?

I used to add a virtual member function to the Instr class and gather SMT expressions they were interested in. But I don't know how to prove them with Z3 :(

TODO list:

• Infer nsw/nuw flags
• Infer nneg flags
• Infer exact flags
• Infer inbounds flags
• Infer disjoint flags ([IR] Add disjoint flag for Or instructions. llvm/llvm-project#72583)
• Infer xxx_is_poison flags for ctlz/cttz/abs
• Drop unused freeze instructions
• Replace logical and/or with the bitwise version

BTW, I think it is also useful to drop some constraints in the src function (e.g., removing noundef attributes). Could you please open an issue for it?

[nunoplopes]

Well, that''s a looong wishlist 😅
Some of those things (like replacing and/or operations) may not be in the realm of Alive itself. They probably should go in a separate tool. Maybe that's what we should do anyway.

The least invasive way of doing this is to add a new operation to all Instr to fetch the supported flags / variations of the instruction. Then we can have a thing on top that calls toSMT() once per flag (modifying the instruction in place). Then that loop on top can create an SMT variable to case split on the which value to use.
It's not as efficient as if toSMT() could itself return all options, but that would require a lot more work. And it's only vcgen time, solving time it would still be optimal.

TL;DR: I think Instr can have a new method that either returns applicable flags, returns an iterator with fresh instructions, or something in between. But the flags thing should be expressive enough to cover most cases you mentioned.