Add explicit overflow-semantics attribute to cast ops and require/verify it (fixes #256)#260
Open
nileshaher-2024si96522 wants to merge 3 commits intoproject-llzk:mainfrom
Open
Add explicit overflow-semantics attribute to cast ops and require/verify it (fixes #256)#260nileshaher-2024si96522 wants to merge 3 commits intoproject-llzk:mainfrom
nileshaher-2024si96522 wants to merge 3 commits intoproject-llzk:mainfrom
Conversation
tim-hoffman
requested changes
Jan 12, 2026
Member
tim-hoffman
left a comment
tim-hoffman
left a comment
There was a problem hiding this comment.
Hi, thanks for your willingness to contribute. There are a lot of issues that need to be addressed for this PR to be accepted.
Comment on lines
+1
to
+13
| //===-- Attrs.td --------------------------------------------*- tablegen -*-===// | ||
| // | ||
| // Attrs used by the Cast dialect. | ||
| // | ||
| // This file defines an attribute that encodes overflow semantics for narrowing | ||
| // casts. The attribute is named `OverflowSemanticsAttr` and supports two values: | ||
| // - "trunc" (truncate, i.e., wrap/truncate) | ||
| // - "sat" (saturate) | ||
| // | ||
| // The Ops.td file requires this attribute on all cast ops that need explicit | ||
| // overflow semantics. | ||
| // | ||
| //===----------------------------------------------------------------------===// |
Member
There was a problem hiding this comment.
Missing license. No need to full description here. That goes on the attrs itself.
Suggested change
| //===-- Attrs.td --------------------------------------------*- tablegen -*-===// | |
| // | |
| // Attrs used by the Cast dialect. | |
| // | |
| // This file defines an attribute that encodes overflow semantics for narrowing | |
| // casts. The attribute is named `OverflowSemanticsAttr` and supports two values: | |
| // - "trunc" (truncate, i.e., wrap/truncate) | |
| // - "sat" (saturate) | |
| // | |
| // The Ops.td file requires this attribute on all cast ops that need explicit | |
| // overflow semantics. | |
| // | |
| //===----------------------------------------------------------------------===// | |
| //===-- Attrs.td -------------------------------------------*- tablegen -*-===// | |
| // | |
| // Part of the LLZK Project, under the Apache License v2.0. | |
| // See LICENSE.txt for license information. | |
| // Copyright 2025 Veridise Inc. | |
| // SPDX-License-Identifier: Apache-2.0 | |
| // | |
| //===----------------------------------------------------------------------===// |
| { let name = "trunc"; let value = 0; let cppEnumName = "Trunc"; }, | ||
| { let name = "sat"; let value = 1; let cppEnumName = "Sat"; } | ||
| ]; | ||
| } No newline at end of file |
Member
There was a problem hiding this comment.
missing newline at EOF
Suggested change
| } | |
| } | |
| add_public_tablegen_target(CastDialectIncGen) | ||
| add_dependencies(mlir-headers CastDialectIncGen) | ||
| add_dependencies(LLZKDialectHeaders CastDialectIncGen) | ||
| add_dependencies(LLZKDialectHeaders CastDialectIncGen) No newline at end of file |
Member
There was a problem hiding this comment.
missing newline at EOF
Suggested change
| add_dependencies(LLZKDialectHeaders CastDialectIncGen) | |
| add_dependencies(LLZKDialectHeaders CastDialectIncGen) | |
| ::mlir::LogicalResult verify(); | ||
| }]; | ||
| } | ||
| #endif // LLZK_CAST_OPS No newline at end of file |
Member
There was a problem hiding this comment.
missing newline at EOF
Suggested change
| #endif // LLZK_CAST_OPS | |
| #endif // LLZK_CAST_OPS | |
| } // namespace llzk::cast | ||
| ::mlir::LogicalResult llzk::cast::FeltToIntOp::verify() { | ||
| return verifyOverflowAttr(getOperation()); | ||
| } No newline at end of file |
Member
There was a problem hiding this comment.
missing newline at EOF
Suggested change
| } | |
| } | |
Comment on lines
+4
to
+5
| # New file: Attrs.td defines the overflow semantics attribute | ||
| set(LLVM_TARGET_DEFINITIONS "${LLVM_TARGET_DEFINITIONS};Attrs.td") |
Member
There was a problem hiding this comment.
This is incorrect. You've put this in the middle of the Dialect gen section. Attrs.td should have its own section like:
set(LLVM_TARGET_DEFINITIONS "Attrs.td")
mlir_tablegen(Attrs.h.inc -gen-attrdef-decls -attrdefs-dialect=cast)
mlir_tablegen(Attrs.cpp.inc -gen-attrdef-defs -attrdefs-dialect=cast)
Comment on lines
+10
to
+11
| # Ops.td depends on Attrs.td, ensure it is present for tablegen | ||
| set(LLVM_TARGET_DEFINITIONS "${LLVM_TARGET_DEFINITIONS};Ops.td") |
Comment on lines
37
to
+38
| let arguments = (ins AnySignlessIntegerOrIndex:$value); | ||
| let attributes = (ins OverflowSemanticsAttr:$overflow); |
Member
There was a problem hiding this comment.
Invalid tablegen syntax. The attribute should be included in the arguments list.
(same in other ops below)
Comment on lines
+43
to
+45
| let extraClassDeclaration = [{ | ||
| ::mlir::LogicalResult verify(); | ||
| }]; |
Member
There was a problem hiding this comment.
This is redundant. hasVerifier=1 causes this to generate
(same in other ops below)
| @@ -1,4 +1,4 @@ | |||
| //===-- Ops.cpp - Cast operation implementations ----------------*- C++ -*-===// | |||
| //===-- Ops.cpp - Cast ops verifiers -----------------------*- C++ -*-===// | |||
Member
There was a problem hiding this comment.
Why was this changed? It's incorrect now.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What this PR does
Adds an explicit Enum-like attribute OverflowSemanticsAttr to the Cast dialect with two choices: trunc and sat.
Requires the overflow attribute on all three cast ops: cast.tofelt, cast.toint, and cast.toindex.
Adds C++ verifiers so each cast op fails verification if the overflow attribute is missing or has an invalid value.
Adds a small MLIR test demonstrating usage.
Why
Makes overflow semantics for narrowing casts explicit in the IR (requested in issue #256).
Prevents ambiguous IR that omits overflow handling and surfaces errors early via op verification.
Lays the groundwork for later implementation of runtime/low-level truncation or saturating semantics.
Files changed (high level)
Added
include/llzk/Dialect/Cast/IR/Attrs.td — defines OverflowSemanticsAttr (enum: trunc, sat)
lib/Dialect/Cast/IR/Ops.cpp — C++ verifier implementations for the three ops
test/Cast/overflow-semantics.mlir — small MLIR snippets exercising the new attribute
Modified
include/llzk/Dialect/Cast/IR/Ops.td — require OverflowSemanticsAttr on tofelt/toint/toindex; declare per-op verify()
include/llzk/Dialect/Cast/IR/CMakeLists.txt — ensure Attrs.td is included in tablegen inputs