Add a regression test for mlir-stage-13-v1

This adds one LIT test covering 16 lines and 12 branch outcomes that the existing suite does not reach, across 2 source files, at 48615bc5925ef4b9db8b4550b5d4322933cf4b7b.

Coverage this test adds

Source file	Newly covered lines	Newly covered branch outcomes
lib/Dataflow/IR/DataflowMemoryContracts.cpp	53–54, 57–58, 63–64	49:3–49:26 false; 53:3–53:26 true; 57:3–57:25 true; 63:3–63:26 true
lib/Frontend/Lowering/LowerGraphMemoryPass.cpp	459–462, 494–495, 498–499, 504–505	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; 498:3–498:38 true; 504:3–504:38 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;+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: 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;

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;+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: 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;@@ 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 test

The input was reduced from 20 to 19 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 %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 _and %ptr, %desired syncscope("system") seq_cst {alignment = 8 : i64} : !llvm.ptr, i32
    %rmw1 = llvm.atomicrmw _or %ptr, %desired syncscope("system") release {alignment = 8 : i64} : !llvm.ptr, i32
    %val3 = llvm.load volatile %ptr {alignment = 4 : i64} : !llvm.ptr -> i32
    %rmw4 = llvm.atomicrmw min %ptr, %desired syncscope("singlethread") monotonic {alignment = 4 : i64} : !llvm.ptr, i32
    %pair5 = llvm.cmpxchg %ptr, %expected, %desired syncscope("singlethread") acquire acquire {alignment = 4 : i64} : !llvm.ptr, i32
    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 = and, access = <ordering = seq_cst, sync_scope = <system>, source_alignment_bytes = 8>>} : memref<?xi32>, !llvm.ptr
// CHECK-NEXT:     %old_0, %done_1 = dataflow.atomic_rmw %arg6[%0] %arg3 %done {contract = #dataflow.rmw_contract<kind = or, access = <ordering = release, sync_scope = <system>, source_alignment_bytes = 8>>} : memref<?xi32>, !llvm.ptr
// CHECK-NEXT:     %data, %done_2 = dataflow.load %arg6[%0] %done_1 {contract = #dataflow.plain_access<is_volatile = true>} : memref<?xi32>, !llvm.ptr
// CHECK-NEXT:     %old_3, %done_4 = dataflow.atomic_rmw %arg6[%0] %arg3 %done_2 {contract = #dataflow.rmw_contract<kind = min, access = <ordering = monotonic, sync_scope = <single_thread>, source_alignment_bytes = 4>>} : memref<?xi32>, !llvm.ptr
// CHECK-NEXT:     %old_5, %success, %done_6 = dataflow.cmpxchg %arg6[%0] %arg2 %arg3 %done_4 {contract = #dataflow.cmpxchg_contract<success_ordering = acquire, failure_ordering = acquire, sync_scope = <single_thread>, source_alignment_bytes = 4>} : memref<?xi32>, !llvm.ptr -> i1
// CHECK-NEXT:     %1 = llvm.mlir.undef : !llvm.struct<(i32, i1)>
// CHECK-NEXT:     %2 = llvm.insertvalue %old_5, %1[0] : !llvm.struct<(i32, i1)> 
// CHECK-NEXT:     %3 = llvm.insertvalue %success, %2[1] : !llvm.struct<(i32, i1)> 
// CHECK-NEXT:     dataflow.graph.return %done_6 : none
// CHECK-NEXT:   }
// CHECK-NEXT: }
// CHECK-EMPTY:

Validation

• Native compiler and FileCheck replay: passed at 48615bc5925ef4b9db8b4550b5d4322933cf4b7b.
• Property checker verdict on the reduced pair: PASS (postcondition.spct, SHA-256 840ba12c591c37fe0a0bf28ef27f6f8a496505d00629390bb6209f57e770e9bb).
• Reduction criterion: accepted checker PASS and every original line/branch increment over the suite baseline; the original postcondition BDD decision path is unchanged; every original fast edge increment over its suite baseline.

Where this test came from

PBT mlir-stage-13-v1, run 20260911-083853, seed 1617.

The property under test is anchored on documentation:

• selected output: docs/spec-compiler-part-3-mem.md lines 482–486 (output side)
• linked input 29: docs/spec-compiler-part-3-mem.md lines 482–486 (input side)
• linked input 32: docs/spec-compiler-part-3-mem.md lines 92–97 (input side)
• linked input 50: docs/spec-compiler-part-3-mem.md lines 148–152 (input side)
• linked input 59: docs/spec-compiler-part-3-mem.md lines 136–140 (input side)
• linked input 66: docs/spec-compiler-part-3-mem.md lines 489–493 (input side)
• linked input 67: docs/spec-compiler-part-3-mem.md lines 3–6 (input side)
• linked input 68: docs/spec-compiler-part-3-mem.md lines 79–90 (input side)
• linked input 80: docs/spec-compiler-part-3-mem.md lines 99–106 (input side)
• linked input 102: docs/spec-compiler-part-3-mem.md lines 389–393 (input side)
• linked input 104: docs/spec-compiler-part-3-mem.md lines 470–480 (input side)
• linked input 115: docs/spec-compiler-part-3-mem.md lines 486–489 (input side)
• linked input 126: docs/spec-compiler-part-3-mem.md lines 142–146 (input side)
• linked input 149: docs/spec-compiler-part-3-mem.md lines 43–46 (input side)
• linked input 170: docs/spec-compiler-part-3-mem.md lines 154–157 (input side)
• linked input 182: docs/spec-compiler-part-3-mem.md lines 382–387 (input side)
• linked input 184: docs/spec-compiler-part-3-mem.md lines 34–35 (input side)
• linked input 195: docs/spec-compiler-part-3-mem.md lines 159–161 (input side)
• linked input 200: docs/spec-compiler-part-3-mem.md lines 40–41 (input side)
• linked input 202: docs/spec-compiler-part-3-mem.md lines 31–32 (input side)
• linked input 211: 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.