E6025

Error · Topology/Hardware

E6025 — A placement naming a location the machine does not have: a memory space no declared topology holds, written either as the space or as the device that would hold it. The derivation between the two spellings has a like-named fallback, so an undeclared name resolves to a space that exists only in the placement that mentions it.

What the compiler reports

Error[E6025]: `Memory::M` in function 'no_parameter' names no location: no declared topology holds `Memory::M`

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

//
// Part of the Vx Project, under the Apache License v2.0 with LLVM Exceptions.
// See LICENSE for license information.
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
//
// `Memory::M` names a memory parameter only in a function with `<M : Memory>`. In any other
// function it must name a memory, and the machine has no memory called `M`.
//

fn with_parameter<M : Memory>(t : &Tensor<i32, [?], Memory::M>) -> i32 {
  return t[0];
}

fn no_parameter(t : &Tensor<i32, [?], Memory::M>) -> i32 {
  return t[0];
}

fn main() -> i32 {
  let h = Tensor<i32, [2]>::fill(3);
  return with_parameter(&h);
}

From tests/frontend/fail/memory_variable_without_a_parameter.vx, which asserts this diagnostic on every commit.

Topologies and memoryThe chapter covering the rule this code enforces. All diagnosticsEvery code the compiler can emit, grouped by stage. E6024A proof obligation could not be discharged because no SMT solver was available. Fails the compilation by default: an undischarged obligation is not a proved one, and treating the two alike is what let a missing z3 certify every seam in silence (Vx#374). Set VX_ALLOW_UNVERIFIED=1 to downgrade this to W1031 and compile anyway. E6026A tensor whose element type the target hardware cannot represent, placed on it anyway. The machine model states what a device has (dtypes: [f32, f16, ...]); this is the check that a placement stays inside it. An H100 has no fp4, so an fp4 tensor placed on one asks for silicon that is not there — and the placement is in the type, so the question is answerable here rather than at a kernel launch on the machine that lacks the type. Only fires against a topology that declares dtypes:. An undeclared machine constrains nothing, which is what keeps every machine file written before the field kept working.

E6025

What the compiler reports

A program that triggers it

Related