diff --git a/include/circt/Conversion/Passes.td b/include/circt/Conversion/Passes.td index 2590595b33bf..6b30213cafbb 100644 --- a/include/circt/Conversion/Passes.td +++ b/include/circt/Conversion/Passes.td @@ -698,7 +698,7 @@ def ConvertCombToSMT : Pass<"convert-comb-to-smt"> { // Need to depend on HWDialect because some 'comb' canonicalization patterns // build 'hw.constant' operations. let dependentDialects = [ - "smt::SMTDialect", "hw::HWDialect", "mlir::func::FuncDialect" + "mlir::smt::SMTDialect", "hw::HWDialect", "mlir::func::FuncDialect" ]; } @@ -708,7 +708,7 @@ def ConvertCombToSMT : Pass<"convert-comb-to-smt"> { def ConvertHWToSMT : Pass<"convert-hw-to-smt", "mlir::ModuleOp"> { let summary = "Convert HW ops and constants to SMT ops"; - let dependentDialects = ["smt::SMTDialect", "mlir::func::FuncDialect"]; + let dependentDialects = ["mlir::smt::SMTDialect", "mlir::func::FuncDialect"]; } //===----------------------------------------------------------------------===// @@ -718,7 +718,7 @@ def ConvertHWToSMT : Pass<"convert-hw-to-smt", "mlir::ModuleOp"> { def ConvertVerifToSMT : Pass<"convert-verif-to-smt", "mlir::ModuleOp"> { let summary = "Convert Verif ops to SMT ops"; let dependentDialects = [ - "smt::SMTDialect", + "mlir::smt::SMTDialect", "mlir::arith::ArithDialect", "mlir::scf::SCFDialect", "mlir::func::FuncDialect" @@ -754,7 +754,7 @@ def LowerArcToLLVM : Pass<"lower-arc-to-llvm", "mlir::ModuleOp"> { def LowerSMTToZ3LLVM : Pass<"lower-smt-to-z3-llvm", "mlir::ModuleOp"> { let summary = "Lower the SMT dialect to LLVM IR calling the Z3 API"; let dependentDialects = [ - "smt::SMTDialect", "mlir::LLVM::LLVMDialect", "mlir::scf::SCFDialect", + "mlir::smt::SMTDialect", "mlir::LLVM::LLVMDialect", "mlir::scf::SCFDialect", "mlir::cf::ControlFlowDialect", "mlir::func::FuncDialect" ]; let options = [ diff --git a/include/circt/Dialect/CMakeLists.txt b/include/circt/Dialect/CMakeLists.txt index e5b55dcb068e..04982e306ada 100644 --- a/include/circt/Dialect/CMakeLists.txt +++ b/include/circt/Dialect/CMakeLists.txt @@ -34,7 +34,6 @@ if (CIRCT_INCLUDE_TESTS) endif() add_subdirectory(Seq) add_subdirectory(Sim) -add_subdirectory(SMT) add_subdirectory(SSP) add_subdirectory(SV) add_subdirectory(SystemC) diff --git a/include/circt/Dialect/SMT/CMakeLists.txt b/include/circt/Dialect/SMT/CMakeLists.txt deleted file mode 100644 index e914462fa7c8..000000000000 --- a/include/circt/Dialect/SMT/CMakeLists.txt +++ /dev/null @@ -1,15 +0,0 @@ -add_circt_dialect(SMT smt) -add_circt_doc(SMT Dialects/SMTOps -gen-op-doc) -add_circt_doc(SMT 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) -add_dependencies(circt-headers CIRCTSMTEnumsIncGen) diff --git a/include/circt/Dialect/SMT/SMT.td b/include/circt/Dialect/SMT/SMT.td deleted file mode 100644 index 05b87b9305e1..000000000000 --- a/include/circt/Dialect/SMT/SMT.td +++ /dev/null @@ -1,22 +0,0 @@ -//===- SMT.td - SMT dialect definition ---------------------*- 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_SMT_TD -#define CIRCT_DIALECT_SMT_SMT_TD - -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/SMTArrayOps.td" -include "circt/Dialect/SMT/SMTBitVectorOps.td" -include "circt/Dialect/SMT/SMTIntOps.td" - -#endif // CIRCT_DIALECT_SMT_SMT_TD diff --git a/include/circt/Dialect/SMT/SMTArrayOps.td b/include/circt/Dialect/SMT/SMTArrayOps.td deleted file mode 100644 index 81b46ce0109b..000000000000 --- a/include/circt/Dialect/SMT/SMTArrayOps.td +++ /dev/null @@ -1,99 +0,0 @@ -//===- SMTArrayOps.td - SMT array operations ---------------*- 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_SMTARRAYOPS_TD -#define CIRCT_DIALECT_SMT_SMTARRAYOPS_TD - -include "circt/Dialect/SMT/SMTDialect.td" -include "circt/Dialect/SMT/SMTAttributes.td" -include "circt/Dialect/SMT/SMTTypes.td" -include "mlir/Interfaces/SideEffectInterfaces.td" - -class SMTArrayOp traits = []> : - SMTOp<"array." # mnemonic, traits>; - -def ArrayStoreOp : SMTArrayOp<"store", [ - Pure, - TypesMatchWith<"summary", "array", "index", - "cast($_self).getDomainType()">, - TypesMatchWith<"summary", "array", "value", - "cast($_self).getRangeType()">, - AllTypesMatch<["array", "result"]>, -]> { - let summary = "stores a value at a given index and returns the new array"; - let description = [{ - This operation returns a new array which is the same as the 'array' operand - except that the value at the given 'index' is changed to the given 'value'. - The semantics are equivalent to the 'store' operator described in the - [SMT ArrayEx theory](https://smtlib.cs.uiowa.edu/Theories/ArraysEx.smt2) of - the SMT-LIB standard 2.6. - }]; - - let arguments = (ins ArrayType:$array, AnySMTType:$index, AnySMTType:$value); - let results = (outs ArrayType:$result); - - let assemblyFormat = [{ - $array `[` $index `]` `,` $value attr-dict `:` qualified(type($array)) - }]; -} - -def ArraySelectOp : SMTArrayOp<"select", [ - Pure, - TypesMatchWith<"summary", "array", "index", - "cast($_self).getDomainType()">, - TypesMatchWith<"summary", "array", "result", - "cast($_self).getRangeType()">, -]> { - let summary = "get the value stored in the array at the given index"; - let description = [{ - This operation is retuns the value stored in the given array at the given - index. The semantics are equivalent to the `select` operator defined in the - [SMT ArrayEx theory](https://smtlib.cs.uiowa.edu/Theories/ArraysEx.smt2) of - the SMT-LIB standard 2.6. - }]; - - let arguments = (ins ArrayType:$array, AnySMTType:$index); - let results = (outs AnySMTType:$result); - - let assemblyFormat = [{ - $array `[` $index `]` attr-dict `:` qualified(type($array)) - }]; -} - -def ArrayBroadcastOp : SMTArrayOp<"broadcast", [ - Pure, - TypesMatchWith<"summary", "result", "value", - "cast($_self).getRangeType()">, -]> { - let summary = "construct an array with the given value stored at every index"; - let description = [{ - This operation represents a broadcast of the 'value' operand to all indices - of the array. It is equivalent to - ``` - %0 = smt.declare_fun "array" : !smt.array<[!smt.int -> !smt.bool]> - %1 = smt.forall ["idx"] { - ^bb0(%idx: !smt.int): - %2 = smt.array.select %0[%idx] : !smt.array<[!smt.int -> !smt.bool]> - %3 = smt.eq %value, %2 : !smt.bool - smt.yield %3 : !smt.bool - } - smt.assert %1 - // return %0 - ``` - - In SMT-LIB, this is frequently written as - `((as const (Array Int Bool)) value)`. - }]; - - let arguments = (ins AnySMTType:$value); - let results = (outs ArrayType:$result); - - let assemblyFormat = "$value attr-dict `:` qualified(type($result))"; -} - -#endif // CIRCT_DIALECT_SMT_SMTARRAYOPS_TD diff --git a/include/circt/Dialect/SMT/SMTAttributes.h b/include/circt/Dialect/SMT/SMTAttributes.h deleted file mode 100644 index 9f21ba8d0b50..000000000000 --- a/include/circt/Dialect/SMT/SMTAttributes.h +++ /dev/null @@ -1,29 +0,0 @@ -//===- 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" - -namespace circt { -namespace smt { -namespace detail { - -struct BitVectorAttrStorage; - -} // namespace detail -} // namespace smt -} // namespace circt - -#define GET_ATTRDEF_CLASSES -#include "circt/Dialect/SMT/SMTAttributes.h.inc" - -#endif // CIRCT_DIALECT_SMT_SMTATTRIBUTES_H diff --git a/include/circt/Dialect/SMT/SMTAttributes.td b/include/circt/Dialect/SMT/SMTAttributes.td deleted file mode 100644 index 2356cc4f2da7..000000000000 --- a/include/circt/Dialect/SMT/SMTAttributes.td +++ /dev/null @@ -1,74 +0,0 @@ -//===- 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 -]> { - 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; - - // We need to manually define the storage class because the generated one is - // buggy (because the APInt asserts matching bitwidth in the `==` operator and - // the generated storage uses that directly. - // Alternatively: add a type parameter to redundantly store the bitwidth of - // of the attribute type, it it's in the order before the 'value' it will be - // checked before the APInt equality (this is the reason it works for the - // builtin integer attribute), but would be more fragile (and we'd store - // duplicate data). - let genStorageClass = false; - - let builders = [ - AttrBuilder<(ins "llvm::StringRef":$value)>, - AttrBuilder<(ins "uint64_t":$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 diff --git a/include/circt/Dialect/SMT/SMTBitVectorOps.td b/include/circt/Dialect/SMT/SMTBitVectorOps.td deleted file mode 100644 index 75e9fb85d869..000000000000 --- a/include/circt/Dialect/SMT/SMTBitVectorOps.td +++ /dev/null @@ -1,255 +0,0 @@ -//===- 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 traits = []> : - Op; - -def BVConstantOp : SMTBVOp<"constant", [ - Pure, - ConstantLike, - FirstAttrDerivedResultType, - DeclareOpInterfaceMethods, - DeclareOpInterfaceMethods -]> { - 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 "uint64_t":$value, "unsigned":$width), [{ - build($_builder, $_state, - BitVectorAttr::get($_builder.getContext(), value, width)); - }]>, - ]; - - let hasFolder = true; -} - -class BVArithmeticOrBitwiseOp : - SMTBVOp { - let summary = "equivalent to bv" # mnemonic # " in SMT-LIB"; - let description = "This operation performs " # desc # [{. The semantics are - equivalent to the `bv}] # mnemonic # [{` operator defined in the SMT-LIB 2.6 - standard. More precisely in the [theory of FixedSizeBitVectors](https://smtlib.cs.uiowa.edu/Theories/FixedSizeBitVectors.smt2) - and the [QF_BV logic](https://smtlib.cs.uiowa.edu/Logics/QF_BV.smt2) - describing closed quantifier-free formulas over the theory of fixed-size - bit-vectors. - }]; - - let results = (outs BitVectorType:$result); -} - -class BinaryBVOp : - BVArithmeticOrBitwiseOp { - let arguments = (ins BitVectorType:$lhs, BitVectorType:$rhs); - let assemblyFormat = "$lhs `,` $rhs attr-dict `:` qualified(type($result))"; -} - -class UnaryBVOp : - BVArithmeticOrBitwiseOp { - let arguments = (ins BitVectorType:$input); - let assemblyFormat = "$input attr-dict `:` qualified(type($result))"; -} - -def BVNotOp : UnaryBVOp<"not", "bitwise negation">; -def BVNegOp : UnaryBVOp<"neg", "two's complement unary minus">; - -def BVAndOp : BinaryBVOp<"and", "bitwise AND">; -def BVOrOp : BinaryBVOp<"or", "bitwise OR">; -def BVXOrOp : BinaryBVOp<"xor", "bitwise exclusive OR">; - -def BVAddOp : BinaryBVOp<"add", "addition">; -def BVMulOp : BinaryBVOp<"mul", "multiplication">; -def BVUDivOp : BinaryBVOp<"udiv", "unsigned division (rounded towards zero)">; -def BVSDivOp : BinaryBVOp<"sdiv", "two's complement signed division">; -def BVURemOp : BinaryBVOp<"urem", "unsigned remainder">; -def BVSRemOp : BinaryBVOp<"srem", - "two's complement signed remainder (sign follows dividend)">; -def BVSModOp : BinaryBVOp<"smod", - "two's complement signed remainder (sign follows divisor)">; -def BVShlOp : BinaryBVOp<"shl", "shift left">; -def BVLShrOp : BinaryBVOp<"lshr", "logical shift right">; -def BVAShrOp : BinaryBVOp<"ashr", "arithmetic shift right">; - -def PredicateSLT : I64EnumAttrCase<"slt", 0>; -def PredicateSLE : I64EnumAttrCase<"sle", 1>; -def PredicateSGT : I64EnumAttrCase<"sgt", 2>; -def PredicateSGE : I64EnumAttrCase<"sge", 3>; -def PredicateULT : I64EnumAttrCase<"ult", 4>; -def PredicateULE : I64EnumAttrCase<"ule", 5>; -def PredicateUGT : I64EnumAttrCase<"ugt", 6>; -def PredicateUGE : I64EnumAttrCase<"uge", 7>; -let cppNamespace = "circt::smt" in -def BVCmpPredicate : I64EnumAttr< - "BVCmpPredicate", - "smt bit-vector comparison predicate", - [PredicateSLT, PredicateSLE, PredicateSGT, PredicateSGE, - PredicateULT, PredicateULE, PredicateUGT, PredicateUGE]>; - -def BVCmpOp : SMTBVOp<"cmp", [Pure, SameTypeOperands]> { - let summary = "compare bit-vectors interpreted as signed or unsigned"; - let description = [{ - This operation compares bit-vector values, interpreting them as signed or - unsigned values depending on the predicate. The semantics are equivalent to - the `bvslt`, `bvsle`, `bvsgt`, `bvsge`, `bvult`, `bvule`, `bvugt`, or - `bvuge` operator defined in the SMT-LIB 2.6 standard depending on the - specified predicate. More precisely in the - [theory of FixedSizeBitVectors](https://smtlib.cs.uiowa.edu/Theories/FixedSizeBitVectors.smt2) - and the [QF_BV logic](https://smtlib.cs.uiowa.edu/Logics/QF_BV.smt2) - describing closed quantifier-free formulas over the theory of fixed-size - bit-vectors. - }]; - - let arguments = (ins BVCmpPredicate:$pred, - BitVectorType:$lhs, - BitVectorType:$rhs); - let results = (outs BoolType:$result); - - let assemblyFormat = [{ - $pred $lhs `,` $rhs attr-dict `:` qualified(type($lhs)) - }]; -} - -def ConcatOp : SMTBVOp<"concat", [ - Pure, - DeclareOpInterfaceMethods -]> { - let summary = "bit-vector concatenation"; - let description = [{ - This operation concatenates bit-vector values with semantics equivalent to - the `concat` operator defined in the SMT-LIB 2.6 standard. More precisely in - the [theory of FixedSizeBitVectors](https://smtlib.cs.uiowa.edu/Theories/FixedSizeBitVectors.smt2) - and the [QF_BV logic](https://smtlib.cs.uiowa.edu/Logics/QF_BV.smt2) - describing closed quantifier-free formulas over the theory of fixed-size - bit-vectors. - - Note that the following equivalences hold: - * `smt.bv.concat %a, %b : !smt.bv<4>, !smt.bv<4>` is equivalent to - `(concat a b)` in SMT-LIB - * `(= (concat #xf #x0) #xf0)` - }]; - - let arguments = (ins BitVectorType:$lhs, BitVectorType:$rhs); - let results = (outs BitVectorType:$result); - - let assemblyFormat = "$lhs `,` $rhs attr-dict `:` qualified(type(operands))"; -} - -def ExtractOp : SMTBVOp<"extract", [Pure]> { - let summary = "bit-vector extraction"; - let description = [{ - This operation extracts the range of bits starting at the 'lowBit' index - (inclusive) up to the 'lowBit' + result-width index (exclusive). The - semantics are equivalent to the `extract` operator defined in the SMT-LIB - 2.6 standard. More precisely in the - [theory of FixedSizeBitVectors](https://smtlib.cs.uiowa.edu/Theories/FixedSizeBitVectors.smt2) - and the [QF_BV logic](https://smtlib.cs.uiowa.edu/Logics/QF_BV.smt2) - describing closed quantifier-free formulas over the theory of fixed-size - bit-vectors. - - Note that `smt.bv.extract %bv from 2 : (!smt.bv<32>) -> !smt.bv<16>` is - equivalent to `((_ extract 17 2) bv)`, i.e., the SMT-LIB operator takes the - low and high indices where both are inclusive. The following equivalence - holds: `(= ((_ extract 3 0) #x0f) #xf)` - }]; - - let arguments = (ins I32Attr:$lowBit, BitVectorType:$input); - let results = (outs BitVectorType:$result); - - let assemblyFormat = [{ - $input `from` $lowBit attr-dict `:` functional-type($input, $result) - }]; - - let hasVerifier = true; -} - -def RepeatOp : SMTBVOp<"repeat", [Pure]> { - let summary = "repeated bit-vector concatenation of one value"; - let description = [{ - This operation is a shorthand for repeated concatenation of the same - bit-vector value, i.e., - ```mlir - smt.bv.repeat 5 times %a : !smt.bv<4> - // is the same as - %0 = smt.bv.repeat 4 times %a : !smt.bv<4> - smt.bv.concat %a, %0 : !smt.bv<4>, !smt.bv<16> - // or also - %0 = smt.bv.repeat 4 times %a : !smt.bv<4> - smt.bv.concat %0, %a : !smt.bv<16>, !smt.bv<4> - ``` - - The semantics are equivalent to the `repeat` operator defined in the SMT-LIB - 2.6 standard. More precisely in the - [theory of FixedSizeBitVectors](https://smtlib.cs.uiowa.edu/Theories/FixedSizeBitVectors.smt2) - and the [QF_BV logic](https://smtlib.cs.uiowa.edu/Logics/QF_BV.smt2) - describing closed quantifier-free formulas over the theory of fixed-size - bit-vectors. - }]; - - let arguments = (ins BitVectorType:$input); - let results = (outs BitVectorType:$result); - - let hasCustomAssemblyFormat = true; - let hasVerifier = true; - - let builders = [ - OpBuilder<(ins "unsigned":$count, "mlir::Value":$input)>, - ]; - - let extraClassDeclaration = [{ - /// Get the number of times the input operand is repeated. - unsigned getCount(); - }]; -} - -def BV2IntOp : SMTOp<"bv2int", [Pure]> { - let summary = "Convert an SMT bit-vector to an SMT integer."; - let description = [{ - Create an integer from the bit-vector argument `input`. If `is_signed` is - present, the bit-vector is treated as two's complement signed. Otherwise, - it is treated as an unsigned integer in the range [0..2^N-1], where N is - the number of bits in `input`. - }]; - let arguments = (ins BitVectorType:$input, UnitAttr:$is_signed); - let results = (outs IntType:$result); - let assemblyFormat = [{$input (`signed` $is_signed^)? attr-dict `:` - qualified(type($input))}]; -} - -#endif // CIRCT_DIALECT_SMT_SMTBITVECTOROPS_TD diff --git a/include/circt/Dialect/SMT/SMTDialect.h b/include/circt/Dialect/SMT/SMTDialect.h deleted file mode 100644 index 6a08234f96ba..000000000000 --- a/include/circt/Dialect/SMT/SMTDialect.h +++ /dev/null @@ -1,20 +0,0 @@ -//===- SMTDialect.h - SMT dialect definition --------------------*- 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_SMTDIALECT_H -#define CIRCT_DIALECT_SMT_SMTDIALECT_H - -#include "circt/Support/LLVM.h" -#include "mlir/IR/BuiltinOps.h" -#include "mlir/IR/Dialect.h" - -// Pull in the dialect definition. -#include "circt/Dialect/SMT/SMTDialect.h.inc" -#include "circt/Dialect/SMT/SMTEnums.h.inc" - -#endif // CIRCT_DIALECT_SMT_SMTDIALECT_H diff --git a/include/circt/Dialect/SMT/SMTDialect.td b/include/circt/Dialect/SMT/SMTDialect.td deleted file mode 100644 index 27de8dff4d71..000000000000 --- a/include/circt/Dialect/SMT/SMTDialect.td +++ /dev/null @@ -1,30 +0,0 @@ -//===- SMTDialect.td - SMT dialect definition --------------*- 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_SMTDIALECT_TD -#define CIRCT_DIALECT_SMT_SMTDIALECT_TD - -include "mlir/IR/DialectBase.td" - -def SMTDialect : Dialect { - let name = "smt"; - 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(); - }]; -} - -#endif // CIRCT_DIALECT_SMT_SMTDIALECT_TD diff --git a/include/circt/Dialect/SMT/SMTIntOps.td b/include/circt/Dialect/SMT/SMTIntOps.td deleted file mode 100644 index dd55a66b563b..000000000000 --- a/include/circt/Dialect/SMT/SMTIntOps.td +++ /dev/null @@ -1,137 +0,0 @@ -//===- SMTIntOps.td - SMT dialect int theory operations ----*- 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_SMTINTOPS_TD -#define CIRCT_DIALECT_SMT_SMTINTOPS_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/SideEffectInterfaces.td" - -class SMTIntOp traits = []> : - SMTOp<"int." # mnemonic, traits>; - -def IntConstantOp : SMTIntOp<"constant", [ - Pure, - ConstantLike, - DeclareOpInterfaceMethods, -]> { - let summary = "produce a constant (infinite-precision) integer"; - let description = [{ - This operation represents (infinite-precision) integer literals of the `Int` - sort. The set of values for the sort `Int` consists of all numerals and - all terms of the form `-n`where n is a numeral other than 0. For more - information refer to the - [SMT Ints theory](https://smtlib.cs.uiowa.edu/Theories/Ints.smt2) of the - SMT-LIB 2.6 standard. - }]; - - let arguments = (ins APIntAttr:$value); - let results = (outs IntType:$result); - - let hasCustomAssemblyFormat = true; - let hasFolder = true; -} - -class VariadicIntOp : SMTIntOp { - let description = [{ - This operation represents (infinite-precision) }] # summary # [{. - The semantics are equivalent to the corresponding operator described in - the [SMT Ints theory](https://smtlib.cs.uiowa.edu/Theories/Ints.smt2) of the - SMT-LIB 2.6 standard. - }]; - - let arguments = (ins Variadic:$inputs); - let results = (outs IntType:$result); - let assemblyFormat = "$inputs attr-dict"; - - let builders = [ - OpBuilder<(ins "mlir::ValueRange":$inputs), [{ - build($_builder, $_state, $_builder.getType(), inputs); - }]>, - ]; -} - -class BinaryIntOp : SMTIntOp { - let description = [{ - This operation represents (infinite-precision) }] # summary # [{. - The semantics are equivalent to the corresponding operator described in - the [SMT Ints theory](https://smtlib.cs.uiowa.edu/Theories/Ints.smt2) of the - SMT-LIB 2.6 standard. - }]; - - let arguments = (ins IntType:$lhs, IntType:$rhs); - let results = (outs IntType:$result); - let assemblyFormat = "$lhs `,` $rhs attr-dict"; -} - -def IntAbsOp : SMTIntOp<"abs", [Pure]> { - let summary = "the absolute value of an Int"; - let description = [{ - This operation represents the absolute value function for the `Int` sort. - The semantics are equivalent to the `abs` operator as described in the - [SMT Ints theory](https://smtlib.cs.uiowa.edu/Theories/Ints.smt2) of the - SMT-LIB 2.6 standard. - }]; - - let arguments = (ins IntType:$input); - let results = (outs IntType:$result); - let assemblyFormat = "$input attr-dict"; -} - -def IntAddOp : VariadicIntOp<"add"> { let summary = "integer addition"; } -def IntMulOp : VariadicIntOp<"mul"> { let summary = "integer multiplication"; } -def IntSubOp : BinaryIntOp<"sub"> { let summary = "integer subtraction"; } -def IntDivOp : BinaryIntOp<"div"> { let summary = "integer division"; } -def IntModOp : BinaryIntOp<"mod"> { let summary = "integer remainder"; } - -def IntPredicateLT : I64EnumAttrCase<"lt", 0>; -def IntPredicateLE : I64EnumAttrCase<"le", 1>; -def IntPredicateGT : I64EnumAttrCase<"gt", 2>; -def IntPredicateGE : I64EnumAttrCase<"ge", 3>; -let cppNamespace = "circt::smt" in -def IntPredicate : I64EnumAttr< - "IntPredicate", - "smt comparison predicate for integers", - [IntPredicateLT, IntPredicateLE, IntPredicateGT, IntPredicateGE]>; - -def IntCmpOp : SMTIntOp<"cmp", [Pure]> { - let summary = "integer comparison"; - let description = [{ - This operation represents the comparison of (infinite-precision) integers. - The semantics are equivalent to the `<= (le)`, `< (lt)`, `>= (ge)`, or - `> (gt)` operator depending on the predicate (indicated in parentheses) as - described in the - [SMT Ints theory](https://smtlib.cs.uiowa.edu/Theories/Ints.smt2) of the - SMT-LIB 2.6 standard. - }]; - - let arguments = (ins IntPredicate:$pred, IntType:$lhs, IntType:$rhs); - let results = (outs BoolType:$result); - let assemblyFormat = "$pred $lhs `,` $rhs attr-dict"; -} - -def Int2BVOp : SMTOp<"int2bv", [Pure]> { - let summary = "Convert an integer to an inferred-width bitvector."; - let description = [{ - Designed to lower directly to an operation of the same name in Z3. The Z3 - C API describes the semantics as follows: - Create an n bit bit-vector from the integer argument t1. - The resulting bit-vector has n bits, where the i'th bit (counting from 0 - to n-1) is 1 if (t1 div 2^i) mod 2 is 1. - The node t1 must have integer sort. - }]; - let arguments = (ins IntType:$input); - let results = (outs BitVectorType:$result); - let assemblyFormat = "$input attr-dict `:` qualified(type($result))"; -} - -#endif // CIRCT_DIALECT_SMT_SMTINTOPS_TD diff --git a/include/circt/Dialect/SMT/SMTOps.h b/include/circt/Dialect/SMT/SMTOps.h deleted file mode 100644 index e4fc4ac7a3f1..000000000000 --- a/include/circt/Dialect/SMT/SMTOps.h +++ /dev/null @@ -1,25 +0,0 @@ -//===- SMTOps.h - SMT dialect operations ------------------------*- 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_SMTOPS_H -#define CIRCT_DIALECT_SMT_SMTOPS_H - -#include "mlir/IR/OpImplementation.h" -#include "mlir/IR/SymbolTable.h" -#include "mlir/Interfaces/ControlFlowInterfaces.h" -#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" - -#define GET_OP_CLASSES -#include "circt/Dialect/SMT/SMT.h.inc" - -#endif // CIRCT_DIALECT_SMT_SMTOPS_H diff --git a/include/circt/Dialect/SMT/SMTOps.td b/include/circt/Dialect/SMT/SMTOps.td deleted file mode 100644 index 07a828a96338..000000000000 --- a/include/circt/Dialect/SMT/SMTOps.td +++ /dev/null @@ -1,477 +0,0 @@ -//===- SMTOps.td - SMT dialect operations ------------------*- 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_SMTOPS_TD -#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" -include "mlir/Interfaces/InferTypeOpInterface.td" -include "mlir/Interfaces/SideEffectInterfaces.td" -include "mlir/Interfaces/ControlFlowInterfaces.td" - -class SMTOp traits = []> : - Op; - -def DeclareFunOp : SMTOp<"declare_fun", [ - DeclareOpInterfaceMethods -]> { - let summary = "declare a symbolic value of a given sort"; - let description = [{ - This operation declares a symbolic value just as the `declare-const` and - `declare-func` statements in SMT-LIB 2.6. The result type determines the SMT - sort of the symbolic value. The returned value can then be used to refer to - the symbolic value instead of using the identifier like in SMT-LIB. - - The optionally provided string will be used as a prefix for the newly - generated identifier (useful for easier readability when exporting to - SMT-LIB). Each `declare` will always provide a unique new symbolic value - even if the identifier strings are the same. - - Note that there does not exist a separate operation equivalent to - SMT-LIBs `define-fun` since - ``` - (define-fun f (a Int) Int (-a)) - ``` - is only syntactic sugar for - ``` - %f = smt.declare_fun : !smt.func<(!smt.int) !smt.int> - %0 = smt.forall { - ^bb0(%arg0: !smt.int): - %1 = smt.apply_func %f(%arg0) : !smt.func<(!smt.int) !smt.int> - %2 = smt.int.neg %arg0 - %3 = smt.eq %1, %2 : !smt.int - smt.yield %3 : !smt.bool - } - smt.assert %0 - ``` - - Note that this operation cannot be marked as Pure since two operations (even - with the same identifier string) could then be CSEd, leading to incorrect - behavior. - }]; - - let arguments = (ins OptionalAttr:$namePrefix); - let results = (outs Res:$result); - - let assemblyFormat = [{ - ($namePrefix^)? attr-dict `:` qualified(type($result)) - }]; - - let builders = [ - OpBuilder<(ins "mlir::Type":$type), [{ - build($_builder, $_state, type, nullptr); - }]> - ]; -} - -def BoolConstantOp : SMTOp<"constant", [ - Pure, - ConstantLike, - DeclareOpInterfaceMethods, -]> { - let summary = "Produce a constant boolean"; - let description = [{ - Produces the constant expressions 'true' and 'false' as described in the - [Core theory](https://smtlib.cs.uiowa.edu/Theories/Core.smt2) of the SMT-LIB - Standard 2.6. - }]; - - let arguments = (ins BoolAttr:$value); - let results = (outs BoolType:$result); - let assemblyFormat = "$value attr-dict"; - - let hasFolder = true; -} - -def SolverOp : SMTOp<"solver", [ - IsolatedFromAbove, - SingleBlockImplicitTerminator<"smt::YieldOp">, -]> { - let summary = "create a solver instance within a lifespan"; - let description = [{ - This operation defines an SMT context with a solver instance. SMT operations - are only valid when being executed between the start and end of the region - of this operation. Any invocation outside is undefined. However, they do not - have to be direct children of this operation. For example, it is allowed to - have SMT operations in a `func.func` which is only called from within this - region. No SMT value may enter or exit the lifespan of this region (such - that no value created from another SMT context can be used in this scope and - the solver can deallocate all state required to keep track of SMT values at - the end). - - As a result, the region is comparable to an entire SMT-LIB script, but - allows for concrete operations and control-flow. Concrete values may be - passed in and returned to influence the computations after the `smt.solver` - operation. - - Example: - ```mlir - %0:2 = smt.solver (%in) {smt.some_attr} : (i8) -> (i8, i32) { - ^bb0(%arg0: i8): - %c = smt.declare_fun "c" : !smt.bool - smt.assert %c - %1 = smt.check sat { - %c1_i32 = arith.constant 1 : i32 - smt.yield %c1_i32 : i32 - } unknown { - %c0_i32 = arith.constant 0 : i32 - smt.yield %c0_i32 : i32 - } unsat { - %c-1_i32 = arith.constant -1 : i32 - smt.yield %c-1_i32 : i32 - } -> i32 - smt.yield %arg0, %1 : i8, i32 - } - ``` - - TODO: solver configuration attributes - }]; - - let arguments = (ins Variadic:$inputs); - let regions = (region SizedRegion<1>:$bodyRegion); - let results = (outs Variadic:$results); - - let assemblyFormat = [{ - `(` $inputs `)` attr-dict `:` functional-type($inputs, $results) $bodyRegion - }]; - - let hasRegionVerifier = true; -} - -def SetLogicOp : SMTOp<"set_logic", [ - HasParent<"smt::SolverOp">, -]> { - let summary = "set the logic for the SMT solver"; - let arguments = (ins StrAttr:$logic); - let assemblyFormat = "$logic attr-dict"; -} - -def AssertOp : SMTOp<"assert", []> { - let summary = "assert that a boolean expression holds"; - let arguments = (ins BoolType:$input); - let assemblyFormat = "$input attr-dict"; -} - -def ResetOp : SMTOp<"reset", []> { - let summary = "reset the solver"; - let assemblyFormat = "attr-dict"; -} - -def PushOp : SMTOp<"push", []> { - let summary = "push a given number of levels onto the assertion stack"; - let arguments = (ins ConfinedAttr:$count); - let assemblyFormat = "$count attr-dict"; -} - -def PopOp : SMTOp<"pop", []> { - let summary = "pop a given number of levels from the assertion stack"; - let arguments = (ins ConfinedAttr:$count); - let assemblyFormat = "$count attr-dict"; -} - -def CheckOp : SMTOp<"check", [ - NoRegionArguments, - SingleBlockImplicitTerminator<"smt::YieldOp">, -]> { - let summary = "check if the current set of assertions is satisfiable"; - let description = [{ - This operation checks if all the assertions in the solver defined by the - nearest ancestor operation of type `smt.solver` are consistent. The outcome - an be 'satisfiable', 'unknown', or 'unsatisfiable' and the corresponding - region will be executed. It is the corresponding construct to the - `check-sat` in SMT-LIB. - - Example: - ```mlir - %0 = smt.check sat { - %c1_i32 = arith.constant 1 : i32 - smt.yield %c1_i32 : i32 - } unknown { - %c0_i32 = arith.constant 0 : i32 - smt.yield %c0_i32 : i32 - } unsat { - %c-1_i32 = arith.constant -1 : i32 - smt.yield %c-1_i32 : i32 - } -> i32 - ``` - }]; - - let regions = (region SizedRegion<1>:$satRegion, - SizedRegion<1>:$unknownRegion, - SizedRegion<1>:$unsatRegion); - let results = (outs Variadic:$results); - - let assemblyFormat = [{ - attr-dict `sat` $satRegion `unknown` $unknownRegion `unsat` $unsatRegion - (`->` qualified(type($results))^ )? - }]; - - let hasRegionVerifier = true; -} - -def YieldOp : SMTOp<"yield", [ - Pure, - Terminator, - ReturnLike, - ParentOneOf<["smt::SolverOp", "smt::CheckOp", - "smt::ForallOp", "smt::ExistsOp"]>, -]> { - let summary = "terminator operation for various regions of SMT operations"; - let arguments = (ins Variadic:$values); - let assemblyFormat = "($values^ `:` qualified(type($values)))? attr-dict"; - let builders = [OpBuilder<(ins), [{ - build($_builder, $_state, std::nullopt); - }]>]; -} - -def ApplyFuncOp : SMTOp<"apply_func", [ - Pure, - TypesMatchWith<"summary", "func", "result", - "cast($_self).getRangeType()">, - RangedTypesMatchWith<"summary", "func", "args", - "cast($_self).getDomainTypes()"> -]> { - let summary = "apply a function"; - let description = [{ - This operation performs a function application as described in the - [SMT-LIB 2.6 standard](https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf). - It is part of the language itself rather than a theory or logic. - }]; - - let arguments = (ins SMTFuncType:$func, - Variadic:$args); - let results = (outs AnyNonFuncSMTType:$result); - - let assemblyFormat = [{ - $func `(` $args `)` attr-dict `:` qualified(type($func)) - }]; -} - -def EqOp : SMTOp<"eq", [Pure, SameTypeOperands]> { - let summary = "returns true iff all operands are identical"; - let description = [{ - This operation compares the operands and returns true iff all operands are - identical. The semantics are equivalent to the `=` operator defined in the - SMT-LIB Standard 2.6 in the - [Core theory](https://smtlib.cs.uiowa.edu/Theories/Core.smt2). - - Any SMT sort/type is allowed for the operands and it supports a variadic - number of operands, but requires at least two. This is because the `=` - operator is annotated with `:chainable` which means that `= a b c d` is - equivalent to `and (= a b) (= b c) (= c d)` where `and` is annotated - `:left-assoc`, i.e., it can be further rewritten to - `and (and (= a b) (= b c)) (= c d)`. - }]; - - let arguments = (ins Variadic:$inputs); - let results = (outs BoolType:$result); - - let builders = [ - OpBuilder<(ins "mlir::Value":$lhs, "mlir::Value":$rhs), [{ - build($_builder, $_state, ValueRange{lhs, rhs}); - }]> - ]; - - let hasCustomAssemblyFormat = true; - let hasVerifier = true; -} - -def DistinctOp : SMTOp<"distinct", [Pure, SameTypeOperands]> { - let summary = "returns true iff all operands are not identical to any other"; - let description = [{ - This operation compares the operands and returns true iff all operands are - not identical to any of the other operands. The semantics are equivalent to - the `distinct` operator defined in the SMT-LIB Standard 2.6 in the - [Core theory](https://smtlib.cs.uiowa.edu/Theories/Core.smt2). - - Any SMT sort/type is allowed for the operands and it supports a variadic - number of operands, but requires at least two. This is because the - `distinct` operator is annotated with `:pairwise` which means that - `distinct a b c d` is equivalent to - ``` - and (distinct a b) (distinct a c) (distinct a d) - (distinct b c) (distinct b d) - (distinct c d) - ``` - where `and` is annotated `:left-assoc`, i.e., it can be further rewritten to - ``` - (and (and (and (and (and (distinct a b) - (distinct a c)) - (distinct a d)) - (distinct b c)) - (distinct b d)) - (distinct c d) - ``` - }]; - - let arguments = (ins Variadic:$inputs); - let results = (outs BoolType:$result); - - let builders = [ - OpBuilder<(ins "mlir::Value":$lhs, "mlir::Value":$rhs), [{ - build($_builder, $_state, ValueRange{lhs, rhs}); - }]> - ]; - - let hasCustomAssemblyFormat = true; - let hasVerifier = true; -} - -def IteOp : SMTOp<"ite", [ - Pure, - AllTypesMatch<["thenValue", "elseValue", "result"]> -]> { - let summary = "an if-then-else function"; - let description = [{ - This operation returns its second operand or its third operand depending on - whether its first operand is true or not. The semantics are equivalent to - the `ite` operator defined in the - [Core theory](https://smtlib.cs.uiowa.edu/Theories/Core.smt2) of the SMT-LIB - 2.6 standard. - }]; - - let arguments = (ins BoolType:$cond, - AnySMTType:$thenValue, - AnySMTType:$elseValue); - let results = (outs AnySMTType:$result); - - let assemblyFormat = [{ - $cond `,` $thenValue `,` $elseValue attr-dict `:` qualified(type($result)) - }]; -} - -def NotOp : SMTOp<"not", [Pure]> { - let summary = "a boolean negation"; - let description = [{ - This operation performs a boolean negation. The semantics are equivalent to - the 'not' operator in the - [Core theory](https://smtlib.cs.uiowa.edu/Theories/Core.smt2) of the SMT-LIB - Standard 2.6. - }]; - - let arguments = (ins BoolType:$input); - let results = (outs BoolType:$result); - let assemblyFormat = "$input attr-dict"; -} - -class VariadicBoolOp : SMTOp { - let summary = desc; - let description = "This operation performs " # desc # [{. - The semantics are equivalent to the '}] # mnemonic # [{' operator in the - [Core theory](https://smtlib.cs.uiowa.edu/Theories/Core.smt2). - of the SMT-LIB Standard 2.6. - - It supports a variadic number of operands, but requires at least two. - This is because the operator is annotated with the `:left-assoc` attribute - which means that `op a b c` is equivalent to `(op (op a b) c)`. - }]; - - let arguments = (ins Variadic:$inputs); - let results = (outs BoolType:$result); - let assemblyFormat = "$inputs attr-dict"; - - let builders = [ - OpBuilder<(ins "mlir::Value":$lhs, "mlir::Value":$rhs), [{ - build($_builder, $_state, ValueRange{lhs, rhs}); - }]> - ]; -} - -def AndOp : VariadicBoolOp<"and", "a boolean conjunction">; -def OrOp : VariadicBoolOp<"or", "a boolean disjunction">; -def XOrOp : VariadicBoolOp<"xor", "a boolean exclusive OR">; - -def ImpliesOp : SMTOp<"implies", [Pure]> { - let summary = "boolean implication"; - let description = [{ - This operation performs a boolean implication. The semantics are equivalent - to the '=>' operator in the - [Core theory](https://smtlib.cs.uiowa.edu/Theories/Core.smt2) of the SMT-LIB - Standard 2.6. - }]; - - let arguments = (ins BoolType:$lhs, BoolType:$rhs); - let results = (outs BoolType:$result); - let assemblyFormat = "$lhs `,` $rhs attr-dict"; -} - -class QuantifierOp : SMTOp, -]> { - let description = [{ - This operation represents the }] # summary # [{ as described in the - [SMT-LIB 2.6 standard](https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf). - It is part of the language itself rather than a theory or logic. - - The operation specifies the name prefixes (as an optional attribute) and - types (as the types of the block arguments of the regions) of bound - variables that may be used in the 'body' of the operation. If a 'patterns' - region is specified, the block arguments must match the ones of the 'body' - region and (other than there) must be used at least once in the 'patterns' - region. It may also not contain any operations that bind variables, such as - quantifiers. While the 'body' region must always yield exactly one - `!smt.bool`-typed value, the 'patterns' region can yield an arbitrary number - (but at least one) of SMT values. - - The bound variables can be any SMT type except of functions, since SMT only - supports first-order logic. - - The 'no_patterns' attribute is only allowed when no 'patterns' region is - specified and forbids the solver to generate and use patterns for this - quantifier. - - The 'weight' attribute indicates the importance of this quantifier being - instantiated compared to other quantifiers that may be present. The default - value is zero. - - Both the 'no_patterns' and 'weight' attributes are annotations to the - quantifiers body term. Annotations and attributes are described in the - standard in sections 3.4, and 3.6 (specifically 3.6.5). SMT-LIB allows - adding custom attributes to provide solvers with additional metadata, e.g., - hints such as above mentioned attributes. They are not part of the standard - themselves, but supported by common SMT solvers (e.g., Z3). - }]; - - let arguments = (ins DefaultValuedAttr:$weight, - UnitAttr:$noPattern, - OptionalAttr:$boundVarNames); - let regions = (region SizedRegion<1>:$body, - VariadicRegion>:$patterns); - let results = (outs BoolType:$result); - - let builders = [ - OpBuilder<(ins - "TypeRange":$boundVarTypes, - "function_ref":$bodyBuilder, - CArg<"std::optional>", "std::nullopt">:$boundVarNames, - CArg<"function_ref", - "{}">:$patternBuilder, - CArg<"uint32_t", "0">:$weight, - CArg<"bool", "false">:$noPattern)> - ]; - let skipDefaultBuilders = true; - - let assemblyFormat = [{ - ($boundVarNames^)? (`no_pattern` $noPattern^)? (`weight` $weight^)? - attr-dict-with-keyword $body (`patterns` $patterns^)? - }]; - - let hasVerifier = true; - let hasRegionVerifier = true; -} - -def ForallOp : QuantifierOp<"forall"> { let summary = "forall quantifier"; } -def ExistsOp : QuantifierOp<"exists"> { let summary = "exists quantifier"; } - -#endif // CIRCT_DIALECT_SMT_SMTOPS_TD diff --git a/include/circt/Dialect/SMT/SMTTypes.h b/include/circt/Dialect/SMT/SMTTypes.h deleted file mode 100644 index 54502a41567e..000000000000 --- a/include/circt/Dialect/SMT/SMTTypes.h +++ /dev/null @@ -1,30 +0,0 @@ -//===- SMTTypes.h - SMT dialect types ---------------------------*- 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_SMTTYPES_H -#define CIRCT_DIALECT_SMT_SMTTYPES_H - -#include "mlir/IR/BuiltinTypes.h" -#include "mlir/IR/Types.h" - -#define GET_TYPEDEF_CLASSES -#include "circt/Dialect/SMT/SMTTypes.h.inc" - -namespace circt { -namespace smt { - -/// Returns whether the given type is an SMT value type. -bool isAnySMTValueType(mlir::Type type); - -/// Returns whether the given type is an SMT value type (excluding functions). -bool isAnyNonFuncSMTValueType(mlir::Type type); - -} // namespace smt -} // namespace circt - -#endif // CIRCT_DIALECT_SMT_SMTTYPES_H diff --git a/include/circt/Dialect/SMT/SMTTypes.td b/include/circt/Dialect/SMT/SMTTypes.td deleted file mode 100644 index 2aa82bf5d5e5..000000000000 --- a/include/circt/Dialect/SMT/SMTTypes.td +++ /dev/null @@ -1,145 +0,0 @@ -//===- SMTTypes.td - SMT dialect types ---------------------*- 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_SMTTYPES_TD -#define CIRCT_DIALECT_SMT_SMTTYPES_TD - -include "circt/Dialect/SMT/SMTDialect.td" -include "mlir/IR/AttrTypeBase.td" - -class SMTTypeDef : TypeDef { } - -def BoolType : SMTTypeDef<"Bool"> { - let mnemonic = "bool"; - let assemblyFormat = ""; -} - -def IntType : SMTTypeDef<"Int"> { - let mnemonic = "int"; - let description = [{ - This type represents the `Int` sort as described in the - [SMT Ints theory](https://smtlib.cs.uiowa.edu/Theories/Ints.smt2) of the - SMT-LIB 2.6 standard. - }]; - 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 "int64_t":$width); - let assemblyFormat = "`<` $width `>`"; - - let genVerifyDecl = true; -} - -def ArrayType : SMTTypeDef<"Array"> { - let mnemonic = "array"; - let description = [{ - This type represents the `(Array X Y)` sort, where X and Y are any - sort/type, as described in the - [SMT ArrayEx theory](https://smtlib.cs.uiowa.edu/Theories/ArraysEx.smt2) of - the SMT-LIB standard 2.6. - }]; - - let parameters = (ins "mlir::Type":$domainType, "mlir::Type":$rangeType); - let assemblyFormat = "`<` `[` $domainType `->` $rangeType `]` `>`"; - - let genVerifyDecl = true; -} - -def SMTFuncType : SMTTypeDef<"SMTFunc"> { - let mnemonic = "func"; - let description = [{ - This type represents the SMT function sort as described in the - [SMT-LIB 2.6 standard](https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf). - It is part of the language itself rather than a theory or logic. - - A function in SMT can have an arbitrary domain size, but always has exactly - one range sort. - - Since SMT only supports first-order logic, it is not possible to nest - function types. - - Example: `!smt.func<(!smt.bool, !smt.int) !smt.bool>` is equivalent to - `((Bool Int) Bool)` in SMT-LIB. - }]; - - let parameters = (ins - ArrayRefParameter<"mlir::Type", "domain types">:$domainTypes, - "mlir::Type":$rangeType - ); - - // Note: We are not printing the parentheses when no domain type is present - // because the default MLIR parser thinks it is a builtin function type - // otherwise. - let assemblyFormat = "`<` `(` $domainTypes `)` ` ` $rangeType `>`"; - - let builders = [ - TypeBuilderWithInferredContext<(ins - "llvm::ArrayRef":$domainTypes, - "mlir::Type":$rangeType), [{ - return $_get(rangeType.getContext(), domainTypes, rangeType); - }]>, - TypeBuilderWithInferredContext<(ins "mlir::Type":$rangeType), [{ - return $_get(rangeType.getContext(), - llvm::ArrayRef{}, rangeType); - }]> - ]; - - let genVerifyDecl = true; -} - -def SortType : SMTTypeDef<"Sort"> { - let mnemonic = "sort"; - let description = [{ - This type represents uninterpreted sorts. The usage of a type like - `!smt.sort<"sort_name"[!smt.bool, !smt.sort<"other_sort">]>` implies a - `declare-sort sort_name 2` and a `declare-sort other_sort 0` in SMT-LIB. - This type represents concrete use-sites of such declared sorts, in this - particular case it would be equivalent to `(sort_name Bool other_sort)` in - SMT-LIB. More details about the semantics can be found in the - [SMT-LIB 2.6 standard](https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf). - }]; - - let parameters = (ins - "mlir::StringAttr":$identifier, - OptionalArrayRefParameter<"mlir::Type", "sort parameters">:$sortParams - ); - - let assemblyFormat = "`<` $identifier (`[` $sortParams^ `]`)? `>`"; - - let builders = [ - TypeBuilder<(ins "llvm::StringRef":$identifier, - "llvm::ArrayRef":$sortParams), [{ - return $_get($_ctxt, mlir::StringAttr::get($_ctxt, identifier), - sortParams); - }]>, - TypeBuilder<(ins "llvm::StringRef":$identifier), [{ - return $_get($_ctxt, mlir::StringAttr::get($_ctxt, identifier), - llvm::ArrayRef{}); - }]>, - ]; - - let genVerifyDecl = true; -} - -def AnySMTType : Type, - "any SMT value type">; -def AnyNonFuncSMTType : Type, - "any non-function SMT value type">; -def AnyNonSMTType : Type, "any non-smt type">; - -#endif // CIRCT_DIALECT_SMT_SMTTYPES_TD diff --git a/include/circt/Dialect/SMT/SMTVisitors.h b/include/circt/Dialect/SMT/SMTVisitors.h deleted file mode 100644 index 56b3c4d7f3e4..000000000000 --- a/include/circt/Dialect/SMT/SMTVisitors.h +++ /dev/null @@ -1,201 +0,0 @@ -//===- SMTVisitors.h - SMT Dialect Visitors ---------------------*- 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 -// -//===----------------------------------------------------------------------===// -// -// This file defines visitors that make it easier to work with the SMT IR. -// -//===----------------------------------------------------------------------===// - -#ifndef CIRCT_DIALECT_SMT_SMTVISITORS_H -#define CIRCT_DIALECT_SMT_SMTVISITORS_H - -#include "circt/Dialect/SMT/SMTOps.h" -#include "llvm/ADT/TypeSwitch.h" - -namespace circt { -namespace smt { - -/// This helps visit SMT nodes. -template -class SMTOpVisitor { -public: - ResultType dispatchSMTOpVisitor(Operation *op, ExtraArgs... args) { - auto *thisCast = static_cast(this); - return TypeSwitch(op) - .template Case< - // Constants - BoolConstantOp, IntConstantOp, BVConstantOp, - // Bit-vector arithmetic - BVNegOp, BVAddOp, BVMulOp, BVURemOp, BVSRemOp, BVSModOp, BVShlOp, - BVLShrOp, BVAShrOp, BVUDivOp, BVSDivOp, - // Bit-vector bitwise - BVNotOp, BVAndOp, BVOrOp, BVXOrOp, - // Other bit-vector ops - ConcatOp, ExtractOp, RepeatOp, BVCmpOp, BV2IntOp, - // Int arithmetic - IntAddOp, IntMulOp, IntSubOp, IntDivOp, IntModOp, IntCmpOp, - Int2BVOp, - // Core Ops - EqOp, DistinctOp, IteOp, - // Variable/symbol declaration - DeclareFunOp, ApplyFuncOp, - // solver interaction - SolverOp, AssertOp, ResetOp, PushOp, PopOp, CheckOp, SetLogicOp, - // Boolean logic - NotOp, AndOp, OrOp, XOrOp, ImpliesOp, - // Arrays - ArrayStoreOp, ArraySelectOp, ArrayBroadcastOp, - // Quantifiers - ForallOp, ExistsOp, YieldOp>([&](auto expr) -> ResultType { - return thisCast->visitSMTOp(expr, args...); - }) - .Default([&](auto expr) -> ResultType { - return thisCast->visitInvalidSMTOp(op, args...); - }); - } - - /// This callback is invoked on any non-expression operations. - ResultType visitInvalidSMTOp(Operation *op, ExtraArgs... args) { - op->emitOpError("unknown SMT node"); - abort(); - } - - /// This callback is invoked on any SMT operations that are not - /// handled by the concrete visitor. - ResultType visitUnhandledSMTOp(Operation *op, ExtraArgs... args) { - return ResultType(); - } - -#define HANDLE(OPTYPE, OPKIND) \ - ResultType visitSMTOp(OPTYPE op, ExtraArgs... args) { \ - return static_cast(this)->visit##OPKIND##SMTOp(op, \ - args...); \ - } - - // Constants - HANDLE(BoolConstantOp, Unhandled); - HANDLE(IntConstantOp, Unhandled); - HANDLE(BVConstantOp, Unhandled); - - // Bit-vector arithmetic - HANDLE(BVNegOp, Unhandled); - HANDLE(BVAddOp, Unhandled); - HANDLE(BVMulOp, Unhandled); - HANDLE(BVURemOp, Unhandled); - HANDLE(BVSRemOp, Unhandled); - HANDLE(BVSModOp, Unhandled); - HANDLE(BVShlOp, Unhandled); - HANDLE(BVLShrOp, Unhandled); - HANDLE(BVAShrOp, Unhandled); - HANDLE(BVUDivOp, Unhandled); - HANDLE(BVSDivOp, Unhandled); - - // Bit-vector bitwise operations - HANDLE(BVNotOp, Unhandled); - HANDLE(BVAndOp, Unhandled); - HANDLE(BVOrOp, Unhandled); - HANDLE(BVXOrOp, Unhandled); - - // Other bit-vector operations - HANDLE(ConcatOp, Unhandled); - HANDLE(ExtractOp, Unhandled); - HANDLE(RepeatOp, Unhandled); - HANDLE(BVCmpOp, Unhandled); - HANDLE(BV2IntOp, Unhandled); - - // Int arithmetic - HANDLE(IntAddOp, Unhandled); - HANDLE(IntMulOp, Unhandled); - HANDLE(IntSubOp, Unhandled); - HANDLE(IntDivOp, Unhandled); - HANDLE(IntModOp, Unhandled); - - HANDLE(IntCmpOp, Unhandled); - HANDLE(Int2BVOp, Unhandled); - - HANDLE(EqOp, Unhandled); - HANDLE(DistinctOp, Unhandled); - HANDLE(IteOp, Unhandled); - - HANDLE(DeclareFunOp, Unhandled); - HANDLE(ApplyFuncOp, Unhandled); - - HANDLE(SolverOp, Unhandled); - HANDLE(AssertOp, Unhandled); - HANDLE(ResetOp, Unhandled); - HANDLE(PushOp, Unhandled); - HANDLE(PopOp, Unhandled); - HANDLE(CheckOp, Unhandled); - HANDLE(SetLogicOp, Unhandled); - - // Boolean logic operations - HANDLE(NotOp, Unhandled); - HANDLE(AndOp, Unhandled); - HANDLE(OrOp, Unhandled); - HANDLE(XOrOp, Unhandled); - HANDLE(ImpliesOp, Unhandled); - - // Array operations - HANDLE(ArrayStoreOp, Unhandled); - HANDLE(ArraySelectOp, Unhandled); - HANDLE(ArrayBroadcastOp, Unhandled); - - // Quantifier operations - HANDLE(ForallOp, Unhandled); - HANDLE(ExistsOp, Unhandled); - HANDLE(YieldOp, Unhandled); - -#undef HANDLE -}; - -/// This helps visit SMT types. -template -class SMTTypeVisitor { -public: - ResultType dispatchSMTTypeVisitor(Type type, ExtraArgs... args) { - auto *thisCast = static_cast(this); - return TypeSwitch(type) - .template Case([&](auto expr) -> ResultType { - return thisCast->visitSMTType(expr, args...); - }) - .Default([&](auto expr) -> ResultType { - return thisCast->visitInvalidSMTType(type, args...); - }); - } - - /// This callback is invoked on any non-expression types. - ResultType visitInvalidSMTType(Type type, ExtraArgs... args) { abort(); } - - /// This callback is invoked on any SMT type that are not - /// handled by the concrete visitor. - ResultType visitUnhandledSMTType(Type type, ExtraArgs... args) { - return ResultType(); - } - -#define HANDLE(TYPE, KIND) \ - ResultType visitSMTType(TYPE op, ExtraArgs... args) { \ - return static_cast(this)->visit##KIND##SMTType(op, \ - args...); \ - } - - HANDLE(BoolType, Unhandled); - HANDLE(IntegerType, Unhandled); - HANDLE(BitVectorType, Unhandled); - HANDLE(ArrayType, Unhandled); - HANDLE(SMTFuncType, Unhandled); - HANDLE(SortType, Unhandled); - -#undef HANDLE -}; - -} // namespace smt -} // namespace circt - -#endif // CIRCT_DIALECT_SMT_SMTVISITORS_H diff --git a/include/circt/InitAllDialects.h b/include/circt/InitAllDialects.h index 8e53c5fe211a..dc7a312bfb43 100644 --- a/include/circt/InitAllDialects.h +++ b/include/circt/InitAllDialects.h @@ -41,13 +41,13 @@ #ifdef CIRCT_INCLUDE_TESTS #include "circt/Dialect/RTGTest/IR/RTGTestDialect.h" #endif -#include "circt/Dialect/SMT/SMTDialect.h" #include "circt/Dialect/SSP/SSPDialect.h" #include "circt/Dialect/SV/SVDialect.h" #include "circt/Dialect/Seq/SeqDialect.h" #include "circt/Dialect/Sim/SimDialect.h" #include "circt/Dialect/SystemC/SystemCDialect.h" #include "circt/Dialect/Verif/VerifDialect.h" +#include "mlir/Dialect/SMT/IR/SMTDialect.h" #include "mlir/IR/Dialect.h" namespace circt { @@ -85,7 +85,7 @@ inline void registerAllDialects(mlir::DialectRegistry ®istry) { #endif seq::SeqDialect, sim::SimDialect, - smt::SMTDialect, + mlir::smt::SMTDialect, ssp::SSPDialect, sv::SVDialect, systemc::SystemCDialect, diff --git a/lib/Bindings/Python/dialects/SMTOps.td b/lib/Bindings/Python/dialects/SMTOps.td index 95ca9fc2e316..e143f071eb65 100644 --- a/lib/Bindings/Python/dialects/SMTOps.td +++ b/lib/Bindings/Python/dialects/SMTOps.td @@ -9,6 +9,6 @@ #ifndef BINDINGS_PYTHON_SMT_OPS #define BINDINGS_PYTHON_SMT_OPS -include "circt/Dialect/SMT/SMT.td" +include "mlir/Dialect/SMT/IR/SMT.td" #endif // BINDINGS_PYTHON_SMT_OPS diff --git a/lib/CAPI/Dialect/CMakeLists.txt b/lib/CAPI/Dialect/CMakeLists.txt index de22b72aecef..7e33d153635d 100644 --- a/lib/CAPI/Dialect/CMakeLists.txt +++ b/lib/CAPI/Dialect/CMakeLists.txt @@ -231,5 +231,5 @@ add_circt_public_c_api_library(CIRCTCAPISMT LINK_LIBS PUBLIC MLIRCAPIIR - CIRCTSMT + MLIRSMT ) diff --git a/lib/CAPI/Dialect/SMT.cpp b/lib/CAPI/Dialect/SMT.cpp index 12cc167fcba1..232622eadda1 100644 --- a/lib/CAPI/Dialect/SMT.cpp +++ b/lib/CAPI/Dialect/SMT.cpp @@ -7,19 +7,19 @@ //===----------------------------------------------------------------------===// #include "circt-c/Dialect/SMT.h" -#include "circt/Dialect/SMT/SMTDialect.h" -#include "circt/Dialect/SMT/SMTOps.h" +#include "mlir/Dialect/SMT/IR/SMTDialect.h" +#include "mlir/Dialect/SMT/IR/SMTOps.h" #include "mlir/CAPI/Registration.h" -using namespace circt; +using namespace mlir; using namespace smt; //===----------------------------------------------------------------------===// // Dialect API. //===----------------------------------------------------------------------===// -MLIR_DEFINE_CAPI_DIALECT_REGISTRATION(SMT, smt, circt::smt::SMTDialect) +MLIR_DEFINE_CAPI_DIALECT_REGISTRATION(SMT, smt, mlir::smt::SMTDialect) //===----------------------------------------------------------------------===// // Type API. diff --git a/lib/Conversion/CombToSMT/CMakeLists.txt b/lib/Conversion/CombToSMT/CMakeLists.txt index 327b1eb74e42..9feb916bd647 100644 --- a/lib/Conversion/CombToSMT/CMakeLists.txt +++ b/lib/Conversion/CombToSMT/CMakeLists.txt @@ -10,6 +10,6 @@ add_circt_conversion_library(CIRCTCombToSMT LINK_LIBS PUBLIC CIRCTComb CIRCTHWToSMT - CIRCTSMT + MLIRSMT MLIRTransforms ) diff --git a/lib/Conversion/CombToSMT/CombToSMT.cpp b/lib/Conversion/CombToSMT/CombToSMT.cpp index abb07fde6486..98a31eee86cf 100644 --- a/lib/Conversion/CombToSMT/CombToSMT.cpp +++ b/lib/Conversion/CombToSMT/CombToSMT.cpp @@ -9,8 +9,8 @@ #include "circt/Conversion/CombToSMT.h" #include "circt/Conversion/HWToSMT.h" #include "circt/Dialect/Comb/CombOps.h" -#include "circt/Dialect/SMT/SMTOps.h" #include "mlir/Dialect/Func/IR/FuncOps.h" +#include "mlir/Dialect/SMT/IR/SMTOps.h" #include "mlir/Pass/Pass.h" #include "mlir/Transforms/DialectConversion.h" @@ -19,6 +19,7 @@ namespace circt { #include "circt/Conversion/Passes.h.inc" } // namespace circt +using namespace mlir; using namespace circt; using namespace comb; @@ -253,7 +254,7 @@ struct VariadicToBinaryOpConversion : OpConversionPattern { namespace { struct ConvertCombToSMTPass - : public impl::ConvertCombToSMTBase { + : public circt::impl::ConvertCombToSMTBase { void runOnOperation() override; }; } // namespace diff --git a/lib/Conversion/HWToSMT/CMakeLists.txt b/lib/Conversion/HWToSMT/CMakeLists.txt index fdd114cf39f3..9aa139fc2653 100644 --- a/lib/Conversion/HWToSMT/CMakeLists.txt +++ b/lib/Conversion/HWToSMT/CMakeLists.txt @@ -9,9 +9,9 @@ add_circt_conversion_library(CIRCTHWToSMT LINK_LIBS PUBLIC CIRCTHW - CIRCTSMT CIRCTSeq MLIRFuncDialect + MLIRSMT MLIRTransforms MLIRTransformUtils ) diff --git a/lib/Conversion/HWToSMT/HWToSMT.cpp b/lib/Conversion/HWToSMT/HWToSMT.cpp index 1fde7865b4d6..816a9cbffe4d 100644 --- a/lib/Conversion/HWToSMT/HWToSMT.cpp +++ b/lib/Conversion/HWToSMT/HWToSMT.cpp @@ -8,10 +8,10 @@ #include "circt/Conversion/HWToSMT.h" #include "circt/Dialect/HW/HWOps.h" -#include "circt/Dialect/SMT/SMTOps.h" #include "circt/Dialect/Seq/SeqOps.h" #include "mlir/Analysis/TopologicalSortUtils.h" #include "mlir/Dialect/Func/IR/FuncOps.h" +#include "mlir/Dialect/SMT/IR/SMTOps.h" #include "mlir/Pass/Pass.h" #include "mlir/Transforms/DialectConversion.h" @@ -38,7 +38,8 @@ struct HWConstantOpConversion : OpConversionPattern { if (adaptor.getValue().getBitWidth() < 1) return rewriter.notifyMatchFailure(op.getLoc(), "0-bit constants not supported"); - rewriter.replaceOpWithNewOp(op, adaptor.getValue()); + rewriter.replaceOpWithNewOp(op, + adaptor.getValue()); return success(); } }; @@ -111,11 +112,11 @@ struct ArrayCreateOpConversion : OpConversionPattern { unsigned width = adaptor.getInputs().size(); - Value arr = rewriter.create(loc, arrTy); + Value arr = rewriter.create(loc, arrTy); for (auto [i, el] : llvm::enumerate(adaptor.getInputs())) { - Value idx = rewriter.create(loc, width - i - 1, - llvm::Log2_64_Ceil(width)); - arr = rewriter.create(loc, arr, idx, el); + Value idx = rewriter.create( + loc, width - i - 1, llvm::Log2_64_Ceil(width)); + arr = rewriter.create(loc, arr, idx, el); } rewriter.replaceOp(op, arr); @@ -139,14 +140,16 @@ struct ArrayGetOpConversion : OpConversionPattern { return rewriter.notifyMatchFailure(op.getLoc(), "unsupported array element type"); - Value oobVal = rewriter.create(loc, type); - Value numElementsVal = rewriter.create( + Value oobVal = rewriter.create(loc, type); + Value numElementsVal = rewriter.create( loc, numElements - 1, llvm::Log2_64_Ceil(numElements)); - Value inBounds = rewriter.create( - loc, smt::BVCmpPredicate::ule, adaptor.getIndex(), numElementsVal); - Value indexed = rewriter.create(loc, adaptor.getInput(), - adaptor.getIndex()); - rewriter.replaceOpWithNewOp(op, inBounds, indexed, oobVal); + Value inBounds = + rewriter.create(loc, mlir::smt::BVCmpPredicate::ule, + adaptor.getIndex(), numElementsVal); + Value indexed = rewriter.create( + loc, adaptor.getInput(), adaptor.getIndex()); + rewriter.replaceOpWithNewOp(op, inBounds, indexed, + oobVal); return success(); } }; @@ -189,18 +192,18 @@ void circt::populateHWToSMTTypeConverter(TypeConverter &converter) { converter.addConversion([](IntegerType type) -> std::optional { if (type.getWidth() <= 0) return std::nullopt; - return smt::BitVectorType::get(type.getContext(), type.getWidth()); + return mlir::smt::BitVectorType::get(type.getContext(), type.getWidth()); }); converter.addConversion([](seq::ClockType type) -> std::optional { - return smt::BitVectorType::get(type.getContext(), 1); + return mlir::smt::BitVectorType::get(type.getContext(), 1); }); converter.addConversion([&](ArrayType type) -> std::optional { auto rangeType = converter.convertType(type.getElementType()); if (!rangeType) return {}; - auto domainType = smt::BitVectorType::get( + auto domainType = mlir::smt::BitVectorType::get( type.getContext(), llvm::Log2_64_Ceil(type.getNumElements())); - return smt::ArrayType::get(type.getContext(), domainType, rangeType); + return mlir::smt::ArrayType::get(type.getContext(), domainType, rangeType); }); // Default target materialization to convert from illegal types to legal @@ -215,25 +218,27 @@ void circt::populateHWToSMTTypeConverter(TypeConverter &converter) { // Convert a 'smt.bool'-typed value to a 'smt.bv'-typed value converter.addTargetMaterialization( - [&](OpBuilder &builder, smt::BitVectorType resultType, ValueRange inputs, - Location loc) -> Value { + [&](OpBuilder &builder, mlir::smt::BitVectorType resultType, + ValueRange inputs, Location loc) -> Value { if (inputs.size() != 1) return Value(); - if (!isa(inputs[0].getType())) + if (!isa(inputs[0].getType())) return Value(); unsigned width = resultType.getWidth(); - Value constZero = builder.create(loc, 0, width); - Value constOne = builder.create(loc, 1, width); - return builder.create(loc, inputs[0], constOne, constZero); + Value constZero = + builder.create(loc, 0, width); + Value constOne = builder.create(loc, 1, width); + return builder.create(loc, inputs[0], constOne, + constZero); }); // Convert an unrealized conversion cast from 'smt.bool' to i1 // into a direct conversion from 'smt.bool' to 'smt.bv<1>'. converter.addTargetMaterialization( - [&](OpBuilder &builder, smt::BitVectorType resultType, ValueRange inputs, - Location loc) -> Value { + [&](OpBuilder &builder, mlir::smt::BitVectorType resultType, + ValueRange inputs, Location loc) -> Value { if (inputs.size() != 1 || resultType.getWidth() != 1) return Value(); @@ -246,28 +251,28 @@ void circt::populateHWToSMTTypeConverter(TypeConverter &converter) { if (!castOp || castOp.getInputs().size() != 1) return Value(); - if (!isa(castOp.getInputs()[0].getType())) + if (!isa(castOp.getInputs()[0].getType())) return Value(); - Value constZero = builder.create(loc, 0, 1); - Value constOne = builder.create(loc, 1, 1); - return builder.create(loc, castOp.getInputs()[0], constOne, - constZero); + Value constZero = builder.create(loc, 0, 1); + Value constOne = builder.create(loc, 1, 1); + return builder.create(loc, castOp.getInputs()[0], + constOne, constZero); }); // Convert a 'smt.bv<1>'-typed value to a 'smt.bool'-typed value converter.addTargetMaterialization( - [&](OpBuilder &builder, smt::BoolType resultType, ValueRange inputs, + [&](OpBuilder &builder, mlir::smt::BoolType resultType, ValueRange inputs, Location loc) -> Value { if (inputs.size() != 1) return Value(); - auto bvType = dyn_cast(inputs[0].getType()); + auto bvType = dyn_cast(inputs[0].getType()); if (!bvType || bvType.getWidth() != 1) return Value(); - Value constOne = builder.create(loc, 1, 1); - return builder.create(loc, inputs[0], constOne); + Value constOne = builder.create(loc, 1, 1); + return builder.create(loc, inputs[0], constOne); }); // Default source materialization to convert from illegal types to legal @@ -294,7 +299,7 @@ void ConvertHWToSMTPass::runOnOperation() { target.addIllegalDialect(); target.addIllegalOp(); target.addIllegalOp(); - target.addLegalDialect(); + target.addLegalDialect(); target.addLegalDialect(); RewritePatternSet patterns(&getContext()); diff --git a/lib/Conversion/SMTToZ3LLVM/CMakeLists.txt b/lib/Conversion/SMTToZ3LLVM/CMakeLists.txt index 61ca420380bd..c907a59887e7 100644 --- a/lib/Conversion/SMTToZ3LLVM/CMakeLists.txt +++ b/lib/Conversion/SMTToZ3LLVM/CMakeLists.txt @@ -8,12 +8,12 @@ add_circt_conversion_library(CIRCTSMTToZ3LLVM Core LINK_LIBS PUBLIC - CIRCTSMT CIRCTSupport MLIRLLVMCommonConversion MLIRSCFToControlFlow MLIRControlFlowToLLVM MLIRArithToLLVM MLIRFuncToLLVM + MLIRSMT MLIRTransforms ) diff --git a/lib/Conversion/SMTToZ3LLVM/LowerSMTToZ3LLVM.cpp b/lib/Conversion/SMTToZ3LLVM/LowerSMTToZ3LLVM.cpp index 62031e00c498..1f611c3743ce 100644 --- a/lib/Conversion/SMTToZ3LLVM/LowerSMTToZ3LLVM.cpp +++ b/lib/Conversion/SMTToZ3LLVM/LowerSMTToZ3LLVM.cpp @@ -7,7 +7,6 @@ //===----------------------------------------------------------------------===// #include "circt/Conversion/SMTToZ3LLVM.h" -#include "circt/Dialect/SMT/SMTOps.h" #include "circt/Support/Namespace.h" #include "mlir/Conversion/ArithToLLVM/ArithToLLVM.h" #include "mlir/Conversion/ControlFlowToLLVM/ControlFlowToLLVM.h" @@ -21,6 +20,7 @@ #include "mlir/Dialect/LLVMIR/LLVMAttrs.h" #include "mlir/Dialect/LLVMIR/LLVMDialect.h" #include "mlir/Dialect/SCF/IR/SCF.h" +#include "mlir/Dialect/SMT/IR/SMTOps.h" #include "mlir/IR/BuiltinDialect.h" #include "mlir/Pass/Pass.h" #include "mlir/Transforms/DialectConversion.h" diff --git a/lib/Conversion/VerifToSMT/CMakeLists.txt b/lib/Conversion/VerifToSMT/CMakeLists.txt index 135c906ff0ad..4d923bc70261 100644 --- a/lib/Conversion/VerifToSMT/CMakeLists.txt +++ b/lib/Conversion/VerifToSMT/CMakeLists.txt @@ -10,11 +10,11 @@ add_circt_conversion_library(CIRCTVerifToSMT LINK_LIBS PUBLIC CIRCTHW CIRCTHWToSMT - CIRCTSMT CIRCTVerif MLIRArithDialect MLIRFuncDialect MLIRSCFDialect + MLIRSMT MLIRTransforms MLIRTransformUtils MLIRReconcileUnrealizedCasts diff --git a/lib/Conversion/VerifToSMT/VerifToSMT.cpp b/lib/Conversion/VerifToSMT/VerifToSMT.cpp index 50b911b23f18..c21dd9862d44 100644 --- a/lib/Conversion/VerifToSMT/VerifToSMT.cpp +++ b/lib/Conversion/VerifToSMT/VerifToSMT.cpp @@ -8,8 +8,6 @@ #include "circt/Conversion/VerifToSMT.h" #include "circt/Conversion/HWToSMT.h" -#include "circt/Dialect/SMT/SMTOps.h" -#include "circt/Dialect/SMT/SMTTypes.h" #include "circt/Dialect/Seq/SeqTypes.h" #include "circt/Dialect/Verif/VerifOps.h" #include "circt/Support/Namespace.h" @@ -17,6 +15,8 @@ #include "mlir/Dialect/Arith/IR/Arith.h" #include "mlir/Dialect/Func/IR/FuncOps.h" #include "mlir/Dialect/SCF/IR/SCF.h" +#include "mlir/Dialect/SMT/IR/SMTOps.h" +#include "mlir/Dialect/SMT/IR/SMTTypes.h" #include "mlir/IR/ValueRange.h" #include "mlir/Pass/Pass.h" #include "mlir/Transforms/DialectConversion.h" diff --git a/lib/Dialect/CMakeLists.txt b/lib/Dialect/CMakeLists.txt index a7bf7be67e1f..51c20d557b54 100644 --- a/lib/Dialect/CMakeLists.txt +++ b/lib/Dialect/CMakeLists.txt @@ -37,7 +37,6 @@ if (CIRCT_INCLUDE_TESTS) endif() add_subdirectory(Seq) add_subdirectory(Sim) -add_subdirectory(SMT) add_subdirectory(SSP) add_subdirectory(SV) add_subdirectory(SystemC) diff --git a/lib/Dialect/SMT/CMakeLists.txt b/lib/Dialect/SMT/CMakeLists.txt deleted file mode 100644 index 1a5beb1f8d02..000000000000 --- a/lib/Dialect/SMT/CMakeLists.txt +++ /dev/null @@ -1,27 +0,0 @@ -add_circt_dialect_library(CIRCTSMT - SMTAttributes.cpp - SMTDialect.cpp - SMTOps.cpp - SMTTypes.cpp - - ADDITIONAL_HEADER_DIRS - ${CIRCT_MAIN_INCLUDE_DIR}/circt/Dialect/SMT - - DEPENDS - CIRCTSMTAttrIncGen - CIRCTSMTEnumsIncGen - MLIRSMTIncGen - - LINK_COMPONENTS - Support - - LINK_LIBS PUBLIC - MLIRIR - MLIRInferTypeOpInterface - MLIRSideEffectInterfaces - MLIRControlFlowInterfaces -) - -add_dependencies(circt-headers - MLIRSMTIncGen -) diff --git a/lib/Dialect/SMT/SMTAttributes.cpp b/lib/Dialect/SMT/SMTAttributes.cpp deleted file mode 100644 index 7616b33816f7..000000000000 --- a/lib/Dialect/SMT/SMTAttributes.cpp +++ /dev/null @@ -1,201 +0,0 @@ -//===- SMTAttributes.cpp - Implement SMT attributes -----------------------===// -// -// 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 -// -//===----------------------------------------------------------------------===// - -#include "circt/Dialect/SMT/SMTAttributes.h" -#include "circt/Dialect/SMT/SMTDialect.h" -#include "circt/Dialect/SMT/SMTTypes.h" -#include "mlir/IR/Builders.h" -#include "mlir/IR/DialectImplementation.h" -#include "llvm/ADT/TypeSwitch.h" -#include "llvm/Support/Format.h" - -using namespace circt; -using namespace circt::smt; - -//===----------------------------------------------------------------------===// -// BitVectorAttr -//===----------------------------------------------------------------------===// - -namespace circt { -namespace smt { -namespace detail { -struct BitVectorAttrStorage : public mlir::AttributeStorage { - using KeyTy = APInt; - BitVectorAttrStorage(APInt value) : value(std::move(value)) {} - - KeyTy getAsKey() const { return value; } - - // NOTE: the implementation of this operator is the reason we need to define - // the storage manually. The auto-generated version would just do the direct - // equality check of the APInt, but that asserts the bitwidth of both to be - // the same, leading to a crash. This implementation, therefore, checks for - // matching bit-width beforehand. - bool operator==(const KeyTy &key) const { - return (value.getBitWidth() == key.getBitWidth() && value == key); - } - - static llvm::hash_code hashKey(const KeyTy &key) { - return llvm::hash_value(key); - } - - static BitVectorAttrStorage * - construct(mlir::AttributeStorageAllocator &allocator, KeyTy &&key) { - return new (allocator.allocate()) - BitVectorAttrStorage(std::move(key)); - } - - APInt value; -}; -} // namespace detail -} // namespace smt -} // namespace circt - -APInt BitVectorAttr::getValue() const { return getImpl()->value; } - -LogicalResult BitVectorAttr::verify( - function_ref emitError, - APInt value) { // NOLINT(performance-unnecessary-value-param) - if (value.getBitWidth() < 1) - return emitError() << "bit-width must be at least 1, but got " - << value.getBitWidth(); - return success(); -} - -std::string BitVectorAttr::getValueAsString(bool prefix) const { - unsigned width = getValue().getBitWidth(); - SmallVector toPrint; - StringRef pref = prefix ? "#" : ""; - if (width % 4 == 0) { - getValue().toString(toPrint, 16, false, false, false); - // APInt's 'toString' omits leading zeros. However, those are critical here - // because they determine the bit-width of the bit-vector. - SmallVector leadingZeros(width / 4 - toPrint.size(), '0'); - return (pref + "x" + Twine(leadingZeros) + toPrint).str(); - } - - getValue().toString(toPrint, 2, false, false, false); - // APInt's 'toString' omits leading zeros - SmallVector leadingZeros(width - toPrint.size(), '0'); - return (pref + "b" + Twine(leadingZeros) + toPrint).str(); -} - -/// Parse an SMT-LIB formatted bit-vector string. -static FailureOr -parseBitVectorString(function_ref emitError, - StringRef value) { - if (value[0] != '#') - return emitError() << "expected '#'"; - - if (value.size() < 3) - return emitError() << "expected at least one digit"; - - if (value[1] == 'b') - return APInt(value.size() - 2, std::string(value.begin() + 2, value.end()), - 2); - - if (value[1] == 'x') - return APInt((value.size() - 2) * 4, - std::string(value.begin() + 2, value.end()), 16); - - return emitError() << "expected either 'b' or 'x'"; -} - -BitVectorAttr BitVectorAttr::get(MLIRContext *context, StringRef value) { - auto maybeValue = parseBitVectorString(nullptr, value); - - assert(succeeded(maybeValue) && "string must have SMT-LIB format"); - return Base::get(context, *maybeValue); -} - -BitVectorAttr -BitVectorAttr::getChecked(function_ref emitError, - MLIRContext *context, StringRef value) { - auto maybeValue = parseBitVectorString(emitError, value); - if (failed(maybeValue)) - return {}; - - return Base::getChecked(emitError, context, *maybeValue); -} - -BitVectorAttr BitVectorAttr::get(MLIRContext *context, uint64_t value, - unsigned width) { - return Base::get(context, APInt(width, value)); -} - -BitVectorAttr -BitVectorAttr::getChecked(function_ref emitError, - MLIRContext *context, uint64_t value, - unsigned width) { - if (width < 64 && value >= (UINT64_C(1) << width)) { - emitError() << "value does not fit in a bit-vector of desired width"; - return {}; - } - return Base::getChecked(emitError, context, APInt(width, value)); -} - -Attribute BitVectorAttr::parse(AsmParser &odsParser, Type odsType) { - llvm::SMLoc loc = odsParser.getCurrentLocation(); - - APInt val; - if (odsParser.parseLess() || odsParser.parseInteger(val) || - odsParser.parseGreater()) - return {}; - - // Requires the use of `quantified()` in operation assembly formats. - if (!odsType || !llvm::isa(odsType)) { - odsParser.emitError(loc) << "explicit bit-vector type required"; - return {}; - } - - unsigned width = llvm::cast(odsType).getWidth(); - - if (width > val.getBitWidth()) { - // sext is always safe here, even for unsigned values, because the - // parseOptionalInteger method will return something with a zero in the - // top bits if it is a positive number. - val = val.sext(width); - } else if (width < val.getBitWidth()) { - // The parser can return an unnecessarily wide result. - // This isn't a problem, but truncating off bits is bad. - unsigned neededBits = - val.isNegative() ? val.getSignificantBits() : val.getActiveBits(); - if (width < neededBits) { - odsParser.emitError(loc) - << "integer value out of range for given bit-vector type " << odsType; - return {}; - } - val = val.trunc(width); - } - - return BitVectorAttr::get(odsParser.getContext(), val); -} - -void BitVectorAttr::print(AsmPrinter &odsPrinter) const { - // This printer only works for the extended format where the MLIR - // infrastructure prints the type for us. This means, the attribute should - // never be used without `quantified` in an assembly format. - odsPrinter << "<" << getValue() << ">"; -} - -Type BitVectorAttr::getType() const { - return BitVectorType::get(getContext(), getValue().getBitWidth()); -} - -//===----------------------------------------------------------------------===// -// ODS Boilerplate -//===----------------------------------------------------------------------===// - -#define GET_ATTRDEF_CLASSES -#include "circt/Dialect/SMT/SMTAttributes.cpp.inc" - -void SMTDialect::registerAttributes() { - addAttributes< -#define GET_ATTRDEF_LIST -#include "circt/Dialect/SMT/SMTAttributes.cpp.inc" - >(); -} diff --git a/lib/Dialect/SMT/SMTDialect.cpp b/lib/Dialect/SMT/SMTDialect.cpp deleted file mode 100644 index 22ad37a3cdce..000000000000 --- a/lib/Dialect/SMT/SMTDialect.cpp +++ /dev/null @@ -1,47 +0,0 @@ -//===- SMTDialect.cpp - SMT dialect implementation ------------------------===// -// -// 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 -// -//===----------------------------------------------------------------------===// - -#include "circt/Dialect/SMT/SMTDialect.h" -#include "circt/Dialect/SMT/SMTAttributes.h" -#include "circt/Dialect/SMT/SMTOps.h" -#include "circt/Dialect/SMT/SMTTypes.h" - -using namespace circt; -using namespace smt; - -void SMTDialect::initialize() { - registerAttributes(); - registerTypes(); - addOperations< -#define GET_OP_LIST -#include "circt/Dialect/SMT/SMT.cpp.inc" - >(); -} - -Operation *SMTDialect::materializeConstant(OpBuilder &builder, Attribute value, - Type type, Location loc) { - // BitVectorType constants can materialize into smt.bv.constant - if (auto bvType = dyn_cast(type)) { - if (auto attrValue = dyn_cast(value)) { - assert(bvType == attrValue.getType() && - "attribute and desired result types have to match"); - return builder.create(loc, attrValue); - } - } - - // BoolType constants can materialize into smt.constant - if (auto boolType = dyn_cast(type)) { - if (auto attrValue = dyn_cast(value)) - return builder.create(loc, attrValue); - } - - return nullptr; -} - -#include "circt/Dialect/SMT/SMTDialect.cpp.inc" -#include "circt/Dialect/SMT/SMTEnums.cpp.inc" diff --git a/lib/Dialect/SMT/SMTOps.cpp b/lib/Dialect/SMT/SMTOps.cpp deleted file mode 100644 index ad60501d97f2..000000000000 --- a/lib/Dialect/SMT/SMTOps.cpp +++ /dev/null @@ -1,472 +0,0 @@ -//===- SMTOps.cpp ---------------------------------------------------------===// -// -// 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 -// -//===----------------------------------------------------------------------===// - -#include "circt/Dialect/SMT/SMTOps.h" -#include "mlir/IR/Builders.h" -#include "mlir/IR/OpImplementation.h" -#include "llvm/ADT/APSInt.h" - -using namespace circt; -using namespace smt; -using namespace mlir; - -//===----------------------------------------------------------------------===// -// BVConstantOp -//===----------------------------------------------------------------------===// - -LogicalResult BVConstantOp::inferReturnTypes( - mlir::MLIRContext *context, std::optional location, - ::mlir::ValueRange operands, ::mlir::DictionaryAttr attributes, - ::mlir::OpaqueProperties properties, ::mlir::RegionRange regions, - ::llvm::SmallVectorImpl<::mlir::Type> &inferredReturnTypes) { - inferredReturnTypes.push_back( - properties.as()->getValue().getType()); - return success(); -} - -void BVConstantOp::getAsmResultNames( - function_ref setNameFn) { - SmallVector specialNameBuffer; - llvm::raw_svector_ostream specialName(specialNameBuffer); - specialName << "c" << getValue().getValue() << "_bv" - << getValue().getValue().getBitWidth(); - setNameFn(getResult(), specialName.str()); -} - -OpFoldResult BVConstantOp::fold(FoldAdaptor adaptor) { - assert(adaptor.getOperands().empty() && "constant has no operands"); - return getValueAttr(); -} - -//===----------------------------------------------------------------------===// -// DeclareFunOp -//===----------------------------------------------------------------------===// - -void DeclareFunOp::getAsmResultNames( - function_ref setNameFn) { - setNameFn(getResult(), getNamePrefix().has_value() ? *getNamePrefix() : ""); -} - -//===----------------------------------------------------------------------===// -// SolverOp -//===----------------------------------------------------------------------===// - -LogicalResult SolverOp::verifyRegions() { - if (getBody()->getTerminator()->getOperands().getTypes() != getResultTypes()) - return emitOpError() << "types of yielded values must match return values"; - if (getBody()->getArgumentTypes() != getInputs().getTypes()) - return emitOpError() - << "block argument types must match the types of the 'inputs'"; - - return success(); -} - -//===----------------------------------------------------------------------===// -// CheckOp -//===----------------------------------------------------------------------===// - -LogicalResult CheckOp::verifyRegions() { - if (getSatRegion().front().getTerminator()->getOperands().getTypes() != - getResultTypes()) - return emitOpError() << "types of yielded values in 'sat' region must " - "match return values"; - if (getUnknownRegion().front().getTerminator()->getOperands().getTypes() != - getResultTypes()) - return emitOpError() << "types of yielded values in 'unknown' region must " - "match return values"; - if (getUnsatRegion().front().getTerminator()->getOperands().getTypes() != - getResultTypes()) - return emitOpError() << "types of yielded values in 'unsat' region must " - "match return values"; - - return success(); -} - -//===----------------------------------------------------------------------===// -// EqOp -//===----------------------------------------------------------------------===// - -static LogicalResult -parseSameOperandTypeVariadicToBoolOp(OpAsmParser &parser, - OperationState &result) { - SmallVector inputs; - SMLoc loc = parser.getCurrentLocation(); - Type type; - - if (parser.parseOperandList(inputs) || - parser.parseOptionalAttrDict(result.attributes) || parser.parseColon() || - parser.parseType(type)) - return failure(); - - result.addTypes(BoolType::get(parser.getContext())); - if (parser.resolveOperands(inputs, SmallVector(inputs.size(), type), - loc, result.operands)) - return failure(); - - return success(); -} - -ParseResult EqOp::parse(OpAsmParser &parser, OperationState &result) { - return parseSameOperandTypeVariadicToBoolOp(parser, result); -} - -void EqOp::print(OpAsmPrinter &printer) { - printer << ' ' << getInputs(); - printer.printOptionalAttrDict(getOperation()->getAttrs()); - printer << " : " << getInputs().front().getType(); -} - -LogicalResult EqOp::verify() { - if (getInputs().size() < 2) - return emitOpError() << "'inputs' must have at least size 2, but got " - << getInputs().size(); - - return success(); -} - -//===----------------------------------------------------------------------===// -// DistinctOp -//===----------------------------------------------------------------------===// - -ParseResult DistinctOp::parse(OpAsmParser &parser, OperationState &result) { - return parseSameOperandTypeVariadicToBoolOp(parser, result); -} - -void DistinctOp::print(OpAsmPrinter &printer) { - printer << ' ' << getInputs(); - printer.printOptionalAttrDict(getOperation()->getAttrs()); - printer << " : " << getInputs().front().getType(); -} - -LogicalResult DistinctOp::verify() { - if (getInputs().size() < 2) - return emitOpError() << "'inputs' must have at least size 2, but got " - << getInputs().size(); - - return success(); -} - -//===----------------------------------------------------------------------===// -// ExtractOp -//===----------------------------------------------------------------------===// - -LogicalResult ExtractOp::verify() { - unsigned rangeWidth = getType().getWidth(); - unsigned inputWidth = cast(getInput().getType()).getWidth(); - if (getLowBit() + rangeWidth > inputWidth) - return emitOpError("range to be extracted is too big, expected range " - "starting at index ") - << getLowBit() << " of length " << rangeWidth - << " requires input width of at least " << (getLowBit() + rangeWidth) - << ", but the input width is only " << inputWidth; - return success(); -} - -//===----------------------------------------------------------------------===// -// ConcatOp -//===----------------------------------------------------------------------===// - -LogicalResult ConcatOp::inferReturnTypes( - MLIRContext *context, std::optional location, ValueRange operands, - DictionaryAttr attributes, OpaqueProperties properties, RegionRange regions, - SmallVectorImpl &inferredReturnTypes) { - inferredReturnTypes.push_back(BitVectorType::get( - context, cast(operands[0].getType()).getWidth() + - cast(operands[1].getType()).getWidth())); - return success(); -} - -//===----------------------------------------------------------------------===// -// RepeatOp -//===----------------------------------------------------------------------===// - -LogicalResult RepeatOp::verify() { - unsigned inputWidth = cast(getInput().getType()).getWidth(); - unsigned resultWidth = getType().getWidth(); - if (resultWidth % inputWidth != 0) - return emitOpError() << "result bit-vector width must be a multiple of the " - "input bit-vector width"; - - return success(); -} - -unsigned RepeatOp::getCount() { - unsigned inputWidth = cast(getInput().getType()).getWidth(); - unsigned resultWidth = getType().getWidth(); - return resultWidth / inputWidth; -} - -void RepeatOp::build(OpBuilder &builder, OperationState &state, unsigned count, - Value input) { - unsigned inputWidth = cast(input.getType()).getWidth(); - Type resultTy = BitVectorType::get(builder.getContext(), inputWidth * count); - build(builder, state, resultTy, input); -} - -ParseResult RepeatOp::parse(OpAsmParser &parser, OperationState &result) { - OpAsmParser::UnresolvedOperand input; - Type inputType; - llvm::SMLoc countLoc = parser.getCurrentLocation(); - - APInt count; - if (parser.parseInteger(count) || parser.parseKeyword("times")) - return failure(); - - if (count.isNonPositive()) - return parser.emitError(countLoc) << "integer must be positive"; - - llvm::SMLoc inputLoc = parser.getCurrentLocation(); - if (parser.parseOperand(input) || - parser.parseOptionalAttrDict(result.attributes) || parser.parseColon() || - parser.parseType(inputType)) - return failure(); - - if (parser.resolveOperand(input, inputType, result.operands)) - return failure(); - - auto bvInputTy = dyn_cast(inputType); - if (!bvInputTy) - return parser.emitError(inputLoc) << "input must have bit-vector type"; - - // Make sure no assertions can trigger and no silent overflows can happen - // Bit-width is stored as 'int64_t' parameter in 'BitVectorType' - const unsigned maxBw = 63; - if (count.getActiveBits() > maxBw) - return parser.emitError(countLoc) - << "integer must fit into " << maxBw << " bits"; - - // Store multiplication in an APInt twice the size to not have any overflow - // and check if it can be truncated to 'maxBw' bits without cutting of - // important bits. - APInt resultBw = bvInputTy.getWidth() * count.zext(2 * maxBw); - if (resultBw.getActiveBits() > maxBw) - return parser.emitError(countLoc) - << "result bit-width (provided integer times bit-width of the input " - "type) must fit into " - << maxBw << " bits"; - - Type resultTy = - BitVectorType::get(parser.getContext(), resultBw.getZExtValue()); - result.addTypes(resultTy); - return success(); -} - -void RepeatOp::print(OpAsmPrinter &printer) { - printer << " " << getCount() << " times " << getInput(); - printer.printOptionalAttrDict((*this)->getAttrs()); - printer << " : " << getInput().getType(); -} - -//===----------------------------------------------------------------------===// -// BoolConstantOp -//===----------------------------------------------------------------------===// - -void BoolConstantOp::getAsmResultNames( - function_ref setNameFn) { - setNameFn(getResult(), getValue() ? "true" : "false"); -} - -OpFoldResult BoolConstantOp::fold(FoldAdaptor adaptor) { - assert(adaptor.getOperands().empty() && "constant has no operands"); - return getValueAttr(); -} - -//===----------------------------------------------------------------------===// -// IntConstantOp -//===----------------------------------------------------------------------===// - -void IntConstantOp::getAsmResultNames( - function_ref setNameFn) { - SmallVector specialNameBuffer; - llvm::raw_svector_ostream specialName(specialNameBuffer); - specialName << "c" << getValue(); - setNameFn(getResult(), specialName.str()); -} - -OpFoldResult IntConstantOp::fold(FoldAdaptor adaptor) { - assert(adaptor.getOperands().empty() && "constant has no operands"); - return getValueAttr(); -} - -void IntConstantOp::print(OpAsmPrinter &p) { - p << " " << getValue(); - p.printOptionalAttrDict((*this)->getAttrs(), /*elidedAttrs=*/{"value"}); -} - -ParseResult IntConstantOp::parse(OpAsmParser &parser, OperationState &result) { - APInt value; - if (parser.parseInteger(value)) - return failure(); - - result.getOrAddProperties().setValue( - IntegerAttr::get(parser.getContext(), APSInt(value))); - - if (parser.parseOptionalAttrDict(result.attributes)) - return failure(); - - result.addTypes(smt::IntType::get(parser.getContext())); - return success(); -} - -//===----------------------------------------------------------------------===// -// ForallOp -//===----------------------------------------------------------------------===// - -template -static LogicalResult verifyQuantifierRegions(QuantifierOp op) { - if (op.getBoundVarNames() && - op.getBody().getNumArguments() != op.getBoundVarNames()->size()) - return op.emitOpError( - "number of bound variable names must match number of block arguments"); - if (!llvm::all_of(op.getBody().getArgumentTypes(), isAnyNonFuncSMTValueType)) - return op.emitOpError() - << "bound variables must by any non-function SMT value"; - - if (op.getBody().front().getTerminator()->getNumOperands() != 1) - return op.emitOpError("must have exactly one yielded value"); - if (!isa( - op.getBody().front().getTerminator()->getOperand(0).getType())) - return op.emitOpError("yielded value must be of '!smt.bool' type"); - - for (auto regionWithIndex : llvm::enumerate(op.getPatterns())) { - unsigned i = regionWithIndex.index(); - Region ®ion = regionWithIndex.value(); - - if (op.getBody().getArgumentTypes() != region.getArgumentTypes()) - return op.emitOpError() - << "block argument number and types of the 'body' " - "and 'patterns' region #" - << i << " must match"; - if (region.front().getTerminator()->getNumOperands() < 1) - return op.emitOpError() << "'patterns' region #" << i - << " must have at least one yielded value"; - - // All operations in the 'patterns' region must be SMT operations. - auto result = region.walk([&](Operation *childOp) { - if (!isa(childOp->getDialect())) { - auto diag = op.emitOpError() - << "the 'patterns' region #" << i - << " may only contain SMT dialect operations"; - diag.attachNote(childOp->getLoc()) << "first non-SMT operation here"; - return WalkResult::interrupt(); - } - - // There may be no quantifier (or other variable binding) operations in - // the 'patterns' region. - if (isa(childOp)) { - auto diag = op.emitOpError() << "the 'patterns' region #" << i - << " must not contain " - "any variable binding operations"; - diag.attachNote(childOp->getLoc()) << "first violating operation here"; - return WalkResult::interrupt(); - } - - return WalkResult::advance(); - }); - if (result.wasInterrupted()) - return failure(); - } - - return success(); -} - -template -static void buildQuantifier( - OpBuilder &odsBuilder, OperationState &odsState, TypeRange boundVarTypes, - function_ref bodyBuilder, - std::optional> boundVarNames, - function_ref patternBuilder, - uint32_t weight, bool noPattern) { - odsState.addTypes(BoolType::get(odsBuilder.getContext())); - if (weight != 0) - odsState.getOrAddProperties().weight = - odsBuilder.getIntegerAttr(odsBuilder.getIntegerType(32), weight); - if (noPattern) - odsState.getOrAddProperties().noPattern = - odsBuilder.getUnitAttr(); - if (boundVarNames.has_value()) { - SmallVector boundVarNamesList; - for (StringRef str : *boundVarNames) - boundVarNamesList.emplace_back(odsBuilder.getStringAttr(str)); - odsState.getOrAddProperties().boundVarNames = - odsBuilder.getArrayAttr(boundVarNamesList); - } - { - OpBuilder::InsertionGuard guard(odsBuilder); - Region *region = odsState.addRegion(); - Block *block = odsBuilder.createBlock(region); - block->addArguments( - boundVarTypes, - SmallVector(boundVarTypes.size(), odsState.location)); - Value returnVal = - bodyBuilder(odsBuilder, odsState.location, block->getArguments()); - odsBuilder.create(odsState.location, returnVal); - } - if (patternBuilder) { - Region *region = odsState.addRegion(); - OpBuilder::InsertionGuard guard(odsBuilder); - Block *block = odsBuilder.createBlock(region); - block->addArguments( - boundVarTypes, - SmallVector(boundVarTypes.size(), odsState.location)); - ValueRange returnVals = - patternBuilder(odsBuilder, odsState.location, block->getArguments()); - odsBuilder.create(odsState.location, returnVals); - } -} - -LogicalResult ForallOp::verify() { - if (!getPatterns().empty() && getNoPattern()) - return emitOpError() << "patterns and the no_pattern attribute must not be " - "specified at the same time"; - - return success(); -} - -LogicalResult ForallOp::verifyRegions() { - return verifyQuantifierRegions(*this); -} - -void ForallOp::build( - OpBuilder &odsBuilder, OperationState &odsState, TypeRange boundVarTypes, - function_ref bodyBuilder, - std::optional> boundVarNames, - function_ref patternBuilder, - uint32_t weight, bool noPattern) { - buildQuantifier(odsBuilder, odsState, boundVarTypes, bodyBuilder, - boundVarNames, patternBuilder, weight, noPattern); -} - -//===----------------------------------------------------------------------===// -// ExistsOp -//===----------------------------------------------------------------------===// - -LogicalResult ExistsOp::verify() { - if (!getPatterns().empty() && getNoPattern()) - return emitOpError() << "patterns and the no_pattern attribute must not be " - "specified at the same time"; - - return success(); -} - -LogicalResult ExistsOp::verifyRegions() { - return verifyQuantifierRegions(*this); -} - -void ExistsOp::build( - OpBuilder &odsBuilder, OperationState &odsState, TypeRange boundVarTypes, - function_ref bodyBuilder, - std::optional> boundVarNames, - function_ref patternBuilder, - uint32_t weight, bool noPattern) { - buildQuantifier(odsBuilder, odsState, boundVarTypes, bodyBuilder, - boundVarNames, patternBuilder, weight, noPattern); -} - -#define GET_OP_CLASSES -#include "circt/Dialect/SMT/SMT.cpp.inc" diff --git a/lib/Dialect/SMT/SMTTypes.cpp b/lib/Dialect/SMT/SMTTypes.cpp deleted file mode 100644 index d67e2a1e9356..000000000000 --- a/lib/Dialect/SMT/SMTTypes.cpp +++ /dev/null @@ -1,92 +0,0 @@ -//===- SMTTypes.cpp -------------------------------------------------------===// -// -// 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 -// -//===----------------------------------------------------------------------===// - -#include "circt/Dialect/SMT/SMTTypes.h" -#include "circt/Dialect/SMT/SMTDialect.h" -#include "mlir/IR/Builders.h" -#include "mlir/IR/DialectImplementation.h" -#include "llvm/ADT/TypeSwitch.h" - -using namespace circt; -using namespace smt; -using namespace mlir; - -#define GET_TYPEDEF_CLASSES -#include "circt/Dialect/SMT/SMTTypes.cpp.inc" - -void SMTDialect::registerTypes() { - addTypes< -#define GET_TYPEDEF_LIST -#include "circt/Dialect/SMT/SMTTypes.cpp.inc" - >(); -} - -bool smt::isAnyNonFuncSMTValueType(Type type) { - return isAnySMTValueType(type) && !isa(type); -} - -bool smt::isAnySMTValueType(Type type) { - return isa(type); -} - -//===----------------------------------------------------------------------===// -// BitVectorType -//===----------------------------------------------------------------------===// - -LogicalResult -BitVectorType::verify(function_ref emitError, - int64_t width) { - if (width <= 0U) - return emitError() << "bit-vector must have at least a width of one"; - return success(); -} - -//===----------------------------------------------------------------------===// -// ArrayType -//===----------------------------------------------------------------------===// - -LogicalResult ArrayType::verify(function_ref emitError, - Type domainType, Type rangeType) { - if (!isAnySMTValueType(domainType)) - return emitError() << "domain must be any SMT value type"; - if (!isAnySMTValueType(rangeType)) - return emitError() << "range must be any SMT value type"; - - return success(); -} - -//===----------------------------------------------------------------------===// -// SMTFuncType -//===----------------------------------------------------------------------===// - -LogicalResult SMTFuncType::verify(function_ref emitError, - ArrayRef domainTypes, Type rangeType) { - if (domainTypes.empty()) - return emitError() << "domain must not be empty"; - if (!llvm::all_of(domainTypes, isAnyNonFuncSMTValueType)) - return emitError() << "domain types must be any non-function SMT type"; - if (!isAnyNonFuncSMTValueType(rangeType)) - return emitError() << "range type must be any non-function SMT type"; - - return success(); -} - -//===----------------------------------------------------------------------===// -// SortType -//===----------------------------------------------------------------------===// - -LogicalResult SortType::verify(function_ref emitError, - StringAttr identifier, - ArrayRef sortParams) { - if (!llvm::all_of(sortParams, isAnyNonFuncSMTValueType)) - return emitError() - << "sort parameter types must be any non-function SMT type"; - - return success(); -} diff --git a/lib/Target/ExportSMTLIB/CMakeLists.txt b/lib/Target/ExportSMTLIB/CMakeLists.txt index 7b7fb8f502e1..5150767ba53f 100644 --- a/lib/Target/ExportSMTLIB/CMakeLists.txt +++ b/lib/Target/ExportSMTLIB/CMakeLists.txt @@ -8,9 +8,9 @@ add_circt_translation_library(CIRCTExportSMTLIB LINK_LIBS PUBLIC CIRCTHW - CIRCTSMT CIRCTSupport MLIRFuncDialect MLIRIR + MLIRSMT MLIRTranslateLib ) diff --git a/lib/Target/ExportSMTLIB/ExportSMTLIB.cpp b/lib/Target/ExportSMTLIB/ExportSMTLIB.cpp index 92fbfdffef0a..bdcc72d2cf75 100644 --- a/lib/Target/ExportSMTLIB/ExportSMTLIB.cpp +++ b/lib/Target/ExportSMTLIB/ExportSMTLIB.cpp @@ -12,10 +12,10 @@ #include "circt/Target/ExportSMTLIB.h" #include "circt/Dialect/HW/HWDialect.h" -#include "circt/Dialect/SMT/SMTOps.h" -#include "circt/Dialect/SMT/SMTVisitors.h" #include "circt/Support/Namespace.h" #include "mlir/Dialect/Func/IR/FuncOps.h" +#include "mlir/Dialect/SMT/IR/SMTOps.h" +#include "mlir/Dialect/SMT/IR/SMTVisitors.h" #include "mlir/IR/BuiltinOps.h" #include "mlir/Support/IndentedOstream.h" #include "mlir/Tools/mlir-translate/Translation.h" @@ -25,6 +25,7 @@ #include "llvm/Support/raw_ostream.h" using namespace circt; +using namespace mlir; using namespace smt; using namespace ExportSMTLIB; diff --git a/llvm b/llvm index 9344b2196cbc..c6a892e0ed82 160000 --- a/llvm +++ b/llvm @@ -1 +1 @@ -Subproject commit 9344b2196cbc36cdc577314bbb2b889606ba6820 +Subproject commit c6a892e0ed82a378ad1a69905f70700bf57c68cf diff --git a/test/Dialect/Moore/types-errors.mlir b/test/Dialect/Moore/types-errors.mlir index 2156781fc46e..67b9d656230a 100644 --- a/test/Dialect/Moore/types-errors.mlir +++ b/test/Dialect/Moore/types-errors.mlir @@ -1,12 +1,12 @@ // RUN: circt-opt --verify-diagnostics --split-input-file %s // ----- -// expected-error @below {{invalid kind of Type specified}} +// expected-error @below {{invalid kind of type specified}} // expected-error @below {{parameter 'elementType' which is to be a `PackedType`}} unrealized_conversion_cast to !moore.array<4 x string> // ----- -// expected-error @below {{invalid kind of Type specified}} +// expected-error @below {{invalid kind of type specified}} // expected-error @below {{parameter 'elementType' which is to be a `PackedType`}} unrealized_conversion_cast to !moore.open_array diff --git a/tools/circt-bmc/CMakeLists.txt b/tools/circt-bmc/CMakeLists.txt index cc9c535719f1..d8dcaa21270f 100644 --- a/tools/circt-bmc/CMakeLists.txt +++ b/tools/circt-bmc/CMakeLists.txt @@ -20,7 +20,6 @@ target_link_libraries(circt-bmc CIRCTHWToSMT CIRCTOMTransforms CIRCTSeq - CIRCTSMT CIRCTSMTToZ3LLVM CIRCTSupport CIRCTVerif @@ -33,6 +32,7 @@ target_link_libraries(circt-bmc MLIRIR MLIRLLVMIRTransforms MLIRLLVMToLLVMIRTranslation + MLIRSMT MLIRTargetLLVMIRExport ${CIRCT_BMC_JIT_DEPS} diff --git a/tools/circt-bmc/circt-bmc.cpp b/tools/circt-bmc/circt-bmc.cpp index 59019e56bc9e..a6bbe45ef5dd 100644 --- a/tools/circt-bmc/circt-bmc.cpp +++ b/tools/circt-bmc/circt-bmc.cpp @@ -20,7 +20,6 @@ #include "circt/Dialect/HW/HWDialect.h" #include "circt/Dialect/OM/OMDialect.h" #include "circt/Dialect/OM/OMPasses.h" -#include "circt/Dialect/SMT/SMTDialect.h" #include "circt/Dialect/Seq/SeqDialect.h" #include "circt/Dialect/Verif/VerifDialect.h" #include "circt/Support/Passes.h" @@ -30,6 +29,7 @@ #include "mlir/Dialect/Func/Extensions/InlinerExtension.h" #include "mlir/Dialect/Func/IR/FuncOps.h" #include "mlir/Dialect/LLVMIR/Transforms/Passes.h" +#include "mlir/Dialect/SMT/IR/SMTDialect.h" #include "mlir/IR/BuiltinDialect.h" #include "mlir/IR/Diagnostics.h" #include "mlir/IR/OwningOpRef.h" @@ -328,7 +328,7 @@ int main(int argc, char **argv) { circt::hw::HWDialect, circt::om::OMDialect, circt::seq::SeqDialect, - circt::smt::SMTDialect, + mlir::smt::SMTDialect, circt::verif::VerifDialect, mlir::arith::ArithDialect, mlir::BuiltinDialect, diff --git a/tools/circt-lec/CMakeLists.txt b/tools/circt-lec/CMakeLists.txt index a167e7cbd9d4..fb59f3e001ea 100644 --- a/tools/circt-lec/CMakeLists.txt +++ b/tools/circt-lec/CMakeLists.txt @@ -19,7 +19,6 @@ target_link_libraries(circt-lec CIRCTHWToSMT CIRCTLECTransforms CIRCTOMTransforms - CIRCTSMT CIRCTSMTToZ3LLVM CIRCTSupport CIRCTVerif @@ -33,6 +32,7 @@ target_link_libraries(circt-lec MLIRLLVMIRTransforms MLIRLLVMToLLVMIRTranslation MLIRLLVMToLLVMIRTranslation + MLIRSMT MLIRTargetLLVMIRExport ${CIRCT_LEC_JIT_DEPS} diff --git a/tools/circt-lec/circt-lec.cpp b/tools/circt-lec/circt-lec.cpp index 2ff6370b7d20..1468e32021b5 100644 --- a/tools/circt-lec/circt-lec.cpp +++ b/tools/circt-lec/circt-lec.cpp @@ -22,7 +22,6 @@ #include "circt/Dialect/HW/HWDialect.h" #include "circt/Dialect/OM/OMDialect.h" #include "circt/Dialect/OM/OMPasses.h" -#include "circt/Dialect/SMT/SMTDialect.h" #include "circt/Dialect/Verif/VerifDialect.h" #include "circt/Support/Passes.h" #include "circt/Support/Version.h" @@ -31,6 +30,7 @@ #include "mlir/Dialect/Func/Extensions/InlinerExtension.h" #include "mlir/Dialect/Func/IR/FuncOps.h" #include "mlir/Dialect/LLVMIR/Transforms/Passes.h" +#include "mlir/Dialect/SMT/IR/SMTDialect.h" #include "mlir/IR/BuiltinDialect.h" #include "mlir/IR/Diagnostics.h" #include "mlir/IR/OwningOpRef.h" @@ -366,7 +366,7 @@ int main(int argc, char **argv) { circt::emit::EmitDialect, circt::hw::HWDialect, circt::om::OMDialect, - circt::smt::SMTDialect, + mlir::smt::SMTDialect, circt::verif::VerifDialect, mlir::arith::ArithDialect, mlir::BuiltinDialect, diff --git a/unittests/Dialect/CMakeLists.txt b/unittests/Dialect/CMakeLists.txt index cfc2573a09a6..3a4570dc69e3 100644 --- a/unittests/Dialect/CMakeLists.txt +++ b/unittests/Dialect/CMakeLists.txt @@ -5,4 +5,3 @@ add_subdirectory(HW) add_subdirectory(OM) add_subdirectory(RTG) add_subdirectory(RTGTest) -add_subdirectory(SMT) diff --git a/unittests/Dialect/SMT/AttributeTest.cpp b/unittests/Dialect/SMT/AttributeTest.cpp deleted file mode 100644 index 7761105a2a7d..000000000000 --- a/unittests/Dialect/SMT/AttributeTest.cpp +++ /dev/null @@ -1,119 +0,0 @@ -//===- AttributeTest.cpp - SMT attribute unit tests -----------------------===// -// -// 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 -// -//===----------------------------------------------------------------------===// - -#include "circt/Dialect/SMT/SMTAttributes.h" -#include "circt/Dialect/SMT/SMTDialect.h" -#include "circt/Dialect/SMT/SMTTypes.h" -#include "gtest/gtest.h" - -using namespace mlir; -using namespace circt; -using namespace smt; - -namespace { - -TEST(BitVectorAttrTest, MinBitWidth) { - MLIRContext context; - context.loadDialect(); - Location loc(UnknownLoc::get(&context)); - - auto attr = BitVectorAttr::getChecked(loc, &context, UINT64_C(0), 0U); - ASSERT_EQ(attr, BitVectorAttr()); - context.getDiagEngine().registerHandler([&](Diagnostic &diag) { - ASSERT_EQ(diag.str(), "bit-width must be at least 1, but got 0"); - }); -} - -TEST(BitVectorAttrTest, ParserAndPrinterCorrect) { - MLIRContext context; - context.loadDialect(); - - auto attr = BitVectorAttr::get(&context, "#b1010"); - ASSERT_EQ(attr.getValue(), APInt(4, 10)); - ASSERT_EQ(attr.getType(), BitVectorType::get(&context, 4)); - - // A bit-width divisible by 4 is always printed in hex - attr = BitVectorAttr::get(&context, "#b01011010"); - ASSERT_EQ(attr.getValueAsString(), "#x5a"); - - // A bit-width not divisible by 4 is always printed in binary - // Also, make sure leading zeros are printed - attr = BitVectorAttr::get(&context, "#b0101101"); - ASSERT_EQ(attr.getValueAsString(), "#b0101101"); - - attr = BitVectorAttr::get(&context, "#x3c"); - ASSERT_EQ(attr.getValueAsString(), "#x3c"); - - attr = BitVectorAttr::get(&context, "#x03c"); - ASSERT_EQ(attr.getValueAsString(), "#x03c"); -} - -TEST(BitVectorAttrTest, ExpectedOneDigit) { - MLIRContext context; - context.loadDialect(); - Location loc(UnknownLoc::get(&context)); - - auto attr = - BitVectorAttr::getChecked(loc, &context, static_cast("#b")); - ASSERT_EQ(attr, BitVectorAttr()); - context.getDiagEngine().registerHandler([&](Diagnostic &diag) { - ASSERT_EQ(diag.str(), "expected at least one digit"); - }); -} - -TEST(BitVectorAttrTest, ExpectedBOrX) { - MLIRContext context; - context.loadDialect(); - Location loc(UnknownLoc::get(&context)); - - auto attr = - BitVectorAttr::getChecked(loc, &context, static_cast("#c0")); - ASSERT_EQ(attr, BitVectorAttr()); - context.getDiagEngine().registerHandler([&](Diagnostic &diag) { - ASSERT_EQ(diag.str(), "expected either 'b' or 'x'"); - }); -} - -TEST(BitVectorAttrTest, ExpectedHashtag) { - MLIRContext context; - context.loadDialect(); - Location loc(UnknownLoc::get(&context)); - - auto attr = - BitVectorAttr::getChecked(loc, &context, static_cast("b0")); - ASSERT_EQ(attr, BitVectorAttr()); - context.getDiagEngine().registerHandler( - [&](Diagnostic &diag) { ASSERT_EQ(diag.str(), "expected '#'"); }); -} - -TEST(BitVectorAttrTest, OutOfRange) { - MLIRContext context; - context.loadDialect(); - Location loc(UnknownLoc::get(&context)); - - auto attr1 = BitVectorAttr::getChecked(loc, &context, UINT64_C(2), 1U); - auto attr63 = - BitVectorAttr::getChecked(loc, &context, UINT64_C(3) << 62, 63U); - ASSERT_EQ(attr1, BitVectorAttr()); - ASSERT_EQ(attr63, BitVectorAttr()); - context.getDiagEngine().registerHandler([&](Diagnostic &diag) { - ASSERT_EQ(diag.str(), - "value does not fit in a bit-vector of desired width"); - }); -} - -TEST(BitVectorAttrTest, GetUInt64Max) { - MLIRContext context; - context.loadDialect(); - auto attr64 = BitVectorAttr::get(&context, UINT64_MAX, 64); - auto attr65 = BitVectorAttr::get(&context, UINT64_MAX, 65); - ASSERT_EQ(attr64.getValue(), APInt::getAllOnes(64)); - ASSERT_EQ(attr65.getValue(), APInt::getAllOnes(64).zext(65)); -} - -} // namespace diff --git a/unittests/Dialect/SMT/CMakeLists.txt b/unittests/Dialect/SMT/CMakeLists.txt deleted file mode 100644 index 42c8fec4627b..000000000000 --- a/unittests/Dialect/SMT/CMakeLists.txt +++ /dev/null @@ -1,10 +0,0 @@ -add_circt_unittest(CIRCTSMTTests - AttributeTest.cpp - QuantifierTest.cpp - TypeTest.cpp -) - -target_link_libraries(CIRCTSMTTests - PRIVATE - CIRCTSMT -) diff --git a/unittests/Dialect/SMT/QuantifierTest.cpp b/unittests/Dialect/SMT/QuantifierTest.cpp deleted file mode 100644 index dd115d4a3f3e..000000000000 --- a/unittests/Dialect/SMT/QuantifierTest.cpp +++ /dev/null @@ -1,188 +0,0 @@ -//===- QuantifierTest.cpp - SMT quantifier operation unit tests -----------===// -// -// 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 -// -//===----------------------------------------------------------------------===// - -#include "circt/Dialect/SMT/SMTOps.h" -#include "gtest/gtest.h" - -using namespace mlir; -using namespace circt; -using namespace smt; - -namespace { - -//===----------------------------------------------------------------------===// -// Test custom builders of ExistsOp -//===----------------------------------------------------------------------===// - -TEST(QuantifierTest, ExistsBuilderWithPattern) { - MLIRContext context; - context.loadDialect(); - Location loc(UnknownLoc::get(&context)); - - OpBuilder builder(&context); - auto boolTy = BoolType::get(&context); - - ExistsOp existsOp = builder.create( - loc, TypeRange{boolTy, boolTy}, - [](OpBuilder &builder, Location loc, ValueRange boundVars) { - return builder.create(loc, boundVars); - }, - std::nullopt, - [](OpBuilder &builder, Location loc, ValueRange boundVars) { - return boundVars; - }, - /*weight=*/2); - - SmallVector buffer; - llvm::raw_svector_ostream stream(buffer); - existsOp.print(stream); - - ASSERT_STREQ( - stream.str().str().c_str(), - "%0 = smt.exists weight 2 {\n^bb0(%arg0: !smt.bool, " - "%arg1: !smt.bool):\n %0 = smt.and %arg0, %arg1\n smt.yield %0 : " - "!smt.bool\n} patterns {\n^bb0(%arg0: !smt.bool, %arg1: !smt.bool):\n " - "smt.yield %arg0, %arg1 : !smt.bool, !smt.bool\n}\n"); -} - -TEST(QuantifierTest, ExistsBuilderNoPattern) { - MLIRContext context; - context.loadDialect(); - Location loc(UnknownLoc::get(&context)); - - OpBuilder builder(&context); - auto boolTy = BoolType::get(&context); - - ExistsOp existsOp = builder.create( - loc, TypeRange{boolTy, boolTy}, - [](OpBuilder &builder, Location loc, ValueRange boundVars) { - return builder.create(loc, boundVars); - }, - ArrayRef{"a", "b"}, nullptr, /*weight=*/0, /*noPattern=*/true); - - SmallVector buffer; - llvm::raw_svector_ostream stream(buffer); - existsOp.print(stream); - - ASSERT_STREQ(stream.str().str().c_str(), - "%0 = smt.exists [\"a\", \"b\"] no_pattern {\n^bb0(%arg0: " - "!smt.bool, %arg1: !smt.bool):\n %0 = smt.and %arg0, %arg1\n " - "smt.yield %0 : !smt.bool\n}\n"); -} - -TEST(QuantifierTest, ExistsBuilderDefault) { - MLIRContext context; - context.loadDialect(); - Location loc(UnknownLoc::get(&context)); - - OpBuilder builder(&context); - auto boolTy = BoolType::get(&context); - - ExistsOp existsOp = builder.create( - loc, TypeRange{boolTy, boolTy}, - [](OpBuilder &builder, Location loc, ValueRange boundVars) { - return builder.create(loc, boundVars); - }, - ArrayRef{"a", "b"}); - - SmallVector buffer; - llvm::raw_svector_ostream stream(buffer); - existsOp.print(stream); - - ASSERT_STREQ(stream.str().str().c_str(), - "%0 = smt.exists [\"a\", \"b\"] {\n^bb0(%arg0: !smt.bool, " - "%arg1: !smt.bool):\n %0 = smt.and %arg0, %arg1\n smt.yield " - "%0 : !smt.bool\n}\n"); -} - -//===----------------------------------------------------------------------===// -// Test custom builders of ForallOp -//===----------------------------------------------------------------------===// - -TEST(QuantifierTest, ForallBuilderWithPattern) { - MLIRContext context; - context.loadDialect(); - Location loc(UnknownLoc::get(&context)); - - OpBuilder builder(&context); - auto boolTy = BoolType::get(&context); - - ForallOp forallOp = builder.create( - loc, TypeRange{boolTy, boolTy}, - [](OpBuilder &builder, Location loc, ValueRange boundVars) { - return builder.create(loc, boundVars); - }, - ArrayRef{"a", "b"}, - [](OpBuilder &builder, Location loc, ValueRange boundVars) { - return boundVars; - }, - /*weight=*/2); - - SmallVector buffer; - llvm::raw_svector_ostream stream(buffer); - forallOp.print(stream); - - ASSERT_STREQ( - stream.str().str().c_str(), - "%0 = smt.forall [\"a\", \"b\"] weight 2 {\n^bb0(%arg0: !smt.bool, " - "%arg1: !smt.bool):\n %0 = smt.and %arg0, %arg1\n smt.yield %0 : " - "!smt.bool\n} patterns {\n^bb0(%arg0: !smt.bool, %arg1: !smt.bool):\n " - "smt.yield %arg0, %arg1 : !smt.bool, !smt.bool\n}\n"); -} - -TEST(QuantifierTest, ForallBuilderNoPattern) { - MLIRContext context; - context.loadDialect(); - Location loc(UnknownLoc::get(&context)); - - OpBuilder builder(&context); - auto boolTy = BoolType::get(&context); - - ForallOp forallOp = builder.create( - loc, TypeRange{boolTy, boolTy}, - [](OpBuilder &builder, Location loc, ValueRange boundVars) { - return builder.create(loc, boundVars); - }, - ArrayRef{"a", "b"}, nullptr, /*weight=*/0, /*noPattern=*/true); - - SmallVector buffer; - llvm::raw_svector_ostream stream(buffer); - forallOp.print(stream); - - ASSERT_STREQ(stream.str().str().c_str(), - "%0 = smt.forall [\"a\", \"b\"] no_pattern {\n^bb0(%arg0: " - "!smt.bool, %arg1: !smt.bool):\n %0 = smt.and %arg0, %arg1\n " - "smt.yield %0 : !smt.bool\n}\n"); -} - -TEST(QuantifierTest, ForallBuilderDefault) { - MLIRContext context; - context.loadDialect(); - Location loc(UnknownLoc::get(&context)); - - OpBuilder builder(&context); - auto boolTy = BoolType::get(&context); - - ForallOp forallOp = builder.create( - loc, TypeRange{boolTy, boolTy}, - [](OpBuilder &builder, Location loc, ValueRange boundVars) { - return builder.create(loc, boundVars); - }, - std::nullopt); - - SmallVector buffer; - llvm::raw_svector_ostream stream(buffer); - forallOp.print(stream); - - ASSERT_STREQ(stream.str().str().c_str(), - "%0 = smt.forall {\n^bb0(%arg0: !smt.bool, " - "%arg1: !smt.bool):\n %0 = smt.and %arg0, %arg1\n smt.yield " - "%0 : !smt.bool\n}\n"); -} - -} // namespace diff --git a/unittests/Dialect/SMT/TypeTest.cpp b/unittests/Dialect/SMT/TypeTest.cpp deleted file mode 100644 index 1eaebbef13d0..000000000000 --- a/unittests/Dialect/SMT/TypeTest.cpp +++ /dev/null @@ -1,32 +0,0 @@ -//===- TypeTest.cpp - SMT type unit tests ---------------------------------===// -// -// 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 -// -//===----------------------------------------------------------------------===// - -#include "circt/Dialect/SMT/SMTDialect.h" -#include "circt/Dialect/SMT/SMTTypes.h" -#include "gtest/gtest.h" - -using namespace mlir; -using namespace circt; -using namespace smt; - -namespace { - -TEST(SMTFuncTypeTest, NonEmptyDomain) { - MLIRContext context; - context.loadDialect(); - Location loc(UnknownLoc::get(&context)); - - auto boolTy = BoolType::get(&context); - auto funcTy = SMTFuncType::getChecked(loc, ArrayRef{}, boolTy); - ASSERT_EQ(funcTy, Type()); - context.getDiagEngine().registerHandler([&](Diagnostic &diag) { - ASSERT_STREQ(diag.str().c_str(), "domain must not be empty"); - }); -} - -} // namespace