82 lines · plain
1// RUN: mlir-opt %s --verify-roundtrip | FileCheck %s2 3// CHECK-LABEL: func @bitvectors4func.func @bitvectors() {5 // CHECK: %c5_bv32 = smt.bv.constant #smt.bv<5> : !smt.bv<32> {smt.some_attr}6 %c5_bv32 = smt.bv.constant #smt.bv<5> : !smt.bv<32> {smt.some_attr}7 // CHECK: %c92_bv8 = smt.bv.constant #smt.bv<92> : !smt.bv<8> {smt.some_attr}8 %c92_bv8 = smt.bv.constant #smt.bv<0x5c> : !smt.bv<8> {smt.some_attr}9 // CHECK: %c-1_bv8 = smt.bv.constant #smt.bv<-1> : !smt.bv<8>10 %c-1_bv8 = smt.bv.constant #smt.bv<-1> : !smt.bv<8>11 // CHECK: %c-1_bv1{{(_[0-9]+)?}} = smt.bv.constant #smt.bv<-1> : !smt.bv<1>12 %c-1_bv1_neg = smt.bv.constant #smt.bv<-1> : !smt.bv<1>13 // CHECK: %c-1_bv1{{(_[0-9]+)?}} = smt.bv.constant #smt.bv<-1> : !smt.bv<1>14 %c-1_bv1_pos = smt.bv.constant #smt.bv<1> : !smt.bv<1>15 16 // CHECK: [[C0:%.+]] = smt.bv.constant #smt.bv<0> : !smt.bv<32>17 %c = smt.bv.constant #smt.bv<0> : !smt.bv<32>18 19 // CHECK: %{{.*}} = smt.bv.neg [[C0]] {smt.some_attr} : !smt.bv<32>20 %0 = smt.bv.neg %c {smt.some_attr} : !smt.bv<32>21 // CHECK: %{{.*}} = smt.bv.add [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>22 %1 = smt.bv.add %c, %c {smt.some_attr} : !smt.bv<32>23 // CHECK: %{{.*}} = smt.bv.mul [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>24 %3 = smt.bv.mul %c, %c {smt.some_attr} : !smt.bv<32>25 // CHECK: %{{.*}} = smt.bv.urem [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>26 %4 = smt.bv.urem %c, %c {smt.some_attr} : !smt.bv<32>27 // CHECK: %{{.*}} = smt.bv.srem [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>28 %5 = smt.bv.srem %c, %c {smt.some_attr} : !smt.bv<32>29 // CHECK: %{{.*}} = smt.bv.smod [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>30 %7 = smt.bv.smod %c, %c {smt.some_attr} : !smt.bv<32>31 // CHECK: %{{.*}} = smt.bv.shl [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>32 %8 = smt.bv.shl %c, %c {smt.some_attr} : !smt.bv<32>33 // CHECK: %{{.*}} = smt.bv.lshr [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>34 %9 = smt.bv.lshr %c, %c {smt.some_attr} : !smt.bv<32>35 // CHECK: %{{.*}} = smt.bv.ashr [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>36 %10 = smt.bv.ashr %c, %c {smt.some_attr} : !smt.bv<32>37 // CHECK: %{{.*}} = smt.bv.udiv [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>38 %11 = smt.bv.udiv %c, %c {smt.some_attr} : !smt.bv<32>39 // CHECK: %{{.*}} = smt.bv.sdiv [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>40 %12 = smt.bv.sdiv %c, %c {smt.some_attr} : !smt.bv<32>41 42 // CHECK: %{{.*}} = smt.bv.not [[C0]] {smt.some_attr} : !smt.bv<32>43 %13 = smt.bv.not %c {smt.some_attr} : !smt.bv<32>44 // CHECK: %{{.*}} = smt.bv.and [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>45 %14 = smt.bv.and %c, %c {smt.some_attr} : !smt.bv<32>46 // CHECK: %{{.*}} = smt.bv.or [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>47 %15 = smt.bv.or %c, %c {smt.some_attr} : !smt.bv<32>48 // CHECK: %{{.*}} = smt.bv.xor [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>49 %16 = smt.bv.xor %c, %c {smt.some_attr} : !smt.bv<32>50 51 // CHECK: %{{.*}} = smt.bv.cmp slt [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>52 %17 = smt.bv.cmp slt %c, %c {smt.some_attr} : !smt.bv<32>53 // CHECK: %{{.*}} = smt.bv.cmp sle [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>54 %18 = smt.bv.cmp sle %c, %c {smt.some_attr} : !smt.bv<32>55 // CHECK: %{{.*}} = smt.bv.cmp sgt [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>56 %19 = smt.bv.cmp sgt %c, %c {smt.some_attr} : !smt.bv<32>57 // CHECK: %{{.*}} = smt.bv.cmp sge [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>58 %20 = smt.bv.cmp sge %c, %c {smt.some_attr} : !smt.bv<32>59 // CHECK: %{{.*}} = smt.bv.cmp ult [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>60 %21 = smt.bv.cmp ult %c, %c {smt.some_attr} : !smt.bv<32>61 // CHECK: %{{.*}} = smt.bv.cmp ule [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>62 %22 = smt.bv.cmp ule %c, %c {smt.some_attr} : !smt.bv<32>63 // CHECK: %{{.*}} = smt.bv.cmp ugt [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>64 %23 = smt.bv.cmp ugt %c, %c {smt.some_attr} : !smt.bv<32>65 // CHECK: %{{.*}} = smt.bv.cmp uge [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>66 %24 = smt.bv.cmp uge %c, %c {smt.some_attr} : !smt.bv<32>67 68 // CHECK: %{{.*}} = smt.bv.concat [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>, !smt.bv<32>69 %25 = smt.bv.concat %c, %c {smt.some_attr} : !smt.bv<32>, !smt.bv<32>70 // CHECK: %{{.*}} = smt.bv.extract [[C0]] from 8 {smt.some_attr} : (!smt.bv<32>) -> !smt.bv<16>71 %26 = smt.bv.extract %c from 8 {smt.some_attr} : (!smt.bv<32>) -> !smt.bv<16>72 // CHECK: %{{.*}} = smt.bv.repeat 2 times [[C0]] {smt.some_attr} : !smt.bv<32>73 %27 = smt.bv.repeat 2 times %c {smt.some_attr} : !smt.bv<32>74 75 // CHECK: %{{.*}} = smt.bv2int [[C0]] {smt.some_attr} : !smt.bv<32>76 %29 = smt.bv2int %c {smt.some_attr} : !smt.bv<32>77 // CHECK: %{{.*}} = smt.bv2int [[C0]] signed {smt.some_attr} : !smt.bv<32>78 %28 = smt.bv2int %c signed {smt.some_attr} : !smt.bv<32>79 80 return81}82