X86 Specification

X86 RREIL Translator
RREIL Specification

- Bug fixes
- Cleanup

specifications/rreil/rreil.ml

@@ -26,7 +26,7 @@ type sem_linear =
 
 type sem_op =
    SEM_LIN of sem_arity1
- | SEM_BSWAP of sem_arity1 
+ | SEM_BSWAP of sem_arity1
  | SEM_MUL of sem_arity2
  | SEM_DIV of sem_arity2
  | SEM_DIVS of sem_arity2
@@ -47,7 +47,7 @@ type sem_op =
  | SEM_CMPLTU of sem_cmp
  | SEM_ARB of {size: int}
 
-type sem_stmt = 
+type sem_stmt =
    SEM_ASSIGN of {lhs: sem_var, rhs: sem_op}
  | SEM_LOAD of {lhs: sem_var, size: int, address: sem_address}
  | SEM_STORE of {address: sem_address, rhs: sem_op}
@@ -57,7 +57,7 @@ type sem_stmt =
  | SEM_CALL of {cond: sem_linear, size:int, target: sem_linear}
  | SEM_RETURN of {cond: sem_linear, size:int, target: sem_linear}
 
-type sem_stmts = 
+type sem_stmts =
    SEM_CONS of {hd:sem_stmt, tl:sem_stmts}
  | SEM_NIL
 
@@ -68,7 +68,7 @@ type sem_writeback =
 val rreil-sizeOf op =
    case op of
       SEM_LIN x: x.size
-    | SEM_BSWAP x: x.size 
+    | SEM_BSWAP x: x.size
     | SEM_MUL x: x.size
     | SEM_DIV x: x.size
     | SEM_DIVS x: x.size

specifications/x86/x86-rreil-translator.ml

@@ -2,7 +2,7 @@
 
 export = translate
 
-val guess-sizeof dst/src1 src2 = 
+val guess-sizeof dst/src1 src2 =
    case dst/src1 of
       REG r: return ($size (semantic-register-of r))
     | MEM x: return x.sz
@@ -25,13 +25,13 @@ val guess-sizeof1 op =
     | IMM64 i: return 64
    end
 
-val conv-with conv sz x = 
+val conv-with conv sz x =
    let
       val conv-imm conv x = return (SEM_LIN_IMM{imm=conv x})
-     
+
       val conv-reg r = return (SEM_LIN_VAR (semantic-register-of r))
 
-      val conv-sum conv sz x = 
+      val conv-sum conv sz x =
          do op1 <- conv-with conv sz x.a;
             op2 <- conv-with conv sz x.b;
             return
@@ -122,7 +122,7 @@ val commit sz a b =
                      end
                 | _: mov sz x.id b
                end
-          | _: mov sz x.id b 
+          | _: mov sz x.id b
          end
    end
 
@@ -198,7 +198,7 @@ val emit-add-flags sz a b c =
       t2 <- mktemp;
       t3 <- mktemp;
       zer0 <- zero;
-      # HACKERS-DELIGHT p27 
+      # HACKERS-DELIGHT p27
       # TODO: Compute {ltu} flag
       undef 1 ltu;
       xorb sz t1 a b;
@@ -212,7 +212,7 @@ val emit-add-flags sz a b c =
       orb 1 les (var lts) (var eq)
    end
 
-val emit-sub-flags sz a b c = 
+val emit-sub-flags sz a b c =
    do eq <- fEQ;
       les <- fLES;
       leu <- fLEU;
@@ -295,13 +295,13 @@ val sem-shl x = do
   convert sz cnt szOp2 c;
   andb sz cnt (var cnt) mask;
   cmpeq sz cntIsZero (var cnt) zer0;
-  ifgotolabel (var cntIsZero) nop; 
+  ifgotolabel (var cntIsZero) nop;
   shl sz t1 b (/SUB (var cnt) one);
   mov 1 cf (var (t1 /+ (sz - 1)));
   shl sz t2 b (var cnt);
   cmpeq sz cntIsOne (var cnt) one;
   ifgotolabel (var cntIsOne) setflag;
