x86-rreil-translator.ml 54.7 KB
Newer Older
mb0's avatar
Up.  
mb0 committed
1
2
# vim:filetype=sml:ts=3:sw=3:expandtab

Julian Kranz's avatar
Julian Kranz committed
3
export = translate translateBlock
mb0's avatar
Up.  
mb0 committed
4

Julian Kranz's avatar
Julian Kranz committed
5
#Todo: fix
Julian Kranz's avatar
Julian Kranz committed
6
val runtime-stack-address-size = do
Julian Kranz's avatar
Julian Kranz committed
7
8
9
10
11
  mode64 <- mode64?;
  if mode64 then
    return 64
  else
    return 32
Julian Kranz's avatar
Julian Kranz committed
12
13
end

Julian Kranz's avatar
Julian Kranz committed
14
val ip-get = do
Julian Kranz's avatar
Julian Kranz committed
15
16
  k <- ipget;
  return (imm k)
Julian Kranz's avatar
Julian Kranz committed
17
18
end

Julian Kranz's avatar
Julian Kranz committed
19
20
21
22
23
24
25
26
val segment-register? x =
  case x of
     CS: '1'
   | SS: '1'
   | DS: '1'
   | ES: '1'
   | FS: '1'
   | GS: '1'
27
   | _ : '0'
Julian Kranz's avatar
Julian Kranz committed
28
29
  end

Julian Kranz's avatar
Julian Kranz committed
30
val sizeof2 dst/src1 src2 =
mb0's avatar
Up.  
mb0 committed
31
32
33
34
35
36
37
38
39
40
   case dst/src1 of
      REG r: return ($size (semantic-register-of r))
    | MEM x: return x.sz
    | _:
         case src2 of
            REG r: return ($size (semantic-register-of r))
          | MEM x: return x.sz
         end
   end

Julian Kranz's avatar
Julian Kranz committed
41
42
43
44
45
46
47
48
49
val sizeof-flow target =
  case target of
     REL8 x: return 8
   | REL16 x: return 16
   | REL32 x: return 32
   | REL64 x: return 64
   | NEARABS x: sizeof1 x
   | FARABS x: sizeof1 x
  end
mb0's avatar
Up.  
mb0 committed
50

Julian Kranz's avatar
Julian Kranz committed
51
val sizeof1 op =
mb0's avatar
Up.  
mb0 committed
52
53
54
55
56
57
58
59
60
   case op of
      REG r: return (semantic-register-of r).size
    | MEM x: return x.sz
    | IMM8 i: return 8
    | IMM16 i: return 16
    | IMM32 i: return 32
    | IMM64 i: return 64
   end

Julian Kranz's avatar
Julian Kranz committed
61
62
63
64
type signedness =
   Signed
 | Unsigned

Julian Kranz's avatar
Julian Kranz committed
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
val expand conv lin from-sz to-sz = do
  if from-sz === to-sz then
    return lin
  else
    do
      expanded <- mktemp;
      case conv of
         Signed: movsx to-sz expanded from-sz lin
       | Unsigned: movzx to-sz expanded from-sz lin
      end;
      return (var expanded)
    end
end

val segment-add mode64 address segment = let
  val seg-sem seg-reg = SEM_LIN_VAR(semantic-register-of seg-reg)
Julian Kranz's avatar
Julian Kranz committed
81
in
Julian Kranz's avatar
Julian Kranz committed
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
  case segment of
     SEG_NONE:
       if mode64 then
         address
       else
         SEM_LIN_ADD {opnd1=seg-sem DS,opnd2=address}
   | SEG_OVERRIDE s:
       if mode64 then
         case s of
            FS: SEM_LIN_ADD {opnd1=seg-sem s,opnd2=address}
  	  | GS: SEM_LIN_ADD {opnd1=seg-sem s,opnd2=address}
	  | _: address
	 end
       else
         SEM_LIN_ADD {opnd1=seg-sem s,opnd2=address}
  end
Julian Kranz's avatar
Julian Kranz committed
98
end
Julian Kranz's avatar
Julian Kranz committed
99

Julian Kranz's avatar
Julian Kranz committed
100
101
102
103
104
#IA-32e => 64 bit real addresses
val real-addr-sz = return 64

val segmented-lin lin sz segment = do
  real-addr-sz <- real-addr-sz;
Julian Kranz's avatar
Julian Kranz committed
105
  mode64 <- mode64?;
Julian Kranz's avatar
Julian Kranz committed
106

Julian Kranz's avatar
Julian Kranz committed
107
  expanded <- expand Unsigned lin sz real-addr-sz;
Julian Kranz's avatar
Julian Kranz committed
108
109
  return (segment-add mode64 expanded segment)
end
Julian Kranz's avatar
Julian Kranz committed
110
val segmented-reg reg segment = segmented-lin (var reg) reg.size segment
Julian Kranz's avatar
Julian Kranz committed
111
112
113
114
115
116
117
118
119
120
121
122
123

val segmented-load dst-sz dst addr-sz address segment = do
  address-segmented <- segmented-lin address addr-sz segment;
  addr-sz <- real-addr-sz;
  load dst-sz dst addr-sz address-segmented
end

val segmented-store addr rhs segment = do
  address-segmented <- segmented-lin addr.address addr.size segment;
  addr-sz <- real-addr-sz;
  store (address addr-sz address-segmented) rhs
