Hello! I’m studying how llvm.assume statements are internally represented. I can see that llvm can simplify simple arithmetic expressions such as x * (x+1) == 2 used in assumptions and infer x == 1 (x is u32) godbolt, but I wonder where in the codebase this happens.
Thanks for any pointers!
Assume is used in many places. The above transformation is likely in instcombine or gvn.
The easiest way to find almost all assumption users is to look for the passes that query “AssumptionAnalysis”. Though, some might not actually use assumptions.
~ J
Thank you. I also came across ValueTracking, which has an SMT-solver like interface - can one use ValueTracking to reason about arbitrary SSA registers?
I don’t understand the question. I would also recommend to forget about “SSA registers” and treat them as “values”. “registers” often leads to wrong conclusions.
ValueTracking follows def-use chains, but it’s unclear what exactly you are trying to achieve.
This isn’t an area I’m familiar with but lib/Analysis/AssumptionCache.cpp might be of interest to you