circt/test/Dialect/SMT/bitvector-errors.mlir

97 lines
2.9 KiB
MLIR

// RUN: circt-opt %s --split-input-file --verify-diagnostics
// expected-error @below {{bit-vector must have at least a width of one}}
func.func @at_least_size_one(%arg0: !smt.bv<0>) {
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}}
%c0_bv32 = "smt.bv.constant"() <{value = #smt.bv<0> : !smt.bv<1>}> : () -> !smt.bv<32>
return
}
// -----
func.func @invalid_bitvector_attr() {
// expected-error @below {{explicit bit-vector type required}}
smt.bv.constant #smt.bv<5>
}
// -----
func.func @invalid_bitvector_attr() {
// expected-error @below {{integer value out of range for given bit-vector type}}
smt.bv.constant #smt.bv<32> : !smt.bv<2>
}
// -----
func.func @invalid_bitvector_attr() {
// expected-error @below {{integer value out of range for given bit-vector type}}
smt.bv.constant #smt.bv<-4> : !smt.bv<2>
}
// -----
func.func @extraction(%arg0: !smt.bv<32>) {
// expected-error @below {{range to be extracted is too big, expected range starting at index 20 of length 16 requires input width of at least 36, but the input width is only 32}}
smt.bv.extract %arg0 from 20 : (!smt.bv<32>) -> !smt.bv<16>
return
}
// -----
func.func @concat(%arg0: !smt.bv<32>) {
// expected-error @below {{inferred type(s) '!smt.bv<64>' are incompatible with return type(s) of operation '!smt.bv<33>'}}
// expected-error @below {{failed to infer returned types}}
"smt.bv.concat"(%arg0, %arg0) {} : (!smt.bv<32>, !smt.bv<32>) -> !smt.bv<33>
return
}
// -----
func.func @repeat_result_type_no_multiple_of_input_type(%arg0: !smt.bv<32>) {
// expected-error @below {{result bit-vector width must be a multiple of the input bit-vector width}}
"smt.bv.repeat"(%arg0) : (!smt.bv<32>) -> !smt.bv<65>
return
}
// -----
func.func @repeat_negative_count(%arg0: !smt.bv<32>) {
// expected-error @below {{integer must be positive}}
smt.bv.repeat -2 times %arg0 : !smt.bv<32>
return
}
// -----
// The parser has to extract the bit-width of the input and thus we need to
// test that this is handled correctly in the parser, we cannot just rely on the
// verifier.
func.func @repeat_wrong_input_type(%arg0: !smt.bool) {
// expected-error @below {{input must have bit-vector type}}
smt.bv.repeat 2 times %arg0 : !smt.bool
return
}
// -----
func.func @repeat_count_too_large(%arg0: !smt.bv<32>) {
// expected-error @below {{integer must fit into 64 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>
return
}