x86-rreil-translator-m-z.ml 56.4 KB
Newer Older
Julian Kranz's avatar
Julian Kranz committed
1
2
## M>>

Julian Kranz's avatar
Julian Kranz committed
3
val sem-maskmov x size = do
Julian Kranz's avatar
Julian Kranz committed
4
5
  src <- read size x.opnd1;
  mask <- read size x.opnd2;
Julian Kranz's avatar
Cleanup    
Julian Kranz committed
6

Julian Kranz's avatar
Julian Kranz committed
7
8
9
10
11
12
  src-temp <- mktemp;
  mov size src-temp src;

  mask-temp <- mktemp;
  mov size mask-temp mask;

Julian Kranz's avatar
Julian Kranz committed
13
  byte-size <- return 8;
Julian Kranz's avatar
Julian Kranz committed
14
  let
Julian Kranz's avatar
Julian Kranz committed
15
    val m i = do
Julian Kranz's avatar
Julian Kranz committed
16
      _if (/d (var (at-offset mask-temp ((i + 1)*8 - 1)))) _then do
Julian Kranz's avatar
Julian Kranz committed
17
18
        dst <- lval-offset byte-size x.opnd3 i;
        write byte-size dst (var (at-offset src-temp (i*8)))
Julian Kranz's avatar
Julian Kranz committed
19
      end
Julian Kranz's avatar
Julian Kranz committed
20
21
    end
  in
Julian Kranz's avatar
Julian Kranz committed
22
    vector-apply size byte-size m
Julian Kranz's avatar
Julian Kranz committed
23
24
25
  end
end

Julian Kranz's avatar
Julian Kranz committed
26
27
28
29
val sem-maskmovdqu-vmaskmovdqu x = sem-maskmov x 128

val sem-maskmovq x = sem-maskmov x 64

Julian Kranz's avatar
Julian Kranz committed
30
31
val sem-mov avx-encoded x = do
  sz <- sizeof1 x.opnd1;
Julian Kranz's avatar
Julian Kranz committed
32
  a <- lval sz x.opnd1;
Julian Kranz's avatar
Julian Kranz committed
33
  b <- read sz x.opnd2;
Julian Kranz's avatar
Julian Kranz committed
34
  write-extend avx-encoded sz a b
Julian Kranz's avatar
Julian Kranz committed
35
36
end

Julian Kranz's avatar
Julian Kranz committed
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
#val sem-movap x = do
#  sz <- sizeof1 x.opnd1;
#  dst <- lval sz x.opnd1;
#  src <- read sz x.opnd2;
#
#  temp <- mktemp;
#  mov sz temp src;
#
#  write sz dst (var temp)
#end
#
#val sem-vmovap x = do
#  x <- case x of VA2 x: return x end;
#
#  sz <- sizeof1 x.opnd1;
#  dst <- lval sz x.opnd1;
#  src <- read sz x.opnd2;
#
#  if sz === 128 then
#    do
#      dst-upper <- lval-upper sz x.opnd1;
#      write sz dst-upper (imm 0)
#    end
#  else
#    return void
#  ;
#
#  temp <- mktemp;
#  mov sz temp src;
#  write sz dst (var temp)
#end
Julian Kranz's avatar
Julian Kranz committed
68

Julian Kranz's avatar
Julian Kranz committed
69
70
val sem-movbe x = do
  src <- read x.opnd-sz x.opnd2;
Julian Kranz's avatar
Julian Kranz committed
71
  dst <- lval x.opnd-sz x.opnd1;
Julian Kranz's avatar
Julian Kranz committed
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99

  src-temp <- mktemp;
  mov x.opnd-sz src-temp src;

  dst-temp <- mktemp;

  limit <- return
    (case x.opnd-sz of
        16: 2
      | 32: 4
      | 64: 8
     end)
  ;

  byte-size <- return 8;
  let
    val f i = do
      mov byte-size (at-offset dst-temp (i*8)) (var (at-offset src-temp ((limit - i - 1)*8)));

      if (i < (limit - 1)) then
        f (i + 1)
      else
        return void
    end
  in
    f 0
  end;

Julian Kranz's avatar
Julian Kranz committed
100
  write x.opnd-sz dst (var dst-temp)
Julian Kranz's avatar
Julian Kranz committed
101
102
end

Julian Kranz's avatar
Julian Kranz committed
103
104
105
106
#val sem-movd-movq-vmovd-vmovq x dst-size = do
#  src-size <- sizeof1 x.opnd2;
#  src <- read src-size x.opnd2;
#
Julian Kranz's avatar
Julian Kranz committed
107
#  dst <- lval dst-size x.opnd1;
Julian Kranz's avatar
Julian Kranz committed
108
109
110
111
112
#
#  temp <- mktemp;
#  mov dst-size temp (imm 0);
#  mov src-size temp src;
#
Julian Kranz's avatar
Julian Kranz committed
113
#  write dst-size dst (var temp)
Julian Kranz's avatar
Julian Kranz committed
114
115
116
117
118
119
120
121
#end
#
#val sem-movd-movq x = do
#  dst-size <- sizeof1 x.opnd1;
#  sem-movd-movq-vmovd-vmovq x dst-size
#end
#
#val sem-vmovd-vmovq x = do
Julian Kranz's avatar
Cleanup    
Julian Kranz committed
122
#  dst-size <-
Julian Kranz's avatar
Julian Kranz committed
123
124
125
126
127
128
129
#    case x.opnd1 of
#       MEM m: sizeof1 x.opnd1
#     | REG r: return 256
#    end
#  ;
#  sem-movd-movq-vmovd-vmovq x dst-size
#end
Julian Kranz's avatar
Julian Kranz committed
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
#
#val sem-mov-sse-avx x size out-size = do
#  src <- read size x.opnd2;
#  dst <- lval out-size x.opnd1;
#
#  temp <- mktemp;
#  movzx out-size temp size src;
#
#  write out-size dst (var temp)
#end
#
#val sem-mov-sse x = do
#  size <- sizeof1 x.opnd1;
#  sem-mov-sse-avx x size size
#end
#
#val sem-mov-avx x = do
#  size <- sizeof1 x.opnd1;
#  out-size <- return
#    (case x.opnd1 of
#        MEM m: size
#      | REG r: 256
#    end)
#  ;
#  sem-mov-sse-avx x size out-size
#end
Julian Kranz's avatar
Julian Kranz committed
156
157
158
159
160
161
162
163
#
#val sem-movdq2q x = do
#  size <- sizeof1 x.opnd1; #Important: Destination size!
#  src <- read size x.opnd2;
#  dst <- lval size x.opnd1;
#
#  write size dst src
#end
Julian Kranz's avatar
Julian Kranz committed
164

