Leverage `instcombine` pass

[shaobo-he]

It seems this pass could produce much simpler LLVM IRs.

[shaobo-he]

I looked into this with a few local experiments. I think the issue is valid, but instcombine is not safe to enable blindly in SMACK's current pipeline.

What I found:

• instcombine can noticeably simplify the LLVM IR before translation. For example, simple arithmetic identities and bitwise no-ops disappear, and that can also remove some warnings from SMACK's later translation.
• The catch is that instcombine is allowed to use LLVM poison/UB semantics. LLVM documents poison as deferred UB: operations such as add nsw overflow produce poison, poison propagates through most instructions, and using poison in places like a branch condition, memory access, divisor, callee, or noundef call/return boundary can trigger immediate UB. freeze is the instruction that turns poison/undef into a stable arbitrary value.
• This is directly related to Modeling LLVM's poison values #717. Since SMACK does not currently model poison generally, running an optimization that exploits poison semantics can hide behavior that SMACK would otherwise see in the unoptimized IR.
• A concrete problematic case is --check=integer-overflow. SMACK currently relies on clang/SMACK instrumentation producing llvm.{s,u}{add,sub,mul}.with.overflow.* intrinsics, which IntegerOverflowChecker recognizes. If instcombine runs before that checker, it can rewrite the code so the direct SMACK overflow checks are lost, leaving UBSan add/sub handlers that SMACK does not currently model as integer-overflow checks.

So my proposal would be:

1. Do not enable instcombine by default.
2. Add it as an opt-in frontend/translation option first, probably with an explicit name such as --llvm-instcombine or as part of an experimental optimization level.
3. Forbid or automatically disable it when --check=integer-overflow is active, unless we first teach IntegerOverflowChecker to handle the relevant UBSan add/sub/mul overflow handlers.
4. Document the poison caveat and link it to Modeling LLVM's poison values #717, because this is a semantic precondition for making LLVM optimization passes generally safe in SMACK.
5. If we want a safer first step, run only very targeted canonicalization passes that we have tested against SMACK's property instrumentation, instead of importing all of instcombine semantics at once.

Relevant LLVM docs:

• https://llvm.org/docs/UndefinedBehavior.html
• https://llvm.org/docs/LangRef.html#poison-values
• https://llvm.org/docs/LangRef.html#freeze-instruction
• https://llvm.org/docs/LangRef.html#add-instruction