portugalfuturista/rizin
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Fix EXEC_WITH_RMODE macro and make the IL generated more concise (#4413)

Browse source 
* Use local variables in methods using `EXEC_WITH_RMODE` instead of
      `DUP`ing the values. Do the same for ST register stack popping.
      This leads to lesser code in the IL since the same long expression
      does not get repeated in the IL everytime (since we don't `DUP`
      anymore).
This commit is contained in:
Dhruv Maroo 2024-04-05 06:00:35 +05:30 committed by GitHub
parent de75daca14
commit c6537d917e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 232 additions and 193 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

144
librz/arch/isa/x86/common.c
View file

@ -1134,9 +1134,9 @@ RZ_IPI RzILOpEffect *init_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__)))))
ITE(EQ(VARL("_rmode"), UN(2, 1)), f(RZ_FLOAT_RMODE_RTN, __VA_ARGS__), \
ITE(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);
@ -1152,13 +1152,14 @@ RzILOpFloat *resize_floating_helper(RzFloatRMode rmode, RzFloatFormat format, Rz
* \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;
RZ_IPI ILPureEffectPair x86_il_resize_floating_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *val, RzFloatFormat format, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
ILPureEffectPair ret = { .val = NULL, .eff = NULL };
rz_return_val_if_fail(val && ctx, ret);
ctx->use_rmode = true;
ret.eff = SETL("f_val_rm", val);
ret.val = EXEC_WITH_RMODE(resize_floating_helper, format, VARL("f_val_rm"));
/* 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;
}
@ -1176,12 +1177,14 @@ RzILOpFloat *sint2f_floating_helper(RzFloatRMode rmode, RzFloatFormat format, Rz
* \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);
RZ_IPI ILPureEffectPair x86_il_floating_from_int_ctx(RZ_OWN RZ_NONNULL RzILOpBitVector *int_val, RzFloatFormat format, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
ILPureEffectPair ret = { .val = NULL, .eff = NULL };
rz_return_val_if_fail(int_val && ctx, ret);
ctx->use_rmode = true;
RzILOpFloat *ret = EXEC_WITH_RMODE(sint2f_floating_helper, format, DUP(int_val));
rz_il_op_pure_free(int_val);
ret.eff = SETL("i_val_rm", int_val);
ret.val = EXEC_WITH_RMODE(sint2f_floating_helper, format, VARL("i_val_rm"));
return ret;
}
@ -1199,11 +1202,14 @@ RzILOpFloat *f2sint_floating_helper(RzFloatRMode rmode, ut32 width, RzILOpFloat
* \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);
RZ_IPI ILPureEffectPair x86_il_int_from_floating_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *float_val, ut32 width, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
ILPureEffectPair ret = { .val = NULL, .eff = NULL };
rz_return_val_if_fail(float_val && ctx, ret);
ctx->use_rmode = true;
RzILOpFloat *ret = EXEC_WITH_RMODE(f2sint_floating_helper, width, DUP(float_val));
rz_il_op_pure_free(float_val);
ret.eff = SETL("f_val_rm", float_val);
ret.val = EXEC_WITH_RMODE(f2sint_floating_helper, width, VARL("f_val_rm"));
return ret;
}
@ -1216,13 +1222,13 @@ RZ_IPI RzILOpBitVector *x86_il_int_from_floating_ctx(RZ_OWN RZ_NONNULL RzILOpFlo
* \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_IPI ILPureEffectPair x86_il_fadd_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
ILPureEffectPair ret = { .val = NULL, .eff = NULL };
rz_return_val_if_fail(x && y && ctx, ret);
rz_il_op_pure_free(x);
rz_il_op_pure_free(y);
ctx->use_rmode = true;
ret.eff = SEQ2(SETL("x_rm", x), SETL("y_rm", y));
ret.val = EXEC_WITH_RMODE(FADD, VARL("x_rm"), VARL("y_rm"));
return ret;
}
@ -1236,13 +1242,13 @@ RZ_IPI RzILOpFloat *x86_il_fadd_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x,
* \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_IPI ILPureEffectPair x86_il_fmul_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
ILPureEffectPair ret = { .val = NULL, .eff = NULL };
rz_return_val_if_fail(x && y && ctx, ret);
rz_il_op_pure_free(x);
rz_il_op_pure_free(y);
ctx->use_rmode = true;
ret.eff = SEQ2(SETL("x_rm", x), SETL("y_rm", y));
ret.val = EXEC_WITH_RMODE(FMUL, VARL("x_rm"), VARL("y_rm"));
return ret;
}
@ -1256,14 +1262,14 @@ RZ_IPI RzILOpFloat *x86_il_fmul_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x,
* \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_IPI ILPureEffectPair x86_il_fsub_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
ILPureEffectPair ret = { .val = NULL, .eff = NULL };
rz_return_val_if_fail(x && y && ctx, ret);
rz_il_op_pure_free(x);
rz_il_op_pure_free(y);
ctx->use_rmode = true;
ret.eff = SEQ2(SETL("x_rm", x), SETL("y_rm", y));
// y - x, hence y is the first argument
ret.val = EXEC_WITH_RMODE(FSUB, VARL("y_rm"), VARL("x_rm"));
return ret;
}
@ -1271,8 +1277,9 @@ RZ_IPI RzILOpFloat *x86_il_fsub_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x,
/**
* \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);
RZ_IPI ILPureEffectPair x86_il_fsubr_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
ILPureEffectPair ret = { .val = NULL, .eff = NULL };
rz_return_val_if_fail(x && y && ctx, ret);
return x86_il_fsub_with_rmode(y, x);
}
@ -1285,14 +1292,13 @@ RZ_IPI RzILOpFloat *x86_il_fsubr_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x
* \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_IPI ILPureEffectPair x86_il_fdiv_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
ILPureEffectPair ret = { .val = NULL, .eff = NULL };
rz_return_val_if_fail(x && y && ctx, ret);
rz_il_op_pure_free(x);
rz_il_op_pure_free(y);
ctx->use_rmode = true;
ret.eff = SEQ2(SETL("x_rm", x), SETL("y_rm", y));
ret.val = EXEC_WITH_RMODE(FDIV, VARL("x_rm"), VARL("y_rm"));
return ret;
}
@ -1300,8 +1306,9 @@ RZ_IPI RzILOpFloat *x86_il_fdiv_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x,
/**
* \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);
RZ_IPI ILPureEffectPair x86_il_fdivr_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
ILPureEffectPair ret = { .val = NULL, .eff = NULL };
rz_return_val_if_fail(x && y && ctx, ret);
return x86_il_fdiv_with_rmode(y, x);
}
@ -1313,12 +1320,13 @@ RZ_IPI RzILOpFloat *x86_il_fdivr_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x
* \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_IPI ILPureEffectPair x86_il_fsqrt_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
ILPureEffectPair ret = { .val = NULL, .eff = NULL };
rz_return_val_if_fail(x && ctx, ret);
rz_il_op_pure_free(x);
ctx->use_rmode = true;
ret.eff = SETL("x_rm", x);
ret.val = EXEC_WITH_RMODE(FSQRT, VARL("x_rm"));
return ret;
}
@ -1338,9 +1346,9 @@ RZ_IPI RzILOpEffect *x86_il_set_st_reg_ctx(X86Reg reg, RZ_OWN RZ_NONNULL RzILOpF
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);
ILPureEffectPair converted_val = x86_il_resize_floating(val, RZ_FLOAT_IEEE754_BIN_80);
return SETG(x86_registers[reg], F2BV(converted_val));
return SEQ2(converted_val.eff, SETG(x86_registers[reg], F2BV(converted_val.val)));
}
}
@ -1437,6 +1445,14 @@ RZ_IPI RzILOpEffect *x86_il_st_pop() {
return SEQ3(set_top, st_shift, set_underflow);
}
RZ_IPI ILPureEffectPair x86_il_st_pop_with_val() {
ILPureEffectPair ret;
ret.val = x86_il_get_st_reg(X86_REG_ST0);
ret.eff = x86_il_st_pop();
return ret;
}
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));
@ -1548,8 +1564,24 @@ RZ_IPI RzILOpEffect *x86_il_set_floating_operand_bits_ctx(X86Op op, RZ_OWN RZ_NO
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);
RzILOpPure *resized_val;
RzILOpEffect *ret = NULL;
if (required_format == val_format) {
ILPureEffectPair resized = x86_il_resize_floating(val, required_format);
resized_val = resized.val;
ret = resized.eff;
} else {
resized_val = val;
}
RzILOpEffect *set_bits = x86_il_set_mem_bits(op.mem, F2BV(resized_val), bits, pc);
if (!ret) {
ret = set_bits;
} else {
ret = SEQ2(ret, set_bits);
}
return ret;
}
case X86_OP_IMM:
default:

32
librz/arch/isa/x86/common.h
View file

@ -126,6 +126,11 @@ typedef enum {
X86_FPU_C3 = 14,
} X86FPUFlags;
typedef struct il_pure_effect_pair_t {
RzILOpPure *val;
RzILOpEffect *eff;
} ILPureEffectPair;
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. */
@ -140,15 +145,10 @@ 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();
RZ_IPI ILPureEffectPair x86_il_st_pop_with_val();
#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);
@ -156,17 +156,17 @@ 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 ILPureEffectPair x86_il_resize_floating_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *val, RzFloatFormat format, RZ_BORROW RZ_NONNULL X86ILContext *ctx);
RZ_IPI ILPureEffectPair x86_il_floating_from_int_ctx(RZ_OWN RZ_NONNULL RzILOpBitVector *int_val, RzFloatFormat format, RZ_BORROW RZ_NONNULL X86ILContext *ctx);
RZ_IPI ILPureEffectPair 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);
RZ_IPI ILPureEffectPair 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 ILPureEffectPair 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 ILPureEffectPair 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 ILPureEffectPair 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 ILPureEffectPair 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 ILPureEffectPair 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 ILPureEffectPair 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)