Julian Kranz's avatar
Julian Kranz committed
165
166
167
val sem-movs x = do
  sz <- sizeof1 x.opnd1;
  src <- read sz x.opnd2;
Julian Kranz's avatar
Julian Kranz committed
168
  dst <- lval sz x.opnd1;
Julian Kranz's avatar
Cleanup    
Julian Kranz committed
169

Julian Kranz's avatar
Julian Kranz committed
170
  write sz dst src;
Julian Kranz's avatar
Julian Kranz committed
171

Julian Kranz's avatar
Julian Kranz committed
172
173
174
175
  reg0-sem <- return (semantic-register-of (read-addr-reg x.opnd1));
  reg1-sem <- return (semantic-register-of (read-addr-reg x.opnd2));

  direction-adjust x.addr-sz reg0-sem sz;
Julian Kranz's avatar
Julian Kranz committed
176
  direction-adjust x.addr-sz reg1-sem sz
Julian Kranz's avatar
Julian Kranz committed
177
178
179
180
181
end

val sem-movsx x = do
  sz-dst <- sizeof1 x.opnd1;
  sz-src <- sizeof1 x.opnd2;
Julian Kranz's avatar
Julian Kranz committed
182
  dst <- lval sz-dst x.opnd1;
Julian Kranz's avatar
Julian Kranz committed
183
184
185
186
187
  src <- read sz-src x.opnd2;

  temp <- mktemp;
  movsx sz-dst temp sz-src src;

Julian Kranz's avatar
Julian Kranz committed
188
  write sz-dst dst (var temp)
Julian Kranz's avatar
Julian Kranz committed
189
190
end

Julian Kranz's avatar
Julian Kranz committed
191
val sem-movzx avx-encoded x = do
Julian Kranz's avatar
Julian Kranz committed
192
193
  sz-dst <- sizeof1 x.opnd1;
  sz-src <- sizeof1 x.opnd2;
Julian Kranz's avatar
Julian Kranz committed
194
  dst <- lval sz-dst x.opnd1;
Julian Kranz's avatar
Julian Kranz committed
195
196
197
198
199
  src <- read sz-src x.opnd2;

  temp <- mktemp;
  movzx sz-dst temp sz-src src;

Julian Kranz's avatar
Julian Kranz committed
200
  write-extend avx-encoded sz-dst dst (var temp)
Julian Kranz's avatar
Julian Kranz committed
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
end

val sem-mul conv x = do
  sz <- sizeof1 x.opnd1;

  factor0-sem <- return (semantic-register-of (register-by-size low A sz));
  factor0 <- expand conv (var factor0-sem) sz (sz + sz);

  factor1 <- reads conv (sz + sz) x.opnd1;

  product <- mktemp;
  mul (sz + sz) product factor0 factor1;

  emit-mul-flags sz product;

  case sz of
     8: do
       ax <- return (semantic-register-of AX);
       mov sz ax (var product)
     end
Julian Kranz's avatar
Julian Kranz committed
221
222
223
224
225
226
227
228
    | _: move-combined sz (register-by-size low D sz) (register-by-size low A sz) product
#   | _: do
#       high <- return (semantic-register-of (register-by-size low D sz));
#       low <- return (semantic-register-of (register-by-size low A sz));
#
#       mov sz high (var (at-offset product sz));
#       mov sz low (var product)
#   end
Julian Kranz's avatar
Julian Kranz committed
229
230
231
232
233
  end
end

## N>>

Julian Kranz's avatar
Julian Kranz committed
234
235
236
val sem-neg x = do
  size <- sizeof1 x.opnd1;
  src <- read size x.opnd1;
Julian Kranz's avatar
Julian Kranz committed
237
  dst <- lval size x.opnd1;
Julian Kranz's avatar
Julian Kranz committed
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256

  temp <- mktemp;
  sub size temp (imm 0) src;

  cf <- fCF;
  ov <- fOF;
  sf <- fSF;
  zf <- fZF;

  cmpneq size cf src (imm 0);

  src-temp <- mktemp;
  mov size src-temp src;
  cmpeq 1 ov (var (at-offset temp (size - 1))) (var (at-offset src-temp (size - 1)));
  cmplts size sf (var temp) (imm 0);

  emit-parity-flag (var temp);
  emit-arithmetic-adjust-flag size (var temp) (imm 0) src; #Todo: Correct?

Julian Kranz's avatar
Julian Kranz committed
257
  write size dst (var temp)
Julian Kranz's avatar
Julian Kranz committed
258
259
end

Julian Kranz's avatar
Julian Kranz committed
260
261
262
263
val sem-nop x = do
  return void
end

Julian Kranz's avatar
Julian Kranz committed
264
265
266
val sem-not x = do
  size <- sizeof1 x.opnd1;
  src <- read size x.opnd1;
Julian Kranz's avatar
Julian Kranz committed
267
  dst <- lval size x.opnd1;
Julian Kranz's avatar
Julian Kranz committed
268
269
270
271

  temp <- mktemp;
  xorb size temp src (imm (0-1));

Julian Kranz's avatar
Julian Kranz committed
272
  write size dst (var temp)
Julian Kranz's avatar
Julian Kranz committed
273
274
end

