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

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

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

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

Julian Kranz's avatar
Julian Kranz committed
14
15
16
17
  is-load <- return (
    case x.opnd1 of
       MEM m: '0'
     | REG r: '1'
Julian Kranz's avatar
Julian Kranz committed
18
    end
Julian Kranz's avatar
Julian Kranz committed
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
  );

  offset-factor <- return (
    if is-load then
      element-size
    else
      divb element-size 8
  );

  let
    val m i =
      let
        val write-dst value = do
          dst <- lval-offset element-size x.opnd1 (i*offset-factor);
          write element-size dst value
        end
      in do
        offset <- return (element-size*i);
        _if (/d (var (at-offset mask-temp ((i + 1)*element-size - 1)))) _then
          write-dst (var (at-offset src-temp offset))
        _else
          if is-load then
  	    write-dst (imm 0)
          else
            return void
      end end
Julian Kranz's avatar
Julian Kranz committed
45
  in
Julian Kranz's avatar
Julian Kranz committed
46
47
48
49
50
51
52
53
    vector-apply size element-size m
  end;

  if is-load and size === 128 then do
    dst <- lval-offset size x.opnd1 size;
    write size dst (imm 0)
  end else
    return void
Julian Kranz's avatar
Julian Kranz committed
54
55
end

Julian Kranz's avatar
Julian Kranz committed
56
val sem-maskmovdqu-vmaskmovdqu x = sem-maskmov 8 x
Julian Kranz's avatar
Julian Kranz committed
57

Julian Kranz's avatar
Julian Kranz committed
58
val sem-maskmovq x = sem-maskmov 8 x
Julian Kranz's avatar
Julian Kranz committed
59

Julian Kranz's avatar
Julian Kranz committed
60
61
val sem-mov avx-encoded x = do
  sz <- sizeof1 x.opnd1;
Julian Kranz's avatar
Julian Kranz committed
62
  a <- lval sz x.opnd1;
Julian Kranz's avatar
Julian Kranz committed
63
  b <- read sz x.opnd2;
Julian Kranz's avatar
Julian Kranz committed
64
  write-extend avx-encoded sz a b
Julian Kranz's avatar
Julian Kranz committed
65
66
end

Julian Kranz's avatar
Julian Kranz committed
67
68
69
70
71
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
#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
98

Julian Kranz's avatar
Julian Kranz committed
99
100
val sem-movbe x = do
  src <- read x.opnd-sz x.opnd2;
Julian Kranz's avatar
Julian Kranz committed
101
  dst <- lval x.opnd-sz x.opnd1;
Julian Kranz's avatar
Julian Kranz committed
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129

  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
130
  write x.opnd-sz dst (var dst-temp)
Julian Kranz's avatar
Julian Kranz committed
131
132
end

Julian Kranz's avatar
Julian Kranz committed
133
134
135
136
#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
137
#  dst <- lval dst-size x.opnd1;
Julian Kranz's avatar
Julian Kranz committed
138
139
140
141
142
#
#  temp <- mktemp;
#  mov dst-size temp (imm 0);
#  mov src-size temp src;
#
Julian Kranz's avatar
Julian Kranz committed
143
#  write dst-size dst (var temp)
Julian Kranz's avatar
Julian Kranz committed
144
145
146
147
148
149
150
151
#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
152
#  dst-size <-
Julian Kranz's avatar
Julian Kranz committed
153
154
155
156
157
158
159
#    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
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
#
#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
186
187
188
189
190
191
192
193
#
#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
194

Julian Kranz's avatar
Julian Kranz committed
195
196
197
val sem-movs x = do
  sz <- sizeof1 x.opnd1;
  src <- read sz x.opnd2;
Julian Kranz's avatar
Julian Kranz committed
198
  dst <- lval sz x.opnd1;
Julian Kranz's avatar
Cleanup    
Julian Kranz committed
199

Julian Kranz's avatar
Julian Kranz committed
200
  write sz dst src;
Julian Kranz's avatar
Julian Kranz committed
201

Julian Kranz's avatar
Julian Kranz committed
202
203
204
205
  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
206
  direction-adjust x.addr-sz reg1-sem sz
Julian Kranz's avatar
Julian Kranz committed
207
208
209
210
211
end

val sem-movsx x = do
  sz-dst <- sizeof1 x.opnd1;
  sz-src <- sizeof1 x.opnd2;
Julian Kranz's avatar
Julian Kranz committed
212
  dst <- lval sz-dst x.opnd1;
