1//===- ShapeBase.td ----------------------------------------*- tablegen -*-===//
2//
3// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4// See https://llvm.org/LICENSE.txt for license information.
5// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6//
7//===----------------------------------------------------------------------===//
8//
9// Base definitions for the `shape` dialect.
10//
11//===----------------------------------------------------------------------===//
12
13#ifndef SHAPE_BASE_TD
14#define SHAPE_BASE_TD
15
16include "mlir/IR/AttrTypeBase.td"
17include "mlir/IR/OpBase.td"
18
19//===----------------------------------------------------------------------===//
20// Shape Inference dialect definitions
21//===----------------------------------------------------------------------===//
22
23def ShapeDialect : Dialect {
24  let name = "shape";
25
26  let summary = "Types and operations for shape dialect";
27  let description = [{
28    This dialect contains operations for shape inference.
29
30    Note: Unless explicitly stated, all functions that return a shape and take
31    shapes as input, return the invalid shape if one of its operands is an
32    invalid shape. This avoids flagging multiple errors for one verification
33    failure. The dialect itself does not specify how errors should be combined
34    (there are multiple different options, from always choosing first operand,
35    concatting etc. on how to combine them).
36  }];
37
38  let cppNamespace = "::mlir::shape";
39  let dependentDialects = ["arith::ArithmeticDialect", "tensor::TensorDialect"];
40
41  let useDefaultTypePrinterParser = 1;
42  let hasConstantMaterializer = 1;
43  let hasOperationAttrVerify = 1;
44  let emitAccessorPrefix = kEmitAccessorPrefix_Prefixed;
45}
46
47class Shape_Type<string name, string typeMnemonic> : TypeDef<ShapeDialect, name> {
48  let mnemonic = typeMnemonic;
49}
50
51def Shape_ShapeType : Shape_Type<"Shape", "shape"> {
52  let description = [{
53    `shape.shape` represents either an unranked shape, a ranked shape with
54    possibly unknown dimensions or an invalid shape. The rank is of type
55    `shape.size` and, if rank is known, the extent is a 1D tensor of type
56    `shape.size`.
57
58    Shape is printed:
59    * `[*]` if it is an unranked shape
60    * `[?, 2]` if a rank 2 tensor with one unknown dimension
61    * `[3, 4]` is a rank 2 static tensor
62    * `[]` is a scalar
63    * `[1]` is a rank 1 tensor with 1 element
64    * `[invalid]` for an invalid shape
65  }];
66}
67
68def Shape_SizeType : Shape_Type<"Size", "size"> {
69  let description = [{
70    `shape.size` represents a non-negative integer with support for being
71    unknown and invalid.
72
73    Operations on `shape.size` types are specialized to handle unknown/dynamic
74    value. So, for example, `<unknown> + x == <unknown>` for all non-error `x :
75    !shape.size` (e.g., an unknown value does not become known due to addition).
76  }];
77}
78
79def Shape_ValueShapeType : Shape_Type<"ValueShape", "value_shape"> {
80  let description = [{
81    `shape.value_shape` represents the value produced by an operation (this
82    corresponds to `Value` in the compiler) and a shape. Conceptually this is a
83    tuple of a value (potentially unknown) and `shape.shape`. The value and
84    shape can either or both be unknown. If both the `value` and `shape` are
85    known, then the shape of `value` is conformant with `shape`. That is, the
86    shape of the value conforms to the shape of the ValueShape, so that if we
87    have ValueShape `(value, shape)` then `join(shape_of(value), shape)` would
88    be error free and in particular it means that if both are statically known,
89    then they are equal.
90  }];
91}
92
93def Shape_ExtentTensorType :
94    1DTensorOf<[Index]>,
95    BuildableType<"::mlir::RankedTensorType::get({ShapedType::kDynamicSize}, "
96                  "$_builder.getType<::mlir::IndexType>())"> {
97  let description = [{
98    The extent tensor is a tensor of rank one with arbitrarily many index
99    elements (tensor<?xindex>). Like `!shape.shape`, it is used to represent
100    shapes with the difference that it is guaranteed to be error-free.
101  }];
102}
103
104def Shape_ShapeOrSizeType : AnyTypeOf<[Shape_SizeType, Shape_ShapeType],
105  "shape or size">;
106
107def Shape_ShapeOrExtentTensorType : AnyTypeOf<[Shape_ShapeType,
108                                               Shape_ExtentTensorType],
109                                              "shape or extent tensor">;
110
111def Shape_SizeOrIndexType : AnyTypeOf<[Shape_SizeType, Index], "size or index">;
112
113def Shape_WitnessType : Shape_Type<"Witness", "witness"> {
114  let description = [{
115    A witness is a structural device in the compiler to maintain ordering of
116    code relying on information obtained from passing assertions. Witnesses do
117    not represent any physical data.
118
119    "cstr_" operations will return witnesses and be lowered into assertion logic
120    when not resolvable at compile time.
121
122    "assuming_" operations will take witnesses as input and represent only
123    information to the compiler, so they do not exist in executing code. Code
124    that is dependent on "assuming_" operations can assume all cstr operations
125    transitively before are honored as true.
126
127    These abstractions are intended to allow the compiler more freedom with
128    assertions by merely showing the assertion through dataflow at this time
129    rather than a side effecting operation that acts as a barrier. This can be
130    viewed similarly to a compiler representation of promises from asynchronous,
131    possibly crashing assertions. Reliant code will not be reordered to before
132    the code and non-reliant code can be reordered freely, and there are no
133    guarantees on the final ordering of the assertions or their related code.
134  }];
135}
136
137#endif // SHAPE_BASE_TD
138