x86-rreil-translator.ml 54.1 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 6 7 8
type sem_writeback =
   SEM_WRITE_VAR of {size:int, id:sem_var}
 | SEM_WRITE_MEM of {size:int, address:sem_linear, segment:seg_override}

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

Julian Kranz's avatar
Julian Kranz committed
18
val ip-get = do
Julian Kranz's avatar
Julian Kranz committed
19 20
  k <- ipget;
  return (imm k)
Julian Kranz's avatar
Julian Kranz committed
21 22
end

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

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

Julian Kranz's avatar
Julian Kranz committed
55
val sizeof1 op =
mb0's avatar
Up.  
mb0 committed
56 57 58 59 60 61 62 63 64
   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
65 66 67 68
type signedness =
   Signed
 | Unsigned

Julian Kranz's avatar
Julian Kranz committed
69
val expand dst-getter conv lin from-sz to-sz =
Julian Kranz's avatar
Julian Kranz committed
70
  if from-sz === to-sz then
Julian Kranz's avatar
Julian Kranz committed
71 72 73
    return lin
  else do
    expanded <- dst-getter;
Julian Kranz's avatar
Julian Kranz committed
74 75 76
    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
77 78 79
    end;
    return (var expanded)
  end
Julian Kranz's avatar
Julian Kranz committed
80 81 82

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
83
in
Julian Kranz's avatar
Julian Kranz committed
84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99
  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
100
end
Julian Kranz's avatar
Julian Kranz committed
101

Julian Kranz's avatar
Julian Kranz committed
102 103 104 105 106
#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
107
  mode64 <- mode64?;
Julian Kranz's avatar
Julian Kranz committed
108

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

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

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

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

Julian Kranz's avatar
Julian Kranz committed
200
	     expanded <- mktemp;
Julian Kranz's avatar
Julian Kranz committed
201 202
	     expanded <- with-subscope (m expanded);
	     return expanded
Julian Kranz's avatar
Julian Kranz committed
203
           end end
mb0's avatar
Up.  
mb0 committed
204 205 206
      end
   end

Julian Kranz's avatar
Julian Kranz committed
207
val read sz x = conv-with Unsigned sz x
Julian Kranz's avatar
Julian Kranz committed
208
val reads conv sz x = conv-with conv sz x
Julian Kranz's avatar
Julian Kranz committed
209

Julian Kranz's avatar
Julian Kranz committed
210 211
val extract-imm-unsigned imm =
  case imm of
Julian Kranz's avatar
*  
Julian Kranz committed
212 213 214 215
     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
216 217
 end

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

Julian Kranz's avatar
Julian Kranz committed
281

Julian Kranz's avatar
Julian Kranz committed
282 283
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
284 285 286 287 288 289 290

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

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

	mode64 <- mode64?;
Julian Kranz's avatar
Julian Kranz committed
317 318
	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
319 320 321 322 323 324
	  #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
325

Julian Kranz's avatar
Julian Kranz committed
326 327 328 329 330 331 332 333 334 335 336 337 338
#        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
339 340
   end

Julian Kranz's avatar
Julian Kranz committed
341 342
val write sz a b = write-extend '0' sz a b

Julian Kranz's avatar
Julian Kranz committed
343 344 345 346 347 348 349 350 351 352 353 354 355
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
356 357 358 359 360 361 362 363
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
364 365 366 367 368 369
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
370 371 372

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

Julian Kranz's avatar
Julian Kranz committed
373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474
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
475
val undef-opnd opnd = do
Julian Kranz's avatar
Julian Kranz committed
476
  sz <- sizeof1 opnd;
Julian Kranz's avatar
Julian Kranz committed
477
  a <- lval sz opnd;
Julian Kranz's avatar
Julian Kranz committed
478
  t <- mktemp;
Julian Kranz's avatar
Julian Kranz committed
479
  write sz a (var t)
Julian Kranz's avatar
Julian Kranz committed
480 481 482 483 484
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
485
   | MEM m: undef-opnd x.opnd1