end

Julian Kranz's avatar
Julian Kranz committed
124
#val segment segment = do
Julian Kranz's avatar
Julian Kranz committed
125
126
127
128
129
130
131
132
133
134
135
136
#  mode64 <- mode64?;
#  if mode64 then
#    case segment of
#       SEG_NONE: return 
#
#    case segment of
#       FS: return segment
#     | GS: return segment
#     | _: return DS
#    end
#  else
#    return segment
Julian Kranz's avatar
Julian Kranz committed
137
138
#  return DS
#end
Julian Kranz's avatar
Julian Kranz committed
139

Julian Kranz's avatar
Julian Kranz committed
140
val conv-with conv sz x =
mb0's avatar
Up.  
mb0 committed
141
   let
Julian Kranz's avatar
Julian Kranz committed
142
143
144
145
146
      val conv-imm conv x = case conv of
      	  Signed: return (SEM_LIN_IMM{imm=sx x})
	| Unsigned: return (SEM_LIN_IMM{imm=zx x})
      end

Julian Kranz's avatar
Julian Kranz committed
147
148
149
150
      val conv-reg conv sz r = do
        reg <- return (semantic-register-of r);
	expand conv (var reg) reg.size sz
      end
mb0's avatar
Up.  
mb0 committed
151

Julian Kranz's avatar
Julian Kranz committed
152
      val conv-sum conv sz x =
mb0's avatar
Up.  
mb0 committed
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
         do op1 <- conv-with conv sz x.a;
            op2 <- conv-with conv sz x.b;
            return
               (SEM_LIN_ADD
                  {opnd1=op1,
                   opnd2=op2})
         end

      val conv-scale conv sz x =
         do op <- conv-with conv sz x.opnd;
            return
               (SEM_LIN_SCALE
                  {opnd=op,
                   imm=
                     case $imm x of
                        '00': 1
                      | '01': 2
                      | '10': 4
                      | '11': 8
                     end})
         end

Julian Kranz's avatar
Julian Kranz committed
175
      val conv-mem x = conv-with Signed x.psz x.opnd
mb0's avatar
Up.  
mb0 committed
176
177
   in
      case x of
Julian Kranz's avatar
*    
Julian Kranz committed
178
179
180
181
         IMM8 x: conv-imm conv x.imm
       | IMM16 x: conv-imm conv x.imm
       | IMM32 x: conv-imm conv x.imm
       | IMM64 x: conv-imm conv x.imm
Julian Kranz's avatar
Julian Kranz committed
182
       | REG x: conv-reg conv sz x
mb0's avatar
Up.  
mb0 committed
183
184
185
       | SUM x: conv-sum conv sz x
       | SCALE x: conv-scale conv sz x
       | MEM x:
Julian Kranz's avatar
Julian Kranz committed
186
           do
Julian Kranz's avatar
Julian Kranz committed
187
188
	     t <- mktemp;
             address <- conv-mem x;
Julian Kranz's avatar
Julian Kranz committed
189
190
             segmented-load x.sz t x.psz address x.segment;
             expand conv (var t) x.sz sz
Julian Kranz's avatar
Julian Kranz committed
191
           end
mb0's avatar
Up.  
mb0 committed
192
193
194
      end
   end

Julian Kranz's avatar
Julian Kranz committed
195
val read sz x = conv-with Unsigned sz x
Julian Kranz's avatar
Julian Kranz committed
196
val reads conv sz x = conv-with conv sz x
Julian Kranz's avatar
Julian Kranz committed
197

Julian Kranz's avatar
Julian Kranz committed
198
199
val extract-imm-unsigned imm =
  case imm of
Julian Kranz's avatar
*    
Julian Kranz committed
200
201
202
203
     IMM8 x: zx x.imm
   | IMM16 x: zx x.imm
   | IMM32 x: zx x.imm
   | IMM64 x: zx x.imm
Julian Kranz's avatar
Julian Kranz committed
204
205
 end

Julian Kranz's avatar
Julian Kranz committed
206
207
208
209
210
211
212
213
val read-addr-reg x =
  case x of
     MEM m:
       case m.opnd of
          REG r: r
       end
  end

mb0's avatar
Up.  
mb0 committed
214
215
216
217
218
219
220
221
222
223
224
225
226
227
val read-flow sz x =
   let
      val conv-bv v = return (SEM_LIN_IMM{imm=sx v})
   in
      case x of
         REL8 x: conv-bv x
       | REL16 x: conv-bv x
       | REL32 x: conv-bv x
       | REL64 x: conv-bv x
       | NEARABS x: read sz x
       | FARABS x: read sz x
      end
   end

Julian Kranz's avatar
Julian Kranz committed
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
val near target =
  case target of
     REL8 x: '1'
   | REL16 x: '1'
   | REL32 x: '1'
   | REL64 x: '1'
   | NEARABS x: '1'
   | _: '0'
  end

val far target = not (near target)

val relative target =
  case target of
     REL8 x: '1'
   | REL16 x: '1'
   | REL32 x: '1'
   | REL64 x: '1'
   | _: '0'
  end

val absolute target = not (relative target)

