X86 RREIL Translator

- Added semantics of: LDDQU
- Cleanup

CFGresolve/CFGresolve/RReil.cpp

@@ -289,9 +289,9 @@ std::ostream& operator<<(std::ostream& o, const Op& s) {
 
 class PrintLinVisitor : public LinVisitor {
   std::ostream& o;
-  int comp = 0;
+  int comp;
 public:
-  PrintLinVisitor(std::ostream& o) : o(o) {};
+  PrintLinVisitor(std::ostream& o) : o(o), comp(0) {};
   void accept(const LinVar& l) {
     o << l.getVar();
   };

CFGresolve/CFGresolve/RReil.h

@@ -12,6 +12,7 @@
 #include <iostream>
 #include <vector>
 #include <inttypes.h>
+#include <algorithm>
 
 class RReilBB;
 typedef char* RReilAddress;

CFGresolve/CFGresolve/Segment.cpp

@@ -9,6 +9,7 @@
 //  Copyright (c) 2012 Axel Simon. All rights reserved.
 //
 
+#include <strings.h>
 #include "Segment.h"
 #include <sys/mman.h>
 #include <unistd.h>

CFGresolve/CFGresolve/main-elf.cpp

+/*
+ * main-elf.cpp
+ *
+ *  Created on: Oct 23, 2012
+ *      Author: jucs
+ */
+
+#include <stdlib.h>
+#include <stdio.h>
+
+int main(void) {
+	printf(":-)\n");
+}

specifications/rreil/rreil.ml

@@ -174,7 +174,6 @@ val divs sz a b c = push (/ASSIGN a (SEM_DIVS{size=sz,opnd1=b,opnd2=c}))
 val shl sz a b c = push (/ASSIGN a (SEM_SHL{size=sz,opnd1=b,opnd2=c}))
 val shr sz a b c = push (/ASSIGN a (SEM_SHR{size=sz,opnd1=b,opnd2=c}))
 val shrs sz a b c = push (/ASSIGN a (SEM_SHRS{size=sz,opnd1=b,opnd2=c}))
-val bswap sz a b = push (/ASSIGN a (SEM_BSWAP{size=sz,opnd1=b}))
 val modulo sz a b c = push (/ASSIGN a (SEM_MOD{size=sz,opnd1=b,opnd2=c}))
 val movsx szA a szB b = push (/ASSIGN a (SEM_SX{size=szA,fromsize=szB,opnd1=b}))
 val movzx szA a szB b = push (/ASSIGN a (SEM_ZX{size=szA,fromsize=szB,opnd1=b}))

specifications/x86/x86-rreil-translator-a-l.ml

+## A>>
+
+val sem-adc x = do
+  sz <- sizeof2 x.opnd1 x.opnd2;
+  a <- write sz x.opnd1;
+  b <- read sz x.opnd1;
+  c <- read sz x.opnd2;
+
+  t <- mktemp;
+  add sz t b c;
+
+  cf <- fCF;
+  tc <- mktemp;
+  movzx sz tc 1 (var cf);
+  add sz t (var t) (var tc);
+
+  emit-add-adc-flags sz (var t) b c (var cf) '1';
+  commit sz a (var t)
+end
+
+val sem-add x = do
+  sz <- sizeof2 x.opnd1 x.opnd2;
+  a <- write sz x.opnd1;
+  b <- read sz x.opnd1;
+  c <- read sz x.opnd2;
+  t <- mktemp;
+  add sz t b c;
+  emit-add-adc-flags sz (var t) b c (imm 0) '1';
+  commit sz a (var t)
+end
+
+#val sem-addpd x = do
+#  size <- return 128;
+#
+#end
+
+val sem-andpd x = do
+  size <- return 128;
+
+  src0 <- read size x.opnd1;
+  src1 <- read size x.opnd2;
+
+  temp <- mktemp;
+  andb size temp src0 src1;
+
+  dst <- write size x.opnd1;
+  commit size dst (var temp)
+end
+
+val sem-vandpd x = do
+  size <- sizeof1 x.opnd1;
+  src0 <- read size x.opnd2;
+  src1 <- read size x.opnd3;
+  out-size <- return 256;
+  
+  temp <- mktemp;
+  andb size temp src0 src1;
+
+  mov (out-size - size) (at-offset temp size) (imm 0);
+
+  dst <- return (semantic-register-of-operand-with-size x.opnd1 out-size);
+  mov out-size dst (var temp)
+end
+
+## B>>
+
+val sem-bsf x = do
+  src <- read x.opnd-sz x.opnd2;
+
+  counter <- mktemp;
+  _if (/neq x.opnd-sz src (imm 0)) _then do
+    mov x.opnd-sz counter (imm 0);
+
+    temp <- mktemp;
+    mov x.opnd-sz temp src;
+
+    _while (/neq 1 (var temp) (imm 1)) __ do
+      add x.opnd-sz counter (var counter) (imm 1);
+      shr x.opnd-sz temp (var temp) (imm 1)
+    end
+
+  end _else
+    return void
+  ;
+
+  zf <- fZF;
+  cmpeq x.opnd-sz zf src (imm 0);
+
+  cf <- fCF;
+  ov <- fOF;
+  sf <- fSF;
+  af <- fAF;
+  pf <- fPF;
+  undef 1 cf;
+  undef 1 ov;
+  undef 1 sf;
+  undef 1 af;
+  undef 1 pf;
+
+  dst <- write x.opnd-sz x.opnd1;
+  commit x.opnd-sz dst (var counter)
+end
+
+val sem-bsr x = do
+  src <- read x.opnd-sz x.opnd2;
+
+  counter <- mktemp;
+  _if (/neq x.opnd-sz src (imm 0)) _then do
+    mov x.opnd-sz counter (imm (x.opnd-sz - 1));
+
+    temp <- mktemp;
+    mov x.opnd-sz temp src;
+
+    _while (/neq 1 (var (at-offset temp (x.opnd-sz - 1))) (imm 1)) __ do
+      sub x.opnd-sz counter (var counter) (imm 1);
+      shl x.opnd-sz temp (var temp) (imm 1)
+    end
+
+  end _else
+    return void
+  ;
+
+  zf <- fZF;
+  cmpeq x.opnd-sz zf src (imm 0);
+
+  cf <- fCF;
+  ov <- fOF;
+  sf <- fSF;
+  af <- fAF;
+  pf <- fPF;
+  undef 1 cf;
+  undef 1 ov;
+  undef 1 sf;
+  undef 1 af;
+  undef 1 pf;
+
+  dst <- write x.opnd-sz x.opnd1;
+  commit x.opnd-sz dst (var counter)
+end
+
+val sem-bswap x = do
+  size <- sizeof1 x.opnd1;
+  src <- read size x.opnd1;
+
+  src-temp <- mktemp;
+  mov size src-temp src;
+
+  temp <- mktemp;
+  if size === 32 then do
+    mov 8 (at-offset temp 0) (var (at-offset src-temp 24));
+    mov 8 (at-offset temp 8) (var (at-offset src-temp 16));
+    mov 8 (at-offset temp 16) (var (at-offset src-temp 8));
+    mov 8 (at-offset temp 24) (var (at-offset src-temp 0))
+  end else do
+    mov 8 (at-offset temp 0) (var (at-offset src-temp 56));
+    mov 8 (at-offset temp 8) (var (at-offset src-temp 48));
+    mov 8 (at-offset temp 16) (var (at-offset src-temp 40));
+    mov 8 (at-offset temp 24) (var (at-offset src-temp 32));
+    mov 8 (at-offset temp 32) (var (at-offset src-temp 24));
+    mov 8 (at-offset temp 40) (var (at-offset src-temp 16));
+    mov 8 (at-offset temp 48) (var (at-offset src-temp 8));
+    mov 8 (at-offset temp 56) (var (at-offset src-temp 0))
+  end;
+
+  dst <- write size x.opnd1;
+  commit size dst (var temp)
+end
+
+val sem-bt-complement base-sz base base-opnd shifted offset-ext = do
+  output <- mktemp;
+  andb base-sz output (var shifted) (imm 1);
+  shl base-sz output (var output) (var offset-ext);
+  xorb base-sz output (var output) base;
+  dst <- write base-sz base-opnd;
+  commit base-sz dst (var output)
+end
+
+val sem-bt-reset base-sz base base-opnd shifted offset-ext = do
+  output <- mktemp;
+  xorb base-sz output (imm (0-1)) (imm 1);
+  shl base-sz output (var output) (var offset-ext);
+  andb base-sz output (var output) base;
+  dst <- write base-sz base-opnd;
+  commit base-sz dst (var output)
+end
+
+val sem-bt-set base-sz base base-opnd shifted offset-ext = do
+  output <- mktemp;
+  shl base-sz output (imm 1) (var offset-ext);
+  orb base-sz output (var output) base;
+  dst <- write base-sz base-opnd;
+  commit base-sz dst (var output)
+end
+
+val sem-bt-none base-sz base base-opnd shifted offset-ext = return void
+
+val sem-bt x modifier = do
+  base-sz <- sizeof1 x.opnd1;
+  base <- read base-sz x.opnd1;
+  offset-sz <- sizeof1 x.opnd2;
+  offset <- read offset-sz x.opnd2;
+
+  offset-real-sz <-
+    case base-sz of
+       16: return 4
+     | 32: return 5
+     | 64: return 6
+    end
+  ;
+
+  offset-ext <- mktemp;
+  mov offset-real-sz offset-ext offset;
+  mov (base-sz - offset-real-sz) (at-offset offset-ext offset-real-sz) (imm 0);
+  
+  shifted <- mktemp;
+  shr base-sz shifted base (var offset-ext);
+  
+  cf <- fCF;
+  mov 1 cf (var shifted);
+
+  modifier base-sz base x.opnd1 shifted offset-ext;
+
+  ov <- fOF;
+  sf <- fSF;
+  af <- fAF;
+  pf <- fPF;
+  undef 1 ov;
+  undef 1 sf;
+  undef 1 af;
+  undef 1 pf
+end
+
+## C>>
+
+val sem-call x = do
+  ip-sz <-
+    if (x.opnd-sz === 64) then
+      return 64
+    else
+      return 32
+  ;
+  temp-ip <- mktemp;
+  
+  mode64 <- mode64?;
+  ip <- ip-get;
+  if (near x.opnd1) then do
+    target <- read-flow ip-sz x.opnd1;
+    if (relative x.opnd1) then do
+      add ip-sz temp-ip ip target;
+      if (x.opnd-sz === 16) then
+          mov (ip-sz - x.opnd-sz) (at-offset temp-ip x.opnd-sz) (imm 0)
+      else
+         return void
+    end else
+      mov ip-sz temp-ip target
+    ;
+    ps-push ip-sz ip
+  end else do
+    sec-reg <- return CS;
+    sec-reg-sem <- return (semantic-register-of sec-reg);
+    reg-size <- sizeof1 (REG sec-reg);
+    sec-reg-extended <- mktemp;
+    movzx x.opnd-sz sec-reg-extended reg-size (var sec-reg-sem);
+    ps-push x.opnd-sz (var sec-reg-extended);
+    ps-push ip-sz ip;
+  
+    target-sz <- sizeof-flow x.opnd1;
+    target <- read-flow target-sz x.opnd1;
+
+    temp-target <- mktemp;
+    mov target-sz temp-target target;
+    mov reg-size sec-reg-sem (var (at-offset temp-target x.opnd-sz));
+
+    temp-ip <- mktemp;
+    movzx ip-sz temp-ip x.opnd-sz target
+  end;
+    
+  call (address ip-sz (var temp-ip))
+end
+
+val sem-convert size = do
+  src <- return (semantic-register-of (register-by-size low A size));
+  dst <- return (semantic-register-of (register-by-size low A (2*size)));
+
+  movsx dst.size dst src.size (var src)
+end
+
+val sem-cdqe = do
+  a <- return (semantic-register-of RAX);
+  movsx 64 a 32 (var a)
+end
+
+val sem-clc = do
+  cf <- fCF;
+  mov 1 cf (imm 0)
+end
+
+val sem-cld = do
+  df <- fDF;
+  mov 1 df (imm 0)
+end
+
+val sem-cmc = do
+  cf <- fCF;
+  xorb 1 cf (var cf) (imm 1)
+end
+
+val sem-cmovcc x cond = do
+  sz <- sizeof1 x.opnd1;
+  dst <- write sz x.opnd1;
+  dst-read <- read sz x.opnd1;
+
+  src <- read sz x.opnd2;
+
+  temp <- mktemp;
+  mov sz temp dst-read;
+
+  _if cond _then
+    mov sz temp src
+  ;
+
+  commit sz dst (var temp)
+end
+
+val sem-cmp x = do
+  sz <- sizeof2 x.opnd1 x.opnd2;
+  a <- write sz x.opnd1;
+  b <- read sz x.opnd1;
+  c <- read sz x.opnd2;
+  t <- mktemp;
+  sub sz t b c;
+  emit-sub-sbb-flags sz (var t) b c (imm 0) '1'
+end
+
+val sem-cmps x = do
+  src0 <- read x.opnd-sz x.opnd1;
+  src1-sz <- sizeof1 x.opnd2;
+  src1 <- read x.opnd-sz x.opnd2;
+
+  temp <- mktemp;
+  sub x.opnd-sz temp src0 src1;
+  emit-sub-sbb-flags x.opnd-sz (var temp) src0 src1 (imm 0) '1';
+
+  reg0-sem <- return (semantic-register-of (read-addr-reg x.opnd1));
+  reg1-sem <- return (semantic-register-of (read-addr-reg x.opnd2));
+
+  direction-adjust x.addr-sz reg0-sem x.opnd-sz;
+  direction-adjust x.addr-sz reg1-sem x.opnd-sz
+
+#  addr-sz <- address-size;
+#
+#  reg0 <-
+#    case addr-sz of
+#       16: return SI
+#     | 32: return ESI
+#     | 64: return RSI
+#    end
+#  ;
+#  reg0-sem <- return (semantic-register-of reg0);
+#  reg0-sz <- sizeof1 (REG reg0);
+#  
+#  #Todo: Fix, use specified segment
+#  reg0-segment <- segment DS;
+#  src0 <- read sz (MEM{sz=sz,psz=addr-sz,segment=reg0-segment,opnd=REG reg0});
+#
+#  reg1 <-
+#    case addr-sz of
+#       16: return DI
+#     | 32: return EDI
+#     | 64: return RDI
+#    end
+#  ;
+#  reg1-sem <- return (semantic-register-of reg1);
+#  reg1-sz <- sizeof1 (REG reg1);
+#  reg1-segment <- segment ES;
+#  src1 <- read sz (MEM{sz=sz,psz=addr-sz,segment=reg1-segment,opnd=REG reg1});
+#
+end
+#val sem-cmpsb = sem-cmps 8
+#val sem-cmpsw = sem-cmps 16
+#val sem-cmpsd = sem-cmps 32
+#val sem-cmpsq = sem-cmps 64
+
+val sem-cmpxchg x = do
+  size <- sizeof1 x.opnd1;
+
+  subtrahend <- read size x.opnd1;
+  minuend <- return (semantic-register-of (register-by-size low A size)); #accumulator
+
+  difference <- mktemp;
+  sub size difference (var minuend) subtrahend;
+
+  emit-sub-sbb-flags size (var difference) (var minuend) subtrahend (imm 0) '1';
+  
+  zf <- fZF;
+  _if (/d (var zf)) _then do
+    dst <- write size x.opnd1;
+    src <- read size x.opnd2;
+    commit size dst src
+  end _else do
+    dst <- read size x.opnd1;
+    mov size minuend dst
+  end
+end
+
+val sem-cmpxchg16b-cmpxchg8b x = do
+  subtrahend <- read (2*x.opnd-sz) x.opnd1;
+
+  minuend <- combine (register-by-size low C x.opnd-sz) (register-by-size low B x.opnd-sz);
+
+  difference <- mktemp;
+  sub (2*x.opnd-sz) difference (var minuend) subtrahend;
+
+  emit-sub-sbb-flags (2*x.opnd-sz) (var difference) (var minuend) subtrahend (imm 0) '1';
+
+  zf <- fZF;
+  _if (/d (var zf)) _then do
+    dst <- write (2*x.opnd-sz) x.opnd1;
+    commit (2*x.opnd-sz) dst (var minuend)
+  end _else do
+    dst <- combine (register-by-size low D x.opnd-sz) (register-by-size low A x.opnd-sz);
+    mov (2*x.opnd-sz) dst subtrahend
+  end
+end
+
+val sem-cpuid x = do
+  #Todo: ;-)
+  eax <- return (semantic-register-of EAX);
+  ebx <- return (semantic-register-of EBX);
+  ecx <- return (semantic-register-of ECX);
+  edx <- return (semantic-register-of EDX);
+  
+  undef eax.size eax;
+  undef ebx.size ebx;
+  undef ecx.size ecx;
+  undef edx.size edx
+end
+
+val sem-cwd-cdq-cqo x = do
+  src <-
+    case x.opnd-sz of
+       16: return AX
+     | 32: return EAX
+     | 64: return RAX
+    end
+  ;
+  src-sem <- return (semantic-register-of src);
+  
+  temp <- mktemp;
+  movsx (src-sem.size + src-sem.size) temp src-sem.size (var src-sem);
+
+  dst-high <-
+    case x.opnd-sz of
+       16: return DX
+     | 32: return EDX
+     | 64: return RDX
+    end
+  ;
+  
+  dst-high-sem <- return (semantic-register-of dst-high);
+  mov dst-high-sem.size dst-high-sem (var (at-offset temp src-sem.size))
+end
+
+## D>>
+
+val sem-dec x = do
+  sz <- sizeof1 x.opnd1;
+  src <- read sz x.opnd1;
+  dst <- write sz x.opnd1;
+
+  temp <- mktemp;
+  sub sz temp src (imm 1);
+  
+  emit-sub-sbb-flags sz (var temp) src (imm 1) (imm 0) '0';
+
+  commit sz dst (var temp)
+end
+
+val sem-div signedness x = do
+  sz <- sizeof1 x.opnd1;
+  divisor <- read (sz + sz) x.opnd1;
+
+  dividend <-
+    case sz of
+       8: return (semantic-register-of AX)
+     | _: combine (register-by-size low D sz) (register-by-size low A sz)
+    end
+  ;
+
+  quotient <- mktemp;
+  #Todo: Handle exception
+  case signedness of
+     Unsigned: div (sz + sz) quotient (var dividend) divisor
+   | Signed: divs (sz + sz) quotient (var dividend) divisor
+  end;
+  quotient-sem <- return (semantic-register-of (register-by-size low A sz));
+  mov sz quotient-sem (var quotient);
+
+  remainder <- mktemp;
+  modulo (sz + sz) remainder (var dividend) divisor;
+  remainder-sem <-
+    case sz of
+       8: return (semantic-register-of AH)
+     | _: return (semantic-register-of (register-by-size high D sz))
+    end
+  ;
+  mov sz remainder-sem (var remainder);
+
+  cf <- fCF;
+  ov <- fOF;
+  sf <- fSF;
+  zf <- fZF;
+  af <- fAF;
+  pf <- fPF;
+
+  undef 1 cf;
+  undef 1 ov;
+  undef 1 sf;
+  undef 1 zf;
+  undef 1 af;
+  undef 1 pf
+end
+
+## E>>
+## F>>
+## G>>
+## H>>
+
+val sem-hlt = do
+  return void
+end
+