E6018

Error · Topology/Hardware

E6018 — A raw:: bounds obligation (0 <= index < extent) that could not be proven. Prove it with a loop bound or invariant the SMT prover can see, or assert it in an unsafe block — which records the obligation as asserted-not-proven, the same standing an unverified spec: figure has.

What the compiler reports

E6018
stays inside

The fragments the test suite holds the compiler to. An ellipsis marks text the test does not constrain; the emitted message also carries a source location.

A program that triggers it

// A bounds obligation the prover can refute: i == 7 against extent 4. Outside
// an unsafe block, unprovable bounds are an error, not a warning.
Topology Dev {
  memory: Memory::L2,
  visible: [Memory::L2, Memory::SMEM],
  transfer Memory::CPU_DRAM -> Memory::L2 : 10 GB/s,
  transfer Memory::L2 -> Memory::SMEM
}
impl Transfer<Memory::L2, Memory::SMEM> for Topology::Dev {
  fn move_tile(src: &Tensor<f32, [4]>, dst: &mut Tensor<f32, [4]>) -> i32 {
    let i = 7;
    raw::store(dst, i, raw::load(src, i));
    raw::barrier();
    return 0;
  }
}
fn main() -> i32 {
  return 0;
}

From tests/middle_end/fail/raw_bounds_unprovable.vx, which asserts this diagnostic on every commit.

Related