Julian Kranz's avatar
Julian Kranz committed
275
276
277
278
## O>>

val sem-or x = do
  sz <- sizeof2 x.opnd1 x.opnd2;
Julian Kranz's avatar
Julian Kranz committed
279
  dst <- lval sz x.opnd1;
Julian Kranz's avatar
Julian Kranz committed
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
  src0 <- read sz x.opnd1;
  src1 <- read sz x.opnd2;
  temp <- mktemp;
  orb sz temp src0 src1;

  ov <- fOF;
  mov 1 ov (imm 0);
  cf <- fCF;
  mov 1 cf (imm 0);
  sf <- fSF;
  cmplts sz sf (var temp) (imm 0);
  zf <- fZF;
  cmpeq sz zf (var temp) (imm 0);
  emit-parity-flag (var temp);
  af <- fAF;
  undef 1 af;

Julian Kranz's avatar
Julian Kranz committed
297
  write sz dst (var temp)
Julian Kranz's avatar
Julian Kranz committed
298
299
300
301
end

## P>>

Julian Kranz's avatar
Julian Kranz committed
302
val sem-pabs avx-encoded element-size x = do
Julian Kranz's avatar
Julian Kranz committed
303
304
  size <- sizeof1 x.opnd1;
  src <- read size x.opnd2;
Julian Kranz's avatar
Julian Kranz committed
305
  dst <- lval size x.opnd1;
Julian Kranz's avatar
Julian Kranz committed
306
307
308
309
310
311
312

  temp-src <- mktemp;
  mov size temp-src src;

  temp-dst <- mktemp;

  let
Julian Kranz's avatar
Julian Kranz committed
313
314
315
316
    val m i = do
      offset <- return (element-size*i);
      current-src <- return (at-offset temp-src offset);
      current-dst <- return (at-offset temp-dst offset);
Julian Kranz's avatar
Julian Kranz committed
317
318
319
320
321
      _if (/lts element-size (var current-src) (imm 0)) _then
        #xorb element-size current-dst (var current-src) (imm (0-1));
	#add element-size current-dst (var current-dst) (imm 1)
        sub element-size current-dst (imm 0) (var current-src)
      _else do
Julian Kranz's avatar
Julian Kranz committed
322
323
        mov element-size current-dst (var current-src)
      end
Julian Kranz's avatar
Julian Kranz committed
324
325
    end
  in
Julian Kranz's avatar
Julian Kranz committed
326
327
328
    vector-apply size element-size m
  end;

Julian Kranz's avatar
Julian Kranz committed
329
  write-extend avx-encoded size dst (var temp-dst)
Julian Kranz's avatar
Julian Kranz committed
330
331
end

Julian Kranz's avatar
Julian Kranz committed
332
333
334
335
336
val sem-packsswb-packssdw-opnd avx-encoded dst-element-size opnd1 opnd2 opnd3 = do
  size <- sizeof1 opnd1;
  src1 <- read size opnd2;
  src2 <- read size opnd3;
  dst <- lval size opnd1;
Julian Kranz's avatar
Julian Kranz committed
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378

  temp-src <- mktemp;
  mov size temp-src src1;
  mov size (at-offset temp-src size) src2;

  temp-dst <- mktemp;

  element-size <- return (2*dst-element-size);

  upper <- return (
    if dst-element-size === 8 then
      0x7f
    else
      0x7fff
  );
  lower <- return (
    if dst-element-size === 8 then
      (0-0x80)
    else
      (0-0x8000)
  );

  let
    val m i = do
      src-offset <- return (element-size*i);
      dst-offset <- return (dst-element-size*i);

      _if (/gts element-size (var (at-offset temp-src src-offset)) (imm upper)) _then (
       mov dst-element-size (at-offset temp-dst dst-offset) (imm upper)
     ) _else ( _if (/lts element-size (var (at-offset temp-src src-offset)) (imm lower)) _then
       mov dst-element-size (at-offset temp-dst dst-offset) (imm lower)
     _else
       mov dst-element-size (at-offset temp-dst dst-offset) (var (at-offset temp-src (src-offset + dst-element-size)))
     )
    end
  in
    vector-apply (2*size) element-size m
  end;

  write-extend avx-encoded size dst (var temp-dst)
end

Julian Kranz's avatar
Julian Kranz committed
379
380
381
val sem-packsswb-packssdw dst-element-size x = sem-packsswb-packssdw-opnd '0' dst-element-size x.opnd1 x.opnd1 x.opnd2
val sem-vpacksswb-vpackssdw dst-element-size x = sem-packsswb-packssdw-opnd '1' dst-element-size x.opnd1 x.opnd2 x.opnd3

Julian Kranz's avatar
Julian Kranz committed
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
val sem-packuswb-packusdw-opnd avx-encoded dst-element-size opnd1 opnd2 opnd3 = do
  size <- sizeof1 opnd1;
  src1 <- read size opnd2;
  src2 <- read size opnd3;
  dst <- lval size opnd1;

  temp-src <- mktemp;
  mov size temp-src src1;
  mov size (at-offset temp-src size) src2;

  temp-dst <- mktemp;

  element-size <- return (2*dst-element-size);

  upper <- return (
    if dst-element-size === 8 then
      0xff
    else
      0xffff
  );

  let
    val m i = do
      src-offset <- return (element-size*i);
      dst-offset <- return (dst-element-size*i);

Julian Kranz's avatar
Julian Kranz committed
408
      _if (/gtu element-size (var (at-offset temp-src src-offset)) (imm upper)) _then (
Julian Kranz's avatar
Julian Kranz committed
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
       mov dst-element-size (at-offset temp-dst dst-offset) (imm upper)
     ) _else (
       mov dst-element-size (at-offset temp-dst dst-offset) (var (at-offset temp-src (src-offset + dst-element-size)))
     )
    end
  in
    vector-apply (2*size) element-size m
  end;

  write-extend avx-encoded size dst (var temp-dst)
end

