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

This adds one LIT test covering 6 lines and 5 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	61–62	49:3–49:26 false; 61:3–61:26 true
lib/Frontend/Lowering/LowerGraphMemoryPass.cpp	461–462, 502–503	461:3–461:45 true; 490:3–490:38 false; 502:3–502:38 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:@@ 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: 64      return llvm::AtomicRMWInst::Min;

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;@@ 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:@@ 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: 505      return ::dataflow::AtomicRmwKind::Min;

The test

The input is 15 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 max %ptr, %desired syncscope("singlethread") release {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 = max, access = <ordering = release, sync_scope = <single_thread>, source_alignment_bytes = 4>>} : memref<?xi32>, !llvm.ptr
// CHECK-NEXT:     dataflow.graph.return %done : 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 2.

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.