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

[dtcxzyw]

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 dtcxzyw/llvm-tools#36.

[dtcxzyw]

More tests:

define i1 @src1(i64 %x) {
entry:
  %trunc = trunc i64 %x to i1
  br i1 %trunc, label %if.then, label %if.else

if.then:
  %cmp1 = icmp ne i64 %x, 0
  ret i1 %cmp1

if.else:
  %cmp2 = icmp eq i64 %x, 1
  ret i1 %cmp2
}

define i1 @src2(i64 %x) {
entry:
  %trunc = trunc i64 %x to i1
  br i1 %trunc, label %if.then, label %if.else

if.then:
  %cmp1 = icmp eq i64 %x, 0
  ret i1 %cmp1

if.else:
  %cmp2 = icmp ne i64 %x, 1
  ret i1 %cmp2
}

Blocked by #112742

[andjo403]

I hade found the assume( trunc x to i1) when trying to solve some regressions that I hade for an other commit so pushed up that PR but if you have a better solution I can abandon it.

I hade not seen the icmp (trunc x ne 1) but looks like it is not KnownBits as all we know is that x is not 1. maybe can hadle trunc in

llvm-project/llvm/lib/Analysis/ValueTracking.cpp

Line 9259 in 4a07433

static std::optional<bool> isImpliedCondICmps(const ICmpInst *LHS,

[dtcxzyw]

I hade found the assume( trunc x to i1) when trying to solve some regressions that I hade for an other commit so pushed up that PR but if you have a better solution I can abandon it.

Actually this issue is not related to llvm.assume. I extracted dominating conditions from large IR corpus and reconstruct them with llvm.assume. See also https://discourse.llvm.org/t/tuning-up-constraint-elimination/83213.

I hade not seen the icmp (trunc x ne 1) but looks like it is not KnownBits as all we know is that x is not 1. maybe can hadle trunc in

We can infer the LSB is 1 or 0, no? I have a local patch which modifies findValuesAffectedByCondition and computeKnownBitsFromCond. But it is blocked by #112742.

[andjo403]

Hmm I thought that we can not say anything about the known bits for

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
}

as the LSB is for eg 1 for %x = 3 but 0 for %x = 2 and the %cond is true for both or maybe I'm missing something.

[dtcxzyw]

Hmm I thought that we can not say anything about the known bits for

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
}

as the LSB is for eg 1 for %x = 3 but 0 for %x = 2 and the %cond is true for both or maybe I'm missing something.

I know what you are saying. But it is not the motivation of this issue. This issue only focuses on eliminating a common pattern in Rust applications (i.e., @src2).

For @src1, I am planning to implement a QBVF solver to address this kind of issues. See also #85647.