x86-rreil-translator.ml 55.5 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
val expand expanded conv lin from-sz to-sz =
Julian Kranz's avatar
Julian Kranz committed
66
  if from-sz === to-sz then
Julian Kranz's avatar
Julian Kranz committed
67
    mov to-sz expanded lin
Julian Kranz's avatar
Julian Kranz committed
68
  else
Julian Kranz's avatar
Julian Kranz committed
69 70 71
    case conv of
       Signed: movsx to-sz expanded from-sz lin
     | Unsigned: movzx to-sz expanded from-sz lin
Julian Kranz's avatar
Julian Kranz committed
72 73 74 75
    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
76
in
Julian Kranz's avatar
Julian Kranz committed
77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92
  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
93
end
Julian Kranz's avatar
Julian Kranz committed
94

Julian Kranz's avatar
Julian Kranz committed
95 96 97 98 99
#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
100
  mode64 <- mode64?;
Julian Kranz's avatar
Julian Kranz committed
101

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

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

Julian Kranz's avatar
Julian Kranz committed
136
val conv-with conv sz x =
mb0's avatar
Up.  
mb0 committed
137
   let
Julian Kranz's avatar
Julian Kranz committed
138 139 140 141 142
      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
143 144
      val conv-reg conv sz r = do
        reg <- return (semantic-register-of r);
Julian Kranz's avatar
Julian Kranz committed
145 146 147
	expanded <- mktemp;
	expand expanded conv (var reg) reg.size sz;
	return (var expanded)
Julian Kranz's avatar
Julian Kranz committed
148
      end
mb0's avatar
Up.  
mb0 committed
149

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

Julian Kranz's avatar
Julian Kranz committed
195 196 197 198
	     expanded <- mktemp;
	     with-subscope (m expanded);
	     return (var expanded)
           end end
mb0's avatar
Up.  
mb0 committed
199 200 201
      end
   end

Julian Kranz's avatar
Julian Kranz committed
202
val read sz x = conv-with Unsigned sz x
Julian Kranz's avatar
Julian Kranz committed
203
val reads conv sz x = conv-with conv sz x
Julian Kranz's avatar
Julian Kranz committed
204

Julian Kranz's avatar
Julian Kranz committed
205 206
val extract-imm-unsigned imm =
  case imm of
Julian Kranz's avatar
*  
Julian Kranz committed
207 208 209 210
     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
211 212
 end

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

Julian Kranz's avatar
Julian Kranz committed
276

Julian Kranz's avatar
Julian Kranz committed
277 278
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
279 280 281 282 283 284 285

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

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

	mode64 <- mode64?;
Julian Kranz's avatar
Julian Kranz committed
312 313
	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
314 315 316 317 318 319
	  #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
320

Julian Kranz's avatar
Julian Kranz committed
321 322 323 324 325 326 327 328 329 330 331 332 333
#        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
334 335
   end

Julian Kranz's avatar
Julian Kranz committed
336 337
val write sz a b = write-extend '0' sz a b

Julian Kranz's avatar
Julian Kranz committed
338 339 340 341 342 343 344 345 346 347 348 349 350
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
351 352 353 354 355 356 357 358
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
359 360 361 362 363 364
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
365 366 367

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

Julian Kranz's avatar
Julian Kranz committed
368
val _if c _then a _else b = do
Julian Kranz's avatar
Julian Kranz committed
369
  c <- with-subscope c;
Julian Kranz's avatar
Julian Kranz committed
370
  stack <- pop-all;
Julian Kranz's avatar
Julian Kranz committed
371
  with-subscope a;
Julian Kranz's avatar
Julian Kranz committed
372
  t <- pop-all;
Julian Kranz's avatar
Julian Kranz committed
373
  t <- return (rreil-stmts-rev t);
Julian Kranz's avatar
Julian Kranz committed
374
  with-subscope b;
Julian Kranz's avatar
Julian Kranz committed
375
  e <- pop-all;
Julian Kranz's avatar
Julian Kranz committed
376
  e <- return (rreil-stmts-rev e);
Julian Kranz's avatar
Julian Kranz committed
377
  stack-set stack;
Julian Kranz's avatar
Julian Kranz committed
378
  ite c t e
Julian Kranz's avatar
Julian Kranz committed
379 380 381 382 383 384
end

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

Julian Kranz's avatar
Julian Kranz committed
385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404
val _while c __ b = let
  val eval-cond ct = do
    cc <- c;
    mov 1 ct cc
  end
in do
  ct <- mktemp;
  with-subscope (eval-cond ct);
  stack <- pop-all;
  
  with-subscope b;

  with-subscope (eval-cond ct);
  body <- pop-all;
  body <- return (rreil-stmts-rev body);

  stack-set stack;
  while (var ct) body
end end

Julian Kranz's avatar
Julian Kranz committed
405 406
val /d cond = return cond

Julian Kranz's avatar
Julian Kranz committed
407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428
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
429 430 431 432 433 434 435 436 437 438
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
439 440
end

Julian Kranz's avatar
Julian Kranz committed
441 442 443 444 445 446 447
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
448 449 450 451 452 453 454
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
455 456 457 458 459 460 461
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
462 463 464 465 466 467
val /lts sz a b = do
  t <- mktemp;
  cmplts sz t a b;
  return (var t)
end

Julian Kranz's avatar
Julian Kranz committed
468 469 470 471 472 473
val /ltu sz a b = do
  t <- mktemp;
  cmpltu sz t a b;
  return (var t)
end

