[MLIR] Double free with double --buffer-deallocation

[Anonymous15592]

I tried to lower and execute the following mlir program:

func.func @func1() {
  %false = arith.constant false
  %52 = tensor.empty() : tensor<1x1x1xi32>
  %69 = scf.while (%arg0 = %52) : (tensor<1x1x1xi32>) -> tensor<1x1x1xi32> {
    %173 = tensor.empty() : tensor<1x1x1xi32>
    scf.condition(%false) %173 : tensor<1x1x1xi32>  // change %173 to %52, the bug disappears
  } do {
    ^bb0(%arg0: tensor<1x1x1xi32>): 
    %175 = tensor.empty() : tensor<1x1x1xi32>
    scf.yield %175 : tensor<1x1x1xi32>  // change %173 to (%52 or %arg0), the bug disappears
  }
  vector.print %false : i1
  return
}

with the passes:

--scf-bufferize \
--empty-tensor-to-alloc-tensor \
--bufferization-bufferize \
--buffer-deallocation \
--buffer-deallocation \
--convert-scf-to-cf \
--convert-func-to-llvm \
--convert-vector-to-llvm \
--convert-bufferization-to-memref \
--finalize-memref-to-llvm \
--convert-arith-to-llvm \
--reconcile-unrealized-casts \

And I ran the executable and finally got the following error:

free(): double free detected in tcache 2
Aborted (core dumped)

I observed that --buffer-deallocation generated double free for %2:

// mlir file after double --buffer-deallocation
module {
  func.func @func1() {
    %false = arith.constant false
    %alloc = memref.alloc() {alignment = 64 : i64} : memref<1x1x1xi32>
    %0 = bufferization.clone %alloc : memref<1x1x1xi32> to memref<1x1x1xi32>
    %1 = bufferization.clone %0 : memref<1x1x1xi32> to memref<1x1x1xi32>
    memref.dealloc %0 : memref<1x1x1xi32>
    memref.dealloc %alloc : memref<1x1x1xi32>
    %2 = scf.while (%arg0 = %1) : (memref<1x1x1xi32>) -> memref<1x1x1xi32> {
      %alloc_0 = memref.alloc() {alignment = 64 : i64} : memref<1x1x1xi32>
      memref.dealloc %arg0 : memref<1x1x1xi32>
      memref.dealloc %arg0 : memref<1x1x1xi32>
      %3 = bufferization.clone %alloc_0 : memref<1x1x1xi32> to memref<1x1x1xi32>
      %4 = bufferization.clone %3 : memref<1x1x1xi32> to memref<1x1x1xi32>
      memref.dealloc %3 : memref<1x1x1xi32>
      memref.dealloc %alloc_0 : memref<1x1x1xi32>
      scf.condition(%false) %4 : memref<1x1x1xi32>
    } do {
    ^bb0(%arg0: memref<1x1x1xi32>):
      %alloc_0 = memref.alloc() {alignment = 64 : i64} : memref<1x1x1xi32>
      memref.dealloc %arg0 : memref<1x1x1xi32>
      memref.dealloc %arg0 : memref<1x1x1xi32>
      %3 = bufferization.clone %alloc_0 : memref<1x1x1xi32> to memref<1x1x1xi32>
      %4 = bufferization.clone %3 : memref<1x1x1xi32> to memref<1x1x1xi32>
      memref.dealloc %3 : memref<1x1x1xi32>
      memref.dealloc %alloc_0 : memref<1x1x1xi32>
      scf.yield %4 : memref<1x1x1xi32>
    }
    memref.dealloc %2 : memref<1x1x1xi32>    // here
    memref.dealloc %2 : memref<1x1x1xi32>
    vector.print %false : i1
    return
  }
}

Then I noticed that using the --buffer-deallocation-simplification option might resolve the double free issue. However, upon trying it, I still got the same error. I'm unsure if there's a problem with how I'm using the passes or with the transformations in --buffer-deallocation and --buffer-deallocation-simplification.