1; RUN: %S/ConcreteTest.py --klee='%klee' --lli=%lli %s 2 3declare void @print_i32(i32) 4 5define i1 @checkSlt() { 6 %c0 = icmp slt i8 -1, 1 ; 1 7 %c1 = icmp slt i8 0, 1 ; 1 8 %c2 = icmp slt i8 1, 1 ; 0 9 %c3 = icmp slt i8 1, -1 ; 0 10 %c4 = icmp slt i8 1, 0 ; 0 11 %c5 = icmp slt i8 1, 1 ; 0 12 %a0 = select i1 %c0, i8 1, i8 0 13 %a1 = select i1 %c1, i8 2, i8 0 14 %a2 = select i1 %c2, i8 4, i8 0 15 %a3 = select i1 %c3, i8 8, i8 0 16 %a4 = select i1 %c4, i8 16, i8 0 17 %a5 = select i1 %c5, i8 32, i8 0 18 %sum0 = add i8 %a0, %a1 19 %sum1 = add i8 %sum0, %a2 20 %sum2 = add i8 %sum1, %a3 21 %sum3 = add i8 %sum2, %a4 22 %sum = add i8 %sum3, %a5 23 %test = icmp eq i8 %sum, 3 ; 0bin000011 24 ret i1 %test 25} 26 27define i1 @checkSle() { 28 %c0 = icmp sle i8 -1, 1 ; 1 29 %c1 = icmp sle i8 0, 1 ; 1 30 %c2 = icmp sle i8 1, 1 ; 1 31 %c3 = icmp sle i8 1, -1 ; 0 32 %c4 = icmp sle i8 1, 0 ; 0 33 %c5 = icmp sle i8 1, 1 ; 1 34 %a0 = select i1 %c0, i8 1, i8 0 35 %a1 = select i1 %c1, i8 2, i8 0 36 %a2 = select i1 %c2, i8 4, i8 0 37 %a3 = select i1 %c3, i8 8, i8 0 38 %a4 = select i1 %c4, i8 16, i8 0 39 %a5 = select i1 %c5, i8 32, i8 0 40 %sum0 = add i8 %a0, %a1 41 %sum1 = add i8 %sum0, %a2 42 %sum2 = add i8 %sum1, %a3 43 %sum3 = add i8 %sum2, %a4 44 %sum = add i8 %sum3, %a5 45 %test = icmp eq i8 %sum, 39 ; 0bin100111 46 ret i1 %test 47} 48 49define i1 @checkSgt() { 50 %c0 = icmp sgt i8 -1, 1 ; 0 51 %c1 = icmp sgt i8 0, 1 ; 0 52 %c2 = icmp sgt i8 1, 1 ; 0 53 %c3 = icmp sgt i8 1, -1 ; 1 54 %c4 = icmp sgt i8 1, 0 ; 1 55 %c5 = icmp sgt i8 1, 1 ; 0 56 %a0 = select i1 %c0, i8 1, i8 0 57 %a1 = select i1 %c1, i8 2, i8 0 58 %a2 = select i1 %c2, i8 4, i8 0 59 %a3 = select i1 %c3, i8 8, i8 0 60 %a4 = select i1 %c4, i8 16, i8 0 61 %a5 = select i1 %c5, i8 32, i8 0 62 %sum0 = add i8 %a0, %a1 63 %sum1 = add i8 %sum0, %a2 64 %sum2 = add i8 %sum1, %a3 65 %sum3 = add i8 %sum2, %a4 66 %sum = add i8 %sum3, %a5 67 %test = icmp eq i8 %sum, 24 ; 0bin011000 68 ret i1 %test 69} 70 71define i1 @checkSge() { 72 %c0 = icmp sge i8 -1, 1 ; 0 73 %c1 = icmp sge i8 0, 1 ; 0 74 %c2 = icmp sge i8 1, 1 ; 1 75 %c3 = icmp sge i8 1, -1 ; 1 76 %c4 = icmp sge i8 1, 0 ; 1 77 %c5 = icmp sge i8 1, 1 ; 1 78 %a0 = select i1 %c0, i8 1, i8 0 79 %a1 = select i1 %c1, i8 2, i8 0 80 %a2 = select i1 %c2, i8 4, i8 0 81 %a3 = select i1 %c3, i8 8, i8 0 82 %a4 = select i1 %c4, i8 16, i8 0 83 %a5 = select i1 %c5, i8 32, i8 0 84 %sum0 = add i8 %a0, %a1 85 %sum1 = add i8 %sum0, %a2 86 %sum2 = add i8 %sum1, %a3 87 %sum3 = add i8 %sum2, %a4 88 %sum = add i8 %sum3, %a5 89 %test = icmp eq i8 %sum, 60 ; 0bin111100 90 ret i1 %test 91} 92 93define i1 @checkUlt() { 94 %c0 = icmp ult i8 -1, 1 ; 0 95 %c1 = icmp ult i8 0, 1 ; 1 96 %c2 = icmp ult i8 1, 1 ; 0 97 %c3 = icmp ult i8 1, -1 ; 1 98 %c4 = icmp ult i8 1, 0 ; 0 99 %c5 = icmp ult i8 1, 1 ; 0 100 %a0 = select i1 %c0, i8 1, i8 0 101 %a1 = select i1 %c1, i8 2, i8 0 102 %a2 = select i1 %c2, i8 4, i8 0 103 %a3 = select i1 %c3, i8 8, i8 0 104 %a4 = select i1 %c4, i8 16, i8 0 105 %a5 = select i1 %c5, i8 32, i8 0 106 %sum0 = add i8 %a0, %a1 107 %sum1 = add i8 %sum0, %a2 108 %sum2 = add i8 %sum1, %a3 109 %sum3 = add i8 %sum2, %a4 110 %sum = add i8 %sum3, %a5 111 %test = icmp eq i8 %sum, 10 ; 0bin001010 112 ret i1 %test 113} 114 115define i1 @checkUle() { 116 %c0 = icmp ule i8 -1, 1 ; 0 117 %c1 = icmp ule i8 0, 1 ; 1 118 %c2 = icmp ule i8 1, 1 ; 1 119 %c3 = icmp ule i8 1, -1 ; 1 120 %c4 = icmp ule i8 1, 0 ; 0 121 %c5 = icmp ule i8 1, 1 ; 1 122 %a0 = select i1 %c0, i8 1, i8 0 123 %a1 = select i1 %c1, i8 2, i8 0 124 %a2 = select i1 %c2, i8 4, i8 0 125 %a3 = select i1 %c3, i8 8, i8 0 126 %a4 = select i1 %c4, i8 16, i8 0 127 %a5 = select i1 %c5, i8 32, i8 0 128 %sum0 = add i8 %a0, %a1 129 %sum1 = add i8 %sum0, %a2 130 %sum2 = add i8 %sum1, %a3 131 %sum3 = add i8 %sum2, %a4 132 %sum = add i8 %sum3, %a5 133 %test = icmp eq i8 %sum, 46 ; 0bin101110 134 ret i1 %test 135} 136 137define i1 @checkUgt() { 138 %c0 = icmp ugt i8 -1, 1 ; 1 139 %c1 = icmp ugt i8 0, 1 ; 0 140 %c2 = icmp ugt i8 1, 1 ; 0 141 %c3 = icmp ugt i8 1, -1 ; 0 142 %c4 = icmp ugt i8 1, 0 ; 1 143 %c5 = icmp ugt i8 1, 1 ; 0 144 %a0 = select i1 %c0, i8 1, i8 0 145 %a1 = select i1 %c1, i8 2, i8 0 146 %a2 = select i1 %c2, i8 4, i8 0 147 %a3 = select i1 %c3, i8 8, i8 0 148 %a4 = select i1 %c4, i8 16, i8 0 149 %a5 = select i1 %c5, i8 32, i8 0 150 %sum0 = add i8 %a0, %a1 151 %sum1 = add i8 %sum0, %a2 152 %sum2 = add i8 %sum1, %a3 153 %sum3 = add i8 %sum2, %a4 154 %sum = add i8 %sum3, %a5 155 %test = icmp eq i8 %sum, 17 ; 0bin010001 156 ret i1 %test 157} 158 159define i1 @checkUge() { 160 %c0 = icmp uge i8 -1, 1 ; 1 161 %c1 = icmp uge i8 0, 1 ; 0 162 %c2 = icmp uge i8 1, 1 ; 1 163 %c3 = icmp uge i8 1, -1 ; 0 164 %c4 = icmp uge i8 1, 0 ; 1 165 %c5 = icmp uge i8 1, 1 ; 1 166 %a0 = select i1 %c0, i8 1, i8 0 167 %a1 = select i1 %c1, i8 2, i8 0 168 %a2 = select i1 %c2, i8 4, i8 0 169 %a3 = select i1 %c3, i8 8, i8 0 170 %a4 = select i1 %c4, i8 16, i8 0 171 %a5 = select i1 %c5, i8 32, i8 0 172 %sum0 = add i8 %a0, %a1 173 %sum1 = add i8 %sum0, %a2 174 %sum2 = add i8 %sum1, %a3 175 %sum3 = add i8 %sum2, %a4 176 %sum = add i8 %sum3, %a5 177 %test = icmp eq i8 %sum, 53 ; 0bin110101 178 ret i1 %test 179} 180 181define i1 @checkEq() { 182 %c0 = icmp eq i8 -1, 1 ; 0 183 %c1 = icmp eq i8 1, 1 ; 1 184 %c2 = icmp eq i8 1, -1 ; 0 185 %a0 = select i1 %c0, i8 1, i8 0 186 %a1 = select i1 %c1, i8 2, i8 0 187 %a2 = select i1 %c2, i8 4, i8 0 188 %sum0 = add i8 %a0, %a1 189 %sum = add i8 %sum0, %a2 190 %test = icmp eq i8 %sum, 2 191 ret i1 %test 192} 193 194define i1 @checkNe() { 195 %c0 = icmp ne i8 -1, 1 ; 1 196 %c1 = icmp ne i8 1, 1 ; 0 197 %c2 = icmp ne i8 1, -1 ; 1 198 %a0 = select i1 %c0, i8 1, i8 0 199 %a1 = select i1 %c1, i8 2, i8 0 200 %a2 = select i1 %c2, i8 4, i8 0 201 %sum0 = add i8 %a0, %a1 202 %sum = add i8 %sum0, %a2 203 %test = icmp eq i8 %sum, 5 204 ret i1 %test 205} 206 207define i32 @main() { 208 %c0 = call i1 @checkSlt () 209 %c1 = call i1 @checkSle () 210 %c2 = call i1 @checkSgt () 211 %c3 = call i1 @checkSge () 212 %c4 = call i1 @checkUlt () 213 %c5 = call i1 @checkUle () 214 %c6 = call i1 @checkUgt () 215 %c7 = call i1 @checkUge () 216 %c8 = call i1 @checkEq () 217 %c9 = call i1 @checkNe () 218 %a0 = select i1 %c0, i16 1, i16 0 219 %a1 = select i1 %c1, i16 2, i16 0 220 %a2 = select i1 %c2, i16 4, i16 0 221 %a3 = select i1 %c3, i16 8, i16 0 222 %a4 = select i1 %c4, i16 16, i16 0 223 %a5 = select i1 %c5, i16 32, i16 0 224 %a6 = select i1 %c6, i16 64, i16 0 225 %a7 = select i1 %c7, i16 128, i16 0 226 %a8 = select i1 %c8, i16 256, i16 0 227 %a9 = select i1 %c9, i16 512, i16 0 228 %sum0 = add i16 %a0, %a1 229 %sum1 = add i16 %sum0, %a2 230 %sum2 = add i16 %sum1, %a3 231 %sum3 = add i16 %sum2, %a4 232 %sum4 = add i16 %sum3, %a5 233 %sum5 = add i16 %sum4, %a6 234 %sum6 = add i16 %sum5, %a7 235 %sum7 = add i16 %sum6, %a8 236 %sum8 = add i16 %sum7, %a9 237 %t = shl i16 63, 10 238 %sum = add i16 %sum8, %t 239 %test = icmp eq i16 %sum, -1 240 br i1 %test, label %exitTrue, label %exitFalse 241exitTrue: 242 call void @print_i32(i32 1) 243 ret i32 0 244exitFalse: 245 call void @print_i32(i32 0) 246 ret i32 0 247} 248