Julian Kranz's avatar
Julian Kranz committed
251
#Todo: MEM => byte offset, REG => bit offset... confusing (division?)
Julian Kranz's avatar
Julian Kranz committed
252
val lval-offset sz x offset =
mb0's avatar
Up.  
mb0 committed
253
   case x of
Julian Kranz's avatar
Julian Kranz committed
254
255
     MEM x:
       do
Julian Kranz's avatar
Julian Kranz committed
256
         #Offset for memory operands? => Add offset to pointer
Julian Kranz's avatar
Julian Kranz committed
257
         address <- conv-with Signed x.psz x.opnd;
Julian Kranz's avatar
Julian Kranz committed
258
259
	 combined <- return (SEM_LIN_ADD{opnd1=address,opnd2=SEM_LIN_IMM {imm=offset}});
         return (SEM_WRITE_MEM{size=x.psz,address=combined,segment=x.segment})
Julian Kranz's avatar
Julian Kranz committed
260
       end
Julian Kranz's avatar
Julian Kranz committed
261
    | REG r:
Julian Kranz's avatar
Julian Kranz committed
262
       do 
Julian Kranz's avatar
Julian Kranz committed
263
         id <- return (semantic-register-of-operand-with-size x sz);
Julian Kranz's avatar
Julian Kranz committed
264
265
266
	 id <- return (@{offset=id.offset + offset} id);
         return (SEM_WRITE_VAR{size= $size id,id=id})
       end
mb0's avatar
Up.  
mb0 committed
267
268
   end

Julian Kranz's avatar
Julian Kranz committed
269

Julian Kranz's avatar
Julian Kranz committed
270
271
val lval sz x = lval-offset sz x 0
val lval-upper sz x = lval-offset sz x sz
Julian Kranz's avatar
Julian Kranz committed
272
273
274
275
276
277
278

val register? x =
  case x of
      REG: '1'
    | _: '0'
  end

Julian Kranz's avatar
Julian Kranz committed
279
val write-extend avx-encoded sz a b =
mb0's avatar
Up.  
mb0 committed
280
281
   case a of
      SEM_WRITE_MEM x:
Julian Kranz's avatar
Julian Kranz committed
282
         #store x (SEM_LIN{size=sz,opnd1=b})
Julian Kranz's avatar
Julian Kranz committed
283
	 segmented-store x (SEM_LIN{size=sz,opnd1=b}) x.segment
Julian Kranz's avatar
Julian Kranz committed
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
    | SEM_WRITE_VAR x: do
        #if mode64 then
	#  mov 32 (semantic-register-of EAX) (imm 100)
	#else
	#  return void
	#;
        #if (is-avx-sse x.id.id) then
	#  mov 32 (semantic-register-of EAX) (imm 101)
	#else
	#  return void
	#;
        #if (avx-encoded) then
	#  mov 32 (semantic-register-of EAX) (imm 102)
	#else
	#  return void
	#;
	#mov 32 (semantic-register-of EAX) (imm (500 + sz));

Julian Kranz's avatar
Julian Kranz committed
302
303
304
	mov sz x.id b;

	mode64 <- mode64?;
Julian Kranz's avatar
Julian Kranz committed
305
306
	if (mode64 and (not (is-avx-sse x.id.id)) and sz === 32) then
	  #Todo: Only if sz == 32? - Yes (tested)!
Julian Kranz's avatar
Julian Kranz committed
307
308
309
310
311
312
	  #Todo: Only for a subset of all registers?
          mov (64 - sz) (at-offset x.id sz) (imm 0)
	else if (avx-encoded and (is-avx-sse x.id.id) and sz < 256) then
	  mov (256 - sz) (at-offset x.id sz) (imm 0)
	else
	  return void
Julian Kranz's avatar
Julian Kranz committed
313

Julian Kranz's avatar
Julian Kranz committed
314
315
316
317
318
319
320
321
322
323
324
325
326
#        case sz of
#           32:
#              case x.id.offset of
#                 0:
#                    do mov 32 x.id b;
#                       # Zero the upper half of the given register/variable
#                       mov 32 (@{offset=32} x.id) (SEM_LIN_IMM {imm=0})
#                    end
#               | _: mov sz x.id b
#              end
#         | _: mov sz x.id b
#        end
        end
mb0's avatar
Up.  
mb0 committed
327
328
   end

Julian Kranz's avatar
Julian Kranz committed
329
330
val write sz a b = write-extend '0' sz a b

Julian Kranz's avatar
Julian Kranz committed
331
332
333
334
335
336
337
338
339
340
341
342
343
val combine high low = do
  high <- return (semantic-register-of high);
  low <- return (semantic-register-of low);
 
  sz <- return high.size;
 
  combined <- mktemp;
  mov sz (at-offset combined sz) (var high);
  mov sz combined (var low);
 
  return combined
end

Julian Kranz's avatar
Julian Kranz committed
344
345
346
347
348
349
350
351
val move-combined size dst-high dst-low src = do
  dst-high <- return (semantic-register-of dst-high);
  dst-low <- return (semantic-register-of dst-low);
 
  mov size dst-high (var (at-offset src size));
  mov size dst-low (var (at-offset src 0))
end

Axel Simon's avatar
Axel Simon committed
352
353
354
355
356
357
val fEQ = return (_var VIRT_EQ)
val fNEQ = return (_var VIRT_NEQ)
val fLES = return (_var VIRT_LES)
val fLEU = return (_var VIRT_LEU)
val fLTS = return (_var VIRT_LTS)
val fLTU = return (_var VIRT_LTU)
mb0's avatar
Up.  
mb0 committed
358
359
360

