x86-rreil-translator.ml 53.4 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
15
16
17
val ip-get = do
  return (imm 0)
end

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

Julian Kranz's avatar
Julian Kranz committed
29
val sizeof2 dst/src1 src2 =
mb0's avatar
Up.  
mb0 committed
30
31
32
33
34
35
36
37
38
39
   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
40
41
42
43
44
45
46
47
48
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
49

Julian Kranz's avatar
Julian Kranz committed
50
val sizeof1 op =
mb0's avatar
Up.  
mb0 committed
51
52
53
54
55
56
57
58
59
   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
60
61
62
63
type signedness =
   Signed
 | Unsigned

Julian Kranz's avatar
Julian Kranz committed
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
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
80
in
Julian Kranz's avatar
Julian Kranz committed
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
  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
97
end
Julian Kranz's avatar
Julian Kranz committed
98

Julian Kranz's avatar
Julian Kranz committed
99
100
101
102
103
#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
104
  mode64 <- mode64?;
Julian Kranz's avatar
Julian Kranz committed
105

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

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
123
#val segment segment = do
Julian Kranz's avatar
Julian Kranz committed
124
125
126
127
128
129
130
131
132
133
134
135
#  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
136
137
#  return DS
#end
Julian Kranz's avatar
Julian Kranz committed
138

Julian Kranz's avatar
Julian Kranz committed
139
val conv-with conv sz x =
mb0's avatar
Up.  
mb0 committed
140
   let
Julian Kranz's avatar
Julian Kranz committed
141
142
143
144
145
      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
146
147
148
149
      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
150

Julian Kranz's avatar
Julian Kranz committed
151
      val conv-sum conv sz x =
mb0's avatar
Up.  
mb0 committed
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
         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
174
      val conv-mem x = conv-with Signed x.psz x.opnd
mb0's avatar
Up.  
mb0 committed
175
176
177
178
179
180
   in
      case x of
         IMM8 x: conv-imm conv x
       | IMM16 x: conv-imm conv x
       | IMM32 x: conv-imm conv x
       | IMM64 x: conv-imm conv x
Julian Kranz's avatar
Julian Kranz committed
181
       | REG x: conv-reg conv sz x
mb0's avatar
Up.  
mb0 committed
182
183
184
       | SUM x: conv-sum conv sz x
       | SCALE x: conv-scale conv sz x
       | MEM x:
Julian Kranz's avatar
Julian Kranz committed
185
           do
Julian Kranz's avatar
Julian Kranz committed
186
187
	     t <- mktemp;
             address <- conv-mem x;
Julian Kranz's avatar
Julian Kranz committed
188
189
             segmented-load x.sz t x.psz address x.segment;
             expand conv (var t) x.sz sz
Julian Kranz's avatar
Julian Kranz committed
190
           end
mb0's avatar
Up.  
mb0 committed
191
192
193
      end
   end

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

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

Julian Kranz's avatar
Julian Kranz committed
205
206
207
208
209
210
211
212
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
213
214
215
216
217
218
219
220
221
222
223
224
225
226
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
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
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
250
#Todo: MEM => byte offset, REG => bit offset... confusing (division?)
Julian Kranz's avatar
Julian Kranz committed
251
val lval-offset sz x offset =
mb0's avatar
Up.  
mb0 committed
252
   case x of
Julian Kranz's avatar
Julian Kranz committed
253
254
     MEM x:
       do
Julian Kranz's avatar
Julian Kranz committed
255
         #Offset for memory operands? => Add offset to pointer
Julian Kranz's avatar
Julian Kranz committed
256
         address <- conv-with Signed x.psz x.opnd;
Julian Kranz's avatar
Julian Kranz committed
257
258
	 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
259
       end
Julian Kranz's avatar
Julian Kranz committed
260
    | REG r:
Julian Kranz's avatar
Julian Kranz committed
261
       do 
Julian Kranz's avatar
Julian Kranz committed
262
         id <- return (semantic-register-of-operand-with-size x sz);
Julian Kranz's avatar
Julian Kranz committed
263
264
265
	 id <- return (@{offset=id.offset + offset} id);
         return (SEM_WRITE_VAR{size= $size id,id=id})
       end
mb0's avatar
Up.  
mb0 committed
266
267
   end

Julian Kranz's avatar
Julian Kranz committed
268

Julian Kranz's avatar
Julian Kranz committed
269
270
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
271
272
273
274
275
276
277

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

Julian Kranz's avatar
Julian Kranz committed
278
val write-extend avx-encoded sz a b =
mb0's avatar
Up.  
mb0 committed
279
280
   case a of
      SEM_WRITE_MEM x:
Julian Kranz's avatar
Julian Kranz committed
281
         #store x (SEM_LIN{size=sz,opnd1=b})
Julian Kranz's avatar
Julian Kranz committed
282
	 segmented-store x (SEM_LIN{size=sz,opnd1=b}) x.segment
