This adds one LIT test covering 23 lines and 18 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/DataflowMemoryContracts.cpp |
145–147, 259–262, 266, 269, 291–294, 396–402, 502, 505, 508 | 107:12–107:36 false; 135:3–135:38 false; 145:3–145:53 true; 146:9–146:18 true; 257:9–257:42 false; 260:9–262:59 false; 266:9–266:58 false; 292:10–292:45 false; 293:10–293:44 false; 392:18–392:23 false; 482:27–482:47 true; 500:12–500:18 true; 502:34–502:73 false; 502:9–502:30 false; 502:9–502:30 true; 505:35–505:74 false; 505:9–505:31 false; 505:9–505:31 true |
lib/Dataflow/IR/DataflowMemoryContracts.cpp 105 auto rmw = llvm::dyn_cast<AtomicRmwOp>(op); 106 if (!rmw)+107 return llvm::isa<CmpXchgOp>(op) [false branch at 107:12] 108 ? AtomicElementCategory::Integer 109 : AtomicElementCategory::IntegerOrFloatingPoint;@@ 133 const char *required = ""; 134 switch (category) {+135 case AtomicElementCategory::Integer: [false branch at 135:3] 136 if (isInteger) 137 return llvm::Error::success();@@ 143 required = "floating-point"; 144 break;+145 case AtomicElementCategory::IntegerOrFloatingPoint: [true branch at 145:3]+146 if (isInteger || isFloat) [true branch at 146:9]+147 return llvm::Error::success(); 148 required = "integer or floating-point"; 149 break;@@ 255 llvm::Error validateSingleContractOwner(Operation *op) { 256 for (NamedAttribute attribute : op->getAttrs()) {+257 if (attribute.getName() == "contract") [false branch at 257:9] 258 continue;+259 llvm::StringRef name = attribute.getName().strref();+260 if (llvm::isa<PlainAccessContractAttr, AtomicAccessContractAttr, [false branch at 260:9]+261 AtomicRmwContractAttr, CompareExchangeContractAttr,+262 FenceContractAttr>(attribute.getValue())) 263 return contractError("'" + name + 264 "' must not carry a second aggregate memory " 265 "contract");+266 if (llvm::isa<SyncScopeRefAttr>(attribute.getValue())) [false branch at 266:9] 267 return contractError("'" + name + 268 "' must not carry a second synchronization scope");+269 } 270 return llvm::Error::success(); 271 }@@ 289 290 /// The orderings an atomic store rejects.+291 bool isAcquireOrAcqRel(AtomicOrdering ordering) {+292 return ordering == AtomicOrdering::Acquire || [false branch at 292:10]+293 ordering == AtomicOrdering::AcqRel; [false branch at 293:10]+294 } 295 296 /// `source_alignment_bytes` is identity-critical typed state and must be a@@ 390 aggregate = PlainAccessContractAttr::get(typedOp.getContext(), 391 /*is_volatile=*/false);+392 if (auto plain = llvm::dyn_cast<PlainAccessContractAttr>(aggregate)) [false branch at 392:18] 393 return MemoryActorContract{ 394 aggregate, /*atomic=*/false, plain.getIsVolatile(), 395 std::nullopt, std::nullopt, SyncScopeRefAttr()};+396 auto access = llvm::cast<AtomicAccessContractAttr>(aggregate);+397 return MemoryActorContract{aggregate,+398 /*atomic=*/true,+399 access.getIsVolatile(),+400 access.getSourceAlignmentBytes(),+401 access.getVectorGranularity(),+402 access.getSyncScope()}; 403 }) 404 .Case<AtomicRmwOp>([](AtomicRmwOp typedOp) {@@ 480 // these. Duplicate effect kinds across the bound and unbound forms are 481 // intentional.+482 if (contract->atomic || contract->isVolatile) { [true branch at 482:27] 483 effects.emplace_back(MemoryEffects::Read::get()); 484 effects.emplace_back(MemoryEffects::Write::get());@@ 498 // Only dataflow.load and dataflow.store nest a bare atomic access contract, 499 // and each rejects the orderings its direction cannot express.+500 if (auto atomic = [true branch at 500:12] 501 llvm::dyn_cast<AtomicAccessContractAttr>(contract->aggregate)) {+502 if (llvm::isa<LoadOp>(op) && isReleaseOrAcqRel(atomic.getOrdering())) [false branch at 502:34, false branch at 502:9, true branch at 502:9] 503 return contractError("atomic load ordering must not be 'release' or " 504 "'acq_rel'");+505 if (llvm::isa<StoreOp>(op) && isAcquireOrAcqRel(atomic.getOrdering())) [false branch at 505:35, false branch at 505:9, true branch at 505:9] 506 return contractError("atomic store ordering must not be 'acquire' or " 507 "'acq_rel'");+508 } 509 if (auto rmw = llvm::dyn_cast<AtomicRmwOp>(op)) 510 if (rmw.getContract().getAccess().getOrdering() ==The input was reduced from 12 to 11 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
dataflow.graph private @sb_strand(
%start: none, %idx: index, %val: i32, %exp: i32, %des: i32,
%a: memref<16xi32>, %b: memref<16xi32>) -> ()
attributes {input_segments = array<i32: 4, 0, 2>,
result_segments = array<i32: 0, 0, 0>} {
%r0, %d0 = dataflow.load %b[%idx] %start {sb_index = 0 : i64} : memref<16xi32>
%r2, %d2 = dataflow.load %b[%idx] %start {contract = #dataflow.plain_access<is_volatile = true>, sb_index = 2 : i64} : memref<16xi32>
%r3, %d3 = dataflow.load %a[%idx] %start {contract = #dataflow.atomic_access<ordering = acquire, sync_scope = <system>, source_alignment_bytes = 4>, sb_index = 3 : i64} : memref<16xi32>
%d4 = dataflow.store %a[%idx] %val %start {contract = #dataflow.atomic_access<ordering = release, sync_scope = <system>, source_alignment_bytes = 4>, sb_index = 4 : i64} : memref<16xi32>
dataflow.graph.return %start : none
}
// CHECK: "builtin.module"() ({
// CHECK-NEXT: "dataflow.graph"() <{function_type = (index, i32, i32, i32, memref<16xi32>, memref<16xi32>) -> (), input_segments = array<i32: 4, 0, 2>, result_segments = array<i32: 0, 0, 0>, sym_name = "sb_strand", sym_visibility = "private"}> ({
// CHECK-NEXT: ^bb0(%arg0: none, %arg1: index, %arg2: i32, %arg3: i32, %arg4: i32, %arg5: memref<16xi32>, %arg6: memref<16xi32>):
// CHECK-NEXT: %0:2 = "dataflow.load"(%arg6, %arg1, %arg0) {sb_index = 0 : i64} : (memref<16xi32>, index, none) -> (i32, none)
// CHECK-NEXT: %1:2 = "dataflow.load"(%arg6, %arg1, %arg0) <{contract = #dataflow.plain_access<is_volatile = true>}> {sb_index = 2 : i64} : (memref<16xi32>, index, none) -> (i32, none)
// CHECK-NEXT: %2:2 = "dataflow.load"(%arg5, %arg1, %arg0) <{contract = #dataflow.atomic_access<ordering = acquire, sync_scope = <system>, source_alignment_bytes = 4>}> {sb_index = 3 : i64} : (memref<16xi32>, index, none) -> (i32, none)
// CHECK-NEXT: %3 = "dataflow.store"(%arg5, %arg1, %arg2, %5#0) <{contract = #dataflow.atomic_access<ordering = release, sync_scope = <system>, source_alignment_bytes = 4>}> {sb_index = 4 : i64} : (memref<16xi32>, index, i32, none) -> none
// CHECK-NEXT: %4:2 = "dataflow.sync"(%0#1, %1#1) : (none, none) -> (none, none)
// CHECK-NEXT: %5:2 = "dataflow.sync"(%4#0, %2#1) : (none, none) -> (none, none)
// CHECK-NEXT: "dataflow.graph.return"(%3) <{operandSegmentSizes = array<i32: 0, 0, 0, 1>}> : (none) -> ()
// CHECK-NEXT: }) : () -> ()
// CHECK-NEXT: }) : () -> ()
// CHECK-EMPTY:
48615bc5925ef4b9db8b4550b5d4322933cf4b7b.postcondition.spct, SHA-256 981132546aa01e9aa4e6c62c2c474f81842870b55876f465b2fa7c9591848256).PBT mlir-stage-08-v1, run 20260911-082329, seed 38.
The property under test is anchored on documentation:
docs/spec-compiler-part-3-mem.md lines 228–238 (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 38
LIT test · PR patch · Native verification