val sem-packuswb-packusdw dst-element-size x = sem-packuswb-packusdw-opnd '0' dst-element-size x.opnd1 x.opnd1 x.opnd2
val sem-vpackuswb-vpackusdw dst-element-size x = sem-packuswb-packusdw-opnd '1' dst-element-size x.opnd1 x.opnd2 x.opnd3

Julian Kranz's avatar
Julian Kranz committed
424
val sem-padd-vpadd-opnd avx-encoded element-size adder opnd1 opnd2 opnd3 = do
Julian Kranz's avatar
Julian Kranz committed
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
  size <- sizeof1 opnd1;
  src1 <- read size opnd2;
  src2 <- read size opnd3;
  dst <- lval size opnd1;

  temp-src1 <- mktemp;
  mov size temp-src1 src1;
  temp-src2 <- mktemp;
  mov size temp-src2 src2;

  temp-dst <- mktemp;

  let
    val m i = do
      offset <- return (element-size*i);
Julian Kranz's avatar
Cleanup    
Julian Kranz committed
440

Julian Kranz's avatar
Julian Kranz committed
441
      adder element-size (at-offset temp-dst offset) (var (at-offset temp-src1 offset)) (var (at-offset temp-src2 offset))
Julian Kranz's avatar
Julian Kranz committed
442
443
444
445
446
447
448
449
    end
  in
    vector-apply size element-size m
  end;

  write-extend avx-encoded size dst (var temp-dst)
end

Julian Kranz's avatar
Julian Kranz committed
450
451
val sem-padd element-size x = sem-padd-vpadd-opnd '0' element-size add x.opnd1 x.opnd1 x.opnd2
val sem-vpadd element-size x = sem-padd-vpadd-opnd '1' element-size add x.opnd1 x.opnd2 x.opnd3
Julian Kranz's avatar
Julian Kranz committed
452

Julian Kranz's avatar
Julian Kranz committed
453
454
val sem-padds element-size x = sem-padd-vpadd-opnd '0' element-size add-signed-saturating x.opnd1 x.opnd1 x.opnd2
val sem-vpadds element-size x = sem-padd-vpadd-opnd '1' element-size add-signed-saturating x.opnd1 x.opnd2 x.opnd3
Julian Kranz's avatar
Julian Kranz committed
455

Julian Kranz's avatar
Julian Kranz committed
456
457
458
459
460
461
462
463
464
465
466
467
val sem-paddus-vpaddus-opnd avx-encoded element-size opnd1 opnd2 opnd3 = do
  size <- sizeof1 opnd1;
  src1 <- read size opnd2;
  src2 <- read size opnd3;
  dst <- lval size opnd1;

  temp-src1 <- mktemp;
  mov size temp-src1 src1;
  temp-src2 <- mktemp;
  mov size temp-src2 src2;

  temp-dst <- mktemp;
Julian Kranz's avatar
Cleanup    
Julian Kranz committed
468

Julian Kranz's avatar
Julian Kranz committed
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
  dst-ex <- mktemp;
  src1-ex <- mktemp;
  src2-ex <- mktemp;

  upper <- return (
    if element-size === 8 then
      0xff
    else
      0xffff
  );

  let
    val m i = do
      offset <- return (element-size*i);

      add (element-size + 1) (at-offset temp-dst offset) (var (at-offset temp-src1 offset)) (var (at-offset temp-src2 offset));
Julian Kranz's avatar
Cleanup    
Julian Kranz committed
485

Julian Kranz's avatar
Julian Kranz committed
486
487
488
489
490
491
492
493
494
495
496
497
498
499
      _if (/ltu element-size (var (at-offset temp-dst offset)) (var (at-offset temp-src1 offset))) _then (
        mov element-size (at-offset temp-dst offset) (imm upper)
      )
    end
  in
    vector-apply size element-size m
  end;

  write-extend avx-encoded size dst (var temp-dst)
end

val sem-paddus element-size x = sem-paddus-vpaddus-opnd '0' element-size x.opnd1 x.opnd1 x.opnd2
val sem-vpaddus element-size x = sem-paddus-vpaddus-opnd '1' element-size x.opnd1 x.opnd2 x.opnd3

Julian Kranz's avatar
Julian Kranz committed
500
val sem-palignr-vpalignr-opnd avx-encoded opnd1 opnd2 opnd3 opnd4 = do
Julian Kranz's avatar
Julian Kranz committed
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
  size <- sizeof1 opnd1;
  dst <- lval size opnd1;
  src1 <- read size opnd2;
  src2 <- read size opnd3;
  imm8 <- read 8 opnd4;

  shift-amount <- mktemp;
  movzx (2*size) shift-amount 8 imm8;
  shl (2*size) shift-amount (var shift-amount) (imm 3);

  concatenated <- mktemp;
  mov size concatenated src2;
  mov size (at-offset concatenated size) src1;

  shr (2*size) concatenated (var concatenated) (var shift-amount);

Julian Kranz's avatar
Julian Kranz committed
517
  write-extend avx-encoded size dst (var concatenated)
Julian Kranz's avatar
Julian Kranz committed
518
519
end

Julian Kranz's avatar
Julian Kranz committed
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
val sem-palignr x = sem-palignr-vpalignr-opnd '0' x.opnd1 x.opnd1 x.opnd2 x.opnd3
val sem-vpalignr x = sem-palignr-vpalignr-opnd '1' x.opnd1 x.opnd2 x.opnd3 x.opnd4

val sem-pand-vpand-opnd avx-encoded opnd1 opnd2 opnd3 = do
  size <- sizeof1 opnd1;
  dst <- lval size opnd1;
  src1 <- read size opnd2;
  src2 <- read size opnd3;

  temp <- mktemp;
  andb size temp src1 src2;

  write-extend avx-encoded size dst (var temp)
end

val sem-pand x = sem-pand-vpand-opnd '0' x.opnd1 x.opnd1 x.opnd2
val sem-vpand x = sem-pand-vpand-opnd '1' x.opnd1 x.opnd2 x.opnd3
Julian Kranz's avatar
Julian Kranz committed
537

