[SMT] Add bv2int op (#8049)

llvm · Jan 10, 2025 · c49c1c3 · c49c1c3
1 parent 00b68e6
commit c49c1c3
Show file tree

Hide file tree

Showing 12 changed files with 108 additions and 7 deletions.
diff --git a/include/circt/Dialect/SMT/SMTBitVectorOps.td b/include/circt/Dialect/SMT/SMTBitVectorOps.td
@@ -238,4 +238,19 @@ def RepeatOp : SMTBVOp<"repeat", [Pure]> {
   }];
 }
 
+def BV2IntOp : SMTOp<"bv2int", [Pure]> {
+  let summary = "Convert an SMT bit-vector to an SMT integer.";
+  let description = [{
+    Adapted from the Z3 documentation:
+    Create an integer from the bit-vector argument `input`.
+    If `is_signed` is false, then the bit-vector `input` is treated as
+    unsigned. So the result is non-negative and in the range [0..2^N-1], where
+    N are the number of bits in `input`. If `is_signed` is true, `input` is
+    treated as a signed bit-vector.
+  }];
+  let arguments = (ins BitVectorType:$input, UnitAttr:$is_signed);
+  let results = (outs IntType:$result);
+  let assemblyFormat = [{$input (`signed` $is_signed^)? attr-dict `:` qualified(type($input))}];
+}
+
 #endif // CIRCT_DIALECT_SMT_SMTBITVECTOROPS_TD
diff --git a/include/circt/Dialect/SMT/SMTVisitors.h b/include/circt/Dialect/SMT/SMTVisitors.h
@@ -36,7 +36,7 @@ class SMTOpVisitor {
             // Bit-vector bitwise
             BVNotOp, BVAndOp, BVOrOp, BVXOrOp,
             // Other bit-vector ops
-            ConcatOp, ExtractOp, RepeatOp, BVCmpOp,
+            ConcatOp, ExtractOp, RepeatOp, BVCmpOp, BV2IntOp,
             // Int arithmetic
             IntAddOp, IntMulOp, IntSubOp, IntDivOp, IntModOp, IntCmpOp,
             Int2BVOp,
@@ -106,6 +106,7 @@ class SMTOpVisitor {
   HANDLE(ExtractOp, Unhandled);
   HANDLE(RepeatOp, Unhandled);
   HANDLE(BVCmpOp, Unhandled);
+  HANDLE(BV2IntOp, Unhandled);
 
   // Int arithmetic
   HANDLE(IntAddOp, Unhandled);

diff --git a/integration_test/Dialect/SMT/basic.mlir b/integration_test/Dialect/SMT/basic.mlir
@@ -205,6 +205,40 @@ func.func @entry() {
     smt.yield
   }
 
+  // CHECK: unsat
+  // CHECK: Res: -1
+  smt.solver () : () -> () {
+    %c4 = smt.int.constant 4
+    %c4_bv16 = smt.bv.constant #smt.bv<4> : !smt.bv<16>
+    %bv2int = smt.bv2int %c4_bv16 : !smt.bv<16>
+    %eq = smt.distinct %c4, %bv2int : !smt.int
+    func.call @check(%eq) : (!smt.bool) -> ()
+    smt.yield
+  }
+
+  // CHECK: unsat
+  // CHECK: Res: -1
+  smt.solver () : () -> () {
+    %c-4 = smt.int.constant -4
+    %c-4_bv16 = smt.bv.constant #smt.bv<-4> : !smt.bv<16>
+    %bv2int = smt.bv2int %c-4_bv16 signed : !smt.bv<16>
+    %eq = smt.distinct %c-4, %bv2int : !smt.int
+    func.call @check(%eq) : (!smt.bool) -> ()
+    smt.yield
+  }
+
+  // Check that unsigned conversion actually produces unsigned result
+  // CHECK: unsat
+  // CHECK: Res: -1
+  smt.solver () : () -> () {
+    %c-4 = smt.int.constant -4
+    %c-4_bv16 = smt.bv.constant #smt.bv<-4> : !smt.bv<16>
+    %bv2int = smt.bv2int %c-4_bv16 : !smt.bv<16>
+    %eq = smt.eq %c-4, %bv2int : !smt.int
+    func.call @check(%eq) : (!smt.bool) -> ()
+    smt.yield
+  }
+
   return
 }
 

diff --git a/lib/Conversion/SMTToZ3LLVM/LowerSMTToZ3LLVM.cpp b/lib/Conversion/SMTToZ3LLVM/LowerSMTToZ3LLVM.cpp
@@ -1211,6 +1211,27 @@ struct Int2BVOpLowering : public SMTLoweringPattern<Int2BVOp> {
   }
 };
 