Julian Kranz's avatar
Julian Kranz committed
474 475 476 477 478 479
val /leu sz a b = do
  t <- mktemp;
  cmpleu sz t a b;
  return (var t)
end

Julian Kranz's avatar
Julian Kranz committed
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 571 572 573 574 575 576 577 578 579 580 581
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
582
val undef-opnd opnd = do
Julian Kranz's avatar
Julian Kranz committed
583
  sz <- sizeof1 opnd;
Julian Kranz's avatar
Julian Kranz committed
584
  a <- lval sz opnd;
Julian Kranz's avatar
Julian Kranz committed
585
  t <- mktemp;
Julian Kranz's avatar
Julian Kranz committed
586
  write sz a (var t)
Julian Kranz's avatar
Julian Kranz committed
587 588 589 590 591
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
592
   | MEM m: undef-opnd x.opnd1
Julian Kranz's avatar
Julian Kranz committed
593 594 595
  end
end

Julian Kranz's avatar
Julian Kranz committed
596
val sem-undef-arity0 x = do
Julian Kranz's avatar
Julian Kranz committed
597
  return void
Julian Kranz's avatar
Julian Kranz committed
598 599 600
end

val sem-undef-arity1 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-arity2 x = do
Julian Kranz's avatar
Julian Kranz committed
605
  sem-undef-arity-ge1 x
Julian Kranz's avatar
Julian Kranz committed
606 607 608
end

val sem-undef-arity3 x = do
Julian Kranz's avatar
Julian Kranz committed
609
  sem-undef-arity-ge1 x
Julian Kranz's avatar
Julian Kranz committed
610 611 612
end

val sem-undef-arity4 x = do
Julian Kranz's avatar
Julian Kranz committed
613
  sem-undef-arity-ge1 x
Julian Kranz's avatar
Julian Kranz committed
614 615 616
end

val sem-undef-varity x = do
Julian Kranz's avatar
Julian Kranz committed
617
  case x of
Julian Kranz's avatar
Julian Kranz committed
618 619
     VA0 x: sem-undef-arity0 x
   | VA1 x: sem-undef-arity1 x
Julian Kranz's avatar
Julian Kranz committed
620 621 622 623
   | 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
624 625 626
end

val sem-undef-flow1 x = do
Julian Kranz's avatar
Julian Kranz committed
627
  return void
Julian Kranz's avatar
Julian Kranz committed
628 629
end

Julian Kranz's avatar
Julian Kranz committed
630
val emit-parity-flag r = do
Julian Kranz's avatar
Julian Kranz committed
631 632
  byte-size <- return 8;

Julian Kranz's avatar
Julian Kranz committed
633
  low-byte <- mktemp;
Julian Kranz's avatar
Julian Kranz committed
634
  mov byte-size low-byte r;
Julian Kranz's avatar
Julian Kranz committed
635 636

  pf <- fPF;
Julian Kranz's avatar
Julian Kranz committed
637 638 639 640 641 642 643 644
  # 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
645 646
end

Julian Kranz's avatar
Julian Kranz committed
647
val emit-arithmetic-adjust-flag sz r op0 op1 = do
Julian Kranz's avatar
Julian Kranz committed
648 649
  # Hacker's Delight - How the Computer Sets Overflow for Signed Add/Subtract
  t <- mktemp;
Julian Kranz's avatar
Julian Kranz committed
650 651
  xorb sz t r op0;
  xorb sz t (var t) op1;
Julian Kranz's avatar
Julian Kranz committed
652 653 654 655

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

Julian Kranz's avatar
Julian Kranz committed
658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685
val emit-add-adc-flags sz sum s0 s1 carry set-carry = let
  val emit = do
    eq <- fEQ;
    les <- fLES;
    leu <- fLEU;
    lts <- fLTS;
    ltu <- fLTU;
    sf <- fSF;
    ov <- fOF;
    z <- fZF;
    cf <- fCF;
    t1 <- mktemp;
    t2 <- mktemp;
    t3 <- mktemp;
    zer0 <- zero;
  
    cmpltu sz ltu s0 s1;
    xorb sz t1 sum s0;
    xorb sz t2 sum s1;
    andb sz t3 (var t1) (var t2);
    cmplts sz ov (var t3) zer0;
    cmplts sz sf sum zer0;
    cmpeq sz eq sum zer0;
    xorb 1 lts (var sf) (var ov);
    orb 1 leu (var ltu) (var eq);
    orb 1 les (var lts) (var eq);
    cmpeq sz z sum zer0;
  
Julian Kranz's avatar
Julian Kranz committed
686
    # Hacker's Delight - Unsigned Add/Subtract
Julian Kranz's avatar
Julian Kranz committed
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 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744
    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
    ;
  
    emit-parity-flag sum;
    emit-arithmetic-adjust-flag sz sum s0 s1
  end
in
  with-subscope emit
end

val emit-sub-sbb-flags sz difference minuend subtrahend carry set-carry = let
  val emit = do
    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;
  
    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
    ;
  
    emit-parity-flag difference;
    emit-arithmetic-adjust-flag sz difference minuend subtrahend
  end
in
  with-subscope emit
Julian Kranz's avatar
Julian Kranz committed
745
end
mb0's avatar
Up.  
mb0 committed
746

Julian Kranz's avatar
Julian Kranz committed
747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768
val emit-mul-flags sz product = let
  val emit = 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
in
  with-subscope emit
Julian Kranz's avatar
Julian Kranz committed
769 770
end