Julian Kranz's avatar
Julian Kranz committed
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
val sem-pandn-vpandn-opnd avx-encoded opnd1 opnd2 opnd3 = do
  size <- sizeof1 opnd1;
  dst <- lval size opnd1;
  src1 <- read size opnd2;
  src2 <- read size opnd3;

  temp <- mktemp;
  xorb size temp src1 (imm (0-1));
  andb size temp (var temp) src2;

  write-extend avx-encoded size dst (var temp)
end

val sem-pandn x = sem-pandn-vpandn-opnd '0' x.opnd1 x.opnd1 x.opnd2
val sem-vpandn x = sem-pandn-vpandn-opnd '1' x.opnd1 x.opnd2 x.opnd3

Julian Kranz's avatar
Julian Kranz committed
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
val sem-pavg-vpavg-opnd avx-encoded element-size opnd1 opnd2 opnd3 = do
  size <- sizeof1 opnd1;
  src1 <- read size opnd2;
  src2 <- read size opnd3;
  dst <- lval size opnd1;

  temp-src1 <- mktemp;
  mov size temp-src1 src1;
  temp-src2 <- mktemp;
  mov size temp-src2 src2;

  temp-dst <- mktemp;

  src1-ex <- mktemp;
  src2-ex <- mktemp;

  let
    val m i = do
      offset <- return (element-size*i);

      movzx (element-size + 1) src1-ex element-size (var (at-offset temp-src1 offset));
      movzx (element-size + 1) src2-ex element-size (var (at-offset temp-src2 offset));
Julian Kranz's avatar
Cleanup    
Julian Kranz committed
576

Julian Kranz's avatar
Julian Kranz committed
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
      add (element-size + 1) src1-ex (var src1-ex) (var src2-ex);
      add (element-size + 1) src1-ex (var src1-ex) (imm 1);
      shr (element-size + 1) src1-ex (var src1-ex) (imm 1);

      mov element-size (at-offset temp-dst offset) (var src1-ex)
    end
  in
    vector-apply size element-size m
  end;

  write-extend avx-encoded size dst (var temp-dst)
end

val sem-pavg element-size x = sem-pavg-vpavg-opnd '0' element-size x.opnd1 x.opnd1 x.opnd2
val sem-vpavg element-size x = sem-pavg-vpavg-opnd '1' element-size x.opnd1 x.opnd2 x.opnd3

Julian Kranz's avatar
Julian Kranz committed
593
594
595
596
597
598
599
600
val blend-bit-selector-register element-size index mask = do
  offset <- return (element-size*index);
  return (at-offset mask (offset + element-size - 1))
end

val blend-bit-selector-immediate element-size index mask = return (at-offset mask index)

val sem-pblend-vpblend-opnd bit-selector avx-encoded element-size opnd1 opnd2 opnd3 opnd4 = do
Julian Kranz's avatar
Julian Kranz committed
601
602
603
604
605
606
607
608
  size <- sizeof1 opnd1;
  src1 <- read size opnd2;
  src2 <- read size opnd3;
  dst <- lval size opnd1;
  mask <- read size opnd4;

  temp-src1 <- mktemp;
  if avx-encoded then do
Julian Kranz's avatar
Julian Kranz committed
609
    mov size temp-src1 src1
Julian Kranz's avatar
Julian Kranz committed
610
611
612
  end else
    return void
  ;
Julian Kranz's avatar
Julian Kranz committed
613
614
  temp-src2 <- mktemp;
  mov size temp-src2 src2;
Julian Kranz's avatar
Julian Kranz committed
615
616
617
618
619
620
621
622
  temp-mask <- mktemp;
  mov size temp-mask mask;

  temp-dst <- mktemp;

  let
    val m i = do
      offset <- return (element-size*i);
Julian Kranz's avatar
Cleanup    
Julian Kranz committed
623
624

      test-bit <- bit-selector element-size i temp-mask;
Julian Kranz's avatar
Julian Kranz committed
625
626
      _if (/d (var test-bit)) _then
        mov element-size (at-offset temp-dst offset) (var (at-offset temp-src2 offset))
Julian Kranz's avatar
Julian Kranz committed
627
628
      _else
        if avx-encoded then
Julian Kranz's avatar
Julian Kranz committed
629
          mov element-size (at-offset temp-dst offset) (var (at-offset temp-src1 offset))
Julian Kranz's avatar
Julian Kranz committed
630
631
	else
	  return void
Julian Kranz's avatar
Cleanup    
Julian Kranz committed
632

Julian Kranz's avatar
Julian Kranz committed
633
634
635
636
637
638
639
640
    end
  in
    vector-apply size element-size m
  end;

  write-extend avx-encoded size dst (var temp-dst)
end

Julian Kranz's avatar
Julian Kranz committed
641
642
643
644
645
val sem-pblendvb x = sem-pblend-vpblend-opnd blend-bit-selector-register '0' 8 x.opnd1 x.opnd1 x.opnd2 (REG XMM0)
val sem-vpblendvb x = sem-pblend-vpblend-opnd blend-bit-selector-register '1' 8 x.opnd1 x.opnd2 x.opnd3 x.opnd4

val sem-pblendw x = sem-pblend-vpblend-opnd blend-bit-selector-immediate '0' 16 x.opnd1 x.opnd1 x.opnd2 x.opnd3
val sem-vpblendw x = sem-pblend-vpblend-opnd blend-bit-selector-immediate '1' 16 x.opnd1 x.opnd2 x.opnd3 x.opnd4
Julian Kranz's avatar
Julian Kranz committed
646

