This adds one LIT test covering 147 lines and 71 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/DataflowActorSemantics.cpp |
1420–1421, 1423, 1429–1430, 1432–1433, 1451–1452, 1457, 1461–1465, 1469, 1473, 1479–1480, 1488–1489 | 1399:19–1399:26 false; 1419:14–1419:51 true; 1421:9–1421:16 false; 1423:9–1423:48 false; 1429:9–1429:17 false; 1429:9–1429:17 true; 1430:23–1430:28 false; 1442:12–1442:19 false; 1452:7–1452:21 false; 1457:7–1457:33 false; 1465:7–1465:20 false; 1469:7–1469:25 false; 1473:7–1473:63 false; 1480:7–1480:21 false |
lib/Dataflow/IR/DataflowOps.cpp |
199–200, 202–203, 205–209, 216, 220–222, 224–226, 230–231, 233–236, 242–243, 245–248, 285–288, 290, 302 | 196:7–196:42 false; 200:7–200:42 false; 203:9–203:52 false; 206:12–206:18 true; 207:12–207:74 true; 209:7–209:42 false; 216:7–216:40 false; 226:7–226:14 false; 243:7–243:50 false; 246:10–246:16 true; 247:10–247:72 false; 272:18–272:43 false; 272:7–272:14 true; 284:7–284:14 true; 286:9–286:23 false; 286:9–288:47 false; 287:9–288:47 false; 301:7–301:11 true; 310:24–310:53 false; 310:8–310:20 true; 323:7–323:11 true |
lib/Dataflow/IR/DataflowVectorSemantics.cpp |
— | 44:26–44:54 true |
lib/Frontend/Lowering/GraphRegionLowering.cpp |
171–173, 177–179, 710, 712, 1147–1149, 1151–1153, 1391–1406, 1409–1424 | 1146:16–1146:20 true; 1150:16–1150:21 true; 169:21–169:25 true; 171:11–173:36 false; 175:21–175:26 true; 177:11–179:37 false; 709:14–709:18 true; 711:14–711:19 true |
lib/Frontend/Lowering/RankedMemRefLowering.cpp |
19–23, 25–35, 43–51, 55, 59–60, 117–119, 122–125, 129–132, 136–138, 141–144 | 119:7–119:14 false; 123:25–123:51 true; 123:7–123:21 false; 123:7–123:21 true; 124:7–124:27 false; 124:7–124:27 true; 124:7–125:65 false; 125:7–125:65 false; 138:18–138:35 false; 138:7–138:14 false; 138:7–138:35 false; 20:10–20:19 true; 20:23–22:12 true; 27:10–27:14 true; 27:18–27:47 true; 28:10–34:16 false; 31:23–31:29 false; 46:30–46:51 false; 46:55–46:76 false; 46:7–46:26 false; 46:7–51:80 false; 47:7–47:57 false; 48:7–48:66 false; 49:30–49:50 false; 49:7–49:26 false; 50:7–51:80 false; 55:7–55:47 false |
lib/Dataflow/IR/DataflowActorSemantics.cpp 1397 std::errc::invalid_argument, 1398 "mask is only valid for a vector memory access");+1399 } else if (auto pointer = [false branch at 1399:19] 1400 llvm::dyn_cast<mlir::LLVM::LLVMPointerType>(dataType)) { 1401 if (maskType)@@ 1417 "P(AS) bits"); 1418 access.dataPointerLayout = *layout;+1419 } else if (llvm::isa<mlir::VectorType>(dataType)) { [true branch at 1419:14]+1420 auto vector = analyzeFixedRankDataVector(dataType, VectorRank::AnyFixed);+1421 if (!vector) [false branch at 1421:9] 1422 return vector.takeError();+1423 if (vector->getElementType() != elementType) [false branch at 1423:9] 1424 return llvm::createStringError( 1425 std::errc::invalid_argument,@@ 1427 typeToString(vector->getElementType()).c_str(), 1428 typeToString(elementType).c_str());+1429 if (maskType) [false branch at 1429:9, true branch at 1429:9]+1430 if (llvm::Error error = validateVectorMaskType(*vector, maskType)) [false branch at 1430:23] 1431 return std::move(error);+1432 access.vectorType = *vector;+1433 } else { 1434 return llvm::createStringError( 1435 std::errc::invalid_argument,@@ 1440 return access; 1441 +1442 if (auto pointer = llvm::dyn_cast<mlir::LLVM::LLVMPointerType>(addressType)) { [false branch at 1442:12] 1443 auto layout = loom::resolvePointerLayout(scope, pointer.getAddressSpace()); 1444 if (!layout)@@ 1449 } 1450 +1451 auto addressVector = llvm::dyn_cast<mlir::VectorType>(addressType);+1452 if (!addressVector) [false branch at 1452:7] 1453 return llvm::createStringError( 1454 std::errc::invalid_argument, 1455 "operand #1 must be index, LLVM pointer, or a fixed-size vector of " 1456 "one of those types");+1457 if (addressVector.isScalable()) [false branch at 1457:7] 1458 return llvm::createStringError(std::errc::invalid_argument, 1459 "address vector must be a fixed-size " 1460 "vector");+1461 const bool indexAddress =+1462 llvm::isa<mlir::IndexType>(addressVector.getElementType());+1463 auto pointerAddress = llvm::dyn_cast<mlir::LLVM::LLVMPointerType>(+1464 addressVector.getElementType());+1465 if (!indexAddress && !pointerAddress) [false branch at 1465:7] 1466 return llvm::createStringError(std::errc::invalid_argument, 1467 "address vector element type must be " 1468 "'index' or an LLVM pointer");+1469 if (!access.isVector()) [false branch at 1469:7] 1470 return llvm::createStringError( 1471 std::errc::invalid_argument, 1472 "vector address requires a fixed-size vector data type");+1473 if (addressVector.getShape() != access.vectorType.getShape()) [false branch at 1473:7] 1474 return llvm::createStringError( 1475 std::errc::invalid_argument,@@ 1477 typeToString(addressVector).c_str(), 1478 typeToString(access.vectorType).c_str());+1479 access.addressVectorType = addressVector;+1480 if (pointerAddress) { [false branch at 1480:7] 1481 auto layout = 1482 loom::resolvePointerLayout(scope, pointerAddress.getAddressSpace());@@ 1486 access.pointerLayout = *layout; 1487 }+1488 return access;+1489 } 1490 1491 llvm::Expected<dataflow::semantics::StreamTransition>lib/Dataflow/IR/DataflowOps.cpp 194 types.addressType = parser.getBuilder().getIndexType(); 195 types.dataType = types.memoryType.getElementType();+196 if (failed(parser.parseOptionalComma())) [false branch at 196:7] 197 return success(); 198 +199 Type firstExplicitType;+200 if (parser.parseType(firstExplicitType)) [false branch at 200:7] 201 return failure();+202 auto isAddressType = [](Type type) {+203 if (isa<IndexType, LLVM::LLVMPointerType>(type)) [false branch at 203:9] 204 return true;+205 auto vector = dyn_cast<VectorType>(type);+206 return vector && [true branch at 206:12]+207 isa<IndexType, LLVM::LLVMPointerType>(vector.getElementType()); [true branch at 207:12]+208 };+209 if (failed(parser.parseOptionalComma())) { [false branch at 209:7] 210 if (isAddressType(firstExplicitType)) 211 types.addressType = firstExplicitType;@@ 214 return success(); 215 }+216 if (!isAddressType(firstExplicitType)) [false branch at 216:7] 217 return parser.emitError(parser.getCurrentLocation(), 218 "first explicit type must be an address type"); 219 +220 types.addressType = firstExplicitType;+221 return parser.parseType(types.dataType);+222 } 223 +224 FailureOr<VectorType> getParsedDataVector(OpAsmParser &parser, Type dataType) {+225 auto vector = dyn_cast<VectorType>(dataType);+226 if (!vector) [false branch at 226:7] 227 return parser.emitError( 228 parser.getCurrentLocation(), 229 "masked memory access requires an explicit vector data type");+230 return vector;+231 } 232 +233 Type getMaskType(OpAsmParser &parser, VectorType dataVector) {+234 return VectorType::get(dataVector.getShape(), parser.getBuilder().getI1Type(),+235 dataVector.getScalableDims());+236 } 237 238 bool hasExplicitMemoryDataType(Value memory, Type dataType) {@@ 240 } 241 +242 bool isMemoryAddressType(Type type) {+243 if (isa<IndexType, LLVM::LLVMPointerType>(type)) [false branch at 243:7] 244 return true;+245 auto vector = dyn_cast<VectorType>(type);+246 return vector && [true branch at 246:10]+247 isa<IndexType, LLVM::LLVMPointerType>(vector.getElementType()); [false branch at 247:10]+248 } 249 250 /// Parses the grammar shared by every addressed memory actor:@@ 270 271 bool hasMask = succeeded(parser.parseOptionalKeyword("mask"));+272 if (hasMask && parser.parseOperand(mask)) [false branch at 272:18, true branch at 272:7] 273 return failure(); 274 if (parser.parseOptionalAttrDict(result.attributes) ||@@ 282 result.operands)) 283 return failure();+284 if (hasMask) { [true branch at 284:7]+285 FailureOr<VectorType> vector = getParsedDataVector(parser, types.dataType);+286 if (failed(vector) || [false branch at 286:9, false branch at 286:9]+287 parser.resolveOperand(mask, getMaskType(parser, *vector), [false branch at 287:9]+288 result.operands)) 289 return failure();+290 } 291 return success(); 292 }@@ 299 printer << ' ' << value; 300 printer << ' ' << control;+301 if (mask) [true branch at 301:7]+302 printer << " mask " << mask; 303 printer.printOptionalAttrDict(op->getAttrs()); 304 printer << " : " << memory.getType();@@ 308 // unambiguous and round-trippable. 309 if (!isa<IndexType>(address.getType()) ||+310 (explicitData && isMemoryAddressType(dataType))) [false branch at 310:24, true branch at 310:8] 311 printer << ", " << address.getType(); 312 if (explicitData)@@ 321 auto access = semantics::analyzeMemoryAccessType( 322 cast<MemRefType>(memory.getType()), dataType, address.getType(), op,+323 mask ? mask.getType() : Type{}); [true branch at 323:7] 324 if (!access) 325 return op->emitOpError(llvm::toString(access.takeError()));lib/Frontend/Lowering/GraphRegionLowering.cpp 167 store, store.getMemRefType(), store.getIndices(), indexBits))) 168 return ::mlir::WalkResult::interrupt();+ 169 } else if (auto read = [true branch at 169:21] 170 ::llvm::dyn_cast<::mlir::vector::TransferReadOp>(op)) {+ 171 if (::mlir::failed( [false branch at 171:11]+ 172 ::loom::lowering::detail::checkRankedVectorTransferRead(+ 173 read, indexBits))) 174 return ::mlir::WalkResult::interrupt();+ 175 } else if (auto write = [true branch at 175:21] 176 ::llvm::dyn_cast<::mlir::vector::TransferWriteOp>(op)) {+ 177 if (::mlir::failed( [false branch at 177:11]+ 178 ::loom::lowering::detail::checkRankedVectorTransferWrite(+ 179 write, indexBits))) 180 return ::mlir::WalkResult::interrupt(); 181 } else if (auto dealloc = ::llvm::dyn_cast<::mlir::memref::DeallocOp>(op)) {@@ 707 if (auto store = ::llvm::dyn_cast<::mlir::memref::StoreOp>(op)) 708 return store.getMemref();+ 709 if (auto read = ::llvm::dyn_cast<::mlir::vector::TransferReadOp>(op)) [true branch at 709:14]+ 710 return read.getBase();+ 711 if (auto write = ::llvm::dyn_cast<::mlir::vector::TransferWriteOp>(op)) [true branch at 711:14]+ 712 return write.getBase(); 713 return {}; 714 }@@ 1144 continue; 1145 }+1146 if (auto read = ::llvm::dyn_cast<::mlir::vector::TransferReadOp>(op)) { [true branch at 1146:16]+1147 lowerVectorRead(read, execution, memory);+1148 continue;+1149 }+1150 if (auto write = ::llvm::dyn_cast<::mlir::vector::TransferWriteOp>(op)) { [true branch at 1150:16]+1151 lowerVectorWrite(write, execution, memory);+1152 continue;+1153 } 1154 if (auto dealloc = ::llvm::dyn_cast<::mlir::memref::DeallocOp>(op)) { 1155 dealloc.erase();@@ 1389 1390 void lowerVectorRead(::mlir::vector::TransferReadOp read,+1391 ::mlir::Value execution, MemoryState &memory) {+1392 ::llvm::SmallVector<unsigned, 4> membership = partitionsFor(read);+1393 ::mlir::Value ctrl = readControl(read, execution, memory);+1394 setInsertionPoint(read.getLoc());+1395 auto memoryType =+1396 ::llvm::cast<::mlir::MemRefType>(read.getBase().getType());+1397 ::mlir::Value address = ::loom::lowering::detail::buildExactLinearIndex(+1398 builder, read.getLoc(), memoryType, read.getIndices(), execution);+1399 auto lowered = ::dataflow::LoadOp::create(+1400 builder, read.getLoc(), read.getVectorType(), builder.getNoneType(),+1401 read.getBase(), address, ctrl, read.getMask(), ::mlir::Attribute{});+1402 partitionsByAccess.try_emplace(lowered, std::move(membership));+1403 read.getResult().replaceAllUsesWith(lowered.getData());+1404 updateReadFrontiers(lowered, lowered.getDone(), memory);+1405 read.erase();+1406 } 1407 1408 void lowerVectorWrite(::mlir::vector::TransferWriteOp write,+1409 ::mlir::Value execution, MemoryState &memory) {+1410 ::llvm::SmallVector<unsigned, 4> membership = partitionsFor(write);+1411 ::mlir::Value ctrl = writeControl(write, execution, memory);+1412 setInsertionPoint(write.getLoc());+1413 auto memoryType =+1414 ::llvm::cast<::mlir::MemRefType>(write.getBase().getType());+1415 ::mlir::Value address = ::loom::lowering::detail::buildExactLinearIndex(+1416 builder, write.getLoc(), memoryType, write.getIndices(), execution);+1417 auto lowered = ::dataflow::StoreOp::create(+1418 builder, write.getLoc(), builder.getNoneType(), write.getBase(),+1419 address, write.getValueToStore(), ctrl, write.getMask(),+1420 ::mlir::Attribute{});+1421 partitionsByAccess.try_emplace(lowered, std::move(membership));+1422 updateWriteFrontiers(lowered, lowered.getDone(), memory);+1423 write.erase();+1424 } 1425 1426 void lowerDataflowLoad(::dataflow::LoadOp load, ::mlir::Value execution,lib/Frontend/Lowering/RankedMemRefLowering.cpp 17 namespace { 18 + 19 bool allTransferDimensionsInBounds(::mlir::ArrayAttr attribute) {+ 20 return attribute && ::llvm::all_of(attribute, [](::mlir::Attribute value) { [true branch at 20:10, true branch at 20:23]+ 21 return ::llvm::cast<::mlir::BoolAttr>(value).getValue();+ 22 });+ 23 } 24 + 25 bool resultIsMaskGuarded(::mlir::vector::TransferReadOp read) {+ 26 ::mlir::Value mask = read.getMask();+ 27 return mask && !read.getResult().use_empty() && [true branch at 27:10, true branch at 27:18]+ 28 ::llvm::all_of( [false branch at 28:10]+ 29 read.getResult().getUsers(), [&](::mlir::Operation *user) {+ 30 auto select = ::llvm::dyn_cast<::mlir::arith::SelectOp>(user);+ 31 return select && select.getCondition() == mask && [false branch at 31:23]+ 32 select.getTrueValue() == read.getResult() &&+ 33 select.getFalseValue() != read.getResult();+ 34 });+ 35 } 36 37 ::mlir::LogicalResult checkRankedVectorTransfer(::mlir::Operation *operation,@@ 41 ::mlir::AffineMap permutation, 42 ::mlir::ArrayAttr inBounds,+ 43 unsigned indexBits) {+ 44 ::llvm::SmallVector<std::int64_t> strides;+ 45 std::int64_t offset = 0;+ 46 if (vector.isScalable() || vector.getRank() != 1 || memory.getRank() != 1 || [false branch at 46:30, false branch at 46:55, false branch at 46:7, false branch at 46:7]+ 47 memory.getElementType() != vector.getElementType() || [false branch at 47:7]+ 48 ::mlir::failed(memory.getStridesAndOffset(strides, offset)) || [false branch at 48:7]+ 49 strides.size() != 1 || strides.front() != 1 || [false branch at 49:30, false branch at 49:7]+ 50 permutation != [false branch at 50:7]+ 51 ::mlir::AffineMap::getMultiDimIdentityMap(1, operation->getContext())) 52 return operation->emitError( 53 "loom-lower-graph-memory: vector transfer requires a fixed rank-one " 54 "minor-identity access over a unit-stride scalar memref");+ 55 if (!allTransferDimensionsInBounds(inBounds)) [false branch at 55:7] 56 return operation->emitError( 57 "loom-lower-graph-memory: vector transfer requires every lane to be " 58 "proven in-bounds");+ 59 return checkRankedMemRefAccess(operation, memory, indices, indexBits);+ 60 } 61 62 } // namespace@@ 115 ::mlir::LogicalResult 116 checkRankedVectorTransferRead(::mlir::vector::TransferReadOp read,+117 unsigned indexBits) {+118 auto memory = ::llvm::dyn_cast<::mlir::MemRefType>(read.getBase().getType());+119 if (!memory) [false branch at 119:7] 120 return read.emitOpError( 121 "loom-lower-graph-memory: vector read requires a ranked memref base");+122 const bool paddingCanBeObserved =+123 read.getMask() && !resultIsMaskGuarded(read); [true branch at 123:25, false branch at 123:7, true branch at 123:7]+124 if (paddingCanBeObserved && [false branch at 124:7, true branch at 124:7, false branch at 124:7]+125 !::mlir::matchPattern(read.getPadding(), ::mlir::m_Zero())) [false branch at 125:7] 126 return read.emitOpError( 127 "loom-lower-graph-memory: observable vector read padding must be " 128 "zero");+129 return checkRankedVectorTransfer(+130 read, memory, read.getIndices(), read.getVectorType(),+131 read.getPermutationMap(), read.getInBounds(), indexBits);+132 } 133 134 ::mlir::LogicalResult 135 checkRankedVectorTransferWrite(::mlir::vector::TransferWriteOp write,+136 unsigned indexBits) {+137 auto memory = ::llvm::dyn_cast<::mlir::MemRefType>(write.getBase().getType());+138 if (!memory || write.getResult()) [false branch at 138:18, false branch at 138:7, false branch at 138:7] 139 return write.emitOpError( 140 "loom-lower-graph-memory: vector write requires a ranked memref base");+141 return checkRankedVectorTransfer(+142 write, memory, write.getIndices(), write.getVectorType(),+143 write.getPermutationMap(), write.getInBounds(), indexBits);+144 } 145 146 ::mlir::Value buildExactLinearIndex(::mlir::OpBuilder &builder,The input was reduced from 30 to 19 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 --mlir-print-op-generic %s | FileCheck %s
module {
dataflow.graph private @graph_0(
%start: none, %i: index, %c: i1, %m: vector<4xi1>,
%av: vector<4xindex>, %val: i32,
%a: memref<16xi32>, %b: memref<16xi32>) -> ()
attributes {input_segments = array<i32: 5, 0, 2>,
result_segments = array<i32: 0, 0, 0>} {
%pad = arith.constant 0 : i32
%g0, %gd0 = dataflow.load %a[%av] %start mask %m : memref<16xi32>, vector<4xindex>, vector<4xi32>
scf.if %c {
%v1 = vector.transfer_read %b[%i], %pad {in_bounds = [true]} : memref<16xi32>, vector<4xi32>
}
scf.if %c {
%v5 = vector.transfer_read %b[%i], %pad, %m {in_bounds = [true]} : memref<16xi32>, vector<4xi32>
vector.transfer_write %v5, %a[%i], %m {in_bounds = [true]} : vector<4xi32>, memref<16xi32>
}
dataflow.graph.return %start : none
}
}
// CHECK: "builtin.module"() ({
// CHECK-NEXT: "dataflow.graph"() <{function_type = (index, i1, vector<4xi1>, vector<4xindex>, i32, memref<16xi32>, memref<16xi32>) -> (), input_segments = array<i32: 5, 0, 2>, result_segments = array<i32: 0, 0, 0>, sym_name = "graph_0", sym_visibility = "private"}> ({
// CHECK-NEXT: ^bb0(%arg0: none, %arg1: index, %arg2: i1, %arg3: vector<4xi1>, %arg4: vector<4xindex>, %arg5: i32, %arg6: memref<16xi32>, %arg7: memref<16xi32>):
// CHECK-NEXT: %0 = "arith.constant"() <{value = 0 : i32}> : () -> i32
// CHECK-NEXT: %1:2 = "dataflow.load"(%arg6, %arg4, %arg0, %arg3) : (memref<16xi32>, vector<4xindex>, none, vector<4xi1>) -> (vector<4xi32>, none)
// CHECK-NEXT: %2:2 = "dataflow.demux"(%arg2, %arg0) : (i1, none) -> (none, none)
// CHECK-NEXT: %3:2 = "dataflow.demux"(%arg2, %arg0) : (i1, none) -> (none, none)
// CHECK-NEXT: %4:2 = "dataflow.demux"(%arg2, %1#1) : (i1, none) -> (none, none)
// CHECK-NEXT: %5:2 = "dataflow.demux"(%arg2, %arg1) : (i1, index) -> (index, index)
// CHECK-NEXT: %6:2 = "dataflow.demux"(%arg2, %0) : (i1, i32) -> (i32, i32)
// CHECK-NEXT: %7:2 = "dataflow.sync"(%2#1, %3#1) : (none, none) -> (none, none)
// CHECK-NEXT: %8:2 = "dataflow.load"(%arg7, %5#1, %7#0) : (memref<16xi32>, index, none) -> (vector<4xi32>, none)
// CHECK-NEXT: %9:2 = "dataflow.sync"(%4#1, %8#1) : (none, none) -> (none, none)
// CHECK-NEXT: %10 = "dataflow.mux"(%arg2, %3#0, %3#1) : (i1, none, none) -> none
// CHECK-NEXT: %11 = "dataflow.mux"(%arg2, %4#0, %9#0) : (i1, none, none) -> none
// CHECK-NEXT: %12 = "dataflow.mux"(%arg2, %2#0, %2#1) : (i1, none, none) -> none
// CHECK-NEXT: %13:2 = "dataflow.demux"(%arg2, %12) : (i1, none) -> (none, none)
// CHECK-NEXT: %14:2 = "dataflow.demux"(%arg2, %10) : (i1, none) -> (none, none)
// CHECK-NEXT: %15:2 = "dataflow.demux"(%arg2, %11) : (i1, none) -> (none, none)
// CHECK-NEXT: %16:2 = "dataflow.demux"(%arg2, %arg1) : (i1, index) -> (index, index)
// CHECK-NEXT: %17:2 = "dataflow.demux"(%arg2, %0) : (i1, i32) -> (i32, i32)
// CHECK-NEXT: %18:2 = "dataflow.demux"(%arg2, %arg3) : (i1, vector<4xi1>) -> (vector<4xi1>, vector<4xi1>)
// CHECK-NEXT: %19:2 = "dataflow.sync"(%13#1, %14#1) : (none, none) -> (none, none)
// CHECK-NEXT: %20:2 = "dataflow.load"(%arg7, %16#1, %19#0, %18#1) : (memref<16xi32>, index, none, vector<4xi1>) -> (vector<4xi32>, none)
// CHECK-NEXT: %21:2 = "dataflow.sync"(%15#1, %20#1) : (none, none) -> (none, none)
// CHECK-NEXT: %22 = "dataflow.store"(%arg6, %16#1, %20#0, %21#0, %18#1) : (memref<16xi32>, index, vector<4xi32>, none, vector<4xi1>) -> none
// CHECK-NEXT: %23 = "dataflow.mux"(%arg2, %15#0, %22) : (i1, none, none) -> none
// CHECK-NEXT: %24 = "dataflow.mux"(%arg2, %13#0, %13#1) : (i1, none, none) -> none
// CHECK-NEXT: "dataflow.graph.return"(%24, %23) <{operandSegmentSizes = array<i32: 0, 0, 0, 2>}> : (none, none) -> ()
// CHECK-NEXT: }) : () -> ()
// CHECK-NEXT: }) : () -> ()
// CHECK-EMPTY:
48615bc5925ef4b9db8b4550b5d4322933cf4b7b.postcondition.spct, SHA-256 c08f4990c78e712426ba965d75e041a5311a52d45abb4c1609b34dedd9f72853).PBT mlir-stage-11-v1, run 20260911-083241, seed 1.
The property under test is anchored on documentation:
docs/spec-compiler-part-3-mem.md lines 245–251 (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 1
LIT test · PR patch · Native verification