1(* x64 - generated by L3 - Thu Dec 21 10:59:16 2017 *) 2 3signature x64 = 4sig 5 6structure Map : Map 7 8(* ------------------------------------------------------------------------- 9 Types 10 ------------------------------------------------------------------------- *) 11 12datatype Zreg 13 = RAX | RCX | RDX | RBX | RSP | RBP | RSI | RDI | zR8 | zR9 | zR10 14 | zR11 | zR12 | zR13 | zR14 | zR15 15 16type MXCSR = 17 { DAZ: bool, DE: bool, DM: bool, FZ: bool, IE: bool, IM: bool, OE: bool, 18 OM: bool, PE: bool, PM: bool, RC: BitsN.nbit, Reserved: BitsN.nbit, 19 UE: bool, UM: bool, ZE: bool, ZM: bool } 20 21datatype Zeflags = Z_CF | Z_PF | Z_AF | Z_ZF | Z_SF | Z_OF 22 23datatype Zsize = Z16 | Z32 | Z64 | Z8 of bool 24 25datatype Zbase = ZnoBase | ZregBase of Zreg | ZripBase 26 27datatype Zrm 28 = Zm of ((BitsN.nbit * Zreg) option) * (Zbase * BitsN.nbit) | Zr of Zreg 29 30datatype Zdest_src 31 = Zr_rm of Zreg * Zrm | Zrm_i of Zrm * BitsN.nbit | Zrm_r of Zrm * Zreg 32 33datatype Zimm_rm = Zimm of BitsN.nbit | Zrm of Zrm 34 35datatype Zmonop_name = Zdec | Zinc | Znot | Zneg 36 37datatype Zbinop_name 38 = Zadd | Zor | Zadc | Zsbb | Zand | Zsub | Zxor | Zcmp | Zrol | Zror 39 | Zrcl | Zrcr | Zshl | Zshr | Ztest | Zsar 40 41datatype Zbit_test_name = Zbt | Zbts | Zbtr | Zbtc 42 43datatype Zcond 44 = Z_O | Z_NO | Z_B | Z_NB | Z_E | Z_NE | Z_NA | Z_A | Z_S | Z_NS | Z_P 45 | Z_NP | Z_L | Z_NL | Z_NG | Z_G | Z_ALWAYS 46 47datatype Zea 48 = Zea_i of Zsize * BitsN.nbit 49 | Zea_m of Zsize * BitsN.nbit 50 | Zea_r of Zsize * Zreg 51 52datatype sse_binop 53 = sse_add | sse_sub | sse_mul | sse_div | sse_max | sse_min 54 55datatype sse_logic = sse_and | sse_andn | sse_or | sse_xor 56 57datatype sse_compare 58 = sse_eq_oq | sse_lt_os | sse_le_os | sse_unord_q | sse_neq_uq 59 | sse_nlt_us | sse_nle_us | sse_ord_q 60 61datatype xmm_mem 62 = xmm_mem of ((BitsN.nbit * Zreg) option) * (Zbase * BitsN.nbit) 63 | xmm_reg of BitsN.nbit 64 65datatype SSE 66 = CMPPD of sse_compare * (BitsN.nbit * xmm_mem) 67 | CMPPS of sse_compare * (BitsN.nbit * xmm_mem) 68 | CMPSD of sse_compare * (BitsN.nbit * xmm_mem) 69 | CMPSS of sse_compare * (BitsN.nbit * xmm_mem) 70 | COMISD of BitsN.nbit * xmm_mem 71 | COMISS of BitsN.nbit * xmm_mem 72 | CVTDQ2PD of BitsN.nbit * xmm_mem 73 | CVTDQ2PS of BitsN.nbit * xmm_mem 74 | CVTPD2DQ of bool * (BitsN.nbit * xmm_mem) 75 | CVTPD2PS of BitsN.nbit * xmm_mem 76 | CVTPS2DQ of bool * (BitsN.nbit * xmm_mem) 77 | CVTPS2PD of BitsN.nbit * xmm_mem 78 | CVTSD2SI of bool * (bool * (Zreg * xmm_mem)) 79 | CVTSD2SS of BitsN.nbit * xmm_mem 80 | CVTSI2SD of bool * (BitsN.nbit * Zrm) 81 | CVTSI2SS of bool * (BitsN.nbit * Zrm) 82 | CVTSS2SD of BitsN.nbit * xmm_mem 83 | CVTSS2SI of bool * (bool * (Zreg * xmm_mem)) 84 | MOVAP_D_S of bool * (xmm_mem * xmm_mem) 85 | MOVQ of xmm_mem * xmm_mem 86 | MOVSD of xmm_mem * xmm_mem 87 | MOVSS of xmm_mem * xmm_mem 88 | MOVUP_D_S of bool * (xmm_mem * xmm_mem) 89 | MOV_D_Q of bool * (bool * (BitsN.nbit * Zrm)) 90 | PCMPEQQ of BitsN.nbit * xmm_mem 91 | PSLLDQ of BitsN.nbit * BitsN.nbit 92 | PSLLD_imm of BitsN.nbit * BitsN.nbit 93 | PSLLQ_imm of BitsN.nbit * BitsN.nbit 94 | PSLLW_imm of BitsN.nbit * BitsN.nbit 95 | PSRAD_imm of BitsN.nbit * BitsN.nbit 96 | PSRAW_imm of BitsN.nbit * BitsN.nbit 97 | PSRLDQ of BitsN.nbit * BitsN.nbit 98 | PSRLD_imm of BitsN.nbit * BitsN.nbit 99 | PSRLQ_imm of BitsN.nbit * BitsN.nbit 100 | PSRLW_imm of BitsN.nbit * BitsN.nbit 101 | SQRTPD of BitsN.nbit * xmm_mem 102 | SQRTPS of BitsN.nbit * xmm_mem 103 | SQRTSD of BitsN.nbit * xmm_mem 104 | SQRTSS of BitsN.nbit * xmm_mem 105 | bin_PD of sse_binop * (BitsN.nbit * xmm_mem) 106 | bin_PS of sse_binop * (BitsN.nbit * xmm_mem) 107 | bin_SD of sse_binop * (BitsN.nbit * xmm_mem) 108 | bin_SS of sse_binop * (BitsN.nbit * xmm_mem) 109 | logic_PD of sse_logic * (BitsN.nbit * xmm_mem) 110 | logic_PS of sse_logic * (BitsN.nbit * xmm_mem) 111 112datatype instruction 113 = SSE of SSE 114 | Zbinop of Zbinop_name * (Zsize * Zdest_src) 115 | Zbit_test of Zbit_test_name * (Zsize * Zdest_src) 116 | Zcall of Zimm_rm 117 | Zclc 118 | Zcmc 119 | Zcmpxchg of Zsize * (Zrm * Zreg) 120 | Zdiv of Zsize * Zrm 121 | Zidiv of Zsize * Zrm 122 | Zimul of Zsize * Zrm 123 | Zimul2 of Zsize * (Zreg * Zrm) 124 | Zimul3 of Zsize * (Zreg * (Zrm * BitsN.nbit)) 125 | Zjcc of Zcond * BitsN.nbit 126 | Zjmp of Zrm 127 | Zlea of Zsize * Zdest_src 128 | Zleave 129 | Zloop of Zcond * BitsN.nbit 130 | Zmonop of Zmonop_name * (Zsize * Zrm) 131 | Zmov of Zcond * (Zsize * Zdest_src) 132 | Zmovsx of Zsize * (Zdest_src * Zsize) 133 | Zmovzx of Zsize * (Zdest_src * Zsize) 134 | Zmul of Zsize * Zrm 135 | Znop of Nat.nat 136 | Zpop of Zrm 137 | Zpush of Zimm_rm 138 | Zret of BitsN.nbit 139 | Zset of Zcond * (bool * Zrm) 140 | Zstc 141 | Zxadd of Zsize * (Zrm * Zreg) 142 | Zxchg of Zsize * (Zrm * Zreg) 143 144datatype Zinst 145 = Zdec_fail of string 146 | Zfull_inst of 147 (BitsN.nbit list) * (instruction * ((BitsN.nbit list) option)) 148 149type REX = { B: bool, R: bool, W: bool, X: bool } 150 151datatype maybe_instruction 152 = FAIL of string 153 | OK of instruction 154 | PENDING of string * instruction 155 | STREAM of BitsN.nbit list 156 157(* ------------------------------------------------------------------------- 158 Exceptions 159 ------------------------------------------------------------------------- *) 160 161exception BadFlagAccess of string 162 163exception FAILURE of string 164 165exception INTERRUPT_EXCEPTION of BitsN.nbit 166 167(* ------------------------------------------------------------------------- 168 Functions 169 ------------------------------------------------------------------------- *) 170 171structure Cast: 172sig 173 174val natToZreg: Nat.nat -> Zreg 175val ZregToNat: Zreg -> Nat.nat 176val stringToZreg: string -> Zreg 177val ZregToString: Zreg -> string 178val natToZeflags: Nat.nat -> Zeflags 179val ZeflagsToNat: Zeflags -> Nat.nat 180val stringToZeflags: string -> Zeflags 181val ZeflagsToString: Zeflags -> string 182val natToZmonop_name: Nat.nat -> Zmonop_name 183val Zmonop_nameToNat: Zmonop_name -> Nat.nat 184val stringToZmonop_name: string -> Zmonop_name 185val Zmonop_nameToString: Zmonop_name -> string 186val natToZbinop_name: Nat.nat -> Zbinop_name 187val Zbinop_nameToNat: Zbinop_name -> Nat.nat 188val stringToZbinop_name: string -> Zbinop_name 189val Zbinop_nameToString: Zbinop_name -> string 190val natToZbit_test_name: Nat.nat -> Zbit_test_name 191val Zbit_test_nameToNat: Zbit_test_name -> Nat.nat 192val stringToZbit_test_name: string -> Zbit_test_name 193val Zbit_test_nameToString: Zbit_test_name -> string 194val natToZcond: Nat.nat -> Zcond 195val ZcondToNat: Zcond -> Nat.nat 196val stringToZcond: string -> Zcond 197val ZcondToString: Zcond -> string 198val natTosse_binop: Nat.nat -> sse_binop 199val sse_binopToNat: sse_binop -> Nat.nat 200val stringTosse_binop: string -> sse_binop 201val sse_binopToString: sse_binop -> string 202val natTosse_logic: Nat.nat -> sse_logic 203val sse_logicToNat: sse_logic -> Nat.nat 204val stringTosse_logic: string -> sse_logic 205val sse_logicToString: sse_logic -> string 206val natTosse_compare: Nat.nat -> sse_compare 207val sse_compareToNat: sse_compare -> Nat.nat 208val stringTosse_compare: string -> sse_compare 209val sse_compareToString: sse_compare -> string 210 211end 212 213val EFLAGS: ((bool option) Map.map) ref 214val MEM: (BitsN.nbit Map.map) ref 215val MXCSR: MXCSR ref 216val REG: (BitsN.nbit Map.map) ref 217val RIP: BitsN.nbit ref 218val XMM_REG: (BitsN.nbit Map.map) ref 219val MXCSR_DAZ_rupd: MXCSR * bool -> MXCSR 220val MXCSR_DE_rupd: MXCSR * bool -> MXCSR 221val MXCSR_DM_rupd: MXCSR * bool -> MXCSR 222val MXCSR_FZ_rupd: MXCSR * bool -> MXCSR 223val MXCSR_IE_rupd: MXCSR * bool -> MXCSR 224val MXCSR_IM_rupd: MXCSR * bool -> MXCSR 225val MXCSR_OE_rupd: MXCSR * bool -> MXCSR 226val MXCSR_OM_rupd: MXCSR * bool -> MXCSR 227val MXCSR_PE_rupd: MXCSR * bool -> MXCSR 228val MXCSR_PM_rupd: MXCSR * bool -> MXCSR 229val MXCSR_RC_rupd: MXCSR * BitsN.nbit -> MXCSR 230val MXCSR_Reserved_rupd: MXCSR * BitsN.nbit -> MXCSR 231val MXCSR_UE_rupd: MXCSR * bool -> MXCSR 232val MXCSR_UM_rupd: MXCSR * bool -> MXCSR 233val MXCSR_ZE_rupd: MXCSR * bool -> MXCSR 234val MXCSR_ZM_rupd: MXCSR * bool -> MXCSR 235val REX_B_rupd: REX * bool -> REX 236val REX_R_rupd: REX * bool -> REX 237val REX_W_rupd: REX * bool -> REX 238val REX_X_rupd: REX * bool -> REX 239val boolify'3: BitsN.nbit -> bool * (bool * bool) 240val boolify'8: 241 BitsN.nbit -> 242 bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) 243val DE_exception: unit -> unit 244val UD_exception: unit -> unit 245val GP_exception: unit -> unit 246val XM_exception: unit -> unit 247val rec'MXCSR: BitsN.nbit -> MXCSR 248val reg'MXCSR: MXCSR -> BitsN.nbit 249val write'rec'MXCSR: (BitsN.nbit * MXCSR) -> BitsN.nbit 250val write'reg'MXCSR: (MXCSR * BitsN.nbit) -> MXCSR 251val mem8: BitsN.nbit -> BitsN.nbit 252val write'mem8: (BitsN.nbit * BitsN.nbit) -> unit 253val mem16: BitsN.nbit -> BitsN.nbit 254val write'mem16: (BitsN.nbit * BitsN.nbit) -> unit 255val mem32: BitsN.nbit -> BitsN.nbit 256val write'mem32: (BitsN.nbit * BitsN.nbit) -> unit 257val mem64: BitsN.nbit -> BitsN.nbit 258val write'mem64: (BitsN.nbit * BitsN.nbit) -> unit 259val mem128: BitsN.nbit -> BitsN.nbit 260val write'mem128: (BitsN.nbit * BitsN.nbit) -> unit 261val Eflag: Zeflags -> bool 262val write'Eflag: (bool * Zeflags) -> unit 263val FlagUnspecified: Zeflags -> unit 264val CF: unit -> bool 265val write'CF: bool -> unit 266val PF: unit -> bool 267val write'PF: bool -> unit 268val AF: unit -> bool 269val write'AF: bool -> unit 270val ZF: unit -> bool 271val write'ZF: bool -> unit 272val SF: unit -> bool 273val write'SF: bool -> unit 274val OF: unit -> bool 275val write'OF: bool -> unit 276val ea_index: ((BitsN.nbit * Zreg) option) -> BitsN.nbit 277val ea_base: Zbase -> BitsN.nbit 278val mem_addr: 279 (((BitsN.nbit * Zreg) option) * (Zbase * BitsN.nbit)) -> BitsN.nbit 280val ea_Zrm: (Zsize * Zrm) -> Zea 281val ea_Zdest: (Zsize * Zdest_src) -> Zea 282val ea_Zsrc: (Zsize * Zdest_src) -> Zea 283val ea_Zimm_rm: Zimm_rm -> Zea 284val modSize: (Zsize * BitsN.nbit) -> BitsN.nbit 285val restrictSize: (Zsize * BitsN.nbit) -> BitsN.nbit 286val EA: Zea -> BitsN.nbit 287val write'EA: (BitsN.nbit * Zea) -> unit 288val read_dest_src_ea: 289 (Zsize * Zdest_src) -> (Zea * (BitsN.nbit * BitsN.nbit)) 290val call_dest_from_ea: Zea -> BitsN.nbit 291val get_ea_address: Zea -> BitsN.nbit 292val jump_to_ea: Zea -> unit 293val ByteParity: BitsN.nbit -> bool 294val Zsize_width: Zsize -> Nat.nat 295val word_size_msb: (Zsize * BitsN.nbit) -> bool 296val write_PF: BitsN.nbit -> unit 297val write_SF: (Zsize * BitsN.nbit) -> unit 298val write_ZF: (Zsize * BitsN.nbit) -> unit 299val write_arith_eflags_except_CF_OF: (Zsize * BitsN.nbit) -> unit 300val write_arith_eflags: (Zsize * (BitsN.nbit * (bool * bool))) -> unit 301val write_logical_eflags: (Zsize * BitsN.nbit) -> unit 302val erase_eflags: unit -> unit 303val value_width: Zsize -> Nat.nat 304val word_signed_overflow_add: (Zsize * (BitsN.nbit * BitsN.nbit)) -> bool 305val word_signed_overflow_sub: (Zsize * (BitsN.nbit * BitsN.nbit)) -> bool 306val add_with_carry_out: 307 (Zsize * (BitsN.nbit * BitsN.nbit)) -> (BitsN.nbit * (bool * bool)) 308val sub_with_borrow: 309 (Zsize * (BitsN.nbit * BitsN.nbit)) -> (BitsN.nbit * (bool * bool)) 310val write_arith_result: 311 (Zsize * ((BitsN.nbit * (bool * bool)) * Zea)) -> unit 312val write_arith_result_no_CF_OF: (Zsize * (BitsN.nbit * Zea)) -> unit 313val write_logical_result: (Zsize * (BitsN.nbit * Zea)) -> unit 314val write_result_erase_eflags: (BitsN.nbit * Zea) -> unit 315val SignExtension: (BitsN.nbit * (Zsize * Zsize)) -> BitsN.nbit 316val SignExtension64: (BitsN.nbit * Zsize) -> BitsN.nbit 317val maskShift: (Zsize * BitsN.nbit) -> Nat.nat 318val ROL: (Zsize * (BitsN.nbit * BitsN.nbit)) -> BitsN.nbit 319val ROR: (Zsize * (BitsN.nbit * BitsN.nbit)) -> BitsN.nbit 320val SAR: (Zsize * (BitsN.nbit * BitsN.nbit)) -> BitsN.nbit 321val write_binop: 322 (Zsize * (Zbinop_name * (BitsN.nbit * (BitsN.nbit * Zea)))) -> unit 323val write_monop: (Zsize * (Zmonop_name * (BitsN.nbit * Zea))) -> unit 324val bit_test: (Zbit_test_name * (Zea * Nat.nat)) -> unit 325val read_cond: Zcond -> bool 326val x64_pop_aux: unit -> BitsN.nbit 327val x64_pop: Zrm -> unit 328val x64_pop_rip: unit -> unit 329val x64_push_aux: BitsN.nbit -> unit 330val x64_push: Zimm_rm -> unit 331val x64_push_rip: unit -> unit 332val x64_drop: BitsN.nbit -> unit 333val initial_ieee_flags: bool -> SSE.ieee_flags 334val set_precision: (SSE.ieee_flags * bool) -> SSE.ieee_flags 335val zero32: BitsN.nbit -> BitsN.nbit 336val zero64: BitsN.nbit -> BitsN.nbit 337val denormal_to_zero32: BitsN.nbit -> BitsN.nbit 338val denormal_to_zero64: BitsN.nbit -> BitsN.nbit 339val flush_to_zero32: 340 (SSE.ieee_flags * BitsN.nbit) -> (SSE.ieee_flags * BitsN.nbit) 341val flush_to_zero64: 342 (SSE.ieee_flags * BitsN.nbit) -> (SSE.ieee_flags * BitsN.nbit) 343val sse_from_int64: Nat.nat -> 344 (IEEEReal.rounding_mode * BitsN.nbit) -> (SSE.ieee_flags * BitsN.nbit) 345val sse_from_int32: Nat.nat -> 346 (IEEEReal.rounding_mode * BitsN.nbit) -> (SSE.ieee_flags * BitsN.nbit) 347val sse_to_int64: Nat.nat -> 348 (IEEEReal.rounding_mode * BitsN.nbit) -> (SSE.ieee_flags * BitsN.nbit) 349val sse_to_int32: Nat.nat -> 350 (IEEEReal.rounding_mode * BitsN.nbit) -> (SSE.ieee_flags * BitsN.nbit) 351val float_min32: 352 (BitsN.nbit * BitsN.nbit) -> (SSE.ieee_flags * BitsN.nbit) 353val float_max32: 354 (BitsN.nbit * BitsN.nbit) -> (SSE.ieee_flags * BitsN.nbit) 355val float_min64: 356 (BitsN.nbit * BitsN.nbit) -> (SSE.ieee_flags * BitsN.nbit) 357val float_max64: 358 (BitsN.nbit * BitsN.nbit) -> (SSE.ieee_flags * BitsN.nbit) 359val process_float_flags: ((bool * SSE.ieee_flags) list) -> unit 360val RoundingMode: unit -> IEEEReal.rounding_mode 361val sse_binop32: 362 (sse_binop * (BitsN.nbit * BitsN.nbit)) -> 363 ((bool * SSE.ieee_flags) * BitsN.nbit) 364val sse_binop64: 365 (sse_binop * (BitsN.nbit * BitsN.nbit)) -> 366 ((bool * SSE.ieee_flags) * BitsN.nbit) 367val sse_sqrt32: BitsN.nbit -> ((bool * SSE.ieee_flags) * BitsN.nbit) 368val sse_sqrt64: BitsN.nbit -> ((bool * SSE.ieee_flags) * BitsN.nbit) 369val sse_logic: Nat.nat -> 370 (sse_logic * (BitsN.nbit * BitsN.nbit)) -> BitsN.nbit 371val sse_compare_signalling: sse_compare -> bool 372val sse_compare32: 373 (sse_compare * (BitsN.nbit * BitsN.nbit)) -> 374 ((bool * SSE.ieee_flags) * BitsN.nbit) 375val sse_compare64: 376 (sse_compare * (BitsN.nbit * BitsN.nbit)) -> 377 ((bool * SSE.ieee_flags) * BitsN.nbit) 378val rm_to_xmm_mem: Zrm -> xmm_mem 379val XMM: xmm_mem -> BitsN.nbit 380val write'XMM: (BitsN.nbit * xmm_mem) -> unit 381val CheckAlignedXMM: (xmm_mem * Nat.nat) -> unit 382val dfn'bin_PD: (sse_binop * (BitsN.nbit * xmm_mem)) -> unit 383val dfn'bin_PS: (sse_binop * (BitsN.nbit * xmm_mem)) -> unit 384val dfn'bin_SD: (sse_binop * (BitsN.nbit * xmm_mem)) -> unit 385val dfn'bin_SS: (sse_binop * (BitsN.nbit * xmm_mem)) -> unit 386val dfn'logic_PD: (sse_logic * (BitsN.nbit * xmm_mem)) -> unit 387val dfn'logic_PS: (sse_logic * (BitsN.nbit * xmm_mem)) -> unit 388val dfn'CMPPD: (sse_compare * (BitsN.nbit * xmm_mem)) -> unit 389val dfn'CMPPS: (sse_compare * (BitsN.nbit * xmm_mem)) -> unit 390val dfn'CMPSD: (sse_compare * (BitsN.nbit * xmm_mem)) -> unit 391val dfn'CMPSS: (sse_compare * (BitsN.nbit * xmm_mem)) -> unit 392val dfn'COMISD: (BitsN.nbit * xmm_mem) -> unit 393val dfn'COMISS: (BitsN.nbit * xmm_mem) -> unit 394val dfn'CVTDQ2PD: (BitsN.nbit * xmm_mem) -> unit 395val dfn'CVTDQ2PS: (BitsN.nbit * xmm_mem) -> unit 396val dfn'CVTPD2DQ: (bool * (BitsN.nbit * xmm_mem)) -> unit 397val dfn'CVTPD2PS: (BitsN.nbit * xmm_mem) -> unit 398val dfn'CVTPS2DQ: (bool * (BitsN.nbit * xmm_mem)) -> unit 399val dfn'CVTPS2PD: (BitsN.nbit * xmm_mem) -> unit 400val dfn'CVTSD2SI: (bool * (bool * (Zreg * xmm_mem))) -> unit 401val dfn'CVTSD2SS: (BitsN.nbit * xmm_mem) -> unit 402val dfn'CVTSI2SD: (bool * (BitsN.nbit * Zrm)) -> unit 403val dfn'CVTSI2SS: (bool * (BitsN.nbit * Zrm)) -> unit 404val dfn'CVTSS2SD: (BitsN.nbit * xmm_mem) -> unit 405val dfn'CVTSS2SI: (bool * (bool * (Zreg * xmm_mem))) -> unit 406val dfn'MOVAP_D_S: (bool * (xmm_mem * xmm_mem)) -> unit 407val dfn'MOVUP_D_S: (bool * (xmm_mem * xmm_mem)) -> unit 408val dfn'MOV_D_Q: (bool * (bool * (BitsN.nbit * Zrm))) -> unit 409val dfn'MOVQ: (xmm_mem * xmm_mem) -> unit 410val dfn'MOVSD: (xmm_mem * xmm_mem) -> unit 411val dfn'MOVSS: (xmm_mem * xmm_mem) -> unit 412val dfn'PCMPEQQ: (BitsN.nbit * xmm_mem) -> unit 413val dfn'PSLLDQ: (BitsN.nbit * BitsN.nbit) -> unit 414val dfn'PSLLD_imm: (BitsN.nbit * BitsN.nbit) -> unit 415val dfn'PSLLQ_imm: (BitsN.nbit * BitsN.nbit) -> unit 416val dfn'PSLLW_imm: (BitsN.nbit * BitsN.nbit) -> unit 417val dfn'PSRAD_imm: (BitsN.nbit * BitsN.nbit) -> unit 418val dfn'PSRAW_imm: (BitsN.nbit * BitsN.nbit) -> unit 419val dfn'PSRLDQ: (BitsN.nbit * BitsN.nbit) -> unit 420val dfn'PSRLD_imm: (BitsN.nbit * BitsN.nbit) -> unit 421val dfn'PSRLQ_imm: (BitsN.nbit * BitsN.nbit) -> unit 422val dfn'PSRLW_imm: (BitsN.nbit * BitsN.nbit) -> unit 423val dfn'SQRTPD: (BitsN.nbit * xmm_mem) -> unit 424val dfn'SQRTSD: (BitsN.nbit * xmm_mem) -> unit 425val dfn'SQRTPS: (BitsN.nbit * xmm_mem) -> unit 426val dfn'SQRTSS: (BitsN.nbit * xmm_mem) -> unit 427val dfn'Zbinop: (Zbinop_name * (Zsize * Zdest_src)) -> unit 428val dfn'Zbit_test: (Zbit_test_name * (Zsize * Zdest_src)) -> unit 429val dfn'Zcall: Zimm_rm -> unit 430val dfn'Zcmpxchg: (Zsize * (Zrm * Zreg)) -> unit 431val dfn'Zdiv: (Zsize * Zrm) -> unit 432val dfn'Zidiv: (Zsize * Zrm) -> unit 433val dfn'Zjcc: (Zcond * BitsN.nbit) -> unit 434val dfn'Zjmp: Zrm -> unit 435val dfn'Zlea: (Zsize * Zdest_src) -> unit 436val dfn'Zleave: unit -> unit 437val dfn'Zloop: (Zcond * BitsN.nbit) -> unit 438val dfn'Zmonop: (Zmonop_name * (Zsize * Zrm)) -> unit 439val dfn'Zmov: (Zcond * (Zsize * Zdest_src)) -> unit 440val dfn'Zmovsx: (Zsize * (Zdest_src * Zsize)) -> unit 441val dfn'Zmovzx: (Zsize * (Zdest_src * Zsize)) -> unit 442val dfn'Zmul: (Zsize * Zrm) -> unit 443val dfn'Zimul: (Zsize * Zrm) -> unit 444val dfn'Zimul2: (Zsize * (Zreg * Zrm)) -> unit 445val dfn'Zimul3: (Zsize * (Zreg * (Zrm * BitsN.nbit))) -> unit 446val dfn'Znop: Nat.nat -> unit 447val dfn'Zpop: Zrm -> unit 448val dfn'Zpush: Zimm_rm -> unit 449val dfn'Zret: BitsN.nbit -> unit 450val dfn'Zset: (Zcond * (bool * Zrm)) -> unit 451val dfn'Zxadd: (Zsize * (Zrm * Zreg)) -> unit 452val dfn'Zxchg: (Zsize * (Zrm * Zreg)) -> unit 453val dfn'Zcmc: unit -> unit 454val dfn'Zclc: unit -> unit 455val dfn'Zstc: unit -> unit 456val Run: instruction -> unit 457val oimmediate8: 458 ((BitsN.nbit list) option) -> (BitsN.nbit * ((BitsN.nbit list) option)) 459val immediate8: 460 (BitsN.nbit list) -> (BitsN.nbit * ((BitsN.nbit list) option)) 461val immediate16: 462 (BitsN.nbit list) -> (BitsN.nbit * ((BitsN.nbit list) option)) 463val immediate32: 464 (BitsN.nbit list) -> (BitsN.nbit * ((BitsN.nbit list) option)) 465val immediate64: 466 (BitsN.nbit list) -> (BitsN.nbit * ((BitsN.nbit list) option)) 467val immediate: 468 (Zsize * (BitsN.nbit list)) -> (BitsN.nbit * ((BitsN.nbit list) option)) 469val oimmediate: 470 (Zsize * ((BitsN.nbit list) option)) -> 471 (BitsN.nbit * ((BitsN.nbit list) option)) 472val full_immediate: 473 (Zsize * (BitsN.nbit list)) -> (BitsN.nbit * ((BitsN.nbit list) option)) 474val rec'REX: BitsN.nbit -> REX 475val reg'REX: REX -> BitsN.nbit 476val write'rec'REX: (BitsN.nbit * REX) -> BitsN.nbit 477val write'reg'REX: (REX * BitsN.nbit) -> REX 478val RexReg: (bool * BitsN.nbit) -> Zreg 479val readDisplacement: 480 (BitsN.nbit * (BitsN.nbit list)) -> 481 (BitsN.nbit * ((BitsN.nbit list) option)) 482val readSibDisplacement: 483 (BitsN.nbit * (BitsN.nbit list)) -> 484 (BitsN.nbit * ((BitsN.nbit list) option)) 485val readSIB: 486 (REX * (BitsN.nbit * (BitsN.nbit list))) -> 487 (Zrm * ((BitsN.nbit list) option)) 488val readModRM: 489 (REX * (BitsN.nbit list)) -> (Zreg * (Zrm * ((BitsN.nbit list) option))) 490val readOpcodeModRM: 491 (REX * (BitsN.nbit list)) -> 492 (BitsN.nbit * (Zrm * ((BitsN.nbit list) option))) 493val prefixGroup: BitsN.nbit -> Nat.nat 494val readPrefix: 495 ((Nat.nat list) * ((BitsN.nbit list) * (BitsN.nbit list))) -> 496 (((BitsN.nbit list) * (bool * (REX * (BitsN.nbit list)))) option) 497val readPrefixes: 498 (BitsN.nbit list) -> 499 (((BitsN.nbit list) * (bool * (REX * (BitsN.nbit list)))) option) 500val OpSize: (bool * (bool * (BitsN.nbit * bool))) -> Zsize 501val isZm: Zrm -> bool 502val x64_decode: (BitsN.nbit list) -> Zinst 503val x64_fetch: unit -> (BitsN.nbit list) 504val x64_next: unit -> unit 505val e_imm8: BitsN.nbit -> (BitsN.nbit list) 506val e_imm16: BitsN.nbit -> (BitsN.nbit list) 507val e_imm32: BitsN.nbit -> (BitsN.nbit list) 508val e_imm64: BitsN.nbit -> (BitsN.nbit list) 509val e_imm: BitsN.nbit -> (BitsN.nbit list) 510val e_imm_8_32: BitsN.nbit -> (Nat.nat * (BitsN.nbit list)) 511val e_ModRM: 512 (BitsN.nbit * Zrm) -> ((BitsN.nbit * (BitsN.nbit list)) option) 513val rex_prefix: BitsN.nbit -> (BitsN.nbit list) 514val e_opsize: (Zsize * BitsN.nbit) -> ((BitsN.nbit list) * BitsN.nbit) 515val e_opsize_imm: 516 (Zsize * (BitsN.nbit * (BitsN.nbit * bool))) -> 517 (((BitsN.nbit list) * (BitsN.nbit * (BitsN.nbit list))) option) 518val e_opc: (BitsN.nbit * (BitsN.nbit * Zrm)) -> (BitsN.nbit list) 519val e_gen_rm_reg: 520 (Zsize * 521 (Zrm * 522 (BitsN.nbit * ((BitsN.nbit list) * (BitsN.nbit * (BitsN.nbit option)))))) -> 523 (BitsN.nbit list) 524val e_rm_imm: 525 (Zsize * (Zrm * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 526 (BitsN.nbit list) 527val e_rm_imm8: 528 (Zsize * (Zrm * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 529 (BitsN.nbit list) 530val e_rm_imm8b: 531 (Zsize * (Zrm * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit list))))) -> 532 (BitsN.nbit list) 533val e_rax_imm: (Zsize * (BitsN.nbit * BitsN.nbit)) -> (BitsN.nbit list) 534val e_jcc_rel32: instruction -> (BitsN.nbit list) 535val not_byte: Zsize -> bool 536val is_rax: Zrm -> bool 537val xmm_mem_to_rm: xmm_mem -> Zrm 538val encode_sse_binop: sse_binop -> BitsN.nbit 539val encode_sse: SSE -> (BitsN.nbit list) 540val encode: instruction -> (BitsN.nbit list) 541val stripLeftSpaces: string -> string 542val stripSpaces: string -> string 543val p_number: string -> (Nat.nat option) 544val p_bin_or_hex_number: string -> (Nat.nat option) 545val p_signed_number: string -> (IntInf.int option) 546val p_imm8: string -> (BitsN.nbit option) 547val p_imm16: string -> (BitsN.nbit option) 548val p_imm32: string -> (BitsN.nbit option) 549val p_imm64: string -> (BitsN.nbit option) 550val p_imm_of_size: (Zsize * string) -> (BitsN.nbit option) 551val readBytes: 552 ((BitsN.nbit list) * (string list)) -> ((BitsN.nbit list) option) 553val p_bytes: string -> ((BitsN.nbit list) option) 554val p_label: string -> (string option) 555val p_register: string -> ((Zsize * Zreg) option) 556val p_xreg: string -> (BitsN.nbit option) 557val p_scale: string -> (BitsN.nbit option) 558val p_scale_index: string -> ((BitsN.nbit * Zreg) option) 559val p_disp: (bool * string) -> ((bool * BitsN.nbit) option) 560val p_rip_disp: string -> ((bool * BitsN.nbit) option) 561val p_parts: 562 ((((BitsN.nbit * Zreg) option) * ((Zreg option) * (BitsN.nbit option))) * 563 string) -> 564 (((BitsN.nbit * Zreg) option) * ((Zreg option) * (BitsN.nbit option))) 565val p_mem_aux: 566 string -> ((((BitsN.nbit * Zreg) option) * (Zbase * BitsN.nbit)) option) 567val p_mem: 568 string -> ((((BitsN.nbit * Zreg) option) * (Zbase * BitsN.nbit)) option) 569val p_rm: string -> ((Zsize * Zrm) option) 570val p_xmm: string -> (xmm_mem option) 571val checkSizeDelim: (Zsize * string) -> (Zsize option) 572val p_sz: string -> ((Zsize option) * string) 573val s_sz: Zsize -> string 574val p_sz_rm: string -> (string * (Zsize * Zrm)) 575val check_sizes: (Zsize * ((Zreg option) * (Zsize * Zrm))) -> string 576val p_rm_of_size: (Zsize * ((Zreg option) * string)) -> (string * Zrm) 577val p_rm32: string -> (string * Zrm) 578val p_rm64: string -> (string * Zrm) 579val p_imm_rm: string -> (string * Zimm_rm) 580val p_dest_src: 581 (bool * (string * string)) -> (string * ((Zsize * Zdest_src) option)) 582val p_cond: string -> (Zcond option) 583val p_binop: (Zbinop_name * (string * string)) -> maybe_instruction 584val p_monop: (Nat.nat * string) -> maybe_instruction 585val p_xop: (Nat.nat * (string * string)) -> maybe_instruction 586val p_imul3: (string * (Zsize * (Zreg * Zrm))) -> maybe_instruction 587val p_sse: (string * (string * string)) -> maybe_instruction 588val p_cvt_2si: (bool * (bool * (string * string))) -> maybe_instruction 589val p_cvtsi2: (bool * (string * string)) -> maybe_instruction 590val p_movap_movup: 591 (bool * (bool * (string * string))) -> maybe_instruction 592val p_movsd_movss: (bool * (string * string)) -> maybe_instruction 593val p_mov_d_q: (bool * (string * string)) -> maybe_instruction 594val p_pshift: (BitsN.nbit * (string * string)) -> maybe_instruction 595val p_tokens: string -> (string list) 596val instructionFromString: string -> maybe_instruction 597val s_register: (Zsize * Zreg) -> string 598val s_qword: BitsN.nbit -> string 599val s_qword0: BitsN.nbit -> string 600val s_sib: (BitsN.nbit * Zreg) -> string 601val s_mem: (((BitsN.nbit * Zreg) option) * (Zbase * BitsN.nbit)) -> string 602val s_rm: (Zsize * Zrm) -> string 603val s_xreg: BitsN.nbit -> string 604val s_xmm_mem: xmm_mem -> string 605val s_xmm: (BitsN.nbit * xmm_mem) -> string 606val s_imm_rm: Zimm_rm -> string 607val s_sz_rm: (Zsize * Zrm) -> string 608val s_dest_src: (Zsize * Zdest_src) -> string 609val s_cond: Zcond -> string 610val s_sse_binop: sse_binop -> string 611val s_sse_logic: sse_logic -> string 612val s_sse_compare: sse_compare -> string 613val sse_instructionToString: SSE -> (string * string) 614val instructionToString: (instruction * Nat.nat) -> (string * string) 615val s_byte: BitsN.nbit -> string 616val writeBytesAux: (string * (BitsN.nbit list)) -> string 617val writeBytes: (BitsN.nbit list) -> string 618val joinString: (string * string) -> string 619 620end