Julian Kranz's avatar
Julian Kranz committed
647
val sem-pclmulqdq-vpclmulqdq-opnd avx-encoded opnd1 opnd2 opnd3 opnd4 = do
Julian Kranz's avatar
Julian Kranz committed
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
  size <- sizeof1 opnd1;
  dst <- lval size opnd1;
  src1 <- read size opnd2;
  src2 <- read size opnd3;
  imm_ <- read 8 opnd4;

  temp-imm <- mktemp;
  mov 8 temp-imm imm_;

  temp-src1 <- mktemp;
  mov size temp-src1 src1;
  temp-src2 <- mktemp;
  mov size temp-src2 src2;

  part-size <- return 64;

  temp1 <- mktemp;
  _if (/not (var temp-imm)) _then
    mov part-size temp1 (var (at-offset temp-src1 0))
  _else
    mov part-size temp1 (var (at-offset temp-src1 part-size))
  ;

  temp2 <- mktemp;
  _if (/not (var (at-offset temp-imm 4))) _then
    mov part-size temp2 (var (at-offset temp-src2 0))
  _else
    mov part-size temp2 (var (at-offset temp-src2 part-size))
  ;

  temp-dst <- mktemp;
Julian Kranz's avatar
Julian Kranz committed
679
  mov part-size temp-dst (imm 0);
Julian Kranz's avatar
Julian Kranz committed
680

Julian Kranz's avatar
Julian Kranz committed
681
682
683
684
685
686
  counter <- mktemp;
  mov 7 counter (imm 0);
  _while (/ltu 7 (var counter) (imm 64)) __ do
    _if (/d (var temp1)) _then
      xorb part-size temp-dst (var temp-dst) (var temp2)
    ;
Julian Kranz's avatar
Julian Kranz committed
687

Julian Kranz's avatar
Julian Kranz committed
688
689
    shr part-size temp1 (var temp1) (imm 1);
    shl part-size temp2 (var temp2) (imm 1);
Julian Kranz's avatar
Julian Kranz committed
690

Julian Kranz's avatar
Julian Kranz committed
691
    add 7 counter (var counter) (imm 1)
Julian Kranz's avatar
Julian Kranz committed
692
693
  end;

Julian Kranz's avatar
Julian Kranz committed
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
  #tmpB <- mktemp;
  #temp-bit <- mktemp;
  #let
  #  val f i = do
  #    andb 1 (at-offset tmpB i) (var (at-offset temp1 0)) (var (at-offset temp2 i));

  #    let
  #      val g j =
  #        if (j <= i) then do
  #          andb 1 temp-bit (var (at-offset temp1 j)) (var (at-offset temp2 (i - j)));
  #          xorb 1 (at-offset tmpB i) (var (at-offset tmpB i)) (var temp-bit);

  #          g (j + 1)
  #        end else
  #          return void
  #    in
  #      g 1
  #    end;

  #    mov 1 (at-offset temp-dst i) (var (at-offset tmpB i));

  #    if (i < 63) then
  #      f (i + 1)
  #    else
  #      return void
  #  end
  #in
  #  f 0
  #end;

  #let
  #  val f i = do
  #    mov 1 (at-offset tmpB i) (imm 0);

  #    let
  #      val g j = do
  #        andb 1 temp-bit (var (at-offset temp1 j)) (var (at-offset temp2 (i - j)));
  #        xorb 1 (at-offset tmpB i) (var (at-offset tmpB i)) (var temp-bit);
Julian Kranz's avatar
Cleanup    
Julian Kranz committed
732
  #
Julian Kranz's avatar
Julian Kranz committed
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
  #        if (j < 63) then
  #          g (j + 1)
  #        else
  #          return void
  #      end
  #    in
  #      g (i - 63)
  #    end;

  #    mov 1 (at-offset temp-dst i) (var (at-offset tmpB i));

  #    if (i < 126) then
  #      f (i + 1)
  #    else
  #      return void
  #  end
  #in
  #  f 64
  #end;

  #mov 1 (at-offset temp-dst (size - 1)) (imm 0);
Julian Kranz's avatar
Julian Kranz committed
754

Julian Kranz's avatar
Julian Kranz committed
755
  write-extend avx-encoded size dst (var temp-dst)
Julian Kranz's avatar
Julian Kranz committed
756
end
Julian Kranz's avatar
Julian Kranz committed
757

Julian Kranz's avatar
Julian Kranz committed
758
759
val sem-pclmulqdq x = sem-pclmulqdq-vpclmulqdq-opnd '0' x.opnd1 x.opnd1 x.opnd2 x.opnd3
val sem-vpclmulqdq x = sem-pclmulqdq-vpclmulqdq-opnd '1' x.opnd1 x.opnd2 x.opnd3 x.opnd4
Julian Kranz's avatar
Julian Kranz committed
760

Julian Kranz's avatar
Julian Kranz committed
761
val sem-pcmp-vpcmp-opnd avx-encoded element-size comparer opnd1 opnd2 opnd3 = do
Julian Kranz's avatar
Julian Kranz committed
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
  size <- sizeof1 opnd1;
  src1 <- read size opnd2;
  src2 <- read size opnd3;
  dst <- lval size opnd1;

  temp-src1 <- mktemp;
  mov size temp-src1 src1;
  temp-src2 <- mktemp;
  mov size temp-src2 src2;

  temp-dst <- mktemp;

  let
    val m i = do
      offset <- return (element-size*i);

Julian Kranz's avatar
Julian Kranz committed
778
      _if (comparer element-size (var (at-offset temp-src1 offset)) (var (at-offset temp-src2 offset))) _then
Julian Kranz's avatar
Julian Kranz committed
779
780
781
        mov element-size (at-offset temp-dst offset) (imm (0-1))
      _else
        mov element-size (at-offset temp-dst offset) (imm 0)
Julian Kranz's avatar
Julian Kranz committed
782
783
    end
  in
Julian Kranz's avatar
Julian Kranz committed
784
    vector-apply size element-size m
Julian Kranz's avatar
Julian Kranz committed
785
786
  end;

Julian Kranz's avatar
Julian Kranz committed
787
  write-extend avx-encoded size dst (var temp-dst)
Julian Kranz's avatar
Julian Kranz committed
788
789
end