Julian Kranz's avatar
Julian Kranz committed
486 487 488
  end
end

Julian Kranz's avatar
Julian Kranz committed
489
val sem-undef-arity0 x = do
Julian Kranz's avatar
Julian Kranz committed
490
  return void
Julian Kranz's avatar
Julian Kranz committed
491 492 493
end

val sem-undef-arity1 x = do
Julian Kranz's avatar
Julian Kranz committed
494
  sem-undef-arity-ge1 x
Julian Kranz's avatar
Julian Kranz committed
495 496 497
end

val sem-undef-arity2 x = do
Julian Kranz's avatar
Julian Kranz committed
498
  sem-undef-arity-ge1 x
Julian Kranz's avatar
Julian Kranz committed
499 500 501
end

val sem-undef-arity3 x = do
Julian Kranz's avatar
Julian Kranz committed
502
  sem-undef-arity-ge1 x
Julian Kranz's avatar
Julian Kranz committed
503 504 505
end

val sem-undef-arity4 x = do
Julian Kranz's avatar
Julian Kranz committed
506
  sem-undef-arity-ge1 x
Julian Kranz's avatar
Julian Kranz committed
507 508 509
end

val sem-undef-varity x = do
Julian Kranz's avatar
Julian Kranz committed
510
  case x of
Julian Kranz's avatar
Julian Kranz committed
511 512
     VA0 x: sem-undef-arity0 x
   | VA1 x: sem-undef-arity1 x
Julian Kranz's avatar
Julian Kranz committed
513 514 515 516
   | 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
517 518 519
end

val sem-undef-flow1 x = do
Julian Kranz's avatar
Julian Kranz committed
520
  return void
Julian Kranz's avatar
Julian Kranz committed
521 522
end

Julian Kranz's avatar
Julian Kranz committed
523
val emit-parity-flag r = do
Julian Kranz's avatar
Julian Kranz committed
524 525
  byte-size <- return 8;

Julian Kranz's avatar
Julian Kranz committed
526
  low-byte <- mktemp;
Julian Kranz's avatar
Julian Kranz committed
527
  mov byte-size low-byte r;
Julian Kranz's avatar
Julian Kranz committed
528 529

  pf <- fPF;
Julian Kranz's avatar
Julian Kranz committed
530 531 532 533 534 535 536 537
  # 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
538 539
end

Julian Kranz's avatar
Julian Kranz committed
540
val emit-arithmetic-adjust-flag sz r op0 op1 = do
Julian Kranz's avatar
Julian Kranz committed
541 542
  # Hacker's Delight - How the Computer Sets Overflow for Signed Add/Subtract
  t <- mktemp;
Julian Kranz's avatar
Julian Kranz committed
543 544
  xorb sz t r op0;
  xorb sz t (var t) op1;
Julian Kranz's avatar
Julian Kranz committed
545 546 547 548

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

Julian Kranz's avatar
Julian Kranz committed
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
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
579
    # Hacker's Delight - Unsigned Add/Subtract
Julian Kranz's avatar
Julian Kranz committed
580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637
    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
638
end
mb0's avatar
Up.  
mb0 committed
639

Julian Kranz's avatar
Julian Kranz committed
640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661
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
662 663
end

Julian Kranz's avatar
Julian Kranz committed
664 665 666 667 668 669 670 671 672 673 674 675 676 677
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
678 679
end

Julian Kranz's avatar
Julian Kranz committed
680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696
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
697 698 699 700
val divb x y =
  case x of
     8:
       case y of
Julian Kranz's avatar
Julian Kranz committed
701 702
          1: 8
        | 2: 4
Julian Kranz's avatar
Julian Kranz committed
703 704 705 706 707
        | 4: 2
        | 8: 1
       end
   | 16:
       case y of
Julian Kranz's avatar
Julian Kranz committed
708 709
          1: 16
        | 2: 8
Julian Kranz's avatar
Julian Kranz committed
710 711 712 713 714 715
        | 4: 4
        | 8: 2
        | 16: 1
       end
   | 32:
       case y of
