sdiv exact keyword not preserved

tobiasgrosser commented 5 days ago

It seems the exact keyword in the generated proof is not preserved: https://github.com/opencompl/lean-mlir/blob/6e76106791a32338882c53685cd860527adda64d/SSA/Projects/InstCombine/tests/LLVM/gexact.lean#L20

The original test case for this is:

define i32 @sdiv2(i32 %x) {
; CHECK-LABEL: @sdiv2(
; CHECK-NEXT:    [[Y:%.*]] = ashr exact i32 [[X:%.*]], 3
; CHECK-NEXT:    ret i32 [[Y]]
;
  %y = sdiv exact i32 %x, 8
  ret i32 %y
}

Our incomplete semantics currently lead to verification failures in the test data @luisacicolini generates. @lfrenot, can you look into this on Monday?

lfrenot commented 4 days ago

When doing the keyword implementations, I skipped over exact (and disjoint) because they are not part of MLIR's LLVM dialect https://mlir.llvm.org/docs/Dialects/LLVM/#llvmsdiv-llvmsdivop They could be added though

tobiasgrosser commented 4 days ago

Right, adding them could be useful. Meanwhile, maybe filter out test cases that contain the exact keyword.

tobiasgrosser commented 4 days ago

Now, maybe adding exact support to MLIR's llvm dialect is easier than skipping over these benchmarks?

opencompl / lean-mlir

sdiv exact keyword not preserved #730