Julian Kranz's avatar
Julian Kranz committed
790
791
792
793
794
val sem-pcmpeq element-size x = sem-pcmp-vpcmp-opnd '0' element-size /eq x.opnd1 x.opnd1 x.opnd2
val sem-vpcmpeq element-size x = sem-pcmp-vpcmp-opnd '1' element-size /eq x.opnd1 x.opnd2 x.opnd3

val sem-pcmpgt element-size x = sem-pcmp-vpcmp-opnd '0' element-size /gts x.opnd1 x.opnd1 x.opnd2
val sem-vpcmpgt element-size x = sem-pcmp-vpcmp-opnd '1' element-size /gts x.opnd1 x.opnd2 x.opnd3
Julian Kranz's avatar
Julian Kranz committed
795

Julian Kranz's avatar
Julian Kranz committed
796
797
798
799
800
801
802
803
val sem-pextr-vpextr element-size x = do
  dst-size <- sizeof1 x.opnd1;
  src-size <- return 128;
  offset-size <- return 8;

  src <- read src-size x.opnd2;
  dst <- lval dst-size x.opnd1;

Julian Kranz's avatar
Julian Kranz committed
804
805
806
807
808
809
810
811
812
  offset <- read offset-size x.opnd3;
  offset-mask <- return (
    case element-size of
       8: 0xf
     | 16: 0x7
     | 32: 0x3
     | 64: 0x1
    end
  );
Julian Kranz's avatar
Julian Kranz committed
813
814
815

  temp <- mktemp;
  movzx src-size temp offset-size offset;
Julian Kranz's avatar
Julian Kranz committed
816
817
  andb offset-size temp (var temp) (imm offset-mask);
  mul offset-size temp (var temp) (imm element-size);
Julian Kranz's avatar
Julian Kranz committed
818
819
  shr src-size temp src (var temp);

Julian Kranz's avatar
Julian Kranz committed
820
821
822
823
824
  if dst-size > element-size then
    mov (dst-size - element-size) (at-offset temp element-size) (imm 0)
  else
    return void
  ;
Julian Kranz's avatar
Julian Kranz committed
825

Julian Kranz's avatar
Julian Kranz committed
826
  write dst-size dst (var temp)
Julian Kranz's avatar
Julian Kranz committed
827
828
end

Julian Kranz's avatar
Julian Kranz committed
829
val sem-phbinop-vphbinop-opnd avx-encoded element-size operator opnd1 opnd2 opnd3 = do
Julian Kranz's avatar
Julian Kranz committed
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
  size <- sizeof1 opnd1;
  src1 <- read size opnd2;
  src2 <- read size opnd3;
  dst <- lval size opnd1;

  temp-src <- mktemp;
  mov size temp-src src1;
  mov size (at-offset temp-src size) src2;

  temp-dst <- mktemp;

  let
    val m i = do
      dst-offset <- return (element-size*i);
      src-offset <- return (2*dst-offset);
Julian Kranz's avatar
Cleanup    
Julian Kranz committed
845

Julian Kranz's avatar
Julian Kranz committed
846
      operator element-size (at-offset temp-dst dst-offset) (var (at-offset temp-src src-offset)) (var (at-offset temp-src (src-offset + element-size)))
Julian Kranz's avatar
Julian Kranz committed
847
848
849
850
851
852
853
854
    end
  in
    vector-apply size element-size m
  end;

  write-extend avx-encoded size dst (var temp-dst)
end

Julian Kranz's avatar
Julian Kranz committed
855
856
val sem-phadd element-size x = sem-phbinop-vphbinop-opnd '0' element-size add x.opnd1 x.opnd1 x.opnd2
val sem-vphadd element-size x = sem-phbinop-vphbinop-opnd '1' element-size add x.opnd1 x.opnd2 x.opnd3
Julian Kranz's avatar
Julian Kranz committed
857

Julian Kranz's avatar
Julian Kranz committed
858
859
val sem-phaddsw x = sem-phbinop-vphbinop-opnd '0' 16 add-signed-saturating x.opnd1 x.opnd1 x.opnd2
val sem-vphaddsw x = sem-phbinop-vphbinop-opnd '1' 16 add-signed-saturating x.opnd1 x.opnd2 x.opnd3
Julian Kranz's avatar
Julian Kranz committed
860

Julian Kranz's avatar
Julian Kranz committed
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
val sem-phminposuw-vphminposuw avx-encoded x = do
  element-size <- return 16;
  size <- sizeof1 x.opnd1;
  src1 <- read size x.opnd2;
  dst <- lval size x.opnd1;

  temp-src <- mktemp;
  mov size temp-src src1;

  temp-dst <- mktemp;
  mov element-size temp-dst (var temp-src);
  mov (size - element-size) (at-offset temp-dst element-size) (imm 0);

  let
    val m i = do
      offset <- return (element-size*i);
Julian Kranz's avatar
Julian Kranz committed
877

Julian Kranz's avatar
Julian Kranz committed
878
879
880
881
882
883
884
885
886
887
888
889
      _if (/leu element-size (var (at-offset temp-src offset)) (var temp-dst)) _then do
        mov element-size temp-dst (var (at-offset temp-src offset));
        mov element-size (at-offset temp-dst element-size) (imm i)
      end
    end
  in
    vector-apply size element-size m
  end;

  write-extend avx-encoded size dst (var temp-dst)
end

Julian Kranz's avatar
Julian Kranz committed
890
891
892
val sem-phsub element-size x = sem-phbinop-vphbinop-opnd '0' element-size sub x.opnd1 x.opnd1 x.opnd2
val sem-vphsub element-size x = sem-phbinop-vphbinop-opnd '1' element-size sub x.opnd1 x.opnd2 x.opnd3

Julian Kranz's avatar
Julian Kranz committed
893
894
895
val sem-phsubsw x = sem-phbinop-vphbinop-opnd '0' 16 sub-signed-saturating x.opnd1 x.opnd1 x.opnd2
val sem-vphsubsw x = sem-phbinop-vphbinop-opnd '1' 16 sub-signed-saturating x.opnd1 x.opnd2 x.opnd3

