This adds one LIT test covering 34 lines and 23 branch outcomes that the existing suite does not reach, across 2 source files, at 48615bc5925ef4b9db8b4550b5d4322933cf4b7b.
| Source file | Newly covered lines | Newly covered branch outcomes |
|---|---|---|
lib/Dataflow/IR/DataflowMemoryContracts.cpp |
57–58, 61–64, 145–147, 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; 292:10–292:45 false; 293:10–293:44 false; 392:18–392:23 false; 49:3–49:26 false; 500:12–500:18 true; 502:9–502:30 false; 505:35–505:74 false; 505:9–505:31 true; 57:3–57:25 true; 61:3–61:26 true; 63:3–63:26 true |
lib/Frontend/Lowering/LowerGraphMemoryPass.cpp |
459–460, 498–499, 502–505, 678–680 | 459:3–459:45 true; 476:43–476:65 true; 490:3–490:38 false; 498:3–498:38 true; 502:3–502:38 true; 504:3–504:38 true; 674:9–674:72 false; 677:21–677:29 true |
lib/Dataflow/IR/DataflowMemoryContracts.cpp 47 case AtomicRmwKind::Xchg: 48 return llvm::AtomicRMWInst::Xchg;+ 49 case AtomicRmwKind::Add: [false branch at 49:3] 50 return llvm::AtomicRMWInst::Add; 51 case AtomicRmwKind::Sub:@@ 55 case AtomicRmwKind::Nand: 56 return llvm::AtomicRMWInst::Nand;+ 57 case AtomicRmwKind::Or: [true branch at 57:3]+ 58 return llvm::AtomicRMWInst::Or; 59 case AtomicRmwKind::Xor: 60 return llvm::AtomicRMWInst::Xor;+ 61 case AtomicRmwKind::Max: [true branch at 61:3]+ 62 return llvm::AtomicRMWInst::Max;+ 63 case AtomicRmwKind::Min: [true branch at 63:3]+ 64 return llvm::AtomicRMWInst::Min; 65 case AtomicRmwKind::UMax: 66 return llvm::AtomicRMWInst::UMax;@@ 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;@@ 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) {@@ 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: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, 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() ==lib/Frontend/Lowering/LowerGraphMemoryPass.cpp 457 case ::mlir::LLVM::AtomicOrdering::monotonic: 458 return ::dataflow::AtomicOrdering::Monotonic;+459 case ::mlir::LLVM::AtomicOrdering::acquire: [true branch at 459:3]+460 return ::dataflow::AtomicOrdering::Acquire; 461 case ::mlir::LLVM::AtomicOrdering::release: 462 return ::dataflow::AtomicOrdering::Release;@@ 474 convertSyncScope(::mlir::MLIRContext *context, 475 std::optional<::llvm::StringRef> syncscope) {+476 if (!syncscope || syncscope->empty() || *syncscope == "system") [true branch at 476:43] 477 return ::dataflow::SyncScopeRefAttr::get( 478 context, ::dataflow::SyncScopeKind::System);@@ 488 case ::mlir::LLVM::AtomicBinOp::xchg: 489 return ::dataflow::AtomicRmwKind::Xchg;+490 case ::mlir::LLVM::AtomicBinOp::add: [false branch at 490:3] 491 return ::dataflow::AtomicRmwKind::Add; 492 case ::mlir::LLVM::AtomicBinOp::sub:@@ 496 case ::mlir::LLVM::AtomicBinOp::nand: 497 return ::dataflow::AtomicRmwKind::Nand;+498 case ::mlir::LLVM::AtomicBinOp::_or: [true branch at 498:3]+499 return ::dataflow::AtomicRmwKind::Or; 500 case ::mlir::LLVM::AtomicBinOp::_xor: 501 return ::dataflow::AtomicRmwKind::Xor;+502 case ::mlir::LLVM::AtomicBinOp::max: [true branch at 502:3]+503 return ::dataflow::AtomicRmwKind::Max;+504 case ::mlir::LLVM::AtomicBinOp::min: [true branch at 504:3]+505 return ::dataflow::AtomicRmwKind::Min; 506 case ::mlir::LLVM::AtomicBinOp::umax: 507 return ::dataflow::AtomicRmwKind::UMax;@@ 672 builder, loc, builder.getNoneType(), mem, address, store.getValue(), 673 ctx.ctrl);+674 if (store.getOrdering() == ::mlir::LLVM::AtomicOrdering::not_atomic) { [false branch at 674:9] 675 lowered.setContractAttr(::dataflow::PlainAccessContractAttr::get( 676 ctx.graph.getContext(), store.getVolatile_()));+677 } else if (auto contract = makeAtomicAccessContract( [true branch at 677:21]+678 store, ctx.graph.getContext(), store.getValue().getType())) {+679 lowered.setContractAttr(*contract);+680 } else { 681 lowered.erase(); 682 return false;The input was reduced from 19 to 18 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 attributes {
llvm.data_layout = "e-p:64:64",
dlti.dl_spec = #dlti.dl_spec<#dlti.dl_entry<index, 64>>
} {
dataflow.graph private @source_memory_graph(
%start: none, %base: !llvm.ptr, %expected: i32, %desired: i32,
%index: i64, %cond: i1) -> ()
attributes {input_segments = array<i32: 5, 0, 0>,
result_segments = array<i32: 0, 0, 0>} {
%ptr = llvm.getelementptr inbounds %base[%index]
: (!llvm.ptr, i64) -> !llvm.ptr, !llvm.array<4 x i8>
llvm.store %desired, %ptr atomic syncscope("system") monotonic {alignment = 8 : i64} : i32, !llvm.ptr
%rmw2 = llvm.atomicrmw min %ptr, %desired acquire {alignment = 4 : i64} : !llvm.ptr, i32
%rmw3 = llvm.atomicrmw _or %ptr, %desired seq_cst {alignment = 8 : i64} : !llvm.ptr, i32
%rmw4 = llvm.atomicrmw max %ptr, %desired acq_rel {alignment = 4 : i64} : !llvm.ptr, i32
dataflow.graph.return %start : none
}
}
// CHECK: "builtin.module"() ({
// CHECK-NEXT: "dataflow.graph"() <{function_type = (!llvm.ptr, i32, i32, i64, i1, memref<?xi32>) -> (), input_segments = array<i32: 5, 0, 1>, result_segments = array<i32: 0, 0, 0>, sym_name = "source_memory_graph", sym_visibility = "private"}> ({
// CHECK-NEXT: ^bb0(%arg0: none, %arg1: !llvm.ptr, %arg2: i32, %arg3: i32, %arg4: i64, %arg5: i1, %arg6: memref<?xi32>):
// CHECK-NEXT: %0 = "llvm.getelementptr"(%arg1, %arg4) <{elem_type = !llvm.array<4 x i8>, noWrapFlags = 3 : i32, rawConstantIndices = array<i32: -2147483648>}> : (!llvm.ptr, i64) -> !llvm.ptr
// CHECK-NEXT: %1 = "dataflow.store"(%arg6, %0, %arg3, %arg0) <{contract = #dataflow.atomic_access<ordering = monotonic, sync_scope = <system>, source_alignment_bytes = 8>}> : (memref<?xi32>, !llvm.ptr, i32, none) -> none
// CHECK-NEXT: %2:2 = "dataflow.atomic_rmw"(%arg6, %0, %arg3, %1) <{contract = #dataflow.rmw_contract<kind = min, access = <ordering = acquire, sync_scope = <system>, source_alignment_bytes = 4>>}> : (memref<?xi32>, !llvm.ptr, i32, none) -> (i32, none)
// CHECK-NEXT: %3:2 = "dataflow.atomic_rmw"(%arg6, %0, %arg3, %2#1) <{contract = #dataflow.rmw_contract<kind = or, access = <ordering = seq_cst, sync_scope = <system>, source_alignment_bytes = 8>>}> : (memref<?xi32>, !llvm.ptr, i32, none) -> (i32, none)
// CHECK-NEXT: %4:2 = "dataflow.atomic_rmw"(%arg6, %0, %arg3, %3#1) <{contract = #dataflow.rmw_contract<kind = max, access = <ordering = acq_rel, sync_scope = <system>, source_alignment_bytes = 4>>}> : (memref<?xi32>, !llvm.ptr, i32, none) -> (i32, none)
// CHECK-NEXT: "dataflow.graph.return"(%4#1) <{operandSegmentSizes = array<i32: 0, 0, 0, 1>}> : (none) -> ()
// CHECK-NEXT: }) : () -> ()
// CHECK-NEXT: }) {dlti.dl_spec = #dlti.dl_spec<index = 64 : i64>, llvm.data_layout = "e-p:64:64"} : () -> ()
// CHECK-EMPTY:
48615bc5925ef4b9db8b4550b5d4322933cf4b7b.postcondition.spct, SHA-256 840ba12c591c37fe0a0bf28ef27f6f8a496505d00629390bb6209f57e770e9bb).PBT mlir-stage-13-v1, run 20260911-083853, seed 40.
The property under test is anchored on documentation:
docs/spec-compiler-part-3-mem.md lines 482–486 (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 40
LIT test · PR patch · Native verification