Julian Kranz's avatar
Julian Kranz committed
771 772 773 774 775 776 777 778 779 780 781 782 783 784
val move-to-rflags size lin = let
  val emit = 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
in
  with-subscope emit
Julian Kranz's avatar
Julian Kranz committed
785 786
end

Julian Kranz's avatar
Julian Kranz committed
787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803
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
804 805 806 807
val divb x y =
  case x of
     8:
       case y of
Julian Kranz's avatar
Julian Kranz committed
808 809
          1: 8
        | 2: 4
Julian Kranz's avatar
Julian Kranz committed
810 811 812 813 814
        | 4: 2
        | 8: 1
       end
   | 16:
       case y of
Julian Kranz's avatar
Julian Kranz committed
815 816
          1: 16
        | 2: 8
Julian Kranz's avatar
Julian Kranz committed
817 818 819 820 821 822
        | 4: 4
        | 8: 2
        | 16: 1
       end
   | 32:
       case y of
Julian Kranz's avatar
Julian Kranz committed
823 824
          1: 32
        | 2: 16
Julian Kranz's avatar
Julian Kranz committed
825 826 827 828 829 830 831
        | 4: 8
        | 8: 4
        | 16: 2
        | 32: 1
       end
   | 64:
       case y of
Julian Kranz's avatar
Julian Kranz committed
832 833
          1: 64
        | 2: 32
Julian Kranz's avatar
Julian Kranz committed
834 835 836 837 838 839 840 841
        | 4: 16
        | 8: 8
        | 16: 4
        | 32: 2
        | 64: 1
       end
   | 128:
       case y of
Julian Kranz's avatar
Julian Kranz committed
842 843
          1: 128
        | 2: 64
Julian Kranz's avatar
Julian Kranz committed
844 845 846 847 848 849 850 851 852
        | 4: 32
        | 8: 16
        | 16: 8
        | 32: 4
        | 64: 2
        | 128: 1
       end
   | 256:
       case y of
Julian Kranz's avatar
Julian Kranz committed
853 854
          1: 256
        | 2: 128
Julian Kranz's avatar
Julian Kranz committed
855 856 857 858 859 860 861 862
        | 4: 64
        | 8: 32
        | 16: 16
        | 32: 8
        | 64: 4
        | 128: 2
        | 256: 1
       end
Julian Kranz's avatar
Julian Kranz committed
863 864 865 866 867
    | k:
       case y of
          1: k
	| k: 1
       end
Julian Kranz's avatar
Julian Kranz committed
868 869
  end
;
Julian Kranz's avatar
Julian Kranz committed
870 871 872 873 874 875 876 877 878 879 880 881 882

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
883

Julian Kranz's avatar
Julian Kranz committed
884 885 886 887 888 889
val exp base e =
  case e of
     0: 1
   | x: base * (exp base (e - 1))
  end

Julian Kranz's avatar
Julian Kranz committed
890
val vector-apply size element-size monad = do
Julian Kranz's avatar
Julian Kranz committed
891
  limit <- return (divb size element-size);
Julian Kranz's avatar
Julian Kranz committed
892 893 894

  let
    val f i = do
Julian Kranz's avatar
Julian Kranz committed
895
      with-subscope (monad i);
Julian Kranz's avatar
Julian Kranz committed
896 897 898 899 900 901 902 903 904 905 906

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

Julian Kranz's avatar
Julian Kranz committed
907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930
#val 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
931

Julian Kranz's avatar
Julian Kranz committed
932
val binop-signed-saturating operator size dst src1 src2 = do
Julian Kranz's avatar
Julian Kranz committed
933 934 935 936 937
  dst-ex <- mktemp;
  src1-ex <- mktemp;
  src2-ex <- mktemp;

  upper <- return (
Julian Kranz's avatar
Julian Kranz committed
938 939 940 941
    case size of
       8: 0x7f
     | 16: 0x7fff
    end
Julian Kranz's avatar
Julian Kranz committed
942 943
  );
  lower <- return (
Julian Kranz's avatar
Julian Kranz committed
944 945 946 947
    case size of
       8: (0-0x80)
     | 16: (0-0x8000)
    end
Julian Kranz's avatar
Julian Kranz committed
948 949 950 951
  );

  movsx (size + 1) src1-ex size src1;
  movsx (size + 1) src2-ex size src2;
Julian Kranz's avatar
Julian Kranz committed
952
  operator (size + 1) dst-ex (var src1-ex) (var src2-ex);
Julian Kranz's avatar
Julian Kranz committed
953 954 955 956 957 958 959 960 961 962
  
  _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
963 964 965
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
966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985
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
986 987
val semantics insn =
  case insn of
Julian Kranz's avatar
Julian Kranz committed
988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005
     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
1006
   | AND x: sem-and x
Julian Kranz's avatar
Julian Kranz committed
1007
   | ANDNPD x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
1008
   | ANDNPS x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
1009
   | ANDPD x: sem-andpd x
Julian Kranz's avatar
Julian Kranz committed
1010 1011 1012 1013 1014 1015 1016
   | 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
1017
   | BSF x: sem-bsf x
Julian Kranz's avatar
Julian Kranz committed
1018 1019
   | BSR x: sem-bsr x
   | BSWAP x: sem-bswap x
Julian Kranz's avatar
Julian Kranz committed
1020 1021 1022 1023
   | 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
1024
   | CALL x: sem-call x
Julian Kranz's avatar
Julian Kranz committed
1025
   | CBW x: sem-convert 8
Julian Kranz's avatar
Julian Kranz committed
1026
   | CDQ x: sem-cwd-cdq-cqo x
