Tuning up constraint elimination?

regehr · November 18, 2024, 10:46pm

constraint elimination is a super impressive pass but there are some holes in what it’s able to do, often apparently related to our canonicalization choices. for example at present it cannot prove that this assert is unreachable:

void f(long a, long b, long c) {
  if (a>b)
    if (b>c)
      assert(a>c);
}

the IR at the relevant point is:

define void @f(i64 noundef %a, i64 noundef %b, i64 noundef %c) {
entry:
  %cmp = icmp sle i64 %a, %b
  %cmp1 = icmp sle i64 %b, %c
  %or.cond.not11 = or i1 %cmp, %cmp1
  %cmp3 = icmp sgt i64 %a, %c
  %or.cond10 = or i1 %cmp3, %or.cond.not11
  br i1 %or.cond10, label %if.end6, label %if.else

if.else:                                          ; preds = %entry
  tail call void @__assert_fail(ptr noundef nonnull @.str, ptr noundef nonnull @.str.1, i32 noundef 6, ptr noundef nonnull @__PRETTY_FUNCTION__.f) #2
  unreachable

if.end6:                                          ; preds = %entry
  ret void
}

there’s more like this, that’s seemingly well within the purview of this pass, that we don’t optimize. I’ve been looking for these examples using a little script that generates a constraint system and then – if it can be optimized away, according to Alive – uses llvm-reduce to come up with a minimal driver for that particular missed optimization.

is anyone interested in working on this? I would be happy to help, particularly with doing an ongoing search for missed optimizations. if this sounds fun for someone, I can start posting these in our issue tracker.

(edit: I can’t prove that this work will matter, but my strong suspicion is that at a time when there’s a lot of interest in safe languages – that tend to generate a lot of unsatisfiable constraints of the kind that this pass can eliminate – it is in our community’s interests to thoroughly and predictably do this job, for the class of constraints that this pass is designed to attack)

amara · November 19, 2024, 7:19am

@fhahn

fhahn · November 20, 2024, 11:16am

That would be super useful! Its effectiveness heavily depends on being able to decompose (canonical) LLVM IR expressions to constraints.

Finding such cases automatically would be great, I think there would be a number of people interested in fixing those. Filing issues would be a good start, I’d be happy to help people submit fixes.

regehr · November 21, 2024, 3:43am

ok, here’s one! I don’t want to load up the system with these so I’ll go slowly here and also I’ll try to keep these within the set of stuff that we pretty clearly want to support. also, some students in my advanced compilers class are looking at these so perhaps we’ll get some help!

github.com/llvm/llvm-project

signed comparison case missed by constraint elimination

opened 03:39AM - 21 Nov 24 UTC

regehr

llvm:optimizations missed-optimization

