fold-scf-if transformation introduces new undefined behavior: access to uninitialized memory

[wyanzhao]

We found that the fold-scf-if transformation may introduce undefined behavior.

Below is an MLIR example demonstrating that the fold-scf-if transformation may introduce undefined behavior. In this example, we have a function @example that selectively stores a float value in memory references %A and %B based on the value of %cond. The function assumes that %A and %B are not initialized within the function.

func @example(%A: memref<10xf32>, %B: memref<10xf32>, %a: f32, %b: f32, %cond: i1) {
  scf.if %cond {
    affine.store %a, %A[0] : memref<10xf32>
  } else {
    affine.store %b, %B[0] : memref<10xf32>
  }
  return
}

After applying the fold-scf-if transformation, we get the following code:

module {
  func @foo(%arg0: memref<10xf32>, %arg1: memref<10xf32>, %arg2: f32, %arg3: f32, %arg4: i1) {
    %0 = affine.load %arg1[0] : memref<10xf32>
    %1 = affine.load %arg0[0] : memref<10xf32>
    %2 = arith.select %arg4, %arg2, %1 : f32
    %3 = arith.select %arg4, %0, %arg3 : f32
    affine.store %2, %arg0[0] : memref<10xf32>
    affine.store %3, %arg1[0] : memref<10xf32>
    return
  }
}

In the transformed code, the two affine.load operations are executed unconditionally, which may access uninitialized memory. In the original code, the affine.store operations were executed only when the corresponding conditions were met. Specifically, when %cond is true, affine.store %a, %A[0] is executed, and when %cond is false, affine.store %a, %B[0] is executed. In this way, the respective memory locations in %A or %B are initialized before the memory access.

However, in the transformed code, the two affine.load operations are executed regardless of the %arg4 value. This may lead to uninitialized memory access in certain cases, resulting in undefined behavior. Specifically, neither %arg0[0] nor %arg1[0] are initialized before the affine.load operations.

This access to uninitialized memory was not present in the original code, resulting in new undefined behavior in the transformed code. The same issue also appears in the match-store-no-else.mlir and match-store-diff-mem.mlir unit tests.