This adds one LIT test covering 12 lines and 10 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 |
53–54, 65–66 | 49:3–49:26 false; 53:3–53:26 true; 65:3–65:27 true |
lib/Frontend/Lowering/LowerGraphMemoryPass.cpp |
459–462, 494–495, 506–507 | 459:3–459:45 true; 461:3–461:45 true; 476:43–476:65 true; 490:3–490:38 false; 494:3–494:39 true; 506:3–506:39 true; 770:9–770:29 false |
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: 52 return llvm::AtomicRMWInst::Sub;+53 case AtomicRmwKind::And: [true branch at 53:3]+54 return llvm::AtomicRMWInst::And; 55 case AtomicRmwKind::Nand: 56 return llvm::AtomicRMWInst::Nand;@@ 63 case AtomicRmwKind::Min: 64 return llvm::AtomicRMWInst::Min;+65 case AtomicRmwKind::UMax: [true branch at 65:3]+66 return llvm::AtomicRMWInst::UMax; 67 case AtomicRmwKind::UMin: 68 return llvm::AtomicRMWInst::UMin;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: [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);@@ 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: 493 return ::dataflow::AtomicRmwKind::Sub;+494 case ::mlir::LLVM::AtomicBinOp::_and: [true branch at 494:3]+495 return ::dataflow::AtomicRmwKind::And; 496 case ::mlir::LLVM::AtomicBinOp::nand: 497 return ::dataflow::AtomicRmwKind::Nand;@@ 504 case ::mlir::LLVM::AtomicBinOp::min: 505 return ::dataflow::AtomicRmwKind::Min;+506 case ::mlir::LLVM::AtomicBinOp::umax: [true branch at 506:3]+507 return ::dataflow::AtomicRmwKind::UMax; 508 case ::mlir::LLVM::AtomicBinOp::umin: 509 return ::dataflow::AtomicRmwKind::UMin;@@ 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) 772 loads.push_back(load);The input was reduced from 20 to 17 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>
%val1 = llvm.load volatile %ptr {alignment = 4 : i64} : !llvm.ptr -> i32
%rmw3 = llvm.atomicrmw _and %ptr, %desired release {alignment = 4 : i64} : !llvm.ptr, i32
%rmw4 = llvm.atomicrmw umax %ptr, %desired syncscope("system") acquire {alignment = 8 : 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.load"(%arg6, %0, %arg0) <{contract = #dataflow.plain_access<is_volatile = true>}> : (memref<?xi32>, !llvm.ptr, none) -> (i32, none)
// CHECK-NEXT: %2:2 = "dataflow.atomic_rmw"(%arg6, %0, %arg3, %1#1) <{contract = #dataflow.rmw_contract<kind = and, access = <ordering = release, 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 = umax, access = <ordering = acquire, sync_scope = <system>, source_alignment_bytes = 8>>}> : (memref<?xi32>, !llvm.ptr, i32, none) -> (i32, none)
// CHECK-NEXT: "dataflow.graph.return"(%3#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 207.
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 207
LIT test · PR patch · Native verification