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.
| 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 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:
48615bc5925ef4b9db8b4550b5d4322933cf4b7b.postcondition.spct, SHA-256 0de7d2e8cdb0257be7bca4ae995ab0ebc1cad50088c0695c63302f67b288fecb).PBT mlir-stage-16-v1, run 20260911-084757, seed 0.
The property under test is anchored on documentation:
docs/spec-compiler-part-3-mem.md lines 463–466 (output side)docs/spec-compiler-part-3-mem.md lines 482–486 (input side)docs/spec-compiler-part-3-mem.md lines 92–97 (input side)docs/spec-compiler-part-3-mem.md lines 148–152 (input side)docs/spec-compiler-part-3-mem.md lines 136–140 (input side)docs/spec-compiler-part-3-mem.md lines 489–493 (input side)docs/spec-compiler-part-3-mem.md lines 3–6 (input side)docs/spec-compiler-part-3-mem.md lines 79–90 (input side)docs/spec-compiler-part-3-mem.md lines 99–106 (input side)docs/spec-compiler-part-3-mem.md lines 389–393 (input side)docs/spec-compiler-part-3-mem.md lines 470–480 (input side)docs/spec-compiler-part-3-mem.md lines 486–489 (input side)docs/spec-compiler-part-3-mem.md lines 142–146 (input side)docs/spec-compiler-part-3-mem.md lines 43–46 (input side)docs/spec-compiler-part-3-mem.md lines 154–157 (input side)docs/spec-compiler-part-3-mem.md lines 382–387 (input side)docs/spec-compiler-part-3-mem.md lines 34–35 (input side)docs/spec-compiler-part-3-mem.md lines 159–161 (input side)docs/spec-compiler-part-3-mem.md lines 40–41 (input side)docs/spec-compiler-part-3-mem.md lines 31–32 (input side)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