Julian Kranz's avatar
Julian Kranz committed
1027
   | CDQE x: sem-convert 32
Julian Kranz's avatar
Julian Kranz committed
1028 1029 1030 1031 1032
   | 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
1033
   | CMC x: sem-cmc
Julian Kranz's avatar
Julian Kranz committed
1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066
   | 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
   | CMOVNG x: sem-ng sem-cmovcc x
   | CMOVNGE x: sem-nge sem-cmovcc x
   | CMOVNL x: sem-nl sem-cmovcc x
   | CMOVNLE x: sem-nle sem-cmovcc x
   | CMOVNO x: sem-no sem-cmovcc x
   | CMOVNP x: sem-np sem-cmovcc x
   | CMOVNS x: sem-ns sem-cmovcc x
   | CMOVNZ x: sem-nz sem-cmovcc x
   | CMOVO x: sem-o sem-cmovcc x
   | CMOVP x: sem-p sem-cmovcc x
   | CMOVPE x: sem-pe sem-cmovcc x
   | CMOVPO x: sem-po sem-cmovcc x
   | CMOVS x: sem-s sem-cmovcc x
   | CMOVZ x: sem-z sem-cmovcc x
   | CMP x: sem-cmp x
   | CMPPD x: sem-undef-arity3 x
   | CMPPS x: sem-undef-arity3 x
Julian Kranz's avatar
Julian Kranz committed
1067
   | CMPS x: sem-repe-repne-insn x sem-cmps
Julian Kranz's avatar
Julian Kranz committed
1068 1069 1070 1071 1072 1073 1074 1075
   | CMPSD x: sem-undef-arity3 x
#   | CMPSD x:
#       case x of
#         VA0: sem-cmpsd
#       | _ x: sem-undef-arity0 x
#      end
#   | CMPSQ x: sem-undef-arity0 x
   | CMPSS x: sem-undef-arity3 x
Julian Kranz's avatar
Julian Kranz committed
1076
   | CMPXCHG x: sem-cmpxchg x
Julian Kranz's avatar
Julian Kranz committed
1077 1078
   | CMPXCHG16B x: sem-cmpxchg16b-cmpxchg8b x
   | CMPXCHG8B x: sem-cmpxchg16b-cmpxchg8b x
Julian Kranz's avatar
Julian Kranz committed
1079 1080
   | COMISD x: sem-undef-arity2 x
   | COMISS x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
1081
   | CPUID x: sem-cpuid x
Julian Kranz's avatar
Julian Kranz committed
1082
   | CQO x: sem-cwd-cdq-cqo x
Julian Kranz's avatar
Julian Kranz committed
1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105
   | CRC32 x: sem-undef-arity2 x
   | CVTDQ2PD x: sem-undef-arity2 x
   | CVTDQ2PS x: sem-undef-arity2 x
   | CVTPD2DQ x: sem-undef-arity2 x
   | CVTPD2PI x: sem-undef-arity2 x
   | CVTPD2PS x: sem-undef-arity2 x
   | CVTPI2PD x: sem-undef-arity2 x
   | CVTPI2PS x: sem-undef-arity2 x
   | CVTPS2DQ x: sem-undef-arity2 x
   | CVTPS2PD x: sem-undef-arity2 x
   | CVTPS2PI x: sem-undef-arity2 x
   | CVTSD2SI x: sem-undef-arity2 x
   | CVTSD2SS x: sem-undef-arity2 x
   | CVTSI2SD x: sem-undef-arity2 x
   | CVTSI2SS x: sem-undef-arity2 x
   | CVTSS2SD x: sem-undef-arity2 x
   | CVTSS2SI x: sem-undef-arity2 x
   | CVTTPD2DQ x: sem-undef-arity2 x
   | CVTTPD2PI x: sem-undef-arity2 x
   | CVTTPS2DQ x: sem-undef-arity2 x
   | CVTTPS2PI x: sem-undef-arity2 x
   | CVTTSD2SI x: sem-undef-arity2 x
   | CVTTSS2SI x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
1106
   | CWD x: sem-cwd-cdq-cqo x
Julian Kranz's avatar
Julian Kranz committed
1107
   | CWDE x: sem-convert 16
Julian Kranz's avatar
Julian Kranz committed
1108 1109
   | DAA x: sem-undef-arity0 x
   | DAS x: sem-undef-arity0 x
Julian Kranz's avatar
Julian Kranz committed
1110
   | DEC x: sem-dec x
Julian Kranz's avatar
Julian Kranz committed
1111
   | DIV x: sem-div Unsigned x