Julian Kranz's avatar
Julian Kranz committed
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
val sem-pinsr-vpinsr-opnd avx-encoded element-size opnd1 opnd2 opnd3 opnd4 = do
  offset <- return (
    case opnd4 of
      IMM8 x: x
    end
  );
  offset-mask <- return (
    case element-size of
       8: '00001111'
     | 16: '00000111'
     | 32: '00000011'
     | 64: '00000001'
    end
  );
  offset-masked <- return (offset and offset-mask);
  index <- return ((zx offset-masked) * element-size);

  dst-size <- sizeof1 opnd1;
  dst <- lval dst-size opnd1;

  src-size <- sizeof1 opnd3;
  src1 <- read dst-size opnd2;
  src2 <- read src-size opnd3;

  temp <- mktemp;
  mov dst-size temp src1;

  mov element-size (at-offset temp index) src2;

  write-extend avx-encoded dst-size dst (var temp)
end

val sem-pinsr element-size x = sem-pinsr-vpinsr-opnd '0' element-size x.opnd1 x.opnd1 x.opnd2 x.opnd3
val sem-vpinsr element-size x = sem-pinsr-vpinsr-opnd '1' element-size x.opnd1 x.opnd2 x.opnd3 x.opnd4

Julian Kranz's avatar
Julian Kranz committed
931
val sem-pmcombine-opnd avx-encoded element-size combiner mover1 mover2 opnd1 opnd2 opnd3 = do
Julian Kranz's avatar
Julian Kranz committed
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
  size <- sizeof1 opnd1;
  src1 <- read size opnd2;
  src2 <- read size opnd3;
  dst <- lval size opnd1;

  temp-src1 <- mktemp;
  mov size temp-src1 src1;
  temp-src2 <- mktemp;
  mov size temp-src2 src2;

  temp-dst <- mktemp;

  local-src1 <- mktemp;
  local-src2 <- mktemp;
  local-dst1 <- mktemp;
  local-dst2 <- mktemp;

  let
    val m i = do
Julian Kranz's avatar
Julian Kranz committed
951
      offset <- return (2*element-size*i);
Julian Kranz's avatar
Julian Kranz committed
952

Julian Kranz's avatar
Julian Kranz committed
953
954
      mover1 (2*element-size) local-src1 element-size (var (at-offset temp-src1 offset));
      mover2 (2*element-size) local-src2 element-size (var (at-offset temp-src2 offset));
Julian Kranz's avatar
Julian Kranz committed
955

Julian Kranz's avatar
Julian Kranz committed
956
      mul (2*element-size) local-dst1 (var local-src1) (var local-src2);
Julian Kranz's avatar
Julian Kranz committed
957

Julian Kranz's avatar
Julian Kranz committed
958
959
      mover1 (2*element-size) local-src1 element-size (var (at-offset temp-src1 (offset + element-size)));
      mover2 (2*element-size) local-src2 element-size (var (at-offset temp-src2 (offset + element-size)));
Julian Kranz's avatar
Julian Kranz committed
960

Julian Kranz's avatar
Julian Kranz committed
961
      mul (2*element-size) local-dst2 (var local-src1) (var local-src2);
Julian Kranz's avatar
Julian Kranz committed
962

Julian Kranz's avatar
Julian Kranz committed
963
      combiner (2*element-size) (at-offset temp-dst offset) (var local-dst1) (var local-dst2)
Julian Kranz's avatar
Julian Kranz committed
964
965
    end
  in
Julian Kranz's avatar
Julian Kranz committed
966
    vector-apply size (2*element-size) m
Julian Kranz's avatar
Julian Kranz committed
967
968
969
970
971
  end;

  write-extend avx-encoded size dst (var temp-dst)
end

Julian Kranz's avatar
Julian Kranz committed
972
973
974
975
976
977
978
979
val sem-pmaddubsw-vpmaddubsw-opnd avx-encoded opnd1 opnd2 opnd3 = sem-pmcombine-opnd avx-encoded 8 add-signed-saturating movzx movsx opnd1 opnd2 opnd3
val sem-pmaddubsw x = sem-pmaddubsw-vpmaddubsw-opnd '0' x.opnd1 x.opnd1 x.opnd2
val sem-vpmaddubsw x = sem-pmaddubsw-vpmaddubsw-opnd '1' x.opnd1 x.opnd2 x.opnd3

val sem-pmaddwd-vpmaddwd-opnd avx-encoded opnd1 opnd2 opnd3 = sem-pmcombine-opnd avx-encoded 16 add movsx movsx opnd1 opnd2 opnd3
val sem-pmaddwd x = sem-pmaddwd-vpmaddwd-opnd '0' x.opnd1 x.opnd1 x.opnd2
val sem-vpmaddwd x = sem-pmaddwd-vpmaddwd-opnd '1' x.opnd1 x.opnd2 x.opnd3

Julian Kranz's avatar
Julian Kranz committed
980
val sem-pcomp-opnd avx-encoded comparer element-size opnd1 opnd2 opnd3 = do
Julian Kranz's avatar
Julian Kranz committed
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
  size <- sizeof1 opnd1;
  src1 <- read size opnd2;
  src2 <- read size opnd3;
  dst <- lval size opnd1;

  temp-src1 <- mktemp;
  mov size temp-src1 src1;
  temp-src2 <- mktemp;
  mov size temp-src2 src2;

  temp-dst <- mktemp;

  let
    val m i = do
      offset <- return (element-size*i);

Julian Kranz's avatar
Julian Kranz committed
997
      _if (comparer element-size (var (at-offset temp-src1 offset)) (var (at-offset temp-src2 offset))) _then
Julian Kranz's avatar
Julian Kranz committed
998
999
1000
        mov element-size (at-offset temp-dst offset) (var (at-offset temp-src1 offset))
      _else
        mov element-size (at-offset temp-dst offset) (var (at-offset temp-src2 offset))