This adds one LIT test covering 6 lines and 7 branch outcomes that the existing suite does not reach, across 3 source files, at 48615bc5925ef4b9db8b4550b5d4322933cf4b7b.
| Source file | Newly covered lines | Newly covered branch outcomes |
|---|---|---|
lib/Dataflow/IR/DataflowActorSemantics.cpp |
287 | 285:7–285:17 true; 285:7–286:48 true; 308:42–308:78 false |
lib/Dataflow/IR/DataflowGraphValidation.cpp |
714, 1128–1130, 1132 | 1123:14–1123:20 false; 1130:11–1130:26 false; 713:28–713:29 true |
lib/Dataflow/IR/OperationSchema.cpp |
— | 738:7–739:56 true |
lib/Dataflow/IR/DataflowActorSemantics.cpp 283 return {}; 284 auto invariant = demux.getInput().getDefiningOp<dataflow::InvariantOp>();+285 if (!invariant || invariant.getCond() != stream.getPhase() || [true branch at 285:7, true branch at 285:7]+286 invariant.getOutput() != demux.getInput())+287 return {}; 288 return invariant.getInit(); 289 }@@ 306 auto stream = demux.getSel().getDefiningOp<dataflow::StreamOp>(); 307 if (stream && demux.getSel() == stream.getPhase() &&+308 result.getResultNumber() == 1 && unwrapPhaseProjection(value, stream)) [false branch at 308:42] 309 return; 310 }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);@@ 1121 }; 1122 +1123 if (auto stream = childPhase.getDefiningOp<dataflow::StreamOp>()) { [false branch at 1123:14] 1124 if (childPhase != stream.getPhase() || !assumeExact(stream.getInit()) || 1125 !assumeExact(stream.getLimit()) || !assumeExact(stream.getStep())) 1126 return false; 1127 } else {+1128 llvm::SmallVector<dataflow::CarryOp, 4> carries;+1129 graphIndex->collectCarries(childPhase, carries);+1130 if (carries.empty()) [false branch at 1130:11] 1131 return false;+1132 } 1133 1134 llvm::SmallVector<mlir::Value, 4> inputs;The input was reduced from 65 to 60 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 --mlir-print-op-generic %s | FileCheck %s
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 2 : index
%kv = arith.constant 7 : index
%ocond = arith.cmpi slt, %c0, %limit : index
scf.if %ocond {
scf.parallel (%lane) = (%c0) to (%cw) step (%c1) {
%bcond = arith.cmpi slt, %lane, %cw : index
scf.if %bcond {
memref.store %kv, %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) {
%rval = arith.constant 3 : index
"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
%kv = arith.constant 7 : index
scf.for %oi = %c0 to %limit step %c1 {
scf.forall (%lane) in (1) {
%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>
}
}
"loom.spatial_yield"()
<{operandSegmentSizes = array<i32: 0, 0>}> : () -> ()
}) {graph_name = "g_t1_0", source_maps = []} :
(index, memref<8xindex>, memref<4x4xindex>) -> ()
dataflow.thread.yield
}
// CHECK: "builtin.module"() ({
// CHECK-NEXT: "dataflow.thread"() <{domain = #dataflow.thread_domain<dense>, function_type = (memref<8xindex>, memref<8xindex>, memref<4x4xindex>, index) -> (), sym_name = "t0", sym_visibility = "private"}> ({
// CHECK-NEXT: ^bb0(%arg13: memref<8xindex>, %arg14: memref<8xindex>, %arg15: memref<4x4xindex>, %arg16: index, %arg17: none):
// CHECK-NEXT: %77 = "dataflow.graph.launch"(%arg17, %arg16, %arg14, %arg15) <{callee = @g_t0_0, operandSegmentSizes = array<i32: 1, 1, 0, 2, 0>, resultSegmentSizes = array<i32: 0, 0, 1>, source_maps = []}> : (none, index, memref<8xindex>, memref<4x4xindex>) -> none
// CHECK-NEXT: "dataflow.thread.yield"(%77) : (none) -> ()
// CHECK-NEXT: }) : () -> ()
// CHECK-NEXT: "dataflow.thread"() <{domain = #dataflow.thread_domain<dense>, function_type = (memref<8xindex>, memref<8xindex>, memref<4x4xindex>, index) -> (), sym_name = "t1", sym_visibility = "private"}> ({
// CHECK-NEXT: ^bb0(%arg8: memref<8xindex>, %arg9: memref<8xindex>, %arg10: memref<4x4xindex>, %arg11: index, %arg12: none):
// CHECK-NEXT: %75 = "arith.constant"() <{value = 3 : index}> : () -> index
// CHECK-NEXT: %76 = "dataflow.graph.launch"(%arg12, %arg11, %arg9, %arg10) <{callee = @g_t1_0, operandSegmentSizes = array<i32: 1, 1, 0, 2, 0>, resultSegmentSizes = array<i32: 0, 0, 1>, source_maps = []}> : (none, index, memref<8xindex>, memref<4x4xindex>) -> none
// CHECK-NEXT: "dataflow.thread.yield"(%76) : (none) -> ()
// CHECK-NEXT: }) : () -> ()
// CHECK-NEXT: "dataflow.graph"() <{function_type = (index, memref<8xindex>, memref<4x4xindex>) -> (), input_segments = array<i32: 1, 0, 2>, result_segments = array<i32: 0, 0, 0>, sym_name = "g_t0_0", sym_visibility = "private"}> ({
// CHECK-NEXT: ^bb0(%arg4: none, %arg5: index, %arg6: memref<8xindex>, %arg7: memref<4x4xindex>):
// CHECK-NEXT: %43 = "dataflow.constant"(%arg4) <{const_value = 0 : index}> : (none) -> index
// CHECK-NEXT: %44 = "dataflow.constant"(%arg4) <{const_value = 2 : index}> : (none) -> index
// CHECK-NEXT: %45 = "dataflow.constant"(%arg4) <{const_value = 7 : index}> : (none) -> index
// CHECK-NEXT: %46 = "arith.cmpi"(%arg5, %43) <{predicate = 4 : i64}> : (index, index) -> i1
// CHECK-NEXT: %47:2 = "dataflow.demux"(%46, %arg4) : (i1, none) -> (none, none)
// CHECK-NEXT: %48:2 = "dataflow.demux"(%46, %arg4) : (i1, none) -> (none, none)
// CHECK-NEXT: %49:2 = "dataflow.demux"(%46, %44) : (i1, index) -> (index, index)
// CHECK-NEXT: %50:2 = "dataflow.demux"(%46, %45) : (i1, index) -> (index, index)
// CHECK-NEXT: %51 = "dataflow.constant"(%47#1) <{const_value = 0 : index}> : (none) -> index
// CHECK-NEXT: %52 = "arith.cmpi"(%51, %49#1) <{predicate = 2 : i64}> : (index, index) -> i1
// CHECK-NEXT: %53:2 = "dataflow.demux"(%52, %47#1) : (i1, none) -> (none, none)
// CHECK-NEXT: %54:2 = "dataflow.demux"(%52, %48#1) : (i1, none) -> (none, none)
// CHECK-NEXT: %55:2 = "dataflow.demux"(%52, %50#1) : (i1, index) -> (index, index)
// CHECK-NEXT: %56:2 = "dataflow.demux"(%52, %51) : (i1, index) -> (index, index)
// CHECK-NEXT: %57:2 = "dataflow.sync"(%53#1, %54#1) : (none, none) -> (none, none)
// CHECK-NEXT: %58 = "dataflow.store"(%arg6, %56#1, %55#1, %57#0) : (memref<8xindex>, index, index, none) -> none
// CHECK-NEXT: %59 = "dataflow.mux"(%52, %54#0, %58) : (i1, none, none) -> none
// CHECK-NEXT: %60 = "dataflow.mux"(%52, %53#0, %53#1) : (i1, none, none) -> none
// CHECK-NEXT: %61 = "dataflow.constant"(%47#1) <{const_value = 1 : index}> : (none) -> index
// CHECK-NEXT: %62 = "arith.cmpi"(%61, %49#1) <{predicate = 2 : i64}> : (index, index) -> i1
// CHECK-NEXT: %63:2 = "dataflow.demux"(%62, %47#1) : (i1, none) -> (none, none)
// CHECK-NEXT: %64:2 = "dataflow.demux"(%62, %48#1) : (i1, none) -> (none, none)
// CHECK-NEXT: %65:2 = "dataflow.demux"(%62, %50#1) : (i1, index) -> (index, index)
// CHECK-NEXT: %66:2 = "dataflow.demux"(%62, %61) : (i1, index) -> (index, index)
// CHECK-NEXT: %67:2 = "dataflow.sync"(%63#1, %64#1) : (none, none) -> (none, none)
// CHECK-NEXT: %68 = "dataflow.store"(%arg6, %66#1, %65#1, %67#0) : (memref<8xindex>, index, index, none) -> none
// CHECK-NEXT: %69 = "dataflow.mux"(%62, %64#0, %68) : (i1, none, none) -> none
// CHECK-NEXT: %70 = "dataflow.mux"(%62, %63#0, %63#1) : (i1, none, none) -> none
// CHECK-NEXT: %71:2 = "dataflow.sync"(%60, %70) : (none, none) -> (none, none)
// CHECK-NEXT: %72:2 = "dataflow.sync"(%59, %69) : (none, none) -> (none, none)
// CHECK-NEXT: %73 = "dataflow.mux"(%46, %48#0, %72#0) : (i1, none, none) -> none
// CHECK-NEXT: %74 = "dataflow.mux"(%46, %47#0, %71#0) : (i1, none, none) -> none
// CHECK-NEXT: "dataflow.graph.return"(%74, %73) <{operandSegmentSizes = array<i32: 0, 0, 0, 2>}> : (none, none) -> ()
// CHECK-NEXT: }) : () -> ()
// CHECK-NEXT: "dataflow.graph"() <{function_type = (index, memref<8xindex>, memref<4x4xindex>) -> (), input_segments = array<i32: 1, 0, 2>, result_segments = array<i32: 0, 0, 0>, sym_name = "g_t1_0", sym_visibility = "private"}> ({
// CHECK-NEXT: ^bb0(%arg0: none, %arg1: index, %arg2: memref<8xindex>, %arg3: memref<4x4xindex>):
// CHECK-NEXT: %0 = "dataflow.constant"(%arg0) <{const_value = 0 : index}> : (none) -> index
// CHECK-NEXT: %1 = "dataflow.constant"(%arg0) <{const_value = 1 : index}> : (none) -> index
// CHECK-NEXT: %2 = "arith.index_cast"(%0) : (index) -> i32
// CHECK-NEXT: %3 = "arith.index_cast"(%arg1) : (index) -> i32
// CHECK-NEXT: %4 = "arith.index_cast"(%1) : (index) -> i32
// CHECK-NEXT: %5:2 = "dataflow.stream"(%2, %3, %4) <{predicate = 2 : i64, step_kind = 0 : i32}> : (i32, i32, i32) -> (i32, i1)
// CHECK-NEXT: %6 = "dataflow.carry"(%5#1, %arg0, %36#0) : (i1, none, none) -> none
// CHECK-NEXT: %7:2 = "dataflow.demux"(%5#1, %6) : (i1, none) -> (none, none)
// CHECK-NEXT: %8 = "dataflow.invariant"(%5#1, %arg1) : (i1, index) -> index
// CHECK-NEXT: %9:2 = "dataflow.gate"(%5#1, %8) : (i1, index) -> (i1, index)
// CHECK-NEXT: %10:2 = "dataflow.demux"(%9#0, %9#1) : (i1, index) -> (index, index)
// CHECK-NEXT: %11 = "dataflow.invariant"(%5#1, %1) : (i1, index) -> index
// CHECK-NEXT: %12:2 = "dataflow.gate"(%5#1, %11) : (i1, index) -> (i1, index)
// CHECK-NEXT: %13:2 = "dataflow.demux"(%12#0, %12#1) : (i1, index) -> (index, index)
// CHECK-NEXT: %14 = "dataflow.invariant"(%5#1, %0) : (i1, index) -> index
// CHECK-NEXT: %15:2 = "dataflow.gate"(%5#1, %14) : (i1, index) -> (i1, index)
// CHECK-NEXT: %16:2 = "dataflow.demux"(%15#0, %15#1) : (i1, index) -> (index, index)
// CHECK-NEXT: %17 = "dataflow.carry"(%5#1, %arg0, %38) : (i1, none, none) -> none
// CHECK-NEXT: %18:2 = "dataflow.demux"(%5#1, %17) : (i1, none) -> (none, none)
// CHECK-NEXT: %19 = "dataflow.carry"(%22, %7#1, %24#1) : (i1, none, none) -> none
// CHECK-NEXT: %20 = "dataflow.carry"(%22, %15#1, %30) : (i1, index, index) -> index
// CHECK-NEXT: %21 = "dataflow.invariant"(%22, %9#1) : (i1, index) -> index
// CHECK-NEXT: %22 = "arith.cmpi"(%20, %21) <{predicate = 2 : i64}> : (index, index) -> i1
// CHECK-NEXT: %23:2 = "dataflow.demux"(%22, %19) : (i1, none) -> (none, none)
// CHECK-NEXT: %24:2 = "dataflow.gate"(%22, %19) : (i1, none) -> (i1, none)
// CHECK-NEXT: %25:2 = "dataflow.demux"(%24#0, %24#1) : (i1, none) -> (none, none)
// CHECK-NEXT: %26:2 = "dataflow.demux"(%22, %20) : (i1, index) -> (index, index)
// CHECK-NEXT: %27 = "dataflow.invariant"(%22, %12#1) : (i1, index) -> index
// CHECK-NEXT: %28:2 = "dataflow.gate"(%22, %27) : (i1, index) -> (i1, index)
// CHECK-NEXT: %29:2 = "dataflow.demux"(%28#0, %28#1) : (i1, index) -> (index, index)
// CHECK-NEXT: %30 = "arith.addi"(%26#1, %28#1) <{overflowFlags = #arith.overflow<none>}> : (index, index) -> index
// CHECK-NEXT: %31:2 = "dataflow.demux"(%24#0, %24#1) : (i1, none) -> (none, none)
// CHECK-NEXT: %32:3 = "dataflow.sync"(%31#0, %25#0, %29#0) : (none, none, index) -> (none, none, index)
// CHECK-NEXT: %33 = "dataflow.mux"(%24#0, %32#0, %31#1) : (i1, none, none) -> none
// CHECK-NEXT: %34 = "dataflow.carry"(%22, %7#1, %33) : (i1, none, none) -> none
// CHECK-NEXT: %35:2 = "dataflow.demux"(%22, %34) : (i1, none) -> (none, none)
// CHECK-NEXT: %36:2 = "dataflow.sync"(%23#0, %35#0) : (none, none) -> (none, none)
// CHECK-NEXT: %37:2 = "dataflow.sync"(%36#0, %18#1) : (none, none) -> (none, none)
// CHECK-NEXT: %38 = "dataflow.store"(%arg2, %15#1, %26#0, %37#0) : (memref<8xindex>, index, index, none) -> none
// CHECK-NEXT: %39 = "arith.cmpi"(%2, %3) <{predicate = 2 : i64}> : (i32, i32) -> i1
// CHECK-NEXT: %40:2 = "dataflow.demux"(%39, %7#0) : (i1, none) -> (none, none)
// CHECK-NEXT: %41:4 = "dataflow.sync"(%40#1, %10#0, %13#0, %16#0) : (none, index, index, index) -> (none, index, index, index)
// CHECK-NEXT: %42 = "dataflow.mux"(%39, %40#0, %41#0) : (i1, none, none) -> none
// CHECK-NEXT: "dataflow.graph.return"(%42, %18#0) <{operandSegmentSizes = array<i32: 0, 0, 0, 2>}> : (none, none) -> ()
// CHECK-NEXT: }) : () -> ()
// CHECK-NEXT: }) : () -> ()
// CHECK-EMPTY:
48615bc5925ef4b9db8b4550b5d4322933cf4b7b.postcondition.spct, SHA-256 f62754955d08be6154989ab4a784f9f5663d3a4084f2a79711c52099539027ff).PBT mlir-stage-09-v1, run 20260911-082633, seed 76.
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 76
LIT test · PR patch · Native verification