Regression test from seed 0

mlir-stage-16-v1 · regression test PR · draft · ← all drafts

Add a regression test for mlir-stage-16-v1

This adds one LIT test covering 15 lines and 8 branch outcomes that the existing suite does not reach, across 2 source files, at 48615bc5925ef4b9db8b4550b5d4322933cf4b7b.

Coverage this test adds

Source file Newly covered lines Newly covered branch outcomes
lib/Frontend/Lowering/GraphRegionAdmission.cpp — 114:8–114:43 true
lib/Frontend/Lowering/GraphRegionLowering.cpp 598–601, 603, 620–621, 623–630 595:11–596:56 false; 598:16–598:20 true; 613:16–613:24 false; 621:11–621:15 false; 623:11–625:19 false; 623:11–625:19 true; 627:16–627:20 true

lib/Frontend/Lowering/GraphRegionLowering.cpp

 593        if (!def) 594          return value;+595        if (::llvm::isa<::mlir::memref::AllocOp, ::mlir::memref::AllocaOp,    [false branch at 595:11]+596                        ::mlir::memref::GetGlobalOp>(def)) 597          return value;+598        if (auto view = ::llvm::dyn_cast<::mlir::ViewLikeOpInterface>(def)) {    [true branch at 598:16]+599          value = view.getViewSource();+600          continue;+601        } 602        return std::nullopt;+603      } 604      return std::nullopt; 605    }@@ 611      ::llvm::DenseSet<::mlir::Value> visited; 612      while (value && visited.insert(value).second) {+613        if (auto argument = ::llvm::dyn_cast<::mlir::BlockArgument>(value)) {    [false branch at 613:16] 614          if (argument.getOwner() != &entry || argument.getArgNumber() == 0) 615            return true;@@ 618        } 619  +620        ::mlir::Operation *def = value.getDefiningOp();+621        if (!def)    [false branch at 621:11] 622          return true;+623        if (::llvm::isa<::mlir::memref::AllocOp, ::mlir::memref::AllocaOp,    [false branch at 623:11, true branch at 623:11]+624                        ::mlir::memref::GetGlobalOp, ::mlir::LLVM::AddressOfOp>(+625                def))+626          return true;+627        if (auto view = ::llvm::dyn_cast<::mlir::ViewLikeOpInterface>(def)) {    [true branch at 627:16]+628          value = view.getViewSource();+629          continue;+630        } 631        if (auto gep = ::llvm::dyn_cast<::mlir::LLVM::GEPOp>(def)) { 632          value = gep.getBase();

The test

The input was reduced from 29 to 27 lines while keeping every covered line and branch outcome above, and while the compiler still accepted it. The CHECK lines are the compiler's exact output on this input at 48615bc5925ef4b9db8b4550b5d4322933cf4b7b.

// RUN: loom-raise-opt --loom-lower-graph-memory %s | FileCheck %s

module {
  dataflow.graph private @view_export_0(
      %start: none, %lb: i64, %ub: i64, %step: i64, %i: index, %c: i1, %v: i32,
      %m: memref<4xi32>) -> (memref<?xi32>)
      attributes {input_segments = array<i32: 6, 0, 1>,
                  result_segments = array<i32: 0, 0, 1>} {
    %view = memref.cast %m : memref<4xi32> to memref<?xi32>
    scf.if %c {
      memref.store %v, %view[%i] : memref<?xi32>
    }
    dataflow.graph.return values() streams()
        memories(%view : memref<?xi32>) complete(%start : none)
  }
  dataflow.graph private @fresh_export_1(
      %start: none, %lb: i64, %ub: i64, %step: i64, %i: index, %c: i1, %v: i32)
      -> (memref<4xi32>)
      attributes {input_segments = array<i32: 6, 0, 0>,
                  result_segments = array<i32: 0, 0, 1>} {
    %slot = memref.alloc() : memref<4xi32>
    scf.for %iv = %lb to %ub step %step : i64 {
      %idx = arith.index_cast %iv : i64 to index
      memref.store %v, %slot[%idx] : memref<4xi32>
    }
    dataflow.graph.return values() streams()
        memories(%slot : memref<4xi32>) complete(%start : none)
  }
}

// CHECK: module {
// CHECK-NEXT:   dataflow.graph private @view_export_0(%arg0: none, %arg1: i64, %arg2: i64, %arg3: i64, %arg4: index, %arg5: i1, %arg6: i32, %arg7: memref<4xi32>) -> memref<?xi32> attributes {input_segments = array<i32: 6, 0, 1>, result_segments = array<i32: 0, 0, 1>} {
// CHECK-NEXT:     %cast = memref.cast %arg7 : memref<4xi32> to memref<?xi32>
// CHECK-NEXT:     %0:2 = dataflow.demux %arg5, %arg0 : (i1, none) -> (none, none)
// CHECK-NEXT:     %1:2 = dataflow.demux %arg5, %arg0 : (i1, none) -> (none, none)
// CHECK-NEXT:     %2:2 = dataflow.demux %arg5, %arg0 : (i1, none) -> (none, none)
// CHECK-NEXT:     %3:2 = dataflow.demux %arg5, %arg6 : (i1, i32) -> (i32, i32)
// CHECK-NEXT:     %4:2 = dataflow.demux %arg5, %arg4 : (i1, index) -> (index, index)
// CHECK-NEXT:     %5:2 = dataflow.sync %0#1, %2#1 : (none, none) -> (none, none)
// CHECK-NEXT:     %6 = dataflow.store %cast[%4#1] %3#1 %5#0 : memref<?xi32>
// CHECK-NEXT:     %7 = dataflow.mux %arg5, %2#0, %6 : (i1, none, none) -> none
// CHECK-NEXT:     %8 = dataflow.mux %arg5, %0#0, %0#1 : (i1, none, none) -> none
// CHECK-NEXT:     dataflow.graph.return values() streams() memories(%cast : memref<?xi32>) complete(%8, %7 : none, none)
// CHECK-NEXT:   }
// CHECK-NEXT:   dataflow.graph private @fresh_export_1(%arg0: none, %arg1: i64, %arg2: i64, %arg3: i64, %arg4: index, %arg5: i1, %arg6: i32) -> memref<4xi32> attributes {input_segments = array<i32: 6, 0, 0>, result_segments = array<i32: 0, 0, 1>} {
// CHECK-NEXT:     %alloc = memref.alloc() : memref<4xi32>
// CHECK-NEXT:     %iv, %phase = dataflow.stream %arg1, %arg2, %arg3 step add while slt : i64
// CHECK-NEXT:     %0 = dataflow.carry %phase, %arg0, %1#1 : none
// CHECK-NEXT:     %1:2 = dataflow.demux %phase, %0 : (i1, none) -> (none, none)
// CHECK-NEXT:     %2 = dataflow.invariant %phase, %arg6 : i32
// CHECK-NEXT:     %after_cond, %after_value = dataflow.gate %phase, %2 : i32
// CHECK-NEXT:     %3:2 = dataflow.demux %after_cond, %after_value : (i1, i32) -> (i32, i32)
// CHECK-NEXT:     %4 = dataflow.carry %phase, %arg0, %10 : none
// CHECK-NEXT:     %5 = dataflow.carry %phase, %arg0, %10 : none
// CHECK-NEXT:     %6:2 = dataflow.demux %phase, %4 : (i1, none) -> (none, none)
// CHECK-NEXT:     %7:2 = dataflow.demux %phase, %5 : (i1, none) -> (none, none)
// CHECK-NEXT:     %8 = arith.index_cast %iv : i64 to index
// CHECK-NEXT:     %9:2 = dataflow.sync %1#1, %7#1 : (none, none) -> (none, none)
// CHECK-NEXT:     %10 = dataflow.store %alloc[%8] %after_value %9#0 : memref<4xi32>
// CHECK-NEXT:     %11 = arith.cmpi slt, %arg1, %arg2 : i64
// CHECK-NEXT:     %12:2 = dataflow.demux %11, %1#0 : (i1, none) -> (none, none)
// CHECK-NEXT:     %13:2 = dataflow.sync %12#1, %3#0 : (none, i32) -> (none, i32)
// CHECK-NEXT:     %14 = dataflow.mux %11, %12#0, %13#0 : (i1, none, none) -> none
// CHECK-NEXT:     dataflow.graph.return values() streams() memories(%alloc : memref<4xi32>) complete(%14, %7#0 : none, none)
// CHECK-NEXT:   }
// CHECK-NEXT: }
// CHECK-EMPTY:

Validation

  • Native compiler and FileCheck replay: passed at 48615bc5925ef4b9db8b4550b5d4322933cf4b7b.
  • Property checker verdict on the reduced pair: PASS (postcondition.spct, SHA-256 0de7d2e8cdb0257be7bca4ae995ab0ebc1cad50088c0695c63302f67b288fecb).
  • Reduction criterion: accepted checker PASS and every original line/branch increment over the suite baseline; the original postcondition BDD decision path is unchanged; every original fast edge increment over its suite baseline.

Where this test came from

PBT mlir-stage-16-v1, run 20260911-084757, seed 0.

The property under test is anchored on documentation:

  • selected output: docs/spec-compiler-part-3-mem.md lines 463–466 (output side)
  • linked input 29: docs/spec-compiler-part-3-mem.md lines 482–486 (input side)
  • linked input 32: docs/spec-compiler-part-3-mem.md lines 92–97 (input side)
  • linked input 50: docs/spec-compiler-part-3-mem.md lines 148–152 (input side)
  • linked input 59: docs/spec-compiler-part-3-mem.md lines 136–140 (input side)
  • linked input 66: docs/spec-compiler-part-3-mem.md lines 489–493 (input side)
  • linked input 67: docs/spec-compiler-part-3-mem.md lines 3–6 (input side)
  • linked input 68: docs/spec-compiler-part-3-mem.md lines 79–90 (input side)
  • linked input 80: docs/spec-compiler-part-3-mem.md lines 99–106 (input side)
  • linked input 102: docs/spec-compiler-part-3-mem.md lines 389–393 (input side)
  • linked input 104: docs/spec-compiler-part-3-mem.md lines 470–480 (input side)
  • linked input 115: docs/spec-compiler-part-3-mem.md lines 486–489 (input side)
  • linked input 126: docs/spec-compiler-part-3-mem.md lines 142–146 (input side)
  • linked input 149: docs/spec-compiler-part-3-mem.md lines 43–46 (input side)
  • linked input 170: docs/spec-compiler-part-3-mem.md lines 154–157 (input side)
  • linked input 182: docs/spec-compiler-part-3-mem.md lines 382–387 (input side)
  • linked input 184: docs/spec-compiler-part-3-mem.md lines 34–35 (input side)
  • linked input 195: docs/spec-compiler-part-3-mem.md lines 159–161 (input side)
  • linked input 200: docs/spec-compiler-part-3-mem.md lines 40–41 (input side)
  • linked input 202: docs/spec-compiler-part-3-mem.md lines 31–32 (input side)
  • linked input 211: docs/spec-compiler-part-3-mem.md lines 245–251 (input side)

Coverage is measured against the recorded baseline suite at this revision, and counts unique mapped file locations including generated code. Reduction retains every added line or branch outcome and a passing property check; it is not a claim of global minimality, nor of a defect.

Originating PBT run · Seed 0

LIT test · PR patch · Native verification