Julian Kranz's avatar
Julian Kranz committed
716 717
          1: 32
        | 2: 16
Julian Kranz's avatar
Julian Kranz committed
718 719 720 721 722 723 724
        | 4: 8
        | 8: 4
        | 16: 2
        | 32: 1
       end
   | 64:
       case y of
Julian Kranz's avatar
Julian Kranz committed
725 726
          1: 64
        | 2: 32
Julian Kranz's avatar
Julian Kranz committed
727 728 729 730 731 732 733 734
        | 4: 16
        | 8: 8
        | 16: 4
        | 32: 2
        | 64: 1
       end
   | 128:
       case y of
Julian Kranz's avatar
Julian Kranz committed
735 736
          1: 128
        | 2: 64
Julian Kranz's avatar
Julian Kranz committed
737 738 739 740 741 742 743 744 745
        | 4: 32
        | 8: 16
        | 16: 8
        | 32: 4
        | 64: 2
        | 128: 1
       end
   | 256:
       case y of
Julian Kranz's avatar
Julian Kranz committed
746 747
          1: 256
        | 2: 128
Julian Kranz's avatar
Julian Kranz committed
748 749 750 751 752 753 754 755
        | 4: 64
        | 8: 32
        | 16: 16
        | 32: 8
        | 64: 4
        | 128: 2
        | 256: 1
       end
Julian Kranz's avatar
Julian Kranz committed
756 757 758 759 760
    | k:
       case y of
          1: k
	| k: 1
       end
Julian Kranz's avatar
Julian Kranz committed
761 762
  end
;
Julian Kranz's avatar
Julian Kranz committed
763 764 765 766 767 768 769 770 771 772 773 774 775

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
776

Julian Kranz's avatar
Julian Kranz committed
777 778 779 780 781 782
val exp base e =
  case e of
     0: 1
   | x: base * (exp base (e - 1))
  end

Julian Kranz's avatar
Julian Kranz committed
783
val vector-apply size element-size monad = do
Julian Kranz's avatar
Julian Kranz committed
784
  limit <- return (divb size element-size);
Julian Kranz's avatar
Julian Kranz committed
785 786 787

  let
    val f i = do
Julian Kranz's avatar
Julian Kranz committed
788
      with-subscope (monad i);
Julian Kranz's avatar
Julian Kranz committed
789 790 791 792 793 794 795 796 797 798 799

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

Julian Kranz's avatar
Julian Kranz committed
800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823
#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
824

Julian Kranz's avatar
Julian Kranz committed
825
val binop-signed-saturating operator size dst src1 src2 = do
Julian Kranz's avatar
Julian Kranz committed
826 827 828 829 830
  dst-ex <- mktemp;
  src1-ex <- mktemp;
  src2-ex <- mktemp;

  upper <- return (
Julian Kranz's avatar
Julian Kranz committed
831 832 833 834
    case size of
       8: 0x7f
     | 16: 0x7fff
    end
Julian Kranz's avatar
Julian Kranz committed
835 836
  );
  lower <- return (
Julian Kranz's avatar
Julian Kranz committed
837 838 839 840
    case size of
       8: (0-0x80)
     | 16: (0-0x8000)
    end
Julian Kranz's avatar
Julian Kranz committed
841 842 843 844
  );

  movsx (size + 1) src1-ex size src1;
  movsx (size + 1) src2-ex size src2;
Julian Kranz's avatar
Julian Kranz committed
845
  operator (size + 1) dst-ex (var src1-ex) (var src2-ex);
Julian Kranz's avatar
Julian Kranz committed
846 847 848 849 850 851 852 853 854 855
  
  _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
856 857 858
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
859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878
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
879 880
val semantics insn =
  case insn of
Julian Kranz's avatar
Julian Kranz committed
881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898
     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
899
   | AND x: sem-and x
Julian Kranz's avatar
Julian Kranz committed
900
   | ANDNPD x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
901
   | ANDNPS x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