val zero = return (SEM_LIN_IMM{imm=0})

Julian Kranz's avatar
Julian Kranz committed
361
val _if c _then a _else b = do
Julian Kranz's avatar
Julian Kranz committed
362
  c <- c;
Julian Kranz's avatar
Julian Kranz committed
363
364
365
  stack <- pop-all;
  a;
  t <- pop-all;
Julian Kranz's avatar
Julian Kranz committed
366
  t <- return (rreil-stmts-rev t);
Julian Kranz's avatar
Julian Kranz committed
367
368
  b;
  e <- pop-all;
Julian Kranz's avatar
Julian Kranz committed
369
  e <- return (rreil-stmts-rev e);
Julian Kranz's avatar
Julian Kranz committed
370
  stack-set stack;
Julian Kranz's avatar
Julian Kranz committed
371
  ite c t e
Julian Kranz's avatar
Julian Kranz committed
372
373
374
375
376
377
378
379
end

val _if c _then a = do
  _if c _then a _else (return void)
end

val /d cond = return cond

Julian Kranz's avatar
Julian Kranz committed
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
val /and a b = do
  a <- a;
  b <- b;
  t <- mktemp;
  andb 1 t a b;
  return (var t)
end

val /or a b = do
  a <- a;
  b <- b;
  t <- mktemp;
  orb 1 t a b;
  return (var t)
end

val /not a = do
  t <- mktemp;
  xorb 1 t a (imm 1);
  return (var t)
end

Julian Kranz's avatar
Julian Kranz committed
402
403
404
405
406
407
408
409
410
411
val /eq sz a b = do
  t <- mktemp;
  cmpeq sz t a b;
  return (var t)
end

val /neq sz a b = do
  t <- mktemp;
  cmpneq sz t a b;
  return (var t)
Julian Kranz's avatar
Julian Kranz committed
412
413
end

Julian Kranz's avatar
Julian Kranz committed
414
415
416
417
418
419
420
val /gtu sz a b = do
  t <- mktemp;
  cmpleu sz t a b;
  xorb 1 t (var t) (imm 1);
  return (var t)
end

Julian Kranz's avatar
Julian Kranz committed
421
422
423
424
425
426
427
val /gts sz a b = do
  t <- mktemp;
  cmples sz t a b;
  xorb 1 t (var t) (imm 1);
  return (var t)
end

Julian Kranz's avatar
Julian Kranz committed
428
429
430
431
432
433
434
val /geu sz a b = do
  t <- mktemp;
  cmpltu sz t a b;
  xorb 1 t (var t) (imm 1);
  return (var t)
end

Julian Kranz's avatar
Julian Kranz committed
435
436
437
438
439
440
val /lts sz a b = do
  t <- mktemp;
  cmplts sz t a b;
  return (var t)
end

Julian Kranz's avatar
Julian Kranz committed
441
442
443
444
445
446
val /ltu sz a b = do
  t <- mktemp;
  cmpltu sz t a b;
  return (var t)
end

Julian Kranz's avatar
Julian Kranz committed
447
448
449
450
451
452
val /leu sz a b = do
  t <- mktemp;
  cmpleu sz t a b;
  return (var t)
end

Julian Kranz's avatar
Julian Kranz committed
453
val _while c __ b = do
Julian Kranz's avatar
Julian Kranz committed
454
455
456
  cc <- c;
  ct <- mktemp;
  mov 1 ct cc;
Julian Kranz's avatar
Julian Kranz committed
457
  stack <- pop-all;
Julian Kranz's avatar
Julian Kranz committed
458
  
Julian Kranz's avatar
Julian Kranz committed
459
  b;
Julian Kranz's avatar
Julian Kranz committed
460
461
  cc <- c;
  mov 1 ct cc;
Julian Kranz's avatar
Julian Kranz committed
462
  body <- pop-all;
Julian Kranz's avatar
Julian Kranz committed
463
  body <- return (rreil-stmts-rev body);
Julian Kranz's avatar
Julian Kranz committed
464

Julian Kranz's avatar
Julian Kranz committed
465
  stack-set stack;
Julian Kranz's avatar
Julian Kranz committed
466
  while (var ct) body
Julian Kranz's avatar
Julian Kranz committed
467
468
end

Julian Kranz's avatar
Julian Kranz committed
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
val sem-a sem-cc x = do
  cf <- fCF;
  zf <- fZF;
  sem-cc x (/and (/not (var cf)) (/not (var zf)))
end
val sem-nbe sem-cc x = sem-a sem-cc x

val sem-ae sem-cc x = do
  cf <- fCF;
  sem-cc x (/not (var cf))
end
val sem-nb sem-cc x = sem-ae sem-cc x
val sem-nc sem-cc x = sem-ae sem-cc x

val sem-c sem-cc x = do
  cf <- fCF;
  sem-cc x (/d (var cf))
end
val sem-b sem-cc x = sem-c sem-cc x
val sem-nae sem-cc x = sem-nae sem-cc x

val sem-be sem-cc x = do
  cf <- fCF;
  zf <- fZF;
  sem-cc x (/or (/d (var cf)) (/d (var zf)))
