Can we solve equality constraint in `ConstraintElimination` pass

IR & Optimizations
1

I recently got to know the constraint elimination pass which solves simple ineqaulty constraints and implications.

But this passes accepts equality facts and view it as ule predicate, while ignores the equality checks in ConstraintInfo::getConstraintForSolving, here is a example Compiler Explorer

I look through some commit logs but still do not figure out the reasons. Is this somewhat compile-time concerns? If we indeed want to do similar implications, what will be the best practice?

2

Equalities need to be transferred into inequalities, so A == B is modeled as A >= B && A <= B. A the moment, the logic to collect facts supports equalities by simplify adding A >= B and A <= B as facts.

To support simplifying equality predicates, checkAndReplaceCondition (llvm-project/ConstraintElimination.cpp at main · llvm/llvm-project · GitHub) would need updating to check if both A >= B and A <= B is implied by the system using 2 isConditionImplied calls. Patches would be most welcome

3

Thank you for the reply.
I have tried to implement a demo and find some problems.

  1. We use unsigned constraint system for equality constraint, this might miss some cases if the facts is in the signed CS.
  2. We somehow need to generate an extra pair A < B and A > B when we try to imply equality checks are false.

It seems tough to handle these two.

4

You don’t need to handle all possible cases in the initial patch. As for 1. yes that’s true, but there’s a bunch of logic to transfer signed facts to the unsigned system. Facts from equality predicates are added to the unsigned system, so initially it should be fine to just query the unsigned system.

As for 2), I think you should be able to just do CS.isConditionImplied(A >= B) && CS.isConditionImplied(A <=B)?