902
   | ANDPD x: sem-andpd x
Julian Kranz's avatar
Julian Kranz committed
903 904 905 906 907 908 909
   | 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
910
   | BSF x: sem-bsf x
Julian Kranz's avatar
Julian Kranz committed
911 912
   | BSR x: sem-bsr x
   | BSWAP x: sem-bswap x
Julian Kranz's avatar
Julian Kranz committed
913 914 915 916
   | 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
917
   | CALL x: sem-call x
Julian Kranz's avatar
Julian Kranz committed
918
   | CBW x: sem-convert 8
Julian Kranz's avatar
Julian Kranz committed
919
   | CDQ x: sem-cwd-cdq-cqo x
Julian Kranz's avatar
Julian Kranz committed
920
   | CDQE x: sem-convert 32
Julian Kranz's avatar
Julian Kranz committed
921 922 923 924 925
   | 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
926
   | CMC x: sem-cmc
Julian Kranz's avatar
Julian Kranz committed
927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959
   | 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
960
   | CMPS x: sem-repe-repne-insn x sem-cmps
Julian Kranz's avatar
Julian Kranz committed
961 962 963 964 965 966 967 968
   | 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
969
   | CMPXCHG x: sem-cmpxchg x
Julian Kranz's avatar
Julian Kranz committed
970 971
   | CMPXCHG16B x: sem-cmpxchg16b-cmpxchg8b x
   | CMPXCHG8B x: sem-cmpxchg16b-cmpxchg8b x
Julian Kranz's avatar
Julian Kranz committed
972 973
   | COMISD x: sem-undef-arity2 x
   | COMISS x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
974
   | CPUID x: sem-cpuid x
Julian Kranz's avatar
Julian Kranz committed
975
   | CQO x: sem-cwd-cdq-cqo x
Julian Kranz's avatar
Julian Kranz committed
976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998
   | 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
999
   | CWD x: sem-cwd-cdq-cqo x
Julian Kranz's avatar
Julian Kranz committed
1000
   | CWDE x: sem-convert 16
Julian Kranz's avatar
Julian Kranz committed
1001 1002
   | DAA x: sem-undef-arity0 x
   | DAS x: sem-undef-arity0 x
Julian Kranz's avatar
Julian Kranz committed
1003
   | DEC x: sem-dec x
Julian Kranz's avatar
Julian Kranz committed
1004
   | DIV x: sem-div Unsigned x
Julian Kranz's avatar
Julian Kranz committed
1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 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 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114
   | 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
1115
   | IDIV x: sem-idiv x
Julian Kranz's avatar
Julian Kranz committed
1116 1117
   | IMUL v:
       case v of
Julian Kranz's avatar
Julian Kranz committed
1118 1119 1120
          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
1121
       end
Julian Kranz's avatar
Julian Kranz committed
1122
   | IN x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
1123
   | INC x: sem-inc x
Julian Kranz's avatar
Julian Kranz committed
1124 1125 1126 1127 1128 1129 1130
   | 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
1131
   | INVD x: sem-invd
Julian Kranz's avatar
Julian Kranz committed
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
   | 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
1171
   | LAHF x: sem-lahf
Julian Kranz's avatar
Julian Kranz committed
1172
   | LAR x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
1173
   | LDDQU x: sem-mov '0' x
Julian Kranz's avatar
Julian Kranz committed
1174
   | LDMXCSR x: sem-undef-arity1 x
Julian Kranz's avatar
Julian Kranz committed
1175
   | LDS x: sem-lds-les-lfs-lgs-lss x DS
Julian Kranz's avatar
Julian Kranz committed
1176 1177
   | LEA x: sem-lea x
   | LEAVE x: sem-undef-arity0 x
Julian Kranz's avatar
Julian Kranz committed
1178
   | LES x: sem-lds-les-lfs-lgs-lss x ES
Julian Kranz's avatar
Julian Kranz committed
1179
   | LFENCE x: sem-undef-arity0 x
