diff --git a/CFGresolve/CFGresolve/RReil.cpp b/CFGresolve/CFGresolve/RReil.cpp
index 6417ba11d4a8ec908d2b4182d00234f0fa645b0f..c5e7ecb4ade8ec0454c641fea5b67383d1308230 100644
--- a/CFGresolve/CFGresolve/RReil.cpp
+++ b/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();
   };
diff --git a/CFGresolve/CFGresolve/RReil.h b/CFGresolve/CFGresolve/RReil.h
index 6ddd93e3970ef4addc0f297089093ac035904e74..584ee882b73f1f68a1807097c98320dd734ecd6d 100644
--- a/CFGresolve/CFGresolve/RReil.h
+++ b/CFGresolve/CFGresolve/RReil.h
@@ -12,6 +12,7 @@
 #include <iostream>
 #include <vector>
 #include <inttypes.h>
+#include <algorithm>
 
 class RReilBB;
 typedef char* RReilAddress;
diff --git a/CFGresolve/CFGresolve/Segment.cpp b/CFGresolve/CFGresolve/Segment.cpp
index 742aa7554f713f8329e62156052876bfb96ea6e2..88a52b81b594d92d6a82ed8cbbc6561e34a5d6f2 100644
--- a/CFGresolve/CFGresolve/Segment.cpp
+++ b/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>
diff --git a/CFGresolve/CFGresolve/main-elf.cpp b/CFGresolve/CFGresolve/main-elf.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..251ce3842e2855648b97bdbd27da0ee51481e32a
--- /dev/null
+++ b/CFGresolve/CFGresolve/main-elf.cpp
@@ -0,0 +1,13 @@
+/*
+ * main-elf.cpp
+ *
+ *  Created on: Oct 23, 2012
+ *      Author: jucs
+ */
+
+#include <stdlib.h>
+#include <stdio.h>
+
+int main(void) {
+	printf(":-)\n");
+}
diff --git a/specifications/rreil/rreil.ml b/specifications/rreil/rreil.ml
index d920bec75604efaea00feec26f0a7705b692183e..1823da783e0d3e25e3010b62c1932bc5d73559dd 100644
--- a/specifications/rreil/rreil.ml
+++ b/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}))
diff --git a/specifications/x86/x86-rreil-translator-a-l.ml b/specifications/x86/x86-rreil-translator-a-l.ml
new file mode 100644
index 0000000000000000000000000000000000000000..359b2e511ff5ef96a0db708296f0745432f30b7f
--- /dev/null
+++ b/specifications/x86/x86-rreil-translator-a-l.ml
@@ -0,0 +1,726 @@
+## 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
+
+## I>>
+
+val sem-idiv x = sem-div Signed x
+
+val sem-imul-1 x = sem-mul Signed x
+val sem-imul-2-3 op1 op2 op3 = do
+  sz <- sizeof1 op1;
+
+  factor0 <- reads Signed (sz + sz) op2;
+  factor1 <- reads Signed (sz + sz) op3;
+
+  product <- mktemp;
+  mul (sz + sz) product factor0 factor1;
+
+  emit-mul-flags sz product;
+
+  result <- write sz op1;
+  commit sz result (var product)
+end
+val sem-imul-2 x = sem-imul-2-3 x.opnd1 x.opnd1 x.opnd2
+val sem-imul-3 x = sem-imul-2-3 x.opnd1 x.opnd2 x.opnd3
+
+val sem-inc x = do
+  sz <- sizeof1 x.opnd1;
+  src <- read sz x.opnd1;
+  dst <- write sz x.opnd1;
+
+  temp <- mktemp;
+  add 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-invd = return void
+
+## J>>
+
+val sem-jcc x cond = do
+  ip-sz <-
+    if (x.opnd-sz === 64) then
+      return 64
+    else
+      return 32
+  ;
+  ip <- ip-get;
+
+  target <- read-flow ip-sz x.opnd1;
+
+  temp-ip <- mktemp;
+  add ip-sz temp-ip target ip;
+
+  cond <- cond;
+  cbranch cond (address ip-sz (var temp-ip)) (address ip-sz ip)
+end
+
+val sem-jregz x reg = do
+  reg-sem <- return (semantic-register-of reg);
+  sem-jcc x (/eq reg-sem.size (var reg-sem) (imm 0))
+end
+
+val sem-jcxz x = sem-jregz x CX
+val sem-jecxz x = sem-jregz x ECX
+val sem-jrcxz x = sem-jregz x RCX
+
+val sem-jmp x = do
+  mode64 <- mode64?;
+  ip-sz <-
+    if mode64 then
+      return 64
+    else
+      return 32
+  ;
+  temp-ip <- mktemp;
+
+  if (near x.opnd1) then do
+    target <- read-flow ip-sz x.opnd1;
+    if (relative x.opnd1) then do
+      ip <- ip-get;
+      add ip-sz temp-ip ip target
+    end else
+      mov ip-sz temp-ip target
+    ;
+    if (x.opnd-sz === 16) then
+      #andb ip-sz temp-ip (var temp-ip) (imm 0xffff)
+      mov (ip-sz - x.opnd-sz) (at-offset temp-ip x.opnd-sz) (imm 0)
+    else
+      return void
+    end
+  else if (not mode64) then do
+    target-sz <- sizeof-flow x.opnd1;
+    target <- read-flow target-sz x.opnd1;
+    movzx ip-sz temp-ip x.opnd-sz target;
+    #if (opnd-sz === 16) then
+    #  #andb ip-sz temp-ip (var temp-ip) (imm 0xffff)
+    #  mov (ip-sz - opnd-sz) (at-offset temp-ip x.opnd-sz) (imm 0)
+    #else
+    #  return void
+    #;
+    reg <- return CS;
+    reg-sem <- return (semantic-register-of reg);
+    reg-size <- sizeof1 (REG reg);
+    temp-target <- mktemp;
+    mov target-sz temp-target target;
+    mov reg-size reg-sem (var (at-offset temp-target x.opnd-sz))
+  end else
+    return void
+  ;
+
+  jump (address ip-sz (var temp-ip))
+end
+
+## K>>
+## L>>
+
+val sem-lahf = do
+  ah <- return (semantic-register-of AH);
+  flags <- rflags;
+
+  mov ah.size ah (var flags)
+end
+
+val sem-lar x = do
+  sem-undef-arity2
+end
+
+val sem-lddqu-vlddqu size x = do
+  src <- read size x.opnd2;
+  dst <- write size x.opnd1;
+
+  commit size dst src
+end
+
+val sem-lddqu x = sem-lddqu-vlddqu 128 x;
+val sem-vlddqu x = sem-lddqu-vlddqu 256 x;
+
+val sem-lea x = do
+  opnd-sz <- sizeof1 x.opnd1;
+  dst <- write opnd-sz x.opnd1;
+  src <-
+    case x.opnd2 of
+      MEM m: return m
+    end
+  ;
+  addr-sz <- return src.psz;
+  address <- conv-with Signed src.psz src.opnd;
+
+  temp <- mktemp;
+  movzx opnd-sz temp addr-sz address;
+
+  commit opnd-sz dst (var temp)
+end
+
+val sem-lods x = do
+  sz <- sizeof1 x.opnd1;
+  src <- read sz x.opnd1;
+
+  dst <- return (semantic-register-of (register-by-size low A sz));
+
+  mov dst.size dst src
+end
+
+val sem-loop-loop x = do
+  reg <- return (semantic-register-of (
+    case x.addr-sz of
+       32: ECX
+     | 64: RCX
+     | _: CX
+    end
+  ));
+
+  sub reg.size reg (var reg) (imm 1);
+
+  return reg
+end
+
+val sem-loop x = do
+  reg <- sem-loop-loop x;
+  sem-jcc x (/neq reg.size (var reg) (imm 0))
+end
+
+val sem-loope x = do
+  reg <- sem-loop-loop x;
+  zf <- fZF;
+  sem-jcc x (/and (/d (var zf)) (/neq reg.size (var reg) (imm 0)))
+end
+
+val sem-loopne x = do
+  reg <- sem-loop-loop x;
+  zf <- fZF;
+  sem-jcc x (/and (/not (var zf)) (/neq reg.size (var reg) (imm 0)))
+end
+
diff --git a/specifications/x86/x86-rreil-translator-m-z.ml b/specifications/x86/x86-rreil-translator-m-z.ml
new file mode 100644
index 0000000000000000000000000000000000000000..ec7bc2650287be19d9328f480331d5f4f8741e7b
--- /dev/null
+++ b/specifications/x86/x86-rreil-translator-m-z.ml
@@ -0,0 +1,793 @@
+## M>>
+
+val sem-mov x = do
+  sz <- sizeof2 x.opnd1 x.opnd2;
+  a <- write sz x.opnd1;
+  b <- read sz x.opnd2;
+  commit sz a b
+end
+
+val sem-movap x = do
+  sz <- sizeof1 x.opnd1;
+  dst <- write sz x.opnd1;
+  src <- read sz x.opnd2;
+
+  temp <- mktemp;
+  mov sz temp src;
+
+  commit sz dst (var temp)
+end
+
+val sem-vmovap x = do
+  x <- case x of VA2 x: return x end;
+
+  sz <- sizeof1 x.opnd1;
+  dst <- write sz x.opnd1;
+  src <- read sz x.opnd2;
+
+  if sz === 128 then
+    do
+      dst-upper <- write-upper sz x.opnd1;
+      commit sz dst-upper (imm 0)
+    end
+  else
+    return void
+  ;
+
+  temp <- mktemp;
+  mov sz temp src;
+  commit sz dst (var temp)
+end
+
+val sem-movs x = do
+  sz <- sizeof1 x.opnd1;
+  src <- read sz x.opnd2;
+  dst <- write sz x.opnd1;
+  commit sz dst src
+end
+
+val sem-movsx x = do
+  sz-dst <- sizeof1 x.opnd1;
+  sz-src <- sizeof1 x.opnd2;
+  dst <- write sz-dst x.opnd1;
+  src <- read sz-src x.opnd2;
+
+  temp <- mktemp;
+  movsx sz-dst temp sz-src src;
+
+  commit sz-dst dst (var temp)
+end
+
+val sem-movzx x = do
+  sz-dst <- sizeof1 x.opnd1;
+  sz-src <- sizeof1 x.opnd2;
+  dst <- write sz-dst x.opnd1;
+  src <- read sz-src x.opnd2;
+
+  temp <- mktemp;
+  movzx sz-dst temp sz-src src;
+
+  commit sz-dst dst (var temp)
+end
+
+val sem-mul conv x = do
+  sz <- sizeof1 x.opnd1;
+
+  factor0-sem <- return (semantic-register-of (register-by-size low A sz));
+  factor0 <- expand conv (var factor0-sem) sz (sz + sz);
+
+  factor1 <- reads conv (sz + sz) x.opnd1;
+
+  product <- mktemp;
+  mul (sz + sz) product factor0 factor1;
+
+  emit-mul-flags sz product;
+
+  case sz of
+     8: do
+       ax <- return (semantic-register-of AX);
+       mov sz ax (var product)
+     end
+   | _: do
+       high <- return (semantic-register-of (register-by-size low D sz));
+       low <- return (semantic-register-of (register-by-size low A sz));
+
+       mov sz high (var (at-offset product sz));
+       mov sz low (var product)
+   end
+  end
+end
+
+## N>>
+
+val sem-nop x = do
+  return void
+end
+
+## O>>
+
+val sem-or x = do
+  sz <- sizeof2 x.opnd1 x.opnd2;
+  dst <- write sz x.opnd1;
+  src0 <- read sz x.opnd1;
+  src1 <- read sz x.opnd2;
+  temp <- mktemp;
+  orb sz temp src0 src1;
+
+  ov <- fOF;
+  mov 1 ov (imm 0);
+  cf <- fCF;
+  mov 1 cf (imm 0);
+  sf <- fSF;
+  cmplts sz sf (var temp) (imm 0);
+  zf <- fZF;
+  cmpeq sz zf (var temp) (imm 0);
+  emit-parity-flag (var temp);
+  af <- fAF;
+  undef 1 af;
+
+  commit sz dst (var temp)
+end
+
+## P>>
+
+val ps-pop opnd-sz opnd = do
+  stack-addr-sz <- runtime-stack-address-size;
+
+  sp-reg <-
+    if stack-addr-sz === 32 then
+      return ESP
+    else if stack-addr-sz === 64 then
+      return RSP
+    else
+      return SP
+  ;
+  
+  sp <- return (semantic-register-of sp-reg);
+  sp-size <- sizeof1 (REG sp-reg);
+
+  segmented-load opnd-sz opnd stack-addr-sz (var sp) (SEG_OVERRIDE SS);
+
+  if stack-addr-sz === 32 then
+    if opnd-sz === 32 then
+      add sp-size sp (var sp) (imm 4)
+    else
+      add sp-size sp (var sp) (imm 2)
+  else if stack-addr-sz === 64 then
+    if opnd-sz === 64 then
+      add sp-size sp (var sp) (imm 8)
+    else
+      add sp-size sp (var sp) (imm 2)
+  else
+    if opnd-sz === 16 then
+      add sp-size sp (var sp) (imm 2)
+    else
+      add sp-size sp (var sp) (imm 4)
+
+  #Todo: Special actions in protected mode
+end
+
+val sem-pop x = do
+  dst <- write x.opnd-sz x.opnd1;
+  temp-dest <- mktemp;
+  ps-pop x.opnd-sz temp-dest;
+  commit x.opnd-sz dst (var temp-dest)
+end
+
+val sem-popf x = do
+  popped <- mktemp;
+  ps-pop x.opnd-sz popped;
+
+  move-to-rflags x.opnd-sz (var popped)
+end
+
+val ps-push opnd-sz opnd = do
+  mode64 <- mode64?;
+  stack-addr-sz <- runtime-stack-address-size;
+  
+  sp-reg <-
+    if mode64 then
+      return RSP
+    else if stack-addr-sz === 32 then
+      return ESP
+    else
+      return SP
+  ;
+  sp <- return (semantic-register-of sp-reg);
+
+  if mode64 then
+    if opnd-sz === 64 then
+      sub sp.size sp (var sp) (imm 8)
+    else
+      sub sp.size sp (var sp) (imm 2)
+  else
+    if opnd-sz === 32 then
+      sub sp.size sp (var sp) (imm 4)
+    else
+      sub sp.size sp (var sp) (imm 2)
+  ;
+
+  segmented-store (address sp.size (var sp)) (lin opnd-sz opnd) (SEG_OVERRIDE SS)
+
+  #store (address sp.size (segment-add (var sp) segment)) (lin opnd-sz opnd)
+end
+
+val sem-push x = do
+  src-size <- sizeof1 x.opnd1;
+  src <- read src-size x.opnd1;
+
+  temp <- mktemp;
+  case x.opnd1 of
+     REG r: 
+       if segment-register? r then
+         movzx x.opnd-sz temp src-size src
+       else
+         mov x.opnd-sz temp src
+   | MEM m:
+       mov x.opnd-sz temp src
+   | IMM8 i:
+       movsx x.opnd-sz temp src-size src
+   | IMM16 i:
+       mov x.opnd-sz temp src
+   | IMM32 i:
+       movsx x.opnd-sz temp src-size src
+  end;
+
+  ps-push x.opnd-sz (var temp)
+end
+
+val sem-pushf x = do
+  mask <- return 0x0000000000fcffff;
+  flags <- rflags;
+
+  temp <- mktemp;
+  andb flags.size temp (var flags) (imm mask);
+
+  ps-push x.opnd-sz (var temp)
+end
+
+## Q>>
+## R>>
+
+val sem-rep-repe-repne size sem fc = do
+  count-reg <- return (semantic-register-of (register-by-size low DI_ size));
+
+  cond-creg <- let
+    val v = /neq size (var count-reg) (imm 0)
+  in
+    return v
+  end;
+
+  cond <- mktemp;
+  c <- cond-creg;
+  mov 1 cond c;
+  _while (/d (var cond)) __ do
+    sem;
+
+    c <- /and cond-creg fc;
+    mov 1 cond c
+  end
+end
+
+val sem-rep size sem = sem-rep-repe-repne size sem (return (imm 1))
+
+val sem-repe size sem = let
+  val fc = do
+    zf <- fZF;
+    /not (var zf)
+  end
+in
+  sem-rep-repe-repne size sem fc
+end
+
+val sem-repne size sem = let
+  val fc = do
+    zf <- fZF;
+    /d (var zf)
+  end
+in
+  sem-rep-repe-repne size sem fc
+end
+
+val sem-repe-repne-insn x sem =
+  if x.rep then
+    sem-repe x.addr-sz (sem x)
+  else if x.repne then
+    sem-repne x.addr-sz (sem x)
+  else
+     sem x
+
+val sem-rep-insn x sem =
+  if x.rep then
+    sem-rep x.addr-sz (sem x)
+  else
+     sem x
+
+val sem-ret x =
+  case x of
+     VA0 x: sem-ret-without-operand x
+   | VA1 x:
+       do
+         release-from-stack x;
+	 sem-ret-without-operand x
+       end
+  end
+
+val sem-ret-far x =
+  case x of
+     VA0 x: sem-ret-far-without-operand x
+   | VA1 x:
+       do
+         release-from-stack x;
+         sem-ret-far-without-operand x
+       end
+  end
+
+val pop-ip opnd-sz = do
+  ip-sz <-
+    if (opnd-sz === 64) then
+      return 64
+    else
+      return 32
+  ;
+
+  temp-ip <- mktemp;
+  ps-pop ip-sz temp-ip;
+  mov (ip-sz - opnd-sz) (at-offset temp-ip opnd-sz) (imm 0);
+
+  return (address opnd-sz (var temp-ip))
+end
+
+val sem-ret-without-operand x = do
+  address <- pop-ip x.opnd-sz;
+  ret address
+end
+
+val sem-ret-far-without-operand x = do
+  address <- pop-ip x.opnd-sz;
+
+  temp-cs <- mktemp;
+  ps-pop x.opnd-sz temp-cs;
+  
+  sec-reg <- return CS;
+  sec-reg-sem <- return (semantic-register-of sec-reg);
+  reg-size <- sizeof1 (REG sec-reg);
+
+  mov reg-size sec-reg-sem (var temp-cs);
+
+  ret address
+end
+
+val release-from-stack x = do
+  x-sz <- sizeof1 x.opnd1;
+  src <- read x-sz x.opnd1;
+
+  stack-addr-sz <- runtime-stack-address-size;
+
+  sp-reg <-
+    if stack-addr-sz === 32 then
+      return ESP
+    else if stack-addr-sz === 64 then
+      return RSP
+    else
+      return SP
+  ;
+
+  sp <- return (semantic-register-of sp-reg);
+  sp-size <- sizeof1 (REG sp-reg);
+
+  src-ext <- mktemp;
+  movzx sp-size src-ext x-sz src;
+
+  add sp-size sp (var sp) (var src-ext)
+end
+
+## S>>
+
+val sem-sahf x = do
+  ah <- return (semantic-register-of AH);
+  flags <- rflags;
+
+  move-to-rflags ah.size (var ah)
+end
+
+val sem-sal-shl x = do
+  sz <- sizeof1 x.opnd1;
+  szOp2 <- sizeof1 x.opnd2;
+  dst <- write sz x.opnd1;
+  src <- read sz x.opnd1;
+  count <- read szOp2 x.opnd2;
+
+  #count-mask <- const
+  #   (case sz of
+  #       8: 31
+  #     | 16: 31
+  #     | 32: 31
+  #     | 64: 63
+  #    end);
+  #temp-count <- mktemp;
+  #andb sz temp-count count count-mask;
+ 
+  real-shift-count-size <-
+    case sz of
+       8: return 5
+     | 16: return 5
+     | 32: return 5
+     | 64: return 6
+    end
+  ;
+  temp-count <- mktemp;
+  mov real-shift-count-size temp-count count;
+  mov (sz - real-shift-count-size) (at-offset temp-count real-shift-count-size) (imm 0);
+
+  tdst <- mktemp;
+  cf <- fCF;
+
+  _if (/gtu sz (var temp-count) (imm 0)) _then do
+    shl sz tdst src (var temp-count);
+
+    temp-c <- mktemp;
+    sub sz temp-c (imm sz) (var temp-count);
+    shr sz temp-c src (var temp-c);
+    mov 1 cf (var temp-c)
+  end;
+
+  ov <- fOF;
+  _if (/eq sz (var temp-count) (imm 1)) _then
+    xorb 1 ov (var (at-offset tdst (sz - 1))) (var cf)
+  _else (_if (/neq sz (var temp-count) (imm 0)) _then
+    undef 1 ov)
+  ;
+
+  sf <- fSF;
+  cmplts sz sf (var tdst) (imm 0);
+
+  zf <- fZF;
+  cmpeq sz zf (var tdst) (imm 0);
+
+  emit-parity-flag (var tdst);
+
+  commit sz dst (var tdst)
+
+#  # dst => a, src => b, amount => c
+#  ## Temporary variables:
+#  t1 <- mktemp;
+#  t2 <- mktemp;
+#  cnt <- mktemp;
+#  cntIsZero <- mktemp;
+#  cntIsOne <- mktemp;
+#  af <- fAF;
+#  ov <- fOF;
+#  cf <- fCF;
+#  eq <- fEQ;
+#  mask <- const
+#     (case sz of
+#         8: 31
+#       | 16: 31
+#       | 32: 31
+#       | 64: 63
+#      end);
+#  zer0 <- const 0;
+#  one <- const 1;
+#
+#  ## Instruction semantics:
+#  setflag <- mklabel;
+#  exit <- mklabel;
+#  nop <- mklabel;
+#  convert sz cnt szOp2 c;
+#  andb sz cnt (var cnt) mask;
+#  cmpeq sz cntIsZero (var cnt) zer0;
+#  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;
+#  gotolabel exit;
+#  label setflag;
+#  xorb 1 ov (var cf) (var (t2 /+ (sz - 1)));
+#  label exit;
+#  undef 1 af;
+#  commit sz a (var t2);
+#  label nop;
+#  cmpeq sz eq b zer0
+end
+
+val sem-sar x = do
+  sz <- sizeof1 x.opnd1;
+  szOp2 <- sizeof1 x.opnd2;
+  dst <- write sz x.opnd1;
+  src <- read sz x.opnd1;
+  count <- read szOp2 x.opnd2;
+
+  #count-mask <- const
+  #   (case sz of
+  #       8: 31
+  #     | 16: 31
+  #     | 32: 31
+  #     | 64: 63
+  #    end);
+  #temp-count <- mktemp;
+  #andb sz temp-count count count-mask;
+ 
+  real-shift-count-size <-
+    case sz of
+       8: return 5
+     | 16: return 5
+     | 32: return 5
+     | 64: return 6
+    end
+  ;
+  temp-count <- mktemp;
+  mov real-shift-count-size temp-count count;
+  mov (sz - real-shift-count-size) (at-offset temp-count real-shift-count-size) (imm 0);
+
+  tdst <- mktemp;
+  cf <- fCF;
+
+  _if (/gtu sz (var temp-count) (imm 0)) _then do
+    sub sz temp-count (var temp-count) (imm 1);
+    shrs sz tdst src (var temp-count);
+
+    mov 1 cf (var tdst);
+
+    shrs sz tdst (var tdst) (imm 1)
+  end;
+ 
+  ov <- fOF;
+  _if (/eq sz (var temp-count) (imm 1)) _then
+    mov 1 ov (imm 0)
+  _else (_if (/neq sz (var temp-count) (imm 0)) _then
+    undef 1 ov)
+  ;
+
+  sf <- fSF;
+  cmplts sz sf (var tdst) (imm 0);
+
+  zf <- fZF;
+  cmpeq sz zf (var tdst) (imm 0);
+
+  emit-parity-flag (var tdst);
+
+  commit sz dst (var tdst)
+end
+
+val sem-sbb x = do
+  sz <- sizeof2 x.opnd1 x.opnd2;
+  difference <- write sz x.opnd1;
+  minuend <- read sz x.opnd1;
+  subtrahend <- read sz x.opnd2;
+
+  t <- mktemp;
+  cf <- fCF;
+  movzx sz t 1 (var cf);
+  add sz t (var t) subtrahend;
+  sub sz t minuend subtrahend;
+
+  emit-sub-sbb-flags sz (var t) minuend subtrahend (var cf) '1';
+  commit sz difference (var t)
+end
+
+val sem-setcc x cond = do
+  dst-sz <- sizeof1 x.opnd1;
+  dst <- write dst-sz x.opnd1;
+
+  cond <- cond;
+  temp <- mktemp;
+  movzx dst-sz temp 1 cond;
+
+  commit dst-sz dst (var temp)
+end
+
+val sem-scas size x = let
+  val sem x = do
+    mem-sem <- return (semantic-register-of (register-by-size low DI_ x.addr-sz));
+
+    mem-val <- mktemp;
+    segmented-load size mem-val x.addr-sz (var mem-sem) (SEG_OVERRIDE ES);
+
+    a <- return (semantic-register-of (register-by-size low A size));
+
+    temp <- mktemp;
+    sub size temp (var a) (var mem-val);
+
+    emit-sub-sbb-flags size (var temp) (var a) (var mem-val) (imm 0) '1';
+
+    direction-adjust mem-sem.size mem-sem size
+  end
+in
+  sem-repe-repne-insn x sem
+end
+
+val sem-shr x = do
+  sz <- sizeof1 x.opnd1;
+  szOp2 <- sizeof1 x.opnd2;
+  dst <- write sz x.opnd1;
+  src <- read sz x.opnd1;
+  count <- read szOp2 x.opnd2;
+
+  #count-mask <- const
+  #   (case sz of
+  #       8: 31
+  #     | 16: 31
+  #     | 32: 31
+  #     | 64: 63
+  #    end);
+  #temp-count <- mktemp;
+  #andb sz temp-count count count-mask;
+
+  real-shift-count-size <-
+    case sz of
+       8: return 5
+     | 16: return 5
+     | 32: return 5
+     | 64: return 6
+    end
+  ;
+  temp-count <- mktemp;
+  mov real-shift-count-size temp-count count;
+  mov (sz - real-shift-count-size) (at-offset temp-count real-shift-count-size) (imm 0);
+
+  tdst <- mktemp;
+  cf <- fCF;
+
+  _if (/gtu sz (var temp-count) (imm 0)) _then do
+    sub sz temp-count (var temp-count) (imm 1);
+    shr sz tdst src (var temp-count);
+
+    mov 1 cf (var tdst);
+
+    shr sz tdst (var tdst) (imm 1)
+  end;
+ 
+  ov <- fOF;
+  _if (/eq sz (var temp-count) (imm 1)) _then do
+    t <- mktemp;
+    mov sz t src;
+    mov 1 ov (var (at-offset t (sz - 1)))
+  end _else (_if (/neq sz (var temp-count) (imm 0)) _then
+    undef 1 ov)
+  ;
+
+  sf <- fSF;
+  cmplts sz sf (var tdst) (imm 0);
+
+  zf <- fZF;
+  cmpeq sz zf (var tdst) (imm 0);
+
+  emit-parity-flag (var tdst);
+
+  commit sz dst (var tdst)
+end
+
+val sem-stc = do
+  cf <- fCF;
+  mov 1 cf (imm 1)
+end
+
+val sem-std = do
+  df <- fDF;
+  mov 1 df (imm 1)
+end
+
+val sem-stos size x = let
+  val sem x = do
+    mem-sem <- return (semantic-register-of (register-by-size low DI_ x.addr-sz));
+    a <- return (semantic-register-of (register-by-size low A size));
+
+    segmented-store (address x.addr-sz (var mem-sem)) (lin a.size (var a)) (SEG_OVERRIDE ES);
+
+    direction-adjust mem-sem.size mem-sem size
+  end
+in
+  sem-rep-insn x sem
+end
+
+val sem-sub x = do
+  sz <- sizeof2 x.opnd1 x.opnd2;
+  difference <- write sz x.opnd1;
+  minuend <- read sz x.opnd1;
+  subtrahend <- read sz x.opnd2;
+
+  t <- mktemp;
+  sub sz t minuend subtrahend;
+
+  emit-sub-sbb-flags sz (var t) minuend subtrahend (imm 0) '1';
+  commit sz difference (var t)
+end
+
+## T>>
+
+val sem-test x = do
+  sz <- sizeof2 x.opnd1 x.opnd2;
+  a <- read sz x.opnd1;
+  b <- read sz x.opnd2;
+  
+  temp <- mktemp;
+  andb sz temp a b;
+
+  sf <- fSF;
+  cmplts sz sf (var temp) (imm 0);
+
+  zf <- fZF;
+  cmpeq sz zf (var temp) (imm 0);
+  
+  emit-parity-flag (var temp);
+
+  cf <- fCF;
+  mov 1 cf (imm 0);
+  
+  ov <- fOF;
+  mov 1 ov (imm 0);
+
+  af <- fAF;
+  undef 1 af
+end
+
+## U>>
+## V>>
+## W>>
+## X>>
+
+val sem-xadd x = do
+  size <- sizeof1 x.opnd1;
+  src0 <- read size x.opnd1;
+  src1 <- read size x.opnd2;
+  dst0 <- write size x.opnd1;
+  dst1 <- write size x.opnd2;
+
+  sum <- mktemp;
+  add size sum src0 src1;
+
+  emit-add-adc-flags size (var sum) src0 src1 (imm 0) '1';
+
+  commit size dst0 (var sum);
+  commit size dst1 src0
+end
+
+val sem-xchg x = do
+  sz <- sizeof1 x.opnd1;
+  a-r <- read sz x.opnd1;
+  b-r <- read sz x.opnd2;
+  a-w <- write sz x.opnd1;
+  b-w <- write sz x.opnd2;
+
+  temp <- mktemp;
+  
+  mov sz temp a-r;
+  commit sz a-w b-r;
+  commit sz b-w (var temp)
+end
+
+val sem-xor x = do
+  sz <- sizeof2 x.opnd1 x.opnd2;
+  dst <- write sz x.opnd1;
+  src0 <- read sz x.opnd1;
+  src1 <- read sz x.opnd2;
+
+  temp <- mktemp;
+  xorb sz temp src0 src1;
+
+  sf <- fSF;
+  cmplts sz sf (var temp) (imm 0);
+
+  zf <- fZF;
+  cmpeq sz zf (var temp) (imm 0);
+  
+  emit-parity-flag (var temp);
+
+  cf <- fCF;
+  mov 1 cf (imm 0);
+  
+  ov <- fOF;
+  mov 1 ov (imm 0);
+
+  af <- fAF;
+  undef 1 af;
+
+  commit sz dst (var temp)
+end
+
+## Y>>
+## Z>>
diff --git a/specifications/x86/x86-rreil-translator.ml b/specifications/x86/x86-rreil-translator.ml
index 9e500da6b6cb643f4f76a35f72fcf2d757ad1cb5..d6bb78719d1fd3b0332857112c6aed0ccb5417c1 100644
--- a/specifications/x86/x86-rreil-translator.ml
+++ b/specifications/x86/x86-rreil-translator.ml
@@ -682,1516 +682,6 @@ val direction-adjust reg-size reg-sem for-size = do
     sub reg-size reg-sem (var reg-sem) (imm amount)
 end
 