Julian Kranz's avatar
Julian Kranz committed
1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184 1185 1186 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203 1204 1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 1219 1220 1221
   | DIVPD x: sem-undef-arity2 x
   | DIVPS x: sem-undef-arity2 x
   | DIVSD x: sem-undef-arity2 x
   | DIVSS x: sem-undef-arity2 x
   | DPPD x: sem-undef-arity3 x
   | DPPS x: sem-undef-arity3 x
   | EMMS x: sem-undef-arity0 x
   | ENTER x: sem-undef-arity2 x
   | EXTRACTPS x: sem-undef-arity3 x
   | F2XM1 x: sem-undef-arity0 x
   | FABS x: sem-undef-arity0 x
   | FADD x: sem-undef-arity2 x
   | FADDP x: sem-undef-arity2 x
   | FBLD x: sem-undef-arity1 x
   | FBSTP x: sem-undef-arity1 x
   | FCHS x: sem-undef-arity0 x
   | FCLEX x: sem-undef-arity0 x
   | FCMOVB x: sem-undef-arity2 x
   | FCMOVBE x: sem-undef-arity2 x
   | FCMOVE x: sem-undef-arity2 x
   | FCMOVNB x: sem-undef-arity2 x
   | FCMOVNBE x: sem-undef-arity2 x
   | FCMOVNE x: sem-undef-arity2 x
   | FCMOVNU x: sem-undef-arity2 x
   | FCMOVU x: sem-undef-arity2 x
   | FCOM x: sem-undef-arity1 x
   | FCOMI x: sem-undef-arity2 x
   | FCOMIP x: sem-undef-arity2 x
   | FCOMP x: sem-undef-arity1 x
   | FCOMPP x: sem-undef-arity0 x
   | FCOS x: sem-undef-arity0 x
   | FDECSTP x: sem-undef-arity0 x
   | FDIV x: sem-undef-arity2 x
   | FDIVP x: sem-undef-arity2 x
   | FDIVR x: sem-undef-arity2 x
   | FDIVRP x: sem-undef-arity2 x
   | FFREE x: sem-undef-arity1 x
   | FIADD x: sem-undef-arity1 x
   | FICOM x: sem-undef-arity1 x
   | FICOMP x: sem-undef-arity1 x
   | FIDIV x: sem-undef-arity2 x
   | FIDIVR x: sem-undef-arity1 x
   | FILD x: sem-undef-arity1 x
   | FIMUL x: sem-undef-arity1 x
   | FINCSTP x: sem-undef-arity0 x
   | FINIT x: sem-undef-arity0 x
   | FIST x: sem-undef-arity1 x
   | FISTP x: sem-undef-arity1 x
   | FISTTP x: sem-undef-arity1 x
   | FISUB x: sem-undef-arity1 x
   | FISUBR x: sem-undef-arity1 x
   | FLD x: sem-undef-arity1 x
   | FLD1 x: sem-undef-arity0 x
   | FLDCW x: sem-undef-arity1 x
   | FLDENV x: sem-undef-arity1 x
   | FLDL2E x: sem-undef-arity0 x
   | FLDL2T x: sem-undef-arity0 x
   | FLDLG2 x: sem-undef-arity0 x
   | FLDLN2 x: sem-undef-arity0 x
   | FLDPI x: sem-undef-arity0 x
   | FLDZ x: sem-undef-arity0 x
   | FMUL x: sem-undef-arity2 x
   | FMULP x: sem-undef-arity2 x
   | FNCLEX x: sem-undef-arity0 x
   | FNINIT x: sem-undef-arity0 x
   | FNOP x: sem-undef-arity0 x
   | FNSAVE x: sem-undef-arity1 x
   | FNSTCW x: sem-undef-arity1 x
   | FNSTENV x: sem-undef-arity1 x
   | FNSTSW x: sem-undef-arity1 x
   | FPATAN x: sem-undef-arity0 x
   | FPREM1 x: sem-undef-arity0 x
   | FPREM x: sem-undef-arity0 x
   | FPTAN x: sem-undef-arity0 x
   | FRNDINT x: sem-undef-arity0 x
   | FRSTOR x: sem-undef-arity1 x
   | FSAVE x: sem-undef-arity1 x
   | FSCALE x: sem-undef-arity0 x
   | FSIN x: sem-undef-arity0 x
   | FSINCOS x: sem-undef-arity0 x
   | FSQRT x: sem-undef-arity0 x
   | FST x: sem-undef-arity1 x
   | FSTCW x: sem-undef-arity1 x
   | FSTENV x: sem-undef-arity1 x
   | FSTP x: sem-undef-arity1 x
   | FSTSW x: sem-undef-arity1 x
   | FSUB x: sem-undef-arity2 x
   | FSUBP x: sem-undef-arity2 x
   | FSUBR x: sem-undef-arity2 x
   | FSUBRP x: sem-undef-arity2 x
   | FTST x: sem-undef-arity0 x
   | FUCOM x: sem-undef-arity1 x
   | FUCOMI x: sem-undef-arity1 x
   | FUCOMIP x: sem-undef-arity1 x
   | FUCOMP x: sem-undef-arity1 x
   | FUCOMPP x: sem-undef-arity0 x
   | FXAM x: sem-undef-arity0 x
   | FXCH x: sem-undef-arity1 x
   | FXRSTOR x: sem-undef-arity1 x
   | FXRSTOR64 x: sem-undef-arity1 x
   | FXSAVE x: sem-undef-arity1 x
   | FXSAVE64 x: sem-undef-arity1 x
   | FXTRACT x: sem-undef-arity0 x
   | FYL2X x: sem-undef-arity0 x
   | FYL2XP1 x: sem-undef-arity0 x
   | HADDPD x: sem-undef-arity2 x
   | HADDPS x: sem-undef-arity2 x
   | HLT x: sem-undef-arity0 x
   | HSUBPD x: sem-undef-arity2 x
   | HSUBPS x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
1222
   | IDIV x: sem-idiv x
Julian Kranz's avatar
Julian Kranz committed
1223 1224
   | IMUL v:
       case v of
Julian Kranz's avatar
Julian Kranz committed
1225 1226 1227
          VA1 x: sem-imul-1 x
        | VA2 x: sem-imul-2 x
        | VA3 x: sem-imul-3 x
Julian Kranz's avatar
Julian Kranz committed
1228
       end
Julian Kranz's avatar
Julian Kranz committed
1229
   | IN x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
