[Mlir-commits] [mlir] [mlir][arith] doc updates for ub semantics, and int representations (PR #72932)

llvmlistbot at llvm.org llvmlistbot at llvm.org
Mon Nov 20 17:01:50 PST 2023


llvmbot wrote:


<!--LLVM PR SUMMARY COMMENT-->

@llvm/pr-subscribers-mlir

Author: Jacob Yu (pingshiyu)

<details>
<summary>Changes</summary>

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

---
Full diff: https://github.com/llvm/llvm-project/pull/72932.diff


2 Files Affected:

- (modified) mlir/include/mlir/Dialect/Arith/IR/ArithBase.td (+5-1) 
- (modified) mlir/include/mlir/Dialect/Arith/IR/ArithOps.td (+48-27) 


``````````diff
diff --git a/mlir/include/mlir/Dialect/Arith/IR/ArithBase.td b/mlir/include/mlir/Dialect/Arith/IR/ArithBase.td
index 133af893e4efa74..240e49cfb13d73b 100644
--- a/mlir/include/mlir/Dialect/Arith/IR/ArithBase.td
+++ b/mlir/include/mlir/Dialect/Arith/IR/ArithBase.td
@@ -19,7 +19,11 @@ 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 unsigned integers are represented by bitvectors, and signed integers 
+    are represented by bitvectors with a two's complement representation. Unless 
+    otherwise stated, the operations within this dialect will propagate poison 
+    values (if any of its inputs are poison, then the output is poison). 
   }];
 
   let hasConstantMaterializer = 1;
diff --git a/mlir/include/mlir/Dialect/Arith/IR/ArithOps.td b/mlir/include/mlir/Dialect/Arith/IR/ArithOps.td
index 58e5385bf3ff268..836606d62554d89 100644
--- a/mlir/include/mlir/Dialect/Arith/IR/ArithOps.td
+++ b/mlir/include/mlir/Dialect/Arith/IR/ArithOps.td
@@ -198,7 +198,9 @@ def Arith_AddIOp : Arith_TotalIntBinaryOp<"addi", [Commutative]> {
     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.
+    has no standard attributes. If an overflow occurs, the result is the 
+    mathematical value of the addition modulo 2^n, where `n` is the width of
+    the integer type. 
 
     Example:
 
@@ -273,7 +275,11 @@ 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. If an overflow occurs, the result is the 
+    mathematical value of the addition modulo 2^n, where `n` is the width of
+    the integer type. 
+  }];
   let hasFolder = 1;
   let hasCanonicalizer = 1;
 }
@@ -283,7 +289,11 @@ def Arith_SubIOp : Arith_TotalIntBinaryOp<"subi"> {
 //===----------------------------------------------------------------------===//
 
 def Arith_MulIOp : Arith_TotalIntBinaryOp<"muli", [Commutative]> {
-  let summary = "integer multiplication operation";
+  let summary = [{
+    integer multiplication operation. If an overflow occurs, the result is the 
+    mathematical value of the addition modulo 2^n, where `n` is the width of
+    the integer type. 
+  }];
   let hasFolder = 1;
   let hasCanonicalizer = 1;
 }
@@ -420,8 +430,8 @@ 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 behaviour.
 
     Example:
 
@@ -457,8 +467,7 @@ def Arith_CeilDivUIOp : Arith_IntBinaryOp<"ceildivui",
     leading bit as the most significant, i.e. for `i16` given two's complement
     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 behaviour.
 
     Example:
 
@@ -486,8 +495,8 @@ 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 behaviour.
 
     Example:
 
@@ -514,8 +523,8 @@ 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 behaviour.
 
     Example:
 
@@ -538,8 +547,7 @@ 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 behaviour.
 
     Example:
 
@@ -567,8 +575,7 @@ 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 behaviour.
 
     Example:
 
@@ -680,8 +687,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 number of bits in the first operand, then the 
+    operation returns a poison.
 
     Example:
 
@@ -701,9 +711,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 number 
+    of bits in the first operand, then the operation returns poison.
 
     Example:
 
@@ -723,10 +735,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 the number of bits in the first operand, then the 
+    operation returns poison.
 
     Example:
 
@@ -1422,9 +1437,15 @@ 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 is `1`, then the second operand is returned, 
+    and the third operand is ignored, even if it were poison. 
+    
+    If the value of the first operand is `0`, then the third operand is returned, 
+    and the second operand is ignored, even if it were poison. 
+    
+    If the value of the first operand 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

``````````

</details>


https://github.com/llvm/llvm-project/pull/72932


More information about the Mlir-commits mailing list