From 9bf7c33ee586085cb58ee5d08c3d548a60bb76d6 Mon Sep 17 00:00:00 2001 From: Martin Erhart Date: Tue, 12 Mar 2024 09:38:54 +0100 Subject: [PATCH] [SMT] Add arithmetic and bitwise operations (#6805) --- include/circt/Dialect/SMT/CMakeLists.txt | 4 +- include/circt/Dialect/SMT/SMTBitVectorOps.td | 46 ++++++++++++++++++++ test/Dialect/SMT/bitvectors.mlir | 35 +++++++++++++++ 3 files changed, 83 insertions(+), 2 deletions(-) diff --git a/include/circt/Dialect/SMT/CMakeLists.txt b/include/circt/Dialect/SMT/CMakeLists.txt index 1e50abc24992..e914462fa7c8 100644 --- a/include/circt/Dialect/SMT/CMakeLists.txt +++ b/include/circt/Dialect/SMT/CMakeLists.txt @@ -1,6 +1,6 @@ add_circt_dialect(SMT smt) -add_circt_doc(SMTOps Dialects/SMTOps -gen-op-doc) -add_circt_doc(SMTTypes Dialects/SMTTypes -gen-typedef-doc -dialect 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) diff --git a/include/circt/Dialect/SMT/SMTBitVectorOps.td b/include/circt/Dialect/SMT/SMTBitVectorOps.td index c2a352bb0e6c..3c8f09901a45 100644 --- a/include/circt/Dialect/SMT/SMTBitVectorOps.td +++ b/include/circt/Dialect/SMT/SMTBitVectorOps.td @@ -61,4 +61,50 @@ def BVConstantOp : SMTBVOp<"constant", [ let hasFolder = true; } +class BVArithmeticOrBitwiseOp : + SMTBVOp { + let summary = "equivalent to bv" # mnemonic # " in SMT-LIB"; + let description = "This operation performs " # desc # [{. The semantics are + equivalent to the `bv}] # mnemonic # [{` operator defined in the SMT-LIB 2.6 + standard. More precisely in the [theory of FixedSizeBitVectors](https://smtlib.cs.uiowa.edu/Theories/FixedSizeBitVectors.smt2) + and the [QF_BV logic](https://smtlib.cs.uiowa.edu/Logics/QF_BV.smt2) + describing closed quantifier-free formulas over the theory of fixed-size + bit-vectors. + }]; + + let results = (outs BitVectorType:$result); +} + +class BinaryBVOp : + BVArithmeticOrBitwiseOp { + let arguments = (ins BitVectorType:$lhs, BitVectorType:$rhs); + let assemblyFormat = "$lhs `,` $rhs attr-dict `:` qualified(type($result))"; +} + +class UnaryBVOp : + BVArithmeticOrBitwiseOp { + let arguments = (ins BitVectorType:$input); + let assemblyFormat = "$input attr-dict `:` qualified(type($result))"; +} + +def BVNotOp : UnaryBVOp<"not", "bitwise negation">; +def BVNegOp : UnaryBVOp<"neg", "two's complement unary minus">; + +def BVAndOp : BinaryBVOp<"and", "bitwise AND">; +def BVOrOp : BinaryBVOp<"or", "bitwise OR">; +def BVXOrOp : BinaryBVOp<"xor", "bitwise exclusive OR">; + +def BVAddOp : BinaryBVOp<"add", "addition">; +def BVMulOp : BinaryBVOp<"mul", "multiplication">; +def BVUDivOp : BinaryBVOp<"udiv", "unsigned division (rounded towards zero)">; +def BVSDivOp : BinaryBVOp<"sdiv", "two's complement signed division">; +def BVURemOp : BinaryBVOp<"urem", "unsigned remainder">; +def BVSRemOp : BinaryBVOp<"srem", + "two's complement signed remainder (sign follows dividend)">; +def BVSModOp : BinaryBVOp<"smod", + "two's complement signed remainder (sign follows divisor)">; +def BVShlOp : BinaryBVOp<"shl", "shift left">; +def BVLShrOp : BinaryBVOp<"lshr", "logical shift right">; +def BVAShrOp : BinaryBVOp<"ashr", "arithmetic shift right">; + #endif // CIRCT_DIALECT_SMT_SMTBITVECTOROPS_TD diff --git a/test/Dialect/SMT/bitvectors.mlir b/test/Dialect/SMT/bitvectors.mlir index 15d07ef197d5..1bfba1d53c4a 100644 --- a/test/Dialect/SMT/bitvectors.mlir +++ b/test/Dialect/SMT/bitvectors.mlir @@ -9,5 +9,40 @@ func.func @bitvectors() { // CHECK: %c-1_bv8 = smt.bv.constant #smt.bv<-1> : !smt.bv<8> %c-1_bv8 = smt.bv.constant #smt.bv<-1> : !smt.bv<8> + // CHECK: [[C0:%.+]] = smt.bv.constant #smt.bv<0> : !smt.bv<32> + %c = smt.bv.constant #smt.bv<0> : !smt.bv<32> + + // CHECK: %{{.*}} = smt.bv.neg [[C0]] {smt.some_attr} : !smt.bv<32> + %0 = smt.bv.neg %c {smt.some_attr} : !smt.bv<32> + // CHECK: %{{.*}} = smt.bv.add [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32> + %1 = smt.bv.add %c, %c {smt.some_attr} : !smt.bv<32> + // CHECK: %{{.*}} = smt.bv.mul [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32> + %3 = smt.bv.mul %c, %c {smt.some_attr} : !smt.bv<32> + // CHECK: %{{.*}} = smt.bv.urem [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32> + %4 = smt.bv.urem %c, %c {smt.some_attr} : !smt.bv<32> + // CHECK: %{{.*}} = smt.bv.srem [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32> + %5 = smt.bv.srem %c, %c {smt.some_attr} : !smt.bv<32> + // CHECK: %{{.*}} = smt.bv.smod [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32> + %7 = smt.bv.smod %c, %c {smt.some_attr} : !smt.bv<32> + // CHECK: %{{.*}} = smt.bv.shl [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32> + %8 = smt.bv.shl %c, %c {smt.some_attr} : !smt.bv<32> + // CHECK: %{{.*}} = smt.bv.lshr [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32> + %9 = smt.bv.lshr %c, %c {smt.some_attr} : !smt.bv<32> + // CHECK: %{{.*}} = smt.bv.ashr [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32> + %10 = smt.bv.ashr %c, %c {smt.some_attr} : !smt.bv<32> + // CHECK: %{{.*}} = smt.bv.udiv [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32> + %11 = smt.bv.udiv %c, %c {smt.some_attr} : !smt.bv<32> + // CHECK: %{{.*}} = smt.bv.sdiv [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32> + %12 = smt.bv.sdiv %c, %c {smt.some_attr} : !smt.bv<32> + + // CHECK: %{{.*}} = smt.bv.not [[C0]] {smt.some_attr} : !smt.bv<32> + %13 = smt.bv.not %c {smt.some_attr} : !smt.bv<32> + // CHECK: %{{.*}} = smt.bv.and [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32> + %14 = smt.bv.and %c, %c {smt.some_attr} : !smt.bv<32> + // CHECK: %{{.*}} = smt.bv.or [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32> + %15 = smt.bv.or %c, %c {smt.some_attr} : !smt.bv<32> + // CHECK: %{{.*}} = smt.bv.xor [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32> + %16 = smt.bv.xor %c, %c {smt.some_attr} : !smt.bv<32> + return }