[SMT] Add bitvector type, attribute, and constant operation (llvm#6804)

To clearly separate semantics, define a bit-vector type and attribute instead of reusing the built-in integer attribute. The built-in integer is usually encoded using two SMT bit-vectors to model poison and the regular bit values.

include/circt/Dialect/SMT/CMakeLists.txt

@@ -3,6 +3,12 @@ add_circt_doc(SMTOps Dialects/SMTOps -gen-op-doc)
 add_circt_doc(SMTTypes Dialects/SMTTypes -gen-typedef-doc -dialect smt)
 
 set(LLVM_TARGET_DEFINITIONS SMT.td)
+
+mlir_tablegen(SMTAttributes.h.inc -gen-attrdef-decls)
+mlir_tablegen(SMTAttributes.cpp.inc -gen-attrdef-defs)
+add_public_tablegen_target(CIRCTSMTAttrIncGen)
+add_dependencies(circt-headers CIRCTSMTAttrIncGen)
+
 mlir_tablegen(SMTEnums.h.inc -gen-enum-decls)
 mlir_tablegen(SMTEnums.cpp.inc -gen-enum-defs)
 add_public_tablegen_target(CIRCTSMTEnumsIncGen)

include/circt/Dialect/SMT/SMT.td

@@ -11,8 +11,10 @@
 
 include "mlir/IR/OpBase.td"
 
+include "circt/Dialect/SMT/SMTAttributes.td"
 include "circt/Dialect/SMT/SMTDialect.td"
 include "circt/Dialect/SMT/SMTTypes.td"
 include "circt/Dialect/SMT/SMTOps.td"
+include "circt/Dialect/SMT/SMTBitVectorOps.td"
 
 #endif // CIRCT_DIALECT_SMT_SMT_TD

include/circt/Dialect/SMT/SMTAttributes.h

@@ -0,0 +1,19 @@
+//===- SMTAttributes.h - Declare SMT dialect attributes ----------*- C++-*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef CIRCT_DIALECT_SMT_SMTATTRIBUTES_H
+#define CIRCT_DIALECT_SMT_SMTATTRIBUTES_H
+
+#include "mlir/IR/Attributes.h"
+#include "mlir/IR/BuiltinAttributeInterfaces.h"
+#include "mlir/IR/BuiltinAttributes.h"
+
+#define GET_ATTRDEF_CLASSES
+#include "circt/Dialect/SMT/SMTAttributes.h.inc"
+
+#endif // CIRCT_DIALECT_SMT_SMTATTRIBUTES_H

include/circt/Dialect/SMT/SMTAttributes.td

@@ -0,0 +1,64 @@
+//===- SMTAttributes.td - Attributes for SMT dialect -------*- tablegen -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// This file defines SMT dialect specific attributes.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef CIRCT_DIALECT_SMT_SMTATTRIBUTES_TD
+#define CIRCT_DIALECT_SMT_SMTATTRIBUTES_TD
+
+include "circt/Dialect/SMT/SMTDialect.td"
+include "mlir/IR/EnumAttr.td"
+include "mlir/IR/BuiltinAttributeInterfaces.td"
+
+def BitVectorAttr : AttrDef<SMTDialect, "BitVector", [
+  DeclareAttrInterfaceMethods<TypedAttrInterface>
+]> {
+  let mnemonic = "bv";
+  let description = [{
+    This attribute represents a constant value of the `(_ BitVec width)` sort as
+    described in the [SMT bit-vector
+    theory](https://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml).
+
+    The constant is as #bX (binary) or #xX (hexadecimal) in SMT-LIB
+    where X is the value in the corresponding format without any further
+    prefixing. Here, the bit-vector constant is given as a regular integer
+    literal and the associated bit-vector type indicating the bit-width.
+
+    Examples:
+    ```mlir
+    #smt.bv<5> : !smt.bv<4>
+    #smt.bv<92> : !smt.bv<8>
+    ```
+
+    The explicit type-suffix is mandatory to uniquely represent the attribute,
+    i.e., this attribute should always be used in the extended form (using the
+    `quantified` keyword in the operation assembly format string).
+
+    The bit-width must be greater than zero (i.e., at least one digit has to be
+    present).
+  }];
+
+  let parameters = (ins "llvm::APInt":$value);
+
+  let hasCustomAssemblyFormat = true;
+  let genVerifyDecl = true;
+
+  let builders = [
+    AttrBuilder<(ins "llvm::StringRef":$value)>,
+    AttrBuilder<(ins "unsigned":$value, "unsigned":$width)>,
+  ];
+
+  let extraClassDeclaration = [{
+    /// Return the bit-vector constant as a SMT-LIB formatted string.
+    std::string getValueAsString(bool prefix = true) const;
+  }];
+}
+
+#endif // CIRCT_DIALECT_SMT_SMTATTRIBUTES_TD

include/circt/Dialect/SMT/SMTBitVectorOps.td

@@ -0,0 +1,64 @@
+//===- SMTBitVectorOps.td - SMT bit-vector dialect ops -----*- tablegen -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef CIRCT_DIALECT_SMT_SMTBITVECTOROPS_TD
+#define CIRCT_DIALECT_SMT_SMTBITVECTOROPS_TD
+
+include "circt/Dialect/SMT/SMTDialect.td"
+include "circt/Dialect/SMT/SMTAttributes.td"
+include "circt/Dialect/SMT/SMTTypes.td"
+include "mlir/IR/EnumAttr.td"
+include "mlir/IR/OpAsmInterface.td"
+include "mlir/Interfaces/InferTypeOpInterface.td"
+include "mlir/Interfaces/SideEffectInterfaces.td"
+
+class SMTBVOp<string mnemonic, list<Trait> traits = []> :
+  Op<SMTDialect, "bv." # mnemonic, traits>;
+
+def BVConstantOp : SMTBVOp<"constant", [
+  Pure,
+  ConstantLike,
+  FirstAttrDerivedResultType,
+  DeclareOpInterfaceMethods<InferTypeOpInterface, ["inferReturnTypes"]>,
+  DeclareOpInterfaceMethods<OpAsmOpInterface, ["getAsmResultNames"]>
+]> {
+  let summary = "produce a constant bit-vector";
+  let description = [{
+    This operation produces an SSA value equal to the bit-vector constant
+    specified by the 'value' attribute.
+    Refer to the `BitVectorAttr` documentation for more information about
+    the semantics of bit-vector constants, their format, and associated sort.
+    The result type always matches the attribute's type.
+
+    Examples:
+    ```mlir
+    %c92_bv8 = smt.bv.constant #smt.bv<92> : !smt.bv<8>
+    %c5_bv4 = smt.bv.constant #smt.bv<5> : !smt.bv<4>
+    ```
+  }];
+
+  let arguments = (ins BitVectorAttr:$value);
+  let results = (outs BitVectorType:$result);
+
+  let assemblyFormat = "qualified($value) attr-dict";
+
+  let builders = [
+    OpBuilder<(ins "const llvm::APInt &":$value), [{
+      build($_builder, $_state,
+            BitVectorAttr::get($_builder.getContext(), value));
+    }]>,
+    OpBuilder<(ins "unsigned":$value, "unsigned":$width), [{
+      build($_builder, $_state,
+            BitVectorAttr::get($_builder.getContext(), value, width));
+    }]>,
+  ];
+
+  let hasFolder = true;
+}
+
+#endif // CIRCT_DIALECT_SMT_SMTBITVECTOROPS_TD

include/circt/Dialect/SMT/SMTDialect.td

@@ -16,9 +16,13 @@ def SMTDialect : Dialect {
   let summary = "a dialect that models satisfiability modulo theories";
   let cppNamespace = "circt::smt";
 
+  let useDefaultAttributePrinterParser = 1;
   let useDefaultTypePrinterParser = 1;
 
+  let hasConstantMaterializer = 1;
+
   let extraClassDeclaration = [{
+    void registerAttributes();
     void registerTypes();
   }];
 }

include/circt/Dialect/SMT/SMTOps.h

@@ -14,6 +14,7 @@
 #include "mlir/Interfaces/InferTypeOpInterface.h"
 #include "mlir/Interfaces/SideEffectInterfaces.h"
 
+#include "circt/Dialect/SMT/SMTAttributes.h"
 #include "circt/Dialect/SMT/SMTDialect.h"
 #include "circt/Dialect/SMT/SMTTypes.h"
 

include/circt/Dialect/SMT/SMTOps.td

@@ -10,6 +10,7 @@
 #define CIRCT_DIALECT_SMT_SMTOPS_TD
 
 include "circt/Dialect/SMT/SMTDialect.td"
+include "circt/Dialect/SMT/SMTAttributes.td"
 include "circt/Dialect/SMT/SMTTypes.td"
 include "mlir/IR/EnumAttr.td"
 include "mlir/IR/OpAsmInterface.td"
@@ -19,5 +20,4 @@ include "mlir/Interfaces/SideEffectInterfaces.td"
 class SMTOp<string mnemonic, list<Trait> traits = []> :
   Op<SMTDialect, mnemonic, traits>;
 
-
 #endif // CIRCT_DIALECT_SMT_SMTOPS_TD

include/circt/Dialect/SMT/SMTTypes.td

@@ -19,4 +19,20 @@ def BoolType : SMTTypeDef<"Bool"> {
   let assemblyFormat = "";
 }
 
+def BitVectorType : SMTTypeDef<"BitVector"> {
+  let mnemonic = "bv";
+  let description = [{
+    This type represents the `(_ BitVec width)` sort as described in the
+    [SMT bit-vector
+    theory](https://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml).
+
+    The bit-width must be strictly greater than zero.
+  }];
+
+  let parameters = (ins "unsigned":$width);
+  let assemblyFormat = "`<` $width `>`";
+
+  let genVerifyDecl = true;
+}
+
 #endif // CIRCT_DIALECT_SMT_SMTTYPES_TD

lib/Dialect/SMT/CMakeLists.txt

@@ -1,4 +1,5 @@
 add_circt_dialect_library(CIRCTSMT
+  SMTAttributes.cpp
   SMTDialect.cpp
   SMTOps.cpp
   SMTTypes.cpp
@@ -7,6 +8,7 @@ add_circt_dialect_library(CIRCTSMT
   ${CIRCT_MAIN_INCLUDE_DIR}/circt/Dialect/SMT
 
   DEPENDS
+  CIRCTSMTAttrIncGen
   CIRCTSMTEnumsIncGen
   MLIRSMTIncGen