end
val sem-na sem-cc x = sem-be sem-cc x

val sem-e sem-cc x = do
  zf <- fZF;
  sem-cc x (/d (var zf))
end
val sem-z sem-cc x = sem-e sem-cc x

val sem-g sem-cc x = do
  zf <- fZF;
  sf <- fSF;
  ov <- fOF;
  sem-cc x (/and (/not (var zf)) (/eq 1 (var sf) (var ov)))
end
val sem-nle sem-cc x = sem-g sem-cc x

val sem-ge sem-cc x = do
  sf <- fSF;
  ov <- fOF;
  sem-cc x (/eq 1 (var sf) (var ov))
end
val sem-nl sem-cc x = sem-ge sem-cc x

val sem-l sem-cc x = do
  sf <- fSF;
  ov <- fOF;
  sem-cc x (/neq 1 (var sf) (var ov))
end
val sem-nge sem-cc x = sem-l sem-cc x

val sem-le sem-cc x = do
  zf <- fZF;
  sf <- fSF;
  ov <- fOF;
  sem-cc x (/or (/d (var zf)) (/neq 1 (var sf) (var ov)))
end
val sem-ng sem-cc x = sem-le sem-cc x

val sem-ne sem-cc x = do
  zf <- fZF;
  sem-cc x (/not (var zf))
end
val sem-nz sem-cc x = sem-ne sem-cc x

val sem-no sem-cc x = do
  ov <- fOF;
  sem-cc x (/not (var ov))
end

val sem-np sem-cc x = do
  pf <- fPF;
  sem-cc x (/not (var pf))
end
val sem-po sem-cc x = sem-np sem-cc x

val sem-ns sem-cc x = do
  sf <- fSF;
  sem-cc x (/not (var sf))
end

val sem-o sem-cc x = do
  ov <- fOF;
  sem-cc x (/d (var ov))
end

val sem-p sem-cc x = do
  pf <- fPF;
  sem-cc x (/d (var pf))
end
val sem-pe sem-cc x = sem-p sem-cc x

val sem-s sem-cc x = do
  sf <- fSF;
  sem-cc x (/d (var sf))
end

Julian Kranz's avatar
Julian Kranz committed
571
val undef-opnd opnd = do
Julian Kranz's avatar
Julian Kranz committed
572
  sz <- sizeof1 opnd;
Julian Kranz's avatar
Julian Kranz committed
573
  a <- lval sz opnd;
Julian Kranz's avatar
Julian Kranz committed
574
  t <- mktemp;
Julian Kranz's avatar
Julian Kranz committed
575
  write sz a (var t)
Julian Kranz's avatar
Julian Kranz committed
576
577
578
579
580
end

val sem-undef-arity-ge1 x = do
  case x.opnd1 of
     REG r: undef-opnd x.opnd1
Julian Kranz's avatar
Julian Kranz committed
581
   | MEM m: undef-opnd x.opnd1
Julian Kranz's avatar
Julian Kranz committed
582
583
584
  end
end

Julian Kranz's avatar
Julian Kranz committed
585
val sem-undef-arity0 x = do
Julian Kranz's avatar
Julian Kranz committed
586
  return void
Julian Kranz's avatar
Julian Kranz committed
587
588
589
end

val sem-undef-arity1 x = do
Julian Kranz's avatar
Julian Kranz committed
590
  sem-undef-arity-ge1 x
Julian Kranz's avatar
Julian Kranz committed
591
592
593
end

val sem-undef-arity2 x = do
Julian Kranz's avatar
Julian Kranz committed
594
  sem-undef-arity-ge1 x
Julian Kranz's avatar
Julian Kranz committed
595
596
597
end

val sem-undef-arity3 x = do
Julian Kranz's avatar
Julian Kranz committed
598
  sem-undef-arity-ge1 x
Julian Kranz's avatar
Julian Kranz committed
599
600
601
end

val sem-undef-arity4 x = do
Julian Kranz's avatar
Julian Kranz committed
602
  sem-undef-arity-ge1 x
Julian Kranz's avatar
Julian Kranz committed
603
604
605
end

val sem-undef-varity x = do
Julian Kranz's avatar
Julian Kranz committed
606
  case x of
Julian Kranz's avatar
Julian Kranz committed
607
608
     VA0 x: sem-undef-arity0 x
   | VA1 x: sem-undef-arity1 x
Julian Kranz's avatar
Julian Kranz committed
609
610
611
612
   | VA2 x: sem-undef-arity2 x
   | VA3 x: sem-undef-arity3 x
   | VA4 x: sem-undef-arity4 x
  end
Julian Kranz's avatar
Julian Kranz committed
613
614
615
end

val sem-undef-flow1 x = do
Julian Kranz's avatar
Julian Kranz committed
616
  return void
Julian Kranz's avatar
Julian Kranz committed
617
618
end

Julian Kranz's avatar
Julian Kranz committed
619
val emit-parity-flag r = do
Julian Kranz's avatar
Julian Kranz committed
620
621
  byte-size <- return 8;

Julian Kranz's avatar
Julian Kranz committed
622
  low-byte <- mktemp;
Julian Kranz's avatar
Julian Kranz committed
623
  mov byte-size low-byte r;
Julian Kranz's avatar
Julian Kranz committed
624
625

  pf <- fPF;
