AliveToolkit / alive2

Automatic verification of LLVM optimizations
MIT License
769 stars 97 forks source link

Infer poison-generating flags #962

Closed dtcxzyw closed 10 months ago

dtcxzyw commented 10 months ago

This patch infers poison-generating flags after the original transform is proven correct. It introduces a new option, -refine-tgt. When enabled, alive2 tries to add poison-generating flags and verify the transform.

Example:

; alive-tv test.srctgt.ll -refine-tgt 
----------------------------------------
define i8 @src(i8 %a, i8 %b) {
entry:
  %sub = sub nsw i8 0, %a
  %add = add nsw i8 %sub, %b
  ret i8 %add
}
=>
define i8 @tgt(i8 %a, i8 %b) {
entry:
  %sub = sub i8 %b, %a
  ret i8 %sub
}

Refined target (potential optimization):

define i8 @tgt.1(i8 %a, i8 %b) {
entry:
  %sub = sub nsw i8 %b, %a
  ret i8 %sub
}
Transformation seems to be correct!

Inspired by https://github.com/llvm/llvm-project/issues/72119, I did this work to exploit some missed optimizations.

nunoplopes commented 10 months ago

It's great that this patch has been used successfully to suggest more optimizations. But the implementation is a bit inefficient as it does 1 refinement check per flag per operation. The old Alive used to have an implementation of this using a more optimized encoding. Plus all the code in the verification function is a bit of a hack; it's not the right place. That said, I would rather not merge the patch as-is, as a proper implementation would need to almost rewrite most of it.