starting with this: ```c extern void side_effect(void); void f(int v0, int …v1, int v2) { if (v0 < v1) return; if (v1 < v2) return; if (v0 < v2) side_effect(); return; } ``` here's what constraint elimination sees: ```llvm define void @f(i32 noundef %v0, i32 noundef %v1, i32 noundef %v2) { entry: %cmp = icmp sge i32 %v0, %v1 %cmp1 = icmp sge i32 %v1, %v2 %or.cond.not11 = and i1 %cmp, %cmp1 %cmp4 = icmp slt i32 %v0, %v2 %or.cond10 = and i1 %cmp4, %or.cond.not11 br i1 %or.cond10, label %if.then5, label %return if.then5: ; preds = %entry tail call void @side_effect() #2 br label %return return: ; preds = %if.then5, %entry ret void } ``` this should all optimize away: https://alive2.llvm.org/ce/z/EPLL_9 but it doesn't: https://gcc.godbolt.org/z/enxd5dqxr the debug output looks sensible, the relations that we want are getting picked up by the constraint system, but I'm not deeply enough into the code to see where we're going wrong ``` Processing condition to simplify: %cmp = icmp sge i32 %v0, %v1 Checking %cmp = icmp sge i32 %v0, %v1 --- %v0 + -1 * %v1 <= -1 sat --- -1 * %v0 + %v1 <= 0 sat Adding 'icmp sge i32 %v1, %v2' constraint: -1 * %v1 + %v2 <= 0 Checking %cmp = icmp sge i32 %v0, %v1 --- -1 * %v1 + %v2 <= 0 %v0 + -1 * %v1 <= -1 sat --- -1 * %v1 + %v2 <= 0 -1 * %v0 + %v1 <= 0 sat Processing condition to simplify: %cmp1 = icmp sge i32 %v1, %v2 Checking %cmp1 = icmp sge i32 %v1, %v2 --- %v1 + -1 * %v2 <= -1 sat --- -1 * %v1 + %v2 <= 0 sat Adding 'icmp sge i32 %v0, %v1' constraint: -1 * %v0 + %v1 <= 0 Checking %cmp1 = icmp sge i32 %v1, %v2 --- -1 * %v0 + %v1 <= 0 %v1 + -1 * %v2 <= -1 sat --- -1 * %v0 + %v1 <= 0 -1 * %v1 + %v2 <= 0 sat Processing condition to simplify: %cmp4 = icmp slt i32 %v0, %v2 Checking %cmp4 = icmp slt i32 %v0, %v2 --- -1 * %v0 + %v2 <= 0 sat --- %v0 + -1 * %v2 <= -1 sat Processing fact to add to the system: icmp slt i32 %v0, %v2 Adding 'icmp slt i32 %v0, %v2' constraint: %v0 + -1 * %v2 <= -1 --- %v0 + -1 * %v2 <= -1 %v0 <= -1 sat Top of stack : 1 2 CB: 1 2 Processing fact to add to the system: icmp sge i32 %v0, %v1 Adding 'icmp sge i32 %v0, %v1' constraint: -1 * %v0 + %v1 <= 0 --- %v0 + -1 * %v2 <= -1 -1 * %v0 + %v1 <= 0 %v1 <= -1 sat Top of stack : 1 2 CB: 1 2 Processing fact to add to the system: icmp sge i32 %v1, %v2 Adding 'icmp sge i32 %v1, %v2' constraint: -1 * %v1 + %v2 <= 0 --- %v0 + -1 * %v2 <= -1 -1 * %v0 + %v1 <= 0 -1 * %v1 + %v2 <= 0 %v2 <= -1 unsat Adding 'icmp uge i32 %v1, %v2' constraint: -1 * %v1 + %v2 <= 0 ``` cc @fhahn

dtcxzyw · November 21, 2024, 3:53am

I am willing to do this. I used to write a tool that extracts boolean expressions from an LLVM IR corpus and use Alive2 to check whether they are tautology or unsatisfiable: llvm-tools/deadcode.cpp at main · dtcxzyw/llvm-tools · GitHub
It has discovered some missed optimization opportunities: Issues · dtcxzyw/llvm-tools · GitHub

I think it is easy to extend the tool to support dominating conditions.

regehr · November 21, 2024, 4:25am

sounds good! I also have a tool that looks for missing stuff (also using Alive) so maybe we can both look for things here

caydenlund · November 21, 2024, 5:24am

I’d love to work on this! It seems like a good first issue. I’m one of John’s advanced compilers students.

regehr · November 21, 2024, 5:29am

looks like @dtcxzyw has signed up for it already but there are a bunch more where this came from!

fhahn · November 22, 2024, 10:16am

Very excited to see more of those cases! I’d expect some of them to be quite good for people starting to contribute to LLVM

dtcxzyw · November 26, 2024, 4:50am

Update: I have updated my script to support dominating conditions and assumptions. Alive2 reported 778 redundant branches on ir snippets extracted from my real-world llvm ir corpus.

An example: [InstSimplify] Missed optimization: `X != Y` implies `X | Y != 0` · Issue #117436 · llvm/llvm-project · GitHub
I will file more interesting issues after deduplication