+/// Lower `smt.bv2int` operations to the following Z3 API function call.
+/// ```
+/// Z3_ast Z3_API Z3_mk_bv2int(Z3_context c, Z3_ast t1, bool is_signed)
+/// ```
+struct BV2IntOpLowering : public SMTLoweringPattern<BV2IntOp> {
+  using SMTLoweringPattern::SMTLoweringPattern;
+
+  LogicalResult
+  matchAndRewrite(BV2IntOp op, OpAdaptor adaptor,
+                  ConversionPatternRewriter &rewriter) const final {
+    // FIXME: ideally we don't want to use i1 here, since bools can sometimes be
+    // compiled to wider widths in LLVM
+    Value isSignedConst = rewriter.create<LLVM::ConstantOp>(
+        op->getLoc(), rewriter.getI1Type(), op.getIsSigned());
+    rewriter.replaceOp(op,
+                       buildPtrAPICall(rewriter, op.getLoc(), "Z3_mk_bv2int",
+                                       {adaptor.getInput(), isSignedConst}));
+    return success();
+  }
+};
+
 /// Lower `smt.bv.cmp` operations to one of the following Z3 API function calls,
 /// performing two's complement comparison, depending on the predicate
 /// attribute.
@@ -1482,8 +1503,9 @@ void circt::populateSMTToZ3LLVMConversionPatterns(
                RepeatOpLowering, ExtractOpLowering, BoolConstantOpLowering,
                IntConstantOpLowering, ArrayBroadcastOpLowering, BVCmpOpLowering,
                IntCmpOpLowering, IntAbsOpLowering, Int2BVOpLowering,
-               QuantifierLowering<ForallOp>, QuantifierLowering<ExistsOp>>(
-      converter, patterns.getContext(), globals, options);
+               BV2IntOpLowering, QuantifierLowering<ForallOp>,
+               QuantifierLowering<ExistsOp>>(converter, patterns.getContext(),
+                                             globals, options);
 }
 
 void LowerSMTToZ3LLVMPass::runOnOperation() {

diff --git a/lib/Dialect/SMT/CMakeLists.txt b/lib/Dialect/SMT/CMakeLists.txt
@@ -16,6 +16,7 @@ add_circt_dialect_library(CIRCTSMT
   Support
 
   LINK_LIBS PUBLIC
+  CIRCTSupport
   MLIRIR
   MLIRInferTypeOpInterface
   MLIRSideEffectInterfaces

diff --git a/lib/Dialect/SMT/SMTOps.cpp b/lib/Dialect/SMT/SMTOps.cpp
@@ -7,6 +7,7 @@
 //===----------------------------------------------------------------------===//
 
 #include "circt/Dialect/SMT/SMTOps.h"
+#include "circt/Support/CustomDirectiveImpl.h"
 #include "mlir/IR/Builders.h"
 #include "mlir/IR/OpImplementation.h"
 #include "llvm/ADT/APSInt.h"

diff --git a/lib/Target/ExportSMTLIB/ExportSMTLIB.cpp b/lib/Target/ExportSMTLIB/ExportSMTLIB.cpp
@@ -602,9 +602,8 @@ struct StatementVisitor
                                     mlir::raw_indented_ostream &stream,
                                     ValueMap &valueMap) {
     // Ignore operations which are handled in the Expression Visitor.
-    if (isa<smt::Int2BVOp>(op))
-      return op->emitError(
-          "int2bv operations are not supported for SMTLIB emission");
+    if (isa<smt::Int2BVOp, BV2IntOp>(op))
+      return op->emitError("operation not supported for SMTLIB emission");
 
     return success();
   }

diff --git a/test/Conversion/SMTToZ3LLVM/smt-to-z3-llvm.mlir b/test/Conversion/SMTToZ3LLVM/smt-to-z3-llvm.mlir
@@ -384,6 +384,13 @@ func.func @test(%arg0: i32) {
     // CHECK: llvm.call @Z3_mk_int2bv({{%[0-9a-zA-Z_]+}}, [[WIDTHCONST]], [[C123]]) : (!llvm.ptr, i32, !llvm.ptr) -> !llvm.ptr
     smt.int2bv %10 : !smt.bv<4>
 
+    // CHECK: [[UNSIGNEDCONST:%.+]] = llvm.mlir.constant(false) : i1
+    // CHECK: llvm.call @Z3_mk_bv2int({{%[0-9a-zA-Z_]+}}, [[BV0]], [[UNSIGNEDCONST]]) : (!llvm.ptr, !llvm.ptr, i1) -> !llvm.ptr
+    smt.bv2int %c0_bv4 : !smt.bv<4>
+    // CHECK: [[SIGNEDCONST:%.+]] = llvm.mlir.constant(true) : i1
+    // CHECK: llvm.call @Z3_mk_bv2int({{%[0-9a-zA-Z_]+}}, [[BV0]], [[SIGNEDCONST]]) : (!llvm.ptr, !llvm.ptr, i1) -> !llvm.ptr
+    smt.bv2int %c0_bv4 signed : !smt.bv<4>
+
     // CHECK: [[C0:%.+]] = llvm.mlir.constant(0 : i32)
     // CHECK: [[C2:%.+]] = llvm.mlir.constant(2 : i32)
     // CHECK: [[ZERO:%.+]] = llvm.mlir.zero : !llvm.ptr

diff --git a/test/Dialect/SMT/bitvector-errors.mlir b/test/Dialect/SMT/bitvector-errors.mlir
@@ -101,3 +101,12 @@ func.func @repeat_result_type_bitwidth_too_large(%arg0: !smt.bv<9223372036854775
   smt.bv.repeat 2 times %arg0 : !smt.bv<9223372036854775807>
   return
 }
+
+// -----
+
+func.func @invalid_bv2int_signedness() {
+  %c5_bv32 = smt.bv.constant #smt.bv<5> : !smt.bv<32>
+  // expected-error @below {{expected ':'}}
+  %bv2int = smt.bv2int %c5_bv32 unsigned : !smt.bv<32>
+  return
+}
diff --git a/test/Dialect/SMT/bitvectors.mlir b/test/Dialect/SMT/bitvectors.mlir
@@ -72,5 +72,10 @@ func.func @bitvectors() {
   // CHECK: %{{.*}} = smt.bv.repeat 2 times [[C0]] {smt.some_attr} : !smt.bv<32>
   %27 = smt.bv.repeat 2 times %c {smt.some_attr} : !smt.bv<32>
 
+  // CHECK: %{{.*}} = smt.bv2int [[C0]] {smt.some_attr} : !smt.bv<32>
+  %29 = smt.bv2int %c {smt.some_attr} : !smt.bv<32>
+  // CHECK: %{{.*}} = smt.bv2int [[C0]] signed {smt.some_attr} : !smt.bv<32>
+  %28 = smt.bv2int %c signed {smt.some_attr} : !smt.bv<32>
+
   return
 }
diff --git a/test/Target/ExportSMTLIB/bitvector-errors.mlir b/test/Target/ExportSMTLIB/bitvector-errors.mlir
@@ -0,0 +1,7 @@
+// RUN: circt-translate --export-smtlib %s --split-input-file --verify-diagnostics
+
+smt.solver () : () -> () {
+  %0 = smt.bv.constant #smt.bv<5> : !smt.bv<16>
+  // expected-error @below {{operation not supported for SMTLIB emission}}
+  %1 = smt.bv2int %0 signed : !smt.bv<16>
+}
diff --git a/test/Target/ExportSMTLIB/integer-errors.mlir b/test/Target/ExportSMTLIB/integer-errors.mlir
@@ -2,6 +2,6 @@
 
 smt.solver () : () -> () {
   %0 = smt.int.constant 5
-  // expected-error @below {{int2bv operations are not supported for SMTLIB emission}}
+  // expected-error @below {{operation not supported for SMTLIB emission}}
   %1 = smt.int2bv %0 : !smt.bv<4>
 }