Julian Kranz's avatar
Julian Kranz committed
626
627
628
629
630
631
632
633
  # Bitwise XNOR
  cmpeq 1 pf (var (at-offset low-byte 7)) (var (at-offset low-byte 6));
  cmpeq 1 pf (var pf) (var (at-offset low-byte 5));
  cmpeq 1 pf (var pf) (var (at-offset low-byte 4));
  cmpeq 1 pf (var pf) (var (at-offset low-byte 3));
  cmpeq 1 pf (var pf) (var (at-offset low-byte 2));
  cmpeq 1 pf (var pf) (var (at-offset low-byte 1));
  cmpeq 1 pf (var pf) (var (at-offset low-byte 0))
Julian Kranz's avatar
Julian Kranz committed
634
635
end

Julian Kranz's avatar
Julian Kranz committed
636
val emit-arithmetic-adjust-flag sz r op0 op1 = do
Julian Kranz's avatar
Julian Kranz committed
637
638
  # Hacker's Delight - How the Computer Sets Overflow for Signed Add/Subtract
  t <- mktemp;
Julian Kranz's avatar
Julian Kranz committed
639
640
  xorb sz t r op0;
  xorb sz t (var t) op1;
Julian Kranz's avatar
Julian Kranz committed
641
642
643
644

  andb sz t (var t) (imm 0x10);
  af <- fAF;
  cmpneq sz af (var t) (imm 0)
Julian Kranz's avatar
Julian Kranz committed
645
end
Julian Kranz's avatar
Julian Kranz committed
646

Julian Kranz's avatar
Julian Kranz committed
647
val emit-add-adc-flags sz sum s0 s1 carry set-carry = do
Julian Kranz's avatar
Julian Kranz committed
648
649
650
651
  eq <- fEQ;
  les <- fLES;
  leu <- fLEU;
  lts <- fLTS;
Julian Kranz's avatar
Julian Kranz committed
652
  ltu <- fLTU;
Julian Kranz's avatar
Julian Kranz committed
653
654
  sf <- fSF;
  ov <- fOF;
Julian Kranz's avatar
Julian Kranz committed
655
656
  z <- fZF;
  cf <- fCF;
Julian Kranz's avatar
Julian Kranz committed
657
658
659
660
  t1 <- mktemp;
  t2 <- mktemp;
  t3 <- mktemp;
  zer0 <- zero;
Julian Kranz's avatar
Julian Kranz committed
661
662
663
664

  cmpltu sz ltu s0 s1;
  xorb sz t1 sum s0;
  xorb sz t2 sum s1;
Julian Kranz's avatar
Julian Kranz committed
665
666
  andb sz t3 (var t1) (var t2);
  cmplts sz ov (var t3) zer0;
Julian Kranz's avatar
Julian Kranz committed
667
668
  cmplts sz sf sum zer0;
  cmpeq sz eq sum zer0;
Julian Kranz's avatar
Julian Kranz committed
669
670
671
  xorb 1 lts (var sf) (var ov);
  orb 1 leu (var ltu) (var eq);
  orb 1 les (var lts) (var eq);
Julian Kranz's avatar
Julian Kranz committed
672
673
674
  cmpeq sz z sum zer0;

  # Hacker's Delight - Unsigned Add/Subtract
Julian Kranz's avatar
Julian Kranz committed
675
676
677
678
679
680
681
682
683
  if set-carry then (
    _if (/d carry) _then do
      cmpleu sz cf sum s0
    end _else do
      cmpltu sz cf sum s0
    end
  ) else
    return void
  ;
Julian Kranz's avatar
Julian Kranz committed
684

Julian Kranz's avatar
Julian Kranz committed
685
  emit-parity-flag sum;
Julian Kranz's avatar
Julian Kranz committed
686
  emit-arithmetic-adjust-flag sz sum s0 s1
Julian Kranz's avatar
Julian Kranz committed
687
end
mb0's avatar
Up.  
mb0 committed
688

Julian Kranz's avatar
Julian Kranz committed
689
val emit-sub-sbb-flags sz difference minuend subtrahend carry set-carry = do
Julian Kranz's avatar
Julian Kranz committed
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
  eq <- fEQ;
  les <- fLES;
  leu <- fLEU;
  lts <- fLTS;
  ltu <- fLTU;
  sf <- fSF;
  ov <- fOF;
  cf <- fCF;
  z <- fZF;
  t1 <- mktemp;
  t2 <- mktemp;
  t3 <- mktemp;
  zer0 <- zero;

  cmpltu sz ltu minuend subtrahend;
  cmpleu sz leu minuend subtrahend;
  cmplts sz lts minuend subtrahend;
  cmples sz les minuend subtrahend;
  cmpeq sz eq minuend subtrahend;
  cmplts sz sf difference zer0;
  xorb 1 ov (var lts) (var sf);
  cmpeq sz z difference zer0;

Julian Kranz's avatar
Julian Kranz committed
713
714
715
716
717
718
719
720
721
722
  if set-carry then (
    # Hacker's Delight - Unsigned Add/Subtract
    _if (/d carry) _then do
      cmpleu sz cf minuend subtrahend
    end _else do
      cmpltu sz cf minuend subtrahend
    end
  ) else
    return void
  ;
Julian Kranz's avatar
Julian Kranz committed
723