Julian Kranz's avatar
Julian Kranz committed
1180
   | LFS x: sem-lds-les-lfs-lgs-lss x FS
Julian Kranz's avatar
Julian Kranz committed
1181
   | LGDT x: sem-undef-arity1 x
Julian Kranz's avatar
Julian Kranz committed
1182
   | LGS x: sem-lds-les-lfs-lgs-lss x GS
Julian Kranz's avatar
Julian Kranz committed
1183 1184 1185
   | 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
1186
   | LODS x: sem-rep-insn x sem-lods
Julian Kranz's avatar
Julian Kranz committed
1187 1188 1189
   | LOOP x: sem-loop x
   | LOOPE x: sem-loope x
   | LOOPNE x: sem-loopne x
Julian Kranz's avatar
Julian Kranz committed
1190
   | LSL x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
1191
   | LSS x: sem-lds-les-lfs-lgs-lss x SS
Julian Kranz's avatar
Julian Kranz committed
1192
   | LTR x: sem-undef-arity1 x
Julian Kranz's avatar
Julian Kranz committed
1193
   | MASKMOVDQU x: sem-maskmovdqu-vmaskmovdqu x
Julian Kranz's avatar
Julian Kranz committed
1194
   | MASKMOVQ x: sem-maskmovq x
Julian Kranz's avatar
Julian Kranz committed
1195 1196 1197 1198 1199 1200 1201 1202 1203 1204
   | 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
1205
   | MOV x: sem-mov '0' x
Julian Kranz's avatar
Julian Kranz committed
1206 1207
   | MOVAPD x: sem-mov '0' x
   | MOVAPS x: sem-mov '0' x
Julian Kranz's avatar
Julian Kranz committed
1208
   | MOVBE x: sem-movbe x
Julian Kranz's avatar
Julian Kranz committed
1209
   | MOVD x: sem-movzx '0' x
Julian Kranz's avatar
Julian Kranz committed
1210
   | MOVDDUP x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
1211
   | MOVDQ2Q x: sem-mov '0' x
Julian Kranz's avatar
Julian Kranz committed
1212 1213
   | MOVDQA x: sem-mov '0' x
   | MOVDQU x: sem-mov '0' x
Julian Kranz's avatar
Julian Kranz committed
1214 1215 1216 1217 1218 1219 1220 1221
   | 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
1222 1223
   | MOVNTDQ x: sem-mov '0' x
   | MOVNTDQA x: sem-mov '0' x
Julian Kranz's avatar
Julian Kranz committed
1224
   | MOVNTI x: sem-mov '0' x
Julian Kranz's avatar
Julian Kranz committed
1225 1226
   | MOVNTPD x: sem-undef-arity2 x
   | MOVNTPS x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
1227 1228 1229
   | 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
1230
   | MOVS x: sem-rep-insn x sem-movs
Julian Kranz's avatar
Julian Kranz committed
1231
   | MOVSD x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
1232 1233 1234 1235 1236 1237 1238 1239
   | 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
1240
   | MOVZX x: sem-movzx '0' x
Julian Kranz's avatar
Julian Kranz committed
1241
   | MPSADBW x: sem-undef-arity3 x
Julian Kranz's avatar
Julian Kranz committed
1242
   | MUL x: sem-mul Unsigned x
Julian Kranz's avatar
Julian Kranz committed
1243 1244 1245 1246
   | 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
1247
   | MWAIT x: sem-nop
Julian Kranz's avatar
Julian Kranz committed
1248
   | NEG x: sem-neg x
Julian Kranz's avatar
Julian Kranz committed
1249
   | NOP x: sem-nop
Julian Kranz's avatar
Julian Kranz committed
1250
   | NOT x: sem-not x
Julian Kranz's avatar
Julian Kranz committed
1251 1252 1253 1254 1255 1256 1257 1258
   | 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
1259 1260 1261
   | 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
1262 1263
   | PACKSSDW x: sem-packsswb-packssdw 16 x
   | PACKSSWB x: sem-packsswb-packssdw 8 x