Julian Kranz's avatar
Julian Kranz committed
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
    | 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
301
302
303
	mov sz x.id b;

	mode64 <- mode64?;
Julian Kranz's avatar
Julian Kranz committed
304
305
	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
306
307
308
309
310
311
	  #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
312

Julian Kranz's avatar
Julian Kranz committed
313
314
315
316
317
318
319
320
321
322
323
324
325
#        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
326
327
   end

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

Julian Kranz's avatar
Julian Kranz committed
330
331
332
333
334
335
336
337
338
339
340
341
342
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
343
344
345
346
347
348
349
350
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
351
352
353
354
355
356
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
357
358
359

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

Julian Kranz's avatar
Julian Kranz committed
360
val _if c _then a _else b = do
Julian Kranz's avatar
Julian Kranz committed
361
  c <- c;
Julian Kranz's avatar
Julian Kranz committed
362
363
364
  stack <- pop-all;
  a;
  t <- pop-all;
Julian Kranz's avatar
Julian Kranz committed
365
  t <- return (rreil-stmts-rev t);
Julian Kranz's avatar
Julian Kranz committed
366
367
  b;
  e <- pop-all;
Julian Kranz's avatar
Julian Kranz committed
368
  e <- return (rreil-stmts-rev e);
Julian Kranz's avatar
Julian Kranz committed
369
  stack-set stack;
Julian Kranz's avatar
Julian Kranz committed
370
  ite c t e
Julian Kranz's avatar
Julian Kranz committed
371
372
373
374
375
376
377
378
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
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
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
401
402
403
404
405
406
407
408
409
410
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
411
412
end

Julian Kranz's avatar
Julian Kranz committed
413
414
415
416
417
418
419
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
420
421
422
423
424
425
426
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
427
428
429
430
431
432
433
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
434
435
436
437
438
439
val /lts sz a b = do
  t <- mktemp;
  cmplts sz t a b;
  return (var t)
end

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

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

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

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

Julian Kranz's avatar
Julian Kranz committed
468
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
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
570
val undef-opnd opnd = do
Julian Kranz's avatar
Julian Kranz committed
571
  sz <- sizeof1 opnd;
Julian Kranz's avatar
Julian Kranz committed
572
  a <- lval sz opnd;
Julian Kranz's avatar
Julian Kranz committed
573
  t <- mktemp;
Julian Kranz's avatar
Julian Kranz committed
574
  write sz a (var t)
Julian Kranz's avatar
Julian Kranz committed
575
576
577
578
579
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
580
   | MEM m: undef-opnd x.opnd1
Julian Kranz's avatar
Julian Kranz committed
581
582
583
  end
end

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

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

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

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

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

val sem-undef-varity x = do
Julian Kranz's avatar
Julian Kranz committed
605
606
607
608
609
610
  case x of
     VA1 x: sem-undef-arity1 x
   | 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
611
612
613
end

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

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

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

  pf <- fPF;
Julian Kranz's avatar
Julian Kranz committed
624
625
626
627
628
629
630
631
  # 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
632
633
end

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

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

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

  cmpltu sz ltu s0 s1;
  xorb sz t1 sum s0;
  xorb sz t2 sum s1;
Julian Kranz's avatar
Julian Kranz committed
663
664
  andb sz t3 (var t1) (var t2);
  cmplts sz ov (var t3) zer0;
Julian Kranz's avatar
Julian Kranz committed
665
666
  cmplts sz sf sum zer0;
  cmpeq sz eq sum zer0;
Julian Kranz's avatar
Julian Kranz committed
667
668
669
  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
670
671
672
  cmpeq sz z sum zer0;

  # Hacker's Delight - Unsigned Add/Subtract
Julian Kranz's avatar
Julian Kranz committed
673
674
675
676
677
678
679
680
681
  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
682

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

Julian Kranz's avatar
Julian Kranz committed
687
val emit-sub-sbb-flags sz difference minuend subtrahend carry set-carry = do
Julian Kranz's avatar
Julian Kranz committed
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
  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
711
712
713
714
715
716
717
718
719
720
  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
721

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

Julian Kranz's avatar
Julian Kranz committed
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
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
746
747
748
749
750
751
752
753
754
755
756
757
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
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
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
775
776
777
778
val divb x y =
  case x of
     8:
       case y of
Julian Kranz's avatar
Julian Kranz committed
779
780
          1: 8
        | 2: 4
Julian Kranz's avatar
Julian Kranz committed
781
782
783
784
785
        | 4: 2
        | 8: 1
       end
   | 16:
       case y of
Julian Kranz's avatar
Julian Kranz committed
786
787
          1: 16
        | 2: 8
Julian Kranz's avatar
Julian Kranz committed
788
789
790
791
792
793
        | 4: 4
        | 8: 2
        | 16: 1
       end
   | 32:
       case y of
