This adds one LIT test covering 31 lines and 22 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 |
47–48, 67–68, 112, 145–147, 291–294, 396–402, 502, 505, 508 | 107:12–107:36 false; 111:7–111:41 true; 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; 47:3–47:27 true; 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; 67:3–67:27 true |
lib/Frontend/Lowering/LowerGraphMemoryPass.cpp |
461–462, 488–489, 508–509, 678–680 | 461:3–461:45 true; 476:43–476:65 true; 488:3–488:39 true; 490:3–490:38 false; 508:3–508:39 true; 674:9–674:72 false; 677:21–677:29 true |
lib/Dataflow/IR/DataflowMemoryContracts.cpp 45 llvm::AtomicRMWInst::BinOp toLLVMBinOp(AtomicRmwKind kind) { 46 switch (kind) {+ 47 case AtomicRmwKind::Xchg: [true branch at 47:3]+ 48 return llvm::AtomicRMWInst::Xchg;+ 49 case AtomicRmwKind::Add: [false branch at 49:3] 50 return llvm::AtomicRMWInst::Add; 51 case AtomicRmwKind::Sub:@@ 65 case AtomicRmwKind::UMax: 66 return llvm::AtomicRMWInst::UMax;+ 67 case AtomicRmwKind::UMin: [true branch at 67:3]+ 68 return llvm::AtomicRMWInst::UMin; 69 case AtomicRmwKind::FAdd: 70 return llvm::AtomicRMWInst::FAdd;@@ 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; 110 llvm::AtomicRMWInst::BinOp binOp = toLLVMBinOp(rmw.getContract().getKind());+111 if (binOp == llvm::AtomicRMWInst::Xchg) [true branch at 111:7]+112 return AtomicElementCategory::IntegerOrFloatingPoint; 113 return llvm::AtomicRMWInst::isFPOperation(binOp) 114 ? AtomicElementCategory::FloatingPoint@@ 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 459 case ::mlir::LLVM::AtomicOrdering::acquire: 460 return ::dataflow::AtomicOrdering::Acquire;+461 case ::mlir::LLVM::AtomicOrdering::release: [true branch at 461:3]+462 return ::dataflow::AtomicOrdering::Release; 463 case ::mlir::LLVM::AtomicOrdering::acq_rel: 464 return ::dataflow::AtomicOrdering::AcqRel;@@ 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);@@ 486 convertAtomicRmwKind(::mlir::LLVM::AtomicBinOp kind) { 487 switch (kind) {+488 case ::mlir::LLVM::AtomicBinOp::xchg: [true branch at 488:3]+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:@@ 506 case ::mlir::LLVM::AtomicBinOp::umax: 507 return ::dataflow::AtomicRmwKind::UMax;+508 case ::mlir::LLVM::AtomicBinOp::umin: [true branch at 508:3]+509 return ::dataflow::AtomicRmwKind::UMin; 510 case ::mlir::LLVM::AtomicBinOp::fadd: 511 return ::dataflow::AtomicRmwKind::FAdd;@@ 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 is 20 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-graph-memory %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>
%rmw0 = llvm.atomicrmw umin %ptr, %desired syncscope("system") acq_rel {alignment = 8 : i64} : !llvm.ptr, i32
llvm.fence syncscope("singlethread") acq_rel
%rmw2 = llvm.atomicrmw add %ptr, %desired syncscope("singlethread") seq_cst {alignment = 8 : i64} : !llvm.ptr, i32
llvm.store %desired, %ptr atomic syncscope("singlethread") monotonic {alignment = 8 : i64} : i32, !llvm.ptr
%rmw4 = llvm.atomicrmw xchg %ptr, %desired syncscope("singlethread") release {alignment = 8 : i64} : !llvm.ptr, i32
llvm.fence syncscope("system") release
dataflow.graph.return %start : none
}
}
// CHECK: module attributes {dlti.dl_spec = #dlti.dl_spec<index = 64 : i64>, llvm.data_layout = "e-p:64:64"} {
// CHECK-NEXT: dataflow.graph private @source_memory_graph(%arg0: none, %arg1: !llvm.ptr, %arg2: i32, %arg3: i32, %arg4: i64, %arg5: i1, %arg6: memref<?xi32>) -> () attributes {input_segments = array<i32: 5, 0, 1>, result_segments = array<i32: 0, 0, 0>} {
// CHECK-NEXT: %0 = llvm.getelementptr inbounds %arg1[%arg4] : (!llvm.ptr, i64) -> !llvm.ptr, !llvm.array<4 x i8>
// CHECK-NEXT: %old, %done = dataflow.atomic_rmw %arg6[%0] %arg3 %arg0 {contract = #dataflow.rmw_contract<kind = umin, access = <ordering = acq_rel, sync_scope = <system>, source_alignment_bytes = 8>>} : memref<?xi32>, !llvm.ptr
// CHECK-NEXT: %1 = dataflow.fence %done {contract = #dataflow.fence_contract<ordering = acq_rel, sync_scope = <single_thread>>}
// CHECK-NEXT: %old_0, %done_1 = dataflow.atomic_rmw %arg6[%0] %arg3 %1 {contract = #dataflow.rmw_contract<kind = add, access = <ordering = seq_cst, sync_scope = <single_thread>, source_alignment_bytes = 8>>} : memref<?xi32>, !llvm.ptr
// CHECK-NEXT: %2 = dataflow.store %arg6[%0] %arg3 %done_1 {contract = #dataflow.atomic_access<ordering = monotonic, sync_scope = <single_thread>, source_alignment_bytes = 8>} : memref<?xi32>, !llvm.ptr
// CHECK-NEXT: %old_2, %done_3 = dataflow.atomic_rmw %arg6[%0] %arg3 %2 {contract = #dataflow.rmw_contract<kind = xchg, access = <ordering = release, sync_scope = <single_thread>, source_alignment_bytes = 8>>} : memref<?xi32>, !llvm.ptr
// CHECK-NEXT: %3 = dataflow.fence %done_3 {contract = #dataflow.fence_contract<ordering = release, sync_scope = <system>>}
// CHECK-NEXT: dataflow.graph.return %3 : none
// CHECK-NEXT: }
// CHECK-NEXT: }
// CHECK-EMPTY:
48615bc5925ef4b9db8b4550b5d4322933cf4b7b.postcondition.spct, SHA-256 840ba12c591c37fe0a0bf28ef27f6f8a496505d00629390bb6209f57e770e9bb).PBT mlir-stage-13-v1, run 20260911-083853, seed 2449.
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 2449
LIT test · PR patch · Native verification