Julian Kranz's avatar
Julian Kranz committed
1264 1265
   | PACKUSDW x: sem-packuswb-packusdw 16 x
   | PACKUSWB x: sem-packuswb-packusdw 8 x
Julian Kranz's avatar
Julian Kranz committed
1266 1267 1268
   | 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
1269 1270
   | PADDSB x: sem-padds 8 x
   | PADDSW x: sem-padds 16 x
Julian Kranz's avatar
Julian Kranz committed
1271 1272
   | PADDUSB x: sem-paddus 8 x
   | PADDUSW x: sem-paddus 16 x
Julian Kranz's avatar
Julian Kranz committed
1273
   | PADDW x: sem-padd 16 x
Julian Kranz's avatar
Julian Kranz committed
1274
   | PALIGNR x: sem-palignr x
Julian Kranz's avatar
Julian Kranz committed
1275
   | PAND x: sem-pand x
Julian Kranz's avatar
Julian Kranz committed
1276
   | PANDN x: sem-pandn x
Julian Kranz's avatar
Julian Kranz committed
1277
   | PAUSE x: sem-undef-arity0 x
Julian Kranz's avatar
Julian Kranz committed
1278 1279 1280
   | PAVGB x: sem-pavg 8 x
   | PAVGW x: sem-pavg 16 x
   | PBLENDVB x: sem-pblendvb x
Julian Kranz's avatar
Julian Kranz committed
1281
   | PBLENDW x: sem-pblendw x
Julian Kranz's avatar
Julian Kranz committed
1282 1283 1284 1285 1286
   | 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
1287 1288 1289
   | 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
1290 1291 1292 1293
   | 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
1294 1295
   | PCMPISTRI x: sem-undef-arity3 x
   | PCMPISTRM x: sem-undef-arity3 x
Julian Kranz's avatar
Julian Kranz committed
1296 1297 1298 1299
   | 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
1300
   | PHADDD x: sem-phadd 32 x
Julian Kranz's avatar
Julian Kranz committed
1301
   | PHADDSW x: sem-phaddsw x
Julian Kranz's avatar
Julian Kranz committed
1302
   | PHADDW x: sem-phadd 16 x
Julian Kranz's avatar
Julian Kranz committed
1303
   | PHMINPOSUW x: sem-phminposuw-vphminposuw '0' x
Julian Kranz's avatar
Julian Kranz committed
1304
   | PHSUBD x: sem-phsub 32 x
Julian Kranz's avatar
Julian Kranz committed
1305
   | PHSUBSW x: sem-phsubsw x
Julian Kranz's avatar
Julian Kranz committed
1306
   | PHSUBW x: sem-phsub 16 x
Julian Kranz's avatar
Julian Kranz committed
1307 1308 1309 1310
   | 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
1311 1312
   | PMADDUBSW x: sem-pmaddubsw x
   | PMADDWD x: sem-pmaddwd x
Julian Kranz's avatar
Julian Kranz committed
1313 1314 1315
   | 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
1316 1317 1318
   | 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
1319 1320 1321
   | 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
1322 1323 1324
   | 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
1325
   | PMOVMSKB x: sem-pmovmskb-vpmovmskb '0' x
Julian Kranz's avatar
Julian Kranz committed
1326 1327 1328 1329 1330 1331
   | 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
1332 1333 1334 1335 1336 1337
   | PMOVZXBD x: sem-pmovzx-vpmovzx '0' 8 32 x
   | PMOVZXBQ x: sem-pmovzx-vpmovzx '0' 8 64 x
   | PMOVZXBW x: sem-pmovzx-vpmovzx '0' 8 16 x
   | PMOVZXDQ x: sem-pmovzx-vpmovzx '0' 32 64 x
   | PMOVZXWD x: sem-pmovzx-vpmovzx '0' 16 32 x
   | PMOVZXWQ x: sem-pmovzx-vpmovzx '0' 16 64 x
Julian Kranz's avatar
Julian Kranz committed
1338
   | PMULDQ x: sem-pmuldq x
