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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

val far target = not (near target)

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

val absolute target = not (relative target)

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

Julian Kranz's avatar
Julian Kranz committed
269

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

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

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

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

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

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

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

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

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

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

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

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

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

val /d cond = return cond

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  let
    val f i = do
      monad i;

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

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

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

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

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

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

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

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

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

Julian Kranz's avatar
Julian Kranz committed
959 960
val semantics insn =
  case insn of
Julian Kranz's avatar
Julian Kranz committed
961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978
     AAA x: sem-undef-arity0 x
   | AAD x: sem-undef-arity1 x
   | AAM x: sem-undef-arity1 x
   | AAS x: sem-undef-arity0 x
   | ADC x: sem-adc x
   | ADD x: sem-add x
   | ADDPD x: sem-undef-arity2 x
   | ADDPS x: sem-undef-arity2 x
   | ADDSD x: sem-undef-arity2 x
   | ADDSS x: sem-undef-arity2 x
   | ADDSUBPD x: sem-undef-arity2 x
   | ADDSUBPS x: sem-undef-arity2 x
   | AESDEC x: sem-undef-arity2 x
   | AESDECLAST x: sem-undef-arity2 x
   | AESENC x: sem-undef-arity2 x
   | AESENCLAST x: sem-undef-arity2 x
   | AESIMC x: sem-undef-arity2 x
   | AESKEYGENASSIST x: sem-undef-arity3 x
Julian Kranz's avatar
Julian Kranz committed
979
   | AND x: sem-and x
Julian Kranz's avatar
Julian Kranz committed
980
   | ANDNPD x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
981
   | ANDNPS x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
982
   | ANDPD x: sem-andpd x
Julian Kranz's avatar
Julian Kranz committed
983 984 985 986 987 988 989
   | ANDPS x: sem-undef-arity2 x
   | ARPL x: sem-undef-arity2 x
   | BLENDPD x: sem-undef-arity3 x
   | BLENDPS x: sem-undef-arity3 x
   | BLENDVPD x: sem-undef-arity3 x
   | BLENDVPS x: sem-undef-arity3 x
   | BOUND x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
990
   | BSF x: sem-bsf x
Julian Kranz's avatar
Julian Kranz committed
991 992
   | BSR x: sem-bsr x
   | BSWAP x: sem-bswap x
Julian Kranz's avatar
Julian Kranz committed
993 994 995 996
   | BT x: sem-bt x sem-bt-none
   | BTC x: sem-bt x sem-bt-complement
   | BTR x: sem-bt x sem-bt-reset
   | BTS x: sem-bt x sem-bt-set
Julian Kranz's avatar
Julian Kranz committed
997
   | CALL x: sem-call x
Julian Kranz's avatar
Julian Kranz committed
998
   | CBW x: sem-convert 8
Julian Kranz's avatar
Julian Kranz committed
999
   | CDQ x: sem-cwd-cdq-cqo x
Julian Kranz's avatar
Julian Kranz committed
1000
   | CDQE x: sem-convert 32
Julian Kranz's avatar
Julian Kranz committed
1001 1002 1003 1004 1005
   | 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
1006
   | CMC x: sem-cmc
Julian Kranz's avatar
Julian Kranz committed
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
   | 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
1040
   | CMPS x: sem-repe-repne-insn x sem-cmps
Julian Kranz's avatar
Julian Kranz committed
1041 1042 1043 1044 1045 1046 1047 1048
   | 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
1049
   | CMPXCHG x: sem-cmpxchg x
Julian Kranz's avatar
Julian Kranz committed
1050 1051
   | CMPXCHG16B x: sem-cmpxchg16b-cmpxchg8b x
   | CMPXCHG8B x: sem-cmpxchg16b-cmpxchg8b x
Julian Kranz's avatar
Julian Kranz committed
1052 1053
   | COMISD x: sem-undef-arity2 x
   | COMISS x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
1054
   | CPUID x: sem-cpuid x
Julian Kranz's avatar
Julian Kranz committed
1055
   | CQO x: sem-cwd-cdq-cqo x
Julian Kranz's avatar
Julian Kranz committed
1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078
   | 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
1079
   | CWD x: sem-cwd-cdq-cqo x
Julian Kranz's avatar
Julian Kranz committed
1080
   | CWDE x: sem-convert 16
Julian Kranz's avatar
Julian Kranz committed
1081 1082
   | DAA x: sem-undef-arity0 x
   | DAS x: sem-undef-arity0 x
Julian Kranz's avatar
Julian Kranz committed
1083
   | DEC x: sem-dec x