-  undef 1 ov; 
+  undef 1 ov;
   gotolabel exit;
   label setflag;
   xorb 1 ov (var cf) (var (t2 /+ (sz - 1)));
@@ -327,7 +327,7 @@ val sem-je x = do
   sz <- guess-sizeof-flow x.opnd1;
   target <- read-flow sz x.opnd1;
   eq <- fEQ;
-  ifgoto (var eq) sz target 
+  ifgoto (var eq) sz target
 end
 
 val sem-jb x = do
@@ -1276,14 +1276,14 @@ val semantics insn =
 #s/^ | \([^\s]*\) of varity\s*/ | \1 x: sem-undef-varity x/g
 #s/^ | \(\S*\)\s*$/ | \1: sem-undef-arity0/g
 
-val translate insn = 
+val translate insn =
    do update@{stack=SEM_NIL,tmp=0,lab=0};
       semantics insn;
       stack <- query $stack;
       return (rreil-stmts-rev stack)
    end
 
-val translate-bottom-up insn = 
+val translate-bottom-up insn =
    do update@{stack=SEM_NIL,tmp=0,lab=0};
       semantics insn;
       stack <- query $stack;

specifications/x86/x86.ml

@@ -3390,8 +3390,6 @@ val /66 [0x0f 0x38 0x82 /r-mem]
  | mode64? = binop INVPCID r64 m128
  | mode32? = binop INVPCID r32 m128
 
-### =><=
-
 ### IRET/IRETD
 ###  - Interrupt Return
 val / [0xcf]
@@ -3473,18 +3471,21 @@ val / [0x0f 0x88] # JS
 
 ### JMP
 ###  - Jump
-#TODO: jmp far
 val / [0xeb] = near-rel JMP rel8
-val /66 [0xe9]
- | mode64? = near-rel JMP rel32
- | otherwise = near-rel JMP rel16
-val / [0xe9] = near-rel JMP rel32
-val /66 [0xff /4]
- | mode64? = near-abs JMP r/m64
- | otherwise = near-abs JMP r/m16
+val / [0xe9]
+ | mode32? & opndsz? = near-rel JMP rel16
+ | otherwise = near-rel JMP rel32
 val / [0xff /4]
+ | mode32? & opndsz? = near-abs JMP r/m16
+ | mode32? = near-abs JMP r/m32
  | mode64? = near-abs JMP r/m64
- | otherwise = near-abs JMP r/m32
+val / [0xea]
+ | mode32? & opndsz? = far-dir JMP ptr16/16
+ | mode32? = far-dir JMP ptr16/32
+val / [0xff /5]
+ | opndsz? = far-ind JMP m16/16
+ | rexw? = far-ind JMP m16/64
+ | otherwise = far-ind JMP m16/32
 
 ### LAHF
 ###  - Load Status Flags into AH Register
@@ -3502,7 +3503,7 @@ val / [0x0f 0x02 /r]
 val /f2 [0x0f 0xf0 /r-mem] = binop LDDQU xmm128 m128
 val /vex/f2/0f [0xf0 /r-mem]
  | vex128? = varity2 VLDDQU xmm128 m128
- | otherwise = varity2 VLDDQU ymm256 m256
+ | vex256? = varity2 VLDDQU ymm256 m256
 
 ### LDMXCSR
 ###  - Load MXCSR Register
@@ -3510,6 +3511,8 @@ val / [0x0f 0xae /2-mem] = unop LDMXCSR m32
 val /vex/0f [0xae /2-mem]
  | vex128? = varity1 VLDMXCSR m32
 
+### =><=
+
 ### LDS/LES/LFS/LGS/LSS
 ###  - Load Far Pointer
 val / [0xc5 /r-mem]