-## 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
-
-## I>>
-
-val sem-idiv x = sem-div Signed x
-
-val sem-imul-1 x = sem-mul Signed x
-val sem-imul-2-3 op1 op2 op3 = do
-  sz <- sizeof1 op1;
-
-  factor0 <- reads Signed (sz + sz) op2;
-  factor1 <- reads Signed (sz + sz) op3;
-
-  product <- mktemp;
-  mul (sz + sz) product factor0 factor1;
-
-  emit-mul-flags sz product;
-
-  result <- write sz op1;
-  commit sz result (var product)
-end
-val sem-imul-2 x = sem-imul-2-3 x.opnd1 x.opnd1 x.opnd2
-val sem-imul-3 x = sem-imul-2-3 x.opnd1 x.opnd2 x.opnd3
-
-val sem-inc x = do
-  sz <- sizeof1 x.opnd1;
-  src <- read sz x.opnd1;
-  dst <- write sz x.opnd1;
-
-  temp <- mktemp;
-  add 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-invd = return void
-
-## J>>
-
-val sem-jcc x cond = do
-  ip-sz <-
-    if (x.opnd-sz === 64) then
-      return 64
-    else
-      return 32
-  ;
-  ip <- ip-get;
-
-  target <- read-flow ip-sz x.opnd1;
-
-  temp-ip <- mktemp;
-  add ip-sz temp-ip target ip;
-
-  cond <- cond;
-  cbranch cond (address ip-sz (var temp-ip)) (address ip-sz ip)
-end
-
-val sem-jregz x reg = do
-  reg-sem <- return (semantic-register-of reg);
-  sem-jcc x (/eq reg-sem.size (var reg-sem) (imm 0))
-end
-
-val sem-jcxz x = sem-jregz x CX
-val sem-jecxz x = sem-jregz x ECX
-val sem-jrcxz x = sem-jregz x RCX
-
-val sem-jmp x = do
-  mode64 <- mode64?;
-  ip-sz <-
-    if mode64 then
-      return 64
-    else
-      return 32
-  ;
-  temp-ip <- mktemp;
-
-  if (near x.opnd1) then do
-    target <- read-flow ip-sz x.opnd1;
-    if (relative x.opnd1) then do
-      ip <- ip-get;
-      add ip-sz temp-ip ip target
-    end else
-      mov ip-sz temp-ip target
-    ;
-    if (x.opnd-sz === 16) then
-      #andb ip-sz temp-ip (var temp-ip) (imm 0xffff)
-      mov (ip-sz - x.opnd-sz) (at-offset temp-ip x.opnd-sz) (imm 0)
-    else
-      return void
-    end
-  else if (not mode64) then do
-    target-sz <- sizeof-flow x.opnd1;
-    target <- read-flow target-sz x.opnd1;
-    movzx ip-sz temp-ip x.opnd-sz target;
-    #if (opnd-sz === 16) then
-    #  #andb ip-sz temp-ip (var temp-ip) (imm 0xffff)
-    #  mov (ip-sz - opnd-sz) (at-offset temp-ip x.opnd-sz) (imm 0)
-    #else
-    #  return void
-    #;
-    reg <- return CS;
-    reg-sem <- return (semantic-register-of reg);
-    reg-size <- sizeof1 (REG reg);
-    temp-target <- mktemp;
-    mov target-sz temp-target target;
-    mov reg-size reg-sem (var (at-offset temp-target x.opnd-sz))
-  end else
-    return void
-  ;
-
-  jump (address ip-sz (var temp-ip))
-end
-
-## K>>
-## L>>
-
-val sem-lahf = do
-  ah <- return (semantic-register-of AH);
-  flags <- rflags;
-
-  mov ah.size ah (var flags)
-end
-
-val sem-lar x = do
-  sem-undef-arity2
-end
-
-val sem-lea x = do
-  opnd-sz <- sizeof1 x.opnd1;
-  dst <- write opnd-sz x.opnd1;
-  src <-
-    case x.opnd2 of
-      MEM m: return m
-    end
-  ;
-  addr-sz <- return src.psz;
-  address <- conv-with Signed src.psz src.opnd;
-
-  temp <- mktemp;
-  movzx opnd-sz temp addr-sz address;
-
-  commit opnd-sz dst (var temp)
-end
-
-val sem-lods x = do
-  sz <- sizeof1 x.opnd1;
-  src <- read sz x.opnd1;
-
-  dst <- return (semantic-register-of (register-by-size low A sz));
-
-  mov dst.size dst src
-end
-
-val sem-loop-loop x = do
-  reg <- return (semantic-register-of (
-    case x.addr-sz of
-       32: ECX
-     | 64: RCX
-     | _: CX
-    end
-  ));
-
-  sub reg.size reg (var reg) (imm 1);
-
-  return reg
-end
-
-val sem-loop x = do
-  reg <- sem-loop-loop x;
-  sem-jcc x (/neq reg.size (var reg) (imm 0))
-end
-
-val sem-loope x = do
-  reg <- sem-loop-loop x;
-  zf <- fZF;
-  sem-jcc x (/and (/d (var zf)) (/neq reg.size (var reg) (imm 0)))
-end
-
-val sem-loopne x = do
-  reg <- sem-loop-loop x;
-  zf <- fZF;
-  sem-jcc x (/and (/not (var zf)) (/neq reg.size (var reg) (imm 0)))
-end
-
-## M>>
-
-val sem-mov x = do
-  sz <- sizeof2 x.opnd1 x.opnd2;
-  a <- write sz x.opnd1;
-  b <- read sz x.opnd2;
-  commit sz a b
-end
-
-val sem-movap x = do
-  sz <- sizeof1 x.opnd1;
-  dst <- write sz x.opnd1;
-  src <- read sz x.opnd2;
-
-  temp <- mktemp;
-  mov sz temp src;
-
-  commit sz dst (var temp)
-end
-
-val sem-vmovap x = do
-  x <- case x of VA2 x: return x end;
-
-  sz <- sizeof1 x.opnd1;
-  dst <- write sz x.opnd1;
-  src <- read sz x.opnd2;
-
-  if sz === 128 then
-    do
-      dst-upper <- write-upper sz x.opnd1;
-      commit sz dst-upper (imm 0)
-    end
-  else
-    return void
-  ;
-
-  temp <- mktemp;
-  mov sz temp src;
-  commit sz dst (var temp)
-end
-
-val sem-movs x = do
-  sz <- sizeof1 x.opnd1;
-  src <- read sz x.opnd2;
-  dst <- write sz x.opnd1;
-  commit sz dst src
-end
-
-val sem-movsx x = do
-  sz-dst <- sizeof1 x.opnd1;
-  sz-src <- sizeof1 x.opnd2;
-  dst <- write sz-dst x.opnd1;
-  src <- read sz-src x.opnd2;
-
-  temp <- mktemp;
-  movsx sz-dst temp sz-src src;
-
-  commit sz-dst dst (var temp)
-end
-
-val sem-movzx x = do
-  sz-dst <- sizeof1 x.opnd1;
-  sz-src <- sizeof1 x.opnd2;
-  dst <- write sz-dst x.opnd1;
-  src <- read sz-src x.opnd2;
-
-  temp <- mktemp;
-  movzx sz-dst temp sz-src src;
-
-  commit sz-dst dst (var temp)
-end
-
-val sem-mul conv x = do
-  sz <- sizeof1 x.opnd1;
-
-  factor0-sem <- return (semantic-register-of (register-by-size low A sz));
-  factor0 <- expand conv (var factor0-sem) sz (sz + sz);
-
-  factor1 <- reads conv (sz + sz) x.opnd1;
-
-  product <- mktemp;
-  mul (sz + sz) product factor0 factor1;
-
-  emit-mul-flags sz product;
-
-  case sz of
-     8: do
-       ax <- return (semantic-register-of AX);
-       mov sz ax (var product)
-     end
-   | _: do
-       high <- return (semantic-register-of (register-by-size low D sz));
-       low <- return (semantic-register-of (register-by-size low A sz));
-
-       mov sz high (var (at-offset product sz));
-       mov sz low (var product)
-   end
-  end
-end
-
-## N>>
-
-val sem-nop x = do
-  return void
-end
-
-## O>>
-
-val sem-or x = do
-  sz <- sizeof2 x.opnd1 x.opnd2;
-  dst <- write sz x.opnd1;
-  src0 <- read sz x.opnd1;
-  src1 <- read sz x.opnd2;
-  temp <- mktemp;
-  orb sz temp src0 src1;
-
-  ov <- fOF;
-  mov 1 ov (imm 0);
-  cf <- fCF;
-  mov 1 cf (imm 0);
-  sf <- fSF;
-  cmplts sz sf (var temp) (imm 0);
-  zf <- fZF;
-  cmpeq sz zf (var temp) (imm 0);
-  emit-parity-flag (var temp);
-  af <- fAF;
-  undef 1 af;
-
-  commit sz dst (var temp)
-end
-
-## P>>
-
-val ps-pop opnd-sz opnd = do
-  stack-addr-sz <- runtime-stack-address-size;
-
-  sp-reg <-
-    if stack-addr-sz === 32 then
-      return ESP
-    else if stack-addr-sz === 64 then
-      return RSP
-    else
-      return SP
-  ;
-  
-  sp <- return (semantic-register-of sp-reg);
-  sp-size <- sizeof1 (REG sp-reg);
-
-  segmented-load opnd-sz opnd stack-addr-sz (var sp) (SEG_OVERRIDE SS);
-
-  if stack-addr-sz === 32 then
-    if opnd-sz === 32 then
-      add sp-size sp (var sp) (imm 4)
-    else
-      add sp-size sp (var sp) (imm 2)
-  else if stack-addr-sz === 64 then
-    if opnd-sz === 64 then
-      add sp-size sp (var sp) (imm 8)
-    else
-      add sp-size sp (var sp) (imm 2)
-  else
-    if opnd-sz === 16 then
-      add sp-size sp (var sp) (imm 2)
-    else
-      add sp-size sp (var sp) (imm 4)
-
-  #Todo: Special actions in protected mode
-end
-
-val sem-pop x = do
-  dst <- write x.opnd-sz x.opnd1;
-  temp-dest <- mktemp;
-  ps-pop x.opnd-sz temp-dest;
-  commit x.opnd-sz dst (var temp-dest)
-end
-
-val sem-popf x = do
-  popped <- mktemp;
-  ps-pop x.opnd-sz popped;
-
-  move-to-rflags x.opnd-sz (var popped)
-end
-
-val ps-push opnd-sz opnd = do
-  mode64 <- mode64?;
-  stack-addr-sz <- runtime-stack-address-size;
-  
-  sp-reg <-
-    if mode64 then
-      return RSP
-    else if stack-addr-sz === 32 then
-      return ESP
-    else
-      return SP
-  ;
-  sp <- return (semantic-register-of sp-reg);
-
-  if mode64 then
-    if opnd-sz === 64 then
-      sub sp.size sp (var sp) (imm 8)
-    else
-      sub sp.size sp (var sp) (imm 2)
-  else
-    if opnd-sz === 32 then
-      sub sp.size sp (var sp) (imm 4)
-    else
-      sub sp.size sp (var sp) (imm 2)
-  ;
-
-  segmented-store (address sp.size (var sp)) (lin opnd-sz opnd) (SEG_OVERRIDE SS)
-
-  #store (address sp.size (segment-add (var sp) segment)) (lin opnd-sz opnd)
-end
-
-val sem-push x = do
-  src-size <- sizeof1 x.opnd1;
-  src <- read src-size x.opnd1;
-
-  temp <- mktemp;
-  case x.opnd1 of
-     REG r: 
-       if segment-register? r then
-         movzx x.opnd-sz temp src-size src
-       else
-         mov x.opnd-sz temp src
-   | MEM m:
-       mov x.opnd-sz temp src
-   | IMM8 i:
-       movsx x.opnd-sz temp src-size src
-   | IMM16 i:
-       mov x.opnd-sz temp src
-   | IMM32 i:
-       movsx x.opnd-sz temp src-size src
-  end;
-
-  ps-push x.opnd-sz (var temp)
-end
-
-val sem-pushf x = do
-  mask <- return 0x0000000000fcffff;
-  flags <- rflags;
-
-  temp <- mktemp;
-  andb flags.size temp (var flags) (imm mask);
-
-  ps-push x.opnd-sz (var temp)
-end
-
-## Q>>
-## R>>
-
-val sem-rep-repe-repne size sem fc = do
-  count-reg <- return (semantic-register-of (register-by-size low DI_ size));
-
-  cond-creg <- let
-    val v = /neq size (var count-reg) (imm 0)
-  in
-    return v
-  end;
-
-  cond <- mktemp;
-  c <- cond-creg;
-  mov 1 cond c;
-  _while (/d (var cond)) __ do
-    sem;
-
-    c <- /and cond-creg fc;
-    mov 1 cond c
-  end
-end
-
-val sem-rep size sem = sem-rep-repe-repne size sem (return (imm 1))
-
-val sem-repe size sem = let
-  val fc = do
-    zf <- fZF;
-    /not (var zf)
-  end
-in
-  sem-rep-repe-repne size sem fc
-end
-
-val sem-repne size sem = let
-  val fc = do
-    zf <- fZF;
-    /d (var zf)
-  end
-in
-  sem-rep-repe-repne size sem fc
-end
-
-val sem-repe-repne-insn x sem =
-  if x.rep then
-    sem-repe x.addr-sz (sem x)
-  else if x.repne then
-    sem-repne x.addr-sz (sem x)
-  else
-     sem x
-
-val sem-rep-insn x sem =
-  if x.rep then
-    sem-rep x.addr-sz (sem x)
-  else
-     sem x
-
-val sem-ret x =
-  case x of
-     VA0 x: sem-ret-without-operand x
-   | VA1 x:
-       do
-         release-from-stack x;
-	 sem-ret-without-operand x
-       end
-  end
-
-val sem-ret-far x =
-  case x of
-     VA0 x: sem-ret-far-without-operand x
-   | VA1 x:
-       do
-         release-from-stack x;
-         sem-ret-far-without-operand x
-       end
-  end
-
-val pop-ip opnd-sz = do
-  ip-sz <-
-    if (opnd-sz === 64) then
-      return 64
-    else
-      return 32
-  ;
-
-  temp-ip <- mktemp;
-  ps-pop ip-sz temp-ip;
-  mov (ip-sz - opnd-sz) (at-offset temp-ip opnd-sz) (imm 0);
-
-  return (address opnd-sz (var temp-ip))
-end
-
-val sem-ret-without-operand x = do
-  address <- pop-ip x.opnd-sz;
-  ret address
-end
-
-val sem-ret-far-without-operand x = do
-  address <- pop-ip x.opnd-sz;
-
-  temp-cs <- mktemp;
-  ps-pop x.opnd-sz temp-cs;
-  
-  sec-reg <- return CS;
-  sec-reg-sem <- return (semantic-register-of sec-reg);
-  reg-size <- sizeof1 (REG sec-reg);
-
-  mov reg-size sec-reg-sem (var temp-cs);
-
-  ret address
-end
-
-val release-from-stack x = do
-  x-sz <- sizeof1 x.opnd1;
-  src <- read x-sz x.opnd1;
-
-  stack-addr-sz <- runtime-stack-address-size;
-
-  sp-reg <-
-    if stack-addr-sz === 32 then
-      return ESP
-    else if stack-addr-sz === 64 then
-      return RSP
-    else
-      return SP
-  ;
-
-  sp <- return (semantic-register-of sp-reg);
-  sp-size <- sizeof1 (REG sp-reg);
-
-  src-ext <- mktemp;
-  movzx sp-size src-ext x-sz src;
-
-  add sp-size sp (var sp) (var src-ext)
-end
-
-## S>>
-
-val sem-sahf x = do
-  ah <- return (semantic-register-of AH);
-  flags <- rflags;
-
-  move-to-rflags ah.size (var ah)
-end
-
-val sem-sal-shl x = do
-  sz <- sizeof1 x.opnd1;
-  szOp2 <- sizeof1 x.opnd2;
-  dst <- write sz x.opnd1;
-  src <- read sz x.opnd1;
-  count <- read szOp2 x.opnd2;
-
-  #count-mask <- const
-  #   (case sz of
-  #       8: 31
-  #     | 16: 31
-  #     | 32: 31
-  #     | 64: 63
-  #    end);
-  #temp-count <- mktemp;
-  #andb sz temp-count count count-mask;
- 
-  real-shift-count-size <-
-    case sz of
-       8: return 5
-     | 16: return 5
-     | 32: return 5
-     | 64: return 6
-    end
-  ;
-  temp-count <- mktemp;
-  mov real-shift-count-size temp-count count;
-  mov (sz - real-shift-count-size) (at-offset temp-count real-shift-count-size) (imm 0);
-
-  tdst <- mktemp;
-  cf <- fCF;
-
-  _if (/gtu sz (var temp-count) (imm 0)) _then do
-    shl sz tdst src (var temp-count);
-
-    temp-c <- mktemp;
-    sub sz temp-c (imm sz) (var temp-count);
-    shr sz temp-c src (var temp-c);
-    mov 1 cf (var temp-c)
-  end;
-
-  ov <- fOF;
-  _if (/eq sz (var temp-count) (imm 1)) _then
-    xorb 1 ov (var (at-offset tdst (sz - 1))) (var cf)
-  _else (_if (/neq sz (var temp-count) (imm 0)) _then
-    undef 1 ov)
-  ;
-
-  sf <- fSF;
-  cmplts sz sf (var tdst) (imm 0);
-
-  zf <- fZF;
-  cmpeq sz zf (var tdst) (imm 0);
-
-  emit-parity-flag (var tdst);
-
-  commit sz dst (var tdst)
-
-#  # dst => a, src => b, amount => c
-#  ## Temporary variables:
-#  t1 <- mktemp;
-#  t2 <- mktemp;
-#  cnt <- mktemp;
-#  cntIsZero <- mktemp;
-#  cntIsOne <- mktemp;
-#  af <- fAF;
-#  ov <- fOF;
-#  cf <- fCF;
-#  eq <- fEQ;
-#  mask <- const
-#     (case sz of
-#         8: 31
-#       | 16: 31
-#       | 32: 31
-#       | 64: 63
-#      end);
-#  zer0 <- const 0;
-#  one <- const 1;
-#
-#  ## Instruction semantics:
-#  setflag <- mklabel;
-#  exit <- mklabel;
-#  nop <- mklabel;
-#  convert sz cnt szOp2 c;
-#  andb sz cnt (var cnt) mask;
-#  cmpeq sz cntIsZero (var cnt) zer0;
-#  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;
-#  gotolabel exit;
-#  label setflag;
-#  xorb 1 ov (var cf) (var (t2 /+ (sz - 1)));
-#  label exit;
-#  undef 1 af;
-#  commit sz a (var t2);
-#  label nop;
-#  cmpeq sz eq b zer0
-end
-
-val sem-sar x = do
-  sz <- sizeof1 x.opnd1;
-  szOp2 <- sizeof1 x.opnd2;
-  dst <- write sz x.opnd1;
-  src <- read sz x.opnd1;
-  count <- read szOp2 x.opnd2;
-
-  #count-mask <- const
-  #   (case sz of
-  #       8: 31
-  #     | 16: 31
-  #     | 32: 31
-  #     | 64: 63
-  #    end);
-  #temp-count <- mktemp;
-  #andb sz temp-count count count-mask;
- 
-  real-shift-count-size <-
-    case sz of
-       8: return 5
-     | 16: return 5
-     | 32: return 5
-     | 64: return 6
-    end
-  ;
-  temp-count <- mktemp;
-  mov real-shift-count-size temp-count count;
-  mov (sz - real-shift-count-size) (at-offset temp-count real-shift-count-size) (imm 0);
-
-  tdst <- mktemp;
-  cf <- fCF;
-
-  _if (/gtu sz (var temp-count) (imm 0)) _then do
-    sub sz temp-count (var temp-count) (imm 1);
-    shrs sz tdst src (var temp-count);
-
-    mov 1 cf (var tdst);
-
-    shrs sz tdst (var tdst) (imm 1)
-  end;
- 
-  ov <- fOF;
-  _if (/eq sz (var temp-count) (imm 1)) _then
-    mov 1 ov (imm 0)
-  _else (_if (/neq sz (var temp-count) (imm 0)) _then
-    undef 1 ov)
-  ;
-
-  sf <- fSF;
-  cmplts sz sf (var tdst) (imm 0);
-
-  zf <- fZF;
-  cmpeq sz zf (var tdst) (imm 0);
-
-  emit-parity-flag (var tdst);
-
-  commit sz dst (var tdst)
-end
-
-val sem-sbb x = do
-  sz <- sizeof2 x.opnd1 x.opnd2;
-  difference <- write sz x.opnd1;
-  minuend <- read sz x.opnd1;
-  subtrahend <- read sz x.opnd2;
-
-  t <- mktemp;
-  cf <- fCF;
-  movzx sz t 1 (var cf);
-  add sz t (var t) subtrahend;
-  sub sz t minuend subtrahend;
-
-  emit-sub-sbb-flags sz (var t) minuend subtrahend (var cf) '1';
-  commit sz difference (var t)
-end
-
-val sem-setcc x cond = do
-  dst-sz <- sizeof1 x.opnd1;
-  dst <- write dst-sz x.opnd1;
-
-  cond <- cond;
-  temp <- mktemp;
-  movzx dst-sz temp 1 cond;
-
-  commit dst-sz dst (var temp)
-end
-
-val sem-scas size x = let
-  val sem x = do
-    mem-sem <- return (semantic-register-of (register-by-size low DI_ x.addr-sz));
-
-    mem-val <- mktemp;
-    segmented-load size mem-val x.addr-sz (var mem-sem) (SEG_OVERRIDE ES);
-
-    a <- return (semantic-register-of (register-by-size low A size));
-
-    temp <- mktemp;
-    sub size temp (var a) (var mem-val);
-
-    emit-sub-sbb-flags size (var temp) (var a) (var mem-val) (imm 0) '1';
-
-    direction-adjust mem-sem.size mem-sem size
-  end
-in
-  sem-repe-repne-insn x sem
-end
-
-val sem-shr x = do
-  sz <- sizeof1 x.opnd1;
-  szOp2 <- sizeof1 x.opnd2;
-  dst <- write sz x.opnd1;
-  src <- read sz x.opnd1;
-  count <- read szOp2 x.opnd2;
-
-  #count-mask <- const
-  #   (case sz of
-  #       8: 31
-  #     | 16: 31
-  #     | 32: 31
-  #     | 64: 63
-  #    end);
-  #temp-count <- mktemp;
-  #andb sz temp-count count count-mask;
-
-  real-shift-count-size <-
-    case sz of
-       8: return 5
-     | 16: return 5
-     | 32: return 5
-     | 64: return 6
-    end
-  ;
-  temp-count <- mktemp;
-  mov real-shift-count-size temp-count count;
-  mov (sz - real-shift-count-size) (at-offset temp-count real-shift-count-size) (imm 0);
-
-  tdst <- mktemp;
-  cf <- fCF;
-
-  _if (/gtu sz (var temp-count) (imm 0)) _then do
-    sub sz temp-count (var temp-count) (imm 1);
-    shr sz tdst src (var temp-count);
-
-    mov 1 cf (var tdst);
-
-    shr sz tdst (var tdst) (imm 1)
-  end;
- 
-  ov <- fOF;
-  _if (/eq sz (var temp-count) (imm 1)) _then do
-    t <- mktemp;
-    mov sz t src;
-    mov 1 ov (var (at-offset t (sz - 1)))
-  end _else (_if (/neq sz (var temp-count) (imm 0)) _then
-    undef 1 ov)
-  ;
-
-  sf <- fSF;
-  cmplts sz sf (var tdst) (imm 0);
-
-  zf <- fZF;
-  cmpeq sz zf (var tdst) (imm 0);
-
-  emit-parity-flag (var tdst);
-
-  commit sz dst (var tdst)
-end
-
-val sem-stc = do
-  cf <- fCF;
-  mov 1 cf (imm 1)
-end
-
-val sem-std = do
-  df <- fDF;
-  mov 1 df (imm 1)
-end
-
-val sem-stos size x = let
-  val sem x = do
-    mem-sem <- return (semantic-register-of (register-by-size low DI_ x.addr-sz));
-    a <- return (semantic-register-of (register-by-size low A size));
-
-    segmented-store (address x.addr-sz (var mem-sem)) (lin a.size (var a)) (SEG_OVERRIDE ES);
-
-    direction-adjust mem-sem.size mem-sem size
-  end
-in
-  sem-rep-insn x sem
-end
-
-val sem-sub x = do
-  sz <- sizeof2 x.opnd1 x.opnd2;
-  difference <- write sz x.opnd1;
-  minuend <- read sz x.opnd1;
-  subtrahend <- read sz x.opnd2;
-
-  t <- mktemp;
-  sub sz t minuend subtrahend;
-
-  emit-sub-sbb-flags sz (var t) minuend subtrahend (imm 0) '1';
-  commit sz difference (var t)
-end
-
-## T>>
-
-val sem-test x = do
-  sz <- sizeof2 x.opnd1 x.opnd2;
-  a <- read sz x.opnd1;
-  b <- read sz x.opnd2;
-  
-  temp <- mktemp;
-  andb sz temp a b;
-
-  sf <- fSF;
-  cmplts sz sf (var temp) (imm 0);
-
-  zf <- fZF;
-  cmpeq sz zf (var temp) (imm 0);
-  
-  emit-parity-flag (var temp);
-
-  cf <- fCF;
-  mov 1 cf (imm 0);
-  
-  ov <- fOF;
-  mov 1 ov (imm 0);
-
-  af <- fAF;
-  undef 1 af
-end
-
-## U>>
-## V>>
-## W>>
-## X>>
-
-val sem-xadd x = do
-  size <- sizeof1 x.opnd1;
-  src0 <- read size x.opnd1;
-  src1 <- read size x.opnd2;
-  dst0 <- write size x.opnd1;
-  dst1 <- write size x.opnd2;
-
-  sum <- mktemp;
-  add size sum src0 src1;
-
-  emit-add-adc-flags size (var sum) src0 src1 (imm 0) '1';
-
-  commit size dst0 (var sum);
-  commit size dst1 src0
-end
-
-val sem-xchg x = do
-  sz <- sizeof1 x.opnd1;
-  a-r <- read sz x.opnd1;
-  b-r <- read sz x.opnd2;
-  a-w <- write sz x.opnd1;
-  b-w <- write sz x.opnd2;
-
-  temp <- mktemp;
-  
-  mov sz temp a-r;
-  commit sz a-w b-r;
-  commit sz b-w (var temp)
-end
-
-val sem-xor x = do
-  sz <- sizeof2 x.opnd1 x.opnd2;
-  dst <- write sz x.opnd1;
-  src0 <- read sz x.opnd1;
-  src1 <- read sz x.opnd2;
-
-  temp <- mktemp;
-  xorb sz temp src0 src1;
-
-  sf <- fSF;
-  cmplts sz sf (var temp) (imm 0);
-
-  zf <- fZF;
-  cmpeq sz zf (var temp) (imm 0);
-  
-  emit-parity-flag (var temp);
-
-  cf <- fCF;
-  mov 1 cf (imm 0);
-  
-  ov <- fOF;
-  mov 1 ov (imm 0);
-
-  af <- fAF;
-  undef 1 af;
-
-  commit sz dst (var temp)
-end
-
-## Y>>
-## Z>>
-
 val semantics insn =
   case insn of
      AAA x: sem-undef-arity0 x
@@ -2486,7 +976,7 @@ val semantics insn =
    | JZ x: sem-z sem-jcc x
    | LAHF x: sem-lahf
    | LAR x: sem-undef-arity2 x
-   | LDDQU x: sem-undef-arity2 x
+   | LDDQU x: sem-lddqu x
    | LDMXCSR x: sem-undef-arity1 x
    | LDS x: sem-undef-arity2 x
    | LEA x: sem-lea x