Julian Kranz's avatar
Julian Kranz committed
1084
   | DIV x: sem-div Unsigned x
Julian Kranz's avatar
Julian Kranz committed
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 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
   | 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
1195
   | IDIV x: sem-idiv x
Julian Kranz's avatar
Julian Kranz committed
1196 1197
   | IMUL v:
       case v of
Julian Kranz's avatar
Julian Kranz committed
1198 1199 1200
          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
1201
       end
Julian Kranz's avatar
Julian Kranz committed
1202
   | IN x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
1203
   | INC x: sem-inc x
Julian Kranz's avatar
Julian Kranz committed
1204 1205 1206 1207 1208 1209 1210
   | 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
1211
   | INVD x: sem-invd
Julian Kranz's avatar
Julian Kranz committed
1212 1213 1214 1215 1216 1217 1218 1219 1220 1221 1222 1223 1224 1225 1226 1227 1228 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242 1243 1244 1245 1246 1247 1248 1249 1250
   | 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
1251
   | LAHF x: sem-lahf
Julian Kranz's avatar
Julian Kranz committed
1252
   | LAR x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
1253
   | LDDQU x: sem-mov '0' x
Julian Kranz's avatar
Julian Kranz committed
1254
   | LDMXCSR x: sem-undef-arity1 x
Julian Kranz's avatar
Julian Kranz committed
1255
   | LDS x: sem-lds-les-lfs-lgs-lss x DS
Julian Kranz's avatar
Julian Kranz committed
1256 1257
   | LEA x: sem-lea x
   | LEAVE x: sem-undef-arity0 x
Julian Kranz's avatar
Julian Kranz committed
1258
   | LES x: sem-lds-les-lfs-lgs-lss x ES
Julian Kranz's avatar
Julian Kranz committed
1259
   | LFENCE x: sem-undef-arity0 x
Julian Kranz's avatar
Julian Kranz committed
1260
   | LFS x: sem-lds-les-lfs-lgs-lss x FS
Julian Kranz's avatar
Julian Kranz committed
1261
   | LGDT x: sem-undef-arity1 x
Julian Kranz's avatar
Julian Kranz committed
1262
   | LGS x: sem-lds-les-lfs-lgs-lss x GS
Julian Kranz's avatar
Julian Kranz committed
1263 1264 1265
   | 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
1266
   | LODS x: sem-rep-insn x sem-lods
Julian Kranz's avatar
Julian Kranz committed
1267 1268 1269
   | LOOP x: sem-loop x
   | LOOPE x: sem-loope x
   | LOOPNE x: sem-loopne x
Julian Kranz's avatar
Julian Kranz committed
1270
   | LSL x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
1271
   | LSS x: sem-lds-les-lfs-lgs-lss x SS
Julian Kranz's avatar
Julian Kranz committed
1272
   | LTR x: sem-undef-arity1 x
Julian Kranz's avatar
Julian Kranz committed
1273
   | MASKMOVDQU x: sem-maskmovdqu-vmaskmovdqu x
Julian Kranz's avatar
Julian Kranz committed
1274
   | MASKMOVQ x: sem-maskmovq x
Julian Kranz's avatar
Julian Kranz committed
1275 1276 1277 1278 1279 1280 1281 1282 1283 1284
   | 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
1285
   | MOV x: sem-mov '0' x
Julian Kranz's avatar
Julian Kranz committed
1286 1287
   | MOVAPD x: sem-mov '0' x
   | MOVAPS x: sem-mov '0' x
Julian Kranz's avatar
Julian Kranz committed
1288
   | MOVBE x: sem-movbe x
Julian Kranz's avatar
Julian Kranz committed
1289
   | MOVD x: sem-movzx '0' x
Julian Kranz's avatar
Julian Kranz committed
1290
   | MOVDDUP x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
1291
   | MOVDQ2Q x: sem-mov '0' x
Julian Kranz's avatar
Julian Kranz committed
1292 1293
   | MOVDQA x: sem-mov '0' x
   | MOVDQU x: sem-mov '0' x
Julian Kranz's avatar
Julian Kranz committed
1294 1295 1296 1297 1298 1299 1300 1301
   | 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
1302 1303
   | MOVNTDQ x: sem-mov '0' x
   | MOVNTDQA x: sem-mov '0' x
Julian Kranz's avatar
Julian Kranz committed
1304
   | MOVNTI x: sem-mov '0' x
Julian Kranz's avatar
Julian Kranz committed
1305 1306
   | MOVNTPD x: sem-undef-arity2 x
   | MOVNTPS x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
