This adds one LIT test covering 1 line and 2 branch outcomes that the existing suite does not reach, across 1 source file, at 48615bc5925ef4b9db8b4550b5d4322933cf4b7b.
| Source file | Newly covered lines | Newly covered branch outcomes |
|---|---|---|
lib/Dataflow/IR/DataflowGraphValidation.cpp |
714 | 1437:11–1437:38 false; 713:28–713:29 true |
lib/Dataflow/IR/DataflowGraphValidation.cpp 711 712 void inheritAssumptions(const GraphCardinalityAnalysis &parent) {+ 713 for (mlir::Value value : parent.exactOneAssumptions) [true branch at 713:28]+ 714 insertExactOneAssumption(value); 715 for (mlir::Value value : parent.alignedCarryAssumptions) 716 insertAlignedCarryAssumption(value);@@ 1435 graphIndex->collectCarries(phase, phaseCarries); 1436 for (dataflow::CarryOp carry : phaseCarries)+1437 if (isExactOne(carry.getInit())) [false branch at 1437:11] 1438 carries.push_back(carry); 1439 }The input was reduced from 65 to 62 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-scf-to-dfg %s | FileCheck %s
func.func @native_helper(%arg0: index) -> index {
return %arg0 : index
}
dataflow.thread private @t0 domain(#dataflow.thread_domain<dense>)(
%scratch: memref<8xindex>, %memory: memref<8xindex>, %grid: memref<4x4xindex>,
%n: index) ctrl (%ctrl: none) {
"loom.spatial_region"(%n, %memory, %grid)
<{operandSegmentSizes = array<i32: 1, 0, 2, 0>,
resultSegmentSizes = array<i32: 0, 0>}> ({
^bb0(%limit: index, %target: memref<8xindex>, %tile: memref<4x4xindex>):
%c0 = arith.constant 0 : index
%c1 = arith.constant 1 : index
%cw = arith.constant 1 : index
%ocond = arith.cmpi slt, %c0, %limit : index
scf.if %ocond {
scf.parallel (%lane) = (%c0) to (%cw) step (%c1) {
%wres = scf.while (%wi = %c0) : (index) -> index {
%wc = arith.cmpi slt, %wi, %limit : index
scf.condition(%wc) %wi : index
} do {
^bb0(%wb: index):
%wn = arith.addi %wb, %c1 : index
scf.yield %wn : index
}
memref.store %wres, %target[%lane] : memref<8xindex>
scf.reduce
}
}
"loom.spatial_yield"()
<{operandSegmentSizes = array<i32: 0, 0>}> : () -> ()
}) {graph_name = "g_t0_0", source_maps = []} :
(index, memref<8xindex>, memref<4x4xindex>) -> ()
dataflow.thread.yield
}
dataflow.thread private @t1 domain(#dataflow.thread_domain<dense>)(
%scratch: memref<8xindex>, %memory: memref<8xindex>, %grid: memref<4x4xindex>,
%n: index) ctrl (%ctrl: none) {
"loom.spatial_region"(%n, %memory, %grid)
<{operandSegmentSizes = array<i32: 1, 0, 2, 0>,
resultSegmentSizes = array<i32: 0, 0>}> ({
^bb0(%limit: index, %target: memref<8xindex>, %tile: memref<4x4xindex>):
%c0 = arith.constant 0 : index
%c1 = arith.constant 1 : index
%ocond = arith.cmpi slt, %c0, %limit : index
scf.if %ocond {
scf.forall (%lane) in (2) {
%bsum = scf.for %bi = %c0 to %limit step %c1 iter_args(%bacc = %lane) -> (index) {
%bnext = arith.addi %bacc, %c1 : index
scf.yield %bnext : index
}
memref.store %bsum, %target[%lane] : memref<8xindex>
}
}
"loom.spatial_yield"()
<{operandSegmentSizes = array<i32: 0, 0>}> : () -> ()
}) {graph_name = "g_t1_0", source_maps = []} :
(index, memref<8xindex>, memref<4x4xindex>) -> ()
dataflow.thread.yield
}
// CHECK: module {
// CHECK-NEXT: func.func @native_helper(%arg0: index) -> index {
// CHECK-NEXT: return %arg0 : index
// CHECK-NEXT: }
// CHECK-NEXT: dataflow.thread private @t0 domain(#dataflow.thread_domain<dense>)(%arg0: memref<8xindex>, %arg1: memref<8xindex>, %arg2: memref<4x4xindex>, %arg3: index) ctrl (%arg4: none) {
// CHECK-NEXT: %done = dataflow.graph.launch @g_t0_0 deps(%arg4) values(%arg3) stream_inputs() memories(%arg1, %arg2) stream_outputs() : (none, index, memref<8xindex>, memref<4x4xindex>) -> none
// CHECK-NEXT: dataflow.thread.yield %done : none
// CHECK-NEXT: }
// CHECK-NEXT: dataflow.thread private @t1 domain(#dataflow.thread_domain<dense>)(%arg0: memref<8xindex>, %arg1: memref<8xindex>, %arg2: memref<4x4xindex>, %arg3: index) ctrl (%arg4: none) {
// CHECK-NEXT: %done = dataflow.graph.launch @g_t1_0 deps(%arg4) values(%arg3) stream_inputs() memories(%arg1, %arg2) stream_outputs() : (none, index, memref<8xindex>, memref<4x4xindex>) -> none
// CHECK-NEXT: dataflow.thread.yield %done : none
// CHECK-NEXT: }
// CHECK-NEXT: dataflow.graph private @g_t0_0(%arg0: none, %arg1: index, %arg2: memref<8xindex>, %arg3: memref<4x4xindex>) -> () attributes {input_segments = array<i32: 1, 0, 2>, result_segments = array<i32: 0, 0, 0>} {
// CHECK-NEXT: %0 = dataflow.constant %arg0 {const_value = 0 : index} : index
// CHECK-NEXT: %1 = dataflow.constant %arg0 {const_value = 1 : index} : index
// CHECK-NEXT: %2 = arith.cmpi sgt, %arg1, %0 : index
// CHECK-NEXT: %3:2 = dataflow.demux %2, %arg0 : (i1, none) -> (none, none)
// CHECK-NEXT: %4:2 = dataflow.demux %2, %arg0 : (i1, none) -> (none, none)
// CHECK-NEXT: %5:2 = dataflow.demux %2, %arg1 : (i1, index) -> (index, index)
// CHECK-NEXT: %6:2 = dataflow.demux %2, %1 : (i1, index) -> (index, index)
// CHECK-NEXT: %7:2 = dataflow.demux %2, %0 : (i1, index) -> (index, index)
// CHECK-NEXT: %8 = dataflow.carry %11, %3#1, %after_value : none
// CHECK-NEXT: %9 = dataflow.carry %11, %7#1, %17 : index
// CHECK-NEXT: %10 = dataflow.invariant %11, %5#1 : index
// CHECK-NEXT: %11 = arith.cmpi slt, %9, %10 : index
// CHECK-NEXT: %12:2 = dataflow.demux %11, %8 : (i1, none) -> (none, none)
// CHECK-NEXT: %after_cond, %after_value = dataflow.gate %11, %8 : none
// CHECK-NEXT: %13:2 = dataflow.demux %after_cond, %after_value : (i1, none) -> (none, none)
// CHECK-NEXT: %14:2 = dataflow.demux %11, %9 : (i1, index) -> (index, index)
// CHECK-NEXT: %15 = dataflow.invariant %11, %6#1 : index
// CHECK-NEXT: %after_cond_0, %after_value_1 = dataflow.gate %11, %15 : index
// CHECK-NEXT: %16:2 = dataflow.demux %after_cond_0, %after_value_1 : (i1, index) -> (index, index)
// CHECK-NEXT: %17 = arith.addi %14#1, %after_value_1 : index
// CHECK-NEXT: %18:2 = dataflow.demux %after_cond, %after_value : (i1, none) -> (none, none)
// CHECK-NEXT: %19:3 = dataflow.sync %18#0, %13#0, %16#0 : (none, none, index) -> (none, none, index)
// CHECK-NEXT: %20 = dataflow.mux %after_cond, %19#0, %18#1 : (i1, none, none) -> none
// CHECK-NEXT: %21 = dataflow.carry %11, %3#1, %20 : none
// CHECK-NEXT: %22:2 = dataflow.demux %11, %21 : (i1, none) -> (none, none)
// CHECK-NEXT: %23:2 = dataflow.sync %12#0, %22#0 : (none, none) -> (none, none)
// CHECK-NEXT: %24:2 = dataflow.sync %23#0, %4#1 : (none, none) -> (none, none)
// CHECK-NEXT: %25 = dataflow.store %arg2[%7#1] %14#0 %24#0 : memref<8xindex>
// CHECK-NEXT: %26 = dataflow.mux %2, %4#0, %25 : (i1, none, none) -> none
// CHECK-NEXT: %27 = dataflow.mux %2, %3#0, %23#0 : (i1, none, none) -> none
// CHECK-NEXT: dataflow.graph.return values() streams() memories() complete(%27, %26 : none, none)
// CHECK-NEXT: }
// CHECK-NEXT: dataflow.graph private @g_t1_0(%arg0: none, %arg1: index, %arg2: memref<8xindex>, %arg3: memref<4x4xindex>) -> () attributes {input_segments = array<i32: 1, 0, 2>, result_segments = array<i32: 0, 0, 0>} {
// CHECK-NEXT: %0 = dataflow.constant %arg0 {const_value = 0 : index} : index
// CHECK-NEXT: %1 = dataflow.constant %arg0 {const_value = 1 : index} : index
// CHECK-NEXT: %2 = arith.cmpi sgt, %arg1, %0 : index
// CHECK-NEXT: %3:2 = dataflow.demux %2, %arg0 : (i1, none) -> (none, none)
// CHECK-NEXT: %4:2 = dataflow.demux %2, %arg0 : (i1, none) -> (none, none)
// CHECK-NEXT: %5:2 = dataflow.demux %2, %1 : (i1, index) -> (index, index)
// CHECK-NEXT: %6:2 = dataflow.demux %2, %0 : (i1, index) -> (index, index)
// CHECK-NEXT: %7:2 = dataflow.demux %2, %arg1 : (i1, index) -> (index, index)
// CHECK-NEXT: %8 = dataflow.constant %3#1 {const_value = 0 : index} : index
// CHECK-NEXT: %9 = arith.index_cast %6#1 : index to i32
// CHECK-NEXT: %10 = arith.index_cast %7#1 : index to i32
// CHECK-NEXT: %11 = arith.index_cast %5#1 : index to i32
// CHECK-NEXT: %iv, %phase = dataflow.stream %9, %10, %11 step add while slt : i32
// CHECK-NEXT: %12 = dataflow.carry %phase, %3#1, %13#1 : none
// CHECK-NEXT: %13:2 = dataflow.demux %phase, %12 : (i1, none) -> (none, none)
// CHECK-NEXT: %14 = dataflow.carry %phase, %8, %18 : index
// CHECK-NEXT: %15:2 = dataflow.demux %phase, %14 : (i1, index) -> (index, index)
// CHECK-NEXT: %16 = dataflow.invariant %phase, %5#1 : index
// CHECK-NEXT: %after_cond, %after_value = dataflow.gate %phase, %16 : index
// CHECK-NEXT: %17:2 = dataflow.demux %after_cond, %after_value : (i1, index) -> (index, index)
// CHECK-NEXT: %18 = arith.addi %15#1, %after_value : index
// CHECK-NEXT: %19 = arith.cmpi slt, %9, %10 : i32
// CHECK-NEXT: %20:2 = dataflow.demux %19, %13#0 : (i1, none) -> (none, none)
// CHECK-NEXT: %21:2 = dataflow.sync %20#1, %17#0 : (none, index) -> (none, index)
// CHECK-NEXT: %22 = dataflow.mux %19, %20#0, %21#0 : (i1, none, none) -> none
// CHECK-NEXT: %23:2 = dataflow.sync %22, %4#1 : (none, none) -> (none, none)
// CHECK-NEXT: %24 = dataflow.store %arg2[%8] %15#0 %23#0 : memref<8xindex>
// CHECK-NEXT: %25 = dataflow.constant %3#1 {const_value = 1 : index} : index
// CHECK-NEXT: %26 = arith.index_cast %6#1 : index to i32
// CHECK-NEXT: %27 = arith.index_cast %7#1 : index to i32
// CHECK-NEXT: %28 = arith.index_cast %5#1 : index to i32
// CHECK-NEXT: %iv_0, %phase_1 = dataflow.stream %26, %27, %28 step add while slt : i32
// CHECK-NEXT: %29 = dataflow.carry %phase_1, %3#1, %30#1 : none
// CHECK-NEXT: %30:2 = dataflow.demux %phase_1, %29 : (i1, none) -> (none, none)
// CHECK-NEXT: %31 = dataflow.carry %phase_1, %25, %35 : index
// CHECK-NEXT: %32:2 = dataflow.demux %phase_1, %31 : (i1, index) -> (index, index)
// CHECK-NEXT: %33 = dataflow.invariant %phase_1, %5#1 : index
// CHECK-NEXT: %after_cond_2, %after_value_3 = dataflow.gate %phase_1, %33 : index
// CHECK-NEXT: %34:2 = dataflow.demux %after_cond_2, %after_value_3 : (i1, index) -> (index, index)
// CHECK-NEXT: %35 = arith.addi %32#1, %after_value_3 : index
// CHECK-NEXT: %36 = arith.cmpi slt, %26, %27 : i32
// CHECK-NEXT: %37:2 = dataflow.demux %36, %30#0 : (i1, none) -> (none, none)
// CHECK-NEXT: %38:2 = dataflow.sync %37#1, %34#0 : (none, index) -> (none, index)
// CHECK-NEXT: %39 = dataflow.mux %36, %37#0, %38#0 : (i1, none, none) -> none
// CHECK-NEXT: %40:2 = dataflow.sync %39, %4#1 : (none, none) -> (none, none)
// CHECK-NEXT: %41 = dataflow.store %arg2[%25] %32#0 %40#0 : memref<8xindex>
// CHECK-NEXT: %42:2 = dataflow.sync %22, %39 : (none, none) -> (none, none)
// CHECK-NEXT: %43:2 = dataflow.sync %24, %41 : (none, none) -> (none, none)
// CHECK-NEXT: %44 = dataflow.mux %2, %4#0, %43#0 : (i1, none, none) -> none
// CHECK-NEXT: %45 = dataflow.mux %2, %3#0, %42#0 : (i1, none, none) -> none
// CHECK-NEXT: dataflow.graph.return values() streams() memories() complete(%45, %44 : none, none)
// CHECK-NEXT: }
// CHECK-NEXT: }
// CHECK-EMPTY:
48615bc5925ef4b9db8b4550b5d4322933cf4b7b.postcondition.spct, SHA-256 f62754955d08be6154989ab4a784f9f5663d3a4084f2a79711c52099539027ff).PBT mlir-stage-09-v1, run 20260911-082633, seed 335.
The property under test is anchored on documentation:
docs/spec-compiler-part-3-dfg.md lines 127–132 (output side)docs/spec-compiler-part-3-dfg.md lines 110–117 (input side)docs/spec-compiler-part-3-dfg.md lines 92–100 (input side)docs/spec-compiler-part-3-dfg.md lines 1454–1461 (input side)docs/spec-compiler-part-3-dfg.md lines 117–120 (input side)docs/spec-compiler-part-3-dfg.md lines 127–132 (input side)docs/spec-compiler-part-3-dfg.md lines 87–90 (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 335
LIT test · PR patch · Native verification