1230
   | INC x: sem-inc x
Julian Kranz's avatar
Julian Kranz committed
1231 1232 1233 1234 1235 1236 1237
   | INSB x: sem-undef-arity0 x
   | INSD x: sem-undef-arity0 x
   | INSERTPS x: sem-undef-arity3 x
   | INSW x: sem-undef-arity0 x
   | INT x: sem-undef-arity1 x
   | INT0 x: sem-undef-arity0 x
   | INT3 x: sem-undef-arity0 x
Julian Kranz's avatar
Julian Kranz committed
1238
   | INVD x: sem-invd
Julian Kranz's avatar
Julian Kranz committed
1239 1240 1241 1242 1243 1244 1245 1246 1247 1248 1249 1250 1251 1252 1253 1254 1255 1256 1257 1258 1259 1260 1261 1262 1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277
   | INVLPG x: sem-undef-arity1 x
   | INVPCID x: sem-undef-arity2 x
   | IRET x: sem-undef-arity0 x
   | IRETD x: sem-undef-arity0 x
   | IRETQ x: sem-undef-arity0 x
   | JA x: sem-a sem-jcc x
   | JAE x: sem-ae sem-jcc x
   | JB x: sem-b sem-jcc x
   | JBE x: sem-be sem-jcc x
   | JC x: sem-c sem-jcc x
   | JCXZ x: sem-jcxz x
   | JE x: sem-e sem-jcc x
   | JECXZ x: sem-jecxz x
   | JG x: sem-g sem-jcc x
   | JGE x: sem-ge sem-jcc x
   | JL x: sem-l sem-jcc x
   | JLE x: sem-le sem-jcc x
   | JMP x: sem-jmp x
   | JNA x: sem-na sem-jcc x
   | JNAE x: sem-nae sem-jcc x
   | JNB x: sem-nb sem-jcc x
   | JNBE x: sem-nbe sem-jcc x
   | JNC x: sem-nc sem-jcc x
   | JNE x: sem-ne sem-jcc x
   | JNG x: sem-ng sem-jcc x
   | JNGE x: sem-nge sem-jcc x
   | JNL x: sem-nl sem-jcc x
   | JNLE x: sem-nle sem-jcc x
   | JNO x: sem-no sem-jcc x
   | JNP x: sem-np sem-jcc x
   | JNS x: sem-ns sem-jcc x
   | JNZ x: sem-nz sem-jcc x
   | JO x: sem-o sem-jcc x
   | JP x: sem-p sem-jcc x
   | JPE x: sem-pe sem-jcc x
   | JPO x: sem-po sem-jcc x
   | JRCXZ x: sem-jrcxz x
   | JS x: sem-s sem-jcc x
   | JZ x: sem-z sem-jcc x
Julian Kranz's avatar
Julian Kranz committed
1278
   | LAHF x: sem-lahf
Julian Kranz's avatar
Julian Kranz committed
1279
   | LAR x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
1280
   | LDDQU x: sem-mov '0' x
Julian Kranz's avatar
Julian Kranz committed
1281
   | LDMXCSR x: sem-undef-arity1 x
Julian Kranz's avatar
Julian Kranz committed
1282
   | LDS x: sem-lds-les-lfs-lgs-lss x DS
Julian Kranz's avatar
Julian Kranz committed
1283 1284
   | LEA x: sem-lea x
   | LEAVE x: sem-undef-arity0 x
Julian Kranz's avatar
Julian Kranz committed
1285
   | LES x: sem-lds-les-lfs-lgs-lss x ES
Julian Kranz's avatar
Julian Kranz committed
1286
   | LFENCE x: sem-undef-arity0 x
Julian Kranz's avatar
Julian Kranz committed
1287
   | LFS x: sem-lds-les-lfs-lgs-lss x FS
Julian Kranz's avatar
Julian Kranz committed
1288
   | LGDT x: sem-undef-arity1 x
Julian Kranz's avatar
Julian Kranz committed
1289
   | LGS x: sem-lds-les-lfs-lgs-lss x GS
Julian Kranz's avatar
Julian Kranz committed
1290 1291 1292
   | LIDT x: sem-undef-arity1 x
   | LLDT x: sem-undef-arity1 x
   | LMSW x: sem-undef-arity1 x
Julian Kranz's avatar
Julian Kranz committed
1293
   | LODS x: sem-rep-insn x sem-lods
Julian Kranz's avatar
Julian Kranz committed
1294 1295 1296
   | LOOP x: sem-loop x
   | LOOPE x: sem-loope x
   | LOOPNE x: sem-loopne x
Julian Kranz's avatar
Julian Kranz committed
1297
   | LSL x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
1298
   | LSS x: sem-lds-les-lfs-lgs-lss x SS
Julian Kranz's avatar
Julian Kranz committed
1299
   | LTR x: sem-undef-arity1 x
Julian Kranz's avatar
Julian Kranz committed
1300
   | MASKMOVDQU x: sem-maskmovdqu-vmaskmovdqu x
Julian Kranz's avatar
Julian Kranz committed
1301
   | MASKMOVQ x: sem-maskmovq x
Julian Kranz's avatar
Julian Kranz committed
1302 1303 1304 1305 1306 1307 1308 1309 1310 1311
   | MAXPD x: sem-undef-arity2 x
   | MAXPS x: sem-undef-arity2 x
   | MAXSD x: sem-undef-arity2 x
   | MAXSS x: sem-undef-arity2 x
   | MFENCE x: sem-undef-arity0 x
   | MINPD x: sem-undef-arity2 x
   | MINPS x: sem-undef-arity2 x
   | MINSD x: sem-undef-arity2 x
   | MINSS x: sem-undef-arity2 x
   | MONITOR x: sem-undef-arity0 x