103
librz/arch/isa/x86/il_fp_ops.inc
View file

@ -94,11 +94,8 @@ IL_LIFTER(fst) {
* 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);
ILPureEffectPair pop = x86_il_st_pop_with_val();
return SEQ2(x86_il_set_floating_op(0, pop.val, RZ_FLOAT_IEEE754_BIN_80), pop.eff);
}
/**
@ -139,7 +136,7 @@ IL_LIFTER(fldz) {
#define FPU_LG2 0x3fff9a209a84fbcfULL, 0xf7988f8959ac200dULL
#define FPU_LN2 0x3ffeb17217f7d1cfULL, 0x79abc9e3b39828efULL
RzILOpFloat *math_const_to_float_ctx(uint64_t upper, uint64_t lower, X86ILContext *ctx) {
ILPureEffectPair 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));
@ -158,7 +155,8 @@ RzILOpFloat *math_const_to_float_ctx(uint64_t upper, uint64_t lower, X86ILContex
* Load log2(10)
*/
IL_LIFTER(fldl2t) {
return x86_il_st_push(math_const_to_float(FPU_L2T), RZ_FLOAT_IEEE754_BIN_80);
ILPureEffectPair math_const = math_const_to_float(FPU_L2T);
return SEQ2(math_const.eff, x86_il_st_push(math_const.val, RZ_FLOAT_IEEE754_BIN_80));
}
/**
@ -166,7 +164,8 @@ IL_LIFTER(fldl2t) {
* Load log2(e)
*/
IL_LIFTER(fldl2e) {
return x86_il_st_push(math_const_to_float(FPU_L2E), RZ_FLOAT_IEEE754_BIN_80);
ILPureEffectPair math_const = math_const_to_float(FPU_L2E);
return SEQ2(math_const.eff, x86_il_st_push(math_const.val, RZ_FLOAT_IEEE754_BIN_80));
}
/**
@ -174,7 +173,8 @@ IL_LIFTER(fldl2e) {
* Load pi
*/
IL_LIFTER(fldpi) {
return x86_il_st_push(math_const_to_float(FPU_PI), RZ_FLOAT_IEEE754_BIN_80);
ILPureEffectPair math_const = math_const_to_float(FPU_PI);
return SEQ2(math_const.eff, x86_il_st_push(math_const.val, RZ_FLOAT_IEEE754_BIN_80));
}
/**
@ -182,7 +182,8 @@ IL_LIFTER(fldpi) {
* Load log10(2)
*/
IL_LIFTER(fldlg2) {
return x86_il_st_push(math_const_to_float(FPU_LG2), RZ_FLOAT_IEEE754_BIN_80);
ILPureEffectPair math_const = math_const_to_float(FPU_LG2);
return SEQ2(math_const.eff, x86_il_st_push(math_const.val, RZ_FLOAT_IEEE754_BIN_80));
}
/**
@ -190,7 +191,8 @@ IL_LIFTER(fldlg2) {
* Load ln(2)
*/
IL_LIFTER(fldln2) {
return x86_il_st_push(math_const_to_float(FPU_LN2), RZ_FLOAT_IEEE754_BIN_80);
ILPureEffectPair math_const = math_const_to_float(FPU_LN2);
return SEQ2(math_const.eff, x86_il_st_push(math_const.val, RZ_FLOAT_IEEE754_BIN_80));
}
/**
@ -223,9 +225,9 @@ IL_LIFTER(fxch) {
*/
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);
ILPureEffectPair 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);
return SEQ2(float_val.eff, x86_il_st_push(float_val.val, RZ_FLOAT_IEEE754_BIN_80));
}
/**
@ -233,8 +235,8 @@ IL_LIFTER(fild) {
* 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);
ILPureEffectPair int_val = x86_il_int_from_floating(x86_il_get_st_reg(X86_REG_ST0), ins->structure->operands[0].size * BITS_PER_BYTE);
return SEQ2(int_val.eff, x86_il_set_op(0, int_val.val));
}
/**
@ -242,12 +244,9 @@ IL_LIFTER(fist) {
* 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);
ILPureEffectPair pop = x86_il_st_pop_with_val();
ILPureEffectPair int_val = x86_il_int_from_floating(pop.val, ins->structure->operands[0].size * BITS_PER_BYTE);
return SEQ3(int_val.eff, x86_il_set_op(0, int_val.val), pop.eff);
}
/**
@ -279,7 +278,8 @@ IL_LIFTER(fbld) {
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));
ILPureEffectPair fval = x86_il_floating_from_int(VARL("val"), RZ_FLOAT_IEEE754_BIN_80);
RzILOpEffect *f_init = SEQ2(fval.eff, SETL("f", fval.val));
/* Check sign byte (index 9) checking if sign byte is zero */
RzILOpPure *sign_byte = LOADW(8, ADD(VARL("mem"), UN(mem_size, 9)));
@ -300,11 +300,10 @@ IL_LIFTER(fbld) {
IL_LIFTER(fbstp) {
ut8 mem_size = analysis->bits;
RzILOpEffect *pop_eff;
RzILOpPure *pop_val;
X86_IL_ST_POP(pop_val, pop_eff);
ILPureEffectPair pop = x86_il_st_pop_with_val();
RzILOpEffect *val_init = SETL("val", x86_il_int_from_floating(pop_val, 64));
ILPureEffectPair val = x86_il_int_from_floating(pop.val, 64);
RzILOpEffect *val_init = SEQ2(val.eff, SETL("val", val.val));
RzILOpEffect *sgn_init = SETL("sgn", MSB(VARL("val")));
RzILOpEffect *val_abs = SETL("val", ITE(VARL("sgn"), NEG(VARL("val")), VARL("val")));
@ -338,7 +337,7 @@ IL_LIFTER(fbstp) {
noexcept_case);
return SEQ5(
val_init, pop_eff, // get val from ST(0) and pop
val_init, pop.eff, // get val from ST(0) and pop
sgn_init, val_abs, // val = |val| and store sign
maybe_except);
}
@ -358,6 +357,7 @@ IL_LIFTER(fabs) {
do { \
RzILOpFloat *src; \
X86Reg dest_reg; \
RzILOpEffect *src_eff = NULL; \
\
/* TODO: Check whether all the enumerated cases here are correct, through \
* code coverage. */ \
@ -365,7 +365,9 @@ IL_LIFTER(fabs) {
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); \
ILPureEffectPair resized = x86_il_resize_floating(x86_il_get_floating_op(0), RZ_FLOAT_IEEE754_BIN_80); \
src = resized.val; \
src_eff = resized.eff; \
break; \
case 2: \
/* ST(i) operand, so no need for resizing */ \
@ -377,8 +379,13 @@ IL_LIFTER(fabs) {
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); \
ILPureEffectPair result = x86_il_##op##_with_rmode(src, x86_il_get_st_reg(dest_reg)); \
RzILOpEffect *ret = SEQ2(result.eff, x86_il_set_st_reg(dest_reg, result.val, RZ_FLOAT_IEEE754_BIN_80)); \
\
if (src_eff) { \
ret = SEQ2(src_eff, ret); \
} \
return ret; \
} while (0)
#define FLOATING_ARITHMETIC_POP_IL(op) \
@ -390,15 +397,15 @@ IL_LIFTER(fabs) {
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()); \
ILPureEffectPair result = x86_il_##op##_with_rmode(x86_il_get_st_reg(X86_REG_ST0), x86_il_get_st_reg(dest_reg)); \
return SEQ3(result.eff, x86_il_set_st_reg(dest_reg, result.val, 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); \
ILPureEffectPair float_val = x86_il_floating_from_int(x86_il_get_op(0), RZ_FLOAT_IEEE754_BIN_80); \
ILPureEffectPair result = x86_il_##op##_with_rmode(float_val.val, x86_il_get_st_reg(X86_REG_ST0)); \
return SEQ3(float_val.eff, result.eff, x86_il_set_st_reg(X86_REG_ST0, result.val, RZ_FLOAT_IEEE754_BIN_80)); \
} while (0)
/**
@ -587,7 +594,8 @@ IL_LIFTER(fcomp) {
* 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));
ILPureEffectPair float_val = x86_il_floating_from_int(x86_il_get_op(0), RZ_FLOAT_IEEE754_BIN_80);
return SEQ2(float_val.eff, fcom_helper(ins, pc, analysis, float_val.val));
}
/**
@ -604,7 +612,8 @@ IL_LIFTER(fcompp) {
* 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());
ILPureEffectPair float_val = x86_il_floating_from_int(x86_il_get_op(0), RZ_FLOAT_IEEE754_BIN_80);
return SEQ2(float_val.eff, SEQ2(fcom_helper(ins, pc, analysis, float_val.val), x86_il_st_pop()));
}
RzILOpEffect *fcomi_helper(const X86ILIns *ins, ut64 pc, RzAnalysis *analysis) {
@ -661,10 +670,11 @@ IL_LIFTER(ftst) {
* 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);
ILPureEffectPair int_from_float = x86_il_int_from_floating(x86_il_get_st_reg(X86_REG_ST0), 64);
ILPureEffectPair float_from_int = x86_il_floating_from_int(int_from_float.val, RZ_FLOAT_IEEE754_BIN_80);
/* Not very sure about whether the rounded integer should be limited to 64 bits or not. */
return SEQ3(int_from_float.eff, float_from_int.eff, x86_il_set_st_reg(X86_REG_ST0, float_from_int.val, RZ_FLOAT_IEEE754_BIN_80));
}
/**
@ -672,7 +682,8 @@ IL_LIFTER(frndint) {
* 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);
ILPureEffectPair fsqrt_res = x86_il_fsqrt_with_rmode(x86_il_get_st_reg(X86_REG_ST0));
return SEQ2(fsqrt_res.eff, x86_il_set_st_reg(X86_REG_ST0, fsqrt_res.val, RZ_FLOAT_IEEE754_BIN_80));
}
/**
@ -688,12 +699,8 @@ IL_LIFTER(fnop) {
* 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());
ILPureEffectPair int_from_float = x86_il_int_from_floating(x86_il_get_st_reg(X86_REG_ST0), ins->structure->operands[0].size * BITS_PER_BYTE);
return SEQ3(int_from_float.eff, x86_il_set_op(0, int_from_float.val), x86_il_st_pop());
}
#include <rz_il/rz_il_opbuilder_end.h>

146
test/db/asm/x86_64
View file

@ -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 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 "fmul st2, st0" dcca 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st2) )) (set y_rm (float 2 (var st2) )) (set st2 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (*. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (*. rtp (var x_rm) (var y_rm)) (*. rtz (var x_rm) (var y_rm))))))))
a "fdiv st0, st1" d8f1 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st1) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
a "fdiv st(0), st(1)" d8f1 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st1) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
a "fdiv st0, st7" d8f7 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st7) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
a "fdiv st(0), st(7)" d8f7 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st7) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
a "fcmove st0, st1" dac9
a "fcmovbe st0, st1" dad1
a "fcmovu st0, st1" dad9
@ -1041,84 +1041,84 @@ a "fxch" d9c9 0x0 (seq (set tmp (float 2 (var st0) )) (set st0 (fbits (float 2 (
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)))))
ad "fldl2t" d9e9 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 3 (| (<< (bv 128 0x3fffd49a784bcd1b) (bv 8 0x8) false) (bv 128 0x8000000000000000)) )) (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 (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm))))))) (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 f_val_rm (float 3 (| (<< (bv 128 0x3fffb8aa3b295c17) (bv 8 0x8) false) (bv 128 0xc000000000000000)) )) (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 (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm))))))) (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 f_val_rm (float 3 (| (<< (bv 128 0x4000c90fdaa22168) (bv 8 0x8) false) (bv 128 0xc000000000000000)) )) (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 (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm))))))) (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 f_val_rm (float 3 (| (<< (bv 128 0x3fff9a209a84fbcf) (bv 8 0x8) false) (bv 128 0xc000000000000000)) )) (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 (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm))))))) (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 f_val_rm (float 3 (| (<< (bv 128 0x3ffeb17217f7d1cf) (bv 8 0x8) false) (bv 128 0x4000000000000000)) )) (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 (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm))))))) (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) ))) (|| (<. (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) ))) (|| (<. (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) ))) (|| (<. (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) ))) (|| (<. (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))))))) (|| (<. (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))))))) (|| (<. (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))))))) (|| (<. (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))))))) (|| (<. (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 "faddp" dec1 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st0) )) (set y_rm (float 2 (var st1) )) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (+. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (+. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (+. rtp (var x_rm) (var y_rm)) (+. rtz (var x_rm) (var y_rm))))))) (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 x_rm (float 2 (var st0) )) (set y_rm (float 2 (var st1) )) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (+. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (+. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (+. rtp (var x_rm) (var y_rm)) (+. rtz (var x_rm) (var y_rm))))))) (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 i_val_rm (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (+. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (+. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (+. rtp (var x_rm) (var y_rm)) (+. rtz (var x_rm) (var y_rm))))))))
a "fiadd dword [rax]" da00 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set i_val_rm (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (+. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (+. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (+. rtp (var x_rm) (var y_rm)) (+. rtz (var x_rm) (var y_rm))))))))
a "fadd dword [rax]" d800 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (+. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (+. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (+. rtp (var x_rm) (var y_rm)) (+. rtz (var x_rm) (var y_rm))))))))
a "fadd qword [rax]" dc00 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (+. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (+. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (+. rtp (var x_rm) (var y_rm)) (+. rtz (var x_rm) (var y_rm))))))))
a "ficom word [rax]" de10 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set i_val_rm (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))))) (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))))) (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 (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))))) (|| (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (<. (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))) (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 i_val_rm (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))))) (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))))) (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 (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))))) (|| (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (<. (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))) (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 i_val_rm (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))))) (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))))) (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 (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))))) (|| (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (<. (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))) (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 i_val_rm (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))))) (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))))) (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 (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))))) (|| (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (<. (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))) (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 i_val_rm (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (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 (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))))) (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 i_val_rm (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (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 (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))))) (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 i_val_rm (loadw 0 64 (+ (var rax) (bv 64 0x0)))) (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 (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))))) (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 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 "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 i_val_rm (var val)) (set f (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (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 f_val_rm (float 2 (var st0) )) (set val (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 64 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sint 64 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sint 64 rtp (var f_val_rm)) (fcast_sint 64 rtz (var f_val_rm)))))) (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 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 "fist word [rax]" df10 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st0) )) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 16 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sint 16 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sint 16 rtp (var f_val_rm)) (fcast_sint 16 rtz (var f_val_rm)))))))
a "fist dword [rax]" db10 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st0) )) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 32 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sint 32 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sint 32 rtp (var f_val_rm)) (fcast_sint 32 rtz (var f_val_rm)))))))
a "fistp word [rax]" df18 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st0) )) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 16 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sint 16 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sint 16 rtp (var f_val_rm)) (fcast_sint 16 rtz (var f_val_rm)))))) (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))) (set f_val_rm (float 2 (var st0) )) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 32 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sint 32 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sint 32 rtp (var f_val_rm)) (fcast_sint 32 rtz (var f_val_rm)))))) (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))) (set f_val_rm (float 2 (var st0) )) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 64 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sint 64 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sint 64 rtp (var f_val_rm)) (fcast_sint 64 rtz (var f_val_rm)))))) (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))) (set f_val_rm (float 2 (var st0) )) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 16 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sint 16 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sint 16 rtp (var f_val_rm)) (fcast_sint 16 rtz (var f_val_rm)))))) (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))) (set f_val_rm (float 2 (var st0) )) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 32 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sint 32 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sint 32 rtp (var f_val_rm)) (fcast_sint 32 rtz (var f_val_rm)))))) (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))) (set f_val_rm (float 2 (var st0) )) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 64 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sint 64 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sint 64 rtp (var f_val_rm)) (fcast_sint 64 rtz (var f_val_rm)))))) (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 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) ))))))
a "fdiv dword[rax]" d830 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
a "fdiv qword [rax]" dc30 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
a "fdiv st0, st7" d8f7 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st7) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
a "fdiv st6, st0" dcfe 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st6) )) (set y_rm (float 2 (var st6) )) (set st6 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
a "fdivp" def9 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st0) )) (set y_rm (float 2 (var st1) )) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))) (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 x_rm (float 2 (var st0) )) (set y_rm (float 2 (var st1) )) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))) (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 i_val_rm (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
a "fidiv dword [rax]" da30 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set i_val_rm (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
a "fdivr dword[rax]" d838 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (set x_rm (float 2 (var st0) )) (set y_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
a "fdivr qword [rax]" dc38 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (set x_rm (float 2 (var st0) )) (set y_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
a "fdivr st0, st7" d8ff 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st7) )) (set x_rm (float 2 (var st0) )) (set y_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
a "fdivr st6, st0" dcf6 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st6) )) (set y_rm (float 2 (var st6) )) (set st6 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
a "fdivrp" def1 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st0) )) (set y_rm (float 2 (var st1) )) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))) (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 x_rm (float 2 (var st0) )) (set y_rm (float 2 (var st1) )) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))) (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 i_val_rm (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (set x_rm (float 2 (var st0) )) (set y_rm (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
a "fidivr dword [rax]" da38 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set i_val_rm (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (set x_rm (float 2 (var st0) )) (set y_rm (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
a "fmul dword[rax]" d808 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (*. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (*. rtp (var x_rm) (var y_rm)) (*. rtz (var x_rm) (var y_rm))))))))
a "fmul qword [rax]" dc08 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (*. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (*. rtp (var x_rm) (var y_rm)) (*. rtz (var x_rm) (var y_rm))))))))
a "fmul st0, st7" d8cf 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st7) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (*. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (*. rtp (var x_rm) (var y_rm)) (*. rtz (var x_rm) (var y_rm))))))))
a "fmul st6, st0" dcce 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st6) )) (set y_rm (float 2 (var st6) )) (set st6 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (*. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (*. rtp (var x_rm) (var y_rm)) (*. rtz (var x_rm) (var y_rm))))))))
a "fmulp" dec9 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st0) )) (set y_rm (float 2 (var st1) )) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (*. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (*. rtp (var x_rm) (var y_rm)) (*. rtz (var x_rm) (var y_rm))))))) (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 x_rm (float 2 (var st0) )) (set y_rm (float 2 (var st1) )) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (*. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (*. rtp (var x_rm) (var y_rm)) (*. rtz (var x_rm) (var y_rm))))))) (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 i_val_rm (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (*. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (*. rtp (var x_rm) (var y_rm)) (*. rtz (var x_rm) (var y_rm))))))))
a "fimul dword [rax]" da08 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set i_val_rm (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (*. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (*. rtp (var x_rm) (var y_rm)) (*. rtz (var x_rm) (var y_rm))))))))
a "fsub dword[rax]" d820 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))))
a "fsub qword [rax]" dc20 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))))
a "fsub st0, st7" d8e7 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st7) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))))
a "fsub st6, st0" dcee 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st6) )) (set y_rm (float 2 (var st6) )) (set st6 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))))
a "fsubp" dee9 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st0) )) (set y_rm (float 2 (var st1) )) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))) (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 x_rm (float 2 (var st0) )) (set y_rm (float 2 (var st1) )) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))) (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 i_val_rm (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))))
a "fisub dword [rax]" da20 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set i_val_rm (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))))
a "fsubr dword[rax]" d828 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (set x_rm (float 2 (var st0) )) (set y_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))))
a "fsubr qword [rax]" dc28 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (set x_rm (float 2 (var st0) )) (set y_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))))
a "fsubr st0, st7" d8ef 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st7) )) (set x_rm (float 2 (var st0) )) (set y_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))))
a "fsubr st6, st0" dce6 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st6) )) (set y_rm (float 2 (var st6) )) (set st6 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))))
a "fsubrp" dee1 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st1) )) (set y_rm (float 2 (var st0) )) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))) (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 x_rm (float 2 (var st1) )) (set y_rm (float 2 (var st0) )) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))) (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 i_val_rm (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (set x_rm (float 2 (var st0) )) (set y_rm (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))))
a "fisubr dword [rax]" da28 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set i_val_rm (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (set x_rm (float 2 (var st0) )) (set y_rm (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))))
# 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 0x0 (storew 0 (+ (var rcx) (bv 64 0x0)) (var cwd))