[SMT] Parse SMT bitvector width as signed (#8042)

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

Hide file tree

Showing 4 changed files with 15 additions and 8 deletions.
diff --git a/include/circt/Dialect/SMT/SMTTypes.td b/include/circt/Dialect/SMT/SMTTypes.td
@@ -39,7 +39,7 @@ def BitVectorType : SMTTypeDef<"BitVector"> {
     The bit-width must be strictly greater than zero.
   }];
 
-  let parameters = (ins "uint64_t":$width);
+  let parameters = (ins "int64_t":$width);
   let assemblyFormat = "`<` $width `>`";
 
   let genVerifyDecl = true;

diff --git a/lib/Dialect/SMT/SMTOps.cpp b/lib/Dialect/SMT/SMTOps.cpp
@@ -234,8 +234,8 @@ ParseResult RepeatOp::parse(OpAsmParser &parser, OperationState &result) {
     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 'uint64_t' parameter in 'BitVectorType'
-  const unsigned maxBw = 64;
+  // 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";

diff --git a/lib/Dialect/SMT/SMTTypes.cpp b/lib/Dialect/SMT/SMTTypes.cpp
@@ -41,7 +41,7 @@ bool smt::isAnySMTValueType(Type type) {
 
 LogicalResult
 BitVectorType::verify(function_ref<InFlightDiagnostic()> emitError,
-                      uint64_t width) {
+                      int64_t width) {
   if (width <= 0U)
     return emitError() << "bit-vector must have at least a width of one";
   return success();

diff --git a/test/Dialect/SMT/bitvector-errors.mlir b/test/Dialect/SMT/bitvector-errors.mlir
@@ -7,6 +7,13 @@ func.func @at_least_size_one(%arg0: !smt.bv<0>) {
 
 // -----
 
+// expected-error @below {{bit-vector must have at least a width of one}}
+func.func @positive_width(%arg0: !smt.bv<-1>) {
+  return
+}
+
+// -----
+
 func.func @attr_type_and_return_type_match() {
   // expected-error @below {{inferred type(s) '!smt.bv<1>' are incompatible with return type(s) of operation '!smt.bv<32>'}}
   // expected-error @below {{failed to infer returned types}}
@@ -82,15 +89,15 @@ func.func @repeat_wrong_input_type(%arg0: !smt.bool) {
 // -----
 
 func.func @repeat_count_too_large(%arg0: !smt.bv<32>) {
-  // expected-error @below {{integer must fit into 64 bits}}
+  // expected-error @below {{integer must fit into 63 bits}}
   smt.bv.repeat 18446744073709551617 times %arg0 : !smt.bv<32>
   return
 }
 
 // -----
 
-func.func @repeat_result_type_bitwidth_too_large(%arg0: !smt.bv<18446744073709551612>) {
-  // expected-error @below {{result bit-width (provided integer times bit-width of the input type) must fit into 64 bits}}
-  smt.bv.repeat 2 times %arg0 : !smt.bv<18446744073709551612>
+func.func @repeat_result_type_bitwidth_too_large(%arg0: !smt.bv<9223372036854775807>) {
+  // expected-error @below {{result bit-width (provided integer times bit-width of the input type) must fit into 63 bits}}
+  smt.bv.repeat 2 times %arg0 : !smt.bv<9223372036854775807>
   return
 }