Julian Kranz's avatar
Julian Kranz committed
1312
   | MOV x: sem-mov '0' x
Julian Kranz's avatar
Julian Kranz committed
1313 1314
   | MOVAPD x: sem-mov '0' x
   | MOVAPS x: sem-mov '0' x
Julian Kranz's avatar
Julian Kranz committed
1315
   | MOVBE x: sem-movbe x
Julian Kranz's avatar
Julian Kranz committed
1316
   | MOVD x: sem-movzx '0' x
Julian Kranz's avatar
Julian Kranz committed
1317
   | MOVDDUP x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
1318
   | MOVDQ2Q x: sem-mov '0' x
Julian Kranz's avatar
Julian Kranz committed
1319 1320
   | MOVDQA x: sem-mov '0' x
   | MOVDQU x: sem-mov '0' x
Julian Kranz's avatar
Julian Kranz committed
1321 1322 1323 1324 1325 1326 1327 1328
   | MOVHLPS x: sem-undef-arity2 x
   | MOVHPD x: sem-undef-arity2 x
   | MOVHPS x: sem-undef-arity2 x
   | MOVLHPS x: sem-undef-arity2 x
   | MOVLPD x: sem-undef-arity2 x
   | MOVLPS x: sem-undef-arity2 x
   | MOVMSKPD x: sem-undef-arity2 x
   | MOVMSKPS x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
1329 1330
   | MOVNTDQ x: sem-mov '0' x
   | MOVNTDQA x: sem-mov '0' x
Julian Kranz's avatar
Julian Kranz committed
1331
   | MOVNTI x: sem-mov '0' x
Julian Kranz's avatar
Julian Kranz committed
1332 1333
   | MOVNTPD x: sem-undef-arity2 x
   | MOVNTPS x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
1334 1335 1336
   | MOVNTQ x: sem-mov '0' x
   | MOVQ x: sem-movzx '0' x
   | MOVQ2DQ x: sem-movzx '0' x
Julian Kranz's avatar
Julian Kranz committed
1337
   | MOVS x: sem-rep-insn x sem-movs
Julian Kranz's avatar
Julian Kranz committed
1338
   | MOVSD x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
1339 1340 1341 1342 1343 1344 1345 1346
   | MOVSHDUP x: sem-undef-arity2 x
   | MOVSLDUP x: sem-undef-arity2 x
   | MOVSS x: sem-undef-arity2 x
   | MOVSW x: sem-undef-arity2 x
   | MOVSX x: sem-movsx x
   | MOVSXD x: sem-movsx x
   | MOVUPD x: sem-undef-arity2 x
   | MOVUPS x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
1347
   | MOVZX x: sem-movzx '0' x
Julian Kranz's avatar
Julian Kranz committed
1348
   | MPSADBW x: sem-undef-arity3 x
Julian Kranz's avatar
Julian Kranz committed
1349
   | MUL x: sem-mul Unsigned x
Julian Kranz's avatar
Julian Kranz committed
1350 1351 1352 1353
   | MULPD x: sem-undef-arity2 x
   | MULPS x: sem-undef-arity2 x
   | MULSD x: sem-undef-arity2 x
   | MULSS x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
1354
   | MWAIT x: sem-nop
Julian Kranz's avatar
Julian Kranz committed
1355
   | NEG x: sem-neg x
Julian Kranz's avatar
Julian Kranz committed
1356
   | NOP x: sem-nop
Julian Kranz's avatar
Julian Kranz committed
1357
   | NOT x: sem-not x
Julian Kranz's avatar
Julian Kranz committed
1358 1359 1360 1361 1362 1363 1364 1365
   | OR x: sem-or x
   | ORPD x: sem-undef-arity2 x
   | ORPS x: sem-undef-arity2 x
   | OUT x: sem-undef-arity2 x
   | OUTS x: sem-undef-arity0 x
   | OUTSB x: sem-undef-arity0 x
   | OUTSD x: sem-undef-arity0 x
   | OUTSW x: sem-undef-arity0 x
Julian Kranz's avatar
Julian Kranz committed
1366 1367 1368
   | PABSB x: sem-pabs '0' 8 x
   | PABSD x: sem-pabs '0' 32 x
   | PABSW x: sem-pabs '0' 16 x
Julian Kranz's avatar
Julian Kranz committed
1369 1370
   | PACKSSDW x: sem-packsswb-packssdw 16 x
   | PACKSSWB x: sem-packsswb-packssdw 8 x
Julian Kranz's avatar
Julian Kranz committed
1371 1372
   | PACKUSDW x: sem-packuswb-packusdw 16 x
   | PACKUSWB x: sem-packuswb-packusdw 8 x
Julian Kranz's avatar
Julian Kranz committed
1373 1374 1375
   | PADDB x: sem-padd 8 x
   | PADDD x: sem-padd 32 x
   | PADDQ x: sem-padd 64 x
Julian Kranz's avatar
Julian Kranz committed
1376 1377
   | PADDSB x: sem-padds 8 x
   | PADDSW x: sem-padds 16 x
Julian Kranz's avatar
Julian Kranz committed
1378 1379
   | PADDUSB x: sem-paddus 8 x
   | PADDUSW x: sem-paddus 16 x
Julian Kranz's avatar
Julian Kranz committed
1380
   | PADDW x: sem-padd 16 x
