From de4a1297a139a61fd358c062bb97528825a422e7 Mon Sep 17 00:00:00 2001 From: Dhruv Maroo Date: Sun, 18 Feb 2024 06:18:34 +0530 Subject: [PATCH] Add RzIL for floating-point x86 instructions (#3865) * Create `il_fp_ops.inc`, for floating-point instructions' IL ops * Add IL implementation for `FABS` * Also add `x86_il_{get,set}_st_reg` helper functions * Add IL implementation for `FNINIT` and `FLDCW` * Add IL implementations for `FNSTCW` and `FNSTSW` * Add IL implementation for `FNCLEX` * Add ST push and pop functions * Fix clang formatting * Add fucntions for updating FPSW TOP pointer * Add `FLD` instruction lifitng, FPSW flag support, FP operand support * Remove `x86_bool_to_bv` and use the standard `BOOL_TO_BV` * Add implementation for `FST{P}`, and rounding mode support * Add `FLD` variants for constants * Fix formatting and build * Add IL lifting for `FXCH` * Add width checks to avoid redundant rounding * Implement IL lifting for `FILD`, `FIST{P}` * Add helper functions to inter-convert floating point values and integers using the rounding mode in the control word * FPU stack regs are 80-bit, not 64-bit * Add RzIL lifting for `FBLD` * Add RzIL implementation for `FBSTP` * An invalid-arithmetic-operand (#IA) exception may occurr if the value being converted to the BCD integer cannot fit in an 18-bit BCD integer. For the IL's purpose, we just jump to the "int" label (stands for interrupt) using `GOTO`. * Remove all the `EMPTY()` ops after `GOTO()` ops * On second thought, using `EMPTY()` ops after `GOTO()` ops is not the best idea to indicate end of analysis. Maybe the hooks can signal that analysis needs to be restarted. * Also, clean up the comments of a bunch of unimplemented ops * Moved some code around * Rename "rmode" local variable to "_rmode" * Add some TODOs for deffered work * Fix failing asm tests * Caused due to the removal of the [empty] opcode * Implement IL lifting for `FADD` (and some other minor refactoring) * Implement the IL lifting for `FADD`: This is not entirely correct as of now, because we don't handle setting C1 based on rounding up/down, but I think it should be fine for now. Need to tackle setting the control word bits later * Start using `RzFloatFormat` to describe the float's width instead of using an unsigned integer. Provide and expose conversion functions between the two * Use a global to denote when RMode needs to be init, implement FIADD * Other minor refactor which fixes the CI (hopefully) * Implement `FMUL` and `FIMUL` * Extract the common code into a C macro * Implement RzIL for `FSUB` and `FISUB` * Also add `x86_il_fsub_with_rmode` helper * Implement RzIL for `FSUBR` and `FISUBR` * Reuse the implementation of `x86_il_fsub_with_rmode` and just pass the arguments in the opposite order * Add RzIL implementation for `FDIV`, `FIDIV`, `FDIVR`, `FIDIVR` * Add pop versions of floating point arithmetic instuctions * Add a new macro `X86_ARITHMETIC_POP_IL` macro for the same * Fix a typo * Add a note for using `X86_INS_PFADD` for FADDP instruction on Capstone version newer than 4 * Add RzIL implementations for `FCOM`, `FCOMP` and `FCOMPP` * Add RzIL lifting for `FUCOM` and `FCOMI` families of instructions * Implement RzIL lifting for `FCHS` and `FTST` * Add RzIL implementation for `FRNDINT` and `FSQRT` * Add RzIL implementation for `FNOP` and `FISTTP` * Remove global variable `use_rmode` and use pass around a context instead * Define a new `X86ILContext` struct to pass around information whether we need to intitialize the rouding mode or not * Remove the global variable which was previously responsible for doing so * Add RzIL for `FICOM` and `FICOMP`, add register bindings and fix bugs * Make `rz-test` more robust against IL outputs with newlines in them * Add RzIL tests in db/asm for x86 FPU instructions * Fix the bug when using `FADDP` with Capstone version > 4 * Fix remaining db tests * Remove tests for `FSTSW` or `FSTCW` instructions * We already test `WAIT` (in `db/asm/x86_32`) and `FSTSW` (or `FSTCW`) (in `db/asm/x86_64`) * Remove the newline replacement code in `rz-test` as well, since we wouldn't need that functionality anymore * Add asm tests for math constant push instructions * Add `RZ_IPI` annotation for all the functions exposed through the header * Add `RZ_OWN`, `RZ_BORROW` and `RZ_NONNULL` annotations * Add Doxygen doc for `ctx` argument * Add description for the `EXEC_WITH_RMODE` macro * Move the non-null check for `ctx` inside the valid branch * When we pop the FPU stack we pass in a `NULL` context since no resizing would be needed, which causes a failure if the non-null check for the `ctx` is outside the branch * Fixes failing tests in `db/asm` * Minor bug fixes + make the annotations less strict than they need to be * Minor bug fixes * Incorrect implementation for `RET` and `CALL` * Swapped arguments for shift right * Fix asm tests for `JMP` and `RET` instructions * Fix indexing error for `FXCH` * Review changes * Move all unimplemented instructions to the end * Remove support for Capstone version less than 4 --- librz/analysis/arch/x86/common.c | 573 +++++++++++++++++++-- librz/analysis/arch/x86/common.h | 120 ++++- librz/analysis/arch/x86/il_fp_ops.inc | 697 ++++++++++++++++++++++++++ librz/analysis/arch/x86/il_ops.inc | 123 ++--- librz/analysis/arch/x86/x86_il.c | 108 +++- librz/analysis/arch/x86/x86_il.h | 8 + librz/analysis/p/analysis_x86_cs.c | 16 +- test/db/asm/x86_16 | 2 +- test/db/asm/x86_32 | 72 +-- test/db/asm/x86_64 | 166 +++--- test/db/cmd/cmd_ar | 34 +- 11 files changed, 1641 insertions(+), 278 deletions(-) create mode 100644 librz/analysis/arch/x86/il_fp_ops.inc diff --git a/librz/analysis/arch/x86/common.c b/librz/analysis/arch/x86/common.c index 16faae233af..b439f3734ef 100644 --- a/librz/analysis/arch/x86/common.c +++ b/librz/analysis/arch/x86/common.c @@ -38,7 +38,7 @@ const char *x86_registers[X86_REG_ENDING] = { [X86_REG_ES] = "es", [X86_REG_ESI] = "esi", [X86_REG_ESP] = "esp", - [X86_REG_FPSW] = "fpsw", + [X86_REG_FPSW] = "swd", [X86_REG_FS] = "fs", [X86_REG_GS] = "gs", [X86_REG_IP] = "ip", @@ -611,7 +611,7 @@ int get_extreg_ind(X86Reg reg) { * \param bits bitness * \param pc Program counter */ -RzILOpPure *x86_il_get_reg_bits(X86Reg reg, int bits, uint64_t pc) { +RZ_IPI RzILOpPure *x86_il_get_reg_bits(X86Reg reg, int bits, uint64_t pc) { if (is_pc_reg(reg)) { return UN(bits, pc); } @@ -643,7 +643,8 @@ RzILOpPure *x86_il_get_reg_bits(X86Reg reg, int bits, uint64_t pc) { * \param val Value to be stored * \param bits bitness */ -RzILOpEffect *x86_il_set_reg_bits(X86Reg reg, RzILOpPure *val, int bits) { +RZ_IPI RzILOpEffect *x86_il_set_reg_bits(X86Reg reg, RZ_OWN RZ_NONNULL RzILOpPure *val, int bits) { + rz_return_val_if_fail(val, NULL); int ind = -1; if (x86_il_is_gpr(reg)) { @@ -670,7 +671,7 @@ RzILOpEffect *x86_il_set_reg_bits(X86Reg reg, RzILOpPure *val, int bits) { * \param segment * \param bits bitness */ -RzILOpPure *x86_il_get_memaddr_segment_bits(X86Mem mem, X86Reg segment, int bits, ut64 pc) { +RZ_IPI RzILOpPure *x86_il_get_memaddr_segment_bits(X86Mem mem, X86Reg segment, int bits, ut64 pc) { RzILOpPure *offset = NULL; if (mem.base != X86_REG_INVALID) { offset = x86_il_get_reg_bits(mem.base, bits, pc); @@ -708,11 +709,12 @@ RzILOpPure *x86_il_get_memaddr_segment_bits(X86Mem mem, X86Reg segment, int bits return offset; } -RzILOpPure *x86_il_get_memaddr_bits(X86Mem mem, int bits, ut64 pc) { +RZ_IPI RzILOpPure *x86_il_get_memaddr_bits(X86Mem mem, int bits, ut64 pc) { return x86_il_get_memaddr_segment_bits(mem, mem.segment, bits, pc); } -RzILOpEffect *x86_il_set_mem_bits(X86Mem mem, RzILOpPure *val, int bits, ut64 pc) { +RZ_IPI RzILOpEffect *x86_il_set_mem_bits(X86Mem mem, RZ_OWN RZ_NONNULL RzILOpPure *val, int bits, ut64 pc) { + rz_return_val_if_fail(val, NULL); return STOREW(x86_il_get_memaddr_bits(mem, bits, pc), val); } @@ -725,7 +727,7 @@ RzILOpEffect *x86_il_set_mem_bits(X86Mem mem, RzILOpPure *val, int bits, ut64 pc * \param op * \param analysis_bits bitness */ -RzILOpPure *x86_il_get_operand_bits(X86Op op, int analysis_bits, ut64 pc, int implicit_size) { +RZ_IPI RzILOpPure *x86_il_get_operand_bits(X86Op op, int analysis_bits, ut64 pc, int implicit_size) { switch (op.type) { case X86_OP_INVALID: if (implicit_size) { @@ -754,7 +756,9 @@ RzILOpPure *x86_il_get_operand_bits(X86Op op, int analysis_bits, ut64 pc, int im * \param op * \param analysis_bits bitness */ -RzILOpEffect *x86_il_set_operand_bits(X86Op op, RzILOpPure *val, int bits, ut64 pc) { +RZ_IPI RzILOpEffect *x86_il_set_operand_bits(X86Op op, RZ_OWN RZ_NONNULL RzILOpPure *val, int bits, ut64 pc) { + rz_return_val_if_fail(val, NULL); + RzILOpEffect *ret = NULL; switch (op.type) { case X86_OP_REG: @@ -780,7 +784,9 @@ RzILOpEffect *x86_il_set_operand_bits(X86Op op, RzILOpPure *val, int bits, ut64 * \param x * \param y */ -RzILOpBool *x86_il_is_add_carry(RZ_OWN RzILOpPure *res, RZ_OWN RzILOpPure *x, RZ_OWN RzILOpPure *y) { +RZ_IPI RzILOpBool *x86_il_is_add_carry(RZ_OWN RZ_NONNULL RzILOpPure *res, RZ_OWN RZ_NONNULL RzILOpPure *x, RZ_OWN RZ_NONNULL RzILOpPure *y) { + rz_return_val_if_fail(res && x && y, NULL); + // res = x + y RzILOpBool *xmsb = MSB(x); RzILOpBool *ymsb = MSB(y); @@ -809,7 +815,9 @@ RzILOpBool *x86_il_is_add_carry(RZ_OWN RzILOpPure *res, RZ_OWN RzILOpPure *x, RZ * \param x * \param y */ -RzILOpBool *x86_il_is_sub_borrow(RZ_OWN RzILOpPure *res, RZ_OWN RzILOpPure *x, RZ_OWN RzILOpPure *y) { +RZ_IPI RzILOpBool *x86_il_is_sub_borrow(RZ_OWN RZ_NONNULL RzILOpPure *res, RZ_OWN RZ_NONNULL RzILOpPure *x, RZ_OWN RZ_NONNULL RzILOpPure *y) { + rz_return_val_if_fail(res && x && y, NULL); + // res = x - y RzILOpBool *xmsb = MSB(x); RzILOpBool *ymsb = MSB(y); @@ -838,7 +846,9 @@ RzILOpBool *x86_il_is_sub_borrow(RZ_OWN RzILOpPure *res, RZ_OWN RzILOpPure *x, R * \param x * \param y */ -RzILOpBool *x86_il_is_add_overflow(RZ_OWN RzILOpPure *res, RZ_OWN RzILOpPure *x, RZ_OWN RzILOpPure *y) { +RZ_IPI RzILOpBool *x86_il_is_add_overflow(RZ_OWN RZ_NONNULL RzILOpPure *res, RZ_OWN RZ_NONNULL RzILOpPure *x, RZ_OWN RZ_NONNULL RzILOpPure *y) { + rz_return_val_if_fail(res && x && y, NULL); + // res = x + y RzILOpBool *xmsb = MSB(x); RzILOpBool *ymsb = MSB(y); @@ -861,7 +871,9 @@ RzILOpBool *x86_il_is_add_overflow(RZ_OWN RzILOpPure *res, RZ_OWN RzILOpPure *x, * \param x * \param y */ -RzILOpBool *x86_il_is_sub_underflow(RZ_OWN RzILOpPure *res, RZ_OWN RzILOpPure *x, RZ_OWN RzILOpPure *y) { +RZ_IPI RzILOpBool *x86_il_is_sub_underflow(RZ_OWN RZ_NONNULL RzILOpPure *res, RZ_OWN RZ_NONNULL RzILOpPure *x, RZ_OWN RZ_NONNULL RzILOpPure *y) { + rz_return_val_if_fail(res && x && y, NULL); + // res = x - y RzILOpBool *xmsb = MSB(x); RzILOpBool *ymsb = MSB(y); @@ -877,16 +889,6 @@ RzILOpBool *x86_il_is_sub_underflow(RZ_OWN RzILOpPure *res, RZ_OWN RzILOpPure *x return or ; } -/** - * \brief Convert a bool \p b to a bitvector of length \p bits - * - * \param b - * \param bits - */ -RzILOpBitVector *x86_bool_to_bv(RzILOpBool *b, unsigned int bits) { - return ITE(b, UN(bits, 1), UN(bits, 0)); -} - struct x86_parity_helper_t { RzILOpBool *val; ///< value of parity RzILOpEffect *eff; ///< RzILOpEffect used to find the parity @@ -906,7 +908,7 @@ struct x86_parity_helper_t x86_il_get_parity(RZ_OWN RzILOpPure *val) { since the value of "_popcnt" wouldn't change any further */ RzILOpBool *condition = NON_ZERO(VARL("_val")); - RzILOpEffect *popcnt = SETL("_popcnt", ADD(VARL("_popcnt"), x86_bool_to_bv(LSB(VARL("_val")), 8))); + RzILOpEffect *popcnt = SETL("_popcnt", ADD(VARL("_popcnt"), BOOL_TO_BV(LSB(VARL("_val")), 8))); popcnt = SEQ2(popcnt, SETL("_val", SHIFTR0(VARL("_val"), U8(1)))); RzILOpEffect *repeat_eff = REPEAT(condition, popcnt); @@ -922,7 +924,9 @@ struct x86_parity_helper_t x86_il_get_parity(RZ_OWN RzILOpPure *val) { /** * \brief Sets the value of PF, ZF, SF according to the \p result */ -RzILOpEffect *x86_il_set_result_flags_bits(RZ_OWN RzILOpPure *result, int bits) { +RZ_IPI RzILOpEffect *x86_il_set_result_flags_bits(RZ_OWN RZ_NONNULL RzILOpPure *result, int bits) { + rz_return_val_if_fail(result, NULL); + RzILOpEffect *set = SETL("_result", result); struct x86_parity_helper_t pf = x86_il_get_parity(UNSIGNED(8, VARL("_result"))); RzILOpBool *zf = IS_ZERO(VARL("_result")); @@ -937,7 +941,9 @@ RzILOpEffect *x86_il_set_result_flags_bits(RZ_OWN RzILOpPure *result, int bits) /** * \brief Sets the value of CF, OF, AF according to the \p res */ -RzILOpEffect *x86_il_set_arithmetic_flags_bits(RZ_OWN RzILOpPure *res, RZ_OWN RzILOpPure *x, RZ_OWN RzILOpPure *y, bool addition, int bits) { +RZ_IPI RzILOpEffect *x86_il_set_arithmetic_flags_bits(RZ_OWN RZ_NONNULL RzILOpPure *res, RZ_OWN RZ_NONNULL RzILOpPure *x, RZ_OWN RZ_NONNULL RzILOpPure *y, bool addition, int bits) { + rz_return_val_if_fail(res && x && y, NULL); + RzILOpBool *cf = NULL; RzILOpBool *of = NULL; RzILOpBool *af = NULL; @@ -965,7 +971,9 @@ RzILOpEffect *x86_il_set_arithmetic_flags_bits(RZ_OWN RzILOpPure *res, RZ_OWN Rz /** * \brief Set OF and AF according to \p res */ -RzILOpEffect *x86_il_set_arithmetic_flags_except_cf_bits(RZ_OWN RzILOpPure *res, RZ_OWN RzILOpPure *x, RZ_OWN RzILOpPure *y, bool addition, int bits) { +RZ_IPI RzILOpEffect *x86_il_set_arithmetic_flags_except_cf_bits(RZ_OWN RZ_NONNULL RzILOpPure *res, RZ_OWN RZ_NONNULL RzILOpPure *x, RZ_OWN RZ_NONNULL RzILOpPure *y, bool addition, int bits) { + rz_return_val_if_fail(res && x && y, NULL); + RzILOpBool *of = NULL; RzILOpBool *af = NULL; @@ -991,7 +999,7 @@ RzILOpEffect *x86_il_set_arithmetic_flags_except_cf_bits(RZ_OWN RzILOpPure *res, * * \param size size of flags needed */ -RzILOpPure *x86_il_get_flags(unsigned int size) { +RZ_IPI RzILOpPure *x86_il_get_flags(unsigned int size) { /* We really don't care about bits higher than 16 for now */ RzILOpPure *val; if (size == 8) { @@ -1002,30 +1010,30 @@ RzILOpPure *x86_il_get_flags(unsigned int size) { always 1 on 8086 and 186, always 0 on later models Assuming 0 */ - val = x86_bool_to_bv(IL_FALSE, size); - val = LOGOR(SHIFTL0(val, UN(size, 1)), x86_bool_to_bv(VARG(EFLAGS(NT)), size)); + val = BOOL_TO_BV(IL_FALSE, size); + val = LOGOR(SHIFTL0(val, UN(size, 1)), BOOL_TO_BV(VARG(EFLAGS(NT)), size)); /** Bit 12-13: IOPL, I/O privilege level (286+ only), always 1 on 8086 and 186 Assuming all 1 */ val = LOGOR(SHIFTL0(val, UN(size, 2)), UN(size, 0x3)); - val = LOGOR(SHIFTL0(val, UN(size, 1)), x86_bool_to_bv(VARG(EFLAGS(OF)), size)); - val = LOGOR(SHIFTL0(val, UN(size, 1)), x86_bool_to_bv(VARG(EFLAGS(DF)), size)); - val = LOGOR(SHIFTL0(val, UN(size, 1)), x86_bool_to_bv(VARG(EFLAGS(IF)), size)); - val = LOGOR(SHIFTL0(val, UN(size, 1)), x86_bool_to_bv(VARG(EFLAGS(TF)), size)); + val = LOGOR(SHIFTL0(val, UN(size, 1)), BOOL_TO_BV(VARG(EFLAGS(OF)), size)); + val = LOGOR(SHIFTL0(val, UN(size, 1)), BOOL_TO_BV(VARG(EFLAGS(DF)), size)); + val = LOGOR(SHIFTL0(val, UN(size, 1)), BOOL_TO_BV(VARG(EFLAGS(IF)), size)); + val = LOGOR(SHIFTL0(val, UN(size, 1)), BOOL_TO_BV(VARG(EFLAGS(TF)), size)); lower_half: if (size == 8) { - val = x86_bool_to_bv(VARG(EFLAGS(SF)), size); + val = BOOL_TO_BV(VARG(EFLAGS(SF)), size); } else { - val = LOGOR(SHIFTL0(val, UN(size, 1)), x86_bool_to_bv(VARG(EFLAGS(ZF)), size)); + val = LOGOR(SHIFTL0(val, UN(size, 1)), BOOL_TO_BV(VARG(EFLAGS(ZF)), size)); } - val = LOGOR(SHIFTL0(val, UN(size, 1)), x86_bool_to_bv(VARG(EFLAGS(ZF)), size)); - val = LOGOR(SHIFTL0(val, UN(size, 2)), x86_bool_to_bv(VARG(EFLAGS(AF)), size)); - val = LOGOR(SHIFTL0(val, UN(size, 2)), x86_bool_to_bv(VARG(EFLAGS(PF)), size)); + val = LOGOR(SHIFTL0(val, UN(size, 1)), BOOL_TO_BV(VARG(EFLAGS(ZF)), size)); + val = LOGOR(SHIFTL0(val, UN(size, 2)), BOOL_TO_BV(VARG(EFLAGS(AF)), size)); + val = LOGOR(SHIFTL0(val, UN(size, 2)), BOOL_TO_BV(VARG(EFLAGS(PF)), size)); val = LOGOR(SHIFTL0(val, UN(size, 1)), UN(size, 1)); - val = LOGOR(SHIFTL0(val, UN(size, 1)), x86_bool_to_bv(VARG(EFLAGS(CF)), size)); + val = LOGOR(SHIFTL0(val, UN(size, 1)), BOOL_TO_BV(VARG(EFLAGS(CF)), size)); return val; } @@ -1036,7 +1044,9 @@ RzILOpPure *x86_il_get_flags(unsigned int size) { * \param val value to set the FLAGS register to * \param size size of \p val */ -RzILOpEffect *x86_il_set_flags(RZ_OWN RzILOpPure *val, unsigned int size) { +RZ_IPI RzILOpEffect *x86_il_set_flags(RZ_OWN RZ_NONNULL RzILOpPure *val, unsigned int size) { + rz_return_val_if_fail(val, NULL); + RzILOpEffect *set_val = SETL("_flags", val); RzILOpEffect *eff = SETG(EFLAGS(CF), LSB(VARL("_flags"))); @@ -1070,4 +1080,487 @@ RzILOpEffect *x86_il_set_flags(RZ_OWN RzILOpPure *val, unsigned int size) { return SEQ2(set_val, eff); } +/** + * \brief Check whether \p reg is an FPU stack register (ST0 - ST7) + * + * \param reg + */ +RZ_IPI bool x86_il_is_st_reg(X86Reg reg) { + return reg >= X86_REG_ST0 && reg <= X86_REG_ST7; +} + +/** + * \brief Get the 11th and 12th bit which stores the rounding mode from the FPU + * control word + * + * \return RzILOpPure* 2 bit rounding mode + */ +RZ_IPI RzILOpPure *x86_il_fpu_get_rmode() { + return UNSIGNED(2, SHIFTR0(VARG(X86_REG_FPU_CW), UN(8, 10))); +} + +/** + * \brief Get the float stored in FPU stack \p reg + * + * \param reg + * \return RzILOpFloat* IEEE754 80 bit float + */ +RZ_IPI RzILOpFloat *x86_il_get_st_reg(X86Reg reg) { + rz_return_val_if_fail(x86_il_is_st_reg(reg), NULL); + return BV2F(RZ_FLOAT_IEEE754_BIN_80, VARG(x86_registers[reg])); +} + +/** + * \brief Set the local variable to the value of "_rmode" computed using control + * word bits + * + * \return RzILOpEffect* + */ +RZ_IPI RzILOpEffect *init_rmode() { + return SETL("_rmode", x86_il_fpu_get_rmode()); +} + +/** + * \brief Execute the function \p f with the correct op mode argument + * + * \param f function which takes in the rounding mode as the first argument + * + * 0 -> RNE + * 1 -> RTN + * 2 -> RTP + * 3 -> RTZ + * + * I hate this, but this is the only way to conditionally use the correct rmode. + */ +#define EXEC_WITH_RMODE(f, ...) \ + ITE(EQ(VARL("_rmode"), UN(2, 0)), f(RZ_FLOAT_RMODE_RNE, __VA_ARGS__), \ + (EQ(VARL("_rmode"), UN(2, 1)), f(RZ_FLOAT_RMODE_RTN, __VA_ARGS__), \ + (EQ(VARL("_rmode"), UN(2, 2)), f(RZ_FLOAT_RMODE_RTP, __VA_ARGS__), \ + (f(RZ_FLOAT_RMODE_RTZ, __VA_ARGS__))))) + +RzILOpFloat *resize_floating_helper(RzFloatRMode rmode, RzFloatFormat format, RzILOpFloat *val) { + return FCONVERT(format, rmode, val); +} + +/** + * \brief Resize the float \p val to \p width + * You need to have initialized a local variable "_rmode" set with the rounding + * mode before you call this function. + * + * \param val Desirable that it is a small expression since it will be duped + * \param format Output float format + * \param ctx use_rmode gets set to true + * \return RzILOpFloat* + */ +RZ_IPI RzILOpFloat *x86_il_resize_floating_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *val, RzFloatFormat format, RZ_BORROW RZ_NONNULL X86ILContext *ctx) { + rz_return_val_if_fail(val && ctx, NULL); + ctx->use_rmode = true; + + /* TODO: Figure out a more elegant solution than to `DUP` the input val. */ + RzILOpFloat *ret = EXEC_WITH_RMODE(resize_floating_helper, format, DUP(val)); + rz_il_op_pure_free(val); + return ret; +} + +RzILOpFloat *sint2f_floating_helper(RzFloatRMode rmode, RzFloatFormat format, RzILOpBitVector *val) { + return SINT2F(format, rmode, val); +} + +/** + * \brief Convert the integer \p int_val to a RzILOpFloat of format \p fmt + * You need to have initialized a local variable "_rmode" set with the rounding + * mode before you call this function. + * + * \param int_val Desirable that it is a small expression since it will be duped + * \param format Output float format + * \param ctx use_rmode gets set to true + * \return RzILOpFloat* + */ +RZ_IPI RzILOpFloat *x86_il_floating_from_int_ctx(RZ_OWN RZ_NONNULL RzILOpBitVector *int_val, RzFloatFormat format, RZ_BORROW RZ_NONNULL X86ILContext *ctx) { + rz_return_val_if_fail(int_val && ctx, NULL); + + ctx->use_rmode = true; + RzILOpFloat *ret = EXEC_WITH_RMODE(sint2f_floating_helper, format, DUP(int_val)); + rz_il_op_pure_free(int_val); + return ret; +} + +RzILOpFloat *f2sint_floating_helper(RzFloatRMode rmode, ut32 width, RzILOpFloat *val) { + return F2SINT(width, rmode, val); +} + +/** + * \brief Convert the floating \p float_val to a RzILOpBitVector of size \p width + * You need to have initialized a local variable "_rmode" set with the rounding + * mode before you call this function. + * + * \param float_val Desirable that it is a small expression since it will be duped + * \param width Output bitvector width + * \param ctx use_rmode gets set to true + * \return RzILOpBitVector* + */ +RZ_IPI RzILOpBitVector *x86_il_int_from_floating_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *float_val, ut32 width, RZ_BORROW RZ_NONNULL X86ILContext *ctx) { + rz_return_val_if_fail(float_val && ctx, NULL); + ctx->use_rmode = true; + RzILOpFloat *ret = EXEC_WITH_RMODE(f2sint_floating_helper, width, DUP(float_val)); + rz_il_op_pure_free(float_val); + return ret; +} + +/** + * \brief Add \p x and \p y with the correct rounding mode as determined from + * the FPU control word + * + * \param x Desirable that it is a small expression since it will be duped + * \param y Desirable that it is a small expression since it will be duped + * \param ctx use_rmode gets set to true + * \return RzILOpFloat* sum + */ +RZ_IPI RzILOpFloat *x86_il_fadd_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx) { + rz_return_val_if_fail(x && y && ctx, NULL); + ctx->use_rmode = true; + RzILOpFloat *ret = EXEC_WITH_RMODE(FADD, DUP(x), DUP(y)); + + rz_il_op_pure_free(x); + rz_il_op_pure_free(y); + + return ret; +} + +/** + * \brief Multiply \p x and \p y with the correct rounding mode as determined + * from the FPU control word + * + * \param x Desirable that it is a small expression since it will be duped + * \param y Desirable that it is a small expression since it will be duped + * \param ctx use_rmode gets set to true + * \return RzILOpFloat* product + */ +RZ_IPI RzILOpFloat *x86_il_fmul_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx) { + rz_return_val_if_fail(x && y && ctx, NULL); + ctx->use_rmode = true; + RzILOpFloat *ret = EXEC_WITH_RMODE(FMUL, DUP(x), DUP(y)); + + rz_il_op_pure_free(x); + rz_il_op_pure_free(y); + + return ret; +} + +/** + * \brief Subtract \p x from \p y with the correct rounding mode as determined + * from the FPU control word + * + * \param x Desirable that it is a small expression since it will be duped + * \param y Desirable that it is a small expression since it will be duped + * \param ctx use_rmode gets set to true + * \return RzILOpFloat* difference + */ +RZ_IPI RzILOpFloat *x86_il_fsub_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx) { + rz_return_val_if_fail(x && y && ctx, NULL); + ctx->use_rmode = true; + // y - x, hence y is the first argument + RzILOpFloat *ret = EXEC_WITH_RMODE(FSUB, DUP(y), DUP(x)); + + rz_il_op_pure_free(x); + rz_il_op_pure_free(y); + + return ret; +} + +/** + * \brief Subtract \p y from \p x (reverse of \ref x86_il_fsub_with_rmode) + */ +RZ_IPI RzILOpFloat *x86_il_fsubr_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx) { + rz_return_val_if_fail(x && y && ctx, NULL); + return x86_il_fsub_with_rmode(y, x); +} + +/** + * \brief Divide \p x from \p y with the correct rounding mode as determined + * from the FPU control word + * + * \param x Desirable that it is a small expression since it will be duped + * \param y Desirable that it is a small expression since it will be duped + * \param ctx use_rmode gets set to true + * \return RzILOpFloat* division + */ +RZ_IPI RzILOpFloat *x86_il_fdiv_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx) { + rz_return_val_if_fail(x && y && ctx, NULL); + ctx->use_rmode = true; + // y / x, hence y is the first argument + RzILOpFloat *ret = EXEC_WITH_RMODE(FDIV, DUP(y), DUP(x)); + + rz_il_op_pure_free(x); + rz_il_op_pure_free(y); + + return ret; +} + +/** + * \brief Divide \p y from \p x (reverse of \ref x86_il_fdiv_with_rmode) + */ +RZ_IPI RzILOpFloat *x86_il_fdivr_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx) { + rz_return_val_if_fail(x && y && ctx, NULL); + return x86_il_fdiv_with_rmode(y, x); +} + +/** + * \brief Calculate the square root of \p x with the correct rounding mode as determined + * from the FPU control word + * + * \param x Desirable that it is a small expression since it will be duped + * \param ctx use_rmode gets set to true + * \return RzILOpFloat* square root + */ +RZ_IPI RzILOpFloat *x86_il_fsqrt_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_BORROW RZ_NONNULL X86ILContext *ctx) { + rz_return_val_if_fail(x && ctx, NULL); + ctx->use_rmode = true; + RzILOpFloat *ret = EXEC_WITH_RMODE(FSQRT, DUP(x)); + + rz_il_op_pure_free(x); + + return ret; +} + +/** + * \brief Store a float \p val at FPU stack \p reg + * + * \param reg + * \param val + * \param val_format Format of \p val + * \param ctx use_rmode gets set to true if any resizing of \p val is required + * \return RzILOpFloat* + */ +RZ_IPI RzILOpEffect *x86_il_set_st_reg_ctx(X86Reg reg, RZ_OWN RZ_NONNULL RzILOpFloat *val, RzFloatFormat val_format, RZ_BORROW X86ILContext *ctx) { + rz_return_val_if_fail(val && x86_il_is_st_reg(reg), NULL); + + if (val_format == RZ_FLOAT_IEEE754_BIN_80) { + return SETG(x86_registers[reg], F2BV(val)); + } else { + RzILOpFloat *converted_val = x86_il_resize_floating(val, RZ_FLOAT_IEEE754_BIN_80); + + return SETG(x86_registers[reg], F2BV(converted_val)); + } +} + +/** + * \brief Get the stack TOP stored in the FPU status word. + * TOP = FPU[12:15] (bits 12, 13 & 14) + * 12th bit is the least significant bit. + * + * \return RzILOpPure* Bitvector of length 3 + */ +RZ_IPI RzILOpPure *x86_il_get_fpu_stack_top() { + RzILOpPure *status_word = x86_il_get_reg_bits(X86_REG_FPSW, 0, 0); + return UNSIGNED(3, SHIFTR0(status_word, UN(8, 11))); +} + +/** + * \brief Set the value of FPU status word. + * See \ref x86_il_get_fpu_stack_top() for the structure of FPU status word and + * stack TOP. + * + * \param top Value to be stored as the new TOP (bitvector length = 3) + * \return RzILOpEffect* + */ +RZ_IPI RzILOpEffect *x86_il_set_fpu_stack_top(RZ_OWN RZ_NONNULL RzILOpPure *top) { + rz_return_val_if_fail(top, NULL); + + RzILOpPure *shifted_top = SHIFTL0(UNSIGNED(16, top), UN(8, 11)); + /* 0x3800 only has the 12, 13 & 14 bits set, so we take its negation for the + * mask. */ + RzILOpPure *mask = UN(16, ~(0x3800)); + RzILOpPure *new_fpsw = LOGOR(shifted_top, LOGAND(mask, x86_il_get_reg_bits(X86_REG_FPSW, 0, 0))); + return x86_il_set_reg_bits(X86_REG_FPSW, new_fpsw, 0); +} + +#define ST_MOVE_RIGHT(l, r) x86_il_set_st_reg(X86_REG_ST##r, x86_il_get_st_reg(X86_REG_ST##l), RZ_FLOAT_IEEE754_BIN_80) + +/** + * \brief Push \p val on the FPU stack + * + * \param val + * \param val_format Format of \p val + * \param ctx use_rmode gets set to true if any resizing of \p val is required + * \return RzILOpEffect* Push effect + */ +RZ_IPI RzILOpEffect *x86_il_st_push_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *val, RzFloatFormat val_format, RZ_BORROW X86ILContext *ctx) { + rz_return_val_if_fail(val, NULL); + + /* No need for a modulo here since the bitvector width will truncate any top + * value > 7 */ + RzILOpEffect *set_top = x86_il_set_fpu_stack_top(SUB(x86_il_get_fpu_stack_top(), UN(3, 1))); + RzILOpEffect *st_shift = SEQ8( + ST_MOVE_RIGHT(6, 7), + ST_MOVE_RIGHT(5, 6), + ST_MOVE_RIGHT(4, 5), + ST_MOVE_RIGHT(3, 4), + ST_MOVE_RIGHT(2, 3), + ST_MOVE_RIGHT(1, 2), + ST_MOVE_RIGHT(0, 1), + x86_il_set_st_reg(X86_REG_ST0, val, val_format)); + + /* Set C1 if stack overflow. If stack overflow occurred, then the value of + * stack TOP must be 0x7. */ + RzILOpEffect *set_overflow = x86_il_set_fpu_flag(X86_FPU_C1, EQ(x86_il_get_fpu_stack_top(), UN(3, 7))); + + return SEQ3(set_top, st_shift, set_overflow); +} + +#define ST_MOVE_LEFT(l, r) x86_il_set_st_reg(X86_REG_ST##l, x86_il_get_st_reg(X86_REG_ST##r), RZ_FLOAT_IEEE754_BIN_80) + +/** + * \brief Pop a value from the FPU stack + * + * \return RzILOpEffect* Pop effect + */ +RZ_IPI RzILOpEffect *x86_il_st_pop() { + /* We actually don't need a context here because we will never need to resize + * any value. */ + X86ILContext *ctx = NULL; + + RzILOpEffect *set_top = x86_il_set_fpu_stack_top(ADD(x86_il_get_fpu_stack_top(), UN(3, 1))); + RzILOpEffect *st_shift = SEQ7( + ST_MOVE_LEFT(0, 1), + ST_MOVE_LEFT(1, 2), + ST_MOVE_LEFT(2, 3), + ST_MOVE_LEFT(3, 4), + ST_MOVE_LEFT(4, 5), + ST_MOVE_LEFT(5, 6), + ST_MOVE_LEFT(6, 7)); + + /* Set C1 if stack underflow. If stack underflow occurred, then the value of + * stack TOP must be 0x0. */ + RzILOpEffect *set_underflow = x86_il_set_fpu_flag(X86_FPU_C1, EQ(x86_il_get_fpu_stack_top(), UN(3, 0))); + + return SEQ3(set_top, st_shift, set_underflow); +} + +RZ_IPI RzILOpBool *x86_il_get_fpu_flag(X86FPUFlags flag) { + RzILOpPure *shifted_fpsw = SHIFTR0(x86_il_get_reg_bits(X86_REG_FPSW, 0, 0), UN(8, flag)); + return NON_ZERO(UNSIGNED(1, shifted_fpsw)); +} + +RZ_IPI RzILOpEffect *x86_il_set_fpu_flag(X86FPUFlags flag, RZ_OWN RZ_NONNULL RzILOpBool *value) { + rz_return_val_if_fail(value, NULL); + + RzILOpPure *zero_mask = UN(16, ~(1 << flag)); + RzILOpPure *value_mask = SHIFTL0(BOOL_TO_BV(value, 16), UN(8, flag)); + RzILOpPure *new_fpsw = LOGOR(value_mask, LOGAND(zero_mask, x86_il_get_reg_bits(X86_REG_FPSW, 0, 0))); + return x86_il_set_reg_bits(X86_REG_FPSW, new_fpsw, 0); +} + +#define FLOATING_OP_MEM_WIDTH_CASE(n) \ + do { \ + case n: \ + return BV2F(RZ_FLOAT_IEEE754_BIN_##n, LOADW(n, x86_il_get_memaddr_bits(op.mem, bits, pc))); \ + } while (0) + +/** + * \brief Get the value of the floating point operand \p op + * This function takes care of everything, like choosing + * the correct typem returning the correct value and + * converting to the correct FP format + * Use the wrapper `x86_il_get_floating_op` + * + * \param op Operand to get + * \param bits bitness + * \param pc + */ +RZ_IPI RzILOpPure *x86_il_get_floating_operand_bits(X86Op op, int bits, ut64 pc) { + switch (op.type) { + case X86_OP_REG: + if (x86_il_is_st_reg(op.reg)) { + return x86_il_get_st_reg(op.reg); + } else { + RZ_LOG_ERROR("x86: RzIL: Invalid register passed as a floating point operand: %d\n", op.reg); + } + break; + case X86_OP_MEM: + switch (op.size * BITS_PER_BYTE) { + /* ~Duff's~ DMaroo's device */ + FLOATING_OP_MEM_WIDTH_CASE(32); + FLOATING_OP_MEM_WIDTH_CASE(64); + FLOATING_OP_MEM_WIDTH_CASE(80); + default: + RZ_LOG_ERROR("x86: RzIL: Invalid memory operand width for a floating point operand: %d\n", op.size); + } + break; + case X86_OP_INVALID: + case X86_OP_IMM: + default: + RZ_LOG_ERROR("x86: RzIL: Invalid param type encountered: %d\n", op.type); + } + + return NULL; +} + +#define FLOAT_WIDTH_TO_FORMAT_SWITCH_CASE(n) \ + do { \ + case n: \ + return RZ_FLOAT_IEEE754_BIN_##n; \ + } while (0) + +RZ_IPI RzFloatFormat x86_width_to_format(ut8 width) { + switch (width) { + FLOAT_WIDTH_TO_FORMAT_SWITCH_CASE(32); + FLOAT_WIDTH_TO_FORMAT_SWITCH_CASE(64); + FLOAT_WIDTH_TO_FORMAT_SWITCH_CASE(80); + FLOAT_WIDTH_TO_FORMAT_SWITCH_CASE(128); + default: + rz_warn_if_reached(); + return RZ_FLOAT_UNK; + } +} + +#define FLOAT_FORMAT_TO_WIDTH_SWITCH_CASE(n) \ + do { \ + case RZ_FLOAT_IEEE754_BIN_##n: \ + return n; \ + } while (0) + +RZ_IPI ut8 x86_format_to_width(RzFloatFormat format) { + return rz_float_get_format_info(format, RZ_FLOAT_INFO_TOTAL_LEN); +} + +/** + * \brief Set the value of the floating point operand \p op + * This function takes care of everything, like choosing + * the correct type, setting the correct value and + * converting to the correct FP format + * Use the wrapper `x86_il_set_floating_op` + * + * \param op Operand to be set + * \param val Value to be used + * \param val_format Format of \p val + * \param bits Bitness + * \param pc + * \param ctx use_rmode gets set to true if any resizing of \p val is required + */ +RZ_IPI RzILOpEffect *x86_il_set_floating_operand_bits_ctx(X86Op op, RZ_OWN RZ_NONNULL RzILOpFloat *val, RzFloatFormat val_format, int bits, ut64 pc, RZ_BORROW X86ILContext *ctx) { + rz_return_val_if_fail(val, NULL); + RzILOpEffect *ret = NULL; + + switch (op.type) { + case X86_OP_REG: + return x86_il_set_st_reg(op.reg, val, val_format); + case X86_OP_MEM: { + ut64 required_format = x86_width_to_format(op.size * BITS_PER_BYTE); + + RzILOpPure *resized_val = required_format == val_format ? val : x86_il_resize_floating(val, required_format); + return x86_il_set_mem_bits(op.mem, F2BV(resized_val), bits, pc); + } + case X86_OP_IMM: + default: + RZ_LOG_ERROR("x86: RzIL: Invalid param type encountered: %d\n", X86_OP_IMM); + return ret; + } +} + +RZ_IPI RzILOpEffect *x86_il_clear_fpsw_flags() { + RzILOpPure *new_fpsw = LOGAND(x86_il_get_reg_bits(X86_REG_FPSW, 0, 0), UN(16, 0x3f80)); + return x86_il_set_reg_bits(X86_REG_FPSW, new_fpsw, 0); +} + #include diff --git a/librz/analysis/arch/x86/common.h b/librz/analysis/arch/x86/common.h index afede0a847b..4468ed61e94 100644 --- a/librz/analysis/arch/x86/common.h +++ b/librz/analysis/arch/x86/common.h @@ -9,7 +9,7 @@ #define X86_BIT(x) UN(1, x) #define X86_TO32(x) UNSIGNED(32, x) -#define IL_LIFTER(mnem) static RzILOpEffect *x86_il_##mnem(const X86ILIns *ins, ut64 pc, RzAnalysis *analysis) +#define IL_LIFTER(mnem) static RzILOpEffect *x86_il_##mnem(const X86ILIns *ins, ut64 pc, RzAnalysis *analysis, X86ILContext *ctx) // Namespace clash with android-ndk-25b's x86_64-linux-android/asm/processor-flags.h #undef X86_EFLAGS_CF @@ -84,24 +84,114 @@ typedef enum x86_eflags_t { extern const char *x86_eflags_registers[X86_EFLAGS_ENDING]; -RzILOpPure *x86_il_get_reg_bits(X86Reg reg, int bits, uint64_t pc); -RzILOpEffect *x86_il_set_reg_bits(X86Reg reg, RzILOpPure *val, int bits); +RZ_IPI RzILOpPure *x86_il_get_reg_bits(X86Reg reg, int bits, uint64_t pc); +RZ_IPI RzILOpEffect *x86_il_set_reg_bits(X86Reg reg, RZ_OWN RZ_NONNULL RzILOpPure *val, int bits); -RzILOpPure *x86_il_get_operand_bits(X86Op op, int analysis_bits, ut64 pc, int implicit_size); -RzILOpEffect *x86_il_set_operand_bits(X86Op op, RzILOpPure *val, int bits, ut64 pc); +RZ_IPI RzILOpPure *x86_il_get_operand_bits(X86Op op, int analysis_bits, ut64 pc, int implicit_size); +RZ_IPI RzILOpEffect *x86_il_set_operand_bits(X86Op op, RZ_OWN RZ_NONNULL RzILOpPure *val, int bits, ut64 pc); -RzILOpPure *x86_il_get_memaddr_bits(X86Mem mem, int bits, ut64 pc); -RzILOpPure *x86_il_get_memaddr_segment_bits(X86Mem mem, X86Reg segment, int bits, ut64 pc); -RzILOpEffect *x86_il_set_mem_bits(X86Mem mem, RzILOpPure *val, int bits, ut64 pc); +RZ_IPI RzILOpPure *x86_il_get_memaddr_bits(X86Mem mem, int bits, ut64 pc); +RZ_IPI RzILOpPure *x86_il_get_memaddr_segment_bits(X86Mem mem, X86Reg segment, int bits, ut64 pc); +RZ_IPI RzILOpEffect *x86_il_set_mem_bits(X86Mem mem, RZ_OWN RZ_NONNULL RzILOpPure *val, int bits, ut64 pc); -RzILOpBool *x86_il_is_sub_borrow(RZ_OWN RzILOpPure *res, RZ_OWN RzILOpPure *x, RZ_OWN RzILOpPure *y); -RzILOpBitVector *x86_bool_to_bv(RzILOpBool *b, unsigned int bits); +RZ_IPI RzILOpBool *x86_il_is_add_carry(RZ_OWN RZ_NONNULL RzILOpPure *res, RZ_OWN RZ_NONNULL RzILOpPure *x, RZ_OWN RZ_NONNULL RzILOpPure *y); +RZ_IPI RzILOpBool *x86_il_is_sub_borrow(RZ_OWN RZ_NONNULL RzILOpPure *res, RZ_OWN RZ_NONNULL RzILOpPure *x, RZ_OWN RZ_NONNULL RzILOpPure *y); +RZ_IPI RzILOpBool *x86_il_is_add_overflow(RZ_OWN RZ_NONNULL RzILOpPure *res, RZ_OWN RZ_NONNULL RzILOpPure *x, RZ_OWN RZ_NONNULL RzILOpPure *y); +RZ_IPI RzILOpBool *x86_il_is_sub_underflow(RZ_OWN RZ_NONNULL RzILOpPure *res, RZ_OWN RZ_NONNULL RzILOpPure *x, RZ_OWN RZ_NONNULL RzILOpPure *y); -RzILOpEffect *x86_il_set_result_flags_bits(RZ_OWN RzILOpPure *result, int bits); -RzILOpEffect *x86_il_set_arithmetic_flags_bits(RZ_OWN RzILOpPure *res, RZ_OWN RzILOpPure *x, RZ_OWN RzILOpPure *y, bool addition, int bits); -RzILOpEffect *x86_il_set_arithmetic_flags_except_cf_bits(RZ_OWN RzILOpPure *res, RZ_OWN RzILOpPure *x, RZ_OWN RzILOpPure *y, bool addition, int bits); +RZ_IPI RzILOpEffect *x86_il_set_result_flags_bits(RZ_OWN RZ_NONNULL RzILOpPure *result, int bits); +RZ_IPI RzILOpEffect *x86_il_set_arithmetic_flags_bits(RZ_OWN RZ_NONNULL RzILOpPure *res, RZ_OWN RZ_NONNULL RzILOpPure *x, RZ_OWN RZ_NONNULL RzILOpPure *y, bool addition, int bits); +RZ_IPI RzILOpEffect *x86_il_set_arithmetic_flags_except_cf_bits(RZ_OWN RZ_NONNULL RzILOpPure *res, RZ_OWN RZ_NONNULL RzILOpPure *x, RZ_OWN RZ_NONNULL RzILOpPure *y, bool addition, int bits); -RzILOpPure *x86_il_get_flags(unsigned int size); -RzILOpEffect *x86_il_set_flags(RZ_OWN RzILOpPure *val, unsigned int size); +RZ_IPI RzILOpPure *x86_il_get_flags(unsigned int size); +RZ_IPI RzILOpEffect *x86_il_set_flags(RZ_OWN RZ_NONNULL RzILOpPure *val, unsigned int size); + +/* Capstone does not have the following FPU registers. */ + +/* FPU control word */ +#define X86_REG_FPU_CW "cwd" +/* FPU tag word */ +#define X86_REG_FPU_TW "ftw" +/* FPU last instruction opcode */ +#define X86_REG_FPU_OP "fop" +/* FPU instruction pointer */ +#define X86_REG_FPU_IP "frip" +/* FPU data pointer */ +#define X86_REG_FPU_DP "frdp" + +typedef enum { + X86_FPU_C0 = 8, + X86_FPU_C1 = 9, + X86_FPU_C2 = 10, + X86_FPU_C3 = 14, +} X86FPUFlags; + +RZ_IPI bool x86_il_is_st_reg(X86Reg reg); + +/* Need to pass in val_size as a param to avoid unnecessary rounding of val. */ + +RZ_IPI RzILOpFloat *x86_il_get_st_reg(X86Reg reg); +RZ_IPI RzILOpEffect *x86_il_set_st_reg_ctx(X86Reg reg, RZ_OWN RZ_NONNULL RzILOpFloat *val, RzFloatFormat val_format, RZ_BORROW X86ILContext *ctx); + +#define x86_il_set_st_reg(reg, val, val_format) x86_il_set_st_reg_ctx(reg, val, val_format, ctx) + +RZ_IPI RzILOpEffect *x86_il_set_fpu_stack_top(RZ_OWN RZ_NONNULL RzILOpPure *top); +RZ_IPI RzILOpPure *x86_il_get_fpu_stack_top(); + +RZ_IPI RzILOpEffect *x86_il_st_push_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *val, RzFloatFormat val_format, RZ_BORROW X86ILContext *ctx); +RZ_IPI RzILOpEffect *x86_il_st_pop(); + +#define x86_il_st_push(val, val_format) x86_il_st_push_ctx(val, val_format, ctx) + +#define X86_IL_ST_POP(val, eff) \ + do { \ + val = x86_il_get_st_reg(X86_REG_ST0); \ + eff = x86_il_st_pop(); \ + } while (0) + +RZ_IPI RzILOpPure *x86_il_get_fpu_flag(X86FPUFlags flag); +RZ_IPI RzILOpEffect *x86_il_set_fpu_flag(X86FPUFlags flag, RZ_OWN RZ_NONNULL RzILOpBool *value); + +RZ_IPI RzILOpPure *x86_il_fpu_get_rmode(); + +RZ_IPI RzILOpEffect *init_rmode(); + +RZ_IPI RzILOpFloat *x86_il_resize_floating_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *val, RzFloatFormat format, RZ_BORROW RZ_NONNULL X86ILContext *ctx); +RZ_IPI RzILOpFloat *x86_il_floating_from_int_ctx(RZ_OWN RZ_NONNULL RzILOpBitVector *int_val, RzFloatFormat format, RZ_BORROW RZ_NONNULL X86ILContext *ctx); +RZ_IPI RzILOpBitVector *x86_il_int_from_floating_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *float_val, ut32 width, RZ_BORROW RZ_NONNULL X86ILContext *ctx); + +RZ_IPI RzILOpFloat *x86_il_fadd_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx); +RZ_IPI RzILOpFloat *x86_il_fmul_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx); +RZ_IPI RzILOpFloat *x86_il_fsub_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx); +RZ_IPI RzILOpFloat *x86_il_fsubr_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx); +RZ_IPI RzILOpFloat *x86_il_fdiv_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx); +RZ_IPI RzILOpFloat *x86_il_fdivr_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx); +RZ_IPI RzILOpFloat *x86_il_fsqrt_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_BORROW RZ_NONNULL X86ILContext *ctx); + +#define x86_il_resize_floating(val, format) x86_il_resize_floating_ctx(val, format, ctx) +#define x86_il_floating_from_int(int_val, format) x86_il_floating_from_int_ctx(int_val, format, ctx) +#define x86_il_int_from_floating(float_val, width) x86_il_int_from_floating_ctx(float_val, width, ctx) +#define x86_il_fadd_with_rmode(x, y) x86_il_fadd_with_rmode_ctx(x, y, ctx) +#define x86_il_fmul_with_rmode(x, y) x86_il_fmul_with_rmode_ctx(x, y, ctx) +#define x86_il_fsub_with_rmode(x, y) x86_il_fsub_with_rmode_ctx(x, y, ctx) +#define x86_il_fsubr_with_rmode(x, y) x86_il_fsubr_with_rmode_ctx(x, y, ctx) +#define x86_il_fdiv_with_rmode(x, y) x86_il_fdiv_with_rmode_ctx(x, y, ctx) +#define x86_il_fdivr_with_rmode(x, y) x86_il_fdivr_with_rmode_ctx(x, y, ctx) +#define x86_il_fsqrt_with_rmode(x) x86_il_fsqrt_with_rmode_ctx(x, ctx) + +RZ_IPI RzILOpPure *x86_il_get_floating_operand_bits(X86Op op, int analysis_bits, ut64 pc); + +#define x86_il_get_floating_op(opnum) \ + x86_il_get_floating_operand_bits(ins->structure->operands[opnum], analysis->bits, pc) + +RZ_IPI RzFloatFormat x86_width_to_format(ut8 width); +RZ_IPI ut8 x86_format_to_width(RzFloatFormat format); + +RZ_IPI RzILOpEffect *x86_il_set_floating_operand_bits_ctx(X86Op op, RZ_OWN RZ_NONNULL RzILOpFloat *val, RzFloatFormat val_format, int bits, ut64 pc, RZ_BORROW X86ILContext *ctx); + +#define x86_il_set_floating_op(opnum, val, val_format) \ + x86_il_set_floating_operand_bits_ctx(ins->structure->operands[opnum], val, val_format, analysis->bits, pc, ctx) + +RZ_IPI RzILOpEffect *x86_il_clear_fpsw_flags(); #endif // X86_IL_COMMON_H diff --git a/librz/analysis/arch/x86/il_fp_ops.inc b/librz/analysis/arch/x86/il_fp_ops.inc new file mode 100644 index 00000000000..ac48b15cdcc --- /dev/null +++ b/librz/analysis/arch/x86/il_fp_ops.inc @@ -0,0 +1,697 @@ +// SPDX-FileCopyrightText: 2023 Dhruv Maroo +// SPDX-License-Identifier: LGPL-3.0-only + +/** + * \file il_fp_ops.c + * + * Contains the IL implementations for x86 floating point instructions. + * + * References: + * - https://docs.oracle.com/cd/E18752_01/html/817-5477/eoizy.html + * - https://eng.libretexts.org/Bookshelves/Computer_Science/Programming_Languages/x86-64_Assembly_Language_Programming_with_Ubuntu_(Jorgensen)/18%3A_Floating-Point_Instructions + * - https://en.wikibooks.org/wiki/X86_Assembly/Floating_Point#Floating-Point_Instruction_Set + * - https://github.com/avast/retdec/wiki/x86-FPU-semantic-model + * - https://redirect.cs.umbc.edu/courses/undergraduate/CMSC313/fall04/burt_katz/lectures/Lect12/floatingpoint.html + * - https://www.plantation-productions.com/Webster/www.artofasm.com/Windows/HTML/RealArithmetica2.html + */ + +#include "common.h" +#include + +/** + * FINIT/FNINIT + * Initialize x87 FPU + */ +IL_LIFTER(fninit) { + RzILOpEffect *set_cw = SETG(X86_REG_FPU_CW, UN(16, 0x37f)); + /* No need to set C0-C3 flags to zero, since we are setting the FPSW to 0, + * so all the flag bits will also be set to 0. */ + RzILOpEffect *set_sw = x86_il_set_reg(X86_REG_FPSW, UN(16, 0x0)); + RzILOpEffect *set_tw = SETG(X86_REG_FPU_TW, UN(16, 0xffff)); + RzILOpEffect *set_ip = SETG(X86_REG_FPU_IP, UN(32, 0x0)); + RzILOpEffect *set_dp = SETG(X86_REG_FPU_DP, UN(32, 0x0)); + + return SEQ5(set_cw, set_sw, set_tw, set_ip, set_dp); +} + +/** + * FLDCW m16 + * Load x87 FPU Control Word + */ +IL_LIFTER(fldcw) { + return SETG(X86_REG_FPU_CW, x86_il_get_op(0)); +} + +/** + * FSTCW/FNSTCW m2byte + * Store x87 FPU Control Word + */ +IL_LIFTER(fnstcw) { + return x86_il_set_op(0, VARG(X86_REG_FPU_CW)); +} + +/** + * FSTSW/FNSTSW {m2byte | AX} + * Store x87 FPU Status Word + */ +IL_LIFTER(fnstsw) { + return x86_il_set_op(0, x86_il_get_reg(X86_REG_FPSW)); +} + +/** + * FCLEX/FNCLEX + * Clear exceptions + */ +IL_LIFTER(fnclex) { + /* Zero out the 15th bit and 0-7 bits. */ + RzILOpPure *new_sw = LOGAND(x86_il_get_reg(X86_REG_FPSW), UN(16, 0x7f00)); + return SEQ2(x86_il_set_reg(X86_REG_FPSW, new_sw), x86_il_clear_fpsw_flags()); +} + +/** + * FLD + * Loads a floating point value and pushes it onto the FPU stack in ST(0) + */ +IL_LIFTER(fld) { + return x86_il_st_push(x86_il_get_floating_op(0), + x86_width_to_format(ins->structure->operands[0].size * BITS_PER_BYTE)); +} + +/** + * FST + * Stores the floating point value stored at the top of the FPU stack in ST(0) + */ +IL_LIFTER(fst) { + // TODO: Set the C1 bit depending on floating-point inexact exception (#P). + return x86_il_set_floating_op(0, x86_il_get_st_reg(X86_REG_ST0), RZ_FLOAT_IEEE754_BIN_80); +} + +// TODO: Implement undocumented instructions, have a look at #4045 for more. + +/** + * FSTP + * Stores the floating point value stored at the top of the FPU stack in ST(0) + * and pops the value off the stack + */ +IL_LIFTER(fstp) { + RzILOpEffect *pop_eff; + RzILOpPure *pop_val; + X86_IL_ST_POP(pop_val, pop_eff); + + return SEQ2(x86_il_set_floating_op(0, pop_val, RZ_FLOAT_IEEE754_BIN_80), pop_eff); +} + +/** + * FLD1 + * Load +1.0 + */ +IL_LIFTER(fld1) { + return x86_il_st_push(F80(1.0), RZ_FLOAT_IEEE754_BIN_80); +} + +/** + * FLDZ + * Load +0.0 + */ +IL_LIFTER(fldz) { + return x86_il_st_push(F80(0.0), RZ_FLOAT_IEEE754_BIN_80); +} + +/* + * 128-bit representation of h for value v, where + * + * v = (h - 1) * 2^x + * + * Here x is the exponent. The reason why we are computing h is because the + * first 66 bits of the mantissa of h are stored as the internal constants in + * the FPU and should be used for rounding. In our case, we will directly use + * + * log2(10) = 3fffd49a784bcd1b8afe492bf6ff1e13 + * log2(e) = 3fffb8aa3b295c17f0bbbe87fed055ed + * pi = 4000c90fdaa22168c234c4c6628b8361 + * log10(2) = 3fff9a209a84fbcff7988f8959ac200d + * ln(2) = 3ffeb17217f7d1cf79abc9e3b39828ef + */ + +#define FPU_L2T 0x3fffd49a784bcd1bULL, 0x8afe492bf6ff1e13ULL +#define FPU_L2E 0x3fffb8aa3b295c17ULL, 0xf0bbbe87fed055edULL +#define FPU_PI 0x4000c90fdaa22168ULL, 0xc234c4c6628b8361ULL +#define FPU_LG2 0x3fff9a209a84fbcfULL, 0xf7988f8959ac200dULL +#define FPU_LN2 0x3ffeb17217f7d1cfULL, 0x79abc9e3b39828efULL + +RzILOpFloat *math_const_to_float_ctx(uint64_t upper, uint64_t lower, X86ILContext *ctx) { + RzILOpPure *upper_unshifted = UN(128, upper); + RzILOpPure *upper_shifted = SHIFTL0(upper_unshifted, UN(8, 8)); + + uint64_t stripped_lower = lower & (0x3ULL << 62); + RzILOpPure *final_bits = LOGOR(upper_shifted, UN(128, stripped_lower)); + + /* We recast the 128-bit value (having only 66 non-zero bits) to an 80-bit + * value to emulate the rounding effect of rounding a 66-bit value. */ + return x86_il_resize_floating(BV2F(RZ_FLOAT_IEEE754_BIN_128, final_bits), RZ_FLOAT_IEEE754_BIN_80); +} + +#define math_const_to_float(upper_lower) math_const_to_float_ctx(upper_lower, ctx) + +/** + * FLDL2T + * Load log2(10) + */ +IL_LIFTER(fldl2t) { + return x86_il_st_push(math_const_to_float(FPU_L2T), RZ_FLOAT_IEEE754_BIN_80); +} + +/** + * FLDL2E + * Load log2(e) + */ +IL_LIFTER(fldl2e) { + return x86_il_st_push(math_const_to_float(FPU_L2E), RZ_FLOAT_IEEE754_BIN_80); +} + +/** + * FLDPI + * Load pi + */ +IL_LIFTER(fldpi) { + return x86_il_st_push(math_const_to_float(FPU_PI), RZ_FLOAT_IEEE754_BIN_80); +} + +/** + * FLDLG2 + * Load log10(2) + */ +IL_LIFTER(fldlg2) { + return x86_il_st_push(math_const_to_float(FPU_LG2), RZ_FLOAT_IEEE754_BIN_80); +} + +/** + * FLDLN2 + * Load ln(2) + */ +IL_LIFTER(fldln2) { + return x86_il_st_push(math_const_to_float(FPU_LN2), RZ_FLOAT_IEEE754_BIN_80); +} + +/** + * FXCH + * Exchange the contents of FPU stack register with ST(0) + */ +IL_LIFTER(fxch) { + X86Reg reg; + + if (ins->structure->op_count == 0) { + /* Use ST1 as the default reg in case no operand is provided. */ + reg = X86_REG_ST1; + } else { + reg = ins->structure->operands[1].reg; + } + + /* TODO: The IL generated from the following code is too verbose because of + many rounding checks, there are ways to remove this sort of rounding checks, + but it doesn't matter for now so I'm not bothering with it. */ + return SEQ4( + SETL("tmp", x86_il_get_st_reg(X86_REG_ST0)), + x86_il_set_st_reg(X86_REG_ST0, x86_il_get_st_reg(reg), RZ_FLOAT_IEEE754_BIN_80), + x86_il_set_st_reg(reg, VARL("tmp"), RZ_FLOAT_IEEE754_BIN_80), + x86_il_set_fpu_flag(X86_FPU_C1, IL_FALSE)); +} + +/** + * FILD + * Load integer onto the FPU register stack + */ +IL_LIFTER(fild) { + RzILOpPure *int_val = x86_il_get_op(0); + RzILOpFloat *float_val = x86_il_floating_from_int(int_val, RZ_FLOAT_IEEE754_BIN_80); + + return x86_il_st_push(float_val, RZ_FLOAT_IEEE754_BIN_80); +} + +/** + * FIST + * Store float in ST(0) after rounding to integer + */ +IL_LIFTER(fist) { + RzILOpPure *int_val = x86_il_int_from_floating(x86_il_get_st_reg(X86_REG_ST0), ins->structure->operands[0].size * BITS_PER_BYTE); + return x86_il_set_op(0, int_val); +} + +/** + * FISTP + * Store float in ST(0) after rounding to integer, pop the FPU register stack + */ +IL_LIFTER(fistp) { + RzILOpEffect *pop_eff; + RzILOpPure *pop_val; + X86_IL_ST_POP(pop_val, pop_eff); + + RzILOpPure *int_val = x86_il_int_from_floating(pop_val, ins->structure->operands[0].size * BITS_PER_BYTE); + return SEQ2(x86_il_set_op(0, int_val), pop_eff); +} + +/** + * FBLD + * Load binary coded decimal in ST(0) + * 80-bit BCD (18-digits) := [sign-byte] + 9 * [data-bytes] + */ +IL_LIFTER(fbld) { + ut8 mem_size = analysis->bits; + + RzILOpEffect *mem_init = SETL("mem", x86_il_get_memaddr(ins->structure->operands[0].mem)); + RzILOpEffect *i_init = SETL("i", UN(mem_size, 8)); + RzILOpEffect *val_init = SETL("val", UN(64, 0)); + + RzILOpPure *byte_mem = ADD(VARL("mem"), VARL("i")); + RzILOpEffect *set_byte = SETL("byte", LOADW(8, byte_mem)); + + RzILOpPure *new_val = ADD( + MUL(VARL("val"), UN(64, 100)), // hundredths position (old val) + UNSIGNED(64, ADD(MUL(SHIFTR0(VARL("byte"), UN(8, 4)), UN(8, 10)), // tenths position (upper nibble) + LOGAND(VARL("byte"), UN(8, 0xf)) // ones position (lower nibble) + ))); + + RzILOpEffect *bcd_decode_loop = REPEAT( // while + UGE(VARL("i"), UN(mem_size, 0)), // i >= 0 + SEQ3( + set_byte, // get byte + SETL("val", new_val), // update val + SETL("i", SUB(VARL("i"), UN(mem_size, 1))) // i-- + )); + + RzILOpEffect *f_init = SETL("f", x86_il_floating_from_int(VARL("val"), RZ_FLOAT_IEEE754_BIN_80)); + + /* Check sign byte (index 9) checking if sign byte is zero */ + RzILOpPure *sign_byte = LOADW(8, ADD(VARL("mem"), UN(mem_size, 9))); + RzILOpFloat *final_float = ITE(IS_ZERO(sign_byte), VARL("f"), FNEG(VARL("f"))); + + return SEQ6( + mem_init, i_init, val_init, // Local vars init + bcd_decode_loop, // BCD decoding loop + f_init, // Conversion to 80-bit float + x86_il_st_push(final_float, RZ_FLOAT_IEEE754_BIN_80) // Push the value onto the FPU stack + ); +} + +/** + * FBSTP + * Pop the float in ST(0), convert it to BCD and store + */ +IL_LIFTER(fbstp) { + ut8 mem_size = analysis->bits; + + RzILOpEffect *pop_eff; + RzILOpPure *pop_val; + X86_IL_ST_POP(pop_val, pop_eff); + + RzILOpEffect *val_init = SETL("val", x86_il_int_from_floating(pop_val, 64)); + RzILOpEffect *sgn_init = SETL("sgn", MSB(VARL("val"))); + RzILOpEffect *val_abs = SETL("val", ITE(VARL("sgn"), NEG(VARL("val")), VARL("val"))); + + RzILOpEffect *mem_init = SETL("mem", x86_il_get_memaddr(ins->structure->operands[0].mem)); + RzILOpEffect *i_init = SETL("i", UN(mem_size, 0)); + RzILOpPure *byte_mem = ADD(VARL("mem"), VARL("i")); + + RzILOpPure *upper_nibble = DIV(MOD(VARL("val"), UN(64, 100)), UN(64, 10)); + RzILOpPure *lower_nibble = MOD(VARL("val"), UN(64, 10)); + RzILOpPure *new_byte = UNSIGNED(8, LOGOR(SHIFTL0(upper_nibble, UN(8, 4)), lower_nibble)); + + RzILOpEffect *bcd_encode_loop = REPEAT( // while + ULT(VARL("i"), UN(mem_size, 9)), // i < 9 + SEQ3( + STOREW(byte_mem, new_byte), // store byte + SETL("val", DIV(VARL("val"), UN(64, 100))), // val /= 100 + SETL("i", ADD(VARL("i"), UN(mem_size, 1))) // i++ + )); + + RzILOpEffect *update_mem = SETL("mem", DUP(byte_mem)); + RzILOpEffect *store_sign = BRANCH(VARL("sgn"), STOREW(VARL("mem"), UN(8, 0xff)), STOREW(VARL("mem"), UN(8, 0))); + + RzILOpEffect *noexcept_case = SEQ5( + mem_init, i_init, // init loop vars + bcd_encode_loop, // convert val to bcd + update_mem, store_sign // update mem pointer and store the saved sign in the bcd + ); + RzILOpEffect *maybe_except = BRANCH( + SGE(VARL("val"), UN(64, 1e18)), // |val| >= 1e18 + GOTO("int"), // throw exception if val can't fit in 18-digit BCD + noexcept_case); + + return SEQ5( + val_init, pop_eff, // get val from ST(0) and pop + sgn_init, val_abs, // val = |val| and store sign + maybe_except); +} + +/* Arithmetic instructions */ + +/** + * FABS + * Clears the sign bit of ST(0) to create absolute value + */ +IL_LIFTER(fabs) { + RzILOpFloat *abs_value = FABS(x86_il_get_st_reg(X86_REG_ST0)); + return SEQ2(x86_il_set_st_reg(X86_REG_ST0, abs_value, RZ_FLOAT_IEEE754_BIN_80), x86_il_set_fpu_flag(X86_FPU_C1, IL_FALSE)); +} + +#define FLOATING_ARITHMETIC_IL(op) \ + do { \ + RzILOpFloat *src; \ + X86Reg dest_reg; \ +\ + /* TODO: Check whether all the enumerated cases here are correct, through \ + * code coverage. */ \ + switch (ins->structure->op_count) { \ + case 1: \ + /* Need to convert a 32-bit or 64-bit memory operand */ \ + dest_reg = X86_REG_ST0; \ + src = x86_il_resize_floating(x86_il_get_floating_op(0), RZ_FLOAT_IEEE754_BIN_80); \ + break; \ + case 2: \ + /* ST(i) operand, so no need for resizing */ \ + dest_reg = ins->structure->operands[0].reg; \ + src = x86_il_get_floating_op(0); \ + break; \ + default: \ + rz_warn_if_reached(); \ + return NULL; \ + } \ +\ + RzILOpFloat *result = x86_il_##op##_with_rmode(src, x86_il_get_st_reg(dest_reg)); \ + return x86_il_set_st_reg(dest_reg, result, RZ_FLOAT_IEEE754_BIN_80); \ + } while (0) + +#define FLOATING_ARITHMETIC_POP_IL(op) \ + do { \ + X86Reg dest_reg = X86_REG_ST1; \ +\ + if (ins->structure->op_count == 2) { \ + /* Destination register passed in as the first operand */ \ + dest_reg = ins->structure->operands[0].reg; \ + } \ +\ + RzILOpPure *result = x86_il_##op##_with_rmode(x86_il_get_st_reg(X86_REG_ST0), x86_il_get_st_reg(dest_reg)); \ + return SEQ2(x86_il_set_st_reg(dest_reg, result, RZ_FLOAT_IEEE754_BIN_80), x86_il_st_pop()); \ + } while (0) + +#define FLOATING_INT_ARITHMETIC_IL(op) \ + do { \ + RzILOpPure *float_val = x86_il_floating_from_int(x86_il_get_op(0), RZ_FLOAT_IEEE754_BIN_80); \ + RzILOpPure *result = x86_il_##op##_with_rmode(float_val, x86_il_get_st_reg(X86_REG_ST0)); \ + return x86_il_set_st_reg(X86_REG_ST0, result, RZ_FLOAT_IEEE754_BIN_80); \ + } while (0) + +/** + * FADD + * Add floating point values + */ +IL_LIFTER(fadd) { + /* Have a unified IL lifter for FADD and FADDP since Capstone has removed the + * distinction after version 4, which I think is a terrible thing. */ + if (ins->structure->opcode[0] == 0xde) { + // FADDP + FLOATING_ARITHMETIC_POP_IL(fadd); + } else { + // FADD + FLOATING_ARITHMETIC_IL(fadd); + } +} + +/** + * FIADD + * Add an integer to ST(0) + */ +IL_LIFTER(fiadd) { + FLOATING_INT_ARITHMETIC_IL(fadd); +} + +/** + * FMUL + * Multiply floating point values + */ +IL_LIFTER(fmul) { + FLOATING_ARITHMETIC_IL(fmul); +} + +/** + * FMULP + * Multiply ST(0) to ST(i) and pop the stack + */ +IL_LIFTER(fmulp) { + FLOATING_ARITHMETIC_POP_IL(fmul); +} + +/** + * FIMUL + * Multiply an integer to ST(0) + */ +IL_LIFTER(fimul) { + FLOATING_INT_ARITHMETIC_IL(fmul); +} + +/** + * FSUB + * Subtract floating point value + */ +IL_LIFTER(fsub) { + FLOATING_ARITHMETIC_IL(fsub); +} + +/** + * FSUBP + * Subtract ST(0) from ST(i) and pop the stack + */ +IL_LIFTER(fsubp) { + FLOATING_ARITHMETIC_POP_IL(fsub); +} + +/** + * FISUB + * Subtract an integer from ST(0) + */ +IL_LIFTER(fisub) { + FLOATING_INT_ARITHMETIC_IL(fsub); +} + +/** + * FSUBR + * Reverse subtract floating point value + */ +IL_LIFTER(fsubr) { + FLOATING_ARITHMETIC_IL(fsubr); +} + +/** + * FSUBRP + * Subtract ST(i) from ST(0), store the result in ST(i) and pop the stack + */ +IL_LIFTER(fsubrp) { + FLOATING_ARITHMETIC_POP_IL(fsubr); +} + +/** + * FISUBR + * Subtract ST(0) from an integer and store the result in ST(0) + */ +IL_LIFTER(fisubr) { + FLOATING_INT_ARITHMETIC_IL(fsubr); +} + +/** + * FDIV + * Divide floating point value + */ +IL_LIFTER(fdiv) { + FLOATING_ARITHMETIC_IL(fdiv); +} + +/** + * FDIVP + * Divide ST(0) from ST(i) and pop the stack + */ +IL_LIFTER(fdivp) { + FLOATING_ARITHMETIC_POP_IL(fdiv); +} + +/** + * FIDIV + * Divide an integer from ST(0) + */ +IL_LIFTER(fidiv) { + FLOATING_INT_ARITHMETIC_IL(fdiv); +} + +/** + * FDIVR + * Reverse divide floating point value + */ +IL_LIFTER(fdivr) { + FLOATING_ARITHMETIC_IL(fdivr); +} + +/** + * FDIVRP + * Divide ST(i) from ST(0), store the result in ST(i) and pop the stack + */ +IL_LIFTER(fdivrp) { + FLOATING_ARITHMETIC_POP_IL(fdiv); +} + +/** + * FIDIVR + * Divide ST(0) from an integer and store the result in ST(0) + */ +IL_LIFTER(fidivr) { + FLOATING_INT_ARITHMETIC_IL(fdivr); +} + +RzILOpEffect *fcom_helper(const X86ILIns *ins, ut64 pc, RzAnalysis *analysis, RzILOpPure *op1_override) { + RzILOpPure *st0 = x86_il_get_st_reg(X86_REG_ST0); + RzILOpPure *op1; + + if (op1_override) { + op1 = op1_override; + } else if (ins->structure->op_count == 0) { + /* ST(1) is the default operand */ + op1 = x86_il_get_st_reg(X86_REG_ST1); + } else { + op1 = x86_il_get_floating_op(0); + } + + // TODO: Set the C0, C2, C3 bits depending on invalid arithmetic operand exception (#IA). + return SEQ4( + x86_il_set_fpu_flag(X86_FPU_C0, FLT(st0, op1)), + x86_il_set_fpu_flag(X86_FPU_C1, IL_FALSE), + x86_il_set_fpu_flag(X86_FPU_C2, IL_FALSE), + x86_il_set_fpu_flag(X86_FPU_C3, FEQ(DUP(st0), DUP(op1)))); +} + +/** + * FCOM + * Compare floating point values and store the result in the FPU control word + */ +IL_LIFTER(fcom) { + return fcom_helper(ins, pc, analysis, NULL); +} + +/** + * FCOMP + * Compare floating point values, store the result in the FPU control word and pop the stack + */ +IL_LIFTER(fcomp) { + return SEQ2(fcom_helper(ins, pc, analysis, NULL), x86_il_st_pop()); +} + +/** + * FICOM + * Compare the floating point value in ST(0) with an integer and store the result in the FPU control word + */ +IL_LIFTER(ficom) { + return fcom_helper(ins, pc, analysis, x86_il_floating_from_int(x86_il_get_op(0), RZ_FLOAT_IEEE754_BIN_80)); +} + +/** + * FCOMPP + * Compare floating point values, store the result in the FPU control word and pop the stack twice + */ +IL_LIFTER(fcompp) { + /* This function takes in no operands, so we pass in the [op1_override] argument in [fcom_helper]. */ + return SEQ3(fcom_helper(ins, pc, analysis, x86_il_get_st_reg(X86_REG_ST1)), x86_il_st_pop(), x86_il_st_pop()); +} + +/** + * FICOMP + * Compare the floating point value in ST(0) with an integer, store the result in the FPU control word and pop the stack + */ +IL_LIFTER(ficomp) { + return SEQ2(fcom_helper(ins, pc, analysis, x86_il_floating_from_int(x86_il_get_op(0), RZ_FLOAT_IEEE754_BIN_80)), x86_il_st_pop()); +} + +RzILOpEffect *fcomi_helper(const X86ILIns *ins, ut64 pc, RzAnalysis *analysis) { + RzILOpPure *st0 = x86_il_get_st_reg(X86_REG_ST0); + RzILOpPure *sti = x86_il_get_floating_op(0); + + // TODO: Set the ZF, PF, CF depending on invalid arithmetic operand exception (#IA). + return SEQ4( + x86_il_set_fpu_flag(X86_FPU_C1, IL_FALSE), + SETG(EFLAGS(ZF), FEQ(st0, sti)), + SETG(EFLAGS(PF), IL_FALSE), + SETG(EFLAGS(CF), FLT(DUP(st0), DUP(sti)))); +} + +/** + * FCOMI + * Compare ST(0) and ST(i) and set the EFLAGS accordingly + */ +IL_LIFTER(fcomi) { + return fcomi_helper(ins, pc, analysis); +} + +/** + * FCOMIP + * Compare ST(0) and ST(i), set the EFLAGS accordingly and pop the stack + */ +IL_LIFTER(fcomip) { + return SEQ2(fcomi_helper(ins, pc, analysis), x86_il_st_pop()); +} + +/** + * FCHS + * Change the sign of ST(0) + */ +IL_LIFTER(fchs) { + return SEQ2( + x86_il_set_st_reg(X86_REG_ST0, FNEG(x86_il_get_st_reg(X86_REG_ST0)), RZ_FLOAT_IEEE754_BIN_80), + x86_il_set_fpu_flag(X86_FPU_C1, IL_FALSE)); +} + +/** + * FTST + * Test the value in ST(0) (i.e. compare with 0.0) + */ +IL_LIFTER(ftst) { + /* We reuse the [fcom_helper] function here by passing in the [op1_override] argument. */ + return fcom_helper(ins, pc, analysis, F80(0.0)); +} + +/** + * FRNDINT + * Round ST(0) to an integer + */ +IL_LIFTER(frndint) { + return x86_il_set_st_reg(X86_REG_ST0, + /* Not very sure about whether the rounded integer should be limited to 64 bits or not. */ + x86_il_floating_from_int(x86_il_int_from_floating(x86_il_get_st_reg(X86_REG_ST0), 64), RZ_FLOAT_IEEE754_BIN_80), + RZ_FLOAT_IEEE754_BIN_80); +} + +/** + * FSQRT + * Calculate the square root of ST(0) + */ +IL_LIFTER(fsqrt) { + return x86_il_set_st_reg(X86_REG_ST0, x86_il_fsqrt_with_rmode(x86_il_get_st_reg(X86_REG_ST0)), RZ_FLOAT_IEEE754_BIN_80); +} + +/** + * FNOP + * No-op + */ +IL_LIFTER(fnop) { + return NOP(); +} + +/** + * FISTTP + * Round ST(0) to an integer (using RZ_FLOAT_RMODE_RTZ), store the integer in the memory operand and pop the stack + */ +IL_LIFTER(fisttp) { + return SEQ2( + x86_il_set_op(0, + x86_il_int_from_floating( + x86_il_get_st_reg(X86_REG_ST0), + ins->structure->operands[0].size * BITS_PER_BYTE)), + x86_il_st_pop()); +} + +#include diff --git a/librz/analysis/arch/x86/il_ops.inc b/librz/analysis/arch/x86/il_ops.inc index 8bc3ee63ee0..d61e3d3a2ca 100644 --- a/librz/analysis/arch/x86/il_ops.inc +++ b/librz/analysis/arch/x86/il_ops.inc @@ -156,7 +156,7 @@ IL_LIFTER(adc) { RzILOpEffect *op2 = SETL("op2", x86_il_get_op(1)); RzILOpPure *cf = VARG(EFLAGS(CF)); - RzILOpEffect *sum = SETL("sum", ADD(ADD(VARL("op1"), VARL("op2")), x86_bool_to_bv(cf, ins->structure->operands[0].size * BITS_PER_BYTE))); + RzILOpEffect *sum = SETL("sum", ADD(ADD(VARL("op1"), VARL("op2")), BOOL_TO_BV(cf, ins->structure->operands[0].size * BITS_PER_BYTE))); RzILOpEffect *set_dest = x86_il_set_op(0, VARL("sum")); RzILOpEffect *set_res_flags = x86_il_set_result_flags(VARL("sum")); RzILOpEffect *set_arith_flags = x86_il_set_arithmetic_flags(VARL("sum"), VARL("op1"), VARL("op2"), true); @@ -633,25 +633,20 @@ IL_LIFTER(div) { return SEQ2(op, BRANCH(IS_ZERO(VARL("_src")), NULL, ret)); } -// /** -// * ESC -// * Escape to coprocessor instruction set -// * To be used with floating-point unit -// */ -// IL_LIFTER(esc) { -// /* Not necessary to implement for binary analysis */ -// return EMPTY(); -// } +/** + * ESC + * Escape to coprocessor instruction set + * To be used with floating-point unit + * Not necessary to implement for binary analysis + */ /** * HLT * Enter HALT state */ IL_LIFTER(hlt) { - /* It just jumps to an empty goto label "halt" - Also need an EMPTY() instruction after it to denote - the end of analysis and restart all IL analysis */ - return SEQ2(GOTO("halt"), EMPTY()); + /* It just jumps to an empty goto label "halt" */ + return GOTO("halt"); } void label_halt(RzILVM *vm, RzILOpEffect *op) { @@ -827,10 +822,8 @@ IL_LIFTER(imul) { * Encodings: I, ZO */ IL_LIFTER(in) { - /* It just jumps to an empty goto label "port" - Also need an EMPTY() instruction after it to denote - the end of analysis and restart all IL analysis */ - return SEQ2(GOTO("port"), EMPTY()); + /* It just jumps to an empty goto label "port" */ + return GOTO("port"); } void label_port(RzILVM *vm, RzILOpEffect *op) { @@ -860,10 +853,8 @@ IL_LIFTER(inc) { * Encodings: I, ZO */ IL_LIFTER(int) { - /* For now, it just jumps to an empty goto label "int" - Also need an EMPTY() instruction after it to denote - the end of analysis and restart all IL analysis */ - return SEQ2(GOTO("int"), EMPTY()); + /* For now, it just jumps to an empty goto label "int" */ + return GOTO("int"); } void label_int(RzILVM *vm, RzILOpEffect *op) { @@ -876,17 +867,14 @@ void label_int(RzILVM *vm, RzILOpEffect *op) { * Call to interrupt if overflow flag set */ IL_LIFTER(into) { - return BRANCH(VARG(EFLAGS(OF)), SEQ2(GOTO("int"), EMPTY()), NOP()); + return BRANCH(VARG(EFLAGS(OF)), GOTO("int"), NOP()); } -// /** -// * IRET -// * Return from interrupt -// */ -// IL_LIFTER(iret) { -// /* TODO: Implement IRET properly */ -// return EMPTY(); -// } +// TODO: Implement IRET +/** + * IRET + * Return from interrupt + */ #define JUMP_IL() \ do { \ @@ -1527,10 +1515,8 @@ IL_LIFTER(or) { * Encodings: I, ZO */ IL_LIFTER(out) { - /* It just jumps to an empty goto label "port" - Also need an EMPTY() instruction after it to denote - the end of analysis and restart all IL analysis */ - return SEQ2(GOTO("port"), EMPTY()); + /* It just jumps to an empty goto label "port" */ + return GOTO("port"); } typedef struct pop_helper_t { @@ -1663,15 +1649,8 @@ IL_LIFTER(call) { * We also need to push the code segment register in case 16 and 32 bit modes. */ - RzILOpEffect *push_stuff = NULL; - - if (analysis->bits == 64) { - push_stuff = x86_push_helper(U64(pc), 8); - } else { - push_stuff = SEQ4(SETL("_cs", UNSIGNED(analysis->bits, x86_il_get_reg(X86_REG_CS))), x86_push_helper(VARL("_cs"), analysis->bits / BITS_PER_BYTE), SETL("_pc", UN(analysis->bits, pc)), x86_push_helper(VARL("_pc"), analysis->bits / BITS_PER_BYTE)); - } - - return SEQ2(push_stuff, JMP(x86_il_get_op(0))); + RzILOpEffect *push_pc = x86_push_helper(UN(analysis->bits, pc), analysis->bits / BITS_PER_BYTE); + return SEQ2(push_pc, JMP(x86_il_get_op(0))); } /** @@ -1800,7 +1779,7 @@ IL_LIFTER(rcl) { RzILOpBool *cond = NON_ZERO(VARL("_tmp_cnt")); RzILOpEffect *repeat = SETL("_tmp_cf", MSB(VARL("_dest"))); - repeat = SEQ2(repeat, SETL("_dest", ADD(SHIFTL0(VARL("_dest"), U8(1)), x86_bool_to_bv(VARG(EFLAGS(CF)), BITS_PER_BYTE * size)))); + repeat = SEQ2(repeat, SETL("_dest", ADD(SHIFTL0(VARL("_dest"), U8(1)), BOOL_TO_BV(VARG(EFLAGS(CF)), BITS_PER_BYTE * size)))); repeat = SEQ2(repeat, SETG(EFLAGS(CF), VARL("_tmp_cf"))); repeat = SEQ2(repeat, SETL("_tmp_cnt", SUB(VARL("_tmp_cnt"), UN(tmp_count_size, 1)))); @@ -1826,7 +1805,7 @@ IL_LIFTER(rcr) { RzILOpBool *cond = NON_ZERO(VARL("_tmp_cnt")); RzILOpEffect *repeat = SETL("_tmp_cf", LSB(VARL("_dest"))); - repeat = SEQ2(repeat, SETL("_dest", ADD(SHIFTR0(VARL("_dest"), U8(1)), SHIFTL0(x86_bool_to_bv(VARG(EFLAGS(CF)), BITS_PER_BYTE * size), U8(size))))); + repeat = SEQ2(repeat, SETL("_dest", ADD(SHIFTR0(VARL("_dest"), U8(1)), SHIFTL0(BOOL_TO_BV(VARG(EFLAGS(CF)), BITS_PER_BYTE * size), U8(size))))); repeat = SEQ2(repeat, SETG(EFLAGS(CF), VARL("_tmp_cf"))); repeat = SEQ2(repeat, SETL("_tmp_cnt", SUB(VARL("_tmp_cnt"), UN(tmp_count_size, 1)))); @@ -1862,7 +1841,7 @@ IL_LIFTER(rol) { RzILOpBool *cond = NON_ZERO(VARL("_tmp_cnt")); RzILOpEffect *repeat = SETL("_tmp_cf", MSB(VARL("_dest"))); - repeat = SEQ2(repeat, SETL("_dest", ADD(SHIFTL0(VARL("_dest"), U8(1)), x86_bool_to_bv(VARL("_tmp_cf"), BITS_PER_BYTE * size)))); + repeat = SEQ2(repeat, SETL("_dest", ADD(SHIFTL0(VARL("_dest"), U8(1)), BOOL_TO_BV(VARL("_tmp_cf"), BITS_PER_BYTE * size)))); repeat = SEQ2(repeat, SETL("_tmp_cnt", SUB(VARL("_tmp_cnt"), UN(cnt_size, 1)))); RzILOpBool *if_cond1 = NON_ZERO(VARL("_masked")); @@ -1887,7 +1866,7 @@ IL_LIFTER(ror) { RzILOpBool *cond = NON_ZERO(VARL("_tmp_cnt")); RzILOpEffect *repeat = SETL("_tmp_cf", LSB(VARL("_dest"))); - repeat = SEQ2(repeat, SETL("_dest", ADD(SHIFTR0(VARL("_dest"), U8(1)), SHIFTL0(x86_bool_to_bv(VARL("_tmp_cf"), BITS_PER_BYTE * size), U8(size))))); + repeat = SEQ2(repeat, SETL("_dest", ADD(SHIFTR0(VARL("_dest"), U8(1)), SHIFTL0(BOOL_TO_BV(VARL("_tmp_cf"), BITS_PER_BYTE * size), U8(size))))); repeat = SEQ2(repeat, SETL("_tmp_cnt", SUB(VARL("_tmp_cnt"), UN(cnt_size, 1)))); RzILOpBool *if_cond1 = NON_ZERO(VARL("_masked")); @@ -1912,39 +1891,31 @@ IL_LIFTER(ror) { */ IL_LIFTER(ret) { PopHelper ph = x86_pop_helper(analysis->bits / BITS_PER_BYTE /* BYTES */); - RzILOpEffect *ret = ph.eff; - /* We can use RSP, and the correct stack pointer will be resolved depending on bitness */ - ret = SEQ2(ret, x86_il_set_reg(X86_REG_RSP, ph.val)); + + RzILOpEffect *ret = SEQ2(SETL("tgt", ph.val), ph.eff); if (ins->structure->op_count == 1) { - /* Immediate operand (Encondig: I) */ + /* Immediate operand (Encoding: I) + * Reduce RSP by that many bytes. */ ret = SEQ2(ret, x86_il_set_reg(X86_REG_RSP, ADD(x86_il_get_reg(X86_REG_RSP), UN(analysis->bits, ins->structure->operands[0].imm)))); } - return ret; + return SEQ2(ret, JMP(VARL("tgt"))); } -// /** -// * RETF -// * Return far pointer -// * Encoding: ZO, I -// * Rarely found in modern programs -// */ -// IL_LIFTER(retf) { -// /* Unimplemented: Too rare and cumbersome to implement */ -// return EMPTY(); -// } - -// /** -// * RETFQ -// * Return far pointer (size: qword) -// * Encoding: ZO, I -// * Rarely found in modern programs -// */ -// IL_LIFTER(retfq) { -// /* Unimplemented: Too rare and cumbersome to implement */ -// return EMPTY(); -// } +/** + * RETF + * Return far pointer + * Encoding: ZO, I + * Rarely found in modern programs + */ + +/** + * RETFQ + * Return far pointer (size: qword) + * Encoding: ZO, I + * Rarely found in modern programs + */ /** * SAHF @@ -2066,7 +2037,7 @@ IL_LIFTER(sbb) { RzILOpEffect *op2 = SETL("_op2", x86_il_get_op(1)); RzILOpPure *cf = VARG(EFLAGS(CF)); - RzILOpEffect *diff = SETL("_diff", SUB(SUB(VARL("_op1"), VARL("_op2")), x86_bool_to_bv(cf, ins->structure->operands[0].size * BITS_PER_BYTE))); + RzILOpEffect *diff = SETL("_diff", SUB(SUB(VARL("_op1"), VARL("_op2")), BOOL_TO_BV(cf, ins->structure->operands[0].size * BITS_PER_BYTE))); RzILOpEffect *set_dest = x86_il_set_op(0, VARL("_diff")); RzILOpEffect *set_res_flags = x86_il_set_result_flags(VARL("_diff")); RzILOpEffect *set_arith_flags = x86_il_set_arithmetic_flags(VARL("_diff"), VARL("_op1"), VARL("_op2"), false); @@ -2431,7 +2402,7 @@ IL_LIFTER(bound) { RzILOpBool *cond = OR(ULT(VARL("_index"), VARL("_lower")), UGT(VARL("_index"), VARL("_upper"))); /* Interrupt if out of bounds, NOP otherwise */ - return SEQ4(index, lower, upper, BRANCH(cond, SEQ2(GOTO("int"), EMPTY()), NOP())); + return SEQ4(index, lower, upper, BRANCH(cond, GOTO("int"), NOP())); } /** diff --git a/librz/analysis/arch/x86/x86_il.c b/librz/analysis/arch/x86/x86_il.c index a4aa12fc619..75728a86e76 100644 --- a/librz/analysis/arch/x86/x86_il.c +++ b/librz/analysis/arch/x86/x86_il.c @@ -3,6 +3,7 @@ #include "x86_il.h" #include "il_ops.inc" +#include "il_fp_ops.inc" #define COMMON_REGS \ "cs", /* X86_REG_CS */ \ @@ -20,6 +21,22 @@ "of", /* X86_EFLAGS_OF */ \ "nt" /* X86_EFLAGS_NT */ +#define FPU_REGS \ + "cwd", /* X86_REG_FPU_CW */ \ + "swd", /* X86_REG_FPSW */ \ + "ftw", /* X86_REG_FPU_TW */ \ + "fop", /* X86_REG_FPU_OP */ \ + "frip", /* X86_REG_FPU_IP */ \ + "frdp", /* X86_REG_FPU_DP */ \ + "st0", /* X86_REG_ST0 */ \ + "st1", /* X86_REG_ST1 */ \ + "st2", /* X86_REG_ST2 */ \ + "st3", /* X86_REG_ST3 */ \ + "st4", /* X86_REG_ST4 */ \ + "st5", /* X86_REG_ST5 */ \ + "st6", /* X86_REG_ST6 */ \ + "st7" /* X86_REG_ST6 */ + /** * \brief All registers bound to IL variables for x86 16-bit */ @@ -90,10 +107,11 @@ const char *x86_bound_regs_64[] = { "gs", /* X86_REG_GS */ "cr0", /* X86_REG_CR0 */ "dr0", /* X86_REG_DR0 */ + FPU_REGS, NULL }; -typedef RzILOpEffect *(*x86_il_ins)(const X86ILIns *, ut64, RzAnalysis *); +typedef RzILOpEffect *(*x86_il_ins)(const X86ILIns *, ut64, RzAnalysis *, X86ILContext *); /** * \brief RzIL handlers for x86 instructions @@ -146,7 +164,6 @@ x86_il_ins x86_ins[X86_INS_ENDING] = { [X86_INS_INC] = x86_il_inc, [X86_INS_INT] = x86_il_int, [X86_INS_INTO] = x86_il_into, - [X86_INS_IRET] = x86_il_unimpl, [X86_INS_JA] = x86_il_ja, [X86_INS_JAE] = x86_il_jae, [X86_INS_JB] = x86_il_jb, @@ -208,8 +225,6 @@ x86_il_ins x86_ins[X86_INS_ENDING] = { [X86_INS_ROL] = x86_il_rol, [X86_INS_ROR] = x86_il_ror, [X86_INS_RET] = x86_il_ret, - [X86_INS_RETF] = x86_il_unimpl, - [X86_INS_RETFQ] = x86_il_unimpl, [X86_INS_SAHF] = x86_il_sahf, [X86_INS_SAL] = x86_il_sal, [X86_INS_SAR] = x86_il_sar, @@ -236,11 +251,84 @@ x86_il_ins x86_ins[X86_INS_ENDING] = { [X86_INS_XOR] = x86_il_xor, [X86_INS_BOUND] = x86_il_bound, [X86_INS_ENTER] = x86_il_enter, + [X86_INS_LEAVE] = x86_il_leave, + + /* floating-point instructions */ + [X86_INS_FNINIT] = x86_il_fninit, + [X86_INS_FLDCW] = x86_il_fldcw, + [X86_INS_FNSTCW] = x86_il_fnstcw, + [X86_INS_FNSTSW] = x86_il_fnstsw, + [X86_INS_FNCLEX] = x86_il_fnclex, + [X86_INS_FLD] = x86_il_fld, + [X86_INS_FST] = x86_il_fst, + [X86_INS_FSTP] = x86_il_fstp, + [X86_INS_FLD1] = x86_il_fld1, + [X86_INS_FLDZ] = x86_il_fldz, + [X86_INS_FLDL2T] = x86_il_fldl2t, + [X86_INS_FLDL2E] = x86_il_fldl2e, + [X86_INS_FLDPI] = x86_il_fldpi, + [X86_INS_FLDLG2] = x86_il_fldlg2, + [X86_INS_FLDLN2] = x86_il_fldln2, + [X86_INS_FXCH] = x86_il_fxch, + [X86_INS_FILD] = x86_il_fild, + [X86_INS_FIST] = x86_il_fist, + [X86_INS_FISTP] = x86_il_fistp, + [X86_INS_FBLD] = x86_il_fbld, + [X86_INS_FBSTP] = x86_il_fbstp, + [X86_INS_FABS] = x86_il_fabs, + [X86_INS_FADD] = x86_il_fadd, +#if CS_API_MAJOR <= 4 + [X86_INS_FADDP] = x86_il_fadd, +#endif + [X86_INS_FIADD] = x86_il_fiadd, + [X86_INS_FMUL] = x86_il_fmul, + [X86_INS_FMULP] = x86_il_fmulp, + [X86_INS_FIMUL] = x86_il_fimul, + [X86_INS_FSUB] = x86_il_fsub, + [X86_INS_FSUBP] = x86_il_fsubp, + [X86_INS_FISUB] = x86_il_fisub, + [X86_INS_FSUBR] = x86_il_fsubr, + [X86_INS_FSUBRP] = x86_il_fsubrp, + [X86_INS_FISUBR] = x86_il_fisubr, + [X86_INS_FDIV] = x86_il_fdiv, + [X86_INS_FDIVP] = x86_il_fdivp, + [X86_INS_FIDIV] = x86_il_fidiv, + [X86_INS_FDIVR] = x86_il_fdivr, + [X86_INS_FDIVRP] = x86_il_fdivrp, + [X86_INS_FIDIVR] = x86_il_fidivr, + [X86_INS_FCOM] = x86_il_fcom, + [X86_INS_FCOMP] = x86_il_fcomp, + [X86_INS_FICOM] = x86_il_ficom, + [X86_INS_FCOMPP] = x86_il_fcompp, + [X86_INS_FICOMP] = x86_il_ficomp, + [X86_INS_FCOMI] = x86_il_fcomi, + [X86_INS_FCOMPI] = x86_il_fcomip, + /* Using the same FCOM & FCOMI family IL lifters for FUCOM & FUCOMI family instructions + * since we don't support invalid arithmetic operand exceptions (#IA) anyways. */ + [X86_INS_FUCOM] = x86_il_fcom, + [X86_INS_FUCOMP] = x86_il_fcomp, + [X86_INS_FUCOMPP] = x86_il_fcompp, + [X86_INS_FUCOMI] = x86_il_fcomi, + [X86_INS_FUCOMPI] = x86_il_fcomip, + [X86_INS_FCHS] = x86_il_fchs, + [X86_INS_FTST] = x86_il_ftst, + [X86_INS_FRNDINT] = x86_il_frndint, + [X86_INS_FSQRT] = x86_il_fsqrt, + [X86_INS_FNOP] = x86_il_fnop, + [X86_INS_FISTTP] = x86_il_fisttp, + + /* unimplemented instructions */ + [X86_INS_IRET] = x86_il_unimpl, + [X86_INS_RETF] = x86_il_unimpl, + [X86_INS_RETFQ] = x86_il_unimpl, [X86_INS_INSB] = x86_il_unimpl, [X86_INS_INSW] = x86_il_unimpl, [X86_INS_OUTSB] = x86_il_unimpl, [X86_INS_OUTSW] = x86_il_unimpl, - [X86_INS_LEAVE] = x86_il_leave + [X86_INS_FLDENV] = x86_il_unimpl, + [X86_INS_FNSTENV] = x86_il_unimpl, + [X86_INS_FNSAVE] = x86_il_unimpl, + [X86_INS_FRSTOR] = x86_il_unimpl }; void label_int(RzILVM *vm, RzILOpEffect *op); @@ -261,7 +349,15 @@ RZ_IPI bool rz_x86_il_opcode(RZ_NONNULL RzAnalysis *analysis, RZ_NONNULL RzAnaly /* For unimplemented instructions */ lifter = x86_il_unimpl; } - lifted = lifter(ins, pc, analysis); + + X86ILContext ctx = { + .use_rmode = false + }; + + lifted = lifter(ins, pc, analysis, &ctx); + if (ctx.use_rmode) { + lifted = rz_il_op_new_seq(init_rmode(), lifted); + } aop->il_op = lifted; return true; diff --git a/librz/analysis/arch/x86/x86_il.h b/librz/analysis/arch/x86/x86_il.h index 16b1eac243d..3935699f80f 100644 --- a/librz/analysis/arch/x86/x86_il.h +++ b/librz/analysis/arch/x86/x86_il.h @@ -24,6 +24,14 @@ typedef struct x86_il_instruction_t { ut8 ins_size; ///< Size of instruction (in bytes) } X86ILIns; +/** + * \brief To store the context of the IL lifter ; Used to pass around information outside effects + * Other context variables *may* be added in the future when the rest of the instructions are lifted + */ +typedef struct x86_il_context_t { + bool use_rmode; ///< Set to true whenever the rounding mode is calculated (used to add a `SETL` effect for the rounding mode local variable, in case it is used) ; Set to false (by default) +} X86ILContext; + RZ_IPI bool rz_x86_il_opcode(RZ_NONNULL RzAnalysis *analysis, RZ_NONNULL RzAnalysisOp *aop, ut64 pc, RZ_BORROW RZ_NONNULL const X86ILIns *ins); RZ_IPI RzAnalysisILConfig *rz_x86_il_config(RZ_NONNULL RzAnalysis *analysis); diff --git a/librz/analysis/p/analysis_x86_cs.c b/librz/analysis/p/analysis_x86_cs.c index 8d050cc092c..4b764c8519d 100644 --- a/librz/analysis/p/analysis_x86_cs.c +++ b/librz/analysis/p/analysis_x86_cs.c @@ -3596,14 +3596,14 @@ static char *get_reg_profile(RzAnalysis *analysis) { "fpu mxcsr .32 24 0\n" "fpu mxcr_mask .32 28 0\n" - "fpu st0 .64 32 0\n" - "fpu st1 .64 48 0\n" - "fpu st2 .64 64 0\n" - "fpu st3 .64 80 0\n" - "fpu st4 .64 96 0\n" - "fpu st5 .64 112 0\n" - "fpu st6 .64 128 0\n" - "fpu st7 .64 144 0\n" + "fpu st0 .80 32 0\n" + "fpu st1 .80 48 0\n" + "fpu st2 .80 64 0\n" + "fpu st3 .80 80 0\n" + "fpu st4 .80 96 0\n" + "fpu st5 .80 112 0\n" + "fpu st6 .80 128 0\n" + "fpu st7 .80 144 0\n" "xmm@fpu xmm0 .128 160 4\n" "fpu xmm0l .64 160 0\n" diff --git a/test/db/asm/x86_16 b/test/db/asm/x86_16 index 8d3803aeec0..a760196ee11 100644 --- a/test/db/asm/x86_16 +++ b/test/db/asm/x86_16 @@ -5,7 +5,7 @@ ad "aam 0xa" d40a 0x0 (seq (set temp_al (cast 8 false (var ax))) (set ax (| (& ( ad "aam 0x42" d442 0x0 (seq (set temp_al (cast 8 false (var ax))) (set ax (| (& (var ax) (~ (bv 16 0xff00))) (<< (cast 16 false (div (var temp_al) (bv 8 0x42))) (bv 8 0x8) false))) (set adjusted (mod (var temp_al) (bv 8 0x42))) (set ax (| (& (var ax) (~ (bv 16 0xff))) (cast 16 false (var adjusted)))) (set _result (var adjusted)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result)))) ad "aas" 3f 0x0 (seq (branch (|| (! (ule (& (cast 8 false (var ax)) (bv 8 0xf)) (bv 8 0x9))) (var af)) (seq (set ax (- (var ax) (bv 16 0x6))) (set ax (| (& (var ax) (~ (bv 16 0xff00))) (<< (cast 16 false (- (cast 8 false (>> (var ax) (bv 8 0x8) false)) (bv 8 0x1))) (bv 8 0x8) false))) (set af true) (set cf true)) (seq (set af false) (set cf false))) (set ax (| (& (var ax) (~ (bv 16 0xff))) (cast 16 false (& (cast 8 false (var ax)) (bv 8 0xf)))))) adB "cbw" 98 -d "call 0" e8fdff 0x0 (seq (set _cs (cast 16 false (var cs))) (set final (- (var sp) (bv 16 0x2))) (storew 0 (var final) (cast 16 false (var _cs))) (set sp (var final)) (set _pc (bv 16 0x3)) (set final (- (var sp) (bv 16 0x2))) (storew 0 (var final) (cast 16 false (var _pc))) (set sp (var final)) (jmp (bv 16 0x0))) +d "call 0" e8fdff 0x0 (seq (set final (- (var sp) (bv 16 0x2))) (storew 0 (var final) (cast 16 false (bv 16 0x3))) (set sp (var final)) (jmp (bv 16 0x0))) d "enter 8, 0" c8080000 0x0 (seq (set _alloc_sz (cast 16 false (bv 16 0x8))) (set _nest_lvl (mod (cast 8 false (bv 16 0x0)) (bv 8 0x20))) (set final (- (var sp) (bv 16 0x2))) (storew 0 (var final) (cast 16 false (var bp))) (set sp (var final)) (set _frame_tmp (var sp)) (branch (is_zero (var _nest_lvl)) nop (seq (branch (! (ule (var _nest_lvl) (bv 8 0x1))) (seq (set _itr (bv 8 0x1)) (repeat (&& (ule (var _itr) (var _nest_lvl)) (! (== (var _itr) (var _nest_lvl)))) (seq (set bp (- (var bp) (bv 16 0x2))) (set final (- (var sp) (bv 16 0x2))) (storew 0 (var final) (cast 16 false (loadw 0 16 (var bp)))) (set sp (var final)) (set _itr (+ (var _itr) (bv 8 0x1)))))) nop) (set final (- (var sp) (bv 16 0x2))) (storew 0 (var final) (cast 16 false (var _frame_tmp))) (set sp (var final)))) (set sp (- (var sp) (cast 16 false (var _alloc_sz)))) (set bp (cast 16 false (cast 15 false (var _frame_tmp))))) a "jmp 0x0" ebfe 0x0 (jmp (cast 16 false (bv 16 0x0))) a "jmp 0x10" eb0e 0x0 (jmp (cast 16 false (bv 16 0x10))) diff --git a/test/db/asm/x86_32 b/test/db/asm/x86_32 index 0e4d82206a5..c1c26a702ed 100644 --- a/test/db/asm/x86_32 +++ b/test/db/asm/x86_32 @@ -31,7 +31,7 @@ d "and byte [eax], al" 2000 0x0 (seq (set and_ (& (loadw 0 8 (+ (var eax) (bv 32 d "and dword [eax], eax" 2100 0x0 (seq (set and_ (& (loadw 0 32 (+ (var eax) (bv 32 0x0))) (var eax))) (storew 0 (+ (var eax) (bv 32 0x0)) (var and_)) (set of false) (set cf false) (set _result (var and_)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result)))) d "and eax, dword [eax]" 2300 0x0 (seq (set and_ (& (var eax) (loadw 0 32 (+ (var eax) (bv 32 0x0))))) (set eax (var and_)) (set of false) (set cf false) (set _result (var and_)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result)))) d "arpl word [eax], ax" 6300 -d "bound eax, qword [eax]" 6200 0x0 (seq (set _index (var eax)) (set _lower (loadw 0 32 (+ (var eax) (bv 32 0x0)))) (set _upper (loadw 0 32 (+ (var eax) (bv 32 0x8)))) (branch (|| (&& (ule (var _index) (var _lower)) (! (== (var _index) (var _lower)))) (! (ule (var _index) (var _upper)))) (seq (goto int) empty) nop)) +d "bound eax, qword [eax]" 6200 0x0 (seq (set _index (var eax)) (set _lower (loadw 0 32 (+ (var eax) (bv 32 0x0)))) (set _upper (loadw 0 32 (+ (var eax) (bv 32 0x8)))) (branch (|| (&& (ule (var _index) (var _lower)) (! (== (var _index) (var _lower)))) (! (ule (var _index) (var _upper)))) (goto int) nop)) d "bsf eax, dword [eax]" 0fbc00 d "bsr eax, dword [eax]" 0fbd00 d "bswap eax" 0fc8 @@ -145,7 +145,7 @@ d "fxsave [eax]" 0fae00 d "getsec" 0f37 d "haddpd xmm0, xmmword [eax]" 660f7c00 d "haddps xmm0, xmmword [eax]" f20f7c00 -d "hlt" f4 0x0 (seq (goto halt) empty) +d "hlt" f4 0x0 (goto halt) d "hsubpd xmm0, xmmword [eax]" 660f7d00 d "hsubps xmm0, xmmword [eax]" f20f7d00 d "idiv byte [eax]" f638 0x0 (seq (set _src (cast 16 false (loadw 0 8 (+ (var eax) (bv 32 0x0))))) (branch (is_zero (var _src)) nop (seq (set _ax (cast 16 false (var eax))) (set _temp (cast 8 false (sdiv (var _ax) (var _src)))) (branch (|| (! (sle (var _temp) (bv 8 0x7f))) (&& (sle (var _temp) (bv 8 0x80)) (! (== (var _temp) (bv 8 0x80))))) nop (seq (set eax (| (& (var eax) (~ (bv 32 0xff))) (cast 32 false (var _temp)))) (set eax (| (& (var eax) (~ (bv 32 0xff00))) (<< (cast 32 false (smod (var _ax) (var _src))) (bv 8 0x8) false)))))))) @@ -156,11 +156,11 @@ d "imul eax, dword [eax]" 0faf00 0x0 (seq (set _dest (var eax)) (set _tmp_xp (* d "imul eax, dword [eax], 0" 690000000000 0x0 (seq (set _tmp_xp (* (cast 64 (msb (loadw 0 32 (+ (var eax) (bv 32 0x0)))) (loadw 0 32 (+ (var eax) (bv 32 0x0)))) (cast 64 (msb (bv 32 0x0)) (bv 32 0x0)))) (set _dest (cast 32 false (var _tmp_xp))) (set eax (var _dest)) (branch (== (cast 64 (msb (var _dest)) (var _dest)) (var _tmp_xp)) (seq (set cf false) (set of false)) (seq (set cf true) (set of true)))) d "imul eax, dword [eax], 0" 6b0000 0x0 (seq (set _tmp_xp (* (cast 64 (msb (loadw 0 32 (+ (var eax) (bv 32 0x0)))) (loadw 0 32 (+ (var eax) (bv 32 0x0)))) (cast 64 (msb (bv 32 0x0)) (bv 32 0x0)))) (set _dest (cast 32 false (var _tmp_xp))) (set eax (var _dest)) (branch (== (cast 64 (msb (var _dest)) (var _dest)) (var _tmp_xp)) (seq (set cf false) (set of false)) (seq (set cf true) (set of true)))) ad "imul ax" 66f7e8 0x0 (seq (set _tmp_xp (* (cast 32 (msb (cast 16 false (var eax))) (cast 16 false (var eax))) (cast 32 (msb (cast 16 false (var eax))) (cast 16 false (var eax))))) (set eax (| (& (var eax) (~ (bv 32 0xffff))) (cast 32 false (cast 16 false (var _tmp_xp))))) (set edx (| (& (var edx) (~ (bv 32 0xffff))) (cast 32 false (cast 32 false (>> (var _tmp_xp) (bv 8 0x10) false))))) (branch (== (cast 32 (msb (cast 16 false (var _tmp_xp))) (cast 16 false (var _tmp_xp))) (var _tmp_xp)) (seq (set cf false) (set of false)) (seq (set cf true) (set of true)))) -d "in al, 0" e400 0x0 (seq (goto port) empty) -d "in al, dx" ec 0x0 (seq (goto port) empty) -d "in eax, 0" e500 0x0 (seq (goto port) empty) -d "in eax, 0x8c" e58c 0x0 (seq (goto port) empty) -d "in eax, dx" ed 0x0 (seq (goto port) empty) +d "in al, 0" e400 0x0 (goto port) +d "in al, dx" ec 0x0 (goto port) +d "in eax, 0" e500 0x0 (goto port) +d "in eax, 0x8c" e58c 0x0 (goto port) +d "in eax, dx" ed 0x0 (goto port) d "inc byte [eax]" fe00 0x0 (seq (set _op (loadw 0 8 (+ (var eax) (bv 32 0x0)))) (set _result (+ (var _op) (bv 8 0x1))) (storew 0 (+ (var eax) (bv 32 0x0)) (var _result)) (set _result (var _result)) (set _x (var _op)) (set _y (bv 8 0x1)) (set of (|| (&& (&& (! (msb (var _result))) (msb (var _x))) (msb (var _y))) (&& (&& (msb (var _result)) (! (msb (var _x)))) (! (msb (var _y)))))) (set af (|| (|| (&& (msb (cast 4 false (var _x))) (msb (cast 4 false (var _y)))) (&& (! (msb (cast 4 false (var _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result)))) d "inc dword [eax]" ff00 0x0 (seq (set _op (loadw 0 32 (+ (var eax) (bv 32 0x0)))) (set _result (+ (var _op) (bv 32 0x1))) (storew 0 (+ (var eax) (bv 32 0x0)) (var _result)) (set _result (var _result)) (set _x (var _op)) (set _y (bv 32 0x1)) (set of (|| (&& (&& (! (msb (var _result))) (msb (var _x))) (msb (var _y))) (&& (&& (msb (var _result)) (! (msb (var _x)))) (! (msb (var _y)))))) (set af (|| (|| (&& (msb (cast 4 false (var _x))) (msb (cast 4 false (var _y)))) (&& (! (msb (cast 4 false (var _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result)))) d "inc eax" 40 0x0 (seq (set _op (var eax)) (set _result (+ (var _op) (bv 32 0x1))) (set eax (var _result)) (set _result (var _result)) (set _x (var _op)) (set _y (bv 32 0x1)) (set of (|| (&& (&& (! (msb (var _result))) (msb (var _x))) (msb (var _y))) (&& (&& (msb (var _result)) (! (msb (var _x)))) (! (msb (var _y)))))) (set af (|| (|| (&& (msb (cast 4 false (var _x))) (msb (cast 4 false (var _y)))) (&& (! (msb (cast 4 false (var _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result)))) @@ -173,11 +173,11 @@ d "inc esi" 46 0x0 (seq (set _op (var esi)) (set _result (+ (var _op) (bv 32 0x1 d "inc esp" 44 0x0 (seq (set _op (var esp)) (set _result (+ (var _op) (bv 32 0x1))) (set esp (var _result)) (set _result (var _result)) (set _x (var _op)) (set _y (bv 32 0x1)) (set of (|| (&& (&& (! (msb (var _result))) (msb (var _x))) (msb (var _y))) (&& (&& (msb (var _result)) (! (msb (var _x)))) (! (msb (var _y)))))) (set af (|| (|| (&& (msb (cast 4 false (var _x))) (msb (cast 4 false (var _y)))) (&& (! (msb (cast 4 false (var _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result)))) d "insb byte es:[edi], dx" 6c d "insd dword es:[edi], dx" 6d -d "int 1" cd01 0x0 (seq (goto int) empty) -d "int 3" cd03 0x0 (seq (goto int) empty) +d "int 1" cd01 0x0 (goto int) +d "int 3" cd03 0x0 (goto int) d "int1" F1 d "int3" CC -d "into" ce 0x0 (branch (var of) (seq (goto int) empty) nop) +d "into" ce 0x0 (branch (var of) (goto int) nop) d "invd" 0f08 d "invlpg byte [eax]" 0f0138 d "iret" 66cf 0x0 empty @@ -341,11 +341,11 @@ d "or al, 0" 0c00 0x0 (seq (set _or (| (cast 8 false (var eax)) (bv 8 0x0))) (se d "or byte [eax], al" 0800 0x0 (seq (set _or (| (loadw 0 8 (+ (var eax) (bv 32 0x0))) (cast 8 false (var eax)))) (storew 0 (+ (var eax) (bv 32 0x0)) (var _or)) (set of false) (set cf false) (set _result (var _or)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result)))) d "or dword [eax], eax" 0900 0x0 (seq (set _or (| (loadw 0 32 (+ (var eax) (bv 32 0x0))) (var eax))) (storew 0 (+ (var eax) (bv 32 0x0)) (var _or)) (set of false) (set cf false) (set _result (var _or)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result)))) d "or eax, dword [eax]" 0b00 0x0 (seq (set _or (| (var eax) (loadw 0 32 (+ (var eax) (bv 32 0x0))))) (set eax (var _or)) (set of false) (set cf false) (set _result (var _or)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result)))) -d "out 0, al" e600 0x0 (seq (goto port) empty) -d "out 0, eax" e700 0x0 (seq (goto port) empty) -d "out 0x84, eax" e784 0x0 (seq (goto port) empty) -ad "out dx, al" ee 0x0 (seq (goto port) empty) -ad "out dx, eax" ef 0x0 (seq (goto port) empty) +d "out 0, al" e600 0x0 (goto port) +d "out 0, eax" e700 0x0 (goto port) +d "out 0x84, eax" e784 0x0 (goto port) +ad "out dx, al" ee 0x0 (goto port) +ad "out dx, eax" ef 0x0 (goto port) d "outsb dx, byte [esi]" 6e d "outsd dx, dword [esi]" 6f d "paddq xmm0, xmmword [eax]" 660fd400 @@ -430,7 +430,7 @@ d "rdpmc" 0f33 d "rdtsc" 0f31 d "rdtscp" 0f01f9 d "repne movsb byte es:[edi], byte ptr [esi]" f2a4 -d "ret" c3 0x0 (seq (set esp (+ (var esp) (bv 32 0x4))) (set esp (loadw 0 32 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false))))) +d "ret" c3 0x0 (seq (set tgt (loadw 0 32 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)))) (set esp (+ (var esp) (bv 32 0x4))) (jmp (var tgt))) d "retf 0" ca0000 0x0 empty d "retf" cb 0x0 empty d "rol byte [eax], 0" c00000 @@ -1056,11 +1056,11 @@ aB "bt edx, 59" 0fbae23b aB "bt ebp, -20" 0fbae5e0 aB "btr dword [eax], eax" 0fb300 aB "bts dword [eax], eax" 0fab00 -a "call 0x8049100" e8fb900408 0x0 (seq (set _cs (cast 32 false (var cs))) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var _cs))) (set esp (var final)) (set _pc (bv 32 0x5)) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var _pc))) (set esp (var final)) (jmp (bv 32 0x8049100))) -a "call 4" e8ffffffff 0x0 (seq (set _cs (cast 32 false (var cs))) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var _cs))) (set esp (var final)) (set _pc (bv 32 0x5)) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var _pc))) (set esp (var final)) (jmp (bv 32 0x4))) -a "call 5" e800000000 0x0 (seq (set _cs (cast 32 false (var cs))) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var _cs))) (set esp (var final)) (set _pc (bv 32 0x5)) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var _pc))) (set esp (var final)) (jmp (bv 32 0x5))) -a "call dword [eax]" ff10 0x0 (seq (set _cs (cast 32 false (var cs))) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var _cs))) (set esp (var final)) (set _pc (bv 32 0x2)) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var _pc))) (set esp (var final)) (jmp (loadw 0 32 (+ (var eax) (bv 32 0x0))))) -a "call ebx" ffd3 0x0 (seq (set _cs (cast 32 false (var cs))) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var _cs))) (set esp (var final)) (set _pc (bv 32 0x2)) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var _pc))) (set esp (var final)) (jmp (var ebx))) +a "call 0x8049100" e8fb900408 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (bv 32 0x5))) (set esp (var final)) (jmp (bv 32 0x8049100))) +a "call 4" e8ffffffff 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (bv 32 0x5))) (set esp (var final)) (jmp (bv 32 0x4))) +a "call 5" e800000000 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (bv 32 0x5))) (set esp (var final)) (jmp (bv 32 0x5))) +a "call dword [eax]" ff10 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (bv 32 0x2))) (set esp (var final)) (jmp (loadw 0 32 (+ (var eax) (bv 32 0x0))))) +a "call ebx" ffd3 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (bv 32 0x2))) (set esp (var final)) (jmp (var ebx))) a "bnd call ebx" f2ffd3 a "cbw" 6698 a "cdq" 99 @@ -1235,8 +1235,8 @@ a "imul ebx, dword [edx], 0" 6b1a00 0x0 (seq (set _tmp_xp (* (cast 64 (msb (load a "imul ebx, edx, 4" 6bda04 0x0 (seq (set _tmp_xp (* (cast 64 (msb (var edx)) (var edx)) (cast 64 (msb (bv 32 0x4)) (bv 32 0x4)))) (set _dest (cast 32 false (var _tmp_xp))) (set ebx (var _dest)) (branch (== (cast 64 (msb (var _dest)) (var _dest)) (var _tmp_xp)) (seq (set cf false) (set of false)) (seq (set cf true) (set of true)))) a "imul eax, dword [eax]" 0faf00 0x0 (seq (set _dest (var eax)) (set _tmp_xp (* (cast 64 (msb (var _dest)) (var _dest)) (cast 64 (msb (loadw 0 32 (+ (var eax) (bv 32 0x0)))) (loadw 0 32 (+ (var eax) (bv 32 0x0)))))) (set _dest (cast 32 false (var _tmp_xp))) (set eax (var _dest)) (branch (== (cast 64 (msb (var _dest)) (var _dest)) (var _tmp_xp)) (seq (set cf false) (set of false)) (seq (set cf true) (set of true)))) a "imul eax, [eax], 0" 6b0000 0x0 (seq (set _tmp_xp (* (cast 64 (msb (loadw 0 32 (+ (var eax) (bv 32 0x0)))) (loadw 0 32 (+ (var eax) (bv 32 0x0)))) (cast 64 (msb (bv 32 0x0)) (bv 32 0x0)))) (set _dest (cast 32 false (var _tmp_xp))) (set eax (var _dest)) (branch (== (cast 64 (msb (var _dest)) (var _dest)) (var _tmp_xp)) (seq (set cf false) (set of false)) (seq (set cf true) (set of true)))) -a "in al,0" e400 0x0 (seq (goto port) empty) -a "in al,dx" ec 0x0 (seq (goto port) empty) +a "in al,0" e400 0x0 (goto port) +a "in al,dx" ec 0x0 (goto port) a "inc byte [eax]" fe00 0x0 (seq (set _op (loadw 0 8 (+ (var eax) (bv 32 0x0)))) (set _result (+ (var _op) (bv 8 0x1))) (storew 0 (+ (var eax) (bv 32 0x0)) (var _result)) (set _result (var _result)) (set _x (var _op)) (set _y (bv 8 0x1)) (set of (|| (&& (&& (! (msb (var _result))) (msb (var _x))) (msb (var _y))) (&& (&& (msb (var _result)) (! (msb (var _x)))) (! (msb (var _y)))))) (set af (|| (|| (&& (msb (cast 4 false (var _x))) (msb (cast 4 false (var _y)))) (&& (! (msb (cast 4 false (var _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result)))) a "inc dword [eax]" ff00 0x0 (seq (set _op (loadw 0 32 (+ (var eax) (bv 32 0x0)))) (set _result (+ (var _op) (bv 32 0x1))) (storew 0 (+ (var eax) (bv 32 0x0)) (var _result)) (set _result (var _result)) (set _x (var _op)) (set _y (bv 32 0x1)) (set of (|| (&& (&& (! (msb (var _result))) (msb (var _x))) (msb (var _y))) (&& (&& (msb (var _result)) (! (msb (var _x)))) (! (msb (var _y)))))) (set af (|| (|| (&& (msb (cast 4 false (var _x))) (msb (cast 4 false (var _y)))) (&& (! (msb (cast 4 false (var _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result)))) a "inc eax" 40 0x0 (seq (set _op (var eax)) (set _result (+ (var _op) (bv 32 0x1))) (set eax (var _result)) (set _result (var _result)) (set _x (var _op)) (set _y (bv 32 0x1)) (set of (|| (&& (&& (! (msb (var _result))) (msb (var _x))) (msb (var _y))) (&& (&& (msb (var _result)) (! (msb (var _x)))) (! (msb (var _y)))))) (set af (|| (|| (&& (msb (cast 4 false (var _x))) (msb (cast 4 false (var _y)))) (&& (! (msb (cast 4 false (var _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result)))) @@ -1247,17 +1247,17 @@ a "inc edi" 47 0x0 (seq (set _op (var edi)) (set _result (+ (var _op) (bv 32 0x1 a "inc edx" 42 0x0 (seq (set _op (var edx)) (set _result (+ (var _op) (bv 32 0x1))) (set edx (var _result)) (set _result (var _result)) (set _x (var _op)) (set _y (bv 32 0x1)) (set of (|| (&& (&& (! (msb (var _result))) (msb (var _x))) (msb (var _y))) (&& (&& (msb (var _result)) (! (msb (var _x)))) (! (msb (var _y)))))) (set af (|| (|| (&& (msb (cast 4 false (var _x))) (msb (cast 4 false (var _y)))) (&& (! (msb (cast 4 false (var _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result)))) a "inc esi" 46 0x0 (seq (set _op (var esi)) (set _result (+ (var _op) (bv 32 0x1))) (set esi (var _result)) (set _result (var _result)) (set _x (var _op)) (set _y (bv 32 0x1)) (set of (|| (&& (&& (! (msb (var _result))) (msb (var _x))) (msb (var _y))) (&& (&& (msb (var _result)) (! (msb (var _x)))) (! (msb (var _y)))))) (set af (|| (|| (&& (msb (cast 4 false (var _x))) (msb (cast 4 false (var _y)))) (&& (! (msb (cast 4 false (var _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result)))) a "inc esp" 44 0x0 (seq (set _op (var esp)) (set _result (+ (var _op) (bv 32 0x1))) (set esp (var _result)) (set _result (var _result)) (set _x (var _op)) (set _y (bv 32 0x1)) (set of (|| (&& (&& (! (msb (var _result))) (msb (var _x))) (msb (var _y))) (&& (&& (msb (var _result)) (! (msb (var _x)))) (! (msb (var _y)))))) (set af (|| (|| (&& (msb (cast 4 false (var _x))) (msb (cast 4 false (var _y)))) (&& (! (msb (cast 4 false (var _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result)))) -a "in eax, 0" e500 0x0 (seq (goto port) empty) -a "in eax, 0x8c" e58c 0x0 (seq (goto port) empty) -a "in eax, dx" ed 0x0 (seq (goto port) empty) +a "in eax, 0" e500 0x0 (goto port) +a "in eax, 0x8c" e58c 0x0 (goto port) +a "in eax, dx" ed 0x0 (goto port) a "insb byte es:[edi], dx" 6c a "insd dword es:[edi], dx" 6d aB "insertps xmm0, xmm0, 0" 660f3a21c000 -a "int 0x21" cd21 0x0 (seq (goto int) empty) -a "int 1" cd01 0x0 (seq (goto int) empty) +a "int 0x21" cd21 0x0 (goto int) +a "int 1" cd01 0x0 (goto int) a "int1" f1 a "int3" cc -a "int 3" cd03 0x0 (seq (goto int) empty) +a "int 3" cd03 0x0 (goto int) a "into" ce a "invd" 0f08 aB "invlpga" 0f01df @@ -1629,9 +1629,9 @@ a "or dword [eax], eax" 0900 0x0 (seq (set _or (| (loadw 0 32 (+ (var eax) (bv 3 a "or eax, dword [eax]" 0b00 0x0 (seq (set _or (| (var eax) (loadw 0 32 (+ (var eax) (bv 32 0x0))))) (set eax (var _or)) (set of false) (set cf false) (set _result (var _or)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result)))) aB "orpd xmm0, xmmword [eax]" 660f5600 aB "orps xmm0, xmmword [eax]" 0f5600 -a "out 0, al" e600 0x0 (seq (goto port) empty) -a "out 0, eax" e700 0x0 (seq (goto port) empty) -a "out 0x84, eax" e784 0x0 (seq (goto port) empty) +a "out 0, al" e600 0x0 (goto port) +a "out 0, eax" e700 0x0 (goto port) +a "out 0x84, eax" e784 0x0 (goto port) a "outsb dx, byte [esi]" 6e a "outsd dx, dword [esi]" 6f aB "pabsb xmm0, xmm0" 660f381cc0 @@ -1900,12 +1900,12 @@ a "rdtsc" 0f31 a "rdtscp" 0f01f9 a "repne movsb byte es:[edi], byte ptr [esi]" f2a4 a "repz movsb" f3a4 -a "ret" c3 0x0 (seq (set esp (+ (var esp) (bv 32 0x4))) (set esp (loadw 0 32 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false))))) -ad "ret 0xff" c2ff00 0x0 (seq (set esp (+ (var esp) (bv 32 0x4))) (set esp (loadw 0 32 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)))) (set esp (+ (var esp) (bv 32 0xff)))) +a "ret" c3 0x0 (seq (set tgt (loadw 0 32 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)))) (set esp (+ (var esp) (bv 32 0x4))) (jmp (var tgt))) +ad "ret 0xff" c2ff00 0x0 (seq (set tgt (loadw 0 32 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)))) (set esp (+ (var esp) (bv 32 0x4))) (set esp (+ (var esp) (bv 32 0xff))) (jmp (var tgt))) a "bnd ret" f2c3 a "retf 0" ca0000 a "retf" cb 0x0 empty -a "retw" 66c3 0x0 (seq (set esp (+ (var esp) (bv 32 0x4))) (set esp (loadw 0 32 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false))))) +a "retw" 66c3 0x0 (seq (set tgt (loadw 0 32 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)))) (set esp (+ (var esp) (bv 32 0x4))) (jmp (var tgt))) ad "rcl byte [eax], cl" d210 0x0 (seq (set _dest (loadw 0 8 (+ (var eax) (bv 32 0x0)))) (set _tmp_cnt (mod (cast 5 false (cast 8 false (var ecx))) (bv 5 0x9))) (set _cnt_mask (cast 5 false (cast 8 false (var ecx)))) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (msb (var _dest))) (set _dest (+ (<< (var _dest) (bv 8 0x1) false) (ite (var cf) (bv 8 0x1) (bv 8 0x0)))) (set cf (var _tmp_cf)) (set _tmp_cnt (- (var _tmp_cnt) (bv 5 0x1))))) (branch (== (var _cnt_mask) (bv 5 0x1)) (set of (^^ (msb (var _dest)) (var cf))) nop) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) # capstone v5 removes the `, 1` and makes it implicit. ad "rcl byte [eax]" d010 0x0 (seq (set _dest (loadw 0 8 (+ (var eax) (bv 32 0x0)))) (set _tmp_cnt (mod (cast 5 false (bv 8 0x1)) (bv 5 0x9))) (set _cnt_mask (cast 5 false (bv 8 0x1))) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (msb (var _dest))) (set _dest (+ (<< (var _dest) (bv 8 0x1) false) (ite (var cf) (bv 8 0x1) (bv 8 0x0)))) (set cf (var _tmp_cf)) (set _tmp_cnt (- (var _tmp_cnt) (bv 5 0x1))))) (branch (== (var _cnt_mask) (bv 5 0x1)) (set of (^^ (msb (var _dest)) (var cf))) nop) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) @@ -2210,7 +2210,7 @@ aB "xorps xmm0, xmmword [eax]" 0f5700 aB "xrstor [eax]" 0fae28 aB "xsave [eax]" 0fae20 a "xsetbv" 0f01d1 -a "int 0x80" cd80 0x0 (seq (goto int) empty) +a "int 0x80" cd80 0x0 (goto int) a "mov eax, 33" b821000000 0x0 (set eax (bv 32 0x21)) aB "mov rax, 33" 48c7c021000000 0x0 (set eax (bv 32 0x21)) a "mov [ebp+4],0" c7450400000000 0x0 (storew 0 (+ (var ebp) (bv 32 0x4)) (bv 32 0x0)) diff --git a/test/db/asm/x86_64 b/test/db/asm/x86_64 index 2c1256e6af5..1c8c8c68648 100644 --- a/test/db/asm/x86_64 +++ b/test/db/asm/x86_64 @@ -3,7 +3,7 @@ d "lea rax, [rip + 0xff9]" 488d05f90f0000 0x0 (set rax (cast 64 false (+ (bv 64 ad "leave" c9 0x0 (seq (set rsp (var rbp)) (set rsp (+ (var rsp) (bv 64 0x8))) (set rbp (loadw 0 64 (+ (var rsp) (bv 64 0x0))))) d "leave" 66c9 0x0 (seq (set rsp (var rbp)) (set rsp (+ (var rsp) (bv 64 0x4))) (set rbp (cast 64 false (loadw 0 32 (+ (var rsp) (bv 64 0x0)))))) ad "nop" 90 0x0 nop -ad "ret" c3 0x0 (seq (set rsp (+ (var rsp) (bv 64 0x8))) (set rsp (loadw 0 64 (+ (var rsp) (bv 64 0x0))))) +ad "ret" c3 0x0 (seq (set tgt (loadw 0 64 (+ (var rsp) (bv 64 0x0)))) (set rsp (+ (var rsp) (bv 64 0x8))) (jmp (var tgt))) a "add r13, r15" 4d01fd 0x0 (seq (set op1 (var r13)) (set op2 (var r15)) (set sum (+ (var op1) (var op2))) (set r13 (cast 64 false (var sum))) (set _result (var sum)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set _result (var sum)) (set _x (var op1)) (set _y (var op2)) (set cf (|| (|| (&& (msb (var _x)) (msb (var _y))) (&& (! (msb (var _result))) (msb (var _y)))) (&& (msb (var _x)) (! (msb (var _result)))))) (set of (|| (&& (&& (! (msb (var _result))) (msb (var _x))) (msb (var _y))) (&& (&& (msb (var _result)) (! (msb (var _x)))) (! (msb (var _y)))))) (set af (|| (|| (&& (msb (cast 4 false (var _x))) (msb (cast 4 false (var _y)))) (&& (! (msb (cast 4 false (var _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result)))))))) a "add r15, rbx" 4901df 0x0 (seq (set op1 (var r15)) (set op2 (var rbx)) (set sum (+ (var op1) (var op2))) (set r15 (cast 64 false (var sum))) (set _result (var sum)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set _result (var sum)) (set _x (var op1)) (set _y (var op2)) (set cf (|| (|| (&& (msb (var _x)) (msb (var _y))) (&& (! (msb (var _result))) (msb (var _y)))) (&& (msb (var _x)) (! (msb (var _result)))))) (set of (|| (&& (&& (! (msb (var _result))) (msb (var _x))) (msb (var _y))) (&& (&& (msb (var _result)) (! (msb (var _x)))) (! (msb (var _y)))))) (set af (|| (|| (&& (msb (cast 4 false (var _x))) (msb (cast 4 false (var _y)))) (&& (! (msb (cast 4 false (var _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result)))))))) a "add rax, 44" 4883c02c 0x0 (seq (set op1 (var rax)) (set op2 (bv 64 0x2c)) (set sum (+ (var op1) (var op2))) (set rax (var sum)) (set _result (var sum)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set _result (var sum)) (set _x (var op1)) (set _y (var op2)) (set cf (|| (|| (&& (msb (var _x)) (msb (var _y))) (&& (! (msb (var _result))) (msb (var _y)))) (&& (msb (var _x)) (! (msb (var _result)))))) (set of (|| (&& (&& (! (msb (var _result))) (msb (var _x))) (msb (var _y))) (&& (&& (msb (var _result)) (! (msb (var _x)))) (! (msb (var _y)))))) (set af (|| (|| (&& (msb (cast 4 false (var _x))) (msb (cast 4 false (var _y)))) (&& (! (msb (cast 4 false (var _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result)))))))) @@ -1022,11 +1022,11 @@ ad "xchg rdx, r8" 4c87c2 0x0 (seq (set _temp (var rdx)) (set rdx (var r8)) (set ad "xchg r15, rdx" 4987d7 0x0 (seq (set _temp (var r15)) (set r15 (cast 64 false (var rdx))) (set rdx (var _temp))) d "call qword [rip + 0x3a8f3e]" 48ff153e8f3a00 0x0 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (bv 64 0x7))) (set rsp (var final)) (jmp (loadw 0 64 (+ (bv 64 0x7) (bv 64 0x3a8f3e))))) d "call qword [rip + 0x1d638f]" 48ff158f631d00 0x0 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (bv 64 0x7))) (set rsp (var final)) (jmp (loadw 0 64 (+ (bv 64 0x7) (bv 64 0x1d638f))))) -a "fmul st2, st0" dcca -a "fdiv st0, st1" d8f1 -a "fdiv st(0), st(1)" d8f1 -a "fdiv st0, st7" d8f7 -a "fdiv st(0), st(7)" d8f7 +a "fmul st2, st0" dcca 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st2 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (float 2 (var st2) ) (float 2 (var st2) )) (*. rtz (float 2 (var st2) ) (float 2 (var st2) )))))) +a "fdiv st0, st1" d8f1 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st1) )) (fconvert ieee754-bin80 rtz (float 2 (var st1) )))) (/. rtz (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st1) )) (fconvert ieee754-bin80 rtz (float 2 (var st1) )))))))) +a "fdiv st(0), st(1)" d8f1 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st1) )) (fconvert ieee754-bin80 rtz (float 2 (var st1) )))) (/. rtz (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st1) )) (fconvert ieee754-bin80 rtz (float 2 (var st1) )))))))) +a "fdiv st0, st7" d8f7 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st7) )) (fconvert ieee754-bin80 rtz (float 2 (var st7) )))) (/. rtz (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st7) )) (fconvert ieee754-bin80 rtz (float 2 (var st7) )))))))) +a "fdiv st(0), st(7)" d8f7 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st7) )) (fconvert ieee754-bin80 rtz (float 2 (var st7) )))) (/. rtz (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st7) )) (fconvert ieee754-bin80 rtz (float 2 (var st7) )))))))) a "fcmove st0, st1" dac9 a "fcmovbe st0, st1" dad1 a "fcmovu st0, st1" dad9 @@ -1037,87 +1037,95 @@ a "fcmovnu st0, st1" dbd9 a "ffree st0" ddc0 a "ffree st(7)" ddc7 a "frstor [eax]" dd20 -a "fxch" d9c9 -a "fxch st2" d9ca -a "fucom" dde1 -a "fucom st(2)" dde2 -a "fucomp" dde9 -a "fucomp st(2)" ddea -a "faddp" dec1 -a "faddp st2, st0" dec2 -a "fiadd word [rax]" de00 -a "fiadd dword [rax]" da00 -a "fadd dword [rax]" d800 -a "fadd qword [rax]" dc00 -a "ficom word [rax]" de10 -a "ficom dword [rax]" da10 -a "ficomp word [rax]" de18 -a "ficomp dword [rax]" da18 -a "fild word [rax]" df00 -a "fild dword [rax]" db00 -a "fild qword [rax]" df28 -a "fldcw word [rax]" d928 +a "fxch" d9c9 0x0 (seq (set tmp (float 2 (var st0) )) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (var tmp))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +a "fxch st2" d9ca 0x0 (seq (set tmp (float 2 (var st0) )) (set st0 (fbits (float 2 (var st2) ))) (set st2 (fbits (var tmp))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +ad "fld1" d9e8 0x0 (seq (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (float 2 (bv 80 0x3fff8000000000000000) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +ad "fldz" d9ee 0x0 (seq (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (float 2 (bv 80 0x0) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +ad "fldl2t" d9e9 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 3 (| (<< (bv 128 0x3fffd49a784bcd1b) (bv 8 0x8) false) (bv 128 0x8000000000000000)) )) (fconvert ieee754-bin80 rtz (float 3 (| (<< (bv 128 0x3fffd49a784bcd1b) (bv 8 0x8) false) (bv 128 0x8000000000000000)) ))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +ad "fldl2e" d9ea 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 3 (| (<< (bv 128 0x3fffb8aa3b295c17) (bv 8 0x8) false) (bv 128 0xc000000000000000)) )) (fconvert ieee754-bin80 rtz (float 3 (| (<< (bv 128 0x3fffb8aa3b295c17) (bv 8 0x8) false) (bv 128 0xc000000000000000)) ))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +ad "fldpi" d9eb 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 3 (| (<< (bv 128 0x4000c90fdaa22168) (bv 8 0x8) false) (bv 128 0xc000000000000000)) )) (fconvert ieee754-bin80 rtz (float 3 (| (<< (bv 128 0x4000c90fdaa22168) (bv 8 0x8) false) (bv 128 0xc000000000000000)) ))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +ad "fldlg2" d9ec 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 3 (| (<< (bv 128 0x3fff9a209a84fbcf) (bv 8 0x8) false) (bv 128 0xc000000000000000)) )) (fconvert ieee754-bin80 rtz (float 3 (| (<< (bv 128 0x3fff9a209a84fbcf) (bv 8 0x8) false) (bv 128 0xc000000000000000)) ))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +ad "fldln2" d9ed 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 3 (| (<< (bv 128 0x3ffeb17217f7d1cf) (bv 8 0x8) false) (bv 128 0x4000000000000000)) )) (fconvert ieee754-bin80 rtz (float 3 (| (<< (bv 128 0x3ffeb17217f7d1cf) (bv 8 0x8) false) (bv 128 0x4000000000000000)) ))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +a "fucom" dde1 0x0 (seq (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st1) )))) (<. (float 2 (var st0) ) (float 2 (var st1) ))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x8) false) (& (bv 16 0xfeff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0xa) false) (& (bv 16 0xfbff) (var swd)))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st1) )))) (! (|| (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st1) ))) (|| (<. (float 2 (var st0) ) (float 2 (var st1) )) (<. (float 2 (var st1) ) (float 2 (var st0) )))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0xe) false) (& (bv 16 0xbfff) (var swd))))) +a "fucom st(2)" dde2 0x0 (seq (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st2) )))) (<. (float 2 (var st0) ) (float 2 (var st2) ))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x8) false) (& (bv 16 0xfeff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0xa) false) (& (bv 16 0xfbff) (var swd)))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st2) )))) (! (|| (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st2) ))) (|| (<. (float 2 (var st0) ) (float 2 (var st2) )) (<. (float 2 (var st2) ) (float 2 (var st0) )))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0xe) false) (& (bv 16 0xbfff) (var swd))))) +a "fucomp" dde9 0x0 (seq (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st1) )))) (<. (float 2 (var st0) ) (float 2 (var st1) ))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x8) false) (& (bv 16 0xfeff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0xa) false) (& (bv 16 0xfbff) (var swd)))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st1) )))) (! (|| (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st1) ))) (|| (<. (float 2 (var st0) ) (float 2 (var st1) )) (<. (float 2 (var st1) ) (float 2 (var st0) )))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0xe) false) (& (bv 16 0xbfff) (var swd)))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +a "fucomp st(2)" ddea 0x0 (seq (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st2) )))) (<. (float 2 (var st0) ) (float 2 (var st2) ))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x8) false) (& (bv 16 0xfeff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0xa) false) (& (bv 16 0xfbff) (var swd)))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st2) )))) (! (|| (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st2) ))) (|| (<. (float 2 (var st0) ) (float 2 (var st2) )) (<. (float 2 (var st2) ) (float 2 (var st0) )))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0xe) false) (& (bv 16 0xbfff) (var swd)))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +a "faddp" dec1 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (+. rne (float 2 (var st0) ) (float 2 (var st1) )) (+. rtz (float 2 (var st0) ) (float 2 (var st1) ))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +a "faddp st2, st0" dec2 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (+. rne (float 2 (var st0) ) (float 2 (var st1) )) (+. rtz (float 2 (var st0) ) (float 2 (var st1) ))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +a "fiadd word [rax]" de00 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (+. rne (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )) (+. rtz (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )))))) +a "fiadd dword [rax]" da00 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (+. rne (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )) (+. rtz (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )))))) +a "fadd dword [rax]" d800 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (+. rne (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) )) (+. rtz (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) )))))) +a "fadd qword [rax]" dc00 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (+. rne (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) )) (+. rtz (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) )))))) +a "ficom word [rax]" de10 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0)))))))) (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x8) false) (& (bv 16 0xfeff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0xa) false) (& (bv 16 0xfbff) (var swd)))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0)))))))) (! (|| (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))))) (|| (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0)))))) (<. (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0xe) false) (& (bv 16 0xbfff) (var swd))))) +a "ficom dword [rax]" da10 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0)))))))) (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x8) false) (& (bv 16 0xfeff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0xa) false) (& (bv 16 0xfbff) (var swd)))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0)))))))) (! (|| (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))))) (|| (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0)))))) (<. (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0xe) false) (& (bv 16 0xbfff) (var swd))))) +a "ficomp word [rax]" de18 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0)))))))) (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x8) false) (& (bv 16 0xfeff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0xa) false) (& (bv 16 0xfbff) (var swd)))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0)))))))) (! (|| (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))))) (|| (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0)))))) (<. (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0xe) false) (& (bv 16 0xbfff) (var swd)))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +a "ficomp dword [rax]" da18 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0)))))))) (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x8) false) (& (bv 16 0xfeff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0xa) false) (& (bv 16 0xfbff) (var swd)))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0)))))))) (! (|| (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))))) (|| (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0)))))) (<. (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0xe) false) (& (bv 16 0xbfff) (var swd)))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +a "fild word [rax]" df00 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +a "fild dword [rax]" db00 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +a "fild qword [rax]" df28 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 64 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 64 (+ (var rax) (bv 64 0x0))))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +a "fldcw word [rax]" d928 0x0 (set cwd (loadw 0 16 (+ (var rax) (bv 64 0x0)))) a "fldenv [rax]" d920 -a "fbld tbyte [rax]" df20 -a "fbstp tbyte [rax]" df30 +a "fbld tbyte [rax]" df20 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set mem (+ (var rax) (bv 64 0x0))) (set i (bv 64 0x8)) (set val (bv 64 0x0)) (repeat (|| (! (ule (var i) (bv 64 0x0))) (== (var i) (bv 64 0x0))) (seq (set byte (loadw 0 8 (+ (var mem) (var i)))) (set val (+ (* (var val) (bv 64 0x64)) (cast 64 false (+ (* (>> (var byte) (bv 8 0x4) false) (bv 8 0xa)) (& (var byte) (bv 8 0xf)))))) (set i (- (var i) (bv 64 0x1))))) (set f (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var val)) (fcast_sfloat ieee754-bin80 rtz (var val)))) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (is_zero (loadw 0 8 (+ (var mem) (bv 64 0x9)))) (var f) (fneg (var f))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +a "fbstp tbyte [rax]" df30 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set val (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 64 rne (float 2 (var st0) )) (fcast_sint 64 rtz (float 2 (var st0) )))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set sgn (msb (var val))) (set val (ite (var sgn) (~- (var val)) (var val))) (branch (|| (! (sle (var val) (bv 64 0xde0b6b3a7640000))) (== (var val) (bv 64 0xde0b6b3a7640000))) (goto int) (seq (set mem (+ (var rax) (bv 64 0x0))) (set i (bv 64 0x0)) (repeat (&& (ule (var i) (bv 64 0x9)) (! (== (var i) (bv 64 0x9)))) (seq (storew 0 (+ (var mem) (var i)) (cast 8 false (| (<< (div (mod (var val) (bv 64 0x64)) (bv 64 0xa)) (bv 8 0x4) false) (mod (var val) (bv 64 0xa))))) (set val (div (var val) (bv 64 0x64))) (set i (+ (var i) (bv 64 0x1))))) (set mem (+ (var mem) (var i))) (branch (var sgn) (storew 0 (var mem) (bv 8 0xff)) (storew 0 (var mem) (bv 8 0x0)))))) a "fxrstor [rax]" 0fae08 a "fxsave [rax]" 0fae00 -a "fist word [rax]" df10 -a "fist dword [rax]" db10 -a "fistp word [rax]" df18 -a "fistp dword [rax]" db18 -a "fistp qword [rax]" df38 -a "fisttp word [rax]" df08 -a "fisttp dword [rax]" db08 -a "fisttp qword [rax]" dd08 +a "fist word [rax]" df10 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 16 rne (float 2 (var st0) )) (fcast_sint 16 rtz (float 2 (var st0) ))))) +a "fist dword [rax]" db10 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 32 rne (float 2 (var st0) )) (fcast_sint 32 rtz (float 2 (var st0) ))))) +a "fistp word [rax]" df18 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 16 rne (float 2 (var st0) )) (fcast_sint 16 rtz (float 2 (var st0) )))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +a "fistp dword [rax]" db18 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 32 rne (float 2 (var st0) )) (fcast_sint 32 rtz (float 2 (var st0) )))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +a "fistp qword [rax]" df38 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 64 rne (float 2 (var st0) )) (fcast_sint 64 rtz (float 2 (var st0) )))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +a "fisttp word [rax]" df08 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 16 rne (float 2 (var st0) )) (fcast_sint 16 rtz (float 2 (var st0) )))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +a "fisttp dword [rax]" db08 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 32 rne (float 2 (var st0) )) (fcast_sint 32 rtz (float 2 (var st0) )))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +a "fisttp qword [rax]" dd08 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 64 rne (float 2 (var st0) )) (fcast_sint 64 rtz (float 2 (var st0) )))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) a "fstenv [rcx]" 9bd931 a "fnstenv [rcx]" d931 -a "fdiv dword[rax]" d830 -a "fdiv qword [rax]" dc30 -a "fdiv st0, st7" d8f7 -a "fdiv st6, st0" dcfe -a "fdivp" def9 -a "fdivp st2, st0" defa -a "fidiv word [rax]" de30 -a "fidiv dword [rax]" da30 -a "fdivr dword[rax]" d838 -a "fdivr qword [rax]" dc38 -a "fdivr st0, st7" d8ff -a "fdivr st6, st0" dcf6 -a "fdivrp" def1 -a "fdivrp st2, st0" def2 -a "fidivr word [rax]" de38 -a "fidivr dword [rax]" da38 -a "fmul dword[rax]" d808 -a "fmul qword [rax]" dc08 -a "fmul st0, st7" d8cf -a "fmul st6, st0" dcce -a "fmulp" dec9 -a "fmulp st2, st0" deca -a "fimul word [rax]" de08 -a "fimul dword [rax]" da08 -a "fsub dword[rax]" d820 -a "fsub qword [rax]" dc20 -a "fsub st0, st7" d8e7 -a "fsub st6, st0" dcee -a "fsubp" dee9 -a "fsubp st2, st0" deea -a "fisub word [rax]" de20 -a "fisub dword [rax]" da20 -a "fsubr dword[rax]" d828 -a "fsubr qword [rax]" dc28 -a "fsubr st0, st7" d8ef -a "fsubr st6, st0" dce6 -a "fsubrp" dee1 -a "fsubrp st2, st0" dee2 -a "fisubr word [rax]" de28 -a "fisubr dword [rax]" da28 +a "fdiv dword[rax]" d830 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )))) (/. rtz (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )))))))) +a "fdiv qword [rax]" dc30 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )))) (/. rtz (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )))))))) +a "fdiv st0, st7" d8f7 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st7) )) (fconvert ieee754-bin80 rtz (float 2 (var st7) )))) (/. rtz (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st7) )) (fconvert ieee754-bin80 rtz (float 2 (var st7) )))))))) +a "fdiv st6, st0" dcfe 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st6 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st6) ) (float 2 (var st6) )) (/. rtz (float 2 (var st6) ) (float 2 (var st6) )))))) +a "fdivp" def9 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st1) ) (float 2 (var st0) )) (/. rtz (float 2 (var st1) ) (float 2 (var st0) ))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +a "fdivp st2, st0" defa 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st1) ) (float 2 (var st0) )) (/. rtz (float 2 (var st1) ) (float 2 (var st0) ))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +a "fidiv word [rax]" de30 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0)))))) (/. rtz (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0)))))))))) +a "fidiv dword [rax]" da30 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0)))))) (/. rtz (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0)))))))))) +a "fdivr dword[rax]" d838 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) )) (/. rtz (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) )))))) +a "fdivr qword [rax]" dc38 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) )) (/. rtz (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) )))))) +a "fdivr st0, st7" d8ff 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st7) )) (fconvert ieee754-bin80 rtz (float 2 (var st7) ))) (float 2 (var st0) )) (/. rtz (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st7) )) (fconvert ieee754-bin80 rtz (float 2 (var st7) ))) (float 2 (var st0) )))))) +a "fdivr st6, st0" dcf6 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st6 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st6) ) (float 2 (var st6) )) (/. rtz (float 2 (var st6) ) (float 2 (var st6) )))))) +a "fdivrp" def1 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st1) ) (float 2 (var st0) )) (/. rtz (float 2 (var st1) ) (float 2 (var st0) ))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +a "fdivrp st2, st0" def2 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st1) ) (float 2 (var st0) )) (/. rtz (float 2 (var st1) ) (float 2 (var st0) ))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +a "fidivr word [rax]" de38 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )) (/. rtz (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )))))) +a "fidivr dword [rax]" da38 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )) (/. rtz (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )))))) +a "fmul dword[rax]" d808 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) )) (*. rtz (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) )))))) +a "fmul qword [rax]" dc08 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) )) (*. rtz (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) )))))) +a "fmul st0, st7" d8cf 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st7) )) (fconvert ieee754-bin80 rtz (float 2 (var st7) ))) (float 2 (var st0) )) (*. rtz (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st7) )) (fconvert ieee754-bin80 rtz (float 2 (var st7) ))) (float 2 (var st0) )))))) +a "fmul st6, st0" dcce 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st6 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (float 2 (var st6) ) (float 2 (var st6) )) (*. rtz (float 2 (var st6) ) (float 2 (var st6) )))))) +a "fmulp" dec9 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (float 2 (var st0) ) (float 2 (var st1) )) (*. rtz (float 2 (var st0) ) (float 2 (var st1) ))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +a "fmulp st2, st0" deca 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (float 2 (var st0) ) (float 2 (var st1) )) (*. rtz (float 2 (var st0) ) (float 2 (var st1) ))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +a "fimul word [rax]" de08 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )) (*. rtz (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )))))) +a "fimul dword [rax]" da08 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )) (*. rtz (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )))))) +a "fsub dword[rax]" d820 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )))) (-. rtz (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )))))))) +a "fsub qword [rax]" dc20 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )))) (-. rtz (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )))))))) +a "fsub st0, st7" d8e7 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st7) )) (fconvert ieee754-bin80 rtz (float 2 (var st7) )))) (-. rtz (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st7) )) (fconvert ieee754-bin80 rtz (float 2 (var st7) )))))))) +a "fsub st6, st0" dcee 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st6 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (float 2 (var st6) ) (float 2 (var st6) )) (-. rtz (float 2 (var st6) ) (float 2 (var st6) )))))) +a "fsubp" dee9 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (float 2 (var st1) ) (float 2 (var st0) )) (-. rtz (float 2 (var st1) ) (float 2 (var st0) ))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +a "fsubp st2, st0" deea 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (float 2 (var st1) ) (float 2 (var st0) )) (-. rtz (float 2 (var st1) ) (float 2 (var st0) ))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +a "fisub word [rax]" de20 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0)))))) (-. rtz (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0)))))))))) +a "fisub dword [rax]" da20 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0)))))) (-. rtz (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0)))))))))) +a "fsubr dword[rax]" d828 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) )) (-. rtz (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) )))))) +a "fsubr qword [rax]" dc28 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) )) (-. rtz (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) )))))) +a "fsubr st0, st7" d8ef 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st7) )) (fconvert ieee754-bin80 rtz (float 2 (var st7) ))) (float 2 (var st0) )) (-. rtz (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st7) )) (fconvert ieee754-bin80 rtz (float 2 (var st7) ))) (float 2 (var st0) )))))) +a "fsubr st6, st0" dce6 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st6 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (float 2 (var st6) ) (float 2 (var st6) )) (-. rtz (float 2 (var st6) ) (float 2 (var st6) )))))) +a "fsubrp" dee1 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (float 2 (var st0) ) (float 2 (var st1) )) (-. rtz (float 2 (var st0) ) (float 2 (var st1) ))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +a "fsubrp st2, st0" dee2 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (float 2 (var st0) ) (float 2 (var st1) )) (-. rtz (float 2 (var st0) ) (float 2 (var st1) ))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd))))) +a "fisubr word [rax]" de28 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )) (-. rtz (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )))))) +a "fisubr dword [rax]" da28 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )) (-. rtz (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )))))) +# Not testing [fstcw] and [fstsw] since they are made up of a [wait] instruction and a [fnstcw] (or [fnstsw]) instruction, and we already test both of these instructions. a "fstcw word [rcx]" 9bd939 -a "fnstcw word [rcx]" d939 +a "fnstcw word [rcx]" d939 0x0 (storew 0 (+ (var rcx) (bv 64 0x0)) (var cwd)) a "fstsw word [rcx]" 9bdd39 -a "fnstsw word [rcx]" dd39 +a "fnstsw word [rcx]" dd39 0x0 (storew 0 (+ (var rcx) (bv 64 0x0)) (var swd)) a "fstsw ax" 9bdfe0 -a "fnstsw ax" dfe0 +a "fnstsw ax" dfe0 0x0 (set rax (| (& (var rax) (~ (bv 64 0xffff))) (cast 64 false (var swd)))) a "fsave dword [rax]" 9bdd30 a "fnsave dword [rax]" dd30 aB "fnsave dword [rdi + rdi*8]" dd34ff diff --git a/test/db/cmd/cmd_ar b/test/db/cmd/cmd_ar index 188c1d89da3..812266fa05e 100644 --- a/test/db/cmd/cmd_ar +++ b/test/db/cmd/cmd_ar @@ -177,8 +177,8 @@ bp = 0xffff ebp = 0xffffffff rbp = 0xffffffffffffffff dr4 = 0x0000000000000000 -st0 = 0x0000000000000000 cr4 = 0x0000000000000000 +st0 = 0x00000000000000000000 bl = 0xee bx = 0xffee ebx = 0x00c0ffee @@ -191,8 +191,8 @@ r11w = 0x0000 r11d = 0x00000000 r11 = 0x0000000000000000 dr6 = 0x0000000000000000 -st1 = 0x0000000000000000 cr6 = 0x0000000000000000 +st1 = 0x00000000000000000000 r10b = 0x00 r10w = 0x0000 r10d = 0x00000000 @@ -203,7 +203,7 @@ r9b = 0x00 r9w = 0x0000 r9d = 0x00000000 r9 = 0x0000000000000000 -st2 = 0x0000000000000000 +st2 = 0x00000000000000000000 r8b = 0x00 r8w = 0x0000 r8d = 0x00000000 @@ -212,7 +212,7 @@ al = 0x37 ax = 0x1337 eax = 0x00001337 rax = 0x0000000000001337 -st3 = 0x0000000000000000 +st3 = 0x00000000000000000000 ah = 0x13 cl = 0x00 cx = 0x0000 @@ -223,7 +223,7 @@ dl = 0x00 dx = 0x0000 edx = 0x00000000 rdx = 0x0000000000000000 -st4 = 0x0000000000000000 +st4 = 0x00000000000000000000 dh = 0x00 sil = 0x00 si = 0x0000 @@ -233,16 +233,16 @@ dil = 0x00 di = 0x0000 edi = 0x00000000 rdi = 0x0000000000000000 -st5 = 0x0000000000000000 +st5 = 0x00000000000000000000 rip = 0xffffffffffffffff -st6 = 0x0000000000000000 +st6 = 0x00000000000000000000 cs = 0x0000000000000000 cf = 0x0 eflags = 0x00000000 pf = 0x0 rflags = 0x0000000000000000 -st7 = 0x0000000000000000 af = 0x0 +st7 = 0x00000000000000000000 zf = 0x0 sf = 0x0 tf = 0x0 @@ -837,14 +837,14 @@ fpu frip .64 8 0 fpu frdp .64 16 0 fpu mxcsr .32 24 0 fpu mxcr_mask .32 28 0 -fpu st0 .64 32 0 -fpu st1 .64 48 0 -fpu st2 .64 64 0 -fpu st3 .64 80 0 -fpu st4 .64 96 0 -fpu st5 .64 112 0 -fpu st6 .64 128 0 -fpu st7 .64 144 0 +fpu st0 .80 32 0 +fpu st1 .80 48 0 +fpu st2 .80 64 0 +fpu st3 .80 80 0 +fpu st4 .80 96 0 +fpu st5 .80 112 0 +fpu st6 .80 128 0 +fpu st7 .80 144 0 xmm@fpu xmm0 .128 160 4 fpu xmm0l .64 160 0 fpu xmm0h .64 168 0 @@ -871,7 +871,7 @@ fpu xmm7l .64 272 0 fpu xmm7h .64 280 0 fpu x64 .64 288 0 -{"alias_info":[{"role":0,"role_str":"PC","reg":"rip"},{"role":1,"role_str":"SP","reg":"rsp"},{"role":3,"role_str":"BP","reg":"rbp"},{"role":5,"role_str":"A0","reg":"rdi"},{"role":6,"role_str":"A1","reg":"rsi"},{"role":7,"role_str":"A2","reg":"rdx"},{"role":8,"role_str":"A3","reg":"rcx"},{"role":9,"role_str":"A4","reg":"r8"},{"role":10,"role_str":"A5","reg":"r9"},{"role":11,"role_str":"A6","reg":"r10"},{"role":12,"role_str":"A7","reg":"r11"},{"role":23,"role_str":"SN","reg":"rax"}],"reg_info":[{"type":0,"type_str":"gpr","name":"rax","size":64,"offset":640},{"type":0,"type_str":"gpr","name":"eax","size":32,"offset":640},{"type":0,"type_str":"gpr","name":"ax","size":16,"offset":640},{"type":0,"type_str":"gpr","name":"al","size":8,"offset":640},{"type":0,"type_str":"gpr","name":"ah","size":8,"offset":648},{"type":0,"type_str":"gpr","name":"rbx","size":64,"offset":320},{"type":0,"type_str":"gpr","name":"ebx","size":32,"offset":320},{"type":0,"type_str":"gpr","name":"bx","size":16,"offset":320},{"type":0,"type_str":"gpr","name":"bl","size":8,"offset":320},{"type":0,"type_str":"gpr","name":"bh","size":8,"offset":328},{"type":0,"type_str":"gpr","name":"rcx","size":64,"offset":704},{"type":0,"type_str":"gpr","name":"ecx","size":32,"offset":704},{"type":0,"type_str":"gpr","name":"cx","size":16,"offset":704},{"type":0,"type_str":"gpr","name":"cl","size":8,"offset":704},{"type":0,"type_str":"gpr","name":"ch","size":8,"offset":712},{"type":0,"type_str":"gpr","name":"rdx","size":64,"offset":768},{"type":0,"type_str":"gpr","name":"edx","size":32,"offset":768},{"type":0,"type_str":"gpr","name":"dx","size":16,"offset":768},{"type":0,"type_str":"gpr","name":"dl","size":8,"offset":768},{"type":0,"type_str":"gpr","name":"dh","size":8,"offset":776},{"type":0,"type_str":"gpr","name":"rsi","size":64,"offset":832},{"type":0,"type_str":"gpr","name":"esi","size":32,"offset":832},{"type":0,"type_str":"gpr","name":"si","size":16,"offset":832},{"type":0,"type_str":"gpr","name":"sil","size":8,"offset":832},{"type":0,"type_str":"gpr","name":"rdi","size":64,"offset":896},{"type":0,"type_str":"gpr","name":"edi","size":32,"offset":896},{"type":0,"type_str":"gpr","name":"di","size":16,"offset":896},{"type":0,"type_str":"gpr","name":"dil","size":8,"offset":896},{"type":0,"type_str":"gpr","name":"r8","size":64,"offset":576},{"type":0,"type_str":"gpr","name":"r8d","size":32,"offset":576},{"type":0,"type_str":"gpr","name":"r8w","size":16,"offset":576},{"type":0,"type_str":"gpr","name":"r8b","size":8,"offset":576},{"type":0,"type_str":"gpr","name":"r9","size":64,"offset":512},{"type":0,"type_str":"gpr","name":"r9d","size":32,"offset":512},{"type":0,"type_str":"gpr","name":"r9w","size":16,"offset":512},{"type":0,"type_str":"gpr","name":"r9b","size":8,"offset":512},{"type":0,"type_str":"gpr","name":"r10","size":64,"offset":448},{"type":0,"type_str":"gpr","name":"r10d","size":32,"offset":448},{"type":0,"type_str":"gpr","name":"r10w","size":16,"offset":448},{"type":0,"type_str":"gpr","name":"r10b","size":8,"offset":448},{"type":0,"type_str":"gpr","name":"r11","size":64,"offset":384},{"type":0,"type_str":"gpr","name":"r11d","size":32,"offset":384},{"type":0,"type_str":"gpr","name":"r11w","size":16,"offset":384},{"type":0,"type_str":"gpr","name":"r11b","size":8,"offset":384},{"type":0,"type_str":"gpr","name":"r12","size":64,"offset":192},{"type":0,"type_str":"gpr","name":"r12d","size":32,"offset":192},{"type":0,"type_str":"gpr","name":"r12w","size":16,"offset":192},{"type":0,"type_str":"gpr","name":"r12b","size":8,"offset":192},{"type":0,"type_str":"gpr","name":"r13","size":64,"offset":128},{"type":0,"type_str":"gpr","name":"r13d","size":32,"offset":128},{"type":0,"type_str":"gpr","name":"r13w","size":16,"offset":128},{"type":0,"type_str":"gpr","name":"r13b","size":8,"offset":128},{"type":0,"type_str":"gpr","name":"r14","size":64,"offset":64},{"type":0,"type_str":"gpr","name":"r14d","size":32,"offset":64},{"type":0,"type_str":"gpr","name":"r14w","size":16,"offset":64},{"type":0,"type_str":"gpr","name":"r14b","size":8,"offset":64},{"type":0,"type_str":"gpr","name":"r15","size":64,"offset":0},{"type":0,"type_str":"gpr","name":"r15d","size":32,"offset":0},{"type":0,"type_str":"gpr","name":"r15w","size":16,"offset":0},{"type":0,"type_str":"gpr","name":"r15b","size":8,"offset":0},{"type":0,"type_str":"gpr","name":"rip","size":64,"offset":1024},{"type":0,"type_str":"gpr","name":"rbp","size":64,"offset":256},{"type":0,"type_str":"gpr","name":"ebp","size":32,"offset":256},{"type":0,"type_str":"gpr","name":"bp","size":16,"offset":256},{"type":0,"type_str":"gpr","name":"bpl","size":8,"offset":256},{"type":6,"type_str":"flg","name":"rflags","size":64,"offset":1152},{"type":6,"type_str":"flg","name":"eflags","size":32,"offset":1152},{"type":6,"type_str":"flg","name":"cf","size":1,"offset":1152},{"type":6,"type_str":"flg","name":"pf","size":1,"offset":1154},{"type":6,"type_str":"flg","name":"af","size":1,"offset":1156},{"type":6,"type_str":"flg","name":"zf","size":1,"offset":1158},{"type":6,"type_str":"flg","name":"sf","size":1,"offset":1159},{"type":6,"type_str":"flg","name":"tf","size":1,"offset":1160},{"type":6,"type_str":"flg","name":"if","size":1,"offset":1161},{"type":6,"type_str":"flg","name":"df","size":1,"offset":1162},{"type":6,"type_str":"flg","name":"of","size":1,"offset":1163},{"type":6,"type_str":"flg","name":"nt","size":1,"offset":1166},{"type":6,"type_str":"flg","name":"rf","size":1,"offset":1168},{"type":6,"type_str":"flg","name":"vm","size":1,"offset":1169},{"type":6,"type_str":"flg","name":"ac","size":1,"offset":1170},{"type":0,"type_str":"gpr","name":"rsp","size":64,"offset":1216},{"type":0,"type_str":"gpr","name":"esp","size":32,"offset":1216},{"type":0,"type_str":"gpr","name":"sp","size":16,"offset":1216},{"type":0,"type_str":"gpr","name":"spl","size":8,"offset":1216},{"type":1,"type_str":"drx","name":"dr0","size":64,"offset":0},{"type":1,"type_str":"drx","name":"dr1","size":64,"offset":64},{"type":1,"type_str":"drx","name":"dr2","size":64,"offset":128},{"type":1,"type_str":"drx","name":"dr3","size":64,"offset":192},{"type":1,"type_str":"drx","name":"dr4","size":64,"offset":256},{"type":1,"type_str":"drx","name":"dr5","size":64,"offset":320},{"type":1,"type_str":"drx","name":"dr6","size":64,"offset":384},{"type":1,"type_str":"drx","name":"dr7","size":64,"offset":448},{"type":2,"type_str":"fpu","name":"cwd","size":16,"offset":0},{"type":2,"type_str":"fpu","name":"swd","size":16,"offset":16},{"type":2,"type_str":"fpu","name":"ftw","size":16,"offset":32},{"type":2,"type_str":"fpu","name":"fop","size":16,"offset":48},{"type":2,"type_str":"fpu","name":"frip","size":64,"offset":64},{"type":2,"type_str":"fpu","name":"frdp","size":64,"offset":128},{"type":2,"type_str":"fpu","name":"mxcsr","size":32,"offset":192},{"type":2,"type_str":"fpu","name":"mxcr_mask","size":32,"offset":224},{"type":2,"type_str":"fpu","name":"st0","size":64,"offset":256},{"type":2,"type_str":"fpu","name":"st1","size":64,"offset":384},{"type":2,"type_str":"fpu","name":"st2","size":64,"offset":512},{"type":2,"type_str":"fpu","name":"st3","size":64,"offset":640},{"type":2,"type_str":"fpu","name":"st4","size":64,"offset":768},{"type":2,"type_str":"fpu","name":"st5","size":64,"offset":896},{"type":2,"type_str":"fpu","name":"st6","size":64,"offset":1024},{"type":2,"type_str":"fpu","name":"st7","size":64,"offset":1152},{"type":4,"type_str":"xmm","name":"xmm0","size":128,"offset":1280},{"type":2,"type_str":"fpu","name":"xmm0l","size":64,"offset":1280},{"type":2,"type_str":"fpu","name":"xmm0h","size":64,"offset":1344},{"type":4,"type_str":"xmm","name":"xmm1","size":128,"offset":1408},{"type":2,"type_str":"fpu","name":"xmm1l","size":64,"offset":1408},{"type":2,"type_str":"fpu","name":"xmm1h","size":64,"offset":1472},{"type":4,"type_str":"xmm","name":"xmm2","size":128,"offset":1536},{"type":2,"type_str":"fpu","name":"xmm2l","size":64,"offset":1536},{"type":2,"type_str":"fpu","name":"xmm2h","size":64,"offset":1600},{"type":4,"type_str":"xmm","name":"xmm3","size":128,"offset":1664},{"type":2,"type_str":"fpu","name":"xmm3l","size":64,"offset":1664},{"type":2,"type_str":"fpu","name":"xmm3h","size":64,"offset":1728},{"type":4,"type_str":"xmm","name":"xmm4","size":128,"offset":1792},{"type":2,"type_str":"fpu","name":"xmm4l","size":64,"offset":1792},{"type":2,"type_str":"fpu","name":"xmm4h","size":64,"offset":1856},{"type":4,"type_str":"xmm","name":"xmm5","size":128,"offset":1920},{"type":2,"type_str":"fpu","name":"xmm5l","size":64,"offset":1920},{"type":2,"type_str":"fpu","name":"xmm5h","size":64,"offset":1984},{"type":4,"type_str":"xmm","name":"xmm6","size":128,"offset":2048},{"type":2,"type_str":"fpu","name":"xmm6l","size":64,"offset":2048},{"type":2,"type_str":"fpu","name":"xmm6h","size":64,"offset":2112},{"type":4,"type_str":"xmm","name":"xmm7","size":128,"offset":2176},{"type":2,"type_str":"fpu","name":"xmm7l","size":64,"offset":2176},{"type":2,"type_str":"fpu","name":"xmm7h","size":64,"offset":2240},{"type":2,"type_str":"fpu","name":"x64","size":64,"offset":2304},{"type":7,"type_str":"seg","name":"cs","size":64,"offset":1088},{"type":7,"type_str":"seg","name":"ss","size":64,"offset":1280},{"type":7,"type_str":"seg","name":"fs_base","size":64,"offset":1344},{"type":7,"type_str":"seg","name":"gs_base","size":64,"offset":1408},{"type":7,"type_str":"seg","name":"ds","size":64,"offset":1472},{"type":7,"type_str":"seg","name":"es","size":64,"offset":1536},{"type":7,"type_str":"seg","name":"fs","size":64,"offset":1600},{"type":7,"type_str":"seg","name":"gs","size":64,"offset":1664},{"type":12,"type_str":"ctr","name":"cr0","size":64,"offset":0},{"type":12,"type_str":"ctr","name":"cr1","size":64,"offset":64},{"type":12,"type_str":"ctr","name":"cr2","size":64,"offset":128},{"type":12,"type_str":"ctr","name":"cr3","size":64,"offset":192},{"type":12,"type_str":"ctr","name":"cr4","size":64,"offset":256},{"type":12,"type_str":"ctr","name":"cr5","size":64,"offset":320},{"type":12,"type_str":"ctr","name":"cr6","size":64,"offset":384},{"type":12,"type_str":"ctr","name":"cr7","size":64,"offset":448}]} +{"alias_info":[{"role":0,"role_str":"PC","reg":"rip"},{"role":1,"role_str":"SP","reg":"rsp"},{"role":3,"role_str":"BP","reg":"rbp"},{"role":5,"role_str":"A0","reg":"rdi"},{"role":6,"role_str":"A1","reg":"rsi"},{"role":7,"role_str":"A2","reg":"rdx"},{"role":8,"role_str":"A3","reg":"rcx"},{"role":9,"role_str":"A4","reg":"r8"},{"role":10,"role_str":"A5","reg":"r9"},{"role":11,"role_str":"A6","reg":"r10"},{"role":12,"role_str":"A7","reg":"r11"},{"role":23,"role_str":"SN","reg":"rax"}],"reg_info":[{"type":0,"type_str":"gpr","name":"rax","size":64,"offset":640},{"type":0,"type_str":"gpr","name":"eax","size":32,"offset":640},{"type":0,"type_str":"gpr","name":"ax","size":16,"offset":640},{"type":0,"type_str":"gpr","name":"al","size":8,"offset":640},{"type":0,"type_str":"gpr","name":"ah","size":8,"offset":648},{"type":0,"type_str":"gpr","name":"rbx","size":64,"offset":320},{"type":0,"type_str":"gpr","name":"ebx","size":32,"offset":320},{"type":0,"type_str":"gpr","name":"bx","size":16,"offset":320},{"type":0,"type_str":"gpr","name":"bl","size":8,"offset":320},{"type":0,"type_str":"gpr","name":"bh","size":8,"offset":328},{"type":0,"type_str":"gpr","name":"rcx","size":64,"offset":704},{"type":0,"type_str":"gpr","name":"ecx","size":32,"offset":704},{"type":0,"type_str":"gpr","name":"cx","size":16,"offset":704},{"type":0,"type_str":"gpr","name":"cl","size":8,"offset":704},{"type":0,"type_str":"gpr","name":"ch","size":8,"offset":712},{"type":0,"type_str":"gpr","name":"rdx","size":64,"offset":768},{"type":0,"type_str":"gpr","name":"edx","size":32,"offset":768},{"type":0,"type_str":"gpr","name":"dx","size":16,"offset":768},{"type":0,"type_str":"gpr","name":"dl","size":8,"offset":768},{"type":0,"type_str":"gpr","name":"dh","size":8,"offset":776},{"type":0,"type_str":"gpr","name":"rsi","size":64,"offset":832},{"type":0,"type_str":"gpr","name":"esi","size":32,"offset":832},{"type":0,"type_str":"gpr","name":"si","size":16,"offset":832},{"type":0,"type_str":"gpr","name":"sil","size":8,"offset":832},{"type":0,"type_str":"gpr","name":"rdi","size":64,"offset":896},{"type":0,"type_str":"gpr","name":"edi","size":32,"offset":896},{"type":0,"type_str":"gpr","name":"di","size":16,"offset":896},{"type":0,"type_str":"gpr","name":"dil","size":8,"offset":896},{"type":0,"type_str":"gpr","name":"r8","size":64,"offset":576},{"type":0,"type_str":"gpr","name":"r8d","size":32,"offset":576},{"type":0,"type_str":"gpr","name":"r8w","size":16,"offset":576},{"type":0,"type_str":"gpr","name":"r8b","size":8,"offset":576},{"type":0,"type_str":"gpr","name":"r9","size":64,"offset":512},{"type":0,"type_str":"gpr","name":"r9d","size":32,"offset":512},{"type":0,"type_str":"gpr","name":"r9w","size":16,"offset":512},{"type":0,"type_str":"gpr","name":"r9b","size":8,"offset":512},{"type":0,"type_str":"gpr","name":"r10","size":64,"offset":448},{"type":0,"type_str":"gpr","name":"r10d","size":32,"offset":448},{"type":0,"type_str":"gpr","name":"r10w","size":16,"offset":448},{"type":0,"type_str":"gpr","name":"r10b","size":8,"offset":448},{"type":0,"type_str":"gpr","name":"r11","size":64,"offset":384},{"type":0,"type_str":"gpr","name":"r11d","size":32,"offset":384},{"type":0,"type_str":"gpr","name":"r11w","size":16,"offset":384},{"type":0,"type_str":"gpr","name":"r11b","size":8,"offset":384},{"type":0,"type_str":"gpr","name":"r12","size":64,"offset":192},{"type":0,"type_str":"gpr","name":"r12d","size":32,"offset":192},{"type":0,"type_str":"gpr","name":"r12w","size":16,"offset":192},{"type":0,"type_str":"gpr","name":"r12b","size":8,"offset":192},{"type":0,"type_str":"gpr","name":"r13","size":64,"offset":128},{"type":0,"type_str":"gpr","name":"r13d","size":32,"offset":128},{"type":0,"type_str":"gpr","name":"r13w","size":16,"offset":128},{"type":0,"type_str":"gpr","name":"r13b","size":8,"offset":128},{"type":0,"type_str":"gpr","name":"r14","size":64,"offset":64},{"type":0,"type_str":"gpr","name":"r14d","size":32,"offset":64},{"type":0,"type_str":"gpr","name":"r14w","size":16,"offset":64},{"type":0,"type_str":"gpr","name":"r14b","size":8,"offset":64},{"type":0,"type_str":"gpr","name":"r15","size":64,"offset":0},{"type":0,"type_str":"gpr","name":"r15d","size":32,"offset":0},{"type":0,"type_str":"gpr","name":"r15w","size":16,"offset":0},{"type":0,"type_str":"gpr","name":"r15b","size":8,"offset":0},{"type":0,"type_str":"gpr","name":"rip","size":64,"offset":1024},{"type":0,"type_str":"gpr","name":"rbp","size":64,"offset":256},{"type":0,"type_str":"gpr","name":"ebp","size":32,"offset":256},{"type":0,"type_str":"gpr","name":"bp","size":16,"offset":256},{"type":0,"type_str":"gpr","name":"bpl","size":8,"offset":256},{"type":6,"type_str":"flg","name":"rflags","size":64,"offset":1152},{"type":6,"type_str":"flg","name":"eflags","size":32,"offset":1152},{"type":6,"type_str":"flg","name":"cf","size":1,"offset":1152},{"type":6,"type_str":"flg","name":"pf","size":1,"offset":1154},{"type":6,"type_str":"flg","name":"af","size":1,"offset":1156},{"type":6,"type_str":"flg","name":"zf","size":1,"offset":1158},{"type":6,"type_str":"flg","name":"sf","size":1,"offset":1159},{"type":6,"type_str":"flg","name":"tf","size":1,"offset":1160},{"type":6,"type_str":"flg","name":"if","size":1,"offset":1161},{"type":6,"type_str":"flg","name":"df","size":1,"offset":1162},{"type":6,"type_str":"flg","name":"of","size":1,"offset":1163},{"type":6,"type_str":"flg","name":"nt","size":1,"offset":1166},{"type":6,"type_str":"flg","name":"rf","size":1,"offset":1168},{"type":6,"type_str":"flg","name":"vm","size":1,"offset":1169},{"type":6,"type_str":"flg","name":"ac","size":1,"offset":1170},{"type":0,"type_str":"gpr","name":"rsp","size":64,"offset":1216},{"type":0,"type_str":"gpr","name":"esp","size":32,"offset":1216},{"type":0,"type_str":"gpr","name":"sp","size":16,"offset":1216},{"type":0,"type_str":"gpr","name":"spl","size":8,"offset":1216},{"type":1,"type_str":"drx","name":"dr0","size":64,"offset":0},{"type":1,"type_str":"drx","name":"dr1","size":64,"offset":64},{"type":1,"type_str":"drx","name":"dr2","size":64,"offset":128},{"type":1,"type_str":"drx","name":"dr3","size":64,"offset":192},{"type":1,"type_str":"drx","name":"dr4","size":64,"offset":256},{"type":1,"type_str":"drx","name":"dr5","size":64,"offset":320},{"type":1,"type_str":"drx","name":"dr6","size":64,"offset":384},{"type":1,"type_str":"drx","name":"dr7","size":64,"offset":448},{"type":2,"type_str":"fpu","name":"cwd","size":16,"offset":0},{"type":2,"type_str":"fpu","name":"swd","size":16,"offset":16},{"type":2,"type_str":"fpu","name":"ftw","size":16,"offset":32},{"type":2,"type_str":"fpu","name":"fop","size":16,"offset":48},{"type":2,"type_str":"fpu","name":"frip","size":64,"offset":64},{"type":2,"type_str":"fpu","name":"frdp","size":64,"offset":128},{"type":2,"type_str":"fpu","name":"mxcsr","size":32,"offset":192},{"type":2,"type_str":"fpu","name":"mxcr_mask","size":32,"offset":224},{"type":2,"type_str":"fpu","name":"st0","size":80,"offset":256},{"type":2,"type_str":"fpu","name":"st1","size":80,"offset":384},{"type":2,"type_str":"fpu","name":"st2","size":80,"offset":512},{"type":2,"type_str":"fpu","name":"st3","size":80,"offset":640},{"type":2,"type_str":"fpu","name":"st4","size":80,"offset":768},{"type":2,"type_str":"fpu","name":"st5","size":80,"offset":896},{"type":2,"type_str":"fpu","name":"st6","size":80,"offset":1024},{"type":2,"type_str":"fpu","name":"st7","size":80,"offset":1152},{"type":4,"type_str":"xmm","name":"xmm0","size":128,"offset":1280},{"type":2,"type_str":"fpu","name":"xmm0l","size":64,"offset":1280},{"type":2,"type_str":"fpu","name":"xmm0h","size":64,"offset":1344},{"type":4,"type_str":"xmm","name":"xmm1","size":128,"offset":1408},{"type":2,"type_str":"fpu","name":"xmm1l","size":64,"offset":1408},{"type":2,"type_str":"fpu","name":"xmm1h","size":64,"offset":1472},{"type":4,"type_str":"xmm","name":"xmm2","size":128,"offset":1536},{"type":2,"type_str":"fpu","name":"xmm2l","size":64,"offset":1536},{"type":2,"type_str":"fpu","name":"xmm2h","size":64,"offset":1600},{"type":4,"type_str":"xmm","name":"xmm3","size":128,"offset":1664},{"type":2,"type_str":"fpu","name":"xmm3l","size":64,"offset":1664},{"type":2,"type_str":"fpu","name":"xmm3h","size":64,"offset":1728},{"type":4,"type_str":"xmm","name":"xmm4","size":128,"offset":1792},{"type":2,"type_str":"fpu","name":"xmm4l","size":64,"offset":1792},{"type":2,"type_str":"fpu","name":"xmm4h","size":64,"offset":1856},{"type":4,"type_str":"xmm","name":"xmm5","size":128,"offset":1920},{"type":2,"type_str":"fpu","name":"xmm5l","size":64,"offset":1920},{"type":2,"type_str":"fpu","name":"xmm5h","size":64,"offset":1984},{"type":4,"type_str":"xmm","name":"xmm6","size":128,"offset":2048},{"type":2,"type_str":"fpu","name":"xmm6l","size":64,"offset":2048},{"type":2,"type_str":"fpu","name":"xmm6h","size":64,"offset":2112},{"type":4,"type_str":"xmm","name":"xmm7","size":128,"offset":2176},{"type":2,"type_str":"fpu","name":"xmm7l","size":64,"offset":2176},{"type":2,"type_str":"fpu","name":"xmm7h","size":64,"offset":2240},{"type":2,"type_str":"fpu","name":"x64","size":64,"offset":2304},{"type":7,"type_str":"seg","name":"cs","size":64,"offset":1088},{"type":7,"type_str":"seg","name":"ss","size":64,"offset":1280},{"type":7,"type_str":"seg","name":"fs_base","size":64,"offset":1344},{"type":7,"type_str":"seg","name":"gs_base","size":64,"offset":1408},{"type":7,"type_str":"seg","name":"ds","size":64,"offset":1472},{"type":7,"type_str":"seg","name":"es","size":64,"offset":1536},{"type":7,"type_str":"seg","name":"fs","size":64,"offset":1600},{"type":7,"type_str":"seg","name":"gs","size":64,"offset":1664},{"type":12,"type_str":"ctr","name":"cr0","size":64,"offset":0},{"type":12,"type_str":"ctr","name":"cr1","size":64,"offset":64},{"type":12,"type_str":"ctr","name":"cr2","size":64,"offset":128},{"type":12,"type_str":"ctr","name":"cr3","size":64,"offset":192},{"type":12,"type_str":"ctr","name":"cr4","size":64,"offset":256},{"type":12,"type_str":"ctr","name":"cr5","size":64,"offset":320},{"type":12,"type_str":"ctr","name":"cr6","size":64,"offset":384},{"type":12,"type_str":"ctr","name":"cr7","size":64,"offset":448}]} EOF RUN