Julian Kranz's avatar
Julian Kranz committed
724
  emit-parity-flag difference;
Julian Kranz's avatar
Julian Kranz committed
725
726
  emit-arithmetic-adjust-flag sz difference minuend subtrahend
end
mb0's avatar
Up.  
mb0 committed
727

Julian Kranz's avatar
Julian Kranz committed
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
val emit-mul-flags sz product = do
  ov <- fOF;
  cf <- fCF;
  sf <- fSF;
  zf <- fZF;
  af <- fAF;
  pf <- fPF;

  sgn-ext <- mktemp;
  movsx sz sgn-ext 1 (var (at-offset product (sz + sz - 1)));

  cmpneq sz ov (var (at-offset product sz)) (var sgn-ext);
  mov 1 cf (var ov);

  undef 1 sf;
  undef 1 zf;
  undef 1 af;
  undef 1 pf
end

Julian Kranz's avatar
Julian Kranz committed
748
749
750
751
752
753
754
755
756
757
758
759
val move-to-rflags size lin = do
  flags <- rflags;

  in-mask <- return 0x0000000000245fd5;
  out-mask <- return 0xffffffffffc3a02a;

  temp <- mktemp;
  andb size temp lin (imm in-mask);
  andb size flags (var flags) (imm out-mask);
  orb size flags (var flags) (var temp)
end

Julian Kranz's avatar
Julian Kranz committed
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
val direction-adjust reg-size reg-sem for-size = do
  amount <-
    case for-size of
       8: return 1
     | 16: return 2
     | 32: return 4
     | 64: return 8
    end
  ;

  df <- fDF;
  _if (/not (var df)) _then
    add reg-size reg-sem (var reg-sem) (imm amount)  
  _else
    sub reg-size reg-sem (var reg-sem) (imm amount)
end

Julian Kranz's avatar
Julian Kranz committed
777
778
779
780
val divb x y =
  case x of
     8:
       case y of
Julian Kranz's avatar
Julian Kranz committed
781
782
          1: 8
        | 2: 4
Julian Kranz's avatar
Julian Kranz committed
783
784
785
786
787
        | 4: 2
        | 8: 1
       end
   | 16:
       case y of
Julian Kranz's avatar
Julian Kranz committed
788
789
          1: 16
        | 2: 8
Julian Kranz's avatar
Julian Kranz committed
790
791
792
793
794
795
        | 4: 4
        | 8: 2
        | 16: 1
       end
   | 32:
       case y of
Julian Kranz's avatar
Julian Kranz committed
796
797
          1: 32
        | 2: 16
Julian Kranz's avatar
Julian Kranz committed
798
799
800
801
802
803
804
        | 4: 8
        | 8: 4
        | 16: 2
        | 32: 1
       end
   | 64:
       case y of
Julian Kranz's avatar
Julian Kranz committed
805
806
          1: 64
        | 2: 32
Julian Kranz's avatar
Julian Kranz committed
807
808
809
810
811
812
813
814
        | 4: 16
        | 8: 8
        | 16: 4
        | 32: 2
        | 64: 1
       end
   | 128:
       case y of
Julian Kranz's avatar
Julian Kranz committed
815
816
          1: 128
        | 2: 64
Julian Kranz's avatar
Julian Kranz committed
817
818
819
820
821
822
823
824
825
        | 4: 32
        | 8: 16
        | 16: 8
        | 32: 4
        | 64: 2
        | 128: 1
       end
   | 256:
       case y of
Julian Kranz's avatar
Julian Kranz committed
826
827
          1: 256
        | 2: 128
Julian Kranz's avatar
Julian Kranz committed
828
829
830
831
832
833
834
835
        | 4: 64
        | 8: 32
        | 16: 16
        | 32: 8
        | 64: 4
        | 128: 2
        | 256: 1
       end
Julian Kranz's avatar
Julian Kranz committed
836
837
838
839
840
    | k:
       case y of
          1: k
	| k: 1
       end
Julian Kranz's avatar
Julian Kranz committed
841
842
  end
;
Julian Kranz's avatar
Julian Kranz committed
843
844
845
846
847
848
849
850
851
852
853
854
855

val logb x =
  case x of
     256: 8
   | 128: 7
   | 64: 6
   | 32: 5
   | 16: 4
   | 8: 3
   | 4: 2
   | 2: 1
   | 1: 0
  end
Julian Kranz's avatar
Julian Kranz committed
856

Julian Kranz's avatar
Julian Kranz committed
857
858
859
860
861
862
val exp base e =
  case e of
     0: 1
   | x: base * (exp base (e - 1))
  end

Julian Kranz's avatar
Julian Kranz committed
863
val vector-apply size element-size monad = do
Julian Kranz's avatar
Julian Kranz committed
864
  limit <- return (divb size element-size);
Julian Kranz's avatar
Julian Kranz committed
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879

  let
    val f i = do
      monad i;

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

Julian Kranz's avatar
Julian Kranz committed
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
#val avx-expand-dst x sem = do
#  sem;
# 
#  size <- sizeof1 x.opnd1;
#  out-size <- return
#    (case x.opnd1 of
#        REG r: 256
#      | _: size
#    end)
#  ;
#
#  if out-size > size then do
#    rest-size <- return (out-size - size);
#    
#    src <- read size x.opnd1;
#    dst <- lval out-size x.opnd1;
#
#    temp <- mktemp;
#    movzx out-size temp size src;
#
#    write out-size dst (var temp)
#  end else
#    return void
#end
Julian Kranz's avatar
Julian Kranz committed
904

