[clang] [llvm] [ValueTracking] Add dominating condition support in computeKnownBits() (PR #73662)

via cfe-commits cfe-commits at lists.llvm.org
Tue Dec 12 18:58:02 PST 2023


eddyz87 wrote:

Some additional details on BPF verifier failure.
Consider the following example:

```llvm
@a = global i32 0, align 4
@g = global i32 0, align 4

define i64 @foo() {
entry:
  %a = load i32, ptr @a
  %a.cmp = icmp ugt i32 %a, 32
  br i1 %a.cmp, label %end, label %l1 ; establish %a in range [0, 32]

l1:
  %g = load i32, ptr @g
  %g.cmp.1 = icmp sgt i32 %g, -1
  %g.cmp.a = icmp slt i32 %g, %a
  %cond = and i1 %g.cmp.a, %g.cmp.1
  br i1 %cond, label %l2, label %end  ; establish %g in range [0, %a]

l2:
  %g.64 = sext i32 %g to i64
  ret i64 %g.64

end:
  ret i64 0
}
```

Also consider the following opt command:

```
opt -passes=instcombine,correlated-propagation -mtriple=bpf-pc-linux -S -o - t.ll
```

Before this MR generated code looked as follows:

```llvm
...
entry:
  %a = load i32, ptr @a, align 4
  %a.cmp = icmp ugt i32 %a, 32
  br i1 %a.cmp, label %end, label %l1

l1:
  %g = load i32, ptr @g, align 4
  %g.cmp.1 = icmp sgt i32 %g, -1
  %g.cmp.a = icmp slt i32 %g, %a
  %cond = and i1 %g.cmp.a, %g.cmp.1
  br i1 %cond, label %l2, label %end

l2:
  %g.64 = zext nneg i32 %g to i64 ; <--- note zext nneg
  ret i64 %g.64
...
```

After this MR generated code looks as follows:

```llvm
...
entry:
  %a = load i32, ptr @a, align 4
  %a.cmp = icmp ugt i32 %a, 32
  br i1 %a.cmp, label %end, label %l1

l1:
  %g = load i32, ptr @g, align 4
  %cond = icmp ult i32 %g, %a ; <--- conditions merged by instcombine
  br i1 %cond, label %l2, label %end

l2:
  %g.64 = sext i32 %g to i64  ; <--- note sext
  ret i64 %g.64
...
```

Updated `instcombine` replaces `%g.cmp.1` and `%g.cmp.a` with a single `ult`, however `correlated-propagation` pass can no longer infer that `%g` is non-negative and thus does not replace `g.64 = sext` by `%g.64 = zext nneg`.
Probably because of variable `%a`, used in `%cond = icmp` (replacing this variable by a constant `32` allows `correlated-propagation` to add `zext`). As far as I understand, previously non-negativity of `%g` was inferred from `%g.cmp.1 = icmp sgt i32 %g, -1` condition, which is now deleted.

I think that there are no issues with transformation applied by updated `instcombine`.
To resolve BPF regression we either need to extend `correlated-propagation` to better figure out range bounds (don't know how hard might that be), or teach verifier to understand that `sext` in this situation is equivalent to `zext`.


https://github.com/llvm/llvm-project/pull/73662


More information about the cfe-commits mailing list