diff --git a/include/circt/Dialect/SMT/SMTTypes.td b/include/circt/Dialect/SMT/SMTTypes.td index 18c236018872..2aa82bf5d5e5 100644 --- 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 index 94c721189244..ad60501d97f2 100644 --- 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 index 22e91abbc98b..d67e2a1e9356 100644 --- 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 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 index 14f7f29666d0..51fb576faac6 100644 --- 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 }