(* x64 - generated by L3 - Thu Dec 21 10:59:16 2017 *) structure x64 :> x64 = struct structure Map = MutableMap (* ------------------------------------------------------------------------- Type declarations ------------------------------------------------------------------------- *) datatype Zreg = RAX | RCX | RDX | RBX | RSP | RBP | RSI | RDI | zR8 | zR9 | zR10 | zR11 | zR12 | zR13 | zR14 | zR15 type MXCSR = { DAZ: bool, DE: bool, DM: bool, FZ: bool, IE: bool, IM: bool, OE: bool, OM: bool, PE: bool, PM: bool, RC: BitsN.nbit, Reserved: BitsN.nbit, UE: bool, UM: bool, ZE: bool, ZM: bool } datatype Zeflags = Z_CF | Z_PF | Z_AF | Z_ZF | Z_SF | Z_OF datatype Zsize = Z16 | Z32 | Z64 | Z8 of bool datatype Zbase = ZnoBase | ZregBase of Zreg | ZripBase datatype Zrm = Zm of ((BitsN.nbit * Zreg) option) * (Zbase * BitsN.nbit) | Zr of Zreg datatype Zdest_src = Zr_rm of Zreg * Zrm | Zrm_i of Zrm * BitsN.nbit | Zrm_r of Zrm * Zreg datatype Zimm_rm = Zimm of BitsN.nbit | Zrm of Zrm datatype Zmonop_name = Zdec | Zinc | Znot | Zneg datatype Zbinop_name = Zadd | Zor | Zadc | Zsbb | Zand | Zsub | Zxor | Zcmp | Zrol | Zror | Zrcl | Zrcr | Zshl | Zshr | Ztest | Zsar datatype Zbit_test_name = Zbt | Zbts | Zbtr | Zbtc datatype Zcond = Z_O | Z_NO | Z_B | Z_NB | Z_E | Z_NE | Z_NA | Z_A | Z_S | Z_NS | Z_P | Z_NP | Z_L | Z_NL | Z_NG | Z_G | Z_ALWAYS datatype Zea = Zea_i of Zsize * BitsN.nbit | Zea_m of Zsize * BitsN.nbit | Zea_r of Zsize * Zreg datatype sse_binop = sse_add | sse_sub | sse_mul | sse_div | sse_max | sse_min datatype sse_logic = sse_and | sse_andn | sse_or | sse_xor datatype sse_compare = sse_eq_oq | sse_lt_os | sse_le_os | sse_unord_q | sse_neq_uq | sse_nlt_us | sse_nle_us | sse_ord_q datatype xmm_mem = xmm_mem of ((BitsN.nbit * Zreg) option) * (Zbase * BitsN.nbit) | xmm_reg of BitsN.nbit datatype SSE = CMPPD of sse_compare * (BitsN.nbit * xmm_mem) | CMPPS of sse_compare * (BitsN.nbit * xmm_mem) | CMPSD of sse_compare * (BitsN.nbit * xmm_mem) | CMPSS of sse_compare * (BitsN.nbit * xmm_mem) | COMISD of BitsN.nbit * xmm_mem | COMISS of BitsN.nbit * xmm_mem | CVTDQ2PD of BitsN.nbit * xmm_mem | CVTDQ2PS of BitsN.nbit * xmm_mem | CVTPD2DQ of bool * (BitsN.nbit * xmm_mem) | CVTPD2PS of BitsN.nbit * xmm_mem | CVTPS2DQ of bool * (BitsN.nbit * xmm_mem) | CVTPS2PD of BitsN.nbit * xmm_mem | CVTSD2SI of bool * (bool * (Zreg * xmm_mem)) | CVTSD2SS of BitsN.nbit * xmm_mem | CVTSI2SD of bool * (BitsN.nbit * Zrm) | CVTSI2SS of bool * (BitsN.nbit * Zrm) | CVTSS2SD of BitsN.nbit * xmm_mem | CVTSS2SI of bool * (bool * (Zreg * xmm_mem)) | MOVAP_D_S of bool * (xmm_mem * xmm_mem) | MOVQ of xmm_mem * xmm_mem | MOVSD of xmm_mem * xmm_mem | MOVSS of xmm_mem * xmm_mem | MOVUP_D_S of bool * (xmm_mem * xmm_mem) | MOV_D_Q of bool * (bool * (BitsN.nbit * Zrm)) | PCMPEQQ of BitsN.nbit * xmm_mem | PSLLDQ of BitsN.nbit * BitsN.nbit | PSLLD_imm of BitsN.nbit * BitsN.nbit | PSLLQ_imm of BitsN.nbit * BitsN.nbit | PSLLW_imm of BitsN.nbit * BitsN.nbit | PSRAD_imm of BitsN.nbit * BitsN.nbit | PSRAW_imm of BitsN.nbit * BitsN.nbit | PSRLDQ of BitsN.nbit * BitsN.nbit | PSRLD_imm of BitsN.nbit * BitsN.nbit | PSRLQ_imm of BitsN.nbit * BitsN.nbit | PSRLW_imm of BitsN.nbit * BitsN.nbit | SQRTPD of BitsN.nbit * xmm_mem | SQRTPS of BitsN.nbit * xmm_mem | SQRTSD of BitsN.nbit * xmm_mem | SQRTSS of BitsN.nbit * xmm_mem | bin_PD of sse_binop * (BitsN.nbit * xmm_mem) | bin_PS of sse_binop * (BitsN.nbit * xmm_mem) | bin_SD of sse_binop * (BitsN.nbit * xmm_mem) | bin_SS of sse_binop * (BitsN.nbit * xmm_mem) | logic_PD of sse_logic * (BitsN.nbit * xmm_mem) | logic_PS of sse_logic * (BitsN.nbit * xmm_mem) datatype instruction = SSE of SSE | Zbinop of Zbinop_name * (Zsize * Zdest_src) | Zbit_test of Zbit_test_name * (Zsize * Zdest_src) | Zcall of Zimm_rm | Zclc | Zcmc | Zcmpxchg of Zsize * (Zrm * Zreg) | Zdiv of Zsize * Zrm | Zidiv of Zsize * Zrm | Zimul of Zsize * Zrm | Zimul2 of Zsize * (Zreg * Zrm) | Zimul3 of Zsize * (Zreg * (Zrm * BitsN.nbit)) | Zjcc of Zcond * BitsN.nbit | Zjmp of Zrm | Zlea of Zsize * Zdest_src | Zleave | Zloop of Zcond * BitsN.nbit | Zmonop of Zmonop_name * (Zsize * Zrm) | Zmov of Zcond * (Zsize * Zdest_src) | Zmovsx of Zsize * (Zdest_src * Zsize) | Zmovzx of Zsize * (Zdest_src * Zsize) | Zmul of Zsize * Zrm | Znop of Nat.nat | Zpop of Zrm | Zpush of Zimm_rm | Zret of BitsN.nbit | Zset of Zcond * (bool * Zrm) | Zstc | Zxadd of Zsize * (Zrm * Zreg) | Zxchg of Zsize * (Zrm * Zreg) datatype Zinst = Zdec_fail of string | Zfull_inst of (BitsN.nbit list) * (instruction * ((BitsN.nbit list) option)) type REX = { B: bool, R: bool, W: bool, X: bool } datatype maybe_instruction = FAIL of string | OK of instruction | PENDING of string * instruction | STREAM of BitsN.nbit list (* ------------------------------------------------------------------------- Casting maps (for enumerated types) ------------------------------------------------------------------------- *) structure Cast = struct fun natToZreg x = case Nat.toInt x of 0 => RAX | 1 => RCX | 2 => RDX | 3 => RBX | 4 => RSP | 5 => RBP | 6 => RSI | 7 => RDI | 8 => zR8 | 9 => zR9 | 10 => zR10 | 11 => zR11 | 12 => zR12 | 13 => zR13 | 14 => zR14 | 15 => zR15 | _ => raise Fail "natToZreg" fun natToZeflags x = case Nat.toInt x of 0 => Z_CF | 1 => Z_PF | 2 => Z_AF | 3 => Z_ZF | 4 => Z_SF | 5 => Z_OF | _ => raise Fail "natToZeflags" fun natToZmonop_name x = case Nat.toInt x of 0 => Zdec | 1 => Zinc | 2 => Znot | 3 => Zneg | _ => raise Fail "natToZmonop_name" fun natToZbinop_name x = case Nat.toInt x of 0 => Zadd | 1 => Zor | 2 => Zadc | 3 => Zsbb | 4 => Zand | 5 => Zsub | 6 => Zxor | 7 => Zcmp | 8 => Zrol | 9 => Zror | 10 => Zrcl | 11 => Zrcr | 12 => Zshl | 13 => Zshr | 14 => Ztest | 15 => Zsar | _ => raise Fail "natToZbinop_name" fun natToZbit_test_name x = case Nat.toInt x of 0 => Zbt | 1 => Zbts | 2 => Zbtr | 3 => Zbtc | _ => raise Fail "natToZbit_test_name" fun natToZcond x = case Nat.toInt x of 0 => Z_O | 1 => Z_NO | 2 => Z_B | 3 => Z_NB | 4 => Z_E | 5 => Z_NE | 6 => Z_NA | 7 => Z_A | 8 => Z_S | 9 => Z_NS | 10 => Z_P | 11 => Z_NP | 12 => Z_L | 13 => Z_NL | 14 => Z_NG | 15 => Z_G | 16 => Z_ALWAYS | _ => raise Fail "natToZcond" fun natTosse_binop x = case Nat.toInt x of 0 => sse_add | 1 => sse_sub | 2 => sse_mul | 3 => sse_div | 4 => sse_max | 5 => sse_min | _ => raise Fail "natTosse_binop" fun natTosse_logic x = case Nat.toInt x of 0 => sse_and | 1 => sse_andn | 2 => sse_or | 3 => sse_xor | _ => raise Fail "natTosse_logic" fun natTosse_compare x = case Nat.toInt x of 0 => sse_eq_oq | 1 => sse_lt_os | 2 => sse_le_os | 3 => sse_unord_q | 4 => sse_neq_uq | 5 => sse_nlt_us | 6 => sse_nle_us | 7 => sse_ord_q | _ => raise Fail "natTosse_compare" fun ZregToNat x = case x of RAX => 0 | RCX => 1 | RDX => 2 | RBX => 3 | RSP => 4 | RBP => 5 | RSI => 6 | RDI => 7 | zR8 => 8 | zR9 => 9 | zR10 => 10 | zR11 => 11 | zR12 => 12 | zR13 => 13 | zR14 => 14 | zR15 => 15 fun ZeflagsToNat x = case x of Z_CF => 0 | Z_PF => 1 | Z_AF => 2 | Z_ZF => 3 | Z_SF => 4 | Z_OF => 5 fun Zmonop_nameToNat x = case x of Zdec => 0 | Zinc => 1 | Znot => 2 | Zneg => 3 fun Zbinop_nameToNat x = case x of Zadd => 0 | Zor => 1 | Zadc => 2 | Zsbb => 3 | Zand => 4 | Zsub => 5 | Zxor => 6 | Zcmp => 7 | Zrol => 8 | Zror => 9 | Zrcl => 10 | Zrcr => 11 | Zshl => 12 | Zshr => 13 | Ztest => 14 | Zsar => 15 fun Zbit_test_nameToNat x = case x of Zbt => 0 | Zbts => 1 | Zbtr => 2 | Zbtc => 3 fun ZcondToNat x = case x of Z_O => 0 | Z_NO => 1 | Z_B => 2 | Z_NB => 3 | Z_E => 4 | Z_NE => 5 | Z_NA => 6 | Z_A => 7 | Z_S => 8 | Z_NS => 9 | Z_P => 10 | Z_NP => 11 | Z_L => 12 | Z_NL => 13 | Z_NG => 14 | Z_G => 15 | Z_ALWAYS => 16 fun sse_binopToNat x = case x of sse_add => 0 | sse_sub => 1 | sse_mul => 2 | sse_div => 3 | sse_max => 4 | sse_min => 5 fun sse_logicToNat x = case x of sse_and => 0 | sse_andn => 1 | sse_or => 2 | sse_xor => 3 fun sse_compareToNat x = case x of sse_eq_oq => 0 | sse_lt_os => 1 | sse_le_os => 2 | sse_unord_q => 3 | sse_neq_uq => 4 | sse_nlt_us => 5 | sse_nle_us => 6 | sse_ord_q => 7 fun ZregToString x = case x of RAX => "RAX" | RCX => "RCX" | RDX => "RDX" | RBX => "RBX" | RSP => "RSP" | RBP => "RBP" | RSI => "RSI" | RDI => "RDI" | zR8 => "zR8" | zR9 => "zR9" | zR10 => "zR10" | zR11 => "zR11" | zR12 => "zR12" | zR13 => "zR13" | zR14 => "zR14" | zR15 => "zR15" fun ZeflagsToString x = case x of Z_CF => "Z_CF" | Z_PF => "Z_PF" | Z_AF => "Z_AF" | Z_ZF => "Z_ZF" | Z_SF => "Z_SF" | Z_OF => "Z_OF" fun Zmonop_nameToString x = case x of Zdec => "Zdec" | Zinc => "Zinc" | Znot => "Znot" | Zneg => "Zneg" fun Zbinop_nameToString x = case x of Zadd => "Zadd" | Zor => "Zor" | Zadc => "Zadc" | Zsbb => "Zsbb" | Zand => "Zand" | Zsub => "Zsub" | Zxor => "Zxor" | Zcmp => "Zcmp" | Zrol => "Zrol" | Zror => "Zror" | Zrcl => "Zrcl" | Zrcr => "Zrcr" | Zshl => "Zshl" | Zshr => "Zshr" | Ztest => "Ztest" | Zsar => "Zsar" fun Zbit_test_nameToString x = case x of Zbt => "Zbt" | Zbts => "Zbts" | Zbtr => "Zbtr" | Zbtc => "Zbtc" fun ZcondToString x = case x of Z_O => "Z_O" | Z_NO => "Z_NO" | Z_B => "Z_B" | Z_NB => "Z_NB" | Z_E => "Z_E" | Z_NE => "Z_NE" | Z_NA => "Z_NA" | Z_A => "Z_A" | Z_S => "Z_S" | Z_NS => "Z_NS" | Z_P => "Z_P" | Z_NP => "Z_NP" | Z_L => "Z_L" | Z_NL => "Z_NL" | Z_NG => "Z_NG" | Z_G => "Z_G" | Z_ALWAYS => "Z_ALWAYS" fun sse_binopToString x = case x of sse_add => "sse_add" | sse_sub => "sse_sub" | sse_mul => "sse_mul" | sse_div => "sse_div" | sse_max => "sse_max" | sse_min => "sse_min" fun sse_logicToString x = case x of sse_and => "sse_and" | sse_andn => "sse_andn" | sse_or => "sse_or" | sse_xor => "sse_xor" fun sse_compareToString x = case x of sse_eq_oq => "sse_eq_oq" | sse_lt_os => "sse_lt_os" | sse_le_os => "sse_le_os" | sse_unord_q => "sse_unord_q" | sse_neq_uq => "sse_neq_uq" | sse_nlt_us => "sse_nlt_us" | sse_nle_us => "sse_nle_us" | sse_ord_q => "sse_ord_q" fun stringToZreg x = case x of "RAX" => RAX | "RCX" => RCX | "RDX" => RDX | "RBX" => RBX | "RSP" => RSP | "RBP" => RBP | "RSI" => RSI | "RDI" => RDI | "zR8" => zR8 | "zR9" => zR9 | "zR10" => zR10 | "zR11" => zR11 | "zR12" => zR12 | "zR13" => zR13 | "zR14" => zR14 | "zR15" => zR15 | _ => raise Fail "stringToZreg" fun stringToZeflags x = case x of "Z_CF" => Z_CF | "Z_PF" => Z_PF | "Z_AF" => Z_AF | "Z_ZF" => Z_ZF | "Z_SF" => Z_SF | "Z_OF" => Z_OF | _ => raise Fail "stringToZeflags" fun stringToZmonop_name x = case x of "Zdec" => Zdec | "Zinc" => Zinc | "Znot" => Znot | "Zneg" => Zneg | _ => raise Fail "stringToZmonop_name" fun stringToZbinop_name x = case x of "Zadd" => Zadd | "Zor" => Zor | "Zadc" => Zadc | "Zsbb" => Zsbb | "Zand" => Zand | "Zsub" => Zsub | "Zxor" => Zxor | "Zcmp" => Zcmp | "Zrol" => Zrol | "Zror" => Zror | "Zrcl" => Zrcl | "Zrcr" => Zrcr | "Zshl" => Zshl | "Zshr" => Zshr | "Ztest" => Ztest | "Zsar" => Zsar | _ => raise Fail "stringToZbinop_name" fun stringToZbit_test_name x = case x of "Zbt" => Zbt | "Zbts" => Zbts | "Zbtr" => Zbtr | "Zbtc" => Zbtc | _ => raise Fail "stringToZbit_test_name" fun stringToZcond x = case x of "Z_O" => Z_O | "Z_NO" => Z_NO | "Z_B" => Z_B | "Z_NB" => Z_NB | "Z_E" => Z_E | "Z_NE" => Z_NE | "Z_NA" => Z_NA | "Z_A" => Z_A | "Z_S" => Z_S | "Z_NS" => Z_NS | "Z_P" => Z_P | "Z_NP" => Z_NP | "Z_L" => Z_L | "Z_NL" => Z_NL | "Z_NG" => Z_NG | "Z_G" => Z_G | "Z_ALWAYS" => Z_ALWAYS | _ => raise Fail "stringToZcond" fun stringTosse_binop x = case x of "sse_add" => sse_add | "sse_sub" => sse_sub | "sse_mul" => sse_mul | "sse_div" => sse_div | "sse_max" => sse_max | "sse_min" => sse_min | _ => raise Fail "stringTosse_binop" fun stringTosse_logic x = case x of "sse_and" => sse_and | "sse_andn" => sse_andn | "sse_or" => sse_or | "sse_xor" => sse_xor | _ => raise Fail "stringTosse_logic" fun stringTosse_compare x = case x of "sse_eq_oq" => sse_eq_oq | "sse_lt_os" => sse_lt_os | "sse_le_os" => sse_le_os | "sse_unord_q" => sse_unord_q | "sse_neq_uq" => sse_neq_uq | "sse_nlt_us" => sse_nlt_us | "sse_nle_us" => sse_nle_us | "sse_ord_q" => sse_ord_q | _ => raise Fail "stringTosse_compare" end (* ------------------------------------------------------------------------- Record update functions ------------------------------------------------------------------------- *) fun MXCSR_DAZ_rupd ({DAZ, DE, DM, FZ, IE, IM, OE, OM, PE, PM, RC, Reserved, UE, UM, ZE, ZM}: MXCSR, x') = {DAZ = x', DE = DE, DM = DM, FZ = FZ, IE = IE, IM = IM, OE = OE, OM = OM, PE = PE, PM = PM, RC = RC, Reserved = Reserved, UE = UE, UM = UM, ZE = ZE, ZM = ZM}: MXCSR fun MXCSR_DE_rupd ({DAZ, DE, DM, FZ, IE, IM, OE, OM, PE, PM, RC, Reserved, UE, UM, ZE, ZM}: MXCSR, x') = {DAZ = DAZ, DE = x', DM = DM, FZ = FZ, IE = IE, IM = IM, OE = OE, OM = OM, PE = PE, PM = PM, RC = RC, Reserved = Reserved, UE = UE, UM = UM, ZE = ZE, ZM = ZM}: MXCSR fun MXCSR_DM_rupd ({DAZ, DE, DM, FZ, IE, IM, OE, OM, PE, PM, RC, Reserved, UE, UM, ZE, ZM}: MXCSR, x') = {DAZ = DAZ, DE = DE, DM = x', FZ = FZ, IE = IE, IM = IM, OE = OE, OM = OM, PE = PE, PM = PM, RC = RC, Reserved = Reserved, UE = UE, UM = UM, ZE = ZE, ZM = ZM}: MXCSR fun MXCSR_FZ_rupd ({DAZ, DE, DM, FZ, IE, IM, OE, OM, PE, PM, RC, Reserved, UE, UM, ZE, ZM}: MXCSR, x') = {DAZ = DAZ, DE = DE, DM = DM, FZ = x', IE = IE, IM = IM, OE = OE, OM = OM, PE = PE, PM = PM, RC = RC, Reserved = Reserved, UE = UE, UM = UM, ZE = ZE, ZM = ZM}: MXCSR fun MXCSR_IE_rupd ({DAZ, DE, DM, FZ, IE, IM, OE, OM, PE, PM, RC, Reserved, UE, UM, ZE, ZM}: MXCSR, x') = {DAZ = DAZ, DE = DE, DM = DM, FZ = FZ, IE = x', IM = IM, OE = OE, OM = OM, PE = PE, PM = PM, RC = RC, Reserved = Reserved, UE = UE, UM = UM, ZE = ZE, ZM = ZM}: MXCSR fun MXCSR_IM_rupd ({DAZ, DE, DM, FZ, IE, IM, OE, OM, PE, PM, RC, Reserved, UE, UM, ZE, ZM}: MXCSR, x') = {DAZ = DAZ, DE = DE, DM = DM, FZ = FZ, IE = IE, IM = x', OE = OE, OM = OM, PE = PE, PM = PM, RC = RC, Reserved = Reserved, UE = UE, UM = UM, ZE = ZE, ZM = ZM}: MXCSR fun MXCSR_OE_rupd ({DAZ, DE, DM, FZ, IE, IM, OE, OM, PE, PM, RC, Reserved, UE, UM, ZE, ZM}: MXCSR, x') = {DAZ = DAZ, DE = DE, DM = DM, FZ = FZ, IE = IE, IM = IM, OE = x', OM = OM, PE = PE, PM = PM, RC = RC, Reserved = Reserved, UE = UE, UM = UM, ZE = ZE, ZM = ZM}: MXCSR fun MXCSR_OM_rupd ({DAZ, DE, DM, FZ, IE, IM, OE, OM, PE, PM, RC, Reserved, UE, UM, ZE, ZM}: MXCSR, x') = {DAZ = DAZ, DE = DE, DM = DM, FZ = FZ, IE = IE, IM = IM, OE = OE, OM = x', PE = PE, PM = PM, RC = RC, Reserved = Reserved, UE = UE, UM = UM, ZE = ZE, ZM = ZM}: MXCSR fun MXCSR_PE_rupd ({DAZ, DE, DM, FZ, IE, IM, OE, OM, PE, PM, RC, Reserved, UE, UM, ZE, ZM}: MXCSR, x') = {DAZ = DAZ, DE = DE, DM = DM, FZ = FZ, IE = IE, IM = IM, OE = OE, OM = OM, PE = x', PM = PM, RC = RC, Reserved = Reserved, UE = UE, UM = UM, ZE = ZE, ZM = ZM}: MXCSR fun MXCSR_PM_rupd ({DAZ, DE, DM, FZ, IE, IM, OE, OM, PE, PM, RC, Reserved, UE, UM, ZE, ZM}: MXCSR, x') = {DAZ = DAZ, DE = DE, DM = DM, FZ = FZ, IE = IE, IM = IM, OE = OE, OM = OM, PE = PE, PM = x', RC = RC, Reserved = Reserved, UE = UE, UM = UM, ZE = ZE, ZM = ZM}: MXCSR fun MXCSR_RC_rupd ({DAZ, DE, DM, FZ, IE, IM, OE, OM, PE, PM, RC, Reserved, UE, UM, ZE, ZM}: MXCSR, x') = {DAZ = DAZ, DE = DE, DM = DM, FZ = FZ, IE = IE, IM = IM, OE = OE, OM = OM, PE = PE, PM = PM, RC = x', Reserved = Reserved, UE = UE, UM = UM, ZE = ZE, ZM = ZM}: MXCSR fun MXCSR_Reserved_rupd ({DAZ, DE, DM, FZ, IE, IM, OE, OM, PE, PM, RC, Reserved, UE, UM, ZE, ZM}: MXCSR, x') = {DAZ = DAZ, DE = DE, DM = DM, FZ = FZ, IE = IE, IM = IM, OE = OE, OM = OM, PE = PE, PM = PM, RC = RC, Reserved = x', UE = UE, UM = UM, ZE = ZE, ZM = ZM}: MXCSR fun MXCSR_UE_rupd ({DAZ, DE, DM, FZ, IE, IM, OE, OM, PE, PM, RC, Reserved, UE, UM, ZE, ZM}: MXCSR, x') = {DAZ = DAZ, DE = DE, DM = DM, FZ = FZ, IE = IE, IM = IM, OE = OE, OM = OM, PE = PE, PM = PM, RC = RC, Reserved = Reserved, UE = x', UM = UM, ZE = ZE, ZM = ZM}: MXCSR fun MXCSR_UM_rupd ({DAZ, DE, DM, FZ, IE, IM, OE, OM, PE, PM, RC, Reserved, UE, UM, ZE, ZM}: MXCSR, x') = {DAZ = DAZ, DE = DE, DM = DM, FZ = FZ, IE = IE, IM = IM, OE = OE, OM = OM, PE = PE, PM = PM, RC = RC, Reserved = Reserved, UE = UE, UM = x', ZE = ZE, ZM = ZM}: MXCSR fun MXCSR_ZE_rupd ({DAZ, DE, DM, FZ, IE, IM, OE, OM, PE, PM, RC, Reserved, UE, UM, ZE, ZM}: MXCSR, x') = {DAZ = DAZ, DE = DE, DM = DM, FZ = FZ, IE = IE, IM = IM, OE = OE, OM = OM, PE = PE, PM = PM, RC = RC, Reserved = Reserved, UE = UE, UM = UM, ZE = x', ZM = ZM}: MXCSR fun MXCSR_ZM_rupd ({DAZ, DE, DM, FZ, IE, IM, OE, OM, PE, PM, RC, Reserved, UE, UM, ZE, ZM}: MXCSR, x') = {DAZ = DAZ, DE = DE, DM = DM, FZ = FZ, IE = IE, IM = IM, OE = OE, OM = OM, PE = PE, PM = PM, RC = RC, Reserved = Reserved, UE = UE, UM = UM, ZE = ZE, ZM = x'}: MXCSR fun REX_B_rupd ({B, R, W, X}: REX, x') = {B = x', R = R, W = W, X = X} : REX fun REX_R_rupd ({B, R, W, X}: REX, x') = {B = B, R = x', W = W, X = X} : REX fun REX_W_rupd ({B, R, W, X}: REX, x') = {B = B, R = R, W = x', X = X} : REX fun REX_X_rupd ({B, R, W, X}: REX, x') = {B = B, R = R, W = W, X = x'} : REX (* ------------------------------------------------------------------------- Exceptions ------------------------------------------------------------------------- *) exception BadFlagAccess of string exception FAILURE of string exception INTERRUPT_EXCEPTION of BitsN.nbit (* ------------------------------------------------------------------------- Global variables (state) ------------------------------------------------------------------------- *) val EFLAGS = ref (Map.mkMap(SOME 6,NONE)): ((bool option) Map.map) ref val MEM = ref (Map.mkMap(SOME 18446744073709551616,BitsN.B(0x0,8))) : (BitsN.nbit Map.map) ref val MXCSR = ref ({DAZ = false, DE = false, DM = false, FZ = false, IE = false, IM = false, OE = false, OM = false, PE = false, PM = false, RC = BitsN.B(0x0,2), Reserved = BitsN.B(0x0,16), UE = false, UM = false, ZE = false, ZM = false}): MXCSR ref val REG = ref (Map.mkMap(SOME 16,BitsN.B(0x0,64))) : (BitsN.nbit Map.map) ref val RIP = ref (BitsN.B(0x0,64)): BitsN.nbit ref val XMM_REG = ref (Map.mkMap(SOME 8,BitsN.B(0x0,128))) : (BitsN.nbit Map.map) ref (* ------------------------------------------------------------------------- Main specification ------------------------------------------------------------------------- *) local fun tuple'3 [t0,t1,t2] = (t0,(t1,t2)) | tuple'3 (_: bool list) = raise Fail "tuple'3" in val boolify'3 = tuple'3 o BitsN.toList end local fun tuple'8 [t0,t1,t2,t3,t4,t5,t6,t7] = (t0,(t1,(t2,(t3,(t4,(t5,(t6,t7))))))) | tuple'8 (_: bool list) = raise Fail "tuple'8" in val boolify'8 = tuple'8 o BitsN.toList end fun DE_exception () = raise INTERRUPT_EXCEPTION (BitsN.B(0x0,8)); fun UD_exception () = raise INTERRUPT_EXCEPTION (BitsN.B(0x6,8)); fun GP_exception () = raise INTERRUPT_EXCEPTION (BitsN.B(0xD,8)); fun XM_exception () = raise INTERRUPT_EXCEPTION (BitsN.B(0x13,8)); fun rec'MXCSR x = {DAZ = BitsN.bit(x,6), DE = BitsN.bit(x,1), DM = BitsN.bit(x,8), FZ = BitsN.bit(x,15), IE = BitsN.bit(x,0), IM = BitsN.bit(x,7), OE = BitsN.bit(x,3), OM = BitsN.bit(x,10), PE = BitsN.bit(x,5), PM = BitsN.bit(x,12), RC = BitsN.bits(14,13) x, Reserved = BitsN.bits(31,16) x, UE = BitsN.bit(x,4), UM = BitsN.bit(x,11), ZE = BitsN.bit(x,2), ZM = BitsN.bit(x,9)}; fun reg'MXCSR x = case x of {DAZ = DAZ, DE = DE, DM = DM, FZ = FZ, IE = IE, IM = IM, OE = OE, OM = OM, PE = PE, PM = PM, RC = RC, Reserved = Reserved, UE = UE, UM = UM, ZE = ZE, ZM = ZM} => BitsN.concat [Reserved,BitsN.fromBit FZ,RC,BitsN.fromBit PM,BitsN.fromBit UM, BitsN.fromBit OM,BitsN.fromBit ZM,BitsN.fromBit DM, BitsN.fromBit IM,BitsN.fromBit DAZ,BitsN.fromBit PE, BitsN.fromBit UE,BitsN.fromBit OE,BitsN.fromBit ZE, BitsN.fromBit DE,BitsN.fromBit IE]; fun write'rec'MXCSR (_,x) = reg'MXCSR x; fun write'reg'MXCSR (_,x) = rec'MXCSR x; fun mem8 addr = Map.lookup((!MEM),BitsN.toNat addr); fun write'mem8 (b,addr) = MEM := (Map.update((!MEM),BitsN.toNat addr,b)); fun mem16 addr = BitsN.@@(mem8(BitsN.+(addr,BitsN.B(0x1,64))),mem8 addr); fun write'mem16 (w,addr) = ( write'mem8(BitsN.bits(7,0) w,addr) ; let val x = BitsN.+(addr,BitsN.B(0x1,64)) in write'mem8(BitsN.bits(15,8) w,x) end ); fun mem32 addr = BitsN.@@(mem16(BitsN.+(addr,BitsN.B(0x2,64))),mem16 addr); fun write'mem32 (w,addr) = ( write'mem16(BitsN.bits(15,0) w,addr) ; let val x = BitsN.+(addr,BitsN.B(0x2,64)) in write'mem16(BitsN.bits(31,16) w,x) end ); fun mem64 addr = BitsN.@@(mem32(BitsN.+(addr,BitsN.B(0x4,64))),mem32 addr); fun write'mem64 (w,addr) = ( write'mem32(BitsN.bits(31,0) w,addr) ; let val x = BitsN.+(addr,BitsN.B(0x4,64)) in write'mem32(BitsN.bits(63,32) w,x) end ); fun mem128 addr = BitsN.@@(mem64(BitsN.+(addr,BitsN.B(0x8,64))),mem64 addr); fun write'mem128 (w,addr) = ( write'mem64(BitsN.bits(63,0) w,addr) ; let val x = BitsN.+(addr,BitsN.B(0x8,64)) in write'mem64(BitsN.bits(127,64) w,x) end ); fun Eflag flag = case Map.lookup((!EFLAGS),Cast.ZeflagsToNat flag) of Option.SOME b => b | NONE => raise BadFlagAccess (Cast.ZeflagsToString flag); fun write'Eflag (b,flag) = EFLAGS := (Map.update((!EFLAGS),Cast.ZeflagsToNat flag,Option.SOME b)); fun FlagUnspecified flag = EFLAGS := (Map.update((!EFLAGS),Cast.ZeflagsToNat flag,NONE)); fun CF () = Eflag Z_CF; fun write'CF b = write'Eflag(b,Z_CF); fun PF () = Eflag Z_PF; fun write'PF b = write'Eflag(b,Z_PF); fun AF () = Eflag Z_AF; fun write'AF b = write'Eflag(b,Z_AF); fun ZF () = Eflag Z_ZF; fun write'ZF b = write'Eflag(b,Z_ZF); fun SF () = Eflag Z_SF; fun write'SF b = write'Eflag(b,Z_SF); fun OF () = Eflag Z_OF; fun write'OF b = write'Eflag(b,Z_OF); fun ea_index index = case index of NONE => BitsN.B(0x0,64) | Option.SOME(scale,idx) => BitsN.* (BitsN.<<(BitsN.B(0x1,64),BitsN.toNat scale), Map.lookup((!REG),Cast.ZregToNat idx)); fun ea_base base = case base of ZnoBase => BitsN.B(0x0,64) | ZripBase => (!RIP) | ZregBase b => Map.lookup((!REG),Cast.ZregToNat b); fun mem_addr m = let val (index,(base,displacement)) = m in BitsN.+(BitsN.+(ea_index index,ea_base base),displacement) end; fun ea_Zrm (size,rm) = case rm of Zr r => Zea_r(size,r) | Zm m => Zea_m(size,mem_addr m); fun ea_Zdest (size,ds) = case ds of Zrm_i(rm,_) => ea_Zrm(size,rm) | Zrm_r(rm,_) => ea_Zrm(size,rm) | Zr_rm(r,_) => Zea_r(size,r); fun ea_Zsrc (size,ds) = case ds of Zrm_i(_,i) => Zea_i(size,i) | Zrm_r(_,r) => Zea_r(size,r) | Zr_rm(_,rm) => ea_Zrm(size,rm); fun ea_Zimm_rm imm_rm = case imm_rm of Zrm rm => ea_Zrm(Z64,rm) | Zimm imm => Zea_i(Z64,imm); fun modSize (size,imm) = case size of Z8 _ => BitsN.mod(imm,BitsN.B(0x8,64)) | Z16 => BitsN.mod(imm,BitsN.B(0x10,64)) | Z32 => BitsN.mod(imm,BitsN.B(0x20,64)) | Z64 => BitsN.mod(imm,BitsN.B(0x40,64)); fun restrictSize (size,imm) = case size of Z8 _ => BitsN.&&(imm,BitsN.B(0xFF,64)) | Z16 => BitsN.&&(imm,BitsN.B(0xFFFF,64)) | Z32 => BitsN.&&(imm,BitsN.B(0xFFFFFFFF,64)) | Z64 => imm; fun EA ea = case ea of Zea_i i => restrictSize i | Zea_r(Z8 have_rex,r) => BitsN.&& (if have_rex orelse (not(Set.mem(r,[RSP,RBP,RSI,RDI]))) then Map.lookup((!REG),Cast.ZregToNat r) else BitsN.>>+ (Map.lookup ((!REG), Cast.ZregToNat (Cast.natToZreg(Nat.-(Cast.ZregToNat r,4)))),8), BitsN.B(0xFF,64)) | Zea_r(s,r) => restrictSize(s,Map.lookup((!REG),Cast.ZregToNat r)) | Zea_m(Z8 _,a) => BitsN.fromNat(BitsN.toNat(mem8 a),64) | Zea_m(Z16,a) => BitsN.fromNat(BitsN.toNat(mem16 a),64) | Zea_m(Z32,a) => BitsN.fromNat(BitsN.toNat(mem32 a),64) | Zea_m(Z64,a) => mem64 a; fun write'EA (w,ea) = case ea of Zea_i i => raise FAILURE "write to constant" | Zea_r(Z8 have_rex,r) => (if have_rex orelse (not(Set.mem(r,[RSP,RBP,RSI,RDI]))) then let val w0 = Map.lookup((!REG),Cast.ZregToNat r) in REG := (Map.update ((!REG),Cast.ZregToNat r, BitsN.bitFieldInsert(7,0) (w0,BitsN.bits(7,0) w))) end else let val x = Cast.natToZreg(Nat.-(Cast.ZregToNat r,4)) val w0 = Map.lookup((!REG),Cast.ZregToNat x) in REG := (Map.update ((!REG),Cast.ZregToNat x, BitsN.bitFieldInsert(15,8) (w0,BitsN.bits(7,0) w))) end) | Zea_r(Z16,r) => let val w0 = Map.lookup((!REG),Cast.ZregToNat r) in REG := (Map.update ((!REG),Cast.ZregToNat r, BitsN.bitFieldInsert(15,0) (w0,BitsN.bits(15,0) w))) end | Zea_r(Z32,r) => REG := (Map.update ((!REG),Cast.ZregToNat r,BitsN.zeroExtend 64 (BitsN.bits(31,0) w))) | Zea_r(Z64,r) => REG := (Map.update((!REG),Cast.ZregToNat r,w)) | Zea_m(Z8 _,a) => write'mem8(BitsN.bits(7,0) w,a) | Zea_m(Z16,a) => write'mem16(BitsN.bits(15,0) w,a) | Zea_m(Z32,a) => write'mem32(BitsN.bits(31,0) w,a) | Zea_m(Z64,a) => write'mem64(w,a); fun read_dest_src_ea sd = let val ea = ea_Zdest sd in (ea,(EA ea,EA(ea_Zsrc sd))) end; fun call_dest_from_ea ea = case ea of Zea_i(_,i) => BitsN.+((!RIP),i) | Zea_r(_,r) => Map.lookup((!REG),Cast.ZregToNat r) | Zea_m(_,a) => mem64 a; fun get_ea_address ea = case ea of Zea_i(_,i) => BitsN.B(0x0,64) | Zea_r(_,r) => BitsN.B(0x0,64) | Zea_m(_,a) => a; fun jump_to_ea ea = RIP := (call_dest_from_ea ea); fun ByteParity b = let val count = Nat.+ (Nat.+ (Nat.+ (Nat.+ (Nat.+ (Nat.+ (Nat.+ (Nat.fromBool(BitsN.bit(b,7)), Nat.fromBool(BitsN.bit(b,6))), Nat.fromBool(BitsN.bit(b,5))), Nat.fromBool(BitsN.bit(b,4))), Nat.fromBool(BitsN.bit(b,3))), Nat.fromBool(BitsN.bit(b,2))),Nat.fromBool(BitsN.bit(b,1))), Nat.fromBool(BitsN.bit(b,0))) in (Nat.mod(count,2)) = 0 end; fun Zsize_width size = case size of Z8 _ => 8 | Z16 => 16 | Z32 => 32 | Z64 => 64; fun word_size_msb (size,w) = BitsN.bit(w,Nat.-(Zsize_width size,1)); fun write_PF w = write'PF(ByteParity(BitsN.bits(7,0) w)); fun write_SF s_w = write'SF(word_size_msb s_w); fun write_ZF (size,w) = write'ZF (case size of Z8 _ => (BitsN.fromNat(BitsN.toNat w,8)) = (BitsN.B(0x0,8)) | Z16 => (BitsN.fromNat(BitsN.toNat w,16)) = (BitsN.B(0x0,16)) | Z32 => (BitsN.fromNat(BitsN.toNat w,32)) = (BitsN.B(0x0,32)) | Z64 => w = (BitsN.B(0x0,64))); fun write_arith_eflags_except_CF_OF (size,w) = ( write_PF w; write_SF(size,w); write_ZF(size,w); FlagUnspecified Z_AF ); fun write_arith_eflags (size,(w,(c,x))) = ( write'CF c; write'OF x; write_arith_eflags_except_CF_OF(size,w) ); fun write_logical_eflags (size,w) = write_arith_eflags(size,(w,(false,false))); fun erase_eflags () = EFLAGS := (Map.mkMap(SOME 6,NONE)); fun value_width s = Nat.pow(2,Zsize_width s); fun word_signed_overflow_add (size,(a,b)) = ((word_size_msb(size,a)) = (word_size_msb(size,b))) andalso (not((word_size_msb(size,BitsN.+(a,b))) = (word_size_msb(size,a)))); fun word_signed_overflow_sub (size,(a,b)) = (not((word_size_msb(size,a)) = (word_size_msb(size,b)))) andalso (not((word_size_msb(size,BitsN.-(a,b))) = (word_size_msb(size,a)))); fun add_with_carry_out (size,(x,y)) = (BitsN.+(x,y), (Nat.<=(value_width size,Nat.+(BitsN.toNat x,BitsN.toNat y)), word_signed_overflow_add(size,(x,y)))); fun sub_with_borrow (size,(x,y)) = (BitsN.-(x,y),(BitsN.<+(x,y),word_signed_overflow_sub(size,(x,y)))); fun write_arith_result (size,(r,ea)) = ( write_arith_eflags(size,r); write'EA(L3.fst r,ea) ); fun write_arith_result_no_CF_OF (size,(w,ea)) = ( write_arith_eflags_except_CF_OF(size,w); write'EA(w,ea) ); fun write_logical_result (size,(w,ea)) = ( write_logical_eflags(size,w); write'EA(w,ea) ); fun write_result_erase_eflags (w,ea) = ( erase_eflags (); write'EA(w,ea) ); fun SignExtension (w,(size1,size2)) = let val v = ref w in ( case (size1,size2) of (Z8 _,Z16) => v := (BitsN.bitFieldInsert(15,0) ((!v),BitsN.signExtend 16 (BitsN.bits(7,0) w))) | (Z8 _,Z32) => v := (BitsN.bitFieldInsert(31,0) ((!v),BitsN.signExtend 32 (BitsN.bits(7,0) w))) | (Z8 _,Z64) => v := (BitsN.signExtend 64 (BitsN.bits(7,0) w)) | (Z16,Z32) => v := (BitsN.bitFieldInsert(31,0) ((!v),BitsN.signExtend 32 (BitsN.bits(15,0) w))) | (Z16,Z64) => v := (BitsN.signExtend 64 (BitsN.bits(15,0) w)) | (Z32,Z64) => v := (BitsN.signExtend 64 (BitsN.bits(31,0) w)) | _ => raise FAILURE "SignExtension" ; (!v) ) end; fun SignExtension64 (w,size) = if size = Z64 then w else SignExtension(w,(size,Z64)); fun maskShift (size,w) = if size = Z64 then BitsN.toNat(BitsN.bits(5,0) w) else BitsN.toNat(BitsN.bits(4,0) w); fun ROL (size,(x,y)) = case size of Z8 _ => BitsN.fromNat (BitsN.toNat (BitsN.#<<(BitsN.bits(7,0) x,BitsN.toNat(BitsN.bits(4,0) y))), 64) | Z16 => BitsN.fromNat (BitsN.toNat (BitsN.#<<(BitsN.bits(15,0) x,BitsN.toNat(BitsN.bits(4,0) y))), 64) | Z32 => BitsN.fromNat (BitsN.toNat (BitsN.#<<(BitsN.bits(31,0) x,BitsN.toNat(BitsN.bits(4,0) y))), 64) | Z64 => BitsN.#<<(x,BitsN.toNat(BitsN.bits(5,0) y)); fun ROR (size,(x,y)) = case size of Z8 _ => BitsN.fromNat (BitsN.toNat (BitsN.#>>(BitsN.bits(7,0) x,BitsN.toNat(BitsN.bits(4,0) y))), 64) | Z16 => BitsN.fromNat (BitsN.toNat (BitsN.#>>(BitsN.bits(15,0) x,BitsN.toNat(BitsN.bits(4,0) y))), 64) | Z32 => BitsN.fromNat (BitsN.toNat (BitsN.#>>(BitsN.bits(31,0) x,BitsN.toNat(BitsN.bits(4,0) y))), 64) | Z64 => BitsN.#>>(x,BitsN.toNat(BitsN.bits(5,0) y)); fun SAR (size,(x,y)) = case size of Z8 _ => BitsN.fromNat (BitsN.toNat (BitsN.>>(BitsN.bits(7,0) x,BitsN.toNat(BitsN.bits(4,0) y))), 64) | Z16 => BitsN.fromNat (BitsN.toNat (BitsN.>>(BitsN.bits(15,0) x,BitsN.toNat(BitsN.bits(4,0) y))),64) | Z32 => BitsN.fromNat (BitsN.toNat (BitsN.>>(BitsN.bits(31,0) x,BitsN.toNat(BitsN.bits(4,0) y))),64) | Z64 => BitsN.>>(x,BitsN.toNat(BitsN.bits(5,0) y)); fun write_binop (s,(bop,(x,(y,ea)))) = case bop of Zadd => write_arith_result(s,(add_with_carry_out(s,(x,y)),ea)) | Zsub => write_arith_result(s,(sub_with_borrow(s,(x,y)),ea)) | Zcmp => write_arith_eflags(s,sub_with_borrow(s,(x,y))) | Ztest => write_logical_eflags(s,BitsN.&&(x,y)) | Zand => write_logical_result(s,(BitsN.&&(x,y),ea)) | Zxor => write_logical_result(s,(BitsN.??(x,y),ea)) | Zor => write_logical_result(s,(BitsN.||(x,y),ea)) | Zrol => write_result_erase_eflags(ROL(s,(x,y)),ea) | Zror => write_result_erase_eflags(ROR(s,(x,y)),ea) | Zsar => write_result_erase_eflags(SAR(s,(x,y)),ea) | Zshl => write_result_erase_eflags(BitsN.<<(x,maskShift(s,y)),ea) | Zshr => write_result_erase_eflags(BitsN.>>+(x,maskShift(s,y)),ea) | Zadc => let val carry = CF () val result = BitsN.+(BitsN.+(x,y),BitsN.fromBool 64 carry) in ( write'CF (Nat.<= (value_width s, Nat.+ (Nat.+(BitsN.toNat x,BitsN.toNat y),Nat.fromBool carry))) ; FlagUnspecified Z_OF ; write_arith_result_no_CF_OF(s,(result,ea)) ) end | Zsbb => let val carry = CF () val result = BitsN.-(x,BitsN.+(y,BitsN.fromBool 64 carry)) in ( write'CF (Nat.<(BitsN.toNat x,Nat.+(BitsN.toNat y,Nat.fromBool carry))) ; FlagUnspecified Z_OF ; write_arith_result_no_CF_OF(s,(result,ea)) ) end | _ => raise FAILURE ("Binary op not implemented: " ^ (Cast.Zbinop_nameToString bop)); fun write_monop (s,(mop,(x,ea))) = case mop of Znot => write'EA(BitsN.~ x,ea) | Zdec => write_arith_result_no_CF_OF(s,(BitsN.-(x,BitsN.B(0x1,64)),ea)) | Zinc => write_arith_result_no_CF_OF(s,(BitsN.+(x,BitsN.B(0x1,64)),ea)) | Zneg => ( write_arith_result_no_CF_OF(s,(BitsN.neg x,ea)) ; FlagUnspecified Z_CF ); fun bit_test (bt,(base,offset)) = let val bit = BitsN.bit(EA base,offset) in ( write'CF bit ; case bt of Zbt => () | Zbtc => let val w = EA base in write'EA (BitsN.bitFieldInsert(offset,offset) (w,BitsN.fromBit(not bit)),base) end | Zbtr => let val w = EA base in write'EA (BitsN.bitFieldInsert(offset,offset) (w,BitsN.fromBit false), base) end | Zbts => let val w = EA base in write'EA (BitsN.bitFieldInsert(offset,offset) (w,BitsN.fromBit true), base) end ) end; fun read_cond c = case c of Z_A => (case (Map.lookup((!EFLAGS),Cast.ZeflagsToNat Z_CF), Map.lookup((!EFLAGS),Cast.ZeflagsToNat Z_ZF)) of (Option.SOME false,Option.SOME false) => true | (Option.SOME true,_) => false | (_,Option.SOME true) => false | _ => raise BadFlagAccess ("read_cond: " ^ (Cast.ZcondToString c))) | Z_NB => not(CF ()) | Z_B => CF () | Z_NA => (case (Map.lookup((!EFLAGS),Cast.ZeflagsToNat Z_CF), Map.lookup((!EFLAGS),Cast.ZeflagsToNat Z_ZF)) of (Option.SOME true,_) => true | (_,Option.SOME true) => true | (Option.SOME false,Option.SOME false) => false | _ => raise BadFlagAccess ("read_cond: " ^ (Cast.ZcondToString c))) | Z_E => ZF () | Z_G => (case (Map.lookup((!EFLAGS),Cast.ZeflagsToNat Z_SF), Map.lookup((!EFLAGS),Cast.ZeflagsToNat Z_OF)) of (Option.SOME a,Option.SOME b) => (a = b) andalso (not(ZF ())) | _ => (case Map.lookup((!EFLAGS),Cast.ZeflagsToNat Z_ZF) of Option.SOME true => false | _ => raise BadFlagAccess ("read_cond: " ^ (Cast.ZcondToString c)))) | Z_NL => (SF ()) = (OF ()) | Z_L => not((SF ()) = (OF ())) | Z_NG => (case (Map.lookup((!EFLAGS),Cast.ZeflagsToNat Z_SF), Map.lookup((!EFLAGS),Cast.ZeflagsToNat Z_OF)) of (Option.SOME a,Option.SOME b) => (not(a = b)) orelse (ZF ()) | _ => (case Map.lookup((!EFLAGS),Cast.ZeflagsToNat Z_ZF) of Option.SOME true => true | _ => raise BadFlagAccess ("read_cond: " ^ (Cast.ZcondToString c)))) | Z_NE => not(ZF ()) | Z_NO => not(OF ()) | Z_NP => not(PF ()) | Z_NS => not(SF ()) | Z_O => OF () | Z_P => PF () | Z_S => SF () | Z_ALWAYS => true; fun x64_pop_aux () = let val rsp = Map.lookup((!REG),Cast.ZregToNat RSP) val top = mem64 rsp in ( REG := (Map.update((!REG),Cast.ZregToNat RSP,BitsN.+(rsp,BitsN.B(0x8,64)))) ; top ) end; fun x64_pop rm = let val x = ea_Zrm(Z64,rm) in write'EA(x64_pop_aux (),x) end; fun x64_pop_rip () = RIP := (x64_pop_aux ()); fun x64_push_aux w = let val rsp = BitsN.-(Map.lookup((!REG),Cast.ZregToNat RSP),BitsN.B(0x8,64)) in ( REG := (Map.update((!REG),Cast.ZregToNat RSP,rsp)) ; write'mem64(w,rsp) ) end; fun x64_push imm_rm = x64_push_aux(EA(ea_Zimm_rm imm_rm)); fun x64_push_rip () = x64_push_aux (!RIP); fun x64_drop imm = ( if not((BitsN.bits(7,0) imm) = (BitsN.B(0x0,8))) then raise FAILURE "x64_drop" else () ; REG := (Map.update ((!REG),Cast.ZregToNat RSP, BitsN.+(Map.lookup((!REG),Cast.ZregToNat RSP),imm))) ); fun initial_ieee_flags invalid = let val flags = ref {DivideByZero = false, InvalidOp = false, Overflow = false, Precision = false, Underflow = false} in ( flags := (SSE.ieee_flags_DivideByZero_rupd((!flags),false)) ; flags := (SSE.ieee_flags_InvalidOp_rupd((!flags),invalid)) ; flags := (SSE.ieee_flags_Overflow_rupd((!flags),false)) ; flags := (SSE.ieee_flags_Precision_rupd((!flags),false)) ; flags := (SSE.ieee_flags_Underflow_rupd((!flags),false)) ; (!flags) ) end; fun set_precision (flags,b) = let val f = ref flags in ( f := (SSE.ieee_flags_Precision_rupd((!f),b)); (!f) ) end; fun zero32 a = if BitsN.msb a then FP32.negZero else FP32.posZero; fun zero64 a = if BitsN.msb a then FP64.negZero else FP64.posZero; fun denormal_to_zero32 a = if (#DAZ((!MXCSR) : MXCSR)) andalso (FP32.isSubnormal a) then zero32 a else a; fun denormal_to_zero64 a = if (#DAZ((!MXCSR) : MXCSR)) andalso (FP64.isSubnormal a) then zero64 a else a; fun flush_to_zero32 (flags,a) = if (#FZ((!MXCSR) : MXCSR)) andalso ((#UM((!MXCSR) : MXCSR)) andalso (#Underflow(flags : SSE.ieee_flags))) then (set_precision(flags,true),zero32 a) else (flags,a); fun flush_to_zero64 (flags,a) = if (#FZ((!MXCSR) : MXCSR)) andalso ((#UM((!MXCSR) : MXCSR)) andalso (#Underflow(flags : SSE.ieee_flags))) then (set_precision(flags,true),zero64 a) else (flags,a); fun sse_from_int64 N (m,w) = let val i = BitsN.toInt w val q = FP64.fromInt(m,i) in (set_precision (initial_ieee_flags false,not((FP64.toInt(m,q)) = (Option.SOME i))), q) end; fun sse_from_int32 N (m,w) = let val i = BitsN.toInt w val d = FP32.fromInt(m,i) in (set_precision (initial_ieee_flags false,not((FP32.toInt(m,d)) = (Option.SOME i))), d) end; fun sse_to_int64 N (m,a) = case FP64.toInt(m,a) of Option.SOME i => (if (IntInf.<= (IntInf.~ (IntExtra.pow(2,Nat.-(BitsN.size(BitsN.BV(0x0,N)),1))),i)) andalso (IntInf.<= (i, IntInf.- (IntExtra.pow(2,Nat.-(BitsN.size(BitsN.BV(0x0,N)),1)),1))) then let val w = BitsN.fromInt(i,N) val f = set_precision (initial_ieee_flags false, not(FP64.equal(FP64.fromInt(m,BitsN.toInt w),a))) in (f,w) end else (initial_ieee_flags true,BitsN.#>>(BitsN.BV(0x1,N),1))) | NONE => (initial_ieee_flags true,BitsN.#>>(BitsN.BV(0x1,N),1)); fun sse_to_int32 N (m,a) = case FP32.toInt(m,a) of Option.SOME i => (if (IntInf.<= (IntInf.~ (IntExtra.pow(2,Nat.-(BitsN.size(BitsN.BV(0x0,N)),1))),i)) andalso (IntInf.<= (i, IntInf.- (IntExtra.pow(2,Nat.-(BitsN.size(BitsN.BV(0x0,N)),1)),1))) then let val w = BitsN.fromInt(i,N) val f = set_precision (initial_ieee_flags false, not(FP32.equal(FP32.fromInt(m,BitsN.toInt w),a))) in (f,w) end else (initial_ieee_flags true,BitsN.#>>(BitsN.BV(0x1,N),1))) | NONE => (initial_ieee_flags true,BitsN.#>>(BitsN.BV(0x1,N),1)); fun float_min32 (a,b) = let val flags = initial_ieee_flags((FP32.compare(a,b)) = IEEEReal.UNORDERED) in (flags, if (not(#InvalidOp(flags : SSE.ieee_flags))) andalso (FP32.lessThan(a,b)) then a else b) end; fun float_max32 (a,b) = let val flags = initial_ieee_flags((FP32.compare(a,b)) = IEEEReal.UNORDERED) in (flags, if (#InvalidOp(flags : SSE.ieee_flags)) orelse (FP32.lessEqual(a,b)) then b else a) end; fun float_min64 (a,b) = let val flags = initial_ieee_flags((FP64.compare(a,b)) = IEEEReal.UNORDERED) in (flags, if (not(#InvalidOp(flags : SSE.ieee_flags))) andalso (FP64.lessThan(a,b)) then a else b) end; fun float_max64 (a,b) = let val flags = initial_ieee_flags((FP64.compare(a,b)) = IEEEReal.UNORDERED) in (flags, if (#InvalidOp(flags : SSE.ieee_flags)) orelse (FP64.lessEqual(a,b)) then b else a) end; fun process_float_flags l = let val denorm = ref false in let val f = ref (initial_ieee_flags false) in ( L3.foreach (l, fn x => let val (d,flags) = x in ( denorm := ((!denorm) orelse d) ; f := (SSE.ieee_flags_DivideByZero_rupd ((!f), (#DivideByZero((!f) : SSE.ieee_flags)) orelse (#DivideByZero(flags : SSE.ieee_flags)))) ; f := (SSE.ieee_flags_InvalidOp_rupd ((!f), (#InvalidOp((!f) : SSE.ieee_flags)) orelse (#InvalidOp(flags : SSE.ieee_flags)))) ; f := (SSE.ieee_flags_Overflow_rupd ((!f), (#Overflow((!f) : SSE.ieee_flags)) orelse (#Overflow(flags : SSE.ieee_flags)))) ; f := (SSE.ieee_flags_Precision_rupd ((!f), (#Precision((!f) : SSE.ieee_flags)) orelse (#Precision(flags : SSE.ieee_flags)))) ; f := (SSE.ieee_flags_Underflow_rupd ((!f), (#Underflow((!f) : SSE.ieee_flags)) orelse (#Underflow(flags : SSE.ieee_flags)))) ) end) ; MXCSR := (MXCSR_IE_rupd ((!MXCSR), (#IE((!MXCSR) : MXCSR)) orelse (#InvalidOp((!f) : SSE.ieee_flags)))) ; MXCSR := (MXCSR_DE_rupd((!MXCSR),(#DE((!MXCSR) : MXCSR)) orelse (!denorm))) ; MXCSR := (MXCSR_ZE_rupd ((!MXCSR), (#ZE((!MXCSR) : MXCSR)) orelse (#DivideByZero((!f) : SSE.ieee_flags)))) ; if ((#InvalidOp((!f) : SSE.ieee_flags)) andalso (not(#IM((!MXCSR) : MXCSR)))) orelse (((!denorm) andalso (not(#DM((!MXCSR) : MXCSR)))) orelse ((#DivideByZero((!f) : SSE.ieee_flags)) andalso (not(#ZM((!MXCSR) : MXCSR))))) then XM_exception () else () ; MXCSR := (MXCSR_OE_rupd ((!MXCSR), (#OE((!MXCSR) : MXCSR)) orelse (#Overflow((!f) : SSE.ieee_flags)))) ; MXCSR := (MXCSR_PE_rupd ((!MXCSR), (#PE((!MXCSR) : MXCSR)) orelse (#Precision((!f) : SSE.ieee_flags)))) ; MXCSR := (MXCSR_UE_rupd ((!MXCSR), (#UE((!MXCSR) : MXCSR)) orelse (#Underflow((!f) : SSE.ieee_flags)))) ; if ((#Overflow((!f) : SSE.ieee_flags)) andalso (not(#OM((!MXCSR) : MXCSR)))) orelse (((#Precision((!f) : SSE.ieee_flags)) andalso (not(#PM((!MXCSR) : MXCSR)))) orelse ((#Underflow((!f) : SSE.ieee_flags)) andalso (not(#UM((!MXCSR) : MXCSR))))) then XM_exception () else () ) end end; fun RoundingMode () = case #RC((!MXCSR) : MXCSR) of BitsN.B(0x0,_) => IEEEReal.TO_NEAREST | BitsN.B(0x1,_) => IEEEReal.TO_NEGINF | BitsN.B(0x2,_) => IEEEReal.TO_POSINF | BitsN.B(0x3,_) => IEEEReal.TO_ZERO | _ => raise General.Bind; fun sse_binop32 (bop,(a,b)) = let val denorm = (FP32.isSubnormal a) orelse (FP32.isSubnormal b) val a = denormal_to_zero32 a val b = denormal_to_zero32 b val (f,r) = case bop of sse_add => flush_to_zero32(FP32.add(RoundingMode (),(a,b))) | sse_sub => flush_to_zero32(FP32.sub(RoundingMode (),(a,b))) | sse_mul => flush_to_zero32(FP32.mul(RoundingMode (),(a,b))) | sse_div => flush_to_zero32(FP32.div(RoundingMode (),(a,b))) | sse_max => float_max32(a,b) | sse_min => float_min32(a,b) in ((denorm,f),r) end; fun sse_binop64 (bop,(a,b)) = let val denorm = (FP64.isSubnormal a) orelse (FP64.isSubnormal b) val a = denormal_to_zero64 a val b = denormal_to_zero64 b val (f,r) = case bop of sse_add => flush_to_zero64(FP64.add(RoundingMode (),(a,b))) | sse_sub => flush_to_zero64(FP64.sub(RoundingMode (),(a,b))) | sse_mul => flush_to_zero64(FP64.mul(RoundingMode (),(a,b))) | sse_div => flush_to_zero64(FP64.div(RoundingMode (),(a,b))) | sse_max => float_max64(a,b) | sse_min => float_min64(a,b) in ((denorm,f),r) end; fun sse_sqrt32 a = let val (f,r) = FP32.sqrt(RoundingMode (),denormal_to_zero32 a) in ((FP32.isSubnormal a,f),r) end; fun sse_sqrt64 a = let val (f,r) = FP64.sqrt(RoundingMode (),denormal_to_zero64 a) in ((FP64.isSubnormal a,f),r) end; fun sse_logic N (bop,(a,b)) = case bop of sse_and => BitsN.&&(a,b) | sse_or => BitsN.||(a,b) | sse_xor => BitsN.??(a,b) | sse_andn => BitsN.&&(BitsN.~ a,b); fun sse_compare_signalling cmp = Set.mem(cmp,[sse_lt_os,sse_le_os,sse_nlt_us,sse_nle_us]); fun sse_compare32 (cmp,(a,b)) = let val unordered = (FP32.compare(a,b)) = IEEEReal.UNORDERED val c = case cmp of sse_eq_oq => FP32.equal(a,b) | sse_lt_os => FP32.lessThan(a,b) | sse_le_os => FP32.lessEqual(a,b) | sse_unord_q => unordered | sse_neq_uq => unordered orelse (not(FP32.equal(a,b))) | sse_nlt_us => unordered orelse (not(FP32.lessThan(a,b))) | sse_nle_us => unordered orelse (not(FP32.lessEqual(a,b))) | sss_ord_q => not unordered val flags = initial_ieee_flags ((FP32.isSignallingNan a) orelse ((FP32.isSignallingNan b) orelse (unordered andalso (sse_compare_signalling cmp)))) in (((FP32.isSubnormal a) orelse (FP32.isSubnormal b),flags), BitsN.signExtend 32 (BitsN.fromBit c)) end; fun sse_compare64 (cmp,(a,b)) = let val unordered = (FP64.compare(a,b)) = IEEEReal.UNORDERED val c = case cmp of sse_eq_oq => FP64.equal(a,b) | sse_lt_os => FP64.lessThan(a,b) | sse_le_os => FP64.lessEqual(a,b) | sse_unord_q => unordered | sse_neq_uq => unordered orelse (not(FP64.equal(a,b))) | sse_nlt_us => unordered orelse (not(FP64.lessThan(a,b))) | sse_nle_us => unordered orelse (not(FP64.lessEqual(a,b))) | sss_ord_q => not unordered val flags = initial_ieee_flags ((FP64.isSignallingNan a) orelse ((FP64.isSignallingNan b) orelse (unordered andalso (sse_compare_signalling cmp)))) in (((FP64.isSubnormal a) orelse (FP64.isSubnormal b),flags), BitsN.signExtend 64 (BitsN.fromBit c)) end; fun rm_to_xmm_mem rm = case rm of Zr r => xmm_reg(BitsN.fromNat(Cast.ZregToNat r,3)) | Zm m => xmm_mem m; fun XMM xm = case xm of xmm_reg r => Map.lookup((!XMM_REG),BitsN.toNat r) | xmm_mem m => mem128(mem_addr m); fun write'XMM (dqw,xm) = case xm of xmm_reg r => XMM_REG := (Map.update((!XMM_REG),BitsN.toNat r,dqw)) | xmm_mem m => let val x = mem_addr m in write'mem128(dqw,x) end; fun CheckAlignedXMM (xm,n) = case xm of xmm_reg r => () | xmm_mem m => let val a = mem_addr m in if not((BitsN.<<(BitsN.>>+(a,n),n)) = a) then GP_exception () else () end; fun dfn'bin_PD (bop,(dst,src)) = let val dst = xmm_reg dst val x = XMM dst val x0 = XMM src val (f1,r1) = sse_binop64(bop,(BitsN.bits(127,64) x,BitsN.bits(127,64) x0)) val (f2,r2) = sse_binop64(bop,(BitsN.bits(63,0) x,BitsN.bits(63,0) x0)) in ( process_float_flags[f1,f2]; write'XMM(BitsN.@@(r1,r2),dst) ) end; fun dfn'bin_PS (bop,(dst,src)) = let val dst = xmm_reg dst val x = XMM dst val x0 = XMM src val (f1,r1) = sse_binop32(bop,(BitsN.bits(127,96) x,BitsN.bits(127,96) x0)) val (f2,r2) = sse_binop32(bop,(BitsN.bits(95,64) x,BitsN.bits(95,64) x0)) val (f3,r3) = sse_binop32(bop,(BitsN.bits(63,32) x,BitsN.bits(63,32) x0)) val (f4,r4) = sse_binop32(bop,(BitsN.bits(31,0) x,BitsN.bits(31,0) x0)) in ( process_float_flags[f1,f2,f3,f4] ; write'XMM(BitsN.concat[r1,r2,r3,r4],dst) ) end; fun dfn'bin_SD (bop,(dst,src)) = let val dst = xmm_reg dst val x = XMM dst val x0 = XMM src val (f,r) = sse_binop64(bop,(BitsN.bits(63,0) x,BitsN.bits(63,0) x0)) in ( process_float_flags[f] ; let val w = XMM dst in write'XMM(BitsN.bitFieldInsert(63,0) (w,r),dst) end ) end; fun dfn'bin_SS (bop,(dst,src)) = let val dst = xmm_reg dst val x = XMM dst val x0 = XMM src val (f,r) = sse_binop32(bop,(BitsN.bits(31,0) x,BitsN.bits(31,0) x0)) in ( process_float_flags[f] ; let val w = XMM dst in write'XMM(BitsN.bitFieldInsert(31,0) (w,r),dst) end ) end; fun dfn'logic_PD (bop,(dst,src)) = let val dst = xmm_reg dst val x = XMM dst val x0 = XMM src val r1 = sse_logic 64 (bop,(BitsN.bits(127,64) x,BitsN.bits(127,64) x0)) val r2 = sse_logic 64 (bop,(BitsN.bits(63,0) x,BitsN.bits(63,0) x0)) in write'XMM(BitsN.@@(r1,r2),dst) end; fun dfn'logic_PS (bop,(dst,src)) = let val dst = xmm_reg dst val x = XMM dst val x0 = XMM src val r1 = sse_logic 32 (bop,(BitsN.bits(127,96) x,BitsN.bits(127,96) x0)) val r2 = sse_logic 32 (bop,(BitsN.bits(95,64) x,BitsN.bits(95,64) x0)) val r3 = sse_logic 32 (bop,(BitsN.bits(63,32) x,BitsN.bits(63,32) x0)) val r4 = sse_logic 32 (bop,(BitsN.bits(31,0) x,BitsN.bits(31,0) x0)) in write'XMM(BitsN.concat[r1,r2,r3,r4],dst) end; fun dfn'CMPPD (cmp,(dst,src)) = let val dst = xmm_reg dst val x = XMM dst val x0 = XMM src val (f1,r1) = sse_compare64(cmp,(BitsN.bits(127,64) x,BitsN.bits(127,64) x0)) val (f2,r2) = sse_compare64(cmp,(BitsN.bits(63,0) x,BitsN.bits(63,0) x0)) in ( process_float_flags[f1,f2]; write'XMM(BitsN.@@(r1,r2),dst) ) end; fun dfn'CMPPS (cmp,(dst,src)) = let val dst = xmm_reg dst val x = XMM dst val x0 = XMM src val (f1,r1) = sse_compare32(cmp,(BitsN.bits(127,96) x,BitsN.bits(127,96) x0)) val (f2,r2) = sse_compare32(cmp,(BitsN.bits(95,64) x,BitsN.bits(95,64) x0)) val (f3,r3) = sse_compare32(cmp,(BitsN.bits(63,32) x,BitsN.bits(63,32) x0)) val (f4,r4) = sse_compare32(cmp,(BitsN.bits(31,0) x,BitsN.bits(31,0) x0)) in ( process_float_flags[f1,f2,f3,f4] ; write'XMM(BitsN.concat[r1,r2,r3,r4],dst) ) end; fun dfn'CMPSD (cmp,(dst,src)) = let val dst = xmm_reg dst val x = XMM dst val x0 = XMM src val (f,r) = sse_compare64(cmp,(BitsN.bits(63,0) x,BitsN.bits(63,0) x0)) in ( process_float_flags[f] ; let val w = XMM dst in write'XMM(BitsN.bitFieldInsert(63,0) (w,r),dst) end ) end; fun dfn'CMPSS (cmp,(dst,src)) = let val dst = xmm_reg dst val x = XMM dst val x0 = XMM src val (f,r) = sse_compare32(cmp,(BitsN.bits(31,0) x,BitsN.bits(31,0) x0)) in ( process_float_flags[f] ; let val w = XMM dst in write'XMM(BitsN.bitFieldInsert(31,0) (w,r),dst) end ) end; fun dfn'COMISD (src1,src2) = let val x = XMM(xmm_reg src1) val x0 = XMM src2 in ( case FP64.compare(BitsN.bits(63,0) x,BitsN.bits(63,0) x0) of IEEEReal.UNORDERED => ( write'ZF true; write'PF true; write'CF true ) | IEEEReal.GREATER => ( write'ZF false; write'PF false; write'CF false ) | IEEEReal.LESS => ( write'ZF false; write'PF false; write'CF true ) | IEEEReal.EQUAL => ( write'ZF true; write'PF false; write'CF false ) ; write'OF false ; write'AF false ; write'SF false ) end; fun dfn'COMISS (src1,src2) = let val x = XMM(xmm_reg src1) val x0 = XMM src2 in ( case FP32.compare(BitsN.bits(31,0) x,BitsN.bits(31,0) x0) of IEEEReal.UNORDERED => ( write'ZF true; write'PF true; write'CF true ) | IEEEReal.GREATER => ( write'ZF false; write'PF false; write'CF false ) | IEEEReal.LESS => ( write'ZF false; write'PF false; write'CF true ) | IEEEReal.EQUAL => ( write'ZF true; write'PF false; write'CF false ) ; write'OF false ; write'AF false ; write'SF false ) end; fun dfn'CVTDQ2PD (dst,src) = let val x = XMM src val mode = RoundingMode () val x0 = xmm_reg dst in write'XMM (BitsN.@@ (FP64.fromInt(mode,BitsN.toInt(BitsN.bits(63,32) x)), FP64.fromInt(mode,BitsN.toInt(BitsN.bits(31,0) x))),x0) end; fun dfn'CVTDQ2PS (dst,src) = let val x = XMM src val mode = RoundingMode () val (f1,d1) = sse_from_int32 32 (mode,BitsN.bits(127,96) x) val (f2,d2) = sse_from_int32 32 (mode,BitsN.bits(95,64) x) val (f3,d3) = sse_from_int32 32 (mode,BitsN.bits(63,32) x) val (f4,d4) = sse_from_int32 32 (mode,BitsN.bits(31,0) x) in ( process_float_flags[(false,f1),(false,f2),(false,f3),(false,f4)] ; let val x = xmm_reg dst in write'XMM(BitsN.concat[d1,d2,d3,d4],x) end ) end; fun dfn'CVTPD2DQ (truncate,(dst,src)) = let val x = XMM src val mode = if truncate then IEEEReal.TO_ZERO else RoundingMode () val (f1,w1) = sse_to_int64 32 (mode,BitsN.bits(127,64) x) val (f2,w2) = sse_to_int64 32 (mode,BitsN.bits(63,0) x) in ( process_float_flags[(false,f1),(false,f2)] ; let val x = xmm_reg dst val w = XMM x in write'XMM(BitsN.bitFieldInsert(63,0) (w,BitsN.@@(w1,w2)),x) end ) end; fun dfn'CVTPD2PS (dst,src) = let val x = XMM src val q1 = BitsN.bits(127,64) x val mode = RoundingMode () val (f1,r1) = FPConvert.fp64_to_fp32_with_flags(mode,q1) val (f2,r2) = FPConvert.fp64_to_fp32_with_flags(mode,q1) val f1 = (FP64.isSubnormal q1,f1) val f2 = (FP64.isSubnormal(BitsN.bits(63,0) x),f2) in ( process_float_flags[f1,f2] ; let val x = xmm_reg dst val w = XMM x in write'XMM(BitsN.bitFieldInsert(63,0) (w,BitsN.@@(r1,r2)),x) end ) end; fun dfn'CVTPS2DQ (truncate,(dst,src)) = let val x = XMM src val mode = if truncate then IEEEReal.TO_ZERO else RoundingMode () val (f1,w1) = sse_to_int32 32 (mode,BitsN.bits(127,96) x) val (f2,w2) = sse_to_int32 32 (mode,BitsN.bits(95,64) x) val (f3,w3) = sse_to_int32 32 (mode,BitsN.bits(63,32) x) val (f4,w4) = sse_to_int32 32 (mode,BitsN.bits(31,0) x) in ( process_float_flags[(false,f1),(false,f2),(false,f3),(false,f4)] ; let val x = xmm_reg dst in write'XMM(BitsN.concat[w1,w2,w3,w4],x) end ) end; fun dfn'CVTPS2PD (dst,src) = let val x = XMM src val d1 = BitsN.bits(63,32) x val d2 = BitsN.bits(31,0) x val f1 = (FP32.isSubnormal d1,initial_ieee_flags(FP32.isSignallingNan d1)) val f2 = (FP32.isSubnormal d2,initial_ieee_flags(FP32.isSignallingNan d2)) in ( process_float_flags[f1,f2] ; let val x = xmm_reg dst in write'XMM (BitsN.@@(FPConvert.fp32_to_fp64 d1,FPConvert.fp32_to_fp64 d2),x) end ) end; fun dfn'CVTSD2SI (truncate,(quad,(dst,src))) = let val x = XMM src val q = BitsN.bits(63,0) x val mode = if truncate then IEEEReal.TO_ZERO else RoundingMode () in if quad then let val (f,w) = sse_to_int64 64 (mode,q) in ( process_float_flags[(false,f)] ; let val x = Zea_r(Z64,dst) in write'EA(w,x) end ) end else let val (f,w) = sse_to_int64 32 (mode,q) in ( process_float_flags[(false,f)] ; let val x = Zea_r(Z32,dst) in write'EA(BitsN.zeroExtend 64 w,x) end ) end end; fun dfn'CVTSD2SS (dst,src) = let val x = XMM src val q = BitsN.bits(63,0) x val (f,r) = FPConvert.fp64_to_fp32_with_flags(RoundingMode (),q) val f = (FP64.isSubnormal q,f) in ( process_float_flags[f] ; let val x = xmm_reg dst val w = XMM x in write'XMM(BitsN.bitFieldInsert(31,0) (w,r),x) end ) end; fun dfn'CVTSI2SD (quad,(dst,src)) = let val ea_src = ea_Zrm(if quad then Z64 else Z32,src) val (f,q) = sse_from_int64 64 (RoundingMode (),EA ea_src) in ( process_float_flags[(false,f)] ; let val x = xmm_reg dst val w = XMM x in write'XMM(BitsN.bitFieldInsert(63,0) (w,q),x) end ) end; fun dfn'CVTSI2SS (quad,(dst,src)) = let val ea_src = ea_Zrm(if quad then Z64 else Z32,src) val (f,d) = sse_from_int32 64 (RoundingMode (),EA ea_src) in ( process_float_flags[(false,f)] ; let val x = xmm_reg dst val w = XMM x in write'XMM(BitsN.bitFieldInsert(31,0) (w,d),x) end ) end; fun dfn'CVTSS2SD (dst,src) = let val x = XMM src val d = BitsN.bits(31,0) x val f = (FP32.isSubnormal d,initial_ieee_flags(FP32.isSignallingNan d)) in ( process_float_flags[f] ; let val x = xmm_reg dst val w = XMM x in write'XMM (BitsN.bitFieldInsert(63,0) (w,FPConvert.fp32_to_fp64 d),x) end ) end; fun dfn'CVTSS2SI (truncate,(quad,(dst,src))) = let val x = XMM src val d = BitsN.bits(31,0) x val mode = if truncate then IEEEReal.TO_ZERO else RoundingMode () in if quad then let val (f,w) = sse_to_int32 64 (mode,d) in ( process_float_flags[(false,f)] ; let val x = Zea_r(Z64,dst) in write'EA(w,x) end ) end else let val (f,w) = sse_to_int32 32 (mode,d) in ( process_float_flags[(false,f)] ; let val x = Zea_r(Z32,dst) in write'EA(BitsN.zeroExtend 64 w,x) end ) end end; fun dfn'MOVAP_D_S (double,(dst,src)) = ( CheckAlignedXMM(dst,4) ; CheckAlignedXMM(src,4) ; write'XMM(XMM src,dst) ); fun dfn'MOVUP_D_S (double,(dst,src)) = write'XMM(XMM src,dst); fun dfn'MOV_D_Q (to_xmm,(quad,(xmm,rm))) = case (to_xmm,quad) of (false,false) => let val x = ea_Zrm(Z32,rm) in write'EA (BitsN.zeroExtend 64 (BitsN.bits(31,0) (XMM(xmm_reg xmm))),x) end | (false,true) => let val x = ea_Zrm(Z64,rm) in write'EA(BitsN.bits(63,0) (XMM(xmm_reg xmm)),x) end | (true,false) => let val x = xmm_reg xmm in write'XMM (BitsN.zeroExtend 128 (BitsN.bits(31,0) (EA(ea_Zrm(Z32,rm)))),x) end | (true,true) => let val x = xmm_reg xmm in write'XMM(BitsN.zeroExtend 128 (EA(ea_Zrm(Z64,rm))),x) end; fun dfn'MOVQ (dst,src) = case dst of xmm_reg _ => write'XMM(BitsN.zeroExtend 128 (BitsN.bits(63,0) (XMM src)),dst) | xmm_mem m => let val x = ea_Zrm(Z64,Zm m) in write'EA(BitsN.bits(63,0) (XMM src),x) end; fun dfn'MOVSD (dst,src) = case src of xmm_reg _ => let val w = XMM dst in write'XMM (BitsN.bitFieldInsert(63,0) (w,BitsN.bits(63,0) (XMM src)),dst) end | xmm_mem _ => write'XMM(BitsN.zeroExtend 128 (BitsN.bits(63,0) (XMM src)),dst); fun dfn'MOVSS (dst,src) = case src of xmm_reg _ => let val w = XMM dst in write'XMM (BitsN.bitFieldInsert(31,0) (w,BitsN.bits(31,0) (XMM src)),dst) end | xmm_mem _ => write'XMM(BitsN.zeroExtend 128 (BitsN.bits(31,0) (XMM src)),dst); fun dfn'PCMPEQQ (dst,src) = let val dst = xmm_reg dst val x = XMM dst val x0 = XMM src in write'XMM (BitsN.@@ (if (BitsN.bits(127,64) x) = (BitsN.bits(127,64) x0) then BitsN.neg(BitsN.B(0x1,64)) else BitsN.B(0x0,64), if (BitsN.bits(63,0) x) = (BitsN.bits(63,0) x0) then BitsN.neg(BitsN.B(0x1,64)) else BitsN.B(0x0,64)),dst) end; fun dfn'PSLLDQ (dst,imm) = let val dst = xmm_reg dst in write'XMM(BitsN.<<(XMM dst,Nat.*(Nat.min(16,BitsN.toNat imm),8)),dst) end; fun dfn'PSLLD_imm (dst,imm) = let val dst = xmm_reg dst val x = XMM dst val i = BitsN.toNat imm in write'XMM (BitsN.concat [BitsN.<<(BitsN.bits(127,96) x,i), BitsN.<<(BitsN.bits(95,64) x,i),BitsN.<<(BitsN.bits(63,32) x,i), BitsN.<<(BitsN.bits(31,0) x,i)],dst) end; fun dfn'PSLLQ_imm (dst,imm) = let val dst = xmm_reg dst val x = XMM dst val i = BitsN.toNat imm in write'XMM (BitsN.@@ (BitsN.<<(BitsN.bits(127,64) x,i),BitsN.<<(BitsN.bits(63,0) x,i)), dst) end; fun dfn'PSLLW_imm (dst,imm) = let val dst = xmm_reg dst val x = XMM dst val i = BitsN.toNat imm in write'XMM (BitsN.concat [BitsN.<<(BitsN.bits(127,112) x,i), BitsN.<<(BitsN.bits(111,96) x,i), BitsN.<<(BitsN.bits(95,80) x,i),BitsN.<<(BitsN.bits(79,64) x,i), BitsN.<<(BitsN.bits(63,48) x,i),BitsN.<<(BitsN.bits(47,32) x,i), BitsN.<<(BitsN.bits(31,16) x,i),BitsN.<<(BitsN.bits(15,0) x,i)], dst) end; fun dfn'PSRAD_imm (dst,imm) = let val dst = xmm_reg dst val x = XMM dst val i = BitsN.toNat imm in write'XMM (BitsN.concat [BitsN.>>(BitsN.bits(127,96) x,i), BitsN.>>(BitsN.bits(95,64) x,i),BitsN.>>(BitsN.bits(63,32) x,i), BitsN.>>(BitsN.bits(31,0) x,i)],dst) end; fun dfn'PSRAW_imm (dst,imm) = let val dst = xmm_reg dst val x = XMM dst val i = BitsN.toNat imm in write'XMM (BitsN.concat [BitsN.>>(BitsN.bits(127,112) x,i), BitsN.>>(BitsN.bits(111,96) x,i), BitsN.>>(BitsN.bits(95,80) x,i),BitsN.>>(BitsN.bits(79,64) x,i), BitsN.>>(BitsN.bits(63,48) x,i),BitsN.>>(BitsN.bits(47,32) x,i), BitsN.>>(BitsN.bits(31,16) x,i),BitsN.>>(BitsN.bits(15,0) x,i)], dst) end; fun dfn'PSRLDQ (dst,imm) = let val dst = xmm_reg dst in write'XMM(BitsN.>>+(XMM dst,Nat.*(Nat.min(16,BitsN.toNat imm),8)),dst) end; fun dfn'PSRLD_imm (dst,imm) = let val dst = xmm_reg dst val x = XMM dst val i = BitsN.toNat imm in write'XMM (BitsN.concat [BitsN.>>+(BitsN.bits(127,96) x,i), BitsN.>>+(BitsN.bits(95,64) x,i), BitsN.>>+(BitsN.bits(63,32) x,i),BitsN.>>+(BitsN.bits(31,0) x,i)], dst) end; fun dfn'PSRLQ_imm (dst,imm) = let val dst = xmm_reg dst val x = XMM dst val i = BitsN.toNat imm in write'XMM (BitsN.@@ (BitsN.>>+(BitsN.bits(127,64) x,i), BitsN.>>+(BitsN.bits(63,0) x,i)),dst) end; fun dfn'PSRLW_imm (dst,imm) = let val dst = xmm_reg dst val x = XMM dst val i = BitsN.toNat imm in write'XMM (BitsN.concat [BitsN.>>+(BitsN.bits(127,112) x,i), BitsN.>>+(BitsN.bits(111,96) x,i), BitsN.>>+(BitsN.bits(95,80) x,i), BitsN.>>+(BitsN.bits(79,64) x,i), BitsN.>>+(BitsN.bits(63,48) x,i), BitsN.>>+(BitsN.bits(47,32) x,i), BitsN.>>+(BitsN.bits(31,16) x,i),BitsN.>>+(BitsN.bits(15,0) x,i)], dst) end; fun dfn'SQRTPD (dst,src) = let val x = XMM src val (f1,r1) = sse_sqrt64(BitsN.bits(127,64) x) val (f2,r2) = sse_sqrt64(BitsN.bits(63,0) x) in ( process_float_flags[f1,f2] ; let val x = xmm_reg dst in write'XMM(BitsN.@@(r1,r2),x) end ) end; fun dfn'SQRTSD (dst,src) = let val x = XMM src val (f,r) = sse_sqrt64(BitsN.bits(63,0) x) in ( process_float_flags[f] ; let val x = xmm_reg dst val w = XMM x in write'XMM(BitsN.bitFieldInsert(63,0) (w,r),x) end ) end; fun dfn'SQRTPS (dst,src) = let val x = XMM src val (f1,r1) = sse_sqrt32(BitsN.bits(127,96) x) val (f2,r2) = sse_sqrt32(BitsN.bits(95,64) x) val (f3,r3) = sse_sqrt32(BitsN.bits(63,32) x) val (f4,r4) = sse_sqrt32(BitsN.bits(31,0) x) in ( process_float_flags[f1,f2,f3,f4] ; let val x = xmm_reg dst in write'XMM(BitsN.concat[r1,r2,r3,r4],x) end ) end; fun dfn'SQRTSS (dst,src) = let val x = XMM src val (f,r) = sse_sqrt32(BitsN.bits(31,0) x) in ( process_float_flags[f] ; let val x = xmm_reg dst val w = XMM x in write'XMM(BitsN.bitFieldInsert(31,0) (w,r),x) end ) end; fun dfn'Zbinop (bop,(size,dst_src)) = let val (ea,(val_dst,val_src)) = read_dest_src_ea(size,dst_src) in write_binop(size,(bop,(val_dst,(val_src,ea)))) end; fun dfn'Zbit_test (bt,(size,dst_src)) = let val ea_src = ea_Zsrc(size,dst_src) val offset = EA ea_src in case dst_src of Zr_rm _ => UD_exception () | Zrm_r(Zr _,_) => bit_test (bt,(ea_Zdest(size,dst_src),BitsN.toNat(modSize(size,offset)))) | Zrm_i(Zr _,_) => bit_test (bt,(ea_Zdest(size,dst_src),BitsN.toNat(modSize(size,offset)))) | Zrm_i(Zm(si,(base,disp)),_) => let val offset = modSize(size,offset) val bit_base = ea_Zrm (Z8 false, Zm(si, (base,BitsN.+(disp,BitsN.sdiv(offset,BitsN.B(0x8,64)))))) in bit_test (bt,(bit_base,BitsN.toNat(BitsN.smod(offset,BitsN.B(0x8,64))))) end | Zrm_r(Zm(si,(base,disp)),_) => let val offset = SignExtension64(offset,size) val bit_base = ea_Zrm (Z8 false, Zm(si, (base,BitsN.+(disp,BitsN.sdiv(offset,BitsN.B(0x8,64)))))) in bit_test (bt,(bit_base,BitsN.toNat(BitsN.smod(offset,BitsN.B(0x8,64))))) end end; fun dfn'Zcall imm_rm = ( x64_push_rip (); jump_to_ea(ea_Zimm_rm imm_rm) ); fun dfn'Zcmpxchg (size,(rm,r)) = let val ea_src = Zea_r(size,r) val ea_acc = Zea_r(size,RAX) val ea_dst = ea_Zrm(size,rm) val val_dst = EA ea_dst val acc = EA ea_src in ( write_binop(size,(Zcmp,(acc,(val_dst,ea_src)))) ; if acc = val_dst then write'EA(EA ea_src,ea_dst) else write'EA(val_dst,ea_acc) ) end; fun dfn'Zdiv (size,rm) = let val w = value_width size val ea_eax = Zea_r(size,RAX) val ea_edx = Zea_r(size,RDX) val ea_rm = ea_Zrm(size,rm) val n = Nat.+(Nat.*(BitsN.toNat(EA ea_edx),w),BitsN.toNat(EA ea_eax)) val d = BitsN.toNat(EA ea_rm) val q = Nat.div(n,d) val r = Nat.mod(n,d) in ( if (d = 0) orelse (Nat.<=(w,q)) then DE_exception () else () ; write'EA(BitsN.fromNat(q,64),ea_eax) ; write'EA(BitsN.fromNat(r,64),ea_edx) ; erase_eflags () ) end; fun dfn'Zidiv (size,rm) = let val w = Nat.toInt(value_width size) val ea_eax = Zea_r(size,RAX) val ea_edx = Zea_r(size,RDX) val ea_rm = ea_Zrm(size,rm) val n = IntInf.+ (IntInf.*(BitsN.toInt(SignExtension64(EA ea_edx,size)),w), Nat.toInt(BitsN.toNat(EA ea_eax))) val d = BitsN.toInt(SignExtension64(EA ea_rm,size)) val q = IntInf.quot(n,d) val r = IntInf.rem(n,d) in ( if (d = 0) orelse ((IntInf.<(q,IntInf.~(IntInf.div(w,2)))) orelse (IntInf.<=(IntInf.div(w,2),q))) then DE_exception () else () ; write'EA(BitsN.fromInt(q,64),ea_eax) ; write'EA(BitsN.fromInt(r,64),ea_edx) ; erase_eflags () ) end; fun dfn'Zjcc (cond,imm) = if read_cond cond then RIP := (BitsN.+((!RIP),imm)) else (); fun dfn'Zjmp rm = RIP := (EA(ea_Zrm(Z64,rm))); fun dfn'Zlea (size,dst_src) = let val ea_src = ea_Zsrc(size,dst_src) val ea_dst = ea_Zdest(size,dst_src) in write'EA(get_ea_address ea_src,ea_dst) end; fun dfn'Zleave () = ( REG := (Map.update ((!REG),Cast.ZregToNat RSP,Map.lookup((!REG),Cast.ZregToNat RBP))) ; x64_pop(Zr RBP) ); fun dfn'Zloop (cond,imm) = let val ecx1 = BitsN.-(Map.lookup((!REG),Cast.ZregToNat RCX),BitsN.B(0x1,64)) in ( REG := (Map.update((!REG),Cast.ZregToNat RCX,ecx1)) ; if (not(ecx1 = (BitsN.B(0x0,64)))) andalso (read_cond cond) then RIP := (BitsN.+((!RIP),imm)) else () ) end; fun dfn'Zmonop (mop,(size,rm)) = let val ea = ea_Zrm(size,rm) in write_monop(size,(mop,(EA ea,ea))) end; fun dfn'Zmov (cond,(size,dst_src)) = if read_cond cond then let val ea_src = ea_Zsrc(size,dst_src) val ea_dst = ea_Zdest(size,dst_src) in write'EA(EA ea_src,ea_dst) end else (); fun dfn'Zmovsx (size1,(dst_src,size2)) = let val x = ea_Zdest(size2,dst_src) in write'EA(SignExtension(EA(ea_Zsrc(size1,dst_src)),(size1,size2)),x) end; fun dfn'Zmovzx (size1,(dst_src,size2)) = let val x = ea_Zdest(size2,dst_src) in write'EA(EA(ea_Zsrc(size1,dst_src)),x) end; fun dfn'Zmul (size,rm) = let val ea_eax = Zea_r(size,RAX) val eax = EA ea_eax val val_src = EA(ea_Zrm(size,rm)) in ( case size of Z8 _ => let val x = Zea_r(Z16,RAX) in write'EA(BitsN.*(eax,val_src),x) end | _ => ( write'EA(BitsN.*(eax,val_src),ea_eax) ; let val ea_edx = Zea_r(size,RDX) in write'EA (BitsN.fromNat (Nat.div (Nat.*(BitsN.toNat eax,BitsN.toNat val_src), value_width size),64),ea_edx) end ) ; erase_eflags () ) end; fun dfn'Zimul (size,rm) = let val ea_eax = Zea_r(size,RAX) val eax = SignExtension64(EA ea_eax,size) val val_src = SignExtension64(EA(ea_Zrm(size,rm)),size) val product = IntInf.*(BitsN.toInt eax,BitsN.toInt val_src) val product64 = BitsN.fromInt(product,64) in ( erase_eflags () ; let val overflow = not(if size = Z64 then (BitsN.toInt product64) = product else (SignExtension64(product64,size)) = product64) in ( write'CF overflow ; write'OF overflow ; case size of Z8 _ => let val x = Zea_r(Z16,RAX) in write'EA(product64,x) end | _ => ( write'EA(product64,ea_eax) ; let val ea_edx = Zea_r(size,RDX) in write'EA (BitsN.fromInt (IntInf.div(product,Nat.toInt(value_width size)),64), ea_edx) end ) ) end ) end; fun dfn'Zimul2 (size,(r,rm)) = let val ea_dst = Zea_r(size,r) val val_dst = SignExtension64(EA ea_dst,size) val val_src = SignExtension64(EA(ea_Zrm(size,rm)),size) val product = IntInf.*(BitsN.toInt val_dst,BitsN.toInt val_src) val product64 = BitsN.fromInt(product,64) in ( erase_eflags () ; let val overflow = not(if size = Z64 then (BitsN.toInt product64) = product else (SignExtension64(product64,size)) = product64) in ( write'CF overflow ; write'OF overflow ; write'EA(product64,ea_dst) ) end ) end; fun dfn'Zimul3 (size,(r,(rm,imm))) = let val val_src = SignExtension64(EA(ea_Zrm(size,rm)),size) val product = IntInf.*(BitsN.toInt val_src,BitsN.toInt imm) val product64 = BitsN.fromInt(product,64) in ( erase_eflags () ; let val overflow = not(if size = Z64 then (BitsN.toInt product64) = product else (SignExtension64(product64,size)) = product64) in ( write'CF overflow ; write'OF overflow ; let val x = Zea_r(size,r) in write'EA(product64,x) end ) end ) end; fun dfn'Znop n = (); fun dfn'Zpop rm = x64_pop rm; fun dfn'Zpush imm_rm = x64_push imm_rm; fun dfn'Zret imm = ( x64_pop_rip (); x64_drop imm ); fun dfn'Zset (cond,(have_rex,rm)) = let val x = ea_Zrm(Z8 have_rex,rm) in write'EA(BitsN.fromBool 64 (read_cond cond),x) end; fun dfn'Zxadd (size,(rm,r)) = let val ea_src = Zea_r(size,r) val ea_dst = ea_Zrm(size,rm) val val_src = EA ea_src val val_dst = EA ea_dst in ( write'EA(val_dst,ea_src) ; write_binop(size,(Zadd,(val_src,(val_dst,ea_dst)))) ) end; fun dfn'Zxchg (size,(rm,r)) = let val ea_src = Zea_r(size,r) val ea_dst = ea_Zrm(size,rm) val val_src = EA ea_src val val_dst = EA ea_dst in ( write'EA(val_dst,ea_src); write'EA(val_src,ea_dst) ) end; fun dfn'Zcmc () = write'CF(not(CF ())); fun dfn'Zclc () = write'CF false; fun dfn'Zstc () = write'CF true; fun Run v0 = case v0 of Zclc => dfn'Zclc () | Zcmc => dfn'Zcmc () | Zleave => dfn'Zleave () | Zstc => dfn'Zstc () | Zbinop v47 => dfn'Zbinop v47 | Zbit_test v48 => dfn'Zbit_test v48 | Zcall v49 => dfn'Zcall v49 | Zcmpxchg v50 => dfn'Zcmpxchg v50 | Zdiv v51 => dfn'Zdiv v51 | Zidiv v52 => dfn'Zidiv v52 | Zimul v53 => dfn'Zimul v53 | Zimul2 v54 => dfn'Zimul2 v54 | Zimul3 v55 => dfn'Zimul3 v55 | Zjcc v56 => dfn'Zjcc v56 | Zjmp v57 => dfn'Zjmp v57 | Zlea v58 => dfn'Zlea v58 | Zloop v59 => dfn'Zloop v59 | Zmonop v60 => dfn'Zmonop v60 | Zmov v61 => dfn'Zmov v61 | Zmovsx v62 => dfn'Zmovsx v62 | Zmovzx v63 => dfn'Zmovzx v63 | Zmul v64 => dfn'Zmul v64 | Znop v65 => dfn'Znop v65 | Zpop v66 => dfn'Zpop v66 | Zpush v67 => dfn'Zpush v67 | Zret v68 => dfn'Zret v68 | Zset v69 => dfn'Zset v69 | Zxadd v70 => dfn'Zxadd v70 | Zxchg v71 => dfn'Zxchg v71 | SSE v1 => (case v1 of CMPPD v2 => dfn'CMPPD v2 | CMPPS v3 => dfn'CMPPS v3 | CMPSD v4 => dfn'CMPSD v4 | CMPSS v5 => dfn'CMPSS v5 | COMISD v6 => dfn'COMISD v6 | COMISS v7 => dfn'COMISS v7 | CVTDQ2PD v8 => dfn'CVTDQ2PD v8 | CVTDQ2PS v9 => dfn'CVTDQ2PS v9 | CVTPD2DQ v10 => dfn'CVTPD2DQ v10 | CVTPD2PS v11 => dfn'CVTPD2PS v11 | CVTPS2DQ v12 => dfn'CVTPS2DQ v12 | CVTPS2PD v13 => dfn'CVTPS2PD v13 | CVTSD2SI v14 => dfn'CVTSD2SI v14 | CVTSD2SS v15 => dfn'CVTSD2SS v15 | CVTSI2SD v16 => dfn'CVTSI2SD v16 | CVTSI2SS v17 => dfn'CVTSI2SS v17 | CVTSS2SD v18 => dfn'CVTSS2SD v18 | CVTSS2SI v19 => dfn'CVTSS2SI v19 | MOVAP_D_S v20 => dfn'MOVAP_D_S v20 | MOVQ v21 => dfn'MOVQ v21 | MOVSD v22 => dfn'MOVSD v22 | MOVSS v23 => dfn'MOVSS v23 | MOVUP_D_S v24 => dfn'MOVUP_D_S v24 | MOV_D_Q v25 => dfn'MOV_D_Q v25 | PCMPEQQ v26 => dfn'PCMPEQQ v26 | PSLLDQ v27 => dfn'PSLLDQ v27 | PSLLD_imm v28 => dfn'PSLLD_imm v28 | PSLLQ_imm v29 => dfn'PSLLQ_imm v29 | PSLLW_imm v30 => dfn'PSLLW_imm v30 | PSRAD_imm v31 => dfn'PSRAD_imm v31 | PSRAW_imm v32 => dfn'PSRAW_imm v32 | PSRLDQ v33 => dfn'PSRLDQ v33 | PSRLD_imm v34 => dfn'PSRLD_imm v34 | PSRLQ_imm v35 => dfn'PSRLQ_imm v35 | PSRLW_imm v36 => dfn'PSRLW_imm v36 | SQRTPD v37 => dfn'SQRTPD v37 | SQRTPS v38 => dfn'SQRTPS v38 | SQRTSD v39 => dfn'SQRTSD v39 | SQRTSS v40 => dfn'SQRTSS v40 | bin_PD v41 => dfn'bin_PD v41 | bin_PS v42 => dfn'bin_PS v42 | bin_SD v43 => dfn'bin_SD v43 | bin_SS v44 => dfn'bin_SS v44 | logic_PD v45 => dfn'logic_PD v45 | logic_PS v46 => dfn'logic_PS v46); fun oimmediate8 strm = case strm of Option.SOME(b :: t) => (BitsN.signExtend 64 b,Option.SOME t) | _ => (BitsN.B(0x0,64),NONE); fun immediate8 strm = oimmediate8(Option.SOME strm); fun immediate16 strm = case strm of b1 :: (b2 :: t) => (BitsN.signExtend 64 (BitsN.@@(b2,b1)),Option.SOME t) | _ => (BitsN.B(0x0,64),NONE); fun immediate32 strm = case strm of b1 :: (b2 :: (b3 :: (b4 :: t))) => (BitsN.signExtend 64 (BitsN.concat[b4,b3,b2,b1]),Option.SOME t) | _ => (BitsN.B(0x0,64),NONE); fun immediate64 strm = case strm of b1 :: (b2 :: (b3 :: (b4 :: (b5 :: (b6 :: (b7 :: (b8 :: t))))))) => (BitsN.concat[b8,b7,b6,b5,b4,b3,b2,b1],Option.SOME t) | _ => (BitsN.B(0x0,64),NONE); fun immediate (size,strm) = case size of Z8 _ => immediate8 strm | Z16 => immediate16 strm | _ => immediate32 strm; fun oimmediate (size,strm) = case strm of Option.SOME s => immediate(size,s) | NONE => (BitsN.B(0x0,64),NONE); fun full_immediate (size,strm) = if size = Z64 then immediate64 strm else immediate(size,strm); fun rec'REX x = {B = BitsN.bit(x,0), R = BitsN.bit(x,2), W = BitsN.bit(x,3), X = BitsN.bit(x,1)}; fun reg'REX x = case x of {B = B, R = R, W = W, X = X} => BitsN.concat [BitsN.fromBit W,BitsN.fromBit R,BitsN.fromBit X,BitsN.fromBit B]; fun write'rec'REX (_,x) = reg'REX x; fun write'reg'REX (_,x) = rec'REX x; fun RexReg (b,r) = (Cast.natToZreg o BitsN.toNat) (BitsN.@@(BitsN.fromBit b,r)); fun readDisplacement (Mod,strm) = if Mod = (BitsN.B(0x1,2)) then immediate8 strm else if Mod = (BitsN.B(0x2,2)) then immediate32 strm else (BitsN.B(0x0,64),Option.SOME strm); fun readSibDisplacement (Mod,strm) = if Mod = (BitsN.B(0x1,2)) then immediate8 strm else immediate32 strm; fun readSIB (REX,(Mod,strm)) = case strm of v'0 :: v'1 => (case (boolify'8 v'0,v'1) of ((SS'1, (SS'0,(Index'2,(Index'1,(Index'0,(Base'2,(Base'1,Base'0))))))), strm1) => let val base = RexReg (#B(REX : REX), BitsN.fromBitstring([Base'2,Base'1,Base'0],3)) val index = RexReg (#X(REX : REX), BitsN.fromBitstring([Index'2,Index'1,Index'0],3)) val scaled_index = if index = RSP then NONE else Option.SOME (BitsN.fromBitstring([SS'1,SS'0],2),index) in if base = RBP then let val (displacement,strm2) = readSibDisplacement(Mod,strm1) val base = if Mod = (BitsN.B(0x0,2)) then ZnoBase else ZregBase base in (Zm(scaled_index,(base,displacement)),strm2) end else let val (displacement,strm2) = readDisplacement(Mod,strm1) in (Zm(scaled_index,(ZregBase base,displacement)),strm2) end end) | _ => (Zm(NONE,(ZnoBase,BitsN.B(0x0,64))),NONE); fun readModRM (REX,strm) = case strm of v'0 :: v'1 => (case (boolify'8 v'0,v'1) of ((false, (false,(RegOpc'2,(RegOpc'1,(RegOpc'0,(true,(false,true))))))), strm1) => let val (displacement,strm2) = immediate32 strm1 in (RexReg (#R(REX : REX), BitsN.fromBitstring([RegOpc'2,RegOpc'1,RegOpc'0],3)), (Zm(NONE,(ZripBase,displacement)),strm2)) end | ((true,(true,(REG'2,(REG'1,(REG'0,(RM'2,(RM'1,RM'0))))))),strm1) => (RexReg (#R(REX : REX),BitsN.fromBitstring([REG'2,REG'1,REG'0],3)), (Zr(RexReg (#B(REX : REX),BitsN.fromBitstring([RM'2,RM'1,RM'0],3))), Option.SOME strm1)) | ((Mod'1, (Mod'0,(RegOpc'2,(RegOpc'1,(RegOpc'0,(true,(false,false))))))), strm1) => let val (sib,strm2) = readSIB(REX,(BitsN.fromBitstring([Mod'1,Mod'0],2),strm1)) in (RexReg (#R(REX : REX), BitsN.fromBitstring([RegOpc'2,RegOpc'1,RegOpc'0],3)), (sib,strm2)) end | ((Mod'1, (Mod'0,(RegOpc'2,(RegOpc'1,(RegOpc'0,(RM'2,(RM'1,RM'0))))))), strm1) => let val (displacement,strm2) = readDisplacement (BitsN.fromBitstring([Mod'1,Mod'0],2),strm1) in (RexReg (#R(REX : REX), BitsN.fromBitstring([RegOpc'2,RegOpc'1,RegOpc'0],3)), (Zm(NONE, (ZregBase (RexReg (#B(REX : REX), BitsN.fromBitstring([RM'2,RM'1,RM'0],3))), displacement)),strm2)) end) | _ => (RAX,(Zm(NONE,(ZnoBase,BitsN.B(0x0,64))),NONE)); fun readOpcodeModRM (REX,strm) = let val (opcode,(rm,strm1)) = readModRM(REX,strm) in (BitsN.fromNat(Nat.mod(Cast.ZregToNat opcode,8),3),(rm,strm1)) end; fun prefixGroup b = case b of BitsN.B(0xF0,_) => 1 | BitsN.B(0xF2,_) => 1 | BitsN.B(0xF3,_) => 1 | BitsN.B(0x26,_) => 2 | BitsN.B(0x2E,_) => 2 | BitsN.B(0x36,_) => 2 | BitsN.B(0x3E,_) => 2 | BitsN.B(0x64,_) => 2 | BitsN.B(0x65,_) => 2 | BitsN.B(0x66,_) => 3 | BitsN.B(0x67,_) => 4 | _ => (if (BitsN.bits(7,4) b) = (BitsN.B(0x4,4)) then 5 else 0); fun readPrefix (s,(p,strm)) = case strm of h :: strm1 => let val group = prefixGroup h in if group = 0 then Option.SOME(p,(false,(rec'REX(BitsN.B(0x0,4)),strm))) else if group = 5 then Option.SOME(p,(true,(rec'REX(BitsN.bits(3,0) h),strm1))) else if Set.mem(group,s) then NONE else readPrefix(Set.insert(group,s),(h :: p,strm1)) end | [] => Option.SOME (p,(false,({B = false, R = false, W = false, X = false},strm))); fun readPrefixes strm = readPrefix([],([],strm)); fun OpSize (have_rex,(w,(v,override))) = if v = (BitsN.B(0x0,1)) then Z8 have_rex else if w then Z64 else if override then Z16 else Z32; fun isZm rm = case rm of Zm _ => true | _ => false; fun x64_decode strm = case readPrefixes strm of NONE => Zdec_fail "Bad prefix" | Option.SOME(p,(have_rex,(REX,strm1))) => let val prefixes = Set.mk p val op_size_override = Set.mem(BitsN.B(0x66,8),prefixes) in if Set.mem(BitsN.B(0x67,8),prefixes) then Zdec_fail "address override prefix not supported" else case strm1 of v'0 :: v'1 => (case (boolify'8 v'0,v'1) of ((false, (false,(opc'2,(opc'1,(opc'0,(false,(x'0,v'0))))))), strm2) => let val (reg,(rm,strm3)) = readModRM(REX,strm2) val size = OpSize (have_rex, (#W(REX : REX), (BitsN.fromBitstring([v'0],1), op_size_override))) val binop = (Cast.natToZbinop_name o BitsN.toNat) (BitsN.fromBitstring([opc'2,opc'1,opc'0],3)) val src_dst = if (BitsN.fromBitstring([x'0],1)) = (BitsN.B(0x0,1)) then Zrm_r(rm,reg) else Zr_rm(reg,rm) in Zfull_inst (p,(Zbinop(binop,(size,src_dst)),strm3)) end | ((false, (false,(opc'2,(opc'1,(opc'0,(true,(false,v'0))))))), strm2) => let val size = OpSize (have_rex, (#W(REX : REX), (BitsN.fromBitstring([v'0],1), op_size_override))) val (imm,strm3) = immediate(size,strm2) in Zfull_inst (p, (Zbinop ((Cast.natToZbinop_name o BitsN.toNat) (BitsN.fromBitstring ([opc'2,opc'1,opc'0],3)), (size,Zrm_i(Zr RAX,imm))),strm3)) end | ((false,(true,(false,(true,(b'0,(r'2,(r'1,r'0))))))), strm2) => let val reg = Zr((Cast.natToZreg o BitsN.toNat) (BitsN.@@ (BitsN.fromBit(#B(REX : REX)), BitsN.fromBitstring([r'2,r'1,r'0],3)))) in Zfull_inst (p, (if (BitsN.fromBitstring([b'0],1)) = (BitsN.B(0x0,1)) then Zpush(Zrm reg) else Zpop reg,Option.SOME strm2)) end | ((false, (true,(true,(false,(false,(false,(true,true))))))), strm2) => let val (reg,(rm,strm3)) = readModRM(REX,strm2) in Zfull_inst (p,(Zmovsx(Z32,(Zr_rm(reg,rm),Z64)),strm3)) end | ((false, (true,(true,(false,(true,(false,(b'0,false))))))), strm2) => let val (imm,strm3) = if (BitsN.fromBitstring([b'0],1)) = (BitsN.B(0x1,1)) then immediate8 strm2 else immediate32 strm2 in Zfull_inst(p,(Zpush(Zimm imm),strm3)) end | ((false, (true,(true,(false,(true,(false,(b'0,true))))))), strm2) => let val size = OpSize (have_rex, (#W(REX : REX), (BitsN.B(0x1,1),op_size_override))) val (reg,(rm,strm3)) = readModRM(REX,strm2) in case strm3 of NONE => Zdec_fail "not enough bytes" | Option.SOME s => let val (imm,strm4) = if (BitsN.fromBitstring([b'0],1)) = (BitsN.B(0x1,1)) then immediate8 s else immediate32 s in Zfull_inst (p,(Zimul3(size,(reg,(rm,imm))),strm4)) end end | ((false,(true,(true,(true,(c'3,(c'2,(c'1,c'0))))))), strm2) => let val (imm,strm3) = immediate8 strm2 in Zfull_inst (p, (Zjcc ((Cast.natToZcond o BitsN.toNat) (BitsN.fromBitstring([c'3,c'2,c'1,c'0],4)), imm),strm3)) end | ((true, (false,(false,(false,(false,(false,(false,v'0))))))), strm2) => let val size = OpSize (have_rex, (#W(REX : REX), (BitsN.fromBitstring([v'0],1), op_size_override))) val (opcode,(rm,strm3)) = readOpcodeModRM(REX,strm2) val (imm,strm4) = oimmediate(size,strm3) val binop = (Cast.natToZbinop_name o BitsN.toNat) opcode in Zfull_inst (p,(Zbinop(binop,(size,Zrm_i(rm,imm))),strm4)) end | ((true, (false,(false,(false,(false,(false,(true,true))))))), strm2) => let val size = OpSize (false, (#W(REX : REX), (BitsN.B(0x1,1),op_size_override))) val (opcode,(rm,strm3)) = readOpcodeModRM(REX,strm2) val (imm,strm4) = oimmediate8 strm3 val binop = (Cast.natToZbinop_name o BitsN.toNat) opcode in Zfull_inst (p,(Zbinop(binop,(size,Zrm_i(rm,imm))),strm4)) end | ((true, (false,(false,(false,(false,(true,(false,v'0))))))), strm2) => let val size = OpSize (have_rex, (#W(REX : REX), (BitsN.fromBitstring([v'0],1), op_size_override))) val (reg,(rm,strm3)) = readModRM(REX,strm2) in Zfull_inst (p,(Zbinop(Ztest,(size,Zrm_r(rm,reg))),strm3)) end | ((true, (false,(false,(false,(false,(true,(true,v'0))))))), strm2) => let val size = OpSize (have_rex, (#W(REX : REX), (BitsN.fromBitstring([v'0],1), op_size_override))) val (reg,(rm,strm3)) = readModRM(REX,strm2) in Zfull_inst(p,(Zxchg(size,(rm,reg)),strm3)) end | ((true, (false,(false,(false,(true,(false,(x'0,v'0))))))), strm2) => let val (reg,(rm,strm3)) = readModRM(REX,strm2) val size = OpSize (have_rex, (#W(REX : REX), (BitsN.fromBitstring([v'0],1), op_size_override))) val src_dst = if (BitsN.fromBitstring([x'0],1)) = (BitsN.B(0x0,1)) then Zrm_r(rm,reg) else Zr_rm(reg,rm) in Zfull_inst(p,(Zmov(Z_ALWAYS,(size,src_dst)),strm3)) end | ((true, (false,(false,(false,(true,(true,(false,true))))))), strm2) => let val size = OpSize (true, (#W(REX : REX), (BitsN.B(0x1,1),op_size_override))) val (reg,(rm,strm3)) = readModRM(REX,strm2) in if isZm rm then Zfull_inst (p,(Zlea(size,Zr_rm(reg,rm)),strm3)) else Zdec_fail "LEA with register argument" end | ((true, (false,(false,(false,(true,(true,(true,true))))))), strm2) => let val (opcode,(rm,strm3)) = readOpcodeModRM(REX,strm2) in if opcode = (BitsN.B(0x0,3)) then Zfull_inst(p,(Zpop rm,strm3)) else Zdec_fail "Unsupported opcode: Group 1a" end | ((true,(false,(false,(true,(false,(r'2,(r'1,r'0))))))), strm2) => let val size = OpSize (true, (#W(REX : REX), (BitsN.B(0x1,1),op_size_override))) val reg = RexReg (#B(REX : REX), BitsN.fromBitstring([r'2,r'1,r'0],3)) in if reg = RAX then Zfull_inst (p, (Znop(L3.length strm),Option.SOME strm2)) else Zfull_inst (p, (Zxchg(size,(Zr RAX,reg)),Option.SOME strm2)) end | ((true, (false,(true,(false,(true,(false,(false,v'0))))))), strm2) => let val size = OpSize (true, (#W(REX : REX), (BitsN.fromBitstring([v'0],1), op_size_override))) val (imm,strm3) = immediate(size,strm2) in Zfull_inst (p,(Zbinop(Ztest,(size,Zrm_i(Zr RAX,imm))),strm3)) end | ((true,(false,(true,(true,(v'0,(r'2,(r'1,r'0))))))), strm2) => let val size = OpSize (have_rex, (#W(REX : REX), (BitsN.fromBitstring([v'0],1), op_size_override))) val (imm,strm3) = full_immediate(size,strm2) val reg = RexReg (#B(REX : REX), BitsN.fromBitstring([r'2,r'1,r'0],3)) in Zfull_inst (p, (Zmov(Z_ALWAYS,(size,Zrm_i(Zr reg,imm))),strm3)) end | ((true, (true,(false,(false,(false,(false,(false,v'0))))))), strm2) => let val size = OpSize (have_rex, (#W(REX : REX), (BitsN.fromBitstring([v'0],1), op_size_override))) val (opcode,(rm,strm3)) = readOpcodeModRM(REX,strm2) val (imm,strm4) = oimmediate8 strm3 val binop = Cast.natToZbinop_name (Nat.+(BitsN.toNat opcode,8)) in if opcode = (BitsN.B(0x6,3)) then Zdec_fail "Unsupported opcode: Shift Group 2" else Zfull_inst (p, (Zbinop(binop,(size,Zrm_i(rm,imm))),strm4)) end | ((true, (true,(false,(false,(false,(false,(true,v'0))))))), strm2) => (if (BitsN.fromBitstring([v'0],1)) = (BitsN.B(0x0,1)) then let val (imm,strm3) = immediate16 strm2 in Zfull_inst(p,(Zret imm,strm3)) end else Zfull_inst (p,(Zret(BitsN.B(0x0,64)),Option.SOME strm2))) | ((true, (true,(false,(false,(false,(true,(true,v'0))))))), strm2) => let val size = OpSize (have_rex, (#W(REX : REX), (BitsN.fromBitstring([v'0],1), op_size_override))) val (opcode,(rm,strm3)) = readOpcodeModRM(REX,strm2) val (imm,strm4) = oimmediate(size,strm3) in if opcode = (BitsN.B(0x0,3)) then Zfull_inst (p, (Zmov(Z_ALWAYS,(size,Zrm_i(rm,imm))), strm4)) else Zdec_fail "Unsupported opcode: Group 11" end | ((true, (true,(false,(false,(true,(false,(false,true))))))), strm2) => Zfull_inst(p,(Zleave,Option.SOME strm2)) | ((true, (true,(false,(true,(false,(false,(b'0,v'0))))))), strm2) => let val size = OpSize (have_rex, (#W(REX : REX), (BitsN.fromBitstring([v'0],1), op_size_override))) val (opcode,(rm,strm3)) = readOpcodeModRM(REX,strm2) val shift = if (BitsN.fromBitstring([b'0],1)) = (BitsN.B(0x0,1)) then Zrm_i(rm,BitsN.B(0x1,64)) else Zrm_r(rm,RCX) val binop = Cast.natToZbinop_name (Nat.+(BitsN.toNat opcode,8)) in if opcode = (BitsN.B(0x6,3)) then Zdec_fail "Unsupported opcode: Shift Group 2" else Zfull_inst (p,(Zbinop(binop,(size,shift)),strm3)) end | ((true, (true,(true,(false,(false,(false,(false,b'0))))))), strm2) => let val (imm,strm3) = immediate8 strm2 val cond = if (BitsN.fromBitstring([b'0],1)) = (BitsN.B(0x0,1)) then Z_NE else Z_E in Zfull_inst(p,(Zloop(cond,imm),strm3)) end | ((true, (true,(true,(false,(false,(false,(true,false))))))), strm2) => let val (imm,strm3) = immediate8 strm2 in Zfull_inst(p,(Zloop(Z_ALWAYS,imm),strm3)) end | ((true, (true,(true,(false,(true,(false,(false,false))))))), strm2) => let val (imm,strm3) = immediate32 strm2 in Zfull_inst(p,(Zcall(Zimm imm),strm3)) end | ((true, (true,(true,(false,(true,(false,(b'0,true))))))), strm2) => let val (imm,strm3) = if (BitsN.fromBitstring([b'0],1)) = (BitsN.B(0x0,1)) then immediate32 strm2 else immediate8 strm2 in Zfull_inst(p,(Zjcc(Z_ALWAYS,imm),strm3)) end | ((true, (true,(true,(true,(false,(true,(false,true))))))), strm2) => Zfull_inst(p,(Zcmc,Option.SOME strm2)) | ((true,(true,(true,(true,(false,(true,(true,v'0))))))), strm2) => let val size = OpSize (have_rex, (#W(REX : REX), (BitsN.fromBitstring([v'0],1), op_size_override))) val (opcode,(rm,strm3)) = readOpcodeModRM(REX,strm2) in case opcode of BitsN.B(0x0,_) => let val (imm,strm4) = oimmediate(size,strm3) in Zfull_inst (p, (Zbinop(Ztest,(size,Zrm_i(rm,imm))),strm4)) end | BitsN.B(0x2,_) => Zfull_inst(p,(Zmonop(Znot,(size,rm)),strm3)) | BitsN.B(0x3,_) => Zfull_inst(p,(Zmonop(Zneg,(size,rm)),strm3)) | BitsN.B(0x4,_) => Zfull_inst(p,(Zmul(size,rm),strm3)) | BitsN.B(0x5,_) => Zfull_inst(p,(Zimul(size,rm),strm3)) | BitsN.B(0x6,_) => Zfull_inst(p,(Zdiv(size,rm),strm3)) | BitsN.B(0x7,_) => Zfull_inst(p,(Zidiv(size,rm),strm3)) | _ => Zdec_fail "Unsupported opcode: Unary Group 3" end | ((true, (true,(true,(true,(true,(false,(false,false))))))), strm2) => Zfull_inst(p,(Zclc,Option.SOME strm2)) | ((true, (true,(true,(true,(true,(false,(false,true))))))), strm2) => Zfull_inst(p,(Zstc,Option.SOME strm2)) | ((true, (true,(true,(true,(true,(true,(true,false))))))), strm2) => let val (opcode,(rm,strm3)) = readOpcodeModRM(REX,strm2) in if opcode = (BitsN.B(0x0,3)) then Zfull_inst (p,(Zmonop(Zinc,(Z8 have_rex,rm)),strm3)) else if opcode = (BitsN.B(0x1,3)) then Zfull_inst (p,(Zmonop(Zdec,(Z8 have_rex,rm)),strm3)) else Zdec_fail "Unsupported opcode: INC/DEC Group 4" end | ((true,(true,(true,(true,(true,(true,(true,true))))))), strm2) => let val size = OpSize (have_rex, (#W(REX : REX), (BitsN.B(0x1,1),op_size_override))) val (opcode,(rm,strm3)) = readOpcodeModRM(REX,strm2) in case opcode of BitsN.B(0x0,_) => Zfull_inst(p,(Zmonop(Zinc,(size,rm)),strm3)) | BitsN.B(0x1,_) => Zfull_inst(p,(Zmonop(Zdec,(size,rm)),strm3)) | BitsN.B(0x2,_) => Zfull_inst(p,(Zcall(Zrm rm),strm3)) | BitsN.B(0x4,_) => Zfull_inst(p,(Zjmp rm,strm3)) | BitsN.B(0x6,_) => Zfull_inst(p,(Zpush(Zrm rm),strm3)) | _ => Zdec_fail "Unsupported opcode: INC/DEC Group 5" end | ((false, (false,(false,(false,(true,(true,(true,true))))))), (BitsN.B(0x38,_)) :: (opc :: strm2)) => (case opc of BitsN.B(0x29,_) => if p = [BitsN.B(0x66,8)] then let val (reg,(rm,strm3)) = readOpcodeModRM(REX,strm2) val a = (reg,rm_to_xmm_mem rm) in Zfull_inst(p,(SSE(PCMPEQQ a),strm3)) end else Zdec_fail ("Unsupported opcode: 0F 38 " ^ (BitsN.toHexString opc)) | _ => Zdec_fail ("Unsupported opcode: 0F 38 " ^ (BitsN.toHexString opc))) | ((false, (false,(false,(false,(true,(true,(true,true))))))), (BitsN.B(0x3A,_)) :: (opc :: _)) => Zdec_fail ("Unsupported opcode: 0F 3A " ^ (BitsN.toHexString opc)) | ((false, (false,(false,(false,(true,(true,(true,true))))))), opc :: strm2) => (case boolify'8 opc of (false, (false, (false,(true,(false,(false,(false,false))))))) => let val (reg,(rm,strm3)) = readOpcodeModRM(REX,strm2) val a = (xmm_reg reg,rm_to_xmm_mem rm) in case p of [BitsN.B(0x66,_)] => Zfull_inst (p,(SSE(MOVUP_D_S(true,a)),strm3)) | [BitsN.B(0xF2,_)] => Zfull_inst(p,(SSE(MOVSD a),strm3)) | [BitsN.B(0xF3,_)] => Zfull_inst(p,(SSE(MOVSS a),strm3)) | _ => Zfull_inst (p,(SSE(MOVUP_D_S(false,a)),strm3)) end | (false, (false,(false,(true,(false,(false,(false,true))))))) => let val (reg,(rm,strm3)) = readOpcodeModRM(REX,strm2) val a = (rm_to_xmm_mem rm,xmm_reg reg) in case p of [BitsN.B(0x66,_)] => Zfull_inst (p,(SSE(MOVUP_D_S(true,a)),strm3)) | [BitsN.B(0xF2,_)] => Zfull_inst(p,(SSE(MOVSD a),strm3)) | [BitsN.B(0xF3,_)] => Zfull_inst(p,(SSE(MOVSS a),strm3)) | _ => Zfull_inst (p,(SSE(MOVUP_D_S(false,a)),strm3)) end | (false, (false,(false,(true,(true,(true,(true,true))))))) => let val (_,(_,strm3)) = readOpcodeModRM(REX,strm2) in Zfull_inst(p,(Znop(L3.length strm),strm3)) end | (false, (false,(true,(false,(true,(false,(false,false))))))) => let val (reg,(rm,strm3)) = readOpcodeModRM(REX,strm2) val double = p = [BitsN.B(0x66,8)] in Zfull_inst (p, (SSE(MOVAP_D_S (double, (xmm_reg reg,rm_to_xmm_mem rm))), strm3)) end | (false, (false,(true,(false,(true,(false,(false,true))))))) => let val (reg,(rm,strm3)) = readOpcodeModRM(REX,strm2) val double = p = [BitsN.B(0x66,8)] in Zfull_inst (p, (SSE(MOVAP_D_S (double, (rm_to_xmm_mem rm,xmm_reg reg))), strm3)) end | (false, (false,(true,(false,(true,(false,(true,false))))))) => let val (reg,(rm,strm3)) = readOpcodeModRM(REX,strm2) val a = (#W(REX : REX),(reg,rm)) in case p of [BitsN.B(0xF3,_)] => Zfull_inst(p,(SSE(CVTSI2SS a),strm3)) | [BitsN.B(0xF2,_)] => Zfull_inst(p,(SSE(CVTSI2SD a),strm3)) | _ => Zdec_fail ("Unsupported opcode: 0F " ^ (BitsN.toHexString opc)) end | (false, (false,(true,(false,(true,(true,(false,b'0))))))) => let val (reg,(rm,strm3)) = readModRM(REX,strm2) val a = (not((not o L3.equal (BitsN.zero (1))) (BitsN.fromBitstring([b'0],1))), (#W(REX : REX),(reg,rm_to_xmm_mem rm))) in case p of [BitsN.B(0xF3,_)] => Zfull_inst(p,(SSE(CVTSS2SI a),strm3)) | [BitsN.B(0xF2,_)] => Zfull_inst(p,(SSE(CVTSD2SI a),strm3)) | _ => Zdec_fail ("Unsupported opcode: 0F " ^ (BitsN.toHexString opc)) end | (false, (false,(true,(false,(true,(true,(true,true))))))) => let val (reg,(rm,strm3)) = readOpcodeModRM(REX,strm2) val a = (reg,rm_to_xmm_mem rm) in case p of [BitsN.B(0x66,_)] => Zfull_inst(p,(SSE(COMISD a),strm3)) | _ => Zfull_inst(p,(SSE(COMISS a),strm3)) end | (false, (true,(false,(false,(c'3,(c'2,(c'1,c'0))))))) => let val size = OpSize (true, (#W(REX : REX), (BitsN.B(0x1,1),op_size_override))) val (reg,(rm,strm3)) = readModRM(REX,strm2) in Zfull_inst (p, (Zmov ((Cast.natToZcond o BitsN.toNat) (BitsN.fromBitstring ([c'3,c'2,c'1,c'0],4)), (size,Zr_rm(reg,rm))),strm3)) end | (false, (true,(false,(true,(false,(false,(false,true))))))) => let val (reg,(rm,strm3)) = readOpcodeModRM(REX,strm2) val a = (reg,rm_to_xmm_mem rm) in case p of [BitsN.B(0x66,_)] => Zfull_inst(p,(SSE(SQRTPD a),strm3)) | [BitsN.B(0xF3,_)] => Zfull_inst(p,(SSE(SQRTSS a),strm3)) | [BitsN.B(0xF2,_)] => Zfull_inst(p,(SSE(SQRTSD a),strm3)) | _ => Zfull_inst(p,(SSE(SQRTPS a),strm3)) end | (false, (true,(false,(true,(false,(true,(c'1,c'0))))))) => let val (reg,(rm,strm3)) = readOpcodeModRM(REX,strm2) val a = ((Cast.natTosse_logic o BitsN.toNat) (BitsN.fromBitstring([c'1,c'0],2)), (reg,rm_to_xmm_mem rm)) in case p of [BitsN.B(0x66,_)] => Zfull_inst(p,(SSE(logic_PD a),strm3)) | _ => Zfull_inst(p,(SSE(logic_PS a),strm3)) end | (false, (true,(false,(true,(true,(c'2,(c'1,c'0))))))) => let val (reg,(rm,strm3)) = readOpcodeModRM(REX,strm2) val a = (reg,rm_to_xmm_mem rm) in case (BitsN.fromBitstring([c'2,c'1,c'0],3),p) of (BitsN.B(0x0,_),[BitsN.B(0x66,_)]) => Zfull_inst (p,(SSE(bin_PD(sse_add,a)),strm3)) | (BitsN.B(0x0,_),[BitsN.B(0xF3,_)]) => Zfull_inst(p,(SSE(bin_SS(sse_add,a)),strm3)) | (BitsN.B(0x0,_),[BitsN.B(0xF2,_)]) => Zfull_inst(p,(SSE(bin_SD(sse_add,a)),strm3)) | (BitsN.B(0x0,_),_) => Zfull_inst(p,(SSE(bin_PS(sse_add,a)),strm3)) | (BitsN.B(0x1,_),[BitsN.B(0x66,_)]) => Zfull_inst(p,(SSE(bin_PD(sse_mul,a)),strm3)) | (BitsN.B(0x1,_),[BitsN.B(0xF3,_)]) => Zfull_inst(p,(SSE(bin_SS(sse_mul,a)),strm3)) | (BitsN.B(0x1,_),[BitsN.B(0xF2,_)]) => Zfull_inst(p,(SSE(bin_SD(sse_mul,a)),strm3)) | (BitsN.B(0x1,_),_) => Zfull_inst(p,(SSE(bin_PS(sse_mul,a)),strm3)) | (BitsN.B(0x2,_),[BitsN.B(0x66,_)]) => Zfull_inst(p,(SSE(CVTPD2PS a),strm3)) | (BitsN.B(0x2,_),[BitsN.B(0xF3,_)]) => Zfull_inst(p,(SSE(CVTSS2SD a),strm3)) | (BitsN.B(0x2,_),[BitsN.B(0xF2,_)]) => Zfull_inst(p,(SSE(CVTSD2SS a),strm3)) | (BitsN.B(0x2,_),_) => Zfull_inst(p,(SSE(CVTPS2PD a),strm3)) | (BitsN.B(0x3,_),[BitsN.B(0x66,_)]) => Zfull_inst(p,(SSE(CVTPS2DQ(false,a)),strm3)) | (BitsN.B(0x3,_),[BitsN.B(0xF3,_)]) => Zfull_inst(p,(SSE(CVTPS2DQ(true,a)),strm3)) | (BitsN.B(0x3,_),[BitsN.B(0xF2,_)]) => Zdec_fail ("Unsupported opcode: 0F " ^ (BitsN.toHexString opc)) | (BitsN.B(0x3,_),_) => Zfull_inst(p,(SSE(CVTDQ2PS a),strm3)) | (BitsN.B(0x4,_),[BitsN.B(0x66,_)]) => Zfull_inst(p,(SSE(bin_PD(sse_sub,a)),strm3)) | (BitsN.B(0x4,_),[BitsN.B(0xF3,_)]) => Zfull_inst(p,(SSE(bin_SS(sse_sub,a)),strm3)) | (BitsN.B(0x4,_),[BitsN.B(0xF2,_)]) => Zfull_inst(p,(SSE(bin_SD(sse_sub,a)),strm3)) | (BitsN.B(0x4,_),_) => Zfull_inst(p,(SSE(bin_PS(sse_sub,a)),strm3)) | (BitsN.B(0x5,_),[BitsN.B(0x66,_)]) => Zfull_inst(p,(SSE(bin_PD(sse_min,a)),strm3)) | (BitsN.B(0x5,_),[BitsN.B(0xF3,_)]) => Zfull_inst(p,(SSE(bin_SS(sse_min,a)),strm3)) | (BitsN.B(0x5,_),[BitsN.B(0xF2,_)]) => Zfull_inst(p,(SSE(bin_SD(sse_min,a)),strm3)) | (BitsN.B(0x5,_),_) => Zfull_inst(p,(SSE(bin_PS(sse_min,a)),strm3)) | (BitsN.B(0x6,_),[BitsN.B(0x66,_)]) => Zfull_inst(p,(SSE(bin_PD(sse_div,a)),strm3)) | (BitsN.B(0x6,_),[BitsN.B(0xF3,_)]) => Zfull_inst(p,(SSE(bin_SS(sse_div,a)),strm3)) | (BitsN.B(0x6,_),[BitsN.B(0xF2,_)]) => Zfull_inst(p,(SSE(bin_SD(sse_div,a)),strm3)) | (BitsN.B(0x6,_),_) => Zfull_inst(p,(SSE(bin_PS(sse_div,a)),strm3)) | (BitsN.B(0x7,_),[BitsN.B(0x66,_)]) => Zfull_inst(p,(SSE(bin_PD(sse_max,a)),strm3)) | (BitsN.B(0x7,_),[BitsN.B(0xF3,_)]) => Zfull_inst(p,(SSE(bin_SS(sse_max,a)),strm3)) | (BitsN.B(0x7,_),[BitsN.B(0xF2,_)]) => Zfull_inst(p,(SSE(bin_SD(sse_max,a)),strm3)) | (BitsN.B(0x7,_),_) => Zfull_inst(p,(SSE(bin_PS(sse_max,a)),strm3)) end | (false, (true,(true,(true,(false,(false,(false,true))))))) => if p = [BitsN.B(0x66,8)] then let val (opcode,(rm,strm3)) = readOpcodeModRM(REX,strm2) val (imm,strm4) = oimmediate8 strm3 in case (opcode,rm) of (BitsN.B(0x2,_),Zr r) => Zfull_inst (p, (SSE(PSRLW_imm (BitsN.fromNat (Cast.ZregToNat r,3), BitsN.fromNat (BitsN.toNat imm,8))), strm4)) | (BitsN.B(0x4,_),Zr r) => Zfull_inst (p, (SSE(PSRAW_imm (BitsN.fromNat (Cast.ZregToNat r,3), BitsN.fromNat (BitsN.toNat imm,8))), strm4)) | (BitsN.B(0x6,_),Zr r) => Zfull_inst (p, (SSE(PSLLW_imm (BitsN.fromNat (Cast.ZregToNat r,3), BitsN.fromNat (BitsN.toNat imm,8))), strm4)) | _ => Zdec_fail "Unsupported group 12 opcode: 0F 71" end else Zdec_fail "Unsupported group 12 opcode: 0F 71" | (false, (true,(true,(true,(false,(false,(true,false))))))) => if p = [BitsN.B(0x66,8)] then let val (opcode,(rm,strm3)) = readOpcodeModRM(REX,strm2) val (imm,strm4) = oimmediate8 strm3 in case (opcode,rm) of (BitsN.B(0x2,_),Zr r) => Zfull_inst (p, (SSE(PSRLD_imm (BitsN.fromNat (Cast.ZregToNat r,3), BitsN.fromNat (BitsN.toNat imm,8))), strm4)) | (BitsN.B(0x4,_),Zr r) => Zfull_inst (p, (SSE(PSRAD_imm (BitsN.fromNat (Cast.ZregToNat r,3), BitsN.fromNat (BitsN.toNat imm,8))), strm4)) | (BitsN.B(0x6,_),Zr r) => Zfull_inst (p, (SSE(PSLLD_imm (BitsN.fromNat (Cast.ZregToNat r,3), BitsN.fromNat (BitsN.toNat imm,8))), strm4)) | _ => Zdec_fail "Unsupported group 13 opcode: 0F 72" end else Zdec_fail "Unsupported group 13 opcode: 0F 71" | (false, (true,(true,(true,(false,(false,(true,true))))))) => if p = [BitsN.B(0x66,8)] then let val (opcode,(rm,strm3)) = readOpcodeModRM(REX,strm2) val (imm,strm4) = oimmediate8 strm3 in case (opcode,rm) of (BitsN.B(0x2,_),Zr r) => Zfull_inst (p, (SSE(PSRLQ_imm (BitsN.fromNat (Cast.ZregToNat r,3), BitsN.fromNat (BitsN.toNat imm,8))), strm4)) | (BitsN.B(0x3,_),Zr r) => Zfull_inst (p, (SSE(PSRLDQ (BitsN.fromNat (Cast.ZregToNat r,3), BitsN.fromNat (BitsN.toNat imm,8))), strm4)) | (BitsN.B(0x6,_),Zr r) => Zfull_inst (p, (SSE(PSLLQ_imm (BitsN.fromNat (Cast.ZregToNat r,3), BitsN.fromNat (BitsN.toNat imm,8))), strm4)) | (BitsN.B(0x7,_),Zr r) => Zfull_inst (p, (SSE(PSLLDQ (BitsN.fromNat (Cast.ZregToNat r,3), BitsN.fromNat (BitsN.toNat imm,8))), strm4)) | _ => Zdec_fail "Unsupported group 14 opcode: 0F 73" end else Zdec_fail "Unsupported group 14 opcode: 0F 71" | (true, (true,(false,(true,(false,(true,(true,false))))))) => let val (reg,(rm,strm3)) = readOpcodeModRM(REX,strm2) val a = (rm_to_xmm_mem rm,xmm_reg reg) in case p of [BitsN.B(0x66,_)] => Zfull_inst(p,(SSE(MOVQ a),strm3)) | _ => Zdec_fail ("Unsupported opcode: 0F " ^ (BitsN.toHexString opc)) end | (false, (true,(true,(b'0,(true,(true,(true,false))))))) => let val b = BitsN.fromBitstring([b'0],1) val (reg,(rm,strm3)) = readOpcodeModRM(REX,strm2) val a = (not((not o L3.equal (BitsN.zero (1))) b), (#W(REX : REX),(reg,rm))) in case p of [BitsN.B(0x66,_)] => Zfull_inst(p,(SSE(MOV_D_Q a),strm3)) | [BitsN.B(0xF3,_)] => if b = (BitsN.B(0x1,1)) then Zfull_inst (p, (SSE(MOVQ (xmm_reg reg, rm_to_xmm_mem rm)),strm3)) else Zdec_fail ("Unsupported opcode: 0F " ^ (BitsN.toHexString opc)) | _ => Zdec_fail ("Unsupported opcode: 0F " ^ (BitsN.toHexString opc)) end | (true, (false,(false,(false,(c'3,(c'2,(c'1,c'0))))))) => let val (imm,strm3) = immediate32 strm2 in Zfull_inst (p, (Zjcc ((Cast.natToZcond o BitsN.toNat) (BitsN.fromBitstring ([c'3,c'2,c'1,c'0],4)),imm),strm3)) end | (true, (false,(false,(true,(c'3,(c'2,(c'1,c'0))))))) => let val (_,(rm,strm3)) = readModRM(REX,strm2) in Zfull_inst (p, (Zset ((Cast.natToZcond o BitsN.toNat) (BitsN.fromBitstring ([c'3,c'2,c'1,c'0],4)), (have_rex,rm)),strm3)) end | (true, (false,(true,(x'1,(x'0,(false,(true,true))))))) => let val size = OpSize (have_rex, (#W(REX : REX), (BitsN.B(0x1,1),op_size_override))) val (reg,(rm,strm3)) = readModRM(REX,strm2) in Zfull_inst (p, (Zbit_test ((Cast.natToZbit_test_name o BitsN.toNat) (BitsN.fromBitstring([x'1,x'0],2)), (size,Zrm_r(rm,reg))),strm3)) end | (true, (false,(true,(true,(true,(false,(true,false))))))) => let val size = OpSize (have_rex, (#W(REX : REX), (BitsN.B(0x1,1),op_size_override))) val (opcode,(rm,strm3)) = readOpcodeModRM(REX,strm2) val (imm,strm4) = oimmediate8 strm3 in case boolify'3 opcode of (true,(x'1,x'0)) => Zfull_inst (p, (Zbit_test ((Cast.natToZbit_test_name o BitsN.toNat) (BitsN.fromBitstring([x'1,x'0],2)), (size,Zrm_i(rm,imm))),strm4)) | _ => Zdec_fail "Unsupported opcode: Group 8" end | (true, (false,(true,(false,(true,(true,(true,true))))))) => let val size = OpSize (have_rex, (#W(REX : REX), (BitsN.B(0x1,1),op_size_override))) val (reg,(rm,strm3)) = readModRM(REX,strm2) in Zfull_inst(p,(Zimul2(size,(reg,rm)),strm3)) end | (true, (false,(true,(true,(false,(false,(false,v'0))))))) => let val size = OpSize (have_rex, (#W(REX : REX), (BitsN.fromBitstring([v'0],1), op_size_override))) val (reg,(rm,strm3)) = readModRM(REX,strm2) in Zfull_inst(p,(Zcmpxchg(size,(rm,reg)),strm3)) end | (true, (false,(true,(true,(s'0,(true,(true,v'0))))))) => let val size2 = OpSize (have_rex, (#W(REX : REX), (BitsN.B(0x1,1),op_size_override))) val size = if (BitsN.fromBitstring([v'0],1)) = (BitsN.B(0x1,1)) then Z16 else Z8 have_rex val (reg,(rm,strm3)) = readModRM(REX,strm2) val arg = (size,(Zr_rm(reg,rm),size2)) val instr = if (BitsN.fromBitstring([s'0],1)) = (BitsN.B(0x1,1)) then Zmovsx arg else Zmovzx arg in Zfull_inst(p,(instr,strm3)) end | (true, (true,(false,(false,(false,(false,(false,v'0))))))) => let val size = OpSize (have_rex, (#W(REX : REX), (BitsN.fromBitstring([v'0],1), op_size_override))) val (reg,(rm,strm3)) = readModRM(REX,strm2) in Zfull_inst(p,(Zxadd(size,(rm,reg)),strm3)) end | (true, (true,(false,(false,(false,(false,(true,false))))))) => let val (reg,(rm,strm3)) = readOpcodeModRM(REX,strm2) val (imm,strm4) = oimmediate8 strm3 val a = ((Cast.natTosse_compare o BitsN.toNat) imm, (reg,rm_to_xmm_mem rm)) in case p of [BitsN.B(0x66,_)] => Zfull_inst(p,(SSE(CMPPD a),strm4)) | [BitsN.B(0xF3,_)] => Zfull_inst(p,(SSE(CMPSS a),strm4)) | [BitsN.B(0xF2,_)] => Zfull_inst(p,(SSE(CMPSD a),strm4)) | _ => Zfull_inst(p,(SSE(CMPPS a),strm4)) end | (true, (true,(true,(false,(false,(true,(true,false))))))) => let val (reg,(rm,strm3)) = readOpcodeModRM(REX,strm2) val a = (reg,rm_to_xmm_mem rm) in case p of [BitsN.B(0x66,_)] => Zfull_inst (p,(SSE(CVTPD2DQ(true,a)),strm3)) | [BitsN.B(0xF3,_)] => Zfull_inst(p,(SSE(CVTDQ2PD a),strm3)) | [BitsN.B(0xF2,_)] => Zfull_inst(p,(SSE(CVTPD2DQ(false,a)),strm3)) | _ => Zdec_fail ("Unsupported opcode: " ^ (BitsN.toHexString opc)) end | _ => Zdec_fail ("Unsupported opcode: 0F " ^ (BitsN.toHexString opc))) | ((opc'7, (opc'6,(opc'5,(opc'4,(opc'3,(opc'2,(opc'1,opc'0))))))), _) => Zdec_fail ("Unsupported opcode: " ^ (BitsN.toHexString (BitsN.fromBitstring ([opc'7,opc'6,opc'5,opc'4,opc'3,opc'2, opc'1,opc'0],8))))) | [] => Zdec_fail "No opcode" end; fun x64_fetch () = let val strm = ref [] in ( L3.for (19,0, fn i => strm := ((Map.lookup ((!MEM),BitsN.toNat(BitsN.+((!RIP),BitsN.fromNat(i,64))))) :: (!strm))) ; (!strm) ) end; fun x64_next () = case x64_decode(x64_fetch ()) of Zfull_inst(_,(i,Option.SOME strm1)) => let val len = Nat.-(20,L3.length strm1) in ( RIP := (BitsN.+((!RIP),BitsN.fromNat(len,64))); Run i ) end | Zfull_inst(_,(_,NONE)) => raise FAILURE "not enough bytes" | Zdec_fail s => raise FAILURE s; fun e_imm8 imm = if (BitsN.<=(BitsN.B(0xFFFFFFFFFFFFFF80,64),imm)) andalso (BitsN.<=(imm,BitsN.B(0x7F,64))) then [BitsN.bits(7,0) imm] else []; fun e_imm16 imm = if (BitsN.<=(BitsN.B(0xFFFFFFFFFFFF8000,64),imm)) andalso (BitsN.<=(imm,BitsN.B(0x7FFF,64))) then [BitsN.bits(7,0) imm,BitsN.bits(15,8) imm] else []; fun e_imm32 imm = if (BitsN.<=(BitsN.B(0xFFFFFFFF80000000,64),imm)) andalso (BitsN.<=(imm,BitsN.B(0x7FFFFFFF,64))) then [BitsN.bits(7,0) imm,BitsN.bits(15,8) imm,BitsN.bits(23,16) imm, BitsN.bits(31,24) imm] else []; fun e_imm64 imm = [BitsN.bits(7,0) imm,BitsN.bits(15,8) imm,BitsN.bits(23,16) imm, BitsN.bits(31,24) imm,BitsN.bits(39,32) imm,BitsN.bits(47,40) imm, BitsN.bits(55,48) imm,BitsN.bits(63,56) imm]; fun e_imm imm = case e_imm8 imm of [] => (case e_imm16 imm of [] => (case e_imm32 imm of [] => e_imm64 imm | l => l) | l => l) | l => l; fun e_imm_8_32 imm = case e_imm8 imm of [] => (case e_imm32 imm of [] => (8,[]) | l => (4,l)) | l => (1,l); fun e_ModRM (r,rm) = case rm of Zm(NONE,(ZripBase,displacement)) => Option.SOME (BitsN.concat[BitsN.B(0x0,1),BitsN.bits(3,3) r,BitsN.B(0x0,2)], (BitsN.concat[BitsN.B(0x0,2),BitsN.bits(2,0) r,BitsN.B(0x5,3)]) :: (e_imm32 displacement)) | Zr rm => let val rm = BitsN.fromNat(Cast.ZregToNat rm,4) in Option.SOME (BitsN.concat [BitsN.B(0x0,1),BitsN.bits(3,3) r,BitsN.B(0x0,1), BitsN.bits(3,3) rm], [BitsN.concat [BitsN.B(0x3,2),BitsN.bits(2,0) r,BitsN.bits(2,0) rm]]) end | Zm(NONE,(ZnoBase,imm)) => (case e_imm32 imm of [] => NONE | l => Option.SOME (BitsN.concat[BitsN.B(0x0,1),BitsN.bits(3,3) r,BitsN.B(0x0,2)], [BitsN.concat[BitsN.B(0x0,2),BitsN.bits(2,0) r,BitsN.B(0x4,3)], BitsN.B(0x25,8)] @ l)) | Zm(Option.SOME(ss,index),(ZnoBase,imm)) => let val i = BitsN.fromNat(Cast.ZregToNat index,4) in case e_imm32 imm of [] => NONE | l => Option.SOME (BitsN.concat [BitsN.B(0x0,1),BitsN.bits(3,3) r,BitsN.bits(3,3) i, BitsN.B(0x0,1)], [BitsN.concat [BitsN.B(0x0,2),BitsN.bits(2,0) r,BitsN.B(0x4,3)], BitsN.concat[ss,BitsN.bits(2,0) i,BitsN.B(0x5,3)]] @ l) end | Zm(Option.SOME(ss,index),(ZregBase base,imm)) => let val b = BitsN.fromNat(Cast.ZregToNat base,4) val i = BitsN.fromNat(Cast.ZregToNat index,4) val b20 = BitsN.bits(2,0) b val (s,l) = if (imm = (BitsN.B(0x0,64))) andalso (not(b20 = (BitsN.B(0x5,3)))) then (0,[]) else e_imm_8_32 imm in if Set.mem(s,[0,1,4]) then Option.SOME (BitsN.concat [BitsN.B(0x0,1),BitsN.bits(3,3) r,BitsN.bits(3,3) i, BitsN.bits(3,3) b], [BitsN.concat [case s of 0 => BitsN.B(0x0,2) | 1 => BitsN.B(0x1,2) | _ => BitsN.B(0x2,2),BitsN.bits(2,0) r, BitsN.B(0x4,3)], BitsN.concat[ss,BitsN.bits(2,0) i,b20]] @ l) else NONE end | Zm(NONE,(ZregBase base,imm)) => let val base = BitsN.fromNat(Cast.ZregToNat base,4) val base20 = BitsN.bits(2,0) base val (s,l) = if (imm = (BitsN.B(0x0,64))) andalso (not(base20 = (BitsN.B(0x5,3)))) then (0,[]) else e_imm_8_32 imm in if Set.mem(s,[0,1,4]) then Option.SOME (BitsN.concat [BitsN.B(0x0,1),BitsN.bits(3,3) r,BitsN.B(0x0,1), BitsN.bits(3,3) base], ((BitsN.concat [case s of 0 => BitsN.B(0x0,2) | 1 => BitsN.B(0x1,2) | _ => BitsN.B(0x2,2),BitsN.bits(2,0) r,base20]) :: (if base20 = (BitsN.B(0x4,3)) then [BitsN.@@(BitsN.B(0x4,5),base20)] else [])) @ l) else NONE end | _ => NONE; fun rex_prefix rex = if rex = (BitsN.B(0x0,4)) then [] else [BitsN.@@(BitsN.B(0x4,4),rex)]; fun e_opsize (sz,rex) = case sz of Z8 have_rex => let val p = rex_prefix rex in (if have_rex andalso (p = []) then [BitsN.B(0x40,8)] else p, BitsN.B(0x0,8)) end | Z16 => ([BitsN.B(0x66,8)] @ (rex_prefix(BitsN.&&(rex,BitsN.B(0x7,4)))), BitsN.B(0x1,8)) | Z32 => (rex_prefix(BitsN.&&(rex,BitsN.B(0x7,4))),BitsN.B(0x1,8)) | Z64 => (rex_prefix(BitsN.||(rex,BitsN.B(0x8,4))),BitsN.B(0x1,8)); fun e_opsize_imm (sz,(rex,(imm,normal))) = let val (prefixes,v) = e_opsize(sz,rex) in case if (sz = Z64) andalso normal then Z32 else sz of Z8 _ => (case e_imm8 imm of [] => NONE | l => (if v = (BitsN.B(0x0,8)) then Option.SOME(prefixes,(v,l)) else NONE)) | Z16 => (case e_imm16 imm of [] => NONE | l => (if v = (BitsN.B(0x1,8)) then Option.SOME(prefixes,(v,l)) else NONE)) | Z32 => (case e_imm32 imm of [] => NONE | l => (if v = (BitsN.B(0x1,8)) then Option.SOME(prefixes,(v,l)) else NONE)) | Z64 => if v = (BitsN.B(0x1,8)) then Option.SOME(prefixes,(v,e_imm64 imm)) else NONE end; fun e_opc (opc1,(opc2,rm)) = case e_ModRM(BitsN.fromNat(BitsN.toNat opc2,4),rm) of NONE => [] | Option.SOME(rex,strm) => (rex_prefix rex) @ (opc1 :: strm); fun e_gen_rm_reg (sz,(rm,(r,(p,(opc,mo))))) = case e_ModRM(r,rm) of NONE => [] | Option.SOME(rex,strm) => let val (prefixes,v) = e_opsize(sz,rex) val m = case mo of Option.SOME x => x | NONE => v in List.concat[prefixes,p,[BitsN.||(opc,m)],strm] end; fun e_rm_imm (sz,(rm,(imm,(opc1,opc2)))) = case e_ModRM(opc1,rm) of NONE => [] | Option.SOME(rex,strm) => (case e_opsize_imm(sz,(rex,(imm,true))) of Option.SOME(prefixes,(v,l)) => List.concat[prefixes,[BitsN.||(opc2,v)],strm,l] | NONE => []); fun e_rm_imm8 (sz,(rm,(imm,(opc1,opc2)))) = case e_ModRM(opc1,rm) of NONE => [] | Option.SOME(rex,strm) => let val (prefixes,v) = e_opsize(sz,rex) in case e_imm8 imm of [] => [] | l => List.concat[prefixes,[BitsN.||(opc2,v)],strm,l] end; fun e_rm_imm8b (sz,(rm,(imm,(opc1,opc2)))) = case e_ModRM(opc1,rm) of Option.SOME(rex,s :: t) => let val prefixes = L3.fst(e_opsize(sz,rex)) in case e_imm8 imm of [] => [] | l => List.concat[prefixes,opc2,[BitsN.||(s,BitsN.B(0x20,8))],t,l] end | _ => []; fun e_rax_imm (sz,(imm,opc)) = case e_opsize_imm(sz,(BitsN.B(0x0,4),(imm,true))) of Option.SOME(prefixes,(v,l)) => List.concat[prefixes,[BitsN.||(opc,v)],l] | NONE => []; fun e_jcc_rel32 i = case i of Zjcc(cond,imm) => (case (e_imm32 imm,cond) of ([],_) => [] | (l,Z_ALWAYS) => (BitsN.B(0xE9,8)) :: l | (l,_) => [BitsN.B(0xF,8), BitsN.@@(BitsN.B(0x8,4),BitsN.fromNat(Cast.ZcondToNat cond,4))] @ l) | _ => []; fun not_byte sz = case sz of Z8 _ => false | _ => true; fun is_rax rm = case rm of Zr RAX => true | _ => false; fun xmm_mem_to_rm x = case x of xmm_reg r => Zr((Cast.natToZreg o BitsN.toNat) r) | xmm_mem m => Zm m; fun encode_sse_binop bop = case bop of sse_add => BitsN.B(0x0,3) | sse_mul => BitsN.B(0x1,3) | sse_sub => BitsN.B(0x4,3) | sse_min => BitsN.B(0x5,3) | sse_div => BitsN.B(0x6,3) | sse_max => BitsN.B(0x7,3); fun encode_sse i = case i of bin_PD(bop,(dst,src)) => (BitsN.B(0x66,8)) :: (e_gen_rm_reg (Z32, (xmm_mem_to_rm src, (BitsN.fromNat(BitsN.toNat dst,4), ([BitsN.B(0xF,8)], (BitsN.concat [BitsN.B(0x5,4),BitsN.B(0x1,1),encode_sse_binop bop], Option.SOME(BitsN.B(0x0,8)))))))) | bin_PS(bop,(dst,src)) => e_gen_rm_reg (Z32, (xmm_mem_to_rm src, (BitsN.fromNat(BitsN.toNat dst,4), ([BitsN.B(0xF,8)], (BitsN.concat [BitsN.B(0x5,4),BitsN.B(0x1,1),encode_sse_binop bop], Option.SOME(BitsN.B(0x0,8))))))) | bin_SD(bop,(dst,src)) => (BitsN.B(0xF2,8)) :: (e_gen_rm_reg (Z32, (xmm_mem_to_rm src, (BitsN.fromNat(BitsN.toNat dst,4), ([BitsN.B(0xF,8)], (BitsN.concat [BitsN.B(0x5,4),BitsN.B(0x1,1),encode_sse_binop bop], Option.SOME(BitsN.B(0x0,8)))))))) | bin_SS(bop,(dst,src)) => (BitsN.B(0xF3,8)) :: (e_gen_rm_reg (Z32, (xmm_mem_to_rm src, (BitsN.fromNat(BitsN.toNat dst,4), ([BitsN.B(0xF,8)], (BitsN.concat [BitsN.B(0x5,4),BitsN.B(0x1,1),encode_sse_binop bop], Option.SOME(BitsN.B(0x0,8)))))))) | logic_PD(bop,(dst,src)) => (BitsN.B(0x66,8)) :: (e_gen_rm_reg (Z32, (xmm_mem_to_rm src, (BitsN.fromNat(BitsN.toNat dst,4), ([BitsN.B(0xF,8)], (BitsN.concat [BitsN.B(0x5,4),BitsN.B(0x1,2), BitsN.fromNat(Cast.sse_logicToNat bop,2)], Option.SOME(BitsN.B(0x0,8)))))))) | logic_PS(bop,(dst,src)) => e_gen_rm_reg (Z32, (xmm_mem_to_rm src, (BitsN.fromNat(BitsN.toNat dst,4), ([BitsN.B(0xF,8)], (BitsN.concat [BitsN.B(0x5,4),BitsN.B(0x1,2), BitsN.fromNat(Cast.sse_logicToNat bop,2)], Option.SOME(BitsN.B(0x0,8))))))) | CMPPD(bop,(dst,src)) => ((BitsN.B(0x66,8)) :: (e_gen_rm_reg (Z32, (xmm_mem_to_rm src, (BitsN.fromNat(BitsN.toNat dst,4), ([BitsN.B(0xF,8)], (BitsN.B(0xC2,8),Option.SOME(BitsN.B(0x0,8))))))))) @ [BitsN.fromNat(Cast.sse_compareToNat bop,8)] | CMPPS(bop,(dst,src)) => (e_gen_rm_reg (Z32, (xmm_mem_to_rm src, (BitsN.fromNat(BitsN.toNat dst,4), ([BitsN.B(0xF,8)],(BitsN.B(0xC2,8),Option.SOME(BitsN.B(0x0,8)))))))) @ [BitsN.fromNat(Cast.sse_compareToNat bop,8)] | CMPSD(bop,(dst,src)) => ((BitsN.B(0xF2,8)) :: (e_gen_rm_reg (Z32, (xmm_mem_to_rm src, (BitsN.fromNat(BitsN.toNat dst,4), ([BitsN.B(0xF,8)], (BitsN.B(0xC2,8),Option.SOME(BitsN.B(0x0,8))))))))) @ [BitsN.fromNat(Cast.sse_compareToNat bop,8)] | CMPSS(bop,(dst,src)) => ((BitsN.B(0xF3,8)) :: (e_gen_rm_reg (Z32, (xmm_mem_to_rm src, (BitsN.fromNat(BitsN.toNat dst,4), ([BitsN.B(0xF,8)], (BitsN.B(0xC2,8),Option.SOME(BitsN.B(0x0,8))))))))) @ [BitsN.fromNat(Cast.sse_compareToNat bop,8)] | COMISD(src1,src2) => (BitsN.B(0x66,8)) :: (e_gen_rm_reg (Z32, (xmm_mem_to_rm src2, (BitsN.fromNat(BitsN.toNat src1,4), ([BitsN.B(0xF,8)], (BitsN.B(0x2F,8),Option.SOME(BitsN.B(0x0,8)))))))) | COMISS(src1,src2) => e_gen_rm_reg (Z32, (xmm_mem_to_rm src2, (BitsN.fromNat(BitsN.toNat src1,4), ([BitsN.B(0xF,8)],(BitsN.B(0x2F,8),NONE))))) | CVTDQ2PD(dst,src) => (BitsN.B(0xF3,8)) :: (e_gen_rm_reg (Z32, (xmm_mem_to_rm src, (BitsN.fromNat(BitsN.toNat dst,4), ([BitsN.B(0xF,8)], (BitsN.B(0xE6,8),Option.SOME(BitsN.B(0x0,8)))))))) | CVTDQ2PS(dst,src) => e_gen_rm_reg (Z32, (xmm_mem_to_rm src, (BitsN.fromNat(BitsN.toNat dst,4), ([BitsN.B(0xF,8)],(BitsN.B(0x5B,8),Option.SOME(BitsN.B(0x0,8))))))) | CVTPD2DQ(truncate,(dst,src)) => (if truncate then BitsN.B(0x66,8) else BitsN.B(0xF2,8)) :: (e_gen_rm_reg (Z32, (xmm_mem_to_rm src, (BitsN.fromNat(BitsN.toNat dst,4), ([BitsN.B(0xF,8)], (BitsN.B(0xE6,8),Option.SOME(BitsN.B(0x0,8)))))))) | CVTPD2PS(dst,src) => (BitsN.B(0x66,8)) :: (e_gen_rm_reg (Z32, (xmm_mem_to_rm src, (BitsN.fromNat(BitsN.toNat dst,4), ([BitsN.B(0xF,8)], (BitsN.B(0x5A,8),Option.SOME(BitsN.B(0x0,8)))))))) | CVTPS2DQ(truncate,(dst,src)) => (if truncate then BitsN.B(0xF3,8) else BitsN.B(0x66,8)) :: (e_gen_rm_reg (Z32, (xmm_mem_to_rm src, (BitsN.fromNat(BitsN.toNat dst,4), ([BitsN.B(0xF,8)], (BitsN.B(0x5B,8),Option.SOME(BitsN.B(0x0,8)))))))) | CVTPS2PD(dst,src) => e_gen_rm_reg (Z32, (xmm_mem_to_rm src, (BitsN.fromNat(BitsN.toNat dst,4), ([BitsN.B(0xF,8)],(BitsN.B(0x5A,8),Option.SOME(BitsN.B(0x0,8))))))) | CVTSD2SI(truncate,(quad,(dst,src))) => (BitsN.B(0xF2,8)) :: (e_gen_rm_reg (if quad then Z64 else Z32, (xmm_mem_to_rm src, (BitsN.fromNat(Cast.ZregToNat dst,4), ([BitsN.B(0xF,8)], (BitsN.B(0x2C,8), Option.SOME(BitsN.fromBool 8 (not truncate)))))))) | CVTSD2SS(dst,src) => (BitsN.B(0xF2,8)) :: (e_gen_rm_reg (Z32, (xmm_mem_to_rm src, (BitsN.fromNat(BitsN.toNat dst,4), ([BitsN.B(0xF,8)], (BitsN.B(0x5A,8),Option.SOME(BitsN.B(0x0,8)))))))) | CVTSI2SD(quad,(reg,src)) => (BitsN.B(0xF2,8)) :: (e_gen_rm_reg (if quad then Z64 else Z32, (src, (BitsN.fromNat(BitsN.toNat reg,4), ([BitsN.B(0xF,8)], (BitsN.B(0x2A,8),Option.SOME(BitsN.B(0x0,8)))))))) | CVTSI2SS(quad,(reg,src)) => (BitsN.B(0xF3,8)) :: (e_gen_rm_reg (if quad then Z64 else Z32, (src, (BitsN.fromNat(BitsN.toNat reg,4), ([BitsN.B(0xF,8)], (BitsN.B(0x2A,8),Option.SOME(BitsN.B(0x0,8)))))))) | CVTSS2SD(dst,src) => (BitsN.B(0xF3,8)) :: (e_gen_rm_reg (Z32, (xmm_mem_to_rm src, (BitsN.fromNat(BitsN.toNat dst,4), ([BitsN.B(0xF,8)], (BitsN.B(0x5A,8),Option.SOME(BitsN.B(0x0,8)))))))) | CVTSS2SI(truncate,(quad,(dst,src))) => (BitsN.B(0xF3,8)) :: (e_gen_rm_reg (if quad then Z64 else Z32, (xmm_mem_to_rm src, (BitsN.fromNat(Cast.ZregToNat dst,4), ([BitsN.B(0xF,8)], (BitsN.B(0x2C,8), Option.SOME(BitsN.fromBool 8 (not truncate)))))))) | MOVAP_D_S(double,(xmm_reg dst,src)) => (if double then [BitsN.B(0x66,8)] else []) @ (e_gen_rm_reg (Z32, (xmm_mem_to_rm src, (BitsN.fromNat(BitsN.toNat dst,4), ([BitsN.B(0xF,8)], (BitsN.B(0x28,8),Option.SOME(BitsN.B(0x0,8)))))))) | MOVAP_D_S(double,(dst,xmm_reg src)) => (if double then [BitsN.B(0x66,8)] else []) @ (e_gen_rm_reg (Z32, (xmm_mem_to_rm dst, (BitsN.fromNat(BitsN.toNat src,4), ([BitsN.B(0xF,8)], (BitsN.B(0x29,8),Option.SOME(BitsN.B(0x0,8)))))))) | MOVAP_D_S _ => [] | MOVUP_D_S(double,(xmm_reg dst,src)) => (if double then [BitsN.B(0x66,8)] else []) @ (e_gen_rm_reg (Z32, (xmm_mem_to_rm src, (BitsN.fromNat(BitsN.toNat dst,4), ([BitsN.B(0xF,8)], (BitsN.B(0x10,8),Option.SOME(BitsN.B(0x0,8)))))))) | MOVUP_D_S(double,(dst,xmm_reg src)) => (if double then [BitsN.B(0x66,8)] else []) @ (e_gen_rm_reg (Z32, (xmm_mem_to_rm dst, (BitsN.fromNat(BitsN.toNat src,4), ([BitsN.B(0xF,8)], (BitsN.B(0x11,8),Option.SOME(BitsN.B(0x0,8)))))))) | MOVUP_D_S _ => [] | MOVSD(xmm_reg dst,src) => (BitsN.B(0xF2,8)) :: (e_gen_rm_reg (Z32, (xmm_mem_to_rm src, (BitsN.fromNat(BitsN.toNat dst,4), ([BitsN.B(0xF,8)], (BitsN.B(0x10,8),Option.SOME(BitsN.B(0x0,8)))))))) | MOVSD(dst,xmm_reg src) => (BitsN.B(0xF2,8)) :: (e_gen_rm_reg (Z32, (xmm_mem_to_rm dst, (BitsN.fromNat(BitsN.toNat src,4), ([BitsN.B(0xF,8)], (BitsN.B(0x11,8),Option.SOME(BitsN.B(0x0,8)))))))) | MOVSD _ => [] | MOVSS(xmm_reg dst,src) => (BitsN.B(0xF3,8)) :: (e_gen_rm_reg (Z32, (xmm_mem_to_rm src, (BitsN.fromNat(BitsN.toNat dst,4), ([BitsN.B(0xF,8)], (BitsN.B(0x10,8),Option.SOME(BitsN.B(0x0,8)))))))) | MOVSS(dst,xmm_reg src) => (BitsN.B(0xF3,8)) :: (e_gen_rm_reg (Z32, (xmm_mem_to_rm dst, (BitsN.fromNat(BitsN.toNat src,4), ([BitsN.B(0xF,8)], (BitsN.B(0x11,8),Option.SOME(BitsN.B(0x0,8)))))))) | MOVSS _ => [] | MOV_D_Q(to_xmm,(quad,(xmm,rm))) => (BitsN.B(0x66,8)) :: (e_gen_rm_reg (if quad then Z64 else Z32, (rm, (BitsN.fromNat(BitsN.toNat xmm,4), ([BitsN.B(0xF,8)], (BitsN.concat [BitsN.B(0x3,3),BitsN.fromBit(not to_xmm),BitsN.B(0xE,4)], Option.SOME(BitsN.B(0x0,8)))))))) | MOVQ(xmm_mem m,xmm_reg src) => (BitsN.B(0x66,8)) :: (e_gen_rm_reg (Z8 false, (Zm m, (BitsN.fromNat(BitsN.toNat src,4), ([BitsN.B(0xF,8)],(BitsN.B(0xD6,8),NONE)))))) | MOVQ(xmm_reg r,src) => (BitsN.B(0xF3,8)) :: (e_gen_rm_reg (Z8 false, (xmm_mem_to_rm src, (BitsN.fromNat(BitsN.toNat r,4), ([BitsN.B(0xF,8)],(BitsN.B(0x7E,8),NONE)))))) | MOVQ _ => [] | PCMPEQQ(dst,src) => (BitsN.B(0x66,8)) :: (e_gen_rm_reg (Z32, (xmm_mem_to_rm src, (BitsN.fromNat(BitsN.toNat dst,4), ([BitsN.B(0xF,8),BitsN.B(0x38,8)], (BitsN.B(0x29,8),Option.SOME(BitsN.B(0x0,8)))))))) | PSRLW_imm(dst,imm) => ((BitsN.B(0x66,8)) :: (e_gen_rm_reg (Z32, (Zr((Cast.natToZreg o BitsN.toNat) dst), (BitsN.B(0x2,4), ([BitsN.B(0xF,8)], (BitsN.B(0x71,8),Option.SOME(BitsN.B(0x0,8))))))))) @ [imm] | PSRAW_imm(dst,imm) => ((BitsN.B(0x66,8)) :: (e_gen_rm_reg (Z32, (Zr((Cast.natToZreg o BitsN.toNat) dst), (BitsN.B(0x4,4), ([BitsN.B(0xF,8)], (BitsN.B(0x71,8),Option.SOME(BitsN.B(0x0,8))))))))) @ [imm] | PSLLW_imm(dst,imm) => ((BitsN.B(0x66,8)) :: (e_gen_rm_reg (Z32, (Zr((Cast.natToZreg o BitsN.toNat) dst), (BitsN.B(0x6,4), ([BitsN.B(0xF,8)], (BitsN.B(0x71,8),Option.SOME(BitsN.B(0x0,8))))))))) @ [imm] | PSRLD_imm(dst,imm) => ((BitsN.B(0x66,8)) :: (e_gen_rm_reg (Z32, (Zr((Cast.natToZreg o BitsN.toNat) dst), (BitsN.B(0x2,4), ([BitsN.B(0xF,8)], (BitsN.B(0x72,8),Option.SOME(BitsN.B(0x0,8))))))))) @ [imm] | PSRAD_imm(dst,imm) => ((BitsN.B(0x66,8)) :: (e_gen_rm_reg (Z32, (Zr((Cast.natToZreg o BitsN.toNat) dst), (BitsN.B(0x4,4), ([BitsN.B(0xF,8)], (BitsN.B(0x72,8),Option.SOME(BitsN.B(0x0,8))))))))) @ [imm] | PSLLD_imm(dst,imm) => ((BitsN.B(0x66,8)) :: (e_gen_rm_reg (Z32, (Zr((Cast.natToZreg o BitsN.toNat) dst), (BitsN.B(0x6,4), ([BitsN.B(0xF,8)], (BitsN.B(0x72,8),Option.SOME(BitsN.B(0x0,8))))))))) @ [imm] | PSRLQ_imm(dst,imm) => ((BitsN.B(0x66,8)) :: (e_gen_rm_reg (Z32, (Zr((Cast.natToZreg o BitsN.toNat) dst), (BitsN.B(0x2,4), ([BitsN.B(0xF,8)], (BitsN.B(0x73,8),Option.SOME(BitsN.B(0x0,8))))))))) @ [imm] | PSRLDQ(dst,imm) => ((BitsN.B(0x66,8)) :: (e_gen_rm_reg (Z32, (Zr((Cast.natToZreg o BitsN.toNat) dst), (BitsN.B(0x3,4), ([BitsN.B(0xF,8)], (BitsN.B(0x73,8),Option.SOME(BitsN.B(0x0,8))))))))) @ [imm] | PSLLQ_imm(dst,imm) => ((BitsN.B(0x66,8)) :: (e_gen_rm_reg (Z32, (Zr((Cast.natToZreg o BitsN.toNat) dst), (BitsN.B(0x6,4), ([BitsN.B(0xF,8)], (BitsN.B(0x73,8),Option.SOME(BitsN.B(0x0,8))))))))) @ [imm] | PSLLDQ(dst,imm) => ((BitsN.B(0x66,8)) :: (e_gen_rm_reg (Z32, (Zr((Cast.natToZreg o BitsN.toNat) dst), (BitsN.B(0x7,4), ([BitsN.B(0xF,8)], (BitsN.B(0x73,8),Option.SOME(BitsN.B(0x0,8))))))))) @ [imm] | SQRTPD(dst,src) => (BitsN.B(0x66,8)) :: (e_gen_rm_reg (Z32, (xmm_mem_to_rm src, (BitsN.fromNat(BitsN.toNat dst,4), ([BitsN.B(0xF,8)], (BitsN.B(0x51,8),Option.SOME(BitsN.B(0x0,8)))))))) | SQRTSD(dst,src) => (BitsN.B(0xF2,8)) :: (e_gen_rm_reg (Z32, (xmm_mem_to_rm src, (BitsN.fromNat(BitsN.toNat dst,4), ([BitsN.B(0xF,8)], (BitsN.B(0x51,8),Option.SOME(BitsN.B(0x0,8)))))))) | SQRTPS(dst,src) => e_gen_rm_reg (Z32, (xmm_mem_to_rm src, (BitsN.fromNat(BitsN.toNat dst,4), ([BitsN.B(0xF,8)],(BitsN.B(0x51,8),Option.SOME(BitsN.B(0x0,8))))))) | SQRTSS(dst,src) => (BitsN.B(0xF3,8)) :: (e_gen_rm_reg (Z32, (xmm_mem_to_rm src, (BitsN.fromNat(BitsN.toNat dst,4), ([BitsN.B(0xF,8)], (BitsN.B(0x51,8),Option.SOME(BitsN.B(0x0,8)))))))); fun encode i = case i of SSE j => encode_sse j | Zbinop(bop,(sz,Zrm_i(rm,imm))) => (if bop = Ztest then if is_rax rm then e_rax_imm(sz,(imm,BitsN.B(0xA8,8))) else e_rm_imm(sz,(rm,(imm,(BitsN.B(0x0,4),BitsN.B(0xF6,8))))) else let val opc = BitsN.fromNat(Cast.Zbinop_nameToNat bop,4) in if BitsN.bit(opc,3) then if imm = (BitsN.B(0x1,64)) then e_gen_rm_reg (sz, (rm, (BitsN.&&(opc,BitsN.B(0x7,4)), ([],(BitsN.B(0xD0,8),NONE))))) else e_rm_imm8 (sz, (rm, (imm, (BitsN.&&(opc,BitsN.B(0x7,4)), BitsN.B(0xC0,8))))) else if (not_byte sz) andalso (not((e_imm8 imm) = [])) then e_rm_imm8(sz,(rm,(imm,(opc,BitsN.B(0x83,8))))) else if is_rax rm then e_rax_imm (sz, (imm, BitsN.concat [BitsN.B(0x0,2),BitsN.bits(2,0) opc, BitsN.B(0x4,3)])) else e_rm_imm(sz,(rm,(imm,(opc,BitsN.B(0x80,8))))) end) | Zbinop(bop,(sz,Zrm_r(rm,r))) => (if bop = Ztest then e_gen_rm_reg (sz, (rm, (BitsN.fromNat(Cast.ZregToNat r,4), ([],(BitsN.B(0x84,8),NONE))))) else let val opc = BitsN.fromNat(Cast.Zbinop_nameToNat bop,4) in if BitsN.bit(opc,3) then if r = RCX then e_gen_rm_reg (sz, (rm, (BitsN.&&(opc,BitsN.B(0x7,4)), ([],(BitsN.B(0xD2,8),NONE))))) else [] else e_gen_rm_reg (sz, (rm, (BitsN.fromNat(Cast.ZregToNat r,4), ([], (BitsN.concat [BitsN.B(0x0,2),BitsN.bits(2,0) opc, BitsN.B(0x0,3)],NONE))))) end) | Zbinop(bop,(sz,Zr_rm(r,rm))) => let val opc = BitsN.fromNat(Cast.Zbinop_nameToNat bop,4) in if BitsN.bit(opc,3) then [] else e_gen_rm_reg (sz, (rm, (BitsN.fromNat(Cast.ZregToNat r,4), ([], (BitsN.concat [BitsN.B(0x0,2),BitsN.bits(2,0) opc,BitsN.B(0x2,3)], NONE))))) end | Zbit_test(bt,(sz,Zrm_r(rm,r))) => e_gen_rm_reg (sz, (rm, (BitsN.fromNat(Cast.ZregToNat r,4), ([BitsN.B(0xF,8)], (BitsN.concat [BitsN.B(0x5,3), BitsN.fromNat(Cast.Zbit_test_nameToNat bt,2),BitsN.B(0x3,3)], NONE))))) | Zbit_test(bt,(sz,Zrm_i(rm,i))) => e_rm_imm8b (sz, (rm, (i, (BitsN.fromNat(Cast.Zbit_test_nameToNat bt,4), [BitsN.B(0xF,8),BitsN.B(0xBA,8)])))) | Zbit_test _ => [] | Zcall(Zrm rm) => e_opc(BitsN.B(0xFF,8),(BitsN.B(0x2,3),rm)) | Zcall(Zimm imm) => (case e_imm32 imm of [] => [] | l => (BitsN.B(0xE8,8)) :: l) | Zcmc => [BitsN.B(0xF5,8)] | Zclc => [BitsN.B(0xF8,8)] | Zstc => [BitsN.B(0xF9,8)] | Zcmpxchg(sz,(rm,r)) => e_gen_rm_reg (sz, (rm, (BitsN.fromNat(Cast.ZregToNat r,4), ([BitsN.B(0xF,8)],(BitsN.B(0xB0,8),NONE))))) | Zdiv(sz,rm) => e_gen_rm_reg(sz,(rm,(BitsN.B(0x6,4),([],(BitsN.B(0xF6,8),NONE))))) | Zidiv(sz,rm) => e_gen_rm_reg(sz,(rm,(BitsN.B(0x7,4),([],(BitsN.B(0xF6,8),NONE))))) | Zjcc(cond,imm) => let val (s,l) = e_imm_8_32 imm in if cond = Z_ALWAYS then if s = 1 then (BitsN.B(0xEB,8)) :: l else if s = 4 then (BitsN.B(0xE9,8)) :: l else [] else if s = 1 then (BitsN.@@ (BitsN.B(0x7,4),BitsN.fromNat(Cast.ZcondToNat cond,4))) :: l else if s = 4 then [BitsN.B(0xF,8), BitsN.@@ (BitsN.B(0x8,4),BitsN.fromNat(Cast.ZcondToNat cond,4))] @ l else [] end | Zjmp rm => e_opc(BitsN.B(0xFF,8),(BitsN.B(0x4,3),rm)) | Zlea(Z8 _,_) => [] | Zlea(sz,Zr_rm(r,Zm m)) => e_gen_rm_reg (sz, (Zm m, (BitsN.fromNat(Cast.ZregToNat r,4),([],(BitsN.B(0x8D,8),NONE))))) | Zlea _ => [] | Zleave => [BitsN.B(0xC9,8)] | Zloop(cond,imm) => (case (cond,e_imm8 imm) of (_,[]) => [] | (Z_NE,l) => (BitsN.B(0xE0,8)) :: l | (Z_E,l) => (BitsN.B(0xE1,8)) :: l | (Z_ALWAYS,l) => (BitsN.B(0xE2,8)) :: l | _ => []) | Zmonop(Zinc,(Z8 _,rm)) => e_opc(BitsN.B(0xFE,8),(BitsN.B(0x0,3),rm)) | Zmonop(Zdec,(Z8 _,rm)) => e_opc(BitsN.B(0xFE,8),(BitsN.B(0x1,3),rm)) | Zmonop(Zinc,(sz,rm)) => e_gen_rm_reg(sz,(rm,(BitsN.B(0x0,4),([],(BitsN.B(0xFF,8),NONE))))) | Zmonop(Zdec,(sz,rm)) => e_gen_rm_reg(sz,(rm,(BitsN.B(0x1,4),([],(BitsN.B(0xFF,8),NONE))))) | Zmonop(Znot,(sz,rm)) => e_gen_rm_reg(sz,(rm,(BitsN.B(0x2,4),([],(BitsN.B(0xF6,8),NONE))))) | Zmonop(Zneg,(sz,rm)) => e_gen_rm_reg(sz,(rm,(BitsN.B(0x3,4),([],(BitsN.B(0xF6,8),NONE))))) | Zmov(Z_ALWAYS,(sz,Zrm_r(rm,r))) => e_gen_rm_reg (sz, (rm, (BitsN.fromNat(Cast.ZregToNat r,4),([],(BitsN.B(0x88,8),NONE))))) | Zmov(Z_ALWAYS,(sz,Zr_rm(r,rm))) => e_gen_rm_reg (sz, (rm, (BitsN.fromNat(Cast.ZregToNat r,4),([],(BitsN.B(0x8A,8),NONE))))) | Zmov(Z_ALWAYS,(sz,Zrm_i(Zr reg,imm))) => let val r = BitsN.fromNat(Cast.ZregToNat reg,4) val rex = if BitsN.bit(r,3) then BitsN.B(0x1,4) else BitsN.B(0x0,4) in case e_opsize_imm(sz,(rex,(imm,false))) of Option.SOME(prefixes,(v,l)) => List.concat [prefixes, [BitsN.concat [BitsN.B(0xB,4),BitsN.fromNat(BitsN.toNat v,1), BitsN.bits(2,0) r]],l] | NONE => [] end | Zmov(Z_ALWAYS,(sz,Zrm_i(rm,imm))) => e_rm_imm(sz,(rm,(imm,(BitsN.B(0x0,4),BitsN.B(0xC6,8))))) | Zmov(cond,(Z8 _,_)) => [] | Zmov(cond,(sz,Zr_rm(r,rm))) => e_gen_rm_reg (sz, (rm, (BitsN.fromNat(Cast.ZregToNat r,4), ([BitsN.B(0xF,8)], (BitsN.B(0x40,8), Option.SOME(BitsN.fromNat(Cast.ZcondToNat cond,8))))))) | Zmov _ => [] | Zmovsx(Z32,(Zr_rm(r,rm),Z64)) => e_gen_rm_reg (Z64, (rm, (BitsN.fromNat(Cast.ZregToNat r,4),([],(BitsN.B(0x63,8),NONE))))) | Zmovsx(sz1,(Zr_rm(r,rm),sz2)) => (if Nat.<(Zsize_width sz1,Zsize_width sz2) then let val v = if sz1 = Z16 then BitsN.B(0x1,8) else BitsN.B(0x0,8) in e_gen_rm_reg (sz2, (rm, (BitsN.fromNat(Cast.ZregToNat r,4), ([BitsN.B(0xF,8)],(BitsN.B(0xBE,8),Option.SOME v))))) end else []) | Zmovsx _ => [] | Zmovzx(sz1,(Zr_rm(r,rm),sz2)) => (if (Nat.<(Zsize_width sz1,Zsize_width sz2)) andalso (not(sz1 = Z32)) then let val v = if sz1 = Z16 then BitsN.B(0x1,8) else BitsN.B(0x0,8) in e_gen_rm_reg (sz2, (rm, (BitsN.fromNat(Cast.ZregToNat r,4), ([BitsN.B(0xF,8)],(BitsN.B(0xB6,8),Option.SOME v))))) end else []) | Zmovzx _ => [] | Zmul(sz,rm) => e_gen_rm_reg(sz,(rm,(BitsN.B(0x4,4),([],(BitsN.B(0xF6,8),NONE))))) | Zimul(sz,rm) => e_gen_rm_reg(sz,(rm,(BitsN.B(0x5,4),([],(BitsN.B(0xF6,8),NONE))))) | Zimul2(Z8 _,_) => [] | Zimul2(sz,(r,rm)) => e_gen_rm_reg (sz, (rm, (BitsN.fromNat(Cast.ZregToNat r,4), ([BitsN.B(0xF,8)],(BitsN.B(0xAF,8),NONE))))) | Zimul3(Z8 _,_) => [] | Zimul3(sz,(r,(rm,imm))) => let val (s,l) = e_imm_8_32 imm in if s = 1 then (e_gen_rm_reg (sz, (rm, (BitsN.fromNat(Cast.ZregToNat r,4), ([],(BitsN.B(0x6B,8),NONE)))))) @ l else if s = 4 then (e_gen_rm_reg (sz, (rm, (BitsN.fromNat(Cast.ZregToNat r,4), ([],(BitsN.B(0x69,8),NONE)))))) @ l else [] end | Znop 1 => [BitsN.B(0x90,8)] | Znop 2 => [BitsN.B(0x66,8),BitsN.B(0x90,8)] | Znop 3 => [BitsN.B(0xF,8),BitsN.B(0x1F,8),BitsN.B(0x0,8)] | Znop 4 => [BitsN.B(0xF,8),BitsN.B(0x1F,8),BitsN.B(0x40,8),BitsN.B(0x0,8)] | Znop 5 => [BitsN.B(0xF,8),BitsN.B(0x1F,8),BitsN.B(0x44,8),BitsN.B(0x0,8), BitsN.B(0x0,8)] | Znop 6 => [BitsN.B(0x66,8),BitsN.B(0xF,8),BitsN.B(0x1F,8),BitsN.B(0x44,8), BitsN.B(0x0,8),BitsN.B(0x0,8)] | Znop 7 => [BitsN.B(0xF,8),BitsN.B(0x1F,8),BitsN.B(0x80,8),BitsN.B(0x0,8), BitsN.B(0x0,8),BitsN.B(0x0,8),BitsN.B(0x0,8)] | Znop 8 => [BitsN.B(0xF,8),BitsN.B(0x1F,8),BitsN.B(0x84,8),BitsN.B(0x0,8), BitsN.B(0x0,8),BitsN.B(0x0,8),BitsN.B(0x0,8),BitsN.B(0x0,8)] | Znop 9 => [BitsN.B(0x66,8),BitsN.B(0xF,8),BitsN.B(0x1F,8),BitsN.B(0x84,8), BitsN.B(0x0,8),BitsN.B(0x0,8),BitsN.B(0x0,8),BitsN.B(0x0,8), BitsN.B(0x0,8)] | Znop _ => [] | Zpop(Zr reg) => let val r = BitsN.fromNat(Cast.ZregToNat reg,4) in (if BitsN.bit(r,3) then [BitsN.B(0x49,8)] else []) @ [BitsN.@@(BitsN.B(0xB,5),BitsN.bits(2,0) r)] end | Zpop rm => e_opc(BitsN.B(0x8F,8),(BitsN.B(0x0,3),rm)) | Zpush(Zrm(Zr reg)) => let val r = BitsN.fromNat(Cast.ZregToNat reg,4) in (if BitsN.bit(r,3) then [BitsN.B(0x49,8)] else []) @ [BitsN.@@(BitsN.B(0xA,5),BitsN.bits(2,0) r)] end | Zpush(Zrm rm) => e_opc(BitsN.B(0xFF,8),(BitsN.B(0x6,3),rm)) | Zpush(Zimm imm) => let val (s,l) = e_imm_8_32 imm in if s = 1 then (BitsN.B(0x6A,8)) :: l else if s = 4 then (BitsN.B(0x68,8)) :: l else [] end | Zret(BitsN.B(0x0,64)) => [BitsN.B(0xC3,8)] | Zret imm => (case e_imm16 imm of [] => [] | l => (BitsN.B(0xC2,8)) :: l) | Zset(Z_ALWAYS,(have_rex,rm)) => [] | Zset(cond,(have_rex,rm)) => e_gen_rm_reg (Z8 have_rex, (rm, (BitsN.B(0x0,4), ([BitsN.B(0xF,8)], (BitsN.@@(BitsN.B(0x9,4),BitsN.fromNat(Cast.ZcondToNat cond,4)), NONE))))) | Zxadd(sz,(rm,r)) => e_gen_rm_reg (sz, (rm, (BitsN.fromNat(Cast.ZregToNat r,4), ([BitsN.B(0xF,8)],(BitsN.B(0xC0,8),NONE))))) | Zxchg(sz,(rm,reg)) => (if (not_byte sz) andalso ((reg = RAX) orelse (is_rax rm)) then let val r = BitsN.fromNat(Cast.ZregToNat reg,4) val rex = if BitsN.bit(r,3) then BitsN.B(0x1,4) else BitsN.B(0x0,4) val (prefixes,v) = e_opsize(sz,rex) in if v = (BitsN.B(0x1,8)) then prefixes @ [BitsN.@@(BitsN.B(0x12,5),BitsN.bits(2,0) r)] else [] end else e_gen_rm_reg (sz, (rm, (BitsN.fromNat(Cast.ZregToNat reg,4), ([],(BitsN.B(0x86,8),NONE)))))); fun stripLeftSpaces s = L3.snd(L3.splitl(fn c => Char.isSpace c,s)); fun stripSpaces s = L3.fst(L3.splitr(fn c => Char.isSpace c,stripLeftSpaces s)); fun p_number s = case String.explode(stripSpaces s) of #"0" :: (#"b" :: t) => Nat.fromBinString(String.implode t) | #"0" :: (#"x" :: t) => Nat.fromHexString(String.implode t) | _ => Nat.fromString s; fun p_bin_or_hex_number s = case String.explode(stripSpaces s) of #"0" :: (#"b" :: t) => Nat.fromBinString(String.implode t) | #"0" :: (#"x" :: t) => Nat.fromHexString(String.implode t) | t => Nat.fromHexString(String.implode t); fun p_signed_number s = case String.explode(stripSpaces s) of #"-" :: t => (case p_number(String.implode t) of Option.SOME n => Option.SOME(IntInf.~(Nat.toInt n)) | NONE => NONE) | #"+" :: t => (case p_number(String.implode t) of Option.SOME n => Option.SOME(Nat.toInt n) | NONE => NONE) | t => (case p_number(String.implode t) of Option.SOME n => Option.SOME(Nat.toInt n) | NONE => NONE); fun p_imm8 s = case p_signed_number s of Option.SOME n => (if (IntInf.<=(IntInf.~ 128,n)) andalso (IntInf.<=(n,255)) then Option.SOME(BitsN.signExtend 64 (BitsN.fromInt(n,8))) else NONE) | NONE => NONE; fun p_imm16 s = case p_signed_number s of Option.SOME n => (if (IntInf.<=(IntInf.~ 32768,n)) andalso (IntInf.<=(n,65535)) then Option.SOME(BitsN.signExtend 64 (BitsN.fromInt(n,16))) else NONE) | NONE => NONE; fun p_imm32 s = case p_signed_number s of Option.SOME n => (if (IntInf.<=(IntInf.~ 2147483648,n)) andalso (IntInf.<=(n,4294967295)) then Option.SOME(BitsN.signExtend 64 (BitsN.fromInt(n,32))) else NONE) | NONE => NONE; fun p_imm64 s = case p_signed_number s of Option.SOME n => (if (IntInf.<=(IntInf.~ 9223372036854775808,n)) andalso (IntInf.<=(n,18446744073709551615)) then Option.SOME(BitsN.fromInt(n,64)) else NONE) | NONE => NONE; fun p_imm_of_size (sz,s) = case sz of Z8 _ => p_imm8 s | Z16 => p_imm16 s | Z32 => p_imm32 s | Z64 => p_imm64 s; fun readBytes (acc,l) = case l of [] => Option.SOME(List.rev acc) | h :: t => (case p_bin_or_hex_number h of Option.SOME n => (if Nat.<=(n,255) then readBytes((BitsN.fromNat(n,8)) :: acc,t) else NONE) | NONE => NONE); fun p_bytes s = readBytes([],L3.uncurry String.tokens (fn c => Char.isSpace c,s)); fun p_label s = case L3.uncurry String.tokens (fn c => Char.isSpace c,s) of [t] => let val (l,r) = L3.splitl (fn c => (Char.isAlphaNum c) orelse (Set.mem(c,[#"_",#"."])), t) in if (r = "") andalso ((not(l = "")) andalso (not(Char.isDigit(L3.strHd l)))) then Option.SOME l else NONE end | _ => NONE; fun p_register s = case stripSpaces s of "al" => Option.SOME(Z8 false,RAX) | "cl" => Option.SOME(Z8 false,RCX) | "dl" => Option.SOME(Z8 false,RDX) | "bl" => Option.SOME(Z8 false,RBX) | "ah" => Option.SOME(Z8 false,RSP) | "ch" => Option.SOME(Z8 false,RBP) | "dh" => Option.SOME(Z8 false,RSI) | "bh" => Option.SOME(Z8 false,RDI) | "spl" => Option.SOME(Z8 true,RSP) | "bpl" => Option.SOME(Z8 true,RBP) | "sil" => Option.SOME(Z8 true,RSI) | "dil" => Option.SOME(Z8 true,RDI) | "r8b" => Option.SOME(Z8 false,zR8) | "r9b" => Option.SOME(Z8 false,zR9) | "r10b" => Option.SOME(Z8 false,zR10) | "r11b" => Option.SOME(Z8 false,zR11) | "r12b" => Option.SOME(Z8 false,zR12) | "r13b" => Option.SOME(Z8 false,zR13) | "r14b" => Option.SOME(Z8 false,zR14) | "r15b" => Option.SOME(Z8 false,zR15) | "ax" => Option.SOME(Z16,RAX) | "cx" => Option.SOME(Z16,RCX) | "dx" => Option.SOME(Z16,RDX) | "bx" => Option.SOME(Z16,RBX) | "sp" => Option.SOME(Z16,RSP) | "bp" => Option.SOME(Z16,RBP) | "si" => Option.SOME(Z16,RSI) | "di" => Option.SOME(Z16,RDI) | "r8w" => Option.SOME(Z16,zR8) | "r9w" => Option.SOME(Z16,zR9) | "r10w" => Option.SOME(Z16,zR10) | "r11w" => Option.SOME(Z16,zR11) | "r12w" => Option.SOME(Z16,zR12) | "r13w" => Option.SOME(Z16,zR13) | "r14w" => Option.SOME(Z16,zR14) | "r15w" => Option.SOME(Z16,zR15) | "eax" => Option.SOME(Z32,RAX) | "ecx" => Option.SOME(Z32,RCX) | "edx" => Option.SOME(Z32,RDX) | "ebx" => Option.SOME(Z32,RBX) | "esp" => Option.SOME(Z32,RSP) | "ebp" => Option.SOME(Z32,RBP) | "esi" => Option.SOME(Z32,RSI) | "edi" => Option.SOME(Z32,RDI) | "r8d" => Option.SOME(Z32,zR8) | "r9d" => Option.SOME(Z32,zR9) | "r10d" => Option.SOME(Z32,zR10) | "r11d" => Option.SOME(Z32,zR11) | "r12d" => Option.SOME(Z32,zR12) | "r13d" => Option.SOME(Z32,zR13) | "r14d" => Option.SOME(Z32,zR14) | "r15d" => Option.SOME(Z32,zR15) | "rax" => Option.SOME(Z64,RAX) | "rcx" => Option.SOME(Z64,RCX) | "rdx" => Option.SOME(Z64,RDX) | "rbx" => Option.SOME(Z64,RBX) | "rsp" => Option.SOME(Z64,RSP) | "rbp" => Option.SOME(Z64,RBP) | "rsi" => Option.SOME(Z64,RSI) | "rdi" => Option.SOME(Z64,RDI) | "r8" => Option.SOME(Z64,zR8) | "r9" => Option.SOME(Z64,zR9) | "r10" => Option.SOME(Z64,zR10) | "r11" => Option.SOME(Z64,zR11) | "r12" => Option.SOME(Z64,zR12) | "r13" => Option.SOME(Z64,zR13) | "r14" => Option.SOME(Z64,zR14) | "r15" => Option.SOME(Z64,zR15) | _ => NONE; fun p_xreg s = case String.explode(stripSpaces s) of #"x" :: (#"m" :: (#"m" :: n)) => (case Nat.fromString(String.implode n) of Option.SOME n => (if Nat.<(n,8) then Option.SOME(BitsN.fromNat(n,3)) else NONE) | _ => NONE) | _ => NONE; fun p_scale s = case stripSpaces s of "1" => Option.SOME(BitsN.B(0x0,2)) | "2" => Option.SOME(BitsN.B(0x1,2)) | "4" => Option.SOME(BitsN.B(0x2,2)) | "8" => Option.SOME(BitsN.B(0x3,2)) | _ => NONE; fun p_scale_index s = case L3.uncurry String.fields (fn c => c = #"*",stripSpaces s) of [v1,v2] => (case p_register v1 of Option.SOME(sz,r) => (case p_scale v2 of Option.SOME n => (if sz = Z64 then Option.SOME(n,r) else NONE) | NONE => NONE) | NONE => (case p_scale v1 of Option.SOME n => (case p_register v2 of Option.SOME(sz,r) => (if sz = Z64 then Option.SOME(n,r) else NONE) | NONE => NONE) | NONE => NONE)) | _ => NONE; fun p_disp (b,s) = case p_imm32 s of Option.SOME imm => Option.SOME(b,imm) | NONE => NONE; fun p_rip_disp s = let val (l,r) = L3.splitl(fn c => not(Set.mem(c,[#"+",#"-"])),stripLeftSpaces s) in if l = "" then if r = "" then NONE else case p_rip_disp(L3.strTl r) of Option.SOME(ripfirst,imm) => (if (L3.strHd r) = #"+" then Option.SOME(ripfirst,imm) else if ripfirst then NONE else Option.SOME(false,BitsN.neg imm)) | NONE => NONE else if r = "" then if (stripSpaces l) = "rip" then Option.SOME(true,BitsN.B(0x0,64)) else NONE else if (stripSpaces l) = "rip" then p_disp(true,r) else if (stripSpaces(L3.strTl r)) = "rip" then p_disp(false,l) else NONE end; fun p_parts (m,s) = let val (v'0,(v'1,(v'2,v'3))) = (stripLeftSpaces s,m) in case (String.explode v'0,(v'1,(v'2,v'3))) of ([],_) => m | (#"-" :: t,(si,(b,disp))) => let val (l,r) = L3.splitl(fn c => not(Set.mem(c,[#"+",#"-"])),String.implode t) in case (p_imm32("-" ^ l),disp) of (NONE,_) => (NONE,(NONE,NONE)) | (Option.SOME imm2,Option.SOME imm1) => p_parts((si,(b,Option.SOME(BitsN.+(imm2,imm1)))),r) | (Option.SOME imm,NONE) => p_parts((si,(b,Option.SOME imm)),r) end | (#"+" :: t,(si,(b,disp))) => let val (l,r) = L3.splitl(fn c => not(Set.mem(c,[#"+",#"-"])),String.implode t) in case (p_imm32 l,disp) of (NONE,_) => (case (p_register l,(si,b)) of (Option.SOME(sz,rg),(_,NONE)) => (if sz = Z64 then p_parts((si,(Option.SOME rg,disp)),r) else (NONE,(NONE,NONE))) | (Option.SOME(sz,rg),(NONE,Option.SOME _)) => (if sz = Z64 then p_parts ((Option.SOME(BitsN.B(0x0,2),rg),(b,disp)),r) else (NONE,(NONE,NONE))) | (NONE,(NONE,_)) => (case p_scale_index l of NONE => (NONE,(NONE,NONE)) | si => p_parts((si,(b,disp)),r)) | (NONE,(Option.SOME(n1,r1),NONE)) => (case p_scale_index l of NONE => (NONE,(NONE,NONE)) | Option.SOME(n2,r2) => (if n1 = (BitsN.B(0x0,2)) then p_parts ((Option.SOME(n2,r2),(Option.SOME r1,disp)), r) else if n2 = (BitsN.B(0x0,2)) then p_parts ((Option.SOME(n1,r1),(Option.SOME r2,disp)), r) else (NONE,(NONE,NONE)))) | _ => (NONE,(NONE,NONE))) | (Option.SOME imm2,Option.SOME imm1) => p_parts((si,(b,Option.SOME(BitsN.+(imm2,imm1)))),r) | (Option.SOME imm,NONE) => p_parts((si,(b,Option.SOME imm)),r) end | (t,(si,(b,disp))) => let val (l,r) = L3.splitl(fn c => not(Set.mem(c,[#"+",#"-"])),String.implode t) in case (p_imm32 l,disp) of (NONE,_) => (case (p_register l,(si,b)) of (Option.SOME(sz,rg),(_,NONE)) => (if sz = Z64 then p_parts((si,(Option.SOME rg,disp)),r) else (NONE,(NONE,NONE))) | (Option.SOME(sz,rg),(NONE,Option.SOME _)) => (if sz = Z64 then p_parts ((Option.SOME(BitsN.B(0x0,2),rg),(b,disp)),r) else (NONE,(NONE,NONE))) | (NONE,(NONE,_)) => (case p_scale_index l of NONE => (NONE,(NONE,NONE)) | si => p_parts((si,(b,disp)),r)) | (NONE,(Option.SOME(n1,r1),NONE)) => (case p_scale_index l of NONE => (NONE,(NONE,NONE)) | Option.SOME(n2,r2) => (if n1 = (BitsN.B(0x0,2)) then p_parts ((Option.SOME(n2,r2),(Option.SOME r1,disp)), r) else if n2 = (BitsN.B(0x0,2)) then p_parts ((Option.SOME(n1,r1),(Option.SOME r2,disp)), r) else (NONE,(NONE,NONE)))) | _ => (NONE,(NONE,NONE))) | (Option.SOME imm2,Option.SOME imm1) => p_parts((si,(b,Option.SOME(BitsN.+(imm2,imm1)))),r) | (Option.SOME imm,NONE) => p_parts((si,(b,Option.SOME imm)),r) end end; fun p_mem_aux s = let val (si,(b,disp)) = case p_parts((NONE,(NONE,NONE)),s) of (Option.SOME(BitsN.B(0x0,_),r),(NONE,disp)) => (NONE,(Option.SOME r,disp)) | (Option.SOME(BitsN.B(0x0,_),RSP),(Option.SOME r,disp)) => (Option.SOME(BitsN.B(0x0,2),r),(Option.SOME RSP,disp)) | x => x in if (si = NONE) andalso ((b = NONE) andalso (disp = NONE)) then NONE else Option.SOME (si, (case b of Option.SOME r => ZregBase r | NONE => ZnoBase, case disp of Option.SOME imm => imm | NONE => BitsN.B(0x0,64))) end; fun p_mem s = let val (l,r) = L3.splitr(fn c => c = #"]",stripSpaces s) in if r = "]" then case p_mem_aux l of Option.SOME v => Option.SOME v | NONE => (case p_rip_disp l of Option.SOME(_,imm) => Option.SOME(NONE,(ZripBase,imm)) | NONE => NONE) else NONE end; fun p_rm s = case String.explode(stripSpaces s) of #"[" :: r => (case p_mem(String.implode r) of Option.SOME v => Option.SOME(Z64,Zm v) | NONE => NONE) | r => (case p_register(String.implode r) of Option.SOME(sz,r) => Option.SOME(sz,Zr r) | NONE => NONE); fun p_xmm s = case String.explode(stripSpaces s) of #"[" :: r => (case p_mem(String.implode r) of Option.SOME v => Option.SOME(xmm_mem v) | NONE => NONE) | r => (case p_xreg(String.implode r) of Option.SOME r => Option.SOME(xmm_reg r) | NONE => NONE); fun checkSizeDelim (sz,s) = case String.explode s of [] => Option.SOME sz | h :: _ => (if (Char.isSpace h) orelse (h = #"[") then Option.SOME sz else NONE); fun p_sz s = case String.explode(stripLeftSpaces s) of #"b" :: (#"y" :: (#"t" :: (#"e" :: r))) => let val r = String.implode r in (checkSizeDelim(Z8 false,r),r) end | #"w" :: (#"o" :: (#"r" :: (#"d" :: r))) => let val r = String.implode r in (checkSizeDelim(Z16,r),r) end | #"d" :: (#"w" :: (#"o" :: (#"r" :: (#"d" :: r)))) => let val r = String.implode r in (checkSizeDelim(Z32,r),r) end | #"q" :: (#"w" :: (#"o" :: (#"r" :: (#"d" :: r)))) => let val r = String.implode r in (checkSizeDelim(Z64,r),r) end | r => (NONE,String.implode r); fun s_sz sz = case sz of Z8 _ => "byte" | Z16 => "word" | Z32 => "dword" | Z64 => "qword"; fun p_sz_rm s = let val (sz1,r) = p_sz s in case p_rm r of Option.SOME(sz2,Zr r) => (case (sz1,sz2) of (Option.SOME(Z8 _),Z8 _) => "" | (NONE,_) => "" | (Option.SOME s1,_) => (if s1 = sz2 then "" else "cannot override register size"), (sz2,Zr r)) | Option.SOME(sz2,x) => (case sz1 of NONE => ("any size",(sz2,x)) | Option.SOME s1 => ("",(s1,x))) | NONE => ("syntax error",(Z16,Zr RAX)) end; fun check_sizes (sz1,(arg1,(sz2,arg2))) = if sz1 = sz2 then "" else case (sz1,(sz2,(arg1,arg2))) of (Z8 _,(Z8 _,(Option.SOME r1,Zr r2))) => (if (Set.mem(r1,[RSP,RBP,RSI,RDI])) andalso (Set.mem(r2,[RSP,RBP,RSI,RDI])) then "cannot mix high and low byte registers" else "") | _ => String.concat ["expecting ",s_sz sz1," value but got ",s_sz sz2," value"]; fun p_rm_of_size (sz,(arg1,s)) = case p_sz_rm s of ("any size",(_,rm)) => ("",rm) | ("",(sz2,rm)) => (check_sizes(sz,(arg1,(sz2,rm))),rm) | (err,_) => (err,Zr RAX); fun p_rm32 s = p_rm_of_size(Z32,(NONE,s)); fun p_rm64 s = p_rm_of_size(Z64,(NONE,s)); fun p_imm_rm s = case p_imm32 s of Option.SOME imm => ("",Zimm imm) | NONE => let val (err,rm) = p_rm64 s in (err,Zrm rm) end; fun p_dest_src (nfull_imm,(a,b)) = case p_sz_rm a of ("",(sz,Zr r)) => (case p_imm_of_size(sz,b) of Option.SOME imm => (if (sz = Z64) andalso (nfull_imm andalso (not((BitsN.signExtend 64 (BitsN.bits(31,0) imm)) = imm))) then ("syntax error: bad immediate",NONE) else ("",Option.SOME(sz,Zrm_i(Zr r,imm)))) | NONE => (case p_rm_of_size(sz,(Option.SOME r,b)) of ("",Zr r2) => ("",Option.SOME(sz,Zrm_r(Zr r,r2))) | ("",rm) => ("",Option.SOME(sz,Zr_rm(r,rm))) | (err,_) => (err,NONE))) | (message,(sz,Zm m)) => (case p_register b of Option.SOME(sz2,r) => (if (message = "any size") orelse (sz = sz2) then ("",Option.SOME(sz2,Zrm_r(Zm m,r))) else ("inconsistent sizes",NONE)) | NONE => (case p_imm_of_size(sz,b) of Option.SOME imm => (if (sz = Z64) andalso (not((BitsN.signExtend 64 (BitsN.bits(31,0) imm)) = imm)) then ("syntax error: bad immediate",NONE) else ("",Option.SOME(sz,Zrm_i(Zm m,imm)))) | NONE => ("syntax error",NONE))) | (err,_) => (err,NONE); fun p_cond s = case s of "o" => Option.SOME Z_O | "b" => Option.SOME Z_B | "c" => Option.SOME Z_B | "nae" => Option.SOME Z_B | "e" => Option.SOME Z_E | "z" => Option.SOME Z_E | "a" => Option.SOME Z_A | "nbe" => Option.SOME Z_A | "s" => Option.SOME Z_S | "p" => Option.SOME Z_P | "pe" => Option.SOME Z_P | "l" => Option.SOME Z_L | "nge" => Option.SOME Z_L | "g" => Option.SOME Z_G | "nle" => Option.SOME Z_G | "no" => Option.SOME Z_NO | "nb" => Option.SOME Z_NB | "nc" => Option.SOME Z_NB | "ae" => Option.SOME Z_NB | "ne" => Option.SOME Z_NE | "nz" => Option.SOME Z_NE | "na" => Option.SOME Z_NA | "be" => Option.SOME Z_NA | "ns" => Option.SOME Z_NS | "np" => Option.SOME Z_NP | "po" => Option.SOME Z_NP | "nl" => Option.SOME Z_NL | "ge" => Option.SOME Z_NL | "ng" => Option.SOME Z_NG | "le" => Option.SOME Z_NG | "" => Option.SOME Z_ALWAYS | _ => NONE; fun p_binop (bop,(a,b)) = case p_dest_src(true,(a,b)) of ("",Option.SOME(sz,dst_src)) => OK(Zbinop(bop,(sz,dst_src))) | ("",NONE) => FAIL "syntax error" | (err,_) => FAIL err; fun p_monop (opc,s) = let val (err,sz_rm) = p_sz_rm s in if (err = "") orelse (err = "any size") then case opc of 0 => OK(Zdiv sz_rm) | 1 => OK(Zidiv sz_rm) | 2 => OK(Zmul sz_rm) | 3 => OK(Zimul sz_rm) | 4 => OK(Zmonop(Zdec,sz_rm)) | 5 => OK(Zmonop(Zinc,sz_rm)) | 6 => OK(Zmonop(Znot,sz_rm)) | 7 => OK(Zmonop(Zneg,sz_rm)) | _ => FAIL "unsupported monop" else FAIL err end; fun p_xop (opc,(a,b)) = case p_register b of Option.SOME(sz,r) => let val (err,rm) = case p_rm a of Option.SOME(sz2,Zr r2) => (check_sizes(sz,(Option.SOME r,(sz2,Zr r2))),Zr r2) | Option.SOME(Z64,m) => ("",m) | _ => ("syntax error",Zm(NONE,(ZnoBase,BitsN.B(0x0,64)))) in if err = "" then let val arg = (sz,(rm,r)) in OK(case opc of 0 => Zxadd arg | 1 => Zxchg arg | _ => Zcmpxchg arg) end else FAIL err end | NONE => FAIL "syntax error"; fun p_imul3 (c,(sz,(r,rm))) = case p_imm8 c of Option.SOME imm8 => OK(Zimul3(sz,(r,(rm,imm8)))) | NONE => if sz = Z16 then case p_imm16 c of Option.SOME imm16 => OK(Zimul3(sz,(r,(rm,imm16)))) | NONE => FAIL "syntax error" else case p_imm32 c of Option.SOME imm32 => OK(Zimul3(sz,(r,(rm,imm32)))) | NONE => FAIL "syntax error"; fun p_sse (s,(a,b)) = case (p_xreg a,p_xmm b) of (Option.SOME dst,Option.SOME src) => let val a = (dst,src) val i = case s of "addpd" => bin_PD(sse_add,a) | "addps" => bin_PS(sse_add,a) | "addsd" => bin_SD(sse_add,a) | "addss" => bin_SS(sse_add,a) | "divpd" => bin_PD(sse_div,a) | "divps" => bin_PS(sse_div,a) | "divsd" => bin_SD(sse_div,a) | "divss" => bin_SS(sse_div,a) | "maxpd" => bin_PD(sse_max,a) | "maxps" => bin_PS(sse_max,a) | "maxsd" => bin_SD(sse_max,a) | "maxss" => bin_SS(sse_max,a) | "minpd" => bin_PD(sse_min,a) | "minps" => bin_PS(sse_min,a) | "minsd" => bin_SD(sse_min,a) | "minss" => bin_SS(sse_min,a) | "mulpd" => bin_PD(sse_mul,a) | "mulps" => bin_PS(sse_mul,a) | "mulsd" => bin_SD(sse_mul,a) | "mulss" => bin_SS(sse_mul,a) | "subpd" => bin_PD(sse_sub,a) | "subps" => bin_PS(sse_sub,a) | "subsd" => bin_SD(sse_sub,a) | "subss" => bin_SS(sse_sub,a) | "andpd" => logic_PD(sse_and,a) | "andps" => logic_PS(sse_and,a) | "andnpd" => logic_PD(sse_andn,a) | "andnps" => logic_PS(sse_andn,a) | "orpd" => logic_PD(sse_or,a) | "orps" => logic_PS(sse_or,a) | "xorpd" => logic_PD(sse_xor,a) | "xorps" => logic_PS(sse_xor,a) | "cmpeqpd" => CMPPD(sse_eq_oq,a) | "cmpeqps" => CMPPS(sse_eq_oq,a) | "cmpeqsd" => CMPSD(sse_eq_oq,a) | "cmpeqss" => CMPSS(sse_eq_oq,a) | "cmpltpd" => CMPPD(sse_lt_os,a) | "cmpltps" => CMPPS(sse_lt_os,a) | "cmpltsd" => CMPSD(sse_lt_os,a) | "cmpltss" => CMPSS(sse_lt_os,a) | "cmplepd" => CMPPD(sse_le_os,a) | "cmpleps" => CMPPS(sse_le_os,a) | "cmplesd" => CMPSD(sse_le_os,a) | "cmpless" => CMPSS(sse_le_os,a) | "cmpunordpd" => CMPPD(sse_unord_q,a) | "cmpunordps" => CMPPS(sse_unord_q,a) | "cmpunordsd" => CMPSD(sse_unord_q,a) | "cmpunordss" => CMPSS(sse_unord_q,a) | "cmpneqpd" => CMPPD(sse_neq_uq,a) | "cmpneqps" => CMPPS(sse_neq_uq,a) | "cmpneqsd" => CMPSD(sse_neq_uq,a) | "cmpneqss" => CMPSS(sse_neq_uq,a) | "cmpnltpd" => CMPPD(sse_nlt_us,a) | "cmpnltps" => CMPPS(sse_nlt_us,a) | "cmpnltsd" => CMPSD(sse_nlt_us,a) | "cmpnltss" => CMPSS(sse_nlt_us,a) | "cmpnlepd" => CMPPD(sse_nle_us,a) | "cmpnleps" => CMPPS(sse_nle_us,a) | "cmpnlesd" => CMPSD(sse_nle_us,a) | "cmpnless" => CMPSS(sse_nle_us,a) | "cmpordpd" => CMPPD(sse_ord_q,a) | "cmpordps" => CMPPS(sse_ord_q,a) | "cmpordsd" => CMPSD(sse_ord_q,a) | "cmpordss" => CMPSS(sse_ord_q,a) | "comisd" => COMISD a | "comiss" => COMISS a | "cvtdq2pd" => CVTDQ2PD a | "cvtdq2ps" => CVTDQ2PS a | "cvtpd2dq" => CVTPD2DQ(false,a) | "cvttpd2dq" => CVTPD2DQ(true,a) | "cvtpd2ps" => CVTPD2PS a | "cvtps2dq" => CVTPS2DQ(false,a) | "cvttps2dq" => CVTPS2DQ(true,a) | "cvtps2pd" => CVTPS2PD a | "cvtsd2ss" => CVTSD2SS a | "cvtss2sd" => CVTSS2SD a | "pcmpeqq" => PCMPEQQ a | "sqrtpd" => SQRTPD a | "sqrtsd" => SQRTPS a | "sqrtps" => SQRTSD a | "sqrtss" => SQRTSS a | _ => CMPPD (sse_eq_oq, (BitsN.B(0x0,3),xmm_mem(NONE,(ZnoBase,BitsN.B(0x0,64))))) in OK(SSE i) end | _ => FAIL("syntax error: SSE " ^ s); fun p_cvt_2si (double,(truncate,(a,b))) = case (p_register a,p_xmm b) of (Option.SOME(sz,r),Option.SOME x) => (if Set.mem(sz,[Z32,Z64]) then let val a = (truncate,(sz = Z64,(r,x))) in OK(SSE(if double then CVTSD2SI a else CVTSS2SI a)) end else FAIL "expecting 32-bit or 64-bit register destination") | _ => FAIL "syntax error"; fun p_cvtsi2 (double,(a,b)) = case (p_xreg a,p_rm b) of (Option.SOME r,Option.SOME(sz,rm)) => (if Set.mem(sz,[Z32,Z64]) then let val a = (sz = Z64,(r,rm)) in OK(SSE(if double then CVTSI2SD a else CVTSI2SS a)) end else FAIL "expecting 32-bit or 64-bit register source") | _ => FAIL "syntax error"; fun p_movap_movup (align,(double,(a,b))) = case (p_xmm a,p_xmm b) of (Option.SOME(xmm_mem _),Option.SOME(xmm_mem _)) => FAIL "syntax error" | (Option.SOME dst,Option.SOME src) => let val a = (double,(dst,src)) in OK(SSE(if align then MOVAP_D_S a else MOVUP_D_S a)) end | _ => FAIL "syntax error"; fun p_movsd_movss (double,(a,b)) = case (p_xmm a,p_xmm b) of (Option.SOME(xmm_mem _),Option.SOME(xmm_mem _)) => FAIL "syntax error" | (Option.SOME dst,Option.SOME src) => let val a = (dst,src) in OK(SSE(if double then MOVSD a else MOVSS a)) end | _ => FAIL "syntax error"; fun p_mov_d_q (quad,(a,b)) = let val sz = if quad then Z64 else Z32 in case p_xreg a of Option.SOME r => (case p_rm_of_size(sz,(NONE,b)) of ("",Zm m) => OK(SSE(if quad then MOVQ(xmm_reg r,xmm_mem m) else MOV_D_Q(true,(quad,(r,Zm m))))) | ("",rm) => OK(SSE(MOV_D_Q(true,(quad,(r,rm))))) | (s,_) => (case (quad,p_xreg b) of (true,Option.SOME t) => OK(SSE(MOVQ(xmm_reg r,xmm_reg t))) | _ => FAIL s)) | NONE => (case (p_rm_of_size(sz,(NONE,a)),(quad,p_xreg b)) of (("",Zm m),(true,Option.SOME r)) => OK(SSE(MOVQ(xmm_mem m,xmm_reg r))) | (("",rm),(_,Option.SOME r)) => OK(SSE(MOV_D_Q(false,(quad,(r,rm))))) | ((s,_),(_,Option.SOME _)) => FAIL s | _ => FAIL "syntax error") end; fun p_pshift (n,(a,b)) = case (p_xreg a,p_number b) of (Option.SOME r,Option.SOME i) => (if Nat.<(i,256) then let val a = (r,BitsN.fromNat(i,8)) in OK(SSE(case n of BitsN.B(0x0,_) => PSRLW_imm a | BitsN.B(0x1,_) => PSRAW_imm a | BitsN.B(0x2,_) => PSLLW_imm a | BitsN.B(0x3,_) => PSRLD_imm a | BitsN.B(0x4,_) => PSRAD_imm a | BitsN.B(0x5,_) => PSLLD_imm a | BitsN.B(0x6,_) => PSRLQ_imm a | BitsN.B(0x7,_) => PSLLQ_imm a | BitsN.B(0x8,_) => PSLLDQ a | _ => PSRLDQ a)) end else FAIL "syntax error: expecting byte immediate") | _ => FAIL "syntax error"; fun p_tokens s = let val (l,r) = L3.splitl (fn c => not(Char.isSpace c), L3.lowercase(L3.snd(L3.splitl(fn c => Char.isSpace c,s)))) val r = L3.uncurry String.fields (fn c => c = #",",r) val r = if ((L3.length r) = 1) andalso ((stripSpaces(List.hd r)) = "") then [] else r in l :: r end; fun instructionFromString s = let val toks = p_tokens s in case toks of v'0 :: v'1 => (case v'1 of v'4 :: v'5 => (case ((String.explode v'4,v'5),String.explode v'0) of ((a,[b]),[#"o",#"r"]) => p_binop(Zor,(String.implode a,b)) | ((a,[b]),[#"a",#"d",#"d"]) => p_binop(Zadd,(String.implode a,b)) | ((a,[b]),[#"a",#"d",#"c"]) => p_binop(Zadc,(String.implode a,b)) | ((a,[b]),[#"s",#"b",#"b"]) => p_binop(Zsbb,(String.implode a,b)) | ((a,[b]),[#"a",#"n",#"d"]) => p_binop(Zand,(String.implode a,b)) | ((a,[b]),[#"s",#"u",#"b"]) => p_binop(Zsub,(String.implode a,b)) | ((a,[b]),[#"x",#"o",#"r"]) => p_binop(Zxor,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p"]) => p_binop(Zcmp,(String.implode a,b)) | ((a,[b]),[#"r",#"o",#"l"]) => p_binop(Zrol,(String.implode a,b)) | ((a,[b]),[#"r",#"o",#"r"]) => p_binop(Zror,(String.implode a,b)) | ((a,[b]),[#"r",#"c",#"l"]) => p_binop(Zrcl,(String.implode a,b)) | ((a,[b]),[#"r",#"c",#"r"]) => p_binop(Zrcr,(String.implode a,b)) | ((a,[b]),[#"s",#"h",#"l"]) => p_binop(Zshl,(String.implode a,b)) | ((a,[b]),[#"s",#"h",#"r"]) => p_binop(Zshr,(String.implode a,b)) | ((a,[b]),[#"s",#"a",#"r"]) => p_binop(Zsar,(String.implode a,b)) | ((a,[b]),[#"t",#"e",#"s",#"t"]) => p_binop(Ztest,(String.implode a,b)) | ((a,[]),#"s" :: (#"e" :: (#"t" :: cond))) => let val cond = String.implode cond in case p_cond cond of Option.SOME c => (case p_sz_rm(String.implode a) of ("",(Z8 have_rex,rm)) => OK(Zset(c,(have_rex,rm))) | ("any size",(Z8 have_rex,rm)) => OK(Zset(c,(have_rex,rm))) | ("any size",_) => FAIL "SETcc requires byte source" | (err,_) => FAIL err) | NONE => FAIL (String.concat ["Unrecognised mnemonic: ","set",cond]) end | ((a,[]),[#"c",#"a",#"l",#"l"]) => let val a = String.implode a in case p_imm_rm a of ("",Zimm imm) => OK(Zcall(Zimm(BitsN.-(imm,BitsN.B(0x5,64))))) | ("",Zrm rm) => OK(Zcall(Zrm rm)) | (err,_) => (case p_label a of Option.SOME l => PENDING(l,Zcall(Zimm(BitsN.B(0x0,64)))) | NONE => FAIL err) end | ((a,[]),[#"p",#"u",#"s",#"h"]) => (case p_imm_rm(String.implode a) of ("",x) => OK(Zpush x) | (err,_) => FAIL err) | ((a,[]),[#"p",#"o",#"p"]) => (case p_rm64(String.implode a) of ("",rm) => OK(Zpop rm) | (err,_) => FAIL err) | ((a,[]),#"j" :: cond) => let val a = String.implode a val cond = String.implode cond val condition = if cond = "mp" then Option.SOME Z_ALWAYS else if cond = "" then NONE else p_cond cond in case condition of Option.SOME c => (case p_imm_rm a of ("",Zrm rm) => (if c = Z_ALWAYS then OK(Zjmp rm) else FAIL "syntax error") | ("",Zimm imm) => let val ast = Zjcc(c,BitsN.-(imm,BitsN.B(0x2,64))) in if (L3.length(encode ast)) = 2 then OK ast else OK(Zjcc (c, BitsN.- (imm, if c = Z_ALWAYS then BitsN.B(0x5,64) else BitsN.B(0x6,64)))) end | (err,_) => let val (sz,b) = p_sz a val far = case sz of Option.SOME Z32 => true | _ => false in case p_label b of Option.SOME l => PENDING (l,Zjcc(c,BitsN.fromBool 64 far)) | NONE => FAIL err end) | NONE => FAIL (String.concat ["Unrecognised mnemonic: ","j",cond]) end | ((a,[]),[#"d",#"i",#"v"]) => p_monop(0,String.implode a) | ((a,[]),[#"i",#"d",#"i",#"v"]) => p_monop(1,String.implode a) | ((a,[]),[#"m",#"u",#"l"]) => p_monop(2,String.implode a) | ((a,[]),[#"i",#"m",#"u",#"l"]) => p_monop(3,String.implode a) | ((a,[]),[#"d",#"e",#"c"]) => p_monop(4,String.implode a) | ((a,[]),[#"i",#"n",#"c"]) => p_monop(5,String.implode a) | ((a,[]),[#"n",#"o",#"t"]) => p_monop(6,String.implode a) | ((a,[]),[#"n",#"e",#"g"]) => p_monop(7,String.implode a) | ((i,[]),[#"r",#"e",#"t"]) => (case p_imm16(String.implode i) of Option.SOME imm => OK(Zret imm) | NONE => FAIL "syntax error: bad immediate") | ((i,[]),#"l" :: (#"o" :: (#"o" :: (#"p" :: cond)))) => let val i = String.implode i val cond = String.implode cond in case p_cond cond of Option.SOME c => (if Set.mem(c,[Z_ALWAYS,Z_E,Z_NE]) then case p_imm8 i of Option.SOME imm => OK(Zloop (c, BitsN.-(imm,BitsN.B(0x2,64)))) | NONE => (case p_label i of Option.SOME l => PENDING (l,Zloop(c,BitsN.B(0x0,64))) | NONE => FAIL "syntax error: bad immediate") else FAIL "bad condition") | NONE => FAIL (String.concat ["Unrecognised mnemonic: ","loop",cond]) end | ((a,[b]),#"b" :: (#"t" :: s)) => let val s = String.implode s in if Set.mem(s,["","s","r","c"]) then let val bt = Cast.stringToZbit_test_name (String.concat["Z","bt",s]) in case p_dest_src(false,(String.implode a,b)) of ("",Option.SOME(Z8 _,_)) => FAIL "syntax error" | ("",Option.SOME(_,Zr_rm _)) => FAIL "syntax error" | ("",Option.SOME(sz,Zrm_i(rm,i))) => (if (BitsN.<= (BitsN.neg(BitsN.B(0x80,64)),i)) andalso (BitsN.<=(i,BitsN.B(0xFF,64))) then OK(Zbit_test(bt,(sz,Zrm_i(rm,i)))) else FAIL "syntax error: expecting byte immediate") | ("",Option.SOME(sz,ds)) => OK(Zbit_test(bt,(sz,ds))) | ("",NONE) => FAIL "syntax error" | (err,_) => FAIL err end else FAIL (String.concat ["Unrecognised mnemonic: ","bt",s]) end | ((a,[b]),[#"i",#"m",#"u",#"l"]) => (case p_dest_src(false,(String.implode a,b)) of ("",Option.SOME(Z8 _,_)) => FAIL "syntax error" | ("",Option.SOME(sz,Zrm_r(Zr r1,r2))) => OK(Zimul2(sz,(r1,Zr r2))) | ("",Option.SOME(sz,Zr_rm(r,rm))) => OK(Zimul2(sz,(r,rm))) | ("",NONE) => FAIL "syntax error" | (err,_) => FAIL err) | ((a,[b,c]),[#"i",#"m",#"u",#"l"]) => (case p_dest_src(false,(String.implode a,b)) of ("",Option.SOME(Z8 _,_)) => FAIL "syntax error" | ("",Option.SOME(sz,Zrm_r(Zr r1,r2))) => p_imul3(c,(sz,(r1,Zr r2))) | ("",Option.SOME(sz,Zr_rm(r,rm))) => p_imul3(c,(sz,(r,rm))) | ("",NONE) => FAIL "syntax error" | (err,_) => FAIL err) | ((a,[b]),[#"m",#"o",#"v",#"z",#"x"]) => (case p_register(String.implode a) of Option.SOME(sz2,r) => let val (message,(sz1,rm)) = p_sz_rm b in if (message = "") orelse (message = "any size") then OK(Zmovzx(sz1,(Zr_rm(r,rm),sz2))) else FAIL message end | NONE => FAIL "syntax error") | ((a,[b]),[#"m",#"o",#"v",#"s",#"x"]) => (case p_register(String.implode a) of Option.SOME(sz2,r) => let val (message,(sz1,rm)) = p_sz_rm b in if (message = "") orelse (message = "any size") then if (sz1 = Z32) andalso (sz2 = Z64) then FAIL "movsx used instead of movsxd" else OK(Zmovsx(sz1,(Zr_rm(r,rm),sz2))) else FAIL message end | NONE => FAIL "syntax error") | ((a,[b]),[#"m",#"o",#"v",#"s",#"x",#"d"]) => (case p_register(String.implode a) of Option.SOME(Z64,r) => (case p_rm32 b of ("",rm) => OK(Zmovsx(Z32,(Zr_rm(r,rm),Z64))) | (err,_) => FAIL err) | Option.SOME _ => FAIL "destination must be a 64-bit register" | NONE => FAIL "syntax error") | ((a,[b]),[#"m",#"o",#"v"]) => (case p_dest_src(false,(String.implode a,b)) of ("",Option.SOME(sz,dst_src)) => OK(Zmov(Z_ALWAYS,(sz,dst_src))) | ("",NONE) => FAIL "syntax error" | (err,_) => FAIL err) | ((a,[b]),#"c" :: (#"m" :: (#"o" :: (#"v" :: cond)))) => let val cond = String.implode cond in case p_cond cond of Option.SOME Z_ALWAYS => FAIL (String.concat ["Unrecognised mnemonic: ","cmov",cond]) | Option.SOME c => (case p_dest_src(true,(String.implode a,b)) of ("",Option.SOME(Z8 _,_)) => FAIL "syntax error" | ("",Option.SOME(sz,Zrm_r(Zr r1,r2))) => OK(Zmov(c,(sz,Zr_rm(r1,Zr r2)))) | ("",Option.SOME(sz,Zr_rm(r,rm))) => OK(Zmov(c,(sz,Zr_rm(r,rm)))) | ("",_) => FAIL "syntax error" | (err,_) => FAIL err) | NONE => FAIL (String.concat ["Unrecognised mnemonic: ","cmov",cond]) end | ((a,[b]),[#"l",#"e",#"a"]) => (case p_register(String.implode a) of Option.SOME(Z8 _,r) => FAIL "syntax error" | Option.SOME(sz,r) => (case p_rm b of Option.SOME(Z64,Zm m) => OK(Zlea(sz,Zr_rm(r,Zm m))) | _ => FAIL "syntax error") | NONE => FAIL "syntax error") | ((a,[b]),[#"x",#"a",#"d",#"d"]) => p_xop(0,(String.implode a,b)) | ((a,[b]),[#"x",#"c",#"h",#"g"]) => p_xop(1,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"x",#"c",#"h",#"g"]) => p_xop(2,(String.implode a,b)) | ((a,[b]),[#"a",#"d",#"d",#"p",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"a",#"d",#"d",#"p",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"a",#"d",#"d",#"s",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"a",#"d",#"d",#"s",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"d",#"i",#"v",#"p",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"d",#"i",#"v",#"p",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"d",#"i",#"v",#"s",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"d",#"i",#"v",#"s",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"m",#"a",#"x",#"p",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"m",#"a",#"x",#"p",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"m",#"a",#"x",#"s",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"m",#"a",#"x",#"s",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"m",#"i",#"n",#"p",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"m",#"i",#"n",#"p",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"m",#"i",#"n",#"s",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"m",#"i",#"n",#"s",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"m",#"u",#"l",#"p",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"m",#"u",#"l",#"p",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"m",#"u",#"l",#"s",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"m",#"u",#"l",#"s",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"s",#"u",#"b",#"p",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"s",#"u",#"b",#"p",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"s",#"u",#"b",#"s",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"s",#"u",#"b",#"s",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"a",#"n",#"d",#"p",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"a",#"n",#"d",#"p",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"a",#"n",#"d",#"n",#"p",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"a",#"n",#"d",#"n",#"p",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"o",#"r",#"p",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"o",#"r",#"p",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"x",#"o",#"r",#"p",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"x",#"o",#"r",#"p",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"e",#"q",#"p",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"e",#"q",#"p",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"e",#"q",#"s",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"e",#"q",#"s",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"l",#"t",#"p",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"l",#"t",#"p",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"l",#"t",#"s",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"l",#"t",#"s",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"l",#"e",#"p",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"l",#"e",#"p",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"l",#"e",#"s",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"l",#"e",#"s",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]), [#"c",#"m",#"p",#"u",#"n",#"o",#"r",#"d",#"p",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]), [#"c",#"m",#"p",#"u",#"n",#"o",#"r",#"d",#"p",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]), [#"c",#"m",#"p",#"u",#"n",#"o",#"r",#"d",#"s",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]), [#"c",#"m",#"p",#"u",#"n",#"o",#"r",#"d",#"s",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"n",#"e",#"q",#"p",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"n",#"e",#"q",#"p",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"n",#"e",#"q",#"s",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"n",#"e",#"q",#"s",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"n",#"l",#"t",#"p",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"n",#"l",#"t",#"p",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"n",#"l",#"t",#"s",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"n",#"l",#"t",#"s",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"n",#"l",#"e",#"p",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"n",#"l",#"e",#"p",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"n",#"l",#"e",#"s",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"n",#"l",#"e",#"s",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"o",#"r",#"d",#"p",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"o",#"r",#"d",#"p",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"o",#"r",#"d",#"s",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"m",#"p",#"o",#"r",#"d",#"s",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"o",#"m",#"i",#"s",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"o",#"m",#"i",#"s",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"v",#"t",#"d",#"q",#"2",#"p",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"v",#"t",#"d",#"q",#"2",#"p",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"v",#"t",#"p",#"d",#"2",#"d",#"q"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"v",#"t",#"t",#"p",#"d",#"2",#"d",#"q"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"v",#"t",#"p",#"d",#"2",#"p",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"v",#"t",#"p",#"s",#"2",#"d",#"q"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"v",#"t",#"t",#"p",#"s",#"2",#"d",#"q"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"v",#"t",#"p",#"s",#"2",#"p",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"v",#"t",#"s",#"d",#"2",#"s",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"v",#"t",#"s",#"s",#"2",#"s",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"c",#"v",#"t",#"s",#"d",#"2",#"s",#"i"]) => p_cvt_2si(true,(false,(String.implode a,b))) | ((a,[b]),[#"c",#"v",#"t",#"t",#"s",#"d",#"2",#"s",#"i"]) => p_cvt_2si(true,(true,(String.implode a,b))) | ((a,[b]),[#"c",#"v",#"t",#"s",#"s",#"2",#"s",#"i"]) => p_cvt_2si(false,(false,(String.implode a,b))) | ((a,[b]),[#"c",#"v",#"t",#"t",#"s",#"s",#"2",#"s",#"i"]) => p_cvt_2si(false,(true,(String.implode a,b))) | ((a,[b]),[#"c",#"v",#"t",#"s",#"i",#"2",#"s",#"d"]) => p_cvtsi2(true,(String.implode a,b)) | ((a,[b]),[#"c",#"v",#"t",#"s",#"i",#"2",#"s",#"s"]) => p_cvtsi2(false,(String.implode a,b)) | ((a,[b]),[#"m",#"o",#"v",#"a",#"p",#"d"]) => p_movap_movup(true,(true,(String.implode a,b))) | ((a,[b]),[#"m",#"o",#"v",#"a",#"p",#"s"]) => p_movap_movup(true,(false,(String.implode a,b))) | ((a,[b]),[#"m",#"o",#"v",#"u",#"p",#"d"]) => p_movap_movup(false,(true,(String.implode a,b))) | ((a,[b]),[#"m",#"o",#"v",#"u",#"p",#"s"]) => p_movap_movup(false,(false,(String.implode a,b))) | ((a,[b]),[#"m",#"o",#"v",#"s",#"d"]) => p_movsd_movss(true,(String.implode a,b)) | ((a,[b]),[#"m",#"o",#"v",#"s",#"s"]) => p_movsd_movss(false,(String.implode a,b)) | ((a,[b]),[#"m",#"o",#"v",#"d"]) => p_mov_d_q(false,(String.implode a,b)) | ((a,[b]),[#"m",#"o",#"v",#"q"]) => p_mov_d_q(true,(String.implode a,b)) | ((a,[b]),[#"p",#"c",#"m",#"p",#"e",#"q",#"q"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"p",#"s",#"r",#"l",#"w"]) => p_pshift(BitsN.B(0x0,4),(String.implode a,b)) | ((a,[b]),[#"p",#"s",#"r",#"a",#"w"]) => p_pshift(BitsN.B(0x1,4),(String.implode a,b)) | ((a,[b]),[#"p",#"s",#"l",#"l",#"w"]) => p_pshift(BitsN.B(0x2,4),(String.implode a,b)) | ((a,[b]),[#"p",#"s",#"r",#"l",#"d"]) => p_pshift(BitsN.B(0x3,4),(String.implode a,b)) | ((a,[b]),[#"p",#"s",#"r",#"a",#"d"]) => p_pshift(BitsN.B(0x4,4),(String.implode a,b)) | ((a,[b]),[#"p",#"s",#"l",#"l",#"d"]) => p_pshift(BitsN.B(0x5,4),(String.implode a,b)) | ((a,[b]),[#"p",#"s",#"r",#"l",#"q"]) => p_pshift(BitsN.B(0x6,4),(String.implode a,b)) | ((a,[b]),[#"p",#"s",#"l",#"l",#"q"]) => p_pshift(BitsN.B(0x7,4),(String.implode a,b)) | ((a,[b]),[#"p",#"s",#"l",#"l",#"d",#"q"]) => p_pshift(BitsN.B(0x8,4),(String.implode a,b)) | ((a,[b]),[#"p",#"s",#"r",#"l",#"d",#"q"]) => p_pshift(BitsN.B(0x9,4),(String.implode a,b)) | ((a,[b]),[#"s",#"q",#"r",#"t",#"p",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"s",#"q",#"r",#"t",#"p",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"s",#"q",#"r",#"t",#"s",#"d"]) => p_sse(List.hd toks,(String.implode a,b)) | ((a,[b]),[#"s",#"q",#"r",#"t",#"s",#"s"]) => p_sse(List.hd toks,(String.implode a,b)) | ((s :: l,[]),[#"b",#"y",#"t",#"e",#"s"]) => (if Char.isSpace s then case p_bytes(String.implode l) of Option.SOME bs => STREAM bs | NONE => FAIL "bad byte list" else FAIL "syntax error") | ((v'7,v'8),v'2) => FAIL ("Unrecognised mnemonic or wrong number of args: " ^ s)) | [] => (case v'0 of "cmc" => OK Zcmc | "clc" => OK Zclc | "stc" => OK Zstc | "leave" => OK Zleave | "nop" => OK(Znop 1) | "ret" => OK(Zret(BitsN.B(0x0,64))) | v'2 => FAIL ("Unrecognised mnemonic or wrong number of args: " ^ s))) | _ => FAIL("Unrecognised mnemonic or wrong number of args: " ^ s) end; fun s_register (sz,r) = case (sz,r) of (Z8 _,RAX) => "al" | (Z8 _,RCX) => "cl" | (Z8 _,RDX) => "dl" | (Z8 _,RBX) => "bl" | (Z8 false,RSP) => "ah" | (Z8 false,RBP) => "ch" | (Z8 false,RSI) => "dh" | (Z8 false,RDI) => "bh" | (Z8 true,RSP) => "spl" | (Z8 true,RBP) => "bpl" | (Z8 true,RSI) => "sil" | (Z8 true,RDI) => "dil" | (Z8 _,zR8) => "r8b" | (Z8 _,zR9) => "r9b" | (Z8 _,zR10) => "r10b" | (Z8 _,zR11) => "r11b" | (Z8 _,zR12) => "r12b" | (Z8 _,zR13) => "r13b" | (Z8 _,zR14) => "r14b" | (Z8 _,zR15) => "r15b" | (Z16,RAX) => "ax" | (Z16,RCX) => "cx" | (Z16,RDX) => "dx" | (Z16,RBX) => "bx" | (Z16,RSP) => "sp" | (Z16,RBP) => "bp" | (Z16,RSI) => "si" | (Z16,RDI) => "di" | (Z16,zR8) => "r8w" | (Z16,zR9) => "r9w" | (Z16,zR10) => "r10w" | (Z16,zR11) => "r11w" | (Z16,zR12) => "r12w" | (Z16,zR13) => "r13w" | (Z16,zR14) => "r14w" | (Z16,zR15) => "r15w" | (Z32,RAX) => "eax" | (Z32,RCX) => "ecx" | (Z32,RDX) => "edx" | (Z32,RBX) => "ebx" | (Z32,RSP) => "esp" | (Z32,RBP) => "ebp" | (Z32,RSI) => "esi" | (Z32,RDI) => "edi" | (Z32,zR8) => "r8d" | (Z32,zR9) => "r9d" | (Z32,zR10) => "r10d" | (Z32,zR11) => "r11d" | (Z32,zR12) => "r12d" | (Z32,zR13) => "r13d" | (Z32,zR14) => "r14d" | (Z32,zR15) => "r15d" | (Z64,RAX) => "rax" | (Z64,RCX) => "rcx" | (Z64,RDX) => "rdx" | (Z64,RBX) => "rbx" | (Z64,RSP) => "rsp" | (Z64,RBP) => "rbp" | (Z64,RSI) => "rsi" | (Z64,RDI) => "rdi" | (Z64,zR8) => "r8" | (Z64,zR9) => "r9" | (Z64,zR10) => "r10" | (Z64,zR11) => "r11" | (Z64,zR12) => "r12" | (Z64,zR13) => "r13" | (Z64,zR14) => "r14" | (Z64,zR15) => "r15"; fun s_qword q = if BitsN.<(q,BitsN.B(0x0,64)) then "-0x" ^ (BitsN.toHexString(BitsN.neg q)) else "0x" ^ (BitsN.toHexString q); fun s_qword0 q = if q = (BitsN.B(0x0,64)) then "" else if BitsN.<(q,BitsN.B(0x0,64)) then "-0x" ^ (BitsN.toHexString(BitsN.neg q)) else "+0x" ^ (BitsN.toHexString q); fun s_sib (scale,idx) = (s_register(Z64,idx)) ^ (if scale = (BitsN.B(0x0,2)) then "" else "*" ^ (Nat.toString(Nat.pow(2,BitsN.toNat scale)))); fun s_mem m = case m of (NONE,(ZripBase,imm)) => String.concat["[rip",s_qword0 imm,"]"] | (NONE,(ZnoBase,imm)) => String.concat["[",s_qword imm,"]"] | (NONE,(ZregBase base,imm)) => String.concat["[",s_register(Z64,base),s_qword0 imm,"]"] | (Option.SOME(scale,idx),(ZnoBase,imm)) => String.concat["[",s_sib(scale,idx),s_qword0 imm,"]"] | (Option.SOME(scale,idx),(ZregBase base,imm)) => String.concat ["[",s_register(Z64,base),"+",s_sib(scale,idx),s_qword0 imm,"]"] | _ => "[invalid]"; fun s_rm (sz,rm) = case rm of Zr r => s_register(sz,r) | Zm m => s_mem m; fun s_xreg r = "xmm" ^ (Nat.toString(BitsN.toNat r)); fun s_xmm_mem x = case x of xmm_reg r => s_xreg r | xmm_mem m => s_mem m; fun s_xmm (r,x) = String.concat[s_xreg r,", ",s_xmm_mem x]; fun s_imm_rm x = case x of Zrm rm => s_rm(Z64,rm) | Zimm imm => s_qword imm; fun s_sz_rm (sz,rm) = case rm of Zr _ => s_rm(sz,rm) | _ => (if sz = Z64 then s_rm(sz,rm) else String.concat[s_sz sz," ",s_rm(Z64,rm)]); fun s_dest_src (sz,ds) = case ds of Zrm_r(rm,r) => String.concat[s_rm(sz,rm),", ",s_register(sz,r)] | Zr_rm(r,rm) => String.concat[s_register(sz,r),", ",s_rm(sz,rm)] | Zrm_i(rm,i) => String.concat[s_sz_rm(sz,rm),", ",s_qword i]; fun s_cond c = case c of Z_O => "o" | Z_B => "b" | Z_E => "e" | Z_A => "a" | Z_S => "s" | Z_P => "p" | Z_L => "l" | Z_G => "g" | Z_NO => "no" | Z_NB => "nb" | Z_NE => "ne" | Z_NA => "na" | Z_NS => "ns" | Z_NP => "np" | Z_NL => "nl" | Z_NG => "ng" | Z_ALWAYS => ""; fun s_sse_binop n = L3.dropString(4,Cast.sse_binopToString n); fun s_sse_logic n = L3.dropString(4,Cast.sse_logicToString n); fun s_sse_compare n = L3.fst (L3.splitl (fn c => not(c = #"_"),L3.dropString(4,Cast.sse_compareToString n))); fun sse_instructionToString i = case i of bin_PD(bop,(dst,src)) => ((s_sse_binop bop) ^ "pd",s_xmm(dst,src)) | bin_PS(bop,(dst,src)) => ((s_sse_binop bop) ^ "ps",s_xmm(dst,src)) | bin_SD(bop,(dst,src)) => ((s_sse_binop bop) ^ "sd",s_xmm(dst,src)) | bin_SS(bop,(dst,src)) => ((s_sse_binop bop) ^ "ss",s_xmm(dst,src)) | logic_PD(bop,(dst,src)) => ((s_sse_logic bop) ^ "pd",s_xmm(dst,src)) | logic_PS(bop,(dst,src)) => ((s_sse_logic bop) ^ "ps",s_xmm(dst,src)) | CMPPD(bop,(dst,src)) => (String.concat["cmp",s_sse_compare bop,"pd"],s_xmm(dst,src)) | CMPPS(bop,(dst,src)) => (String.concat["cmp",s_sse_compare bop,"ps"],s_xmm(dst,src)) | CMPSD(bop,(dst,src)) => (String.concat["cmp",s_sse_compare bop,"sd"],s_xmm(dst,src)) | CMPSS(bop,(dst,src)) => (String.concat["cmp",s_sse_compare bop,"ss"],s_xmm(dst,src)) | COMISD(src1,src2) => ("comisd",s_xmm(src1,src2)) | COMISS(src1,src2) => ("comiss",s_xmm(src1,src2)) | CVTDQ2PD(dst,src) => ("cvtdq2pd",s_xmm(dst,src)) | CVTDQ2PS(dst,src) => ("cvtdq2ps",s_xmm(dst,src)) | CVTPD2DQ(false,(dst,src)) => ("cvtpd2dq",s_xmm(dst,src)) | CVTPD2DQ(true,(dst,src)) => ("cvttpd2dq",s_xmm(dst,src)) | CVTPD2PS(dst,src) => ("cvtpd2ps",s_xmm(dst,src)) | CVTPS2DQ(false,(dst,src)) => ("cvtps2dq",s_xmm(dst,src)) | CVTPS2DQ(true,(dst,src)) => ("cvttps2dq",s_xmm(dst,src)) | CVTPS2PD(dst,src) => ("cvtps2pd",s_xmm(dst,src)) | CVTSD2SI(truncate,(quad,(dst,src))) => (String.concat["cvt",if truncate then "t" else "","sd2si"], String.concat [s_register(if quad then Z64 else Z32,dst),", ",s_xmm_mem src]) | CVTSD2SS(dst,src) => ("cvtsd2ss",s_xmm(dst,src)) | CVTSI2SD(quad,(dst,src)) => ("cvtsi2sd", String.concat[s_xreg dst,", ",s_rm(if quad then Z64 else Z32,src)]) | CVTSI2SS(quad,(dst,src)) => ("cvtsi2ss", String.concat[s_xreg dst,", ",s_rm(if quad then Z64 else Z32,src)]) | CVTSS2SD(dst,src) => ("cvtss2sd",s_xmm(dst,src)) | CVTSS2SI(truncate,(quad,(dst,src))) => (String.concat["cvt",if truncate then "t" else "","ss2si"], String.concat [s_register(if quad then Z64 else Z32,dst),", ",s_xmm_mem src]) | MOVAP_D_S(double,(dst,src)) => ("movap" ^ (if double then "d" else "s"), String.concat[s_xmm_mem dst,", ",s_xmm_mem src]) | MOVUP_D_S(double,(dst,src)) => ("movup" ^ (if double then "d" else "s"), String.concat[s_xmm_mem dst,", ",s_xmm_mem src]) | MOV_D_Q(to_xmm,(quad,(xmm,rm))) => ("mov" ^ (if quad then "q" else "d"), if to_xmm then String.concat [s_xreg xmm,", ",s_rm(if quad then Z64 else Z32,rm)] else String.concat [s_rm(if quad then Z64 else Z32,rm),", ",s_xreg xmm]) | MOVSD(dst,src) => ("movsd",String.concat[s_xmm_mem dst,", ",s_xmm_mem src]) | MOVSS(dst,src) => ("movss",String.concat[s_xmm_mem dst,", ",s_xmm_mem src]) | MOVQ(dst,src) => ("movq",String.concat[s_xmm_mem dst,", ",s_xmm_mem src]) | PCMPEQQ(dst,src) => ("pcmpeqq",s_xmm(dst,src)) | PSRLW_imm(dst,i) => ("psrlw",String.concat[s_xreg dst,", ",BitsN.toHexString i]) | PSRAW_imm(dst,i) => ("psraw",String.concat[s_xreg dst,", ",BitsN.toHexString i]) | PSLLW_imm(dst,i) => ("psllw",String.concat[s_xreg dst,", ",BitsN.toHexString i]) | PSRLD_imm(dst,i) => ("psrld",String.concat[s_xreg dst,", ",BitsN.toHexString i]) | PSRAD_imm(dst,i) => ("psrad",String.concat[s_xreg dst,", ",BitsN.toHexString i]) | PSLLD_imm(dst,i) => ("pslld",String.concat[s_xreg dst,", ",BitsN.toHexString i]) | PSRLQ_imm(dst,i) => ("psrlq",String.concat[s_xreg dst,", ",BitsN.toHexString i]) | PSLLQ_imm(dst,i) => ("psllq",String.concat[s_xreg dst,", ",BitsN.toHexString i]) | PSRLDQ(dst,i) => ("psrldq",String.concat[s_xreg dst,", ",BitsN.toHexString i]) | PSLLDQ(dst,i) => ("pslldq",String.concat[s_xreg dst,", ",BitsN.toHexString i]) | SQRTPD(dst,src) => ("sqrtpd",s_xmm(dst,src)) | SQRTPS(dst,src) => ("sqrtps",s_xmm(dst,src)) | SQRTSD(dst,src) => ("sqrtsd",s_xmm(dst,src)) | SQRTSS(dst,src) => ("sqrtss",s_xmm(dst,src)); fun instructionToString (i,width) = case i of SSE j => sse_instructionToString j | Zbinop(bop,(sz,dst_src)) => (L3.strTl(Cast.Zbinop_nameToString bop),s_dest_src(sz,dst_src)) | Zbit_test(bt,(sz,dst_src)) => (L3.strTl(Cast.Zbit_test_nameToString bt),s_dest_src(sz,dst_src)) | Zcall(Zimm imm) => ("call",s_qword(BitsN.+(imm,BitsN.fromNat(width,64)))) | Zcall(Zrm rm) => ("call",s_rm(Z64,rm)) | Zcmc => ("cmc","") | Zclc => ("clc","") | Zstc => ("stc","") | Zcmpxchg(sz,(rm,r)) => ("cmpxchg",String.concat[s_rm(sz,rm),", ",s_register(sz,r)]) | Zdiv sz_rm => ("div",s_sz_rm sz_rm) | Zidiv sz_rm => ("idiv",s_sz_rm sz_rm) | Zjcc(Z_ALWAYS,imm) => ("jmp",s_qword(BitsN.+(imm,BitsN.fromNat(width,64)))) | Zjcc(cond,imm) => ("j" ^ (s_cond cond),s_qword(BitsN.+(imm,BitsN.fromNat(width,64)))) | Zjmp rm => ("jmp",s_rm(Z64,rm)) | Zlea(Z8 _,_) => ("?lea?","") | Zlea(sz,Zr_rm(r,Zm m)) => ("lea",String.concat[s_register(sz,r),", ",s_rm(Z64,Zm m)]) | Zlea _ => ("?lea?","") | Zleave => ("leave","") | Zloop(Z_NE,imm) => ("loopne",s_qword(BitsN.+(imm,BitsN.fromNat(width,64)))) | Zloop(Z_E,imm) => ("loope",s_qword(BitsN.+(imm,BitsN.fromNat(width,64)))) | Zloop(Z_ALWAYS,imm) => ("loop",s_qword(BitsN.+(imm,BitsN.fromNat(width,64)))) | Zloop _ => ("?loop?","") | Zmonop(mop,sz_rm) => (L3.strTl(Cast.Zmonop_nameToString mop),s_sz_rm sz_rm) | Zmov(Z_ALWAYS,(sz,dst_src)) => ("mov",s_dest_src(sz,dst_src)) | Zmov(cond,(sz,Zr_rm(r,rm))) => ("cmov" ^ (s_cond cond), String.concat[s_register(sz,r),", ",s_rm(sz,rm)]) | Zmov _ => ("?mov?","") | Zmovsx(Z32,(Zr_rm(r,rm),Z64)) => ("movsxd",String.concat[s_register(Z64,r),", ",s_sz_rm(Z32,rm)]) | Zmovsx(Z32,_) => ("?movsx?","") | Zmovsx(Z64,_) => ("?movsx?","") | Zmovsx(sz1,(Zr_rm(r,rm),sz2)) => ("movsx",String.concat[s_register(sz2,r),", ",s_sz_rm(sz1,rm)]) | Zmovsx _ => ("?movsx?","") | Zmovzx(Z32,_) => ("?movzx?","") | Zmovzx(Z64,_) => ("?movzx?","") | Zmovzx(sz1,(Zr_rm(r,rm),sz2)) => ("movzx",String.concat[s_register(sz2,r),", ",s_sz_rm(sz1,rm)]) | Zmovzx _ => ("?movzx?","") | Zmul sz_rm => ("mul",s_sz_rm sz_rm) | Zimul sz_rm => ("imul",s_sz_rm sz_rm) | Zimul2(sz,(r,rm)) => ("imul",String.concat[s_register(sz,r),", ",s_rm(sz,rm)]) | Zimul3(sz,(r,(rm,imm))) => ("imul", String.concat[s_register(sz,r),", ",s_rm(sz,rm),", ",s_qword imm]) | Znop 1 => ("nop","") | Znop i => ("nop",Nat.toString i) | Zpop rm => ("pop",s_rm(Z64,rm)) | Zpush x => ("push",s_imm_rm x) | Zret imm => ("ret",s_qword0 imm) | Zset(cond,(have_rex,rm)) => ("set" ^ (s_cond cond),s_rm(Z8 have_rex,rm)) | Zxadd(sz,(rm,r)) => ("xadd",String.concat[s_rm(sz,rm),", ",s_register(sz,r)]) | Zxchg(sz,(rm,r)) => ("xchg",String.concat[s_rm(sz,rm),", ",s_register(sz,r)]); fun s_byte b = L3.padLeftString(#"0",(2,BitsN.toHexString b)); fun writeBytesAux (acc,l) = case l of h :: t => writeBytesAux(String.concat[acc," ",s_byte h],t) | _ => acc; fun writeBytes l = L3.strTl(writeBytesAux("",l)); fun joinString (s1,s2) = if s2 = "" then s1 else String.concat[s1," ",s2]; end