This adds one LIT test covering 51 lines and 38 branch outcomes that the existing suite does not reach, across 5 source files, at 48615bc5925ef4b9db8b4550b5d4322933cf4b7b.
| Source file | Newly covered lines | Newly covered branch outcomes |
|---|---|---|
lib/Dataflow/IR/DataflowGraphCausality.cpp |
— | 27:12–27:34 false |
lib/Dataflow/IR/DataflowGraphValidation.cpp |
1128–1130, 1132 | 1123:14–1123:20 false; 1130:11–1130:26 false |
lib/Dataflow/IR/OperationSchema.cpp |
— | 730:7–730:27 true; 738:7–739:56 true |
lib/Frontend/Lowering/GraphParallelLowering.cpp |
427, 479, 483, 582–589, 591, 594, 597–601, 603–605, 608–612, 615–621, 623–624, 626–630, 634, 638–639, 1320, 1322–1324 | 1314:17–1314:50 false; 1314:54–1314:76 false; 1315:17–1315:30 false; 1320:17–1320:50 false; 426:41–426:61 true; 478:14–478:17 true; 482:14–482:17 true; 583:23–583:31 false; 585:30–585:57 false; 585:30–585:57 true; 586:29–586:37 false; 589:44–589:45 false; 591:42–591:43 false; 600:18–600:24 false; 600:28–600:53 false; 600:9–600:14 false; 601:9–601:35 false; 611:18–611:24 false; 611:28–611:53 false; 611:9–611:14 false; 612:9–612:35 false; 616:14–616:40 true; 616:44–616:78 true; 617:14–619:16 false; 617:14–619:16 true; 621:31–621:50 false; 621:9–621:27 true; 623:9–623:27 true; 628:37–628:38 false; 628:37–628:38 true; 630:38–630:39 false; 634:36–634:37 false |
lib/Frontend/Lowering/LowerGraphConstantsPass.cpp |
— | 70:16–70:32 false |
lib/Dataflow/IR/DataflowGraphValidation.cpp 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;lib/Frontend/Lowering/GraphParallelLowering.cpp 424 425 std::optional<LinearExpression> build(::mlir::Value value) {+ 426 if (auto found = cache.find(value); found != cache.end()) [true branch at 426:41]+ 427 return found->second; 428 if (failed.contains(value) || !active.insert(value).second) 429 return std::nullopt;@@ 476 } 477 + 478 if (auto add = ::llvm::dyn_cast<::mlir::arith::AddIOp>(def)) [true branch at 478:14]+ 479 return finish(combine(add.getLhs(), add.getRhs(), /*subtract=*/false)); 480 if (auto sub = ::llvm::dyn_cast<::mlir::arith::SubIOp>(def)) 481 return finish(combine(sub.getLhs(), sub.getRhs(), /*subtract=*/true));+ 482 if (auto mul = ::llvm::dyn_cast<::mlir::arith::MulIOp>(def)) [true branch at 482:14]+ 483 return finish(multiply(mul.getLhs(), mul.getRhs())); 484 if (auto cast = ::llvm::dyn_cast<::mlir::arith::IndexCastOp>(def)) 485 return finish(projectIndexCast(cast.getIn(), cast.getType(), false));@@ 580 581 void add(LinearExpression &target, const LinearExpression &source,+ 582 bool subtract) {+ 583 target.constant = subtract ? target.constant - source.constant [false branch at 583:23]+ 584 : target.constant + source.constant;+ 585 for (unsigned index = 0; index < target.lanes.size(); ++index) [false branch at 585:30, true branch at 585:30]+ 586 target.lanes[index] = subtract [false branch at 586:29]+ 587 ? target.lanes[index] - source.lanes[index]+ 588 : target.lanes[index] + source.lanes[index];+ 589 for (const auto &[symbol, coefficient] : source.symbols) [false branch at 589:44] 590 addSymbol(target, symbol, subtract ? -coefficient : coefficient);+ 591 for (const auto &[lane, coefficient] : source.descendantLanes) [false branch at 591:42] 592 addCoefficient(target.descendantLanes, lane, 593 subtract ? -coefficient : coefficient);+ 594 } 595 596 std::optional<LinearExpression> combine(::mlir::Value lhs, ::mlir::Value rhs,+ 597 bool subtract) {+ 598 auto left = build(lhs);+ 599 auto right = build(rhs);+ 600 if (!left || !right || !left->transforms.empty() || [false branch at 600:18, false branch at 600:28, false branch at 600:9]+ 601 !right->transforms.empty()) [false branch at 601:9] 602 return std::nullopt;+ 603 add(*left, *right, subtract);+ 604 return left;+ 605 } 606 607 std::optional<LinearExpression> multiply(::mlir::Value lhs,+ 608 ::mlir::Value rhs) {+ 609 auto left = build(lhs);+ 610 auto right = build(rhs);+ 611 if (!left || !right || !left->transforms.empty() || [false branch at 611:18, false branch at 611:28, false branch at 611:9]+ 612 !right->transforms.empty()) [false branch at 612:9] 613 return std::nullopt; 614 + 615 auto isConstant = [](const LinearExpression &expression) {+ 616 return expression.symbols.empty() && expression.descendantLanes.empty() && [true branch at 616:14, true branch at 616:44]+ 617 ::llvm::all_of(expression.lanes, [](const ::llvm::APInt &value) { [false branch at 617:14, true branch at 617:14]+ 618 return value.isZero();+ 619 });+ 620 };+ 621 if (!isConstant(*left) && !isConstant(*right)) [false branch at 621:31, true branch at 621:9] 622 return std::nullopt;+ 623 if (!isConstant(*left)) [true branch at 623:9]+ 624 std::swap(left, right); 625 + 626 ::llvm::APInt scale = left->constant;+ 627 right->constant *= scale;+ 628 for (::llvm::APInt &coefficient : right->lanes) [false branch at 628:37, true branch at 628:37]+ 629 coefficient *= scale;+ 630 for (auto &[symbol, coefficient] : right->symbols) { [false branch at 630:38] 631 (void)symbol; 632 coefficient *= scale; 633 }+ 634 for (auto &[lane, coefficient] : right->descendantLanes) { [false branch at 634:36] 635 (void)lane; 636 coefficient *= scale; 637 }+ 638 return right;+ 639 } 640 641 bool dependsOnLane(::mlir::Value value) {@@ 1312 SeenAddress &previous = found->second; 1313 bool differentLane =+1314 previous.firstLane != currentLane || previous.multipleLanes; [false branch at 1314:17, false branch at 1314:54]+1315 if (differentLane && (previous.writes || access.access->writes) && [false branch at 1315:17] 1316 (!previous.allAtomic || !access.access->atomic)) { 1317 overlap = true; 1318 return false; 1319 }+1320 if (previous.firstLane != currentLane) [false branch at 1320:17] 1321 previous.multipleLanes = true;+1322 previous.writes |= access.access->writes;+1323 previous.allAtomic &= access.access->atomic;+1324 } 1325 return true; 1326 });The input is 90 lines; reduction found nothing further to remove that kept the coverage above and a compiler that 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
llvm.func @imported_callable(i64) -> i64
func.func private @native_callable(%arg_a: i32) -> i32 {
return %arg_a : i32
}
dataflow.thread private @thread_0 domain(#dataflow.thread_domain<dense>)(
%limit: index, %memory: memref<?xindex>) ctrl (%ctrl: none) {
"loom.spatial_region"(%limit, %memory)
<{operandSegmentSizes = array<i32: 1, 0, 1, 0>,
resultSegmentSizes = array<i32: 0, 0>}> ({
^bb0(%lim: index, %target: memref<?xindex>):
%zero = arith.constant 0 : index
%one = arith.constant 1 : index
%two = arith.constant 2 : index
%flag = arith.cmpi ult, %zero, %two : index
scf.parallel (%iv0) = (%zero) to (%two) step (%one) {
%mx0 = arith.muli %zero, %two : index
%ix0 = arith.addi %mx0, %iv0 : index
scf.parallel (%iv1) = (%zero) to (%two) step (%one) {
%mx1 = arith.muli %ix0, %two : index
%ix1 = arith.addi %mx1, %iv1 : index
%ld2 = memref.load %target[%ix1] : memref<?xindex>
%ad2 = arith.addi %ld2, %one : index
memref.store %ad2, %target[%ix1] : memref<?xindex>
scf.reduce
}
scf.reduce
}
"loom.spatial_yield"()
<{operandSegmentSizes = array<i32: 0, 0>}> : () -> ()
}) {graph_name = "g_thread_0", source_maps = []} :
(index, memref<?xindex>) -> ()
dataflow.thread.yield
}
dataflow.thread private @thread_1 domain(#dataflow.thread_domain<dense>)(
%limit: index, %memory: memref<?xindex>) ctrl (%ctrl: none) {
"loom.spatial_region"(%limit, %memory)
<{operandSegmentSizes = array<i32: 1, 0, 1, 0>,
resultSegmentSizes = array<i32: 0, 0>}> ({
^bb0(%lim: index, %target: memref<?xindex>):
%zero = arith.constant 0 : index
%one = arith.constant 1 : index
%two = arith.constant 2 : index
%flag = arith.cmpi ult, %zero, %two : index
%wr3 = scf.while (%wa3 = %zero) : (index) -> index {
%wc3 = arith.cmpi ult, %wa3, %two : index
scf.condition(%wc3) %wa3 : index
} do {
^bb0(%wb3: index):
%wr4 = scf.while (%wa4 = %zero) : (index) -> index {
%wc4 = arith.cmpi ult, %wa4, %two : index
scf.condition(%wc4) %wa4 : index
} do {
^bb0(%wb4: index):
memref.store %one, %target[%zero] : memref<?xindex>
%ld6 = memref.load %target[%zero] : memref<?xindex>
%ad6 = arith.addi %ld6, %one : index
memref.store %ad6, %target[%zero] : memref<?xindex>
%wn4 = arith.addi %wb4, %one : index
scf.yield %wn4 : index
}
memref.store %one, %target[%zero] : memref<?xindex>
%wn3 = arith.addi %wb3, %one : index
scf.yield %wn3 : index
}
%wr8 = scf.while (%wa8 = %zero) : (index) -> index {
%wc8 = arith.cmpi ult, %wa8, %two : index
scf.condition(%wc8) %wa8 : index
} do {
^bb0(%wb8: index):
%wr9 = scf.while (%wa9 = %zero) : (index) -> index {
%wc9 = arith.cmpi ult, %wa9, %two : index
scf.condition(%wc9) %wa9 : index
} do {
^bb0(%wb9: index):
memref.store %one, %target[%zero] : memref<?xindex>
%wn9 = arith.addi %wb9, %one : index
scf.yield %wn9 : index
}
%ld11 = memref.load %target[%zero] : memref<?xindex>
%ad11 = arith.addi %ld11, %one : index
memref.store %ad11, %target[%zero] : memref<?xindex>
%wn8 = arith.addi %wb8, %one : index
scf.yield %wn8 : index
}
"loom.spatial_yield"()
<{operandSegmentSizes = array<i32: 0, 0>}> : () -> ()
}) {graph_name = "g_thread_1", source_maps = []} :
(index, memref<?xindex>) -> ()
dataflow.thread.yield
}
// CHECK: "builtin.module"() ({
// CHECK-NEXT: "llvm.func"() <{CConv = #llvm.cconv<ccc>, function_type = !llvm.func<i64 (i64)>, linkage = #llvm.linkage<external>, sym_name = "imported_callable", unnamed_addr = 0 : i64, visibility_ = 0 : i64}> ({
// CHECK-NEXT: }) : () -> ()
// CHECK-NEXT: "func.func"() <{function_type = (i32) -> i32, sym_name = "native_callable", sym_visibility = "private"}> ({
// CHECK-NEXT: ^bb0(%arg12: i32):
// CHECK-NEXT: "func.return"(%arg12) : (i32) -> ()
// CHECK-NEXT: }) : () -> ()
// CHECK-NEXT: "dataflow.thread"() <{domain = #dataflow.thread_domain<dense>, function_type = (index, memref<?xindex>) -> (), sym_name = "thread_0", sym_visibility = "private"}> ({
// CHECK-NEXT: ^bb0(%arg9: index, %arg10: memref<?xindex>, %arg11: none):
// CHECK-NEXT: %152 = "dataflow.graph.launch"(%arg11, %arg9, %arg10) <{callee = @g_thread_0, operandSegmentSizes = array<i32: 1, 1, 0, 1, 0>, resultSegmentSizes = array<i32: 0, 0, 1>, source_maps = []}> : (none, index, memref<?xindex>) -> none
// CHECK-NEXT: "dataflow.thread.yield"(%152) : (none) -> ()
// CHECK-NEXT: }) : () -> ()
// CHECK-NEXT: "dataflow.thread"() <{domain = #dataflow.thread_domain<dense>, function_type = (index, memref<?xindex>) -> (), sym_name = "thread_1", sym_visibility = "private"}> ({
// CHECK-NEXT: ^bb0(%arg6: index, %arg7: memref<?xindex>, %arg8: none):
// CHECK-NEXT: %151 = "dataflow.graph.launch"(%arg8, %arg6, %arg7) <{callee = @g_thread_1, operandSegmentSizes = array<i32: 1, 1, 0, 1, 0>, resultSegmentSizes = array<i32: 0, 0, 1>, source_maps = []}> : (none, index, memref<?xindex>) -> none
// CHECK-NEXT: "dataflow.thread.yield"(%151) : (none) -> ()
// CHECK-NEXT: }) : () -> ()
// CHECK-NEXT: "dataflow.graph"() <{arg_attrs = [{}, {llvm.noalias}], function_type = (index, memref<?xindex>) -> (), input_segments = array<i32: 1, 0, 1>, result_segments = array<i32: 0, 0, 0>, sym_name = "g_thread_0", sym_visibility = "private"}> ({
// CHECK-NEXT: ^bb0(%arg3: none, %arg4: index, %arg5: memref<?xindex>):
// CHECK-NEXT: %127 = "dataflow.constant"(%arg3) <{const_value = 1 : index}> : (none) -> index
// CHECK-NEXT: %128 = "dataflow.constant"(%arg3) <{const_value = 2 : index}> : (none) -> index
// CHECK-NEXT: %129 = "dataflow.constant"(%arg3) <{const_value = 0 : index}> : (none) -> index
// CHECK-NEXT: %130 = "arith.muli"(%129, %128) <{overflowFlags = #arith.overflow<none>}> : (index, index) -> index
// CHECK-NEXT: %131 = "arith.addi"(%130, %129) <{overflowFlags = #arith.overflow<none>}> : (index, index) -> index
// CHECK-NEXT: %132 = "arith.addi"(%142#0, %127) <{overflowFlags = #arith.overflow<none>}> : (index, index) -> index
// CHECK-NEXT: %133 = "arith.muli"(%129, %128) <{overflowFlags = #arith.overflow<none>}> : (index, index) -> index
// CHECK-NEXT: %134 = "arith.addi"(%133, %127) <{overflowFlags = #arith.overflow<none>}> : (index, index) -> index
// CHECK-NEXT: %135 = "arith.addi"(%144#0, %127) <{overflowFlags = #arith.overflow<none>}> : (index, index) -> index
// CHECK-NEXT: %136 = "arith.muli"(%127, %128) <{overflowFlags = #arith.overflow<none>}> : (index, index) -> index
// CHECK-NEXT: %137 = "arith.addi"(%136, %129) <{overflowFlags = #arith.overflow<none>}> : (index, index) -> index
// CHECK-NEXT: %138 = "arith.addi"(%146#0, %127) <{overflowFlags = #arith.overflow<none>}> : (index, index) -> index
// CHECK-NEXT: %139 = "arith.muli"(%127, %128) <{overflowFlags = #arith.overflow<none>}> : (index, index) -> index
// CHECK-NEXT: %140 = "arith.addi"(%139, %127) <{overflowFlags = #arith.overflow<none>}> : (index, index) -> index
// CHECK-NEXT: %141 = "arith.addi"(%148#0, %127) <{overflowFlags = #arith.overflow<none>}> : (index, index) -> index
// CHECK-NEXT: %142:2 = "dataflow.load"(%arg5, %131, %arg3) : (memref<?xindex>, index, none) -> (index, none)
// CHECK-NEXT: %143 = "dataflow.store"(%arg5, %131, %132, %142#1) : (memref<?xindex>, index, index, none) -> none
// CHECK-NEXT: %144:2 = "dataflow.load"(%arg5, %134, %arg3) : (memref<?xindex>, index, none) -> (index, none)
// CHECK-NEXT: %145 = "dataflow.store"(%arg5, %134, %135, %144#1) : (memref<?xindex>, index, index, none) -> none
// CHECK-NEXT: %146:2 = "dataflow.load"(%arg5, %137, %arg3) : (memref<?xindex>, index, none) -> (index, none)
// CHECK-NEXT: %147 = "dataflow.store"(%arg5, %137, %138, %146#1) : (memref<?xindex>, index, index, none) -> none
// CHECK-NEXT: %148:2 = "dataflow.load"(%arg5, %140, %arg3) : (memref<?xindex>, index, none) -> (index, none)
// CHECK-NEXT: %149 = "dataflow.store"(%arg5, %140, %141, %148#1) : (memref<?xindex>, index, index, none) -> none
// CHECK-NEXT: %150:4 = "dataflow.sync"(%143, %145, %147, %149) : (none, none, none, none) -> (none, none, none, none)
// CHECK-NEXT: "dataflow.graph.return"(%150#0) <{operandSegmentSizes = array<i32: 0, 0, 0, 1>}> : (none) -> ()
// CHECK-NEXT: }) : () -> ()
// CHECK-NEXT: "dataflow.graph"() <{arg_attrs = [{}, {llvm.noalias}], function_type = (index, memref<?xindex>) -> (), input_segments = array<i32: 1, 0, 1>, result_segments = array<i32: 0, 0, 0>, sym_name = "g_thread_1", sym_visibility = "private"}> ({
// CHECK-NEXT: ^bb0(%arg0: none, %arg1: index, %arg2: memref<?xindex>):
// 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 = "dataflow.constant"(%arg0) <{const_value = 2 : index}> : (none) -> index
// CHECK-NEXT: %3 = "dataflow.carry"(%8, %arg0, %51#0) : (i1, none, none) -> none
// CHECK-NEXT: %4 = "dataflow.carry"(%8, %0, %54) : (i1, index, index) -> index
// CHECK-NEXT: %5 = "dataflow.invariant"(%8, %2) : (i1, index) -> index
// CHECK-NEXT: %6 = "dataflow.carry"(%8, %arg0, %53) : (i1, none, none) -> none
// CHECK-NEXT: %7 = "dataflow.carry"(%8, %arg0, %53) : (i1, none, none) -> none
// CHECK-NEXT: %8 = "arith.cmpi"(%4, %5) <{predicate = 6 : i64}> : (index, index) -> i1
// CHECK-NEXT: %9:2 = "dataflow.demux"(%8, %3) : (i1, none) -> (none, none)
// CHECK-NEXT: %10:2 = "dataflow.gate"(%8, %3) : (i1, none) -> (i1, none)
// CHECK-NEXT: %11:2 = "dataflow.demux"(%10#0, %10#1) : (i1, none) -> (none, none)
// CHECK-NEXT: %12:2 = "dataflow.demux"(%8, %6) : (i1, none) -> (none, none)
// CHECK-NEXT: %13:2 = "dataflow.demux"(%8, %7) : (i1, none) -> (none, none)
// CHECK-NEXT: %14:2 = "dataflow.demux"(%8, %4) : (i1, index) -> (index, index)
// CHECK-NEXT: %15 = "dataflow.invariant"(%8, %2) : (i1, index) -> index
// CHECK-NEXT: %16:2 = "dataflow.gate"(%8, %15) : (i1, index) -> (i1, index)
// CHECK-NEXT: %17:2 = "dataflow.demux"(%16#0, %16#1) : (i1, index) -> (index, index)
// CHECK-NEXT: %18 = "dataflow.invariant"(%8, %1) : (i1, index) -> index
// CHECK-NEXT: %19:2 = "dataflow.gate"(%8, %18) : (i1, index) -> (i1, index)
// CHECK-NEXT: %20:2 = "dataflow.demux"(%19#0, %19#1) : (i1, index) -> (index, index)
// CHECK-NEXT: %21 = "dataflow.invariant"(%8, %0) : (i1, index) -> index
// CHECK-NEXT: %22:2 = "dataflow.gate"(%8, %21) : (i1, index) -> (i1, index)
// CHECK-NEXT: %23:2 = "dataflow.demux"(%22#0, %22#1) : (i1, index) -> (index, index)
// CHECK-NEXT: %24 = "dataflow.carry"(%28, %10#1, %30#1) : (i1, none, none) -> none
// CHECK-NEXT: %25 = "dataflow.carry"(%28, %22#1, %45) : (i1, index, index) -> index
// CHECK-NEXT: %26 = "dataflow.invariant"(%28, %16#1) : (i1, index) -> index
// CHECK-NEXT: %27 = "dataflow.carry"(%28, %13#1, %44) : (i1, none, none) -> none
// CHECK-NEXT: %28 = "arith.cmpi"(%25, %26) <{predicate = 6 : i64}> : (index, index) -> i1
// CHECK-NEXT: %29:2 = "dataflow.demux"(%28, %24) : (i1, none) -> (none, none)
// CHECK-NEXT: %30:2 = "dataflow.gate"(%28, %24) : (i1, none) -> (i1, none)
// CHECK-NEXT: %31:2 = "dataflow.demux"(%30#0, %30#1) : (i1, none) -> (none, none)
// CHECK-NEXT: %32:2 = "dataflow.demux"(%28, %27) : (i1, none) -> (none, none)
// CHECK-NEXT: %33:2 = "dataflow.demux"(%28, %25) : (i1, index) -> (index, index)
// CHECK-NEXT: %34 = "dataflow.invariant"(%28, %19#1) : (i1, index) -> index
// CHECK-NEXT: %35:2 = "dataflow.gate"(%28, %34) : (i1, index) -> (i1, index)
// CHECK-NEXT: %36:2 = "dataflow.demux"(%35#0, %35#1) : (i1, index) -> (index, index)
// CHECK-NEXT: %37 = "dataflow.invariant"(%28, %22#1) : (i1, index) -> index
// CHECK-NEXT: %38:2 = "dataflow.gate"(%28, %37) : (i1, index) -> (i1, index)
// CHECK-NEXT: %39:2 = "dataflow.demux"(%38#0, %38#1) : (i1, index) -> (index, index)
// CHECK-NEXT: %40:2 = "dataflow.sync"(%30#1, %32#1) : (none, none) -> (none, none)
// CHECK-NEXT: %41 = "dataflow.store"(%arg2, %38#1, %35#1, %40#0) : (memref<?xindex>, index, index, none) -> none
// CHECK-NEXT: %42:2 = "dataflow.load"(%arg2, %38#1, %41) : (memref<?xindex>, index, none) -> (index, none)
// CHECK-NEXT: %43 = "arith.addi"(%42#0, %35#1) <{overflowFlags = #arith.overflow<none>}> : (index, index) -> index
// CHECK-NEXT: %44 = "dataflow.store"(%arg2, %38#1, %43, %42#1) : (memref<?xindex>, index, index, none) -> none
// CHECK-NEXT: %45 = "arith.addi"(%33#1, %35#1) <{overflowFlags = #arith.overflow<none>}> : (index, index) -> index
// CHECK-NEXT: %46:2 = "dataflow.demux"(%30#0, %30#1) : (i1, none) -> (none, none)
// CHECK-NEXT: %47:4 = "dataflow.sync"(%46#0, %31#0, %36#0, %39#0) : (none, none, index, index) -> (none, none, index, index)
// CHECK-NEXT: %48 = "dataflow.mux"(%30#0, %47#0, %46#1) : (i1, none, none) -> none
// CHECK-NEXT: %49 = "dataflow.carry"(%28, %10#1, %48) : (i1, none, none) -> none
// CHECK-NEXT: %50:2 = "dataflow.demux"(%28, %49) : (i1, none) -> (none, none)
// CHECK-NEXT: %51:2 = "dataflow.sync"(%29#0, %50#0) : (none, none) -> (none, none)
// CHECK-NEXT: %52:2 = "dataflow.sync"(%51#0, %32#0) : (none, none) -> (none, none)
// CHECK-NEXT: %53 = "dataflow.store"(%arg2, %22#1, %19#1, %52#0) : (memref<?xindex>, index, index, none) -> none
// CHECK-NEXT: %54 = "arith.addi"(%14#1, %19#1) <{overflowFlags = #arith.overflow<none>}> : (index, index) -> index
// CHECK-NEXT: %55:2 = "dataflow.demux"(%10#0, %51#0) : (i1, none) -> (none, none)
// CHECK-NEXT: %56:2 = "dataflow.sync"(%55#0, %11#0) : (none, none) -> (none, none)
// CHECK-NEXT: %57:2 = "dataflow.sync"(%56#0, %17#0) : (none, index) -> (none, index)
// CHECK-NEXT: %58:2 = "dataflow.sync"(%20#0, %23#0) : (index, index) -> (index, index)
// CHECK-NEXT: %59:2 = "dataflow.sync"(%57#0, %58#0) : (none, index) -> (none, index)
// CHECK-NEXT: %60 = "dataflow.mux"(%10#0, %59#0, %55#1) : (i1, none, none) -> none
// CHECK-NEXT: %61 = "dataflow.carry"(%8, %arg0, %60) : (i1, none, none) -> none
// CHECK-NEXT: %62:2 = "dataflow.demux"(%8, %61) : (i1, none) -> (none, none)
// CHECK-NEXT: %63:2 = "dataflow.sync"(%9#0, %62#0) : (none, none) -> (none, none)
// CHECK-NEXT: %64 = "dataflow.carry"(%69, %63#0, %111#0) : (i1, none, none) -> none
// CHECK-NEXT: %65 = "dataflow.carry"(%69, %0, %117) : (i1, index, index) -> index
// CHECK-NEXT: %66 = "dataflow.invariant"(%69, %2) : (i1, index) -> index
// CHECK-NEXT: %67 = "dataflow.carry"(%69, %12#0, %116) : (i1, none, none) -> none
// CHECK-NEXT: %68 = "dataflow.carry"(%69, %13#0, %116) : (i1, none, none) -> none
// CHECK-NEXT: %69 = "arith.cmpi"(%65, %66) <{predicate = 6 : i64}> : (index, index) -> i1
// CHECK-NEXT: %70:2 = "dataflow.demux"(%69, %64) : (i1, none) -> (none, none)
// CHECK-NEXT: %71:2 = "dataflow.gate"(%69, %64) : (i1, none) -> (i1, none)
// CHECK-NEXT: %72:2 = "dataflow.demux"(%71#0, %71#1) : (i1, none) -> (none, none)
// CHECK-NEXT: %73:2 = "dataflow.demux"(%69, %67) : (i1, none) -> (none, none)
// CHECK-NEXT: %74:2 = "dataflow.demux"(%69, %68) : (i1, none) -> (none, none)
// CHECK-NEXT: %75:2 = "dataflow.demux"(%69, %65) : (i1, index) -> (index, index)
// CHECK-NEXT: %76 = "dataflow.invariant"(%69, %2) : (i1, index) -> index
// CHECK-NEXT: %77:2 = "dataflow.gate"(%69, %76) : (i1, index) -> (i1, index)
// CHECK-NEXT: %78:2 = "dataflow.demux"(%77#0, %77#1) : (i1, index) -> (index, index)
// CHECK-NEXT: %79 = "dataflow.invariant"(%69, %1) : (i1, index) -> index
// CHECK-NEXT: %80:2 = "dataflow.gate"(%69, %79) : (i1, index) -> (i1, index)
// CHECK-NEXT: %81:2 = "dataflow.demux"(%80#0, %80#1) : (i1, index) -> (index, index)
// CHECK-NEXT: %82 = "dataflow.invariant"(%69, %0) : (i1, index) -> index
// CHECK-NEXT: %83:2 = "dataflow.gate"(%69, %82) : (i1, index) -> (i1, index)
// CHECK-NEXT: %84:2 = "dataflow.demux"(%83#0, %83#1) : (i1, index) -> (index, index)
// CHECK-NEXT: %85 = "dataflow.carry"(%90, %71#1, %92#1) : (i1, none, none) -> none
// CHECK-NEXT: %86 = "dataflow.carry"(%90, %83#1, %105) : (i1, index, index) -> index
// CHECK-NEXT: %87 = "dataflow.invariant"(%90, %77#1) : (i1, index) -> index
// CHECK-NEXT: %88 = "dataflow.carry"(%90, %73#1, %104) : (i1, none, none) -> none
// CHECK-NEXT: %89 = "dataflow.carry"(%90, %74#1, %104) : (i1, none, none) -> none
// CHECK-NEXT: %90 = "arith.cmpi"(%86, %87) <{predicate = 6 : i64}> : (index, index) -> i1
// CHECK-NEXT: %91:2 = "dataflow.demux"(%90, %85) : (i1, none) -> (none, none)
// CHECK-NEXT: %92:2 = "dataflow.gate"(%90, %85) : (i1, none) -> (i1, none)
// CHECK-NEXT: %93:2 = "dataflow.demux"(%92#0, %92#1) : (i1, none) -> (none, none)
// CHECK-NEXT: %94:2 = "dataflow.demux"(%90, %88) : (i1, none) -> (none, none)
// CHECK-NEXT: %95:2 = "dataflow.demux"(%90, %89) : (i1, none) -> (none, none)
// CHECK-NEXT: %96:2 = "dataflow.demux"(%90, %86) : (i1, index) -> (index, index)
// CHECK-NEXT: %97 = "dataflow.invariant"(%90, %80#1) : (i1, index) -> index
// CHECK-NEXT: %98:2 = "dataflow.gate"(%90, %97) : (i1, index) -> (i1, index)
// CHECK-NEXT: %99:2 = "dataflow.demux"(%98#0, %98#1) : (i1, index) -> (index, index)
// CHECK-NEXT: %100 = "dataflow.invariant"(%90, %83#1) : (i1, index) -> index
// CHECK-NEXT: %101:2 = "dataflow.gate"(%90, %100) : (i1, index) -> (i1, index)
// CHECK-NEXT: %102:2 = "dataflow.demux"(%101#0, %101#1) : (i1, index) -> (index, index)
// CHECK-NEXT: %103:2 = "dataflow.sync"(%92#1, %95#1) : (none, none) -> (none, none)
// CHECK-NEXT: %104 = "dataflow.store"(%arg2, %101#1, %98#1, %103#0) : (memref<?xindex>, index, index, none) -> none
// CHECK-NEXT: %105 = "arith.addi"(%96#1, %98#1) <{overflowFlags = #arith.overflow<none>}> : (index, index) -> index
// CHECK-NEXT: %106:2 = "dataflow.demux"(%92#0, %92#1) : (i1, none) -> (none, none)
// CHECK-NEXT: %107:4 = "dataflow.sync"(%106#0, %93#0, %99#0, %102#0) : (none, none, index, index) -> (none, none, index, index)
// CHECK-NEXT: %108 = "dataflow.mux"(%92#0, %107#0, %106#1) : (i1, none, none) -> none
// CHECK-NEXT: %109 = "dataflow.carry"(%90, %71#1, %108) : (i1, none, none) -> none
// CHECK-NEXT: %110:2 = "dataflow.demux"(%90, %109) : (i1, none) -> (none, none)
// CHECK-NEXT: %111:2 = "dataflow.sync"(%91#0, %110#0) : (none, none) -> (none, none)
// CHECK-NEXT: %112:2 = "dataflow.sync"(%111#0, %94#0) : (none, none) -> (none, none)
// CHECK-NEXT: %113:2 = "dataflow.load"(%arg2, %83#1, %112#0) : (memref<?xindex>, index, none) -> (index, none)
// CHECK-NEXT: %114:2 = "dataflow.sync"(%95#0, %113#1) : (none, none) -> (none, none)
// CHECK-NEXT: %115 = "arith.addi"(%113#0, %80#1) <{overflowFlags = #arith.overflow<none>}> : (index, index) -> index
// CHECK-NEXT: %116 = "dataflow.store"(%arg2, %83#1, %115, %114#0) : (memref<?xindex>, index, index, none) -> none
// CHECK-NEXT: %117 = "arith.addi"(%75#1, %80#1) <{overflowFlags = #arith.overflow<none>}> : (index, index) -> index
// CHECK-NEXT: %118:2 = "dataflow.demux"(%71#0, %111#0) : (i1, none) -> (none, none)
// CHECK-NEXT: %119:2 = "dataflow.sync"(%118#0, %72#0) : (none, none) -> (none, none)
// CHECK-NEXT: %120:2 = "dataflow.sync"(%119#0, %78#0) : (none, index) -> (none, index)
// CHECK-NEXT: %121:2 = "dataflow.sync"(%81#0, %84#0) : (index, index) -> (index, index)
// CHECK-NEXT: %122:2 = "dataflow.sync"(%120#0, %121#0) : (none, index) -> (none, index)
// CHECK-NEXT: %123 = "dataflow.mux"(%71#0, %122#0, %118#1) : (i1, none, none) -> none
// CHECK-NEXT: %124 = "dataflow.carry"(%69, %63#0, %123) : (i1, none, none) -> none
// CHECK-NEXT: %125:2 = "dataflow.demux"(%69, %124) : (i1, none) -> (none, none)
// CHECK-NEXT: %126:2 = "dataflow.sync"(%70#0, %125#0) : (none, none) -> (none, none)
// CHECK-NEXT: "dataflow.graph.return"(%126#0, %74#0) <{operandSegmentSizes = array<i32: 0, 0, 0, 2>}> : (none, none) -> ()
// CHECK-NEXT: }) : () -> ()
// CHECK-NEXT: }) : () -> ()
// CHECK-EMPTY:
48615bc5925ef4b9db8b4550b5d4322933cf4b7b.postcondition.spct, SHA-256 1b36ea6d4e36596888d4e5081bae7a2edc8494a8b4713cc2852e0b4c08951bdd).PBT mlir-stage-06-v1, run 20260911-081718, seed 421.
The property under test is anchored on documentation:
docs/spec-compiler-part-3-dfg.md lines 102–109 (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 421
LIT test · PR patch · Native verification