Julian Kranz's avatar
Julian Kranz committed
794
795
          1: 32
        | 2: 16
Julian Kranz's avatar
Julian Kranz committed
796
797
798
799
800
801
802
        | 4: 8
        | 8: 4
        | 16: 2
        | 32: 1
       end
   | 64:
       case y of
Julian Kranz's avatar
Julian Kranz committed
803
804
          1: 64
        | 2: 32
Julian Kranz's avatar
Julian Kranz committed
805
806
807
808
809
810
811
812
        | 4: 16
        | 8: 8
        | 16: 4
        | 32: 2
        | 64: 1
       end
   | 128:
       case y of
Julian Kranz's avatar
Julian Kranz committed
813
814
          1: 128
        | 2: 64
Julian Kranz's avatar
Julian Kranz committed
815
816
817
818
819
820
821
822
823
        | 4: 32
        | 8: 16
        | 16: 8
        | 32: 4
        | 64: 2
        | 128: 1
       end
   | 256:
       case y of
Julian Kranz's avatar
Julian Kranz committed
824
825
          1: 256
        | 2: 128
Julian Kranz's avatar
Julian Kranz committed
826
827
828
829
830
831
832
833
        | 4: 64
        | 8: 32
        | 16: 16
        | 32: 8
        | 64: 4
        | 128: 2
        | 256: 1
       end
Julian Kranz's avatar
Julian Kranz committed
834
835
836
837
838
    | k:
       case y of
          1: k
	| k: 1
       end
Julian Kranz's avatar
Julian Kranz committed
839
840
  end
;
Julian Kranz's avatar
Julian Kranz committed
841
842
843
844
845
846
847
848
849
850
851
852
853

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
854

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

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

  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
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
#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
902

Julian Kranz's avatar
Julian Kranz committed
903
val binop-signed-saturating operator size dst src1 src2 = do
Julian Kranz's avatar
Julian Kranz committed
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
  dst-ex <- mktemp;
  src1-ex <- mktemp;
  src2-ex <- mktemp;

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

  movsx (size + 1) src1-ex size src1;
  movsx (size + 1) src2-ex size src2;
Julian Kranz's avatar
Julian Kranz committed
923
  operator (size + 1) dst-ex (var src1-ex) (var src2-ex);
Julian Kranz's avatar
Julian Kranz committed
924
925
926
927
928
929
930
931
932
933
  
  _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
934
935
936
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
937
938
val semantics insn =
  case insn of
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
     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
   | AND x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
958
   | ANDNPD x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
959
   | ANDNPS x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
960
   | ANDPD x: sem-andpd x
Julian Kranz's avatar
Julian Kranz committed
961
962
963
964
965
966
967
   | 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
968
   | BSF x: sem-bsf x
Julian Kranz's avatar
Julian Kranz committed
969
970
   | BSR x: sem-bsr x
   | BSWAP x: sem-bswap x
Julian Kranz's avatar
Julian Kranz committed
971
972
973
974
   | 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
975
   | CALL x: sem-call x
Julian Kranz's avatar
Julian Kranz committed
976
   | CBW x: sem-convert 8
Julian Kranz's avatar
Julian Kranz committed
977
   | CDQ x: sem-cwd-cdq-cqo x
Julian Kranz's avatar
Julian Kranz committed
978
   | CDQE x: sem-convert 32
Julian Kranz's avatar
Julian Kranz committed
979
980
981
982
983
   | CLC x: sem-undef-arity0 x
   | CLD x: sem-undef-arity0 x
   | CLFLUSH x: sem-undef-arity1 x
   | CLI x: sem-undef-arity0 x
   | CLTS x: sem-undef-arity0 x
Julian Kranz's avatar
Julian Kranz committed
984
   | CMC x: sem-cmc
Julian Kranz's avatar
Julian Kranz committed
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
   | CMOVA x: sem-a sem-cmovcc x
   | CMOVAE x: sem-ae sem-cmovcc x
   | CMOVB x: sem-b sem-cmovcc x
   | CMOVBE x: sem-be sem-cmovcc x
   | CMOVC x: sem-c sem-cmovcc x
   | CMOVE x: sem-e sem-cmovcc x
   | CMOVG x: sem-g sem-cmovcc x
   | CMOVGE x: sem-ge sem-cmovcc x
   | CMOVL x: sem-l sem-cmovcc x
   | CMOVLE x: sem-le sem-cmovcc x
   | CMOVNA x: sem-na sem-cmovcc x
   | CMOVNAE x: sem-nae sem-cmovcc x
   | CMOVNB x: sem-nb sem-cmovcc x
   | CMOVNBE x: sem-nbe sem-cmovcc x
   | CMOVNC x: sem-nc sem-cmovcc x
   | CMOVNE x: sem-ne sem-cmovcc x