Julian Kranz's avatar
Julian Kranz committed
905
val binop-signed-saturating operator size dst src1 src2 = do
Julian Kranz's avatar
Julian Kranz committed
906
907
908
909
910
  dst-ex <- mktemp;
  src1-ex <- mktemp;
  src2-ex <- mktemp;

  upper <- return (
Julian Kranz's avatar
Julian Kranz committed
911
912
913
914
    case size of
       8: 0x7f
     | 16: 0x7fff
    end
Julian Kranz's avatar
Julian Kranz committed
915
916
  );
  lower <- return (
Julian Kranz's avatar
Julian Kranz committed
917
918
919
920
    case size of
       8: (0-0x80)
     | 16: (0-0x8000)
    end
Julian Kranz's avatar
Julian Kranz committed
921
922
923
924
  );

  movsx (size + 1) src1-ex size src1;
  movsx (size + 1) src2-ex size src2;
Julian Kranz's avatar
Julian Kranz committed
925
  operator (size + 1) dst-ex (var src1-ex) (var src2-ex);
Julian Kranz's avatar
Julian Kranz committed
926
927
928
929
930
931
932
933
934
935
  
  _if (/gts (size + 1) (var dst-ex) (imm upper)) _then (
    mov size dst (imm upper)
  ) _else ( _if (/lts (size + 1) (var dst-ex) (imm lower)) _then
    mov size dst (imm lower)
  _else
    mov size dst (var dst-ex)
  )
end

Julian Kranz's avatar
Julian Kranz committed
936
937
938
val add-signed-saturating size dst src1 src2 = binop-signed-saturating add size dst src1 src2
val sub-signed-saturating size dst src1 src2 = binop-signed-saturating sub size dst src1 src2

Julian Kranz's avatar
Julian Kranz committed
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
val binop-unsigned-saturating operator comparer limit size dst src1 src2 = do
  operator size dst src1 src2;
 
  _if (comparer size (var dst) src1) _then (
    mov size dst (imm limit)
  )
end

val add-unsigned-saturating size dst src1 src2 = do
  limit <- return (
    case size of
       8: 0xff
     | 16: 0xffff
    end
  );
  binop-unsigned-saturating add /ltu limit size dst src1 src2
end

val sub-unsigned-saturating size dst src1 src2 = binop-unsigned-saturating sub /gtu 0 size dst src1 src2

Julian Kranz's avatar
Julian Kranz committed
959
960
val semantics insn =
  case insn of
Julian Kranz's avatar
Julian Kranz committed
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
     AAA x: sem-undef-arity0 x
   | AAD x: sem-undef-arity1 x
   | AAM x: sem-undef-arity1 x
   | AAS x: sem-undef-arity0 x
   | ADC x: sem-adc x
   | ADD x: sem-add x
   | ADDPD x: sem-undef-arity2 x
   | ADDPS x: sem-undef-arity2 x
   | ADDSD x: sem-undef-arity2 x
   | ADDSS x: sem-undef-arity2 x
   | ADDSUBPD x: sem-undef-arity2 x
   | ADDSUBPS x: sem-undef-arity2 x
   | AESDEC x: sem-undef-arity2 x
   | AESDECLAST x: sem-undef-arity2 x
   | AESENC x: sem-undef-arity2 x
   | AESENCLAST x: sem-undef-arity2 x
   | AESIMC x: sem-undef-arity2 x
   | AESKEYGENASSIST x: sem-undef-arity3 x
Julian Kranz's avatar
Julian Kranz committed
979
   | AND x: sem-and x
Julian Kranz's avatar
Julian Kranz committed
980
   | ANDNPD x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
981
   | ANDNPS x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
982
   | ANDPD x: sem-andpd x
Julian Kranz's avatar
Julian Kranz committed
983
984
985
986
987
988
989
   | ANDPS x: sem-undef-arity2 x
   | ARPL x: sem-undef-arity2 x
   | BLENDPD x: sem-undef-arity3 x
   | BLENDPS x: sem-undef-arity3 x
   | BLENDVPD x: sem-undef-arity3 x
   | BLENDVPS x: sem-undef-arity3 x
   | BOUND x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
990
   | BSF x: sem-bsf x
Julian Kranz's avatar
Julian Kranz committed
991
992
   | BSR x: sem-bsr x
   | BSWAP x: sem-bswap x
Julian Kranz's avatar
Julian Kranz committed
993
994
995
996
   | BT x: sem-bt x sem-bt-none
   | BTC x: sem-bt x sem-bt-complement
   | BTR x: sem-bt x sem-bt-reset
   | BTS x: sem-bt x sem-bt-set
Julian Kranz's avatar
Julian Kranz committed
997
   | CALL x: sem-call x
Julian Kranz's avatar
Julian Kranz committed
998
   | CBW x: sem-convert 8
Julian Kranz's avatar
Julian Kranz committed
999
   | CDQ x: sem-cwd-cdq-cqo x
Julian Kranz's avatar
Julian Kranz committed
1000
   | CDQE x: sem-convert 32