Julian Kranz's avatar
Julian Kranz committed
1381
   | PALIGNR x: sem-palignr x
Julian Kranz's avatar
Julian Kranz committed
1382
   | PAND x: sem-pand x
Julian Kranz's avatar
Julian Kranz committed
1383
   | PANDN x: sem-pandn x
Julian Kranz's avatar
Julian Kranz committed
1384
   | PAUSE x: sem-undef-arity0 x
Julian Kranz's avatar
Julian Kranz committed
1385 1386 1387
   | PAVGB x: sem-pavg 8 x
   | PAVGW x: sem-pavg 16 x
   | PBLENDVB x: sem-pblendvb x
Julian Kranz's avatar
Julian Kranz committed
1388
   | PBLENDW x: sem-pblendw x
Julian Kranz's avatar
Julian Kranz committed
1389 1390 1391 1392 1393
   | PCLMULQDQ x: sem-pclmulqdq x
   | PCMPEQB x: sem-pcmpeq 8 x
   | PCMPEQD x: sem-pcmpeq 32 x
   | PCMPEQQ x: sem-pcmpeq 64 x
   | PCMPEQW x: sem-pcmpeq 16 x
Julian Kranz's avatar
Julian Kranz committed
1394 1395 1396
   | PCMPESTRI x: sem-undef-arity3 x
   | PCMPESTRM x: sem-undef-arity3 x
   | PCMPGRD x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
1397 1398 1399 1400
   | PCMPGTB x: sem-pcmpgt 8 x
   | PCMPGTD x: sem-pcmpgt 32 x 
   | PCMPGTQ x: sem-pcmpgt 64 x
   | PCMPGTW x: sem-pcmpgt 16 x
Julian Kranz's avatar
Julian Kranz committed
1401 1402
   | PCMPISTRI x: sem-undef-arity3 x
   | PCMPISTRM x: sem-undef-arity3 x
Julian Kranz's avatar
Julian Kranz committed
1403 1404 1405 1406
   | PEXTRB x: sem-pextr-vpextr 8 x
   | PEXTRD x: sem-pextr-vpextr 32 x
   | PEXTRQ x: sem-pextr-vpextr 64 x
   | PEXTRW x: sem-pextr-vpextr 16 x
Julian Kranz's avatar
Julian Kranz committed
1407
   | PHADDD x: sem-phadd 32 x
Julian Kranz's avatar
Julian Kranz committed
1408
   | PHADDSW x: sem-phaddsw x
Julian Kranz's avatar
Julian Kranz committed
1409
   | PHADDW x: sem-phadd 16 x
Julian Kranz's avatar
Julian Kranz committed
1410
   | PHMINPOSUW x: sem-phminposuw-vphminposuw '0' x
Julian Kranz's avatar
Julian Kranz committed
1411
   | PHSUBD x: sem-phsub 32 x
Julian Kranz's avatar
Julian Kranz committed
1412
   | PHSUBSW x: sem-phsubsw x
Julian Kranz's avatar
Julian Kranz committed
1413
   | PHSUBW x: sem-phsub 16 x
Julian Kranz's avatar
Julian Kranz committed
1414 1415 1416 1417
   | PINSRB x: sem-pinsr 8 x
   | PINSRD x: sem-pinsr 32 x
   | PINSRQ x: sem-pinsr 64 x
   | PINSRW x: sem-pinsr 16 x
Julian Kranz's avatar
Julian Kranz committed
1418 1419
   | PMADDUBSW x: sem-pmaddubsw x
   | PMADDWD x: sem-pmaddwd x
Julian Kranz's avatar
Julian Kranz committed
1420 1421 1422
   | PMAXSB x: sem-pmaxs 8 x
   | PMAXSD x: sem-pmaxs 32 x
   | PMAXSW x: sem-pmaxs 16 x
Julian Kranz's avatar
Julian Kranz committed
1423 1424 1425
   | PMAXUB x: sem-pmaxu 8 x
   | PMAXUD x: sem-pmaxu 32 x
   | PMAXUW x: sem-pmaxu 16 x
Julian Kranz's avatar
Julian Kranz committed
1426 1427 1428
   | PMINSB x: sem-pmins 8 x
   | PMINSD x: sem-pmins 32 x
   | PMINSW x: sem-pmins 16 x
Julian Kranz's avatar
Julian Kranz committed
1429 1430 1431
   | PMINUB x: sem-pminu 8 x
   | PMINUD x: sem-pminu 32 x
   | PMINUW x: sem-pminu 16 x
Julian Kranz's avatar
Julian Kranz committed
1432
   | PMOVMSKB x: sem-pmovmskb-vpmovmskb '0' x
Julian Kranz's avatar
Julian Kranz committed
1433 1434 1435 1436 1437 1438
   | PMOVSXBD x: sem-pmovsx-vpmovsx '0' 8 32 x
   | PMOVSXBQ x: sem-pmovsx-vpmovsx '0' 8 64 x
   | PMOVSXBW x: sem-pmovsx-vpmovsx '0' 8 16 x
   | PMOVSXDQ x: sem-pmovsx-vpmovsx '0' 32 64 x
   | PMOVSXWD x: sem-pmovsx-vpmovsx '0' 16 32 x
   | PMOVSXWQ x: sem-pmovsx-vpmovsx '0' 16 64 x
Julian Kranz's avatar
Julian Kranz committed
1439 1440 1441 1442 1443 1444
   | PMOVZXBD x: sem-pmovzx-vpmovzx '