137 lines · plain
1// RUN: mlir-opt %s --transform-interpreter --split-input-file --verify-diagnostics2 3// CHECK-LABEL: @incorrect terminator4module attributes {transform.with_named_sequence} {5 transform.named_sequence @operands_not_one_to_one_with_vars(%arg0: !transform.any_op {transform.readonly}) {6 %param_as_param = transform.param.constant 42 -> !transform.param<i64>7 // expected-error@below {{op expected 'smt.yield' as terminator}}8 transform.smt.constrain_params(%param_as_param) : (!transform.param<i64>) -> () {9 ^bb0(%param_as_smt_var: !smt.int):10 transform.yield11 }12 transform.yield13 }14}15 16// -----17 18// CHECK-LABEL: @operands_not_one_to_one_with_vars19module attributes {transform.with_named_sequence} {20 transform.named_sequence @operands_not_one_to_one_with_vars(%arg0: !transform.any_op {transform.readonly}) {21 %param_as_param = transform.param.constant 42 -> !transform.param<i64>22 // expected-error@below {{must have the same number of block arguments as operands}}23 transform.smt.constrain_params(%param_as_param) : (!transform.param<i64>) -> () {24 ^bb0(%param_as_smt_var: !smt.int, %param_as_another_smt_var: !smt.int):25 }26 transform.yield27 }28}29 30// -----31 32// CHECK-LABEL: @constraint_not_using_smt_ops33module attributes {transform.with_named_sequence} {34 transform.named_sequence @constraint_not_using_smt_ops(%arg0: !transform.any_op {transform.readonly}) {35 %param_as_param = transform.param.constant 42 -> !transform.param<i64>36 // expected-error@below {{ops contained in region should belong to SMT-dialect}}37 transform.smt.constrain_params(%param_as_param) : (!transform.param<i64>) -> () {38 ^bb0(%param_as_smt_var: !smt.int):39 %c4 = arith.constant 4 : i3240 // This is the kind of thing one might think works:41 //arith.remsi %param_as_smt_var, %c4 : i3242 }43 transform.yield44 }45}46 47// -----48 49// CHECK-LABEL: @results_not_one_to_one_with_vars50module attributes {transform.with_named_sequence} {51 transform.named_sequence @results_not_one_to_one_with_vars(%arg0: !transform.any_op {transform.readonly}) {52 %param_as_param = transform.param.constant 42 -> !transform.param<i64>53 transform.smt.constrain_params(%param_as_param, %param_as_param) : (!transform.param<i64>, !transform.param<i64>) -> () {54 ^bb0(%param_as_smt_var: !smt.int, %param_as_another_smt_var: !smt.int):55 // expected-error@below {{expected terminator to have as many operands as the parent op has results}}56 smt.yield %param_as_smt_var : !smt.int57 }58 transform.yield59 }60}61 62// -----63 64// CHECK-LABEL: @non_smt_type_block_args65module attributes {transform.with_named_sequence} {66 transform.named_sequence @non_smt_type_block_args(%arg0: !transform.any_op {transform.readonly}) {67 %param_as_param = transform.param.constant 42 -> !transform.param<i8>68 // expected-error@below {{the type of block arg #0 is expected to be either a !smt.bool, a !smt.int, or a !smt.bv}}69 transform.smt.constrain_params(%param_as_param) : (!transform.param<i8>) -> (!transform.param<i8>) {70 ^bb0(%param_as_smt_var: !transform.param<i8>):71 smt.yield %param_as_smt_var : !transform.param<i8>72 }73 transform.yield74 }75}76 77 78// -----79 80// CHECK-LABEL: @mismatched_arg_type_bool81module attributes {transform.with_named_sequence} {82 transform.named_sequence @mismatched_arg_type_bool(%arg0: !transform.any_op {transform.readonly}) {83 %param_as_param = transform.param.constant 42 -> !transform.param<i64>84 // expected-error@below {{the type of block arg #0 is !smt.bool though the corresponding operand type ('!transform.param<i64>') is not wrapping i1}}85 transform.smt.constrain_params(%param_as_param) : (!transform.param<i64>) -> (!transform.param<i64>) {86 ^bb0(%param_as_smt_var: !smt.bool):87 smt.yield %param_as_smt_var : !smt.bool88 }89 transform.yield90 }91}92 93// -----94 95// CHECK-LABEL: @mismatched_arg_type_bitvector96module attributes {transform.with_named_sequence} {97 transform.named_sequence @mismatched_arg_type_bitvector(%arg0: !transform.any_op {transform.readonly}) {98 %param_as_param = transform.param.constant 42 -> !transform.param<i64>99 // expected-error@below {{the type of block arg #0 is '!smt.bv<8>' though the corresponding operand type ('!transform.param<i64>') is not wrapping an integer type of the same bitwidth}}100 transform.smt.constrain_params(%param_as_param) : (!transform.param<i64>) -> (!transform.param<i64>) {101 ^bb0(%param_as_smt_var: !smt.bv<8>):102 smt.yield %param_as_smt_var : !smt.bv<8>103 }104 transform.yield105 }106}107 108// -----109 110// CHECK-LABEL: @mismatched_result_type_bool111module attributes {transform.with_named_sequence} {112 transform.named_sequence @mismatched_result_type_bool(%arg0: !transform.any_op {transform.readonly}) {113 %param_as_param = transform.param.constant 1 -> !transform.param<i1>114 transform.smt.constrain_params(%param_as_param) : (!transform.param<i1>) -> (!transform.param<i64>) {115 ^bb0(%param_as_smt_var: !smt.bool):116 // expected-error@below {{the type of terminator operand #0 is !smt.bool though the corresponding result type ('!transform.param<i64>') is not wrapping i1}}117 smt.yield %param_as_smt_var : !smt.bool118 }119 transform.yield120 }121}122 123// -----124 125// CHECK-LABEL: @mismatched_result_type_bitvector126module attributes {transform.with_named_sequence} {127 transform.named_sequence @mismatched_result_type_bitvector(%arg0: !transform.any_op {transform.readonly}) {128 %param_as_param = transform.param.constant 42 -> !transform.param<i8>129 transform.smt.constrain_params(%param_as_param) : (!transform.param<i8>) -> (!transform.param<i64>) {130 ^bb0(%param_as_smt_var: !smt.bv<8>):131 // expected-error@below {{the type of terminator operand #0 is '!smt.bv<8>' though the corresponding result type ('!transform.param<i64>') is not wrapping an integer type of the same bitwidth}}132 smt.yield %param_as_smt_var : !smt.bv<8>133 }134 transform.yield135 }136}137