This adds one LIT test covering 34 lines and 29 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, 51–52, 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: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; 51:3–51:26 true |
lib/Frontend/Lowering/LowerGraphMemoryPass.cpp |
461–462, 488–489, 492–493, 662–664, 678–680 | 461:3–461:45 true; 476:43–476:65 true; 488:3–488:39 true; 490:3–490:38 false; 492:3–492:38 true; 658:9–658:71 false; 661:21–661:29 true; 674:9–674:72 false; 677:21–677:29 true; 770:9–770:29 false; 771:9–771:71 false |
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: [true branch at 51:3]+ 52 return llvm::AtomicRMWInst::Sub; 53 case AtomicRmwKind::And: 54 return llvm::AtomicRMWInst::And;@@ 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: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() ==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: [true branch at 492:3]+493 return ::dataflow::AtomicRmwKind::Sub; 494 case ::mlir::LLVM::AtomicBinOp::_and: 495 return ::dataflow::AtomicRmwKind::And;@@ 656 auto lowered = ::dataflow::LoadOp::create( 657 builder, loc, elemTy, builder.getNoneType(), mem, address, ctx.ctrl);+658 if (load.getOrdering() == ::mlir::LLVM::AtomicOrdering::not_atomic) { [false branch at 658:9] 659 lowered.setContractAttr(::dataflow::PlainAccessContractAttr::get( 660 ctx.graph.getContext(), load.getVolatile_()));+661 } else if (auto contract = makeAtomicAccessContract( [true branch at 661:21]+662 load, ctx.graph.getContext(), elemTy)) {+663 lowered.setContractAttr(*contract);+664 } else { 665 lowered.erase(); 666 return false;@@ 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;@@ 768 ::llvm::SmallVector<::mlir::LLVM::LoadOp, 4> loads; 769 graph.getBody().walk([&](::mlir::LLVM::LoadOp load) {+770 if (!load.getVolatile_() && [false branch at 770:9]+771 load.getOrdering() == ::mlir::LLVM::AtomicOrdering::not_atomic) [false branch at 771:9] 772 loads.push_back(load); 773 });The input is 21 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 --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>
scf.if %cond {
llvm.store %desired, %ptr atomic syncscope("system") monotonic {alignment = 4 : i64} : i32, !llvm.ptr
%val1 = llvm.load volatile %ptr {alignment = 8 : i64} : !llvm.ptr -> i32
%rmw2 = llvm.atomicrmw sub %ptr, %desired release {alignment = 4 : i64} : !llvm.ptr, i32
%rmw3 = llvm.atomicrmw xchg %ptr, %desired syncscope("singlethread") acq_rel {alignment = 4 : i64} : !llvm.ptr, i32
%val4 = llvm.load %ptr atomic syncscope("singlethread") monotonic {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:2 = "dataflow.demux"(%arg5, %arg0) : (i1, none) -> (none, none)
// CHECK-NEXT: %2:2 = "dataflow.demux"(%arg5, %arg0) : (i1, none) -> (none, none)
// CHECK-NEXT: %3:2 = "dataflow.demux"(%arg5, %arg0) : (i1, none) -> (none, none)
// CHECK-NEXT: %4:2 = "dataflow.demux"(%arg5, %0) : (i1, !llvm.ptr) -> (!llvm.ptr, !llvm.ptr)
// CHECK-NEXT: %5:2 = "dataflow.demux"(%arg5, %arg3) : (i1, i32) -> (i32, i32)
// CHECK-NEXT: %6:2 = "dataflow.sync"(%1#1, %3#1) : (none, none) -> (none, none)
// CHECK-NEXT: %7 = "dataflow.store"(%arg6, %4#1, %5#1, %6#0) <{contract = #dataflow.atomic_access<ordering = monotonic, sync_scope = <system>, source_alignment_bytes = 4>}> : (memref<?xi32>, !llvm.ptr, i32, none) -> none
// CHECK-NEXT: %8:2 = "dataflow.load"(%arg6, %4#1, %7) <{contract = #dataflow.plain_access<is_volatile = true>}> : (memref<?xi32>, !llvm.ptr, none) -> (i32, none)
// CHECK-NEXT: %9:2 = "dataflow.atomic_rmw"(%arg6, %4#1, %5#1, %8#1) <{contract = #dataflow.rmw_contract<kind = sub, access = <ordering = release, sync_scope = <system>, source_alignment_bytes = 4>>}> : (memref<?xi32>, !llvm.ptr, i32, none) -> (i32, none)
// CHECK-NEXT: %10:2 = "dataflow.atomic_rmw"(%arg6, %4#1, %5#1, %9#1) <{contract = #dataflow.rmw_contract<kind = xchg, access = <ordering = acq_rel, sync_scope = <single_thread>, source_alignment_bytes = 4>>}> : (memref<?xi32>, !llvm.ptr, i32, none) -> (i32, none)
// CHECK-NEXT: %11:2 = "dataflow.load"(%arg6, %4#1, %10#1) <{contract = #dataflow.atomic_access<ordering = monotonic, sync_scope = <single_thread>, source_alignment_bytes = 4>}> : (memref<?xi32>, !llvm.ptr, none) -> (i32, none)
// CHECK-NEXT: %12 = "dataflow.mux"(%arg5, %3#0, %11#1) : (i1, none, none) -> none
// CHECK-NEXT: %13 = "dataflow.mux"(%arg5, %1#0, %10#1) : (i1, none, none) -> none
// CHECK-NEXT: "dataflow.graph.return"(%13, %12) <{operandSegmentSizes = array<i32: 0, 0, 0, 2>}> : (none, 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 528.
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 528
LIT test · PR patch · Native verification