From 45eb0dd5eedf0f57da18fb370586fa440f5d4a18 Mon Sep 17 00:00:00 2001 From: Bea Healy Date: Wed, 8 Jan 2025 16:37:00 +0000 Subject: [PATCH 1/3] [SMT] Parse SMT bitvector width as signed --- include/circt/Dialect/SMT/SMTTypes.td | 2 +- lib/Dialect/SMT/SMTTypes.cpp | 2 +- test/Dialect/SMT/bitvector-errors.mlir | 13 ++++++++++--- 3 files changed, 12 insertions(+), 5 deletions(-) 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/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..61f695432797 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 @at_least_size_one(%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}} @@ -89,8 +96,8 @@ func.func @repeat_count_too_large(%arg0: !smt.bv<32>) { // ----- -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> +// expected-error @below {{integer value too large}} +// expected-error @below {{failed to parse BitVectorType parameter 'width' which is to be a `int64_t`}} +func.func @bitwidth_too_large(%arg0: !smt.bv<18446744073709551612>) { return } From bb8102ba94b9fc41d604c83bce98cc9386b67b40 Mon Sep 17 00:00:00 2001 From: Bea Healy Date: Wed, 8 Jan 2025 16:42:58 +0000 Subject: [PATCH 2/3] Update test func name --- test/Dialect/SMT/bitvector-errors.mlir | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/Dialect/SMT/bitvector-errors.mlir b/test/Dialect/SMT/bitvector-errors.mlir index 61f695432797..719513dce93c 100644 --- a/test/Dialect/SMT/bitvector-errors.mlir +++ b/test/Dialect/SMT/bitvector-errors.mlir @@ -8,7 +8,7 @@ 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 @at_least_size_one(%arg0: !smt.bv<-1>) { +func.func @positive_width(%arg0: !smt.bv<-1>) { return } From 25e9ba937799edee785581b21b97740893f21451 Mon Sep 17 00:00:00 2001 From: Bea Healy Date: Fri, 10 Jan 2025 12:45:19 +0000 Subject: [PATCH 3/3] Update max bitwidth check --- lib/Dialect/SMT/SMTOps.cpp | 4 ++-- test/Dialect/SMT/bitvector-errors.mlir | 8 ++++---- 2 files changed, 6 insertions(+), 6 deletions(-) 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/test/Dialect/SMT/bitvector-errors.mlir b/test/Dialect/SMT/bitvector-errors.mlir index 719513dce93c..51fb576faac6 100644 --- a/test/Dialect/SMT/bitvector-errors.mlir +++ b/test/Dialect/SMT/bitvector-errors.mlir @@ -89,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 } // ----- -// expected-error @below {{integer value too large}} -// expected-error @below {{failed to parse BitVectorType parameter 'width' which is to be a `int64_t`}} -func.func @bitwidth_too_large(%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 }