terapines
/
circt
mirror of https://github.com/llvm/circt.git
2
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

[LLVM] integrate upstream SMT (#8408)

This commit is contained in:
Maksim Levental 2025-04-14 14:34:14 -04:00 committed by GitHub
parent 30571383d9
commit 7ea40140a1
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
47 changed files with 75 additions and 2818 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
include/circt/Conversion/Passes.td
View File

@ -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 = [

1
include/circt/Dialect/CMakeLists.txt
View File

@ -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)

15
include/circt/Dialect/SMT/CMakeLists.txt
View File

@ -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)

22
include/circt/Dialect/SMT/SMT.td
View File

@ -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

99
include/circt/Dialect/SMT/SMTArrayOps.td
View File

@ -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<string mnemonic, list<Trait> traits = []> :
SMTOp<"array." # mnemonic, traits>;
def ArrayStoreOp : SMTArrayOp<"store", [
Pure,
TypesMatchWith<"summary", "array", "index",
"cast<ArrayType>($_self).getDomainType()">,
TypesMatchWith<"summary", "array", "value",
"cast<ArrayType>($_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<ArrayType>($_self).getDomainType()">,
TypesMatchWith<"summary", "array", "result",
"cast<ArrayType>($_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<ArrayType>($_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

29
include/circt/Dialect/SMT/SMTAttributes.h
View File

@ -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

74
include/circt/Dialect/SMT/SMTAttributes.td
View File

@ -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<SMTDialect, "BitVector", [
DeclareAttrInterfaceMethods<TypedAttrInterface>
]> {
let mnemonic = "bv";
let description = [{
This attribute represents a constant value of the `(_ BitVec width)` sort as
described in the [SMT bit-vector
theory](https://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml).
The constant is as #bX (binary) or #xX (hexadecimal) in SMT-LIB
where X is the value in the corresponding format without any further
prefixing. Here, the bit-vector constant is given as a regular integer
literal and the associated bit-vector type indicating the bit-width.
Examples:
```mlir
#smt.bv<5> : !smt.bv<4>
#smt.bv<92> : !smt.bv<8>
```
The explicit type-suffix is mandatory to uniquely represent the attribute,
i.e., this attribute should always be used in the extended form (using the
`quantified` keyword in the operation assembly format string).
The bit-width must be greater than zero (i.e., at least one digit has to be
present).
}];
let parameters = (ins "llvm::APInt":$value);
let hasCustomAssemblyFormat = true;
let genVerifyDecl = true;
// 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

255
include/circt/Dialect/SMT/SMTBitVectorOps.td
View File

@ -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<string mnemonic, list<Trait> traits = []> :
Op<SMTDialect, "bv." # mnemonic, traits>;
def BVConstantOp : SMTBVOp<"constant", [
Pure,
ConstantLike,
FirstAttrDerivedResultType,
DeclareOpInterfaceMethods<InferTypeOpInterface, ["inferReturnTypes"]>,
DeclareOpInterfaceMethods<OpAsmOpInterface, ["getAsmResultNames"]>
]> {
let summary = "produce a constant bit-vector";
let description = [{
This operation produces an SSA value equal to the bit-vector constant
specified by the 'value' attribute.
Refer to the `BitVectorAttr` documentation for more information about
the semantics of bit-vector constants, their format, and associated sort.
The result type always matches the attribute's type.
Examples:
```mlir
%c92_bv8 = smt.bv.constant #smt.bv<92> : !smt.bv<8>
%c5_bv4 = smt.bv.constant #smt.bv<5> : !smt.bv<4>
```
}];
let arguments = (ins BitVectorAttr:$value);
let results = (outs BitVectorType:$result);
let assemblyFormat = "qualified($value) attr-dict";
let builders = [
OpBuilder<(ins "const llvm::APInt &":$value), [{
build($_builder, $_state,
BitVectorAttr::get($_builder.getContext(), value));
}]>,
OpBuilder<(ins "uint64_t":$value, "unsigned":$width), [{
build($_builder, $_state,
BitVectorAttr::get($_builder.getContext(), value, width));
}]>,
];
let hasFolder = true;
}
class BVArithmeticOrBitwiseOp<string mnemonic, string desc> :
SMTBVOp<mnemonic, [Pure, SameOperandsAndResultType]> {
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<string mnemonic, string desc> :
BVArithmeticOrBitwiseOp<mnemonic, desc> {
let arguments = (ins BitVectorType:$lhs, BitVectorType:$rhs);
let assemblyFormat = "$lhs `,` $rhs attr-dict `:` qualified(type($result))";
}
class UnaryBVOp<string mnemonic, string desc> :
BVArithmeticOrBitwiseOp<mnemonic, desc> {
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<InferTypeOpInterface, ["inferReturnTypes"]>
]> {
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

20
include/circt/Dialect/SMT/SMTDialect.h
View File

@ -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

30
include/circt/Dialect/SMT/SMTDialect.td
View File

@ -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

137
include/circt/Dialect/SMT/SMTIntOps.td
View File

@ -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<string mnemonic, list<Trait> traits = []> :
SMTOp<"int." # mnemonic, traits>;
def IntConstantOp : SMTIntOp<"constant", [
Pure,
ConstantLike,
DeclareOpInterfaceMethods<OpAsmOpInterface, ["getAsmResultNames"]>,
]> {
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<string mnemonic> : SMTIntOp<mnemonic, [Pure, Commutative]> {
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<IntType>:$inputs);
let results = (outs IntType:$result);
let assemblyFormat = "$inputs attr-dict";
let builders = [
OpBuilder<(ins "mlir::ValueRange":$inputs), [{
build($_builder, $_state, $_builder.getType<smt::IntType>(), inputs);
}]>,
];
}
class BinaryIntOp<string mnemonic> : SMTIntOp<mnemonic, [Pure]> {
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

25
include/circt/Dialect/SMT/SMTOps.h
View File

@ -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

477
include/circt/Dialect/SMT/SMTOps.td
View File

@ -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<string mnemonic, list<Trait> traits = []> :
Op<SMTDialect, mnemonic, traits>;
def DeclareFunOp : SMTOp<"declare_fun", [
DeclareOpInterfaceMethods<OpAsmOpInterface, ["getAsmResultNames"]>
]> {
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<StrAttr>:$namePrefix);
let results = (outs Res<AnySMTType, "a symbolic value", [MemAlloc]>:$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<OpAsmOpInterface, ["getAsmResultNames"]>,
]> {
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<AnyNonSMTType>:$inputs);
let regions = (region SizedRegion<1>:$bodyRegion);
let results = (outs Variadic<AnyNonSMTType>:$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<I32Attr, [IntNonNegative]>:$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<I32Attr, [IntNonNegative]>:$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<AnyType>:$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<AnyType>:$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<SMTFuncType>($_self).getRangeType()">,
RangedTypesMatchWith<"summary", "func", "args",
"cast<SMTFuncType>($_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<AnyNonFuncSMTType>:$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<AnyNonFuncSMTType>:$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<AnyNonFuncSMTType>:$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<string mnemonic, string desc> : SMTOp<mnemonic, [Pure]> {
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<BoolType>:$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<string mnemonic> : SMTOp<mnemonic, [
RecursivelySpeculatable,
RecursiveMemoryEffects,
SingleBlockImplicitTerminator<"smt::YieldOp">,
]> {
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<I32Attr, "0">:$weight,
UnitAttr:$noPattern,
OptionalAttr<StrArrayAttr>:$boundVarNames);
let regions = (region SizedRegion<1>:$body,
VariadicRegion<SizedRegion<1>>:$patterns);
let results = (outs BoolType:$result);
let builders = [
OpBuilder<(ins
"TypeRange":$boundVarTypes,
"function_ref<Value(OpBuilder &, Location, ValueRange)>":$bodyBuilder,
CArg<"std::optional<ArrayRef<StringRef>>", "std::nullopt">:$boundVarNames,
CArg<"function_ref<ValueRange(OpBuilder &, Location, ValueRange)>",
"{}">:$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

30
include/circt/Dialect/SMT/SMTTypes.h
View File

@ -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

145
include/circt/Dialect/SMT/SMTTypes.td
View File

@ -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<string name> : TypeDef<SMTDialect, name> { }
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<mlir::Type>":$domainTypes,
"mlir::Type":$rangeType), [{
return $_get(rangeType.getContext(), domainTypes, rangeType);
}]>,
TypeBuilderWithInferredContext<(ins "mlir::Type":$rangeType), [{
return $_get(rangeType.getContext(),
llvm::ArrayRef<mlir::Type>{}, 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<mlir::Type>":$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<mlir::Type>{});
}]>,
];
let genVerifyDecl = true;
}
def AnySMTType : Type<CPred<"smt::isAnySMTValueType($_self)">,
"any SMT value type">;
def AnyNonFuncSMTType : Type<CPred<"smt::isAnyNonFuncSMTValueType($_self)">,
"any non-function SMT value type">;
def AnyNonSMTType : Type<Neg<AnySMTType.predicate>, "any non-smt type">;
#endif // CIRCT_DIALECT_SMT_SMTTYPES_TD

201
include/circt/Dialect/SMT/SMTVisitors.h
View File

@ -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 <typename ConcreteType, typename ResultType = void,
typename... ExtraArgs>
class SMTOpVisitor {
public:
ResultType dispatchSMTOpVisitor(Operation *op, ExtraArgs... args) {
auto *thisCast = static_cast<ConcreteType *>(this);
return TypeSwitch<Operation *, ResultType>(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<ConcreteType *>(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 <typename ConcreteType, typename ResultType = void,
typename... ExtraArgs>
class SMTTypeVisitor {
public:
ResultType dispatchSMTTypeVisitor(Type type, ExtraArgs... args) {
auto *thisCast = static_cast<ConcreteType *>(this);
return TypeSwitch<Type, ResultType>(type)
.template Case<BoolType, IntType, BitVectorType, ArrayType, SMTFuncType,
SortType>([&](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<ConcreteType *>(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

4
include/circt/InitAllDialects.h
View File

@ -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 &registry) {
#endif
seq::SeqDialect,
sim::SimDialect,
smt::SMTDialect,
mlir::smt::SMTDialect,
ssp::SSPDialect,
sv::SVDialect,
systemc::SystemCDialect,

2
lib/Bindings/Python/dialects/SMTOps.td
View File

@ -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

2
lib/CAPI/Dialect/CMakeLists.txt
View File

@ -231,5 +231,5 @@ add_circt_public_c_api_library(CIRCTCAPISMT
LINK_LIBS PUBLIC
MLIRCAPIIR
CIRCTSMT
MLIRSMT
)

8
lib/CAPI/Dialect/SMT.cpp
View File

@ -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.

2
lib/Conversion/CombToSMT/CMakeLists.txt
View File

@ -10,6 +10,6 @@ add_circt_conversion_library(CIRCTCombToSMT
LINK_LIBS PUBLIC
CIRCTComb
CIRCTHWToSMT
CIRCTSMT
MLIRSMT
MLIRTransforms
)

5
lib/Conversion/CombToSMT/CombToSMT.cpp
View File

@ -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<SourceOp> {
namespace {
struct ConvertCombToSMTPass
: public impl::ConvertCombToSMTBase<ConvertCombToSMTPass> {
: public circt::impl::ConvertCombToSMTBase<ConvertCombToSMTPass> {
void runOnOperation() override;
};
} // namespace

2
lib/Conversion/HWToSMT/CMakeLists.txt
View File

@ -9,9 +9,9 @@ add_circt_conversion_library(CIRCTHWToSMT
LINK_LIBS PUBLIC
CIRCTHW
CIRCTSMT
CIRCTSeq
MLIRFuncDialect
MLIRSMT
MLIRTransforms
MLIRTransformUtils
)

75
lib/Conversion/HWToSMT/HWToSMT.cpp
View File

@ -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<ConstantOp> {
if (adaptor.getValue().getBitWidth() < 1)
return rewriter.notifyMatchFailure(op.getLoc(),
"0-bit constants not supported");
rewriter.replaceOpWithNewOp<smt::BVConstantOp>(op, adaptor.getValue());
rewriter.replaceOpWithNewOp<mlir::smt::BVConstantOp>(op,
adaptor.getValue());
return success();
}
};
@ -111,11 +112,11 @@ struct ArrayCreateOpConversion : OpConversionPattern<ArrayCreateOp> {
unsigned width = adaptor.getInputs().size();
Value arr = rewriter.create<smt::DeclareFunOp>(loc, arrTy);
Value arr = rewriter.create<mlir::smt::DeclareFunOp>(loc, arrTy);
for (auto [i, el] : llvm::enumerate(adaptor.getInputs())) {
Value idx = rewriter.create<smt::BVConstantOp>(loc, width - i - 1,
llvm::Log2_64_Ceil(width));
arr = rewriter.create<smt::ArrayStoreOp>(loc, arr, idx, el);
Value idx = rewriter.create<mlir::smt::BVConstantOp>(
loc, width - i - 1, llvm::Log2_64_Ceil(width));
arr = rewriter.create<mlir::smt::ArrayStoreOp>(loc, arr, idx, el);
}
rewriter.replaceOp(op, arr);
@ -139,14 +140,16 @@ struct ArrayGetOpConversion : OpConversionPattern<ArrayGetOp> {
return rewriter.notifyMatchFailure(op.getLoc(),
"unsupported array element type");
Value oobVal = rewriter.create<smt::DeclareFunOp>(loc, type);
Value numElementsVal = rewriter.create<smt::BVConstantOp>(
Value oobVal = rewriter.create<mlir::smt::DeclareFunOp>(loc, type);
Value numElementsVal = rewriter.create<mlir::smt::BVConstantOp>(
loc, numElements - 1, llvm::Log2_64_Ceil(numElements));
Value inBounds = rewriter.create<smt::BVCmpOp>(
loc, smt::BVCmpPredicate::ule, adaptor.getIndex(), numElementsVal);
Value indexed = rewriter.create<smt::ArraySelectOp>(loc, adaptor.getInput(),
adaptor.getIndex());
rewriter.replaceOpWithNewOp<smt::IteOp>(op, inBounds, indexed, oobVal);
Value inBounds =
rewriter.create<mlir::smt::BVCmpOp>(loc, mlir::smt::BVCmpPredicate::ule,
adaptor.getIndex(), numElementsVal);
Value indexed = rewriter.create<mlir::smt::ArraySelectOp>(
loc, adaptor.getInput(), adaptor.getIndex());
rewriter.replaceOpWithNewOp<mlir::smt::IteOp>(op, inBounds, indexed,
oobVal);
return success();
}
};
@ -189,18 +192,18 @@ void circt::populateHWToSMTTypeConverter(TypeConverter &converter) {
converter.addConversion([](IntegerType type) -> std::optional<Type> {
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<Type> {
return smt::BitVectorType::get(type.getContext(), 1);
return mlir::smt::BitVectorType::get(type.getContext(), 1);
});
converter.addConversion([&](ArrayType type) -> std::optional<Type> {
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<N>'-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<smt::BoolType>(inputs[0].getType()))
if (!isa<mlir::smt::BoolType>(inputs[0].getType()))
return Value();
unsigned width = resultType.getWidth();
Value constZero = builder.create<smt::BVConstantOp>(loc, 0, width);
Value constOne = builder.create<smt::BVConstantOp>(loc, 1, width);
return builder.create<smt::IteOp>(loc, inputs[0], constOne, constZero);
Value constZero =
builder.create<mlir::smt::BVConstantOp>(loc, 0, width);
Value constOne = builder.create<mlir::smt::BVConstantOp>(loc, 1, width);
return builder.create<mlir::smt::IteOp>(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<smt::BoolType>(castOp.getInputs()[0].getType()))
if (!isa<mlir::smt::BoolType>(castOp.getInputs()[0].getType()))
return Value();
Value constZero = builder.create<smt::BVConstantOp>(loc, 0, 1);
Value constOne = builder.create<smt::BVConstantOp>(loc, 1, 1);
return builder.create<smt::IteOp>(loc, castOp.getInputs()[0], constOne,
constZero);
Value constZero = builder.create<mlir::smt::BVConstantOp>(loc, 0, 1);
Value constOne = builder.create<mlir::smt::BVConstantOp>(loc, 1, 1);
return builder.create<mlir::smt::IteOp>(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<smt::BitVectorType>(inputs[0].getType());
auto bvType = dyn_cast<mlir::smt::BitVectorType>(inputs[0].getType());
if (!bvType || bvType.getWidth() != 1)
return Value();
Value constOne = builder.create<smt::BVConstantOp>(loc, 1, 1);
return builder.create<smt::EqOp>(loc, inputs[0], constOne);
Value constOne = builder.create<mlir::smt::BVConstantOp>(loc, 1, 1);
return builder.create<mlir::smt::EqOp>(loc, inputs[0], constOne);
});
// Default source materialization to convert from illegal types to legal
@ -294,7 +299,7 @@ void ConvertHWToSMTPass::runOnOperation() {
target.addIllegalDialect<hw::HWDialect>();
target.addIllegalOp<seq::FromClockOp>();
target.addIllegalOp<seq::ToClockOp>();
target.addLegalDialect<smt::SMTDialect>();
target.addLegalDialect<mlir::smt::SMTDialect>();
target.addLegalDialect<mlir::func::FuncDialect>();
RewritePatternSet patterns(&getContext());

2
lib/Conversion/SMTToZ3LLVM/CMakeLists.txt
View File

@ -8,12 +8,12 @@ add_circt_conversion_library(CIRCTSMTToZ3LLVM
Core
LINK_LIBS PUBLIC
CIRCTSMT
CIRCTSupport
MLIRLLVMCommonConversion
MLIRSCFToControlFlow
MLIRControlFlowToLLVM
MLIRArithToLLVM
MLIRFuncToLLVM
MLIRSMT
MLIRTransforms
)

2
lib/Conversion/SMTToZ3LLVM/LowerSMTToZ3LLVM.cpp
View File

@ -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"

2
lib/Conversion/VerifToSMT/CMakeLists.txt
View File

@ -10,11 +10,11 @@ add_circt_conversion_library(CIRCTVerifToSMT
LINK_LIBS PUBLIC
CIRCTHW
CIRCTHWToSMT
CIRCTSMT
CIRCTVerif
MLIRArithDialect
MLIRFuncDialect
MLIRSCFDialect
MLIRSMT
MLIRTransforms
MLIRTransformUtils
MLIRReconcileUnrealizedCasts

4
lib/Conversion/VerifToSMT/VerifToSMT.cpp
View File

@ -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"

1
lib/Dialect/CMakeLists.txt
View File

@ -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)

27
lib/Dialect/SMT/CMakeLists.txt
View File

@ -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
)

201
lib/Dialect/SMT/SMTAttributes.cpp
View File

@ -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>())
BitVectorAttrStorage(std::move(key));
}
APInt value;
};
} // namespace detail
} // namespace smt
} // namespace circt
APInt BitVectorAttr::getValue() const { return getImpl()->value; }
LogicalResult BitVectorAttr::verify(
function_ref<InFlightDiagnostic()> 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<char> 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<char> 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<char> leadingZeros(width - toPrint.size(), '0');
return (pref + "b" + Twine(leadingZeros) + toPrint).str();
}
/// Parse an SMT-LIB formatted bit-vector string.
static FailureOr<APInt>
parseBitVectorString(function_ref<InFlightDiagnostic()> 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<InFlightDiagnostic()> 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<InFlightDiagnostic()> 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(<attr>)` in operation assembly formats.
if (!odsType || !llvm::isa<BitVectorType>(odsType)) {
odsParser.emitError(loc) << "explicit bit-vector type required";
return {};
}
unsigned width = llvm::cast<BitVectorType>(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"
>();
}

47
lib/Dialect/SMT/SMTDialect.cpp
View File

@ -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<BitVectorType>(type)) {
if (auto attrValue = dyn_cast<BitVectorAttr>(value)) {
assert(bvType == attrValue.getType() &&
"attribute and desired result types have to match");
return builder.create<BVConstantOp>(loc, attrValue);
}
}
// BoolType constants can materialize into smt.constant
if (auto boolType = dyn_cast<BoolType>(type)) {
if (auto attrValue = dyn_cast<BoolAttr>(value))
return builder.create<BoolConstantOp>(loc, attrValue);
}
return nullptr;
}
#include "circt/Dialect/SMT/SMTDialect.cpp.inc"
#include "circt/Dialect/SMT/SMTEnums.cpp.inc"

472
lib/Dialect/SMT/SMTOps.cpp
View File

@ -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<mlir::Location> location,
::mlir::ValueRange operands, ::mlir::DictionaryAttr attributes,
::mlir::OpaqueProperties properties, ::mlir::RegionRange regions,
::llvm::SmallVectorImpl<::mlir::Type> &inferredReturnTypes) {
inferredReturnTypes.push_back(
properties.as<Properties *>()->getValue().getType());
return success();
}
void BVConstantOp::getAsmResultNames(
function_ref<void(Value, StringRef)> setNameFn) {
SmallVector<char, 128> 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<void(Value, StringRef)> 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<OpAsmParser::UnresolvedOperand, 4> 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<Type>(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<BitVectorType>(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> location, ValueRange operands,
DictionaryAttr attributes, OpaqueProperties properties, RegionRange regions,
SmallVectorImpl<Type> &inferredReturnTypes) {
inferredReturnTypes.push_back(BitVectorType::get(
context, cast<BitVectorType>(operands[0].getType()).getWidth() +
cast<BitVectorType>(operands[1].getType()).getWidth()));
return success();
}
//===----------------------------------------------------------------------===//
// RepeatOp
//===----------------------------------------------------------------------===//
LogicalResult RepeatOp::verify() {
unsigned inputWidth = cast<BitVectorType>(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<BitVectorType>(getInput().getType()).getWidth();
unsigned resultWidth = getType().getWidth();
return resultWidth / inputWidth;
}
void RepeatOp::build(OpBuilder &builder, OperationState &state, unsigned count,
Value input) {
unsigned inputWidth = cast<BitVectorType>(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<BitVectorType>(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<void(Value, StringRef)> 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<void(Value, StringRef)> setNameFn) {
SmallVector<char, 32> 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<Properties>().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 <typename QuantifierOp>
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<BoolType>(
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 &region = 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<SMTDialect>(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<ForallOp, ExistsOp>(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 <typename Properties>
static void buildQuantifier(
OpBuilder &odsBuilder, OperationState &odsState, TypeRange boundVarTypes,
function_ref<Value(OpBuilder &, Location, ValueRange)> bodyBuilder,
std::optional<ArrayRef<StringRef>> boundVarNames,
function_ref<ValueRange(OpBuilder &, Location, ValueRange)> patternBuilder,
uint32_t weight, bool noPattern) {
odsState.addTypes(BoolType::get(odsBuilder.getContext()));
if (weight != 0)
odsState.getOrAddProperties<Properties>().weight =
odsBuilder.getIntegerAttr(odsBuilder.getIntegerType(32), weight);
if (noPattern)
odsState.getOrAddProperties<Properties>().noPattern =
odsBuilder.getUnitAttr();
if (boundVarNames.has_value()) {
SmallVector<Attribute> boundVarNamesList;
for (StringRef str : *boundVarNames)
boundVarNamesList.emplace_back(odsBuilder.getStringAttr(str));
odsState.getOrAddProperties<Properties>().boundVarNames =
odsBuilder.getArrayAttr(boundVarNamesList);
}
{
OpBuilder::InsertionGuard guard(odsBuilder);
Region *region = odsState.addRegion();
Block *block = odsBuilder.createBlock(region);
block->addArguments(
boundVarTypes,
SmallVector<Location>(boundVarTypes.size(), odsState.location));
Value returnVal =
bodyBuilder(odsBuilder, odsState.location, block->getArguments());
odsBuilder.create<smt::YieldOp>(odsState.location, returnVal);
}
if (patternBuilder) {
Region *region = odsState.addRegion();
OpBuilder::InsertionGuard guard(odsBuilder);
Block *block = odsBuilder.createBlock(region);
block->addArguments(
boundVarTypes,
SmallVector<Location>(boundVarTypes.size(), odsState.location));
ValueRange returnVals =
patternBuilder(odsBuilder, odsState.location, block->getArguments());
odsBuilder.create<smt::YieldOp>(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<Value(OpBuilder &, Location, ValueRange)> bodyBuilder,
std::optional<ArrayRef<StringRef>> boundVarNames,
function_ref<ValueRange(OpBuilder &, Location, ValueRange)> patternBuilder,
uint32_t weight, bool noPattern) {
buildQuantifier<Properties>(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<Value(OpBuilder &, Location, ValueRange)> bodyBuilder,
std::optional<ArrayRef<StringRef>> boundVarNames,
function_ref<ValueRange(OpBuilder &, Location, ValueRange)> patternBuilder,
uint32_t weight, bool noPattern) {
buildQuantifier<Properties>(odsBuilder, odsState, boundVarTypes, bodyBuilder,
boundVarNames, patternBuilder, weight, noPattern);
}
#define GET_OP_CLASSES
#include "circt/Dialect/SMT/SMT.cpp.inc"

92
lib/Dialect/SMT/SMTTypes.cpp
View File

@ -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<SMTFuncType>(type);
}
bool smt::isAnySMTValueType(Type type) {
return isa<BoolType, BitVectorType, ArrayType, IntType, SortType,
SMTFuncType>(type);
}
//===----------------------------------------------------------------------===//
// BitVectorType
//===----------------------------------------------------------------------===//
LogicalResult
BitVectorType::verify(function_ref<InFlightDiagnostic()> 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<InFlightDiagnostic()> 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<InFlightDiagnostic()> emitError,
ArrayRef<Type> 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<InFlightDiagnostic()> emitError,
StringAttr identifier,
ArrayRef<Type> sortParams) {
if (!llvm::all_of(sortParams, isAnyNonFuncSMTValueType))
return emitError()
<< "sort parameter types must be any non-function SMT type";
return success();
}

2
lib/Target/ExportSMTLIB/CMakeLists.txt
View File

@ -8,9 +8,9 @@ add_circt_translation_library(CIRCTExportSMTLIB
LINK_LIBS PUBLIC
CIRCTHW
CIRCTSMT
CIRCTSupport
MLIRFuncDialect
MLIRIR
MLIRSMT
MLIRTranslateLib
)

5
lib/Target/ExportSMTLIB/ExportSMTLIB.cpp
View File

@ -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;

2
llvm

@ -1 +1 @@
Subproject commit 9344b2196cbc36cdc577314bbb2b889606ba6820
Subproject commit c6a892e0ed82a378ad1a69905f70700bf57c68cf

4
test/Dialect/Moore/types-errors.mlir
View File

@ -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<string>

2
tools/circt-bmc/CMakeLists.txt
View File

@ -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}

4
tools/circt-bmc/circt-bmc.cpp
View File

@ -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,

2
tools/circt-lec/CMakeLists.txt
View File

@ -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}

4
tools/circt-lec/circt-lec.cpp
View File

@ -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,

1
unittests/Dialect/CMakeLists.txt
View File

@ -5,4 +5,3 @@ add_subdirectory(HW)
add_subdirectory(OM)
add_subdirectory(RTG)
add_subdirectory(RTGTest)
add_subdirectory(SMT)

119
unittests/Dialect/SMT/AttributeTest.cpp
View File

@ -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<SMTDialect>();
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<SMTDialect>();
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<SMTDialect>();
Location loc(UnknownLoc::get(&context));
auto attr =
BitVectorAttr::getChecked(loc, &context, static_cast<StringRef>("#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<SMTDialect>();
Location loc(UnknownLoc::get(&context));
auto attr =
BitVectorAttr::getChecked(loc, &context, static_cast<StringRef>("#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<SMTDialect>();
Location loc(UnknownLoc::get(&context));
auto attr =
BitVectorAttr::getChecked(loc, &context, static_cast<StringRef>("b0"));
ASSERT_EQ(attr, BitVectorAttr());
context.getDiagEngine().registerHandler(
[&](Diagnostic &diag) { ASSERT_EQ(diag.str(), "expected '#'"); });
}
TEST(BitVectorAttrTest, OutOfRange) {
MLIRContext context;
context.loadDialect<SMTDialect>();
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<SMTDialect>();
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

10
unittests/Dialect/SMT/CMakeLists.txt
View File

@ -1,10 +0,0 @@
add_circt_unittest(CIRCTSMTTests
AttributeTest.cpp
QuantifierTest.cpp
TypeTest.cpp
)
target_link_libraries(CIRCTSMTTests
PRIVATE
CIRCTSMT
)

188
unittests/Dialect/SMT/QuantifierTest.cpp
View File

@ -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<SMTDialect>();
Location loc(UnknownLoc::get(&context));
OpBuilder builder(&context);
auto boolTy = BoolType::get(&context);
ExistsOp existsOp = builder.create<ExistsOp>(
loc, TypeRange{boolTy, boolTy},
[](OpBuilder &builder, Location loc, ValueRange boundVars) {
return builder.create<AndOp>(loc, boundVars);
},
std::nullopt,
[](OpBuilder &builder, Location loc, ValueRange boundVars) {
return boundVars;
},
/*weight=*/2);
SmallVector<char, 1024> 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<SMTDialect>();
Location loc(UnknownLoc::get(&context));
OpBuilder builder(&context);
auto boolTy = BoolType::get(&context);
ExistsOp existsOp = builder.create<ExistsOp>(
loc, TypeRange{boolTy, boolTy},
[](OpBuilder &builder, Location loc, ValueRange boundVars) {
return builder.create<AndOp>(loc, boundVars);
},
ArrayRef<StringRef>{"a", "b"}, nullptr, /*weight=*/0, /*noPattern=*/true);
SmallVector<char, 1024> 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<SMTDialect>();
Location loc(UnknownLoc::get(&context));
OpBuilder builder(&context);
auto boolTy = BoolType::get(&context);
ExistsOp existsOp = builder.create<ExistsOp>(
loc, TypeRange{boolTy, boolTy},
[](OpBuilder &builder, Location loc, ValueRange boundVars) {
return builder.create<AndOp>(loc, boundVars);
},
ArrayRef<StringRef>{"a", "b"});
SmallVector<char, 1024> 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<SMTDialect>();
Location loc(UnknownLoc::get(&context));
OpBuilder builder(&context);
auto boolTy = BoolType::get(&context);
ForallOp forallOp = builder.create<ForallOp>(
loc, TypeRange{boolTy, boolTy},
[](OpBuilder &builder, Location loc, ValueRange boundVars) {
return builder.create<AndOp>(loc, boundVars);
},
ArrayRef<StringRef>{"a", "b"},
[](OpBuilder &builder, Location loc, ValueRange boundVars) {
return boundVars;
},
/*weight=*/2);
SmallVector<char, 1024> 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<SMTDialect>();
Location loc(UnknownLoc::get(&context));
OpBuilder builder(&context);
auto boolTy = BoolType::get(&context);
ForallOp forallOp = builder.create<ForallOp>(
loc, TypeRange{boolTy, boolTy},
[](OpBuilder &builder, Location loc, ValueRange boundVars) {
return builder.create<AndOp>(loc, boundVars);
},
ArrayRef<StringRef>{"a", "b"}, nullptr, /*weight=*/0, /*noPattern=*/true);
SmallVector<char, 1024> 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<SMTDialect>();
Location loc(UnknownLoc::get(&context));
OpBuilder builder(&context);
auto boolTy = BoolType::get(&context);
ForallOp forallOp = builder.create<ForallOp>(
loc, TypeRange{boolTy, boolTy},
[](OpBuilder &builder, Location loc, ValueRange boundVars) {
return builder.create<AndOp>(loc, boundVars);
},
std::nullopt);
SmallVector<char, 1024> 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

32
unittests/Dialect/SMT/TypeTest.cpp
View File

@ -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<SMTDialect>();
Location loc(UnknownLoc::get(&context));
auto boolTy = BoolType::get(&context);
auto funcTy = SMTFuncType::getChecked(loc, ArrayRef<Type>{}, boolTy);
ASSERT_EQ(funcTy, Type());
context.getDiagEngine().registerHandler([&](Diagnostic &diag) {
ASSERT_STREQ(diag.str().c_str(), "domain must not be empty");
});
}
} // namespace