[SMT] Add arithmetic and bitwise operations (llvm#6805)

elhewaty · Mar 12, 2024 · 9bf7c33 · 9bf7c33
1 parent 7e0ae45
commit 9bf7c33
Show file tree

Hide file tree

Showing 3 changed files with 83 additions and 2 deletions.
diff --git 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
@@ -61,4 +61,50 @@ def BVConstantOp : SMTBVOp<"constant", [
   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">;
+
 #endif // CIRCT_DIALECT_SMT_SMTBITVECTOROPS_TD
diff --git 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
 }