[llvm-branch-commits] [mlir] 9a7f4bd - [mlir][arith] doc updates for ub semantics, and int representations (#72932)
via llvm-branch-commits
llvm-branch-commits at lists.llvm.org
Mon Nov 27 17:17:03 PST 2023
Author: Jacob Yu
Date: 2023-11-27T19:48:06-05:00
New Revision: 9a7f4bde2489f6529d336998e2c3fe902a1d864a
URL: https://github.com/llvm/llvm-project/commit/9a7f4bde2489f6529d336998e2c3fe902a1d864a
DIFF: https://github.com/llvm/llvm-project/commit/9a7f4bde2489f6529d336998e2c3fe902a1d864a.diff
LOG: [mlir][arith] doc updates for ub semantics, and int representations (#72932)
Following the discussions in this thread,
https://discourse.llvm.org/t/some-question-on-the-semantics-of-the-arith-dialect/74861,
here are some updates to the documented semantics of Arith.
Added are clarifications on poison behaviour, UBs, overflow semantics,
and the underlying two's complement representation used for integers
Co-authored-by: kuhar <jakubk at openxla.org>
Co-authored-by: math-fehr <mathieu.fehr at gmail.com>
Added:
Modified:
mlir/include/mlir/Dialect/Arith/IR/ArithBase.td
mlir/include/mlir/Dialect/Arith/IR/ArithOps.td
Removed:
################################################################################
diff --git a/mlir/include/mlir/Dialect/Arith/IR/ArithBase.td b/mlir/include/mlir/Dialect/Arith/IR/ArithBase.td
index 133af893e4efa74..1e4061392b22d48 100644
--- a/mlir/include/mlir/Dialect/Arith/IR/ArithBase.td
+++ b/mlir/include/mlir/Dialect/Arith/IR/ArithBase.td
@@ -19,7 +19,12 @@ def Arith_Dialect : Dialect {
The arith dialect is intended to hold basic integer and floating point
mathematical operations. This includes unary, binary, and ternary arithmetic
ops, bitwise and shift ops, cast ops, and compare ops. Operations in this
- dialect also accept vectors and tensors of integers or floats.
+ dialect also accept vectors and tensors of integers or floats. The dialect
+ assumes integers are represented by bitvectors with a two's complement
+ representation. Unless otherwise stated, the operations within this dialect
+ propagate poison values, i.e., if any of its inputs are poison, then the
+ output is poison. Unless otherwise stated, operations applied to `vector`
+ and `tensor` values propagates poison elementwise.
}];
let hasConstantMaterializer = 1;
diff --git a/mlir/include/mlir/Dialect/Arith/IR/ArithOps.td b/mlir/include/mlir/Dialect/Arith/IR/ArithOps.td
index e382f18340856ff..38cce99679e99dc 100644
--- a/mlir/include/mlir/Dialect/Arith/IR/ArithOps.td
+++ b/mlir/include/mlir/Dialect/Arith/IR/ArithOps.td
@@ -196,9 +196,9 @@ def Arith_AddIOp : Arith_TotalIntBinaryOp<"addi", [Commutative]> {
let summary = "integer addition operation";
let description = [{
The `addi` operation takes two operands and returns one result, each of
- these is required to be the same type. This type may be an integer scalar
- type, a vector whose element type is integer, or a tensor of integers. It
- has no standard attributes.
+ these is required to be the same type. This type may be an integer scalar type,
+ a vector whose element type is integer, or a tensor of integers. It has no
+ standard attributes.
Example:
@@ -273,7 +273,9 @@ def Arith_AddUIExtendedOp : Arith_Op<"addui_extended", [Pure, Commutative,
//===----------------------------------------------------------------------===//
def Arith_SubIOp : Arith_TotalIntBinaryOp<"subi"> {
- let summary = "integer subtraction operation";
+ let summary = [{
+ Integer subtraction operation.
+ }];
let hasFolder = 1;
let hasCanonicalizer = 1;
}
@@ -283,7 +285,9 @@ def Arith_SubIOp : Arith_TotalIntBinaryOp<"subi"> {
//===----------------------------------------------------------------------===//
def Arith_MulIOp : Arith_TotalIntBinaryOp<"muli", [Commutative]> {
- let summary = "integer multiplication operation";
+ let summary = [{
+ Integer multiplication operation.
+ }];
let hasFolder = 1;
let hasCanonicalizer = 1;
}
@@ -385,8 +389,9 @@ def Arith_DivUIOp : Arith_IntBinaryOp<"divui", [ConditionallySpeculatable]> {
the most significant, i.e. for `i16` given two's complement representation,
`6 / -2 = 6 / (2^16 - 2) = 0`.
- Note: the semantics of division by zero is TBD; do NOT assume any specific
- behavior.
+ Division by zero is undefined behavior. When applied to `vector` and
+ `tensor` values, the behavior is undefined if _any_ elements are divided by
+ zero.
Example:
@@ -420,8 +425,10 @@ def Arith_DivSIOp : Arith_IntBinaryOp<"divsi", [ConditionallySpeculatable]> {
Signed integer division. Rounds towards zero. Treats the leading bit as
sign, i.e. `6 / -2 = -3`.
- Note: the semantics of division by zero or signed division overflow (minimum
- value divided by -1) is TBD; do NOT assume any specific behavior.
+ Divison by zero, or signed division overflow (minimum value divided by -1)
+ is undefined behavior. When applied to `vector` and `tensor` values, the
+ behavior is undefined if _any_ of its elements are divided by zero or has a
+ signed division overflow.
Example:
@@ -455,10 +462,11 @@ def Arith_CeilDivUIOp : Arith_IntBinaryOp<"ceildivui",
let description = [{
Unsigned integer division. Rounds towards positive infinity. Treats the
leading bit as the most significant, i.e. for `i16` given two's complement
- representation, `6 / -2 = 6 / (2^16 - 2) = 1`.
+ representation, `6 / -2 = 6 / (2^16 - 2) = 1`.
- Note: the semantics of division by zero is TBD; do NOT assume any specific
- behavior.
+ Division by zero is undefined behavior. When applied to `vector` and
+ `tensor` values, the behavior is undefined if _any_ elements are divided by
+ zero.
Example:
@@ -486,8 +494,10 @@ def Arith_CeilDivSIOp : Arith_IntBinaryOp<"ceildivsi",
let description = [{
Signed integer division. Rounds towards positive infinity, i.e. `7 / -2 = -3`.
- Note: the semantics of division by zero or signed division overflow (minimum
- value divided by -1) is TBD; do NOT assume any specific behavior.
+ Divison by zero, or signed division overflow (minimum value divided by -1)
+ is undefined behavior. When applied to `vector` and `tensor` values, the
+ behavior is undefined if _any_ of its elements are divided by zero or has a
+ signed division overflow.
Example:
@@ -514,8 +524,10 @@ def Arith_FloorDivSIOp : Arith_TotalIntBinaryOp<"floordivsi"> {
let description = [{
Signed integer division. Rounds towards negative infinity, i.e. `5 / -2 = -3`.
- Note: the semantics of division by zero or signed division overflow (minimum
- value divided by -1) is TBD; do NOT assume any specific behavior.
+ Divison by zero, or signed division overflow (minimum value divided by -1)
+ is undefined behavior. When applied to `vector` and `tensor` values, the
+ behavior is undefined if _any_ of its elements are divided by zero or has a
+ signed division overflow.
Example:
@@ -538,8 +550,9 @@ def Arith_RemUIOp : Arith_TotalIntBinaryOp<"remui"> {
Unsigned integer division remainder. Treats the leading bit as the most
significant, i.e. for `i16`, `6 % -2 = 6 % (2^16 - 2) = 6`.
- Note: the semantics of division by zero is TBD; do NOT assume any specific
- behavior.
+ Division by zero is undefined behavior. When applied to `vector` and
+ `tensor` values, the behavior is undefined if _any_ elements are divided by
+ zero.
Example:
@@ -567,8 +580,9 @@ def Arith_RemSIOp : Arith_TotalIntBinaryOp<"remsi"> {
Signed integer division remainder. Treats the leading bit as sign, i.e. `6 %
-2 = 0`.
- Note: the semantics of division by zero is TBD; do NOT assume any specific
- behavior.
+ Division by zero is undefined behavior. When applied to `vector` and
+ `tensor` values, the behavior is undefined if _any_ elements are divided by
+ zero.
Example:
@@ -680,8 +694,11 @@ def Arith_XOrIOp : Arith_TotalIntBinaryOp<"xori", [Commutative]> {
def Arith_ShLIOp : Arith_TotalIntBinaryOp<"shli"> {
let summary = "integer left-shift";
let description = [{
- The `shli` operation shifts an integer value to the left by a variable
- amount. The low order bits are filled with zeros.
+ The `shli` operation shifts the integer value of the first operand to the left
+ by the integer value of the second operand. The second operand is interpreted as
+ unsigned. The low order bits are filled with zeros. If the value of the second
+ operand is greater than the bitwidth of the first operand, then the
+ operation returns poison.
Example:
@@ -701,9 +718,11 @@ def Arith_ShLIOp : Arith_TotalIntBinaryOp<"shli"> {
def Arith_ShRUIOp : Arith_TotalIntBinaryOp<"shrui"> {
let summary = "unsigned integer right-shift";
let description = [{
- The `shrui` operation shifts an integer value to the right by a variable
- amount. The integer is interpreted as unsigned. The high order bits are
- always filled with zeros.
+ The `shrui` operation shifts an integer value of the first operand to the right
+ by the value of the second operand. The first operand is interpreted as unsigned,
+ and the second operand is interpreted as unsigned. The high order bits are always
+ filled with zeros. If the value of the second operand is greater than the bitwidth
+ of the first operand, then the operation returns poison.
Example:
@@ -723,10 +742,13 @@ def Arith_ShRUIOp : Arith_TotalIntBinaryOp<"shrui"> {
def Arith_ShRSIOp : Arith_TotalIntBinaryOp<"shrsi"> {
let summary = "signed integer right-shift";
let description = [{
- The `shrsi` operation shifts an integer value to the right by a variable
- amount. The integer is interpreted as signed. The high order bits in the
- output are filled with copies of the most-significant bit of the shifted
- value (which means that the sign of the value is preserved).
+ The `shrsi` operation shifts an integer value of the first operand to the right
+ by the value of the second operand. The first operand is interpreted as signed,
+ and the second operand is interpreter as unsigned. The high order bits in the
+ output are filled with copies of the most-significant bit of the shifted value
+ (which means that the sign of the value is preserved). If the value of the second
+ operand is greater than bitwidth of the first operand, then the operation returns
+ poison.
Example:
@@ -1398,9 +1420,16 @@ def SelectOp : Arith_Op<"select", [Pure,
let summary = "select operation";
let description = [{
The `arith.select` operation chooses one value based on a binary condition
- supplied as its first operand. If the value of the first operand is `1`,
- the second operand is chosen, otherwise the third operand is chosen.
- The second and the third operand must have the same type.
+ supplied as its first operand.
+
+ If the value of the first operand (the condition) is `1`, then the second
+ operand is returned, and the third operand is ignored, even if it was poison.
+
+ If the value of the first operand (the condition) is `0`, then the third
+ operand is returned, and the second operand is ignored, even if it was poison.
+
+ If the value of the first operand (the condition) is poison, then the
+ operation returns poison.
The operation applies to vectors and tensors elementwise given the _shape_
of all operands is identical. The choice is made for each element
More information about the llvm-branch-commits
mailing list