Julian Kranz's avatar
Julian Kranz committed
213
214
215
216
217
  src <- read sz-src x.opnd2;

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

Julian Kranz's avatar
Julian Kranz committed
218
  write sz-dst dst (var temp)
Julian Kranz's avatar
Julian Kranz committed
219
220
end

Julian Kranz's avatar
Julian Kranz committed
221
val sem-movzx avx-encoded x = do
Julian Kranz's avatar
Julian Kranz committed
222
223
  sz-dst <- sizeof1 x.opnd1;
  sz-src <- sizeof1 x.opnd2;
Julian Kranz's avatar
Julian Kranz committed
224
  dst <- lval sz-dst x.opnd1;
Julian Kranz's avatar
Julian Kranz committed
225
226
227
228
229
  src <- read sz-src x.opnd2;

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

Julian Kranz's avatar
Julian Kranz committed
230
  write-extend avx-encoded sz-dst dst (var temp)
Julian Kranz's avatar
Julian Kranz committed
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
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
251
252
253
254
255
256
257
258
    | _: 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
259
260
261
262
263
  end
end

## N>>

Julian Kranz's avatar
Julian Kranz committed
264
265
266
val sem-neg 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
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286

  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
287
  write size dst (var temp)
Julian Kranz's avatar
Julian Kranz committed
288
289
end

Julian Kranz's avatar
Julian Kranz committed
290
val sem-nop = do
Julian Kranz's avatar
Julian Kranz committed
291
292
293
  return void
end

Julian Kranz's avatar
Julian Kranz committed
294
295
296
val sem-not x = do
  size <- sizeof1 x.opnd1;
  src <- read size x.opnd1;
Julian Kranz's avatar
Julian Kranz committed
297
  dst <- lval size x.opnd1;
Julian Kranz's avatar
Julian Kranz committed
298
299
300
301

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

Julian Kranz's avatar
Julian Kranz committed
302
  write size dst (var temp)
Julian Kranz's avatar
Julian Kranz committed
303
304
end

Julian Kranz's avatar
Julian Kranz committed
305
306
307
308
## O>>

val sem-or x = do
  sz <- sizeof2 x.opnd1 x.opnd2;
Julian Kranz's avatar
Julian Kranz committed
309
  dst <- lval sz x.opnd1;
Julian Kranz's avatar
Julian Kranz committed
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
  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
327
  write sz dst (var temp)
Julian Kranz's avatar
Julian Kranz committed
328
329
330
331
end

## P>>

Julian Kranz's avatar
Julian Kranz committed
332
val sem-pabs avx-encoded element-size x = do
Julian Kranz's avatar
Julian Kranz committed
333
334
  size <- sizeof1 x.opnd1;
  src <- read size x.opnd2;
Julian Kranz's avatar
Julian Kranz committed
335
  dst <- lval size x.opnd1;
Julian Kranz's avatar
Julian Kranz committed
336
337
338
339
340
341
342

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

  temp-dst <- mktemp;

  let
Julian Kranz's avatar
Julian Kranz committed
343
344
345
346
    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
347
348
349
350
351
      _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
352
353
        mov element-size current-dst (var current-src)
      end
Julian Kranz's avatar
Julian Kranz committed
354
355
    end
  in
Julian Kranz's avatar
Julian Kranz committed
356
357
358
    vector-apply size element-size m
  end;

Julian Kranz's avatar
Julian Kranz committed
359
  write-extend avx-encoded size dst (var temp-dst)
Julian Kranz's avatar
Julian Kranz committed
360
361
end

Julian Kranz's avatar
Julian Kranz committed
362
363
364
365
366
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
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
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
408

  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
