113 lines · plain
1// RUN: mlir-opt %s --split-input-file --verify-diagnostics2 3// expected-error @below {{bit-vector must have at least a width of one}}4func.func @at_least_size_one(%arg0: !smt.bv<0>) {5 return6}7 8// -----9 10// expected-error @below {{bit-vector must have at least a width of one}}11func.func @positive_width(%arg0: !smt.bv<-1>) {12 return13}14 15// -----16 17func.func @attr_type_and_return_type_match() {18 // expected-error @below {{inferred type(s) '!smt.bv<1>' are incompatible with return type(s) of operation '!smt.bv<32>'}}19 // expected-error @below {{failed to infer returned types}}20 %c0_bv32 = "smt.bv.constant"() <{value = #smt.bv<0> : !smt.bv<1>}> : () -> !smt.bv<32>21 return22}23 24// -----25 26func.func @invalid_bitvector_attr() {27 // expected-error @below {{explicit bit-vector type required}}28 smt.bv.constant #smt.bv<5>29}30 31// -----32 33func.func @invalid_bitvector_attr() {34 // expected-error @below {{integer value out of range for given bit-vector type}}35 smt.bv.constant #smt.bv<32> : !smt.bv<2>36}37 38// -----39 40func.func @invalid_bitvector_attr() {41 // expected-error @below {{integer value out of range for given bit-vector type}}42 smt.bv.constant #smt.bv<-4> : !smt.bv<2>43}44 45// -----46 47func.func @extraction(%arg0: !smt.bv<32>) {48 // 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}}49 smt.bv.extract %arg0 from 20 : (!smt.bv<32>) -> !smt.bv<16>50 return51}52 53// -----54 55func.func @concat(%arg0: !smt.bv<32>) {56 // expected-error @below {{inferred type(s) '!smt.bv<64>' are incompatible with return type(s) of operation '!smt.bv<33>'}}57 // expected-error @below {{failed to infer returned types}}58 "smt.bv.concat"(%arg0, %arg0) {} : (!smt.bv<32>, !smt.bv<32>) -> !smt.bv<33>59 return60}61 62// -----63 64func.func @repeat_result_type_no_multiple_of_input_type(%arg0: !smt.bv<32>) {65 // expected-error @below {{result bit-vector width must be a multiple of the input bit-vector width}}66 "smt.bv.repeat"(%arg0) : (!smt.bv<32>) -> !smt.bv<65>67 return68}69 70// -----71 72func.func @repeat_negative_count(%arg0: !smt.bv<32>) {73 // expected-error @below {{integer must be positive}}74 smt.bv.repeat -2 times %arg0 : !smt.bv<32>75 return76}77 78// -----79 80// The parser has to extract the bit-width of the input and thus we need to81// test that this is handled correctly in the parser, we cannot just rely on the82// verifier.83func.func @repeat_wrong_input_type(%arg0: !smt.bool) {84 // expected-error @below {{input must have bit-vector type}}85 smt.bv.repeat 2 times %arg0 : !smt.bool86 return87}88 89// -----90 91func.func @repeat_count_too_large(%arg0: !smt.bv<32>) {92 // expected-error @below {{integer must fit into 63 bits}}93 smt.bv.repeat 18446744073709551617 times %arg0 : !smt.bv<32>94 return95}96 97// -----98 99func.func @repeat_result_type_bitwidth_too_large(%arg0: !smt.bv<9223372036854775807>) {100 // expected-error @below {{result bit-width (provided integer times bit-width of the input type) must fit into 63 bits}}101 smt.bv.repeat 2 times %arg0 : !smt.bv<9223372036854775807>102 return103}104 105// -----106 107func.func @invalid_bv2int_signedness() {108 %c5_bv32 = smt.bv.constant #smt.bv<5> : !smt.bv<32>109 // expected-error @below {{expected ':'}}110 %bv2int = smt.bv2int %c5_bv32 unsigned : !smt.bv<32>111 return112}113