regehr · November 28, 2024, 3:52am

ok! here’s another one, where we don’t eliminate a constraint, this time the root cause appears to be not adding constraints that come from icmp eq and icmp ne:

github.com/llvm/llvm-project

constraint elimination missing a case related to != and ==

opened 03:51AM - 28 Nov 24 UTC

regehr

missed-optimization llvm:transforms

consider this code: ```c extern void side_effect(void); void f(int v0, int v1, i…nt v2) { if (v2 != v0) return; if (v0 < v1) return; if (v1 > v2) side_effect(); } ``` we compile this to: ```llvm define void @f(i32 noundef %v0, i32 noundef %v1, i32 noundef %v2) { entry: %cmp.not = icmp eq i32 %v2, %v0 %cmp1 = icmp sge i32 %v0, %v1 %or.cond.not11 = and i1 %cmp1, %cmp.not %cmp4 = icmp sgt i32 %v1, %v2 %or.cond10 = and i1 %cmp4, %or.cond.not11 br i1 %or.cond10, label %if.then5, label %if.end6 if.then5: ; preds = %entry tail call void @side_effect() #2 br label %if.end6 if.end6: ; preds = %entry, %if.then5 ret void } ``` but that last conditional is always false: https://alive2.llvm.org/ce/z/LaLygS this issue seems to involve both `icmp eq` and `icmp ne`: https://gcc.godbolt.org/z/MK4xhMna6 cc @fhahn @dtcxzyw

regehr · November 29, 2024, 5:10pm

and here’s an orthogonal one where a canonicalization is obscuring the constraints that we need to be picking up:

github.com/llvm/llvm-project

constraint elimination should understand the (x<0)&&(y<0) => (x|y)<0 canonicalization

opened 05:08PM - 29 Nov 24 UTC

regehr

missed-optimization llvm:transforms

here's a function: ```c extern void side_effect(void); void f(int v1, int v2) {… if (v1 < 0) return; if (v2 < 0) return; if (v2 > -5) return; side_effect(); } ``` at present, we're not optimizing this away. the IR is: ```lllvm define void @f(i32 noundef %v1, i32 noundef %v2) { entry: %0 = or i32 %v2, %v1 %or.cond = icmp slt i32 %0, 0 %cmp4 = icmp sgt i32 %v2, -5 %or.cond7 = or i1 %cmp4, %or.cond br i1 %or.cond7, label %return, label %if.end6 if.end6: ; preds = %entry tail call void @side_effect() #2 br label %return return: ; preds = %entry, %if.end6 ret void } ``` constraint elimination is correctly learning that `!(%0 < 0)` but I guess we need a little recognizer for the `(x<0)&&(y<0) => (x|y)<0` canonicalization ``` Processing condition to simplify: %or.cond = icmp slt i32 %0, 0 Checking %or.cond = icmp slt i32 %0, 0 failed to decompose condition Adding 'icmp sle i32 %v2, -5' constraint: %v2 <= -5 Checking %or.cond = icmp slt i32 %0, 0 failed to decompose condition Processing condition to simplify: %cmp4 = icmp sgt i32 %v2, -5 Checking %cmp4 = icmp sgt i32 %v2, -5 --- %v2 <= -5 sat --- -1 * %v2 <= 4 sat Adding 'icmp sge i32 %0, 0' constraint: -1 * %0 <= 0 Checking %cmp4 = icmp sgt i32 %v2, -5 --- -1 * %0 <= 0 %v2 <= -5 sat --- -1 * %0 <= 0 -1 * %v2 <= 4 sat Processing fact to add to the system: icmp sle i32 %v2, -5 Adding 'icmp sle i32 %v2, -5' constraint: %v2 <= -5 Top of stack : 3 4 CB: 3 4 Processing fact to add to the system: icmp sge i32 %0, 0 Adding 'icmp sge i32 %0, 0' constraint: -1 * %0 <= 0 Adding 'icmp uge i32 %0, 0' constraint: -1 * %0 <= 0 ``` cc @fhahn @dtcxzyw