1307 1308 1309
   | 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
1310
   | MOVS x: sem-rep-insn x sem-movs
Julian Kranz's avatar
Julian Kranz committed
1311
   | MOVSD x: sem-undef-arity2 x
Julian Kranz's avatar
Julian Kranz committed
1312 1313 1314 1315 1316 1317 1318 1319
   | 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
1320
   | MOVZX x: sem-movzx '0' x
Julian Kranz's avatar
Julian Kranz committed
1321
   | MPSADBW x: sem-undef-arity3 x
Julian Kranz's avatar
Julian Kranz committed
1322
   | MUL x: sem-mul Unsigned x
Julian Kranz's avatar
Julian Kranz committed
1323 1324 1325 1326
   | 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
1327
   | MWAIT x: sem-nop
Julian Kranz's avatar
Julian Kranz committed
1328
   | NEG x: sem-neg x
Julian Kranz's avatar
Julian Kranz committed
1329
   | NOP x: sem-nop
Julian Kranz's avatar
Julian Kranz committed
1330
   | NOT x: sem-not x
Julian Kranz's avatar
Julian Kranz committed
1331 1332 1333 1334 1335 1336 1337 1338
   | 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
1339 1340 1341
   | 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
1342 1343
   | PACKSSDW x: sem-packsswb-packssdw 16 x
   | PACKSSWB x: sem-packsswb-packssdw 8 x
Julian Kranz's avatar
Julian Kranz committed
1344 1345
   | PACKUSDW x: sem-packuswb-packusdw 16 x
   | PACKUSWB x: sem-packuswb-packusdw 8 x
Julian Kranz's avatar
Julian Kranz committed
1346 1347 1348
   | 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
1349 1350
   | PADDSB x: sem-padds 8 x
   | PADDSW x: sem-padds 16 x
Julian Kranz's avatar
Julian Kranz committed
1351 1352
   | PADDUSB x: sem-paddus 8 x
   | PADDUSW x: sem-paddus 16 x
Julian Kranz's avatar
Julian Kranz committed
1353
   | PADDW x: sem-padd 16 x
Julian Kranz's avatar
Julian Kranz committed
1354
   | PALIGNR x: sem-palignr x
Julian Kranz's avatar
Julian Kranz committed
1355
   | PAND x: sem-pand x
Julian Kranz's avatar
Julian Kranz committed
1356
   | PANDN x: sem-pandn x
Julian Kranz's avatar
Julian Kranz committed
1357
   | PAUSE x: sem-undef-arity0 x
Julian Kranz's avatar
Julian Kranz committed
1358 1359 1360
   | PAVGB x: sem-pavg 8 x
   | PAVGW x: sem-pavg 16 x
   | PBLENDVB x: sem-pblendvb x
Julian Kranz's avatar
Julian Kranz committed
1361
   | PBLENDW x: sem-pblendw x
Julian Kranz's avatar
Julian Kranz committed
1362 1363 1364 1365 1366
   | 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
1367 1368 1369
   | 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
1370 1371 1372 1373
   | 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
1374 1375
   | PCMPISTRI x: sem-undef-arity3 x
   | PCMPISTRM x: sem-undef-arity3 x
Julian Kranz's avatar
Julian Kranz committed
1376 1377 1378 1379
   | 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
1380
   | PHADDD x: sem-phadd 32 x
Julian Kranz's avatar
Julian Kranz committed
1381
   | PHADDSW x: sem-phaddsw x
Julian Kranz's avatar
Julian Kranz committed
1382
   | PHADDW x: sem-phadd 16 x
Julian Kranz's avatar
Julian Kranz committed
1383
   | PHMINPOSUW x: sem-phminposuw-vphminposuw '0' x
Julian Kranz's avatar
Julian Kranz committed
1384
   | PHSUBD x: sem-phsub 32 x
Julian Kranz's avatar
Julian Kranz committed
1385
   | PHSUBSW x: sem-phsubsw x
Julian Kranz's avatar
Julian Kranz committed
1386
   | PHSUBW x: sem-phsub 16 x
Julian Kranz's avatar
Julian Kranz committed
1387 1388 1389 1390
   | 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
1391 1392
   | PMADDUBSW x: sem-pmaddubsw x
   | PMADDWD x: sem-pmaddwd x
Julian Kranz's avatar
Julian Kranz committed
1393 1394 1395
   | 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
1396 1397 1398
   | 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
1399 1400 1401
   | 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
1402 1403 1404
   | PMINUB x: sem-pminu 8 x
   | PMINUD x: sem-pminu 32 x
   | PMINUW x