Julian Kranz's avatar
Julian Kranz committed
1339
   | PMULHRSW x: sem-pmulhrsw x
Julian Kranz's avatar
Julian Kranz committed
1340
   | PMULHUW x: sem-pmulhuw x
Julian Kranz's avatar
Julian Kranz committed
1341
   | PMULHW x: sem-pmulhw x
Julian Kranz's avatar
Julian Kranz committed
1342 1343
   | PMULLD x: sem-pmull 32 x
   | PMULLW x: sem-pmull 16 x
Julian Kranz's avatar
Julian Kranz committed
1344
   | PMULUDQ x: sem-pmuludq x
Julian Kranz's avatar
Julian Kranz committed
1345
   | POP x: sem-pop x
Julian Kranz's avatar
Julian Kranz committed
1346 1347 1348
   | POPA x: sem-popa-popad x
   | POPAD x: sem-popa-popad x
   | POPCNT x: sem-popcnt x
Julian Kranz's avatar
Julian Kranz committed
1349 1350 1351
   | POPF x: sem-popf x
   | POPFD x: sem-popf x
   | POPFQ x: sem-popf x
Julian Kranz's avatar
Julian Kranz committed
1352
   | POR x: sem-por x
Julian Kranz's avatar
Julian Kranz committed
1353 1354 1355 1356 1357
   | PREFETCHNTA x: sem-undef-arity1 x
   | PREFETCHT0 x: sem-undef-arity1 x
   | PREFETCHT1 x: sem-undef-arity1 x
   | PREFETCHT2 x: sem-undef-arity1 x
   | PREFETCHW x: sem-undef-arity1 x
Julian Kranz's avatar
Julian Kranz committed
1358
   | PSADBW x: sem-psadbw x
Julian Kranz's avatar
Julian Kranz committed
1359
   | PSHUFB x: sem-pshufb x
Julian Kranz's avatar
Julian Kranz committed
1360
   | PSHUFD x: sem-pshufd-vpshufd '0' x
Julian Kranz's avatar
Julian Kranz committed
1361
   | PSHUFHW x: sem-pshufhw-vpshufhw '0' x
Julian Kranz's avatar
Julian Kranz committed
1362
   | PSHUFLW x: sem-pshuflw-vpshuflw '0' x
Julian Kranz's avatar
Julian Kranz committed
1363
   | PSHUFW x: sem-pshufw x
Julian Kranz's avatar
Julian Kranz committed
1364 1365 1366
   | PSIGNB x: sem-psign 8 x
   | PSIGND x: sem-psign 32 x
   | PSIGNW x: sem-psign 16 x
Julian Kranz's avatar
Julian Kranz committed
1367
   | PSLLD x: sem-psll 32 x
Julian Kranz's avatar
Julian Kranz committed
1368
   | PSLLDQ x: sem-pslldq x
Julian Kranz's avatar
Julian Kranz committed
1369 1370
   | PSLLQ x: sem-psll 64 x
   | PSLLW x: sem-psll 16 x
Julian Kranz's avatar
Julian Kranz committed
1371 1372
   | PSRAD x: sem-psra 32 x
   | PSRAW x: sem-psra 16 x
Julian Kranz's avatar
Julian Kranz committed
1373
   | PSRLD x: sem-psrl 32 x
Julian Kranz's avatar
Julian Kranz committed
1374
   | PSRLDQ x: sem-psrldq x
Julian Kranz's avatar
Julian Kranz committed
1375 1376
   | PSRLQ x: sem-psrl 64 x
   | PSRLW x: sem-psrl 16 x
Julian Kranz's avatar
Julian Kranz committed
1377 1378 1379
   | PSUBB x: sem-psub 8 x
   | PSUBD x: sem-psub 32 x
   | PSUBQ x: sem-psub 64 x
Julian Kranz's avatar
Julian Kranz committed
1380 1381
   | PSUBSB x: sem-psubs 8 x
   | PSUBSW x: sem-psubs 16 x