409
410
411
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
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
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
438
      _if (/gtu element-size (var (at-offset temp-src src-offset)) (imm upper)) _then (
Julian Kranz's avatar
Julian Kranz committed
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
       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
454
val sem-pbinop-opnd avx-encoded element-size operator opnd1 opnd2 opnd3 = do
Julian Kranz's avatar
Julian Kranz committed
455
456
457
458
459
460
461
462
463
464
465
466
467
468
  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
469

Julian Kranz's avatar
Julian Kranz committed
470
      operator 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
471
472
473
474
475
476
477
478
    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
479
480
val sem-padd element-size x = sem-pbinop-opnd '0' element-size add x.opnd1 x.opnd1 x.opnd2
val sem-vpadd element-size x = sem-pbinop-opnd '1' element-size add x.opnd1 x.opnd2 x.opnd3
Julian Kranz's avatar
Julian Kranz committed
481

Julian Kranz's avatar
Julian Kranz committed
482
483
val sem-padds element-size x = sem-pbinop-opnd '0' element-size add-signed-saturating x.opnd1 x.opnd1 x.opnd2
val sem-vpadds element-size x = sem-pbinop-opnd '1' element-size add-signed-saturating x.opnd1 x.opnd2 x.opnd3
Julian Kranz's avatar
Julian Kranz committed
484

Julian Kranz's avatar
Julian Kranz committed
485
486
val sem-paddus element-size x = sem-pbinop-opnd '0' element-size add-unsigned-saturating x.opnd1 x.opnd1 x.opnd2
val sem-vpaddus element-size x = sem-pbinop-opnd '1' element-size add-unsigned-saturating x.opnd1 x.opnd2 x.opnd3
Julian Kranz's avatar
Julian Kranz committed
487

Julian Kranz's avatar
Julian Kranz committed
488
val sem-palignr-vpalignr-opnd avx-encoded opnd1 opnd2 opnd3 opnd4 = do
Julian Kranz's avatar
Julian Kranz committed
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
  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
505
  write-extend avx-encoded size dst (var concatenated)
Julian Kranz's avatar
Julian Kranz committed
506
507
end

Julian Kranz's avatar
Julian Kranz committed
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
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
525

Julian Kranz's avatar
Julian Kranz committed
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
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
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
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
564

Julian Kranz's avatar
Julian Kranz committed
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
      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
581
582
583
584
585
586
587
588
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
589
590
591
592
593
594
595
596
  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
597
    mov size temp-src1 src1
Julian Kranz's avatar
Julian Kranz committed
598
599
600
  end else
    return void
  ;
Julian Kranz's avatar
Julian Kranz committed
601
602
  temp-src2 <- mktemp;
  mov size temp-src2 src2;
Julian Kranz's avatar
Julian Kranz committed
603
604
605
606
607
608
609
610
  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
611
612

      test-bit <- bit-selector element-size i temp-mask;
Julian Kranz's avatar
Julian Kranz committed
613
614
      _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
615
616
      _else
        if avx-encoded then
Julian Kranz's avatar
Julian Kranz committed
617
          mov element-size (at-offset temp-dst offset) (var (at-offset temp-src1 offset))
Julian Kranz's avatar
Julian Kranz committed
618
619
	else
	  return void
Julian Kranz's avatar
Cleanup    
Julian Kranz committed
620

Julian Kranz's avatar
Julian Kranz committed
621
622
623
624
625
626
627
628
    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
629
630
631
632
633
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
634

Julian Kranz's avatar
Julian Kranz committed
635
val sem-pclmulqdq-vpclmulqdq-opnd avx-encoded opnd1 opnd2 opnd3 opnd4 = do
Julian Kranz's avatar
Julian Kranz committed
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
  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
667
  mov part-size temp-dst (imm 0);
Julian Kranz's avatar
Julian Kranz committed
668

Julian Kranz's avatar
Julian Kranz committed
669
670
671
672
673
674
  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
675

Julian Kranz's avatar
Julian Kranz committed
676
677
    shr part-size temp1 (var temp1) (imm 1);
    shl part-size temp2 (var temp2) (imm 1);
Julian Kranz's avatar
Julian Kranz committed
678

Julian Kranz's avatar
Julian Kranz committed
679
    add 7 counter (var counter) (imm 1)
Julian Kranz's avatar
Julian Kranz committed
680
681
  end;

Julian Kranz's avatar
Julian Kranz committed
682
683
684
685
686
687
688
689
690
691
692
693
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
  #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
720
  #
Julian Kranz's avatar
Julian Kranz committed
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
  #        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
742

Julian Kranz's avatar
Julian Kranz committed
743
  write-extend avx-encoded size dst (var temp-dst)
Julian Kranz's avatar
Julian Kranz committed
744
end
Julian Kranz's avatar
Julian Kranz committed
745

Julian Kranz's avatar
Julian Kranz committed
746
747
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
748

Julian Kranz's avatar
Julian Kranz committed
749
val sem-pcmp-vpcmp-opnd avx-encoded element-size comparer opnd1 opnd2 opnd3 = do
Julian Kranz's avatar
Julian Kranz committed
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
  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
766
      _if (comparer element-size (var (at-offset temp-src1 offset)) (var (at-offset temp-src2 offset))) _then
Julian Kranz's avatar
Julian Kranz committed
767
768
769
        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
770
771
    end
  in
Julian Kranz's avatar
Julian Kranz committed
772
    vector-apply size element-size m
Julian Kranz's avatar
Julian Kranz committed
773
774
  end;

Julian Kranz's avatar
Julian Kranz committed
775
  write-extend avx-encoded size dst (var temp-dst)
Julian Kranz's avatar
Julian Kranz committed
776
777
end

Julian Kranz's avatar
Julian Kranz committed
778
779
780
781
782
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
783

Julian Kranz's avatar
Julian Kranz committed
784
785
786
787
788
789
790
791
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
792
793
794
795
796
797
798
799
800
  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
801
802
803

  temp <- mktemp;
  movzx src-size temp offset-size offset;
Julian Kranz's avatar
Julian Kranz committed
804
805
  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
806
807
  shr src-size temp src (var temp);

Julian Kranz's avatar
Julian Kranz committed
808
809
810
811
812
  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
813

Julian Kranz's avatar
Julian Kranz committed
814
  write dst-size dst (var temp)
Julian Kranz's avatar
Julian Kranz committed
815
816
end

Julian Kranz's avatar
Julian Kranz committed
817
val sem-phbinop-vphbinop-opnd avx-encoded element-size operator opnd1 opnd2 opnd3 = do
Julian Kranz's avatar
Julian Kranz committed
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
  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
833

Julian Kranz's avatar
Julian Kranz committed
834
      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
835
836
837
838
839
840
841
842
    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
843
844
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
845

Julian Kranz's avatar
Julian Kranz committed
846
847
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
848

Julian Kranz's avatar
Julian Kranz committed
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
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
865

Julian Kranz's avatar
Julian Kranz committed
866
867
868
869
870
871
872
873
874
875
876
877
      _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
878
879
880
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
881
882
883
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
884
885
886
val sem-pinsr-vpinsr-opnd avx-encoded element-size opnd1 opnd2 opnd3 opnd4 = do
  offset <- return (
    case opnd4 of
Julian Kranz's avatar
*    
Julian Kranz committed
887
      IMM8 x: x.imm
Julian Kranz's avatar
Julian Kranz committed
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
    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
919
val sem-pmcombine-opnd avx-encoded element-size combiner mover1 mover2 opnd1 opnd2 opnd3 = do
Julian Kranz's avatar
Julian Kranz committed
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
  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
939
      offset <- return (2*element-size*i);
Julian Kranz's avatar
Julian Kranz committed
940

Julian Kranz's avatar
Julian Kranz committed
941
942
      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
943

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

Julian Kranz's avatar
Julian Kranz committed
946
947
      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
948

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

Julian Kranz's avatar
Julian Kranz committed
951
      combiner (2*element-size) (at-offset temp-dst offset) (var local-dst1) (var local-dst2)
Julian Kranz's avatar
Julian Kranz committed
952
953
    end
  in
Julian Kranz's avatar
Julian Kranz committed
954
    vector-apply size (2*element-size) m
Julian Kranz's avatar
Julian Kranz committed
955
956
957
958
959
  end;

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

Julian Kranz's avatar
Julian Kranz committed
960
961
962
963
964
965
966
967
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
968
val sem-pcomp-opnd avx-encoded comparer element-size opnd1 opnd2 opnd3 = do
Julian Kranz's avatar
Julian Kranz committed
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
  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
985
      _if (comparer element-size (var (at-offset temp-src1 offset)) (var (at-offset temp-src2 offset))) _then
Julian Kranz's avatar
Julian Kranz committed
986
987
988
989
990
991
992
993
994
995
996
        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))
    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
997
val sem-pmaxs-vpmaxs-opnd avx-encoded element-size opnd1 opnd2 opnd3 = sem-pcomp-opnd avx-encoded /gts element-size opnd1 opnd2 opnd3
Julian Kranz's avatar
Julian Kranz committed
998
999
val sem-pmaxs element-size x = sem-pmaxs-vpmaxs-opnd '0' element-size x.opnd1 x.opnd1 x.opnd2
val sem-vpmaxs element-size x = sem-pmaxs-vpmaxs-opnd '1' element-size x.opnd1 x.opnd2 x.opnd3
Julian Kranz's avatar
Julian Kranz committed
1000