dtcxzyw · December 1, 2024, 1:44pm

I have checked all the missed-optimization reports generated by my tool.
Here are some interesting frequently used patterns:

github.com/llvm/llvm-project

[InstSimplify] Missed optimization: `X != Y` implies `X | Y != 0`

opened 03:12PM - 23 Nov 24 UTC

dtcxzyw

missed-optimization llvm:transforms

Proof: https://alive2.llvm.org/ce/z/cJ75Ya ``` define i1 @src(i8 %x, i8 %y) { … entry: %cond = icmp ne i8 %x, %y br i1 %cond, label %if.then, label %if.else if.then: %or = or i8 %x, %y %cmp = icmp eq i8 %or, 0 ret i1 %cmp if.else: ret i1 false } define i1 @tgt(i8 %x, i8 %y) { entry: %cond = icmp ne i8 %x, %y br i1 %cond, label %if.then, label %if.else if.then: ret i1 false if.else: ret i1 false } ``` See also https://github.com/dtcxzyw/llvm-tools/issues/32 and https://discourse.llvm.org/t/tuning-up-constraint-elimination/83213/5?u=dtcxzyw.

github.com/llvm/llvm-project

[KnownBits] `(Trunc X) != 1` implies `X != 1`

opened 04:09PM - 29 Nov 24 UTC

dtcxzyw

missed-optimization llvm:analysis

Alive2: https://alive2.llvm.org/ce/z/3yxP4T ``` define i1 @src1(i64 %x) { entry:… %trunc = trunc i64 %x to i32 %cond = icmp ne i32 %trunc, 1 call void @llvm.assume(i1 %cond) %cmp = icmp eq i64 %x, 1 ret i1 %cmp } define i1 @tgt1(i64 %x) { entry: ret i1 false } define i1 @src2(i64 %x) { entry: %trunc = trunc i64 %x to i1 %not = xor i1 %trunc, true call void @llvm.assume(i1 %not) %cmp = icmp eq i64 %x, 1 ret i1 %cmp } define i1 @tgt2(i64 %x) { entry: ret i1 false } ``` The second pattern is common in Rust applications. See also https://github.com/dtcxzyw/llvm-tools/issues/36.

github.com/llvm/llvm-project

[ValueTracking] `ptrdiff(X, Y) != 0` implies `X != Y`

opened 04:14PM - 29 Nov 24 UTC

dtcxzyw

missed-optimization llvm:analysis

Alive2: https://alive2.llvm.org/ce/z/NdrNbE ``` target datalayout = "p:8:8:8" d…efine i1 @src(ptr %p0, ptr %p1, i8 range(i8 1, 0) %nonzero) { entry: %i0 = ptrtoint ptr %p0 to i8 %i1 = ptrtoint ptr %p1 to i8 %diff = sub i8 %i0, %i1 %cond = icmp eq i8 %diff, %nonzero call void @llvm.assume(i1 %cond) %cmp = icmp eq ptr %p0, %p1 ret i1 %cmp } define i1 @tgt(ptr %p0, ptr %p1, i8 range(i8 1, 0) %nonzero) { ret i1 false } ``` See also https://github.com/dtcxzyw/llvm-tools/issues/35.

For the complete list, please refer to Issues · dtcxzyw/llvm-tools · GitHub.

Topic		Replies	Views
RFC: canonical icmp predicates? LLVM Dev List Archives	2	91	April 27, 2015
Questions for Constraint Elimination pass Beginners llvm	2	92	February 19, 2025
Recent improvements to the IR parser IR & Optimizations	11	1172	April 18, 2024
Fuzzing + alive2 for finding optimization bugs IR & Optimizations	4	298	June 2, 2022
missing optimization for icmps in induction variables? LLVM Dev List Archives	4	105	January 14, 2015

Related topics