X86 RREIL Translator

X86 Specification

- Segmentation
- Bug fixes
- Continued to add semantics for: CMPS

specifications/x86/x86-pretty.ml

@@ -279,11 +279,9 @@ val show/instruction insn =
     | CMP x: "CMP" -++ show/arity2 x
     | CMPPD x: "CMPPD" -++ show/arity3 x
     | CMPPS x: "CMPPS" -++ show/arity3 x
-    | CMPSB: "CMPSB"
-    | CMPSD x: "CMPSD" -++ show/varity x
-    | CMPSQ: "CMPSQ"
+    | CMPS x: "CMPS" -++ show/arity2
+    | CMPSD x: "CMPSD" -++ show/arity3 x
     | CMPSS x: "CMPSS" -++ show/arity3 x
-    | CMPSW: "CMPSW"
     | CMPXCHG x: "CMPXCHG" -++ show/arity2 x
     | CMPXCHG16B x: "CMPXCHG16B" -++ show/arity1 x
     | CMPXCHG8B x: "CMPXCHG8B" -++ show/arity1 x

specifications/x86/x86-rreil-translator.ml

@@ -12,10 +12,6 @@ val static-flow-opnd-sz x = do
   return 64
 end
 
-val address-size = do
-  return 32
-end
-
 val runtime-stack-address-size = do
   return 32
 end
@@ -200,6 +196,15 @@ val conv-with conv sz x =
    end
 
 val read sz x = conv-with Unsigned sz x
+
+val read-addr-reg x =
+  case x of
+     MEM m:
+       case m.opnd of
+          REG r: r
+       end
+  end
+
 val read-flow sz x =
    let
       val conv-bv v = return (SEM_LIN_IMM{imm=sx v})
@@ -253,6 +258,7 @@ val write-offset sz x offset =
        end
    end
 
+
 val write sz x = write-offset sz x 0
 val write-upper sz x = write-offset sz x sz
 
@@ -779,18 +785,17 @@ val sem-cmp x = do
 end
 
 val sem-cmps x = do
-  src0-sz <- sizeof1 x.opnd1;
-  src0 <- read src0-sz x.opnd1;
+  opnd-sz <- return x.opnd-sz;
+  src0 <- read opnd-sz x.opnd1;
   src1-sz <- sizeof1 x.opnd2;
-  src1 <- read src1-sz x.opnd2;
-
+  src1 <- read opnd-sz x.opnd2;
 
   temp <- mktemp;
-  sub sz temp src0 src1;
-  emit-sub-sbb-flags sz (var temp) src0 src1 (imm 0);
+  sub opnd-sz temp src0 src1;
+  emit-sub-sbb-flags opnd-sz (var temp) src0 src1 (imm 0);
 
   amount <-
-    case sz of
+    case opnd-sz of
        8: return 1
      | 16: return 2
      | 32: return 4
@@ -798,17 +803,19 @@ val sem-cmps x = do
     end
   ;
 
+  reg0-sem <- return (semantic-register-of (read-addr-reg x.opnd1));
+  reg1-sem <- return (semantic-register-of (read-addr-reg x.opnd2));
+  addr-sz <- return x.addr-sz;
+
   df <- fDF;
   _if (/not (var df)) _then do
-    add reg0-sz reg0-sem (var reg0-sem) (imm amount); 
-    add reg1-sz reg1-sem (var reg1-sem) (imm amount)  
+    add addr-sz reg0-sem (var reg0-sem) (imm amount); 
+    add addr-sz reg1-sem (var reg1-sem) (imm amount)  
   end _else do
-    sub reg0-sz reg0-sem (var reg0-sem) (imm amount);  
-    sub reg1-sz reg1-sem (var reg1-sem) (imm amount)  
+    sub addr-sz reg0-sem (var reg0-sem) (imm amount);  
+    sub addr-sz reg1-sem (var reg1-sem) (imm amount)  
   end
 
-  return void
-
 #  addr-sz <- address-size;
 #
 #  reg0 <-

specifications/x86/x86.ml

@@ -1635,7 +1635,7 @@ val operand-size = do
   #Todo: D flag
   mode64 <- mode64?;
   opndsz <- opndsz?;
-  rexw <- rexw?
+  rexw <- rexw?;
   if mode64 then
     if rexw then
       return 64