RzIL: replace float comparison macros with functions (#4400)
* Replace float comparison macros with functions * Move to float operations into il_routines.c * Add RZ_OWN/RZ_BORROW tags
This commit is contained in:
pelijah
GitHub
parent
5cd4cff7eb
commit
3d93397dd8
6 changed files with 73 additions and 17 deletions
|
|
@ -244,3 +244,53 @@ RZ_API RZ_OWN RzILOpBool *rz_il_op_new_ne(RZ_NONNULL RzILOpPure *x, RZ_NONNULL R
|
|||
}
|
||||
return rz_il_op_new_bool_inv(result);
|
||||
}
|
||||
|
||||
static inline RZ_OWN RzILOpBool *_any_fl_is_nan(RZ_NONNULL RZ_OWN RzILOpFloat *x, RZ_NONNULL RZ_OWN RzILOpFloat *y) {
|
||||
return rz_il_op_new_bool_or(rz_il_op_new_is_nan(x), rz_il_op_new_is_nan(y));
|
||||
}
|
||||
|
||||
static inline RZ_OWN RzILOpBool *_fl_is_less(RZ_NONNULL RZ_BORROW RzILOpFloat *x, RZ_NONNULL RZ_BORROW RzILOpFloat *y) {
|
||||
RzILOpFloat *x_dup = rz_il_op_pure_dup(x);
|
||||
RzILOpFloat *y_dup = rz_il_op_pure_dup(y);
|
||||
return rz_il_op_new_forder(x_dup, y_dup);
|
||||
}
|
||||
|
||||
RZ_API RZ_OWN RzILOpBool *rz_il_op_new_fneq(RZ_NONNULL RZ_OWN RzILOpFloat *x, RZ_NONNULL RZ_OWN RzILOpFloat *y) {
|
||||
rz_return_val_if_fail(x && y, NULL);
|
||||
RzILOpBool *is_nan = _any_fl_is_nan(x, y);
|
||||
RzILOpBool *not_equal = rz_il_op_new_bool_or(_fl_is_less(x, y), _fl_is_less(y, x));
|
||||
return rz_il_op_new_bool_or(is_nan, not_equal);
|
||||
}
|
||||
|
||||
RZ_API RZ_OWN RzILOpBool *rz_il_op_new_feq(RZ_NONNULL RZ_OWN RzILOpFloat *x, RZ_NONNULL RZ_OWN RzILOpFloat *y) {
|
||||
rz_return_val_if_fail(x && y, NULL);
|
||||
return rz_il_op_new_bool_inv(rz_il_op_new_fneq(x, y));
|
||||
}
|
||||
|
||||
RZ_API RZ_OWN RzILOpBool *rz_il_op_new_flt(RZ_NONNULL RZ_OWN RzILOpFloat *x, RZ_NONNULL RZ_OWN RzILOpFloat *y) {
|
||||
rz_return_val_if_fail(x && y, NULL);
|
||||
RzILOpBool *not_nan = rz_il_op_new_bool_inv(_any_fl_is_nan(x, y));
|
||||
RzILOpBool *is_less = _fl_is_less(x, y);
|
||||
return rz_il_op_new_bool_and(not_nan, is_less);
|
||||
}
|
||||
|
||||
RZ_API RZ_OWN RzILOpBool *rz_il_op_new_fle(RZ_NONNULL RZ_OWN RzILOpFloat *x, RZ_NONNULL RZ_OWN RzILOpFloat *y) {
|
||||
rz_return_val_if_fail(x && y, NULL);
|
||||
RzILOpBool *not_nan = rz_il_op_new_bool_inv(_any_fl_is_nan(x, y));
|
||||
RzILOpBool *is_great = _fl_is_less(y, x);
|
||||
return rz_il_op_new_bool_and(not_nan, rz_il_op_new_bool_inv(is_great));
|
||||
}
|
||||
|
||||
RZ_API RZ_OWN RzILOpBool *rz_il_op_new_fgt(RZ_NONNULL RZ_OWN RzILOpFloat *x, RZ_NONNULL RZ_OWN RzILOpFloat *y) {
|
||||
rz_return_val_if_fail(x && y, NULL);
|
||||
RzILOpBool *not_nan = rz_il_op_new_bool_inv(_any_fl_is_nan(x, y));
|
||||
RzILOpBool *is_great = _fl_is_less(y, x);
|
||||
return rz_il_op_new_bool_and(not_nan, is_great);
|
||||
}
|
||||
|
||||
RZ_API RZ_OWN RzILOpBool *rz_il_op_new_fge(RZ_NONNULL RZ_OWN RzILOpFloat *x, RZ_NONNULL RZ_OWN RzILOpFloat *y) {
|
||||
rz_return_val_if_fail(x && y, NULL);
|
||||
RzILOpBool *not_nan = rz_il_op_new_bool_inv(_any_fl_is_nan(x, y));
|
||||
RzILOpBool *is_less = _fl_is_less(x, y);
|
||||
return rz_il_op_new_bool_and(not_nan, rz_il_op_new_bool_inv(is_less));
|
||||
}
|
||||
|
|
|
|||
|
|
@ -99,12 +99,12 @@
|
|||
#define AND(x, y) rz_il_op_new_bool_and(x, y)
|
||||
#define OR(x, y) rz_il_op_new_bool_or(x, y)
|
||||
|
||||
#define FNEQ(flx, fly) OR(OR(IS_FNAN(flx), IS_FNAN(fly)), OR(FORDER(DUP(flx), DUP(fly)), FORDER(DUP(fly), DUP(flx))))
|
||||
#define FEQ(flx, fly) AND(INV(OR(IS_FNAN(flx), IS_FNAN(fly))), INV(FNEQ(DUP(flx), DUP(fly))))
|
||||
#define FLT(flx, fly) AND(INV(OR(IS_FNAN(flx), IS_FNAN(fly))), FORDER(DUP(flx), DUP(fly)))
|
||||
#define FLE(flx, fly) AND(INV(OR(IS_FNAN(flx), IS_FNAN(fly))), OR(FLT(DUP(flx), DUP(fly)), FEQ(DUP(flx), DUP(fly))))
|
||||
#define FGT(flx, fly) AND(INV(OR(IS_FNAN(flx), IS_FNAN(fly))), INV(FLE(DUP(flx), DUP(fly))))
|
||||
#define FGE(flx, fly) AND(INV(OR(IS_FNAN(flx), IS_FNAN(fly))), INV(FLT(DUP(flx), DUP(fly))))
|
||||
#define FNEQ(flx, fly) rz_il_op_new_fneq(flx, fly)
|
||||
#define FEQ(flx, fly) rz_il_op_new_feq(flx, fly)
|
||||
#define FLT(flx, fly) rz_il_op_new_flt(flx, fly)
|
||||
#define FLE(flx, fly) rz_il_op_new_fle(flx, fly)
|
||||
#define FGT(flx, fly) rz_il_op_new_fgt(flx, fly)
|
||||
#define FGE(flx, fly) rz_il_op_new_fge(flx, fly)
|
||||
|
||||
#define UNSIGNED(n, x) rz_il_op_new_unsigned(n, x)
|
||||
#define SIGNED(n, x) rz_il_op_new_signed(n, x)
|
||||
|
|
|
|||
|
|
@ -780,6 +780,12 @@ RZ_API RZ_OWN RzILOpBitVector *rz_il_bswap16(RZ_BORROW RzILOpBitVector *t);
|
|||
RZ_API RZ_OWN RzILOpBitVector *rz_il_bswap32(RZ_BORROW RzILOpBitVector *t);
|
||||
RZ_API RZ_OWN RzILOpBitVector *rz_il_bswap64(RZ_BORROW RzILOpBitVector *t);
|
||||
RZ_API RZ_OWN RzILOpBool *rz_il_op_new_ne(RZ_NONNULL RzILOpPure *x, RZ_NONNULL RzILOpPure *y);
|
||||
RZ_API RZ_OWN RzILOpBool *rz_il_op_new_fneq(RZ_NONNULL RZ_OWN RzILOpFloat *x, RZ_NONNULL RZ_OWN RzILOpFloat *y);
|
||||
RZ_API RZ_OWN RzILOpBool *rz_il_op_new_feq(RZ_NONNULL RZ_OWN RzILOpFloat *x, RZ_NONNULL RZ_OWN RzILOpFloat *y);
|
||||
RZ_API RZ_OWN RzILOpBool *rz_il_op_new_flt(RZ_NONNULL RZ_OWN RzILOpFloat *x, RZ_NONNULL RZ_OWN RzILOpFloat *y);
|
||||
RZ_API RZ_OWN RzILOpBool *rz_il_op_new_fle(RZ_NONNULL RZ_OWN RzILOpFloat *x, RZ_NONNULL RZ_OWN RzILOpFloat *y);
|
||||
RZ_API RZ_OWN RzILOpBool *rz_il_op_new_fgt(RZ_NONNULL RZ_OWN RzILOpFloat *x, RZ_NONNULL RZ_OWN RzILOpFloat *y);
|
||||
RZ_API RZ_OWN RzILOpBool *rz_il_op_new_fge(RZ_NONNULL RZ_OWN RzILOpFloat *x, RZ_NONNULL RZ_OWN RzILOpFloat *y);
|
||||
|
||||
///////////////////////////////
|
||||
// Opcodes of type 'a effect //
|
||||
|
|
|
|||
|
|
@ -691,7 +691,7 @@ d "vacgt.f32 q0, q1, q2" 540e22f3 0x0 (seq empty (set d0 (cast 64 false (<< (cas
|
|||
d "vceq.i8 d0, d1, d2" 120801f3 0x0 (seq empty (set d0 (<< (cast 64 false (ite (== (cast 8 false (>> (var d1) (bv 8 0x0) false)) (cast 8 false (>> (var d2) (bv 8 0x0) false))) (~ (bv 8 0x0)) (bv 8 0x0))) (bv 8 0x0) false)) (set d0 (<< (cast 64 false (ite (== (cast 8 false (>> (var d1) (bv 8 0x8) false)) (cast 8 false (>> (var d2) (bv 8 0x8) false))) (~ (bv 8 0x0)) (bv 8 0x0))) (bv 8 0x8) false)) (set d0 (<< (cast 64 false (ite (== (cast 8 false (>> (var d1) (bv 8 0x10) false)) (cast 8 false (>> (var d2) (bv 8 0x10) false))) (~ (bv 8 0x0)) (bv 8 0x0))) (bv 8 0x10) false)) (set d0 (<< (cast 64 false (ite (== (cast 8 false (>> (var d1) (bv 8 0x18) false)) (cast 8 false (>> (var d2) (bv 8 0x18) false))) (~ (bv 8 0x0)) (bv 8 0x0))) (bv 8 0x18) false)) (set d0 (<< (cast 64 false (ite (== (cast 8 false (>> (var d1) (bv 8 0x20) false)) (cast 8 false (>> (var d2) (bv 8 0x20) false))) (~ (bv 8 0x0)) (bv 8 0x0))) (bv 8 0x20) false)) (set d0 (<< (cast 64 false (ite (== (cast 8 false (>> (var d1) (bv 8 0x28) false)) (cast 8 false (>> (var d2) (bv 8 0x28) false))) (~ (bv 8 0x0)) (bv 8 0x0))) (bv 8 0x28) false)) (set d0 (<< (cast 64 false (ite (== (cast 8 false (>> (var d1) (bv 8 0x30) false)) (cast 8 false (>> (var d2) (bv 8 0x30) false))) (~ (bv 8 0x0)) (bv 8 0x0))) (bv 8 0x30) false)) (set d0 (<< (cast 64 false (ite (== (cast 8 false (>> (var d1) (bv 8 0x38) false)) (cast 8 false (>> (var d2) (bv 8 0x38) false))) (~ (bv 8 0x0)) (bv 8 0x0))) (bv 8 0x38) false)))
|
||||
d "vceq.i16 d0, d1, d2" 120811f3 0x0 (seq empty (set d0 (<< (cast 64 false (ite (== (cast 16 false (>> (var d1) (bv 8 0x0) false)) (cast 16 false (>> (var d2) (bv 8 0x0) false))) (~ (bv 16 0x0)) (bv 16 0x0))) (bv 8 0x0) false)) (set d0 (<< (cast 64 false (ite (== (cast 16 false (>> (var d1) (bv 8 0x10) false)) (cast 16 false (>> (var d2) (bv 8 0x10) false))) (~ (bv 16 0x0)) (bv 16 0x0))) (bv 8 0x10) false)) (set d0 (<< (cast 64 false (ite (== (cast 16 false (>> (var d1) (bv 8 0x20) false)) (cast 16 false (>> (var d2) (bv 8 0x20) false))) (~ (bv 16 0x0)) (bv 16 0x0))) (bv 8 0x20) false)) (set d0 (<< (cast 64 false (ite (== (cast 16 false (>> (var d1) (bv 8 0x30) false)) (cast 16 false (>> (var d2) (bv 8 0x30) false))) (~ (bv 16 0x0)) (bv 16 0x0))) (bv 8 0x30) false)))
|
||||
d "vceq.i32 d0, d1, d2" 120821f3 0x0 (seq empty (set d0 (<< (cast 64 false (ite (== (cast 32 false (>> (var d1) (bv 8 0x0) false)) (cast 32 false (>> (var d2) (bv 8 0x0) false))) (~ (bv 32 0x0)) (bv 32 0x0))) (bv 8 0x0) false)) (set d0 (<< (cast 64 false (ite (== (cast 32 false (>> (var d1) (bv 8 0x20) false)) (cast 32 false (>> (var d2) (bv 8 0x20) false))) (~ (bv 32 0x0)) (bv 32 0x0))) (bv 8 0x20) false)))
|
||||
d "vceq.f32 d0, d1, d2" 020e01f2 0x0 (seq empty (set d0 (<< (cast 64 false (ite (&& (! (|| (is_nan (float 0 (cast 32 false (>> (var d1) (bv 8 0x0) false)) )) (is_nan (float 0 (cast 32 false (>> (var d2) (bv 8 0x0) false)) )))) (! (|| (|| (is_nan (float 0 (cast 32 false (>> (var d1) (bv 8 0x0) false)) )) (is_nan (float 0 (cast 32 false (>> (var d2) (bv 8 0x0) false)) ))) (|| (<. (float 0 (cast 32 false (>> (var d1) (bv 8 0x0) false)) ) (float 0 (cast 32 false (>> (var d2) (bv 8 0x0) false)) )) (<. (float 0 (cast 32 false (>> (var d2) (bv 8 0x0) false)) ) (float 0 (cast 32 false (>> (var d1) (bv 8 0x0) false)) )))))) (~ (bv 32 0x0)) (bv 32 0x0))) (bv 8 0x0) false)) (set d0 (<< (cast 64 false (ite (&& (! (|| (is_nan (float 0 (cast 32 false (>> (var d1) (bv 8 0x20) false)) )) (is_nan (float 0 (cast 32 false (>> (var d2) (bv 8 0x20) false)) )))) (! (|| (|| (is_nan (float 0 (cast 32 false (>> (var d1) (bv 8 0x20) false)) )) (is_nan (float 0 (cast 32 false (>> (var d2) (bv 8 0x20) false)) ))) (|| (<. (float 0 (cast 32 false (>> (var d1) (bv 8 0x20) false)) ) (float 0 (cast 32 false (>> (var d2) (bv 8 0x20) false)) )) (<. (float 0 (cast 32 false (>> (var d2) (bv 8 0x20) false)) ) (float 0 (cast 32 false (>> (var d1) (bv 8 0x20) false)) )))))) (~ (bv 32 0x0)) (bv 32 0x0))) (bv 8 0x20) false)))
|
||||
d "vceq.f32 d0, d1, d2" 020e01f2 0x0 (seq empty (set d0 (<< (cast 64 false (ite (! (|| (|| (is_nan (float 0 (cast 32 false (>> (var d1) (bv 8 0x0) false)) )) (is_nan (float 0 (cast 32 false (>> (var d2) (bv 8 0x0) false)) ))) (|| (<. (float 0 (cast 32 false (>> (var d1) (bv 8 0x0) false)) ) (float 0 (cast 32 false (>> (var d2) (bv 8 0x0) false)) )) (<. (float 0 (cast 32 false (>> (var d2) (bv 8 0x0) false)) ) (float 0 (cast 32 false (>> (var d1) (bv 8 0x0) false)) ))))) (~ (bv 32 0x0)) (bv 32 0x0))) (bv 8 0x0) false)) (set d0 (<< (cast 64 false (ite (! (|| (|| (is_nan (float 0 (cast 32 false (>> (var d1) (bv 8 0x20) false)) )) (is_nan (float 0 (cast 32 false (>> (var d2) (bv 8 0x20) false)) ))) (|| (<. (float 0 (cast 32 false (>> (var d1) (bv 8 0x20) false)) ) (float 0 (cast 32 false (>> (var d2) (bv 8 0x20) false)) )) (<. (float 0 (cast 32 false (>> (var d2) (bv 8 0x20) false)) ) (float 0 (cast 32 false (>> (var d1) (bv 8 0x20) false)) ))))) (~ (bv 32 0x0)) (bv 32 0x0))) (bv 8 0x20) false)))
|
||||
d "vcge.s8 d0, d1, d2" 120301f2 0x0 (seq empty (set d0 (<< (cast 64 false (ite (|| (! (sle (cast 8 false (>> (var d1) (bv 8 0x0) false)) (cast 8 false (>> (var d2) (bv 8 0x0) false)))) (== (cast 8 false (>> (var d1) (bv 8 0x0) false)) (cast 8 false (>> (var d2) (bv 8 0x0) false)))) (~ (bv 8 0x0)) (bv 8 0x0))) (bv 8 0x0) false)) (set d0 (<< (cast 64 false (ite (|| (! (sle (cast 8 false (>> (var d1) (bv 8 0x8) false)) (cast 8 false (>> (var d2) (bv 8 0x8) false)))) (== (cast 8 false (>> (var d1) (bv 8 0x8) false)) (cast 8 false (>> (var d2) (bv 8 0x8) false)))) (~ (bv 8 0x0)) (bv 8 0x0))) (bv 8 0x8) false)) (set d0 (<< (cast 64 false (ite (|| (! (sle (cast 8 false (>> (var d1) (bv 8 0x10) false)) (cast 8 false (>> (var d2) (bv 8 0x10) false)))) (== (cast 8 false (>> (var d1) (bv 8 0x10) false)) (cast 8 false (>> (var d2) (bv 8 0x10) false)))) (~ (bv 8 0x0)) (bv 8 0x0))) (bv 8 0x10) false)) (set d0 (<< (cast 64 false (ite (|| (! (sle (cast 8 false (>> (var d1) (bv 8 0x18) false)) (cast 8 false (>> (var d2) (bv 8 0x18) false)))) (== (cast 8 false (>> (var d1) (bv 8 0x18) false)) (cast 8 false (>> (var d2) (bv 8 0x18) false)))) (~ (bv 8 0x0)) (bv 8 0x0))) (bv 8 0x18) false)) (set d0 (<< (cast 64 false (ite (|| (! (sle (cast 8 false (>> (var d1) (bv 8 0x20) false)) (cast 8 false (>> (var d2) (bv 8 0x20) false)))) (== (cast 8 false (>> (var d1) (bv 8 0x20) false)) (cast 8 false (>> (var d2) (bv 8 0x20) false)))) (~ (bv 8 0x0)) (bv 8 0x0))) (bv 8 0x20) false)) (set d0 (<< (cast 64 false (ite (|| (! (sle (cast 8 false (>> (var d1) (bv 8 0x28) false)) (cast 8 false (>> (var d2) (bv 8 0x28) false)))) (== (cast 8 false (>> (var d1) (bv 8 0x28) false)) (cast 8 false (>> (var d2) (bv 8 0x28) false)))) (~ (bv 8 0x0)) (bv 8 0x0))) (bv 8 0x28) false)) (set d0 (<< (cast 64 false (ite (|| (! (sle (cast 8 false (>> (var d1) (bv 8 0x30) false)) (cast 8 false (>> (var d2) (bv 8 0x30) false)))) (== (cast 8 false (>> (var d1) (bv 8 0x30) false)) (cast 8 false (>> (var d2) (bv 8 0x30) false)))) (~ (bv 8 0x0)) (bv 8 0x0))) (bv 8 0x30) false)) (set d0 (<< (cast 64 false (ite (|| (! (sle (cast 8 false (>> (var d1) (bv 8 0x38) false)) (cast 8 false (>> (var d2) (bv 8 0x38) false)))) (== (cast 8 false (>> (var d1) (bv 8 0x38) false)) (cast 8 false (>> (var d2) (bv 8 0x38) false)))) (~ (bv 8 0x0)) (bv 8 0x0))) (bv 8 0x38) false)))
|
||||
d "vcge.s16 d0, d1, d2" 120311f2 0x0 (seq empty (set d0 (<< (cast 64 false (ite (|| (! (sle (cast 16 false (>> (var d1) (bv 8 0x0) false)) (cast 16 false (>> (var d2) (bv 8 0x0) false)))) (== (cast 16 false (>> (var d1) (bv 8 0x0) false)) (cast 16 false (>> (var d2) (bv 8 0x0) false)))) (~ (bv 16 0x0)) (bv 16 0x0))) (bv 8 0x0) false)) (set d0 (<< (cast 64 false (ite (|| (! (sle (cast 16 false (>> (var d1) (bv 8 0x10) false)) (cast 16 false (>> (var d2) (bv 8 0x10) false)))) (== (cast 16 false (>> (var d1) (bv 8 0x10) false)) (cast 16 false (>> (var d2) (bv 8 0x10) false)))) (~ (bv 16 0x0)) (bv 16 0x0))) (bv 8 0x10) false)) (set d0 (<< (cast 64 false (ite (|| (! (sle (cast 16 false (>> (var d1) (bv 8 0x20) false)) (cast 16 false (>> (var d2) (bv 8 0x20) false)))) (== (cast 16 false (>> (var d1) (bv 8 0x20) false)) (cast 16 false (>> (var d2) (bv 8 0x20) false)))) (~ (bv 16 0x0)) (bv 16 0x0))) (bv 8 0x20) false)) (set d0 (<< (cast 64 false (ite (|| (! (sle (cast 16 false (>> (var d1) (bv 8 0x30) false)) (cast 16 false (>> (var d2) (bv 8 0x30) false)))) (== (cast 16 false (>> (var d1) (bv 8 0x30) false)) (cast 16 false (>> (var d2) (bv 8 0x30) false)))) (~ (bv 16 0x0)) (bv 16 0x0))) (bv 8 0x30) false)))
|
||||
d "vcge.s32 d0, d1, d2" 120321f2 0x0 (seq empty (set d0 (<< (cast 64 false (ite (|| (! (sle (cast 32 false (>> (var d1) (bv 8 0x0) false)) (cast 32 false (>> (var d2) (bv 8 0x0) false)))) (== (cast 32 false (>> (var d1) (bv 8 0x0) false)) (cast 32 false (>> (var d2) (bv 8 0x0) false)))) (~ (bv 32 0x0)) (bv 32 0x0))) (bv 8 0x0) false)) (set d0 (<< (cast 64 false (ite (|| (! (sle (cast 32 false (>> (var d1) (bv 8 0x20) false)) (cast 32 false (>> (var d2) (bv 8 0x20) false)))) (== (cast 32 false (>> (var d1) (bv 8 0x20) false)) (cast 32 false (>> (var d2) (bv 8 0x20) false)))) (~ (bv 32 0x0)) (bv 32 0x0))) (bv 8 0x20) false)))
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@ d "call #0" 5c00 0x0 (branch (is_zero (var FCX)) nop (seq (branch (! (is_zero (&
|
|||
d "call #0" 6d000000 0x0 (branch (is_zero (var FCX)) nop (seq (branch (! (is_zero (& (>> (var PSW) (bv 32 0x7) false) (bv 32 0x1)))) (seq (set _psw_cdc (& (>> (var PSW) (bv 32 0x0) false) (bv 32 0x7f))) (branch (== (var _psw_cdc) (bv 32 0x7f)) (seq (set CDC (& (>> (var PSW) (bv 32 0x0) false) (bv 32 0x7f))) (set CDC_COUNT (let CDC (& (>> (var PSW) (bv 32 0x0) false) (bv 32 0x7f)) (ite (== (& (>> (var CDC) (bv 32 0x6) false) (bv 32 0x1)) (bv 32 0x0)) (& (>> (var CDC) (bv 32 0x0) false) (bv 32 0x3f)) (ite (== (& (>> (var CDC) (bv 32 0x5) false) (bv 32 0x3)) (bv 32 0x2)) (& (>> (var CDC) (bv 32 0x0) false) (bv 32 0x1f)) (ite (== (& (>> (var CDC) (bv 32 0x4) false) (bv 32 0x7)) (bv 32 0x6)) (& (>> (var CDC) (bv 32 0x0) false) (bv 32 0xf)) (ite (== (& (>> (var CDC) (bv 32 0x3) false) (bv 32 0xf)) (bv 32 0xe)) (& (>> (var CDC) (bv 32 0x0) false) (bv 32 0x7)) (ite (== (& (>> (var CDC) (bv 32 0x2) false) (bv 32 0x1f)) (bv 32 0x1e)) (& (>> (var CDC) (bv 32 0x0) false) (bv 32 0x3)) (ite (== (& (>> (var CDC) (bv 32 0x1) false) (bv 32 0x3f)) (bv 32 0x3e)) (& (>> (var CDC) (bv 32 0x0) false) (bv 32 0x1)) (bv 32 0x0))))))))) (set CDC_i (let CDC (& (>> (var PSW) (bv 32 0x0) false) (bv 32 0x7f)) (ite (== (& (>> (var CDC) (bv 32 0x6) false) (bv 32 0x1)) (bv 32 0x0)) (bv 32 0x6) (ite (== (& (>> (var CDC) (bv 32 0x5) false) (bv 32 0x3)) (bv 32 0x2)) (bv 32 0x5) (ite (== (& (>> (var CDC) (bv 32 0x4) false) (bv 32 0x7)) (bv 32 0x6)) (bv 32 0x4) (ite (== (& (>> (var CDC) (bv 32 0x3) false) (bv 32 0xf)) (bv 32 0xe)) (bv 32 0x3) (ite (== (& (>> (var CDC) (bv 32 0x2) false) (bv 32 0x1f)) (bv 32 0x1e)) (bv 32 0x2) (ite (== (& (>> (var CDC) (bv 32 0x1) false) (bv 32 0x3f)) (bv 32 0x3e)) (bv 32 0x1) (bv 32 0x0))))))))) (set PSW (| (& (var PSW) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (var CDC_i)) false) (bv 32 0x0) false))) (& (<< (+ (var _psw_cdc) (bv 32 0x1)) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (var CDC_i)) false) (bv 32 0x0) false)))) (branch (== (var CDC_COUNT) (- (<< (bv 32 0x1) (var CDC_i) false) (bv 32 0x1))) nop nop)) nop)) nop) (set PSW (| (& (var PSW) (bv 32 0xffffff7f)) (<< (& (bv 32 0x1) (bv 32 0x1)) (bv 32 0x7) false))) (set tmp_FCX (var FCX)) (set EA (| (<< (& (>> (var FCX) (bv 32 0x10) false) (bv 32 0xf)) (bv 32 0x1c) false) (<< (& (>> (var FCX) (bv 32 0x0) false) (bv 32 0x7fff)) (bv 32 0x6) false))) (set new_FCX (loadw 0 32 (var EA))) (storew 0 (var EA) (var d15)) (storew 0 (+ (var EA) (bv 32 0x4)) (var d14)) (storew 0 (+ (var EA) (bv 32 0x8)) (var d13)) (storew 0 (+ (var EA) (bv 32 0xc)) (var d12)) (storew 0 (+ (var EA) (bv 32 0x10)) (var a15)) (storew 0 (+ (var EA) (bv 32 0x14)) (var a14)) (storew 0 (+ (var EA) (bv 32 0x18)) (var a13)) (storew 0 (+ (var EA) (bv 32 0x1c)) (var a12)) (storew 0 (+ (var EA) (bv 32 0x20)) (var d11)) (storew 0 (+ (var EA) (bv 32 0x24)) (var d10)) (storew 0 (+ (var EA) (bv 32 0x28)) (var d9)) (storew 0 (+ (var EA) (bv 32 0x2c)) (var d8)) (storew 0 (+ (var EA) (bv 32 0x30)) (var a11)) (storew 0 (+ (var EA) (bv 32 0x34)) (var a10)) (storew 0 (+ (var EA) (bv 32 0x38)) (var PSW)) (storew 0 (+ (var EA) (bv 32 0x3c)) (var PCXI)) (set PCXI (| (& (var PCXI) (bv 32 0xc03fffff)) (<< (& (& (>> (var ICR) (bv 32 0x0) false) (bv 32 0xff)) (bv 32 0xff)) (bv 32 0x16) false))) (set PCXI (| (& (var PCXI) (bv 32 0xc03fffff)) (<< (& (& (>> (var ICR) (bv 32 0x8) false) (bv 32 0x1)) (bv 32 0xff)) (bv 32 0x16) false))) (set PCXI (| (& (var PCXI) (bv 32 0xc03fffff)) (<< (& (bv 32 0x1) (bv 32 0xff)) (bv 32 0x16) false))) (set PCXI (| (& (var PCXI) (bv 32 0xfff00000)) (<< (& (& (>> (var FCX) (bv 32 0x0) false) (bv 32 0xfffff)) (bv 32 0xfffff)) (bv 32 0x0) false))) (set FCX (| (& (var FCX) (bv 32 0xfff00000)) (<< (& (& (>> (var new_FCX) (bv 32 0x0) false) (bv 32 0xfffff)) (bv 32 0xfffff)) (bv 32 0x0) false))) (set a11 (bv 32 0x4)) (branch (== (var new_FCX) (var LCX)) nop (jmp (bv 32 0x0)))))
|
||||
d "fret" 0070 0x80001000 (seq (set a11_tmp (var a11)) (set EA (var a10)) (set a11 (loadw 0 32 (var EA))) (set a10 (+ (var a10) (bv 32 0x4))) (jmp (& (var a11_tmp) (bv 32 0xfffffffe))))
|
||||
d "fret" 0d00c000 0x80001000 (seq (set a11_tmp (var a11)) (set EA (var a10)) (set a11 (loadw 0 32 (var EA))) (set a10 (+ (var a10) (bv 32 0x4))) (jmp (& (var a11_tmp) (bv 32 0xfffffffe))))
|
||||
d "ftohp d0, d0" 4b005102 0x80001000 (branch (is_inf (float 0 (var d0) )) (branch (msb (var d0)) (set d0 (bv 32 0xfc00)) (set d0 (bv 32 0x7c00))) (branch (is_nan (float 0 (var d0) )) (seq (set D_c (| (| (| (& (var d0) (bv 32 0x80000000)) (<< (bv 32 0x1f) (bv 32 0xa) false)) (<< (& (>> (var d0) (bv 32 0x15) false) (bv 32 0x3)) (bv 32 0x8) false)) (& (>> (var d0) (bv 32 0x0) false) (bv 32 0xff)))) (set d0 (ite (== (& (>> (var D_c) (bv 32 0x0) false) (bv 32 0x3ff)) (bv 32 0x0)) (| (& (var D_c) (bv 32 0xfffffeff)) (<< (& (bv 32 0x1) (bv 32 0x1)) (bv 32 0x8) false)) (var D_c)))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (<< (& (cast 32 false (fbits (fconvert unk_format rne (let tmp (float 0 (var d0) ) (ite (&& (&& (! (|| (is_nan (var tmp)) (is_nan (float 0 (bv 32 0x0) )))) (<. (var tmp) (float 0 (bv 32 0x0) ))) (&& (! (|| (is_nan (var tmp)) (is_nan (float 0 (bv 32 0x800000) )))) (! (&& (! (|| (is_nan (var tmp)) (is_nan (float 0 (bv 32 0x800000) )))) (|| (&& (! (|| (is_nan (var tmp)) (is_nan (float 0 (bv 32 0x800000) )))) (<. (var tmp) (float 0 (bv 32 0x800000) ))) (&& (! (|| (is_nan (var tmp)) (is_nan (float 0 (bv 32 0x800000) )))) (! (|| (|| (is_nan (var tmp)) (is_nan (float 0 (bv 32 0x800000) ))) (|| (<. (var tmp) (float 0 (bv 32 0x800000) )) (<. (float 0 (bv 32 0x800000) ) (var tmp))))))))))) (fneg (float 0 (bv 32 0x0) )) (ite (&& (&& (! (|| (is_nan (var tmp)) (is_nan (float 0 (bv 32 0x0) )))) (! (&& (! (|| (is_nan (var tmp)) (is_nan (float 0 (bv 32 0x0) )))) (|| (&& (! (|| (is_nan (var tmp)) (is_nan (float 0 (bv 32 0x0) )))) (<. (var tmp) (float 0 (bv 32 0x0) ))) (&& (! (|| (is_nan (var tmp)) (is_nan (float 0 (bv 32 0x0) )))) (! (|| (|| (is_nan (var tmp)) (is_nan (float 0 (bv 32 0x0) ))) (|| (<. (var tmp) (float 0 (bv 32 0x0) )) (<. (float 0 (bv 32 0x0) ) (var tmp)))))))))) (&& (! (|| (is_nan (var tmp)) (is_nan (float 0 (bv 32 0x800000) )))) (<. (var tmp) (float 0 (bv 32 0x800000) )))) (float 0 (bv 32 0x0) ) (var tmp))))))) (bv 32 0xffff)) (bv 32 0x0) false)))))
|
||||
d "ftohp d0, d0" 4b005102 0x80001000 (branch (is_inf (float 0 (var d0) )) (branch (msb (var d0)) (set d0 (bv 32 0xfc00)) (set d0 (bv 32 0x7c00))) (branch (is_nan (float 0 (var d0) )) (seq (set D_c (| (| (| (& (var d0) (bv 32 0x80000000)) (<< (bv 32 0x1f) (bv 32 0xa) false)) (<< (& (>> (var d0) (bv 32 0x15) false) (bv 32 0x3)) (bv 32 0x8) false)) (& (>> (var d0) (bv 32 0x0) false) (bv 32 0xff)))) (set d0 (ite (== (& (>> (var D_c) (bv 32 0x0) false) (bv 32 0x3ff)) (bv 32 0x0)) (| (& (var D_c) (bv 32 0xfffffeff)) (<< (& (bv 32 0x1) (bv 32 0x1)) (bv 32 0x8) false)) (var D_c)))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (<< (& (cast 32 false (fbits (fconvert unk_format rne (let tmp (float 0 (var d0) ) (ite (&& (&& (! (|| (is_nan (var tmp)) (is_nan (float 0 (bv 32 0x0) )))) (<. (var tmp) (float 0 (bv 32 0x0) ))) (&& (! (|| (is_nan (var tmp)) (is_nan (float 0 (bv 32 0x800000) )))) (<. (float 0 (bv 32 0x800000) ) (var tmp)))) (fneg (float 0 (bv 32 0x0) )) (ite (&& (&& (! (|| (is_nan (var tmp)) (is_nan (float 0 (bv 32 0x0) )))) (<. (float 0 (bv 32 0x0) ) (var tmp))) (&& (! (|| (is_nan (var tmp)) (is_nan (float 0 (bv 32 0x800000) )))) (<. (var tmp) (float 0 (bv 32 0x800000) )))) (float 0 (bv 32 0x0) ) (var tmp))))))) (bv 32 0xffff)) (bv 32 0x0) false)))))
|
||||
d "ld.w d0, #0x3c0" 850000f0 0x80001000 (set d0 (loadw 0 32 (bv 32 0x3c0)))
|
||||
d "ld.a a0, #0" 85000008 0x80001000 (set a0 (loadw 0 32 (bv 32 0x0)))
|
||||
d "ld.d e0, #0" 85000004 0x80001000 (seq (set temp (loadw 0 64 (bv 32 0x0))) (set d0 (cast 32 false (var temp))) (set d1 (cast 32 false (& (>> (var temp) (bv 64 0x20) false) (bv 64 0xffffffff)))))
|
||||
|
|
@ -799,4 +799,4 @@ d "swapmsk.w [p0+c]#0, e0" 69008004 0x0 (seq (set index (& (>> (var a0) (bv 32 0
|
|||
d "swapmsk.w [a0]#0, e0" 49008008 0x0 (seq (set EA (+ (var a0) (bv 32 0x0))) (set tmp (loadw 0 32 (var EA))) (storew 0 (var EA) (| (& (var tmp) (~ (var d1))) (& (var d0) (var d1)))) (set d0 (var tmp)))
|
||||
d "swapmsk.w [p0+i], e0" 69008008
|
||||
d "updfl d0" 4b00c100 0x0 (set PSW (| (& (var PSW) (bv 32 0xffffff)) (<< (& (| (& (& (>> (var PSW) (bv 32 0x18) false) (bv 32 0xff)) (~ (& (>> (var d0) (bv 32 0x8) false) (bv 32 0xff)))) (& (& (>> (var d0) (bv 32 0x0) false) (bv 32 0xff)) (& (>> (var d0) (bv 32 0x8) false) (bv 32 0xff)))) (bv 32 0xff)) (bv 32 0x18) false)))
|
||||
d "cmp.f d0, d0, d0" 4b000000 0x0 (set d0 (| (ite (&& (! (|| (is_nan (float 0 (var d0) )) (is_nan (float 0 (var d0) )))) (<. (float 0 (var d0) ) (float 0 (var d0) ))) (bv 32 0x1) (bv 32 0x0)) (| (<< (ite (&& (! (|| (is_nan (float 0 (var d0) )) (is_nan (float 0 (var d0) )))) (! (|| (|| (is_nan (float 0 (var d0) )) (is_nan (float 0 (var d0) ))) (|| (<. (float 0 (var d0) ) (float 0 (var d0) )) (<. (float 0 (var d0) ) (float 0 (var d0) )))))) (bv 32 0x1) (bv 32 0x0)) (bv 32 0x1) false) (| (<< (ite (&& (! (|| (is_nan (float 0 (var d0) )) (is_nan (float 0 (var d0) )))) (! (&& (! (|| (is_nan (float 0 (var d0) )) (is_nan (float 0 (var d0) )))) (|| (&& (! (|| (is_nan (float 0 (var d0) )) (is_nan (float 0 (var d0) )))) (<. (float 0 (var d0) ) (float 0 (var d0) ))) (&& (! (|| (is_nan (float 0 (var d0) )) (is_nan (float 0 (var d0) )))) (! (|| (|| (is_nan (float 0 (var d0) )) (is_nan (float 0 (var d0) ))) (|| (<. (float 0 (var d0) ) (float 0 (var d0) )) (<. (float 0 (var d0) ) (float 0 (var d0) )))))))))) (bv 32 0x1) (bv 32 0x0)) (bv 32 0x2) false) (| (<< (ite (|| (is_nan (float 0 (var d0) )) (is_nan (float 0 (var d0) ))) (bv 32 0x1) (bv 32 0x0)) (bv 32 0x3) false) (| (<< (ite (&& (is_zero (& (>> (var d0) (bv 32 0x17) false) (bv 32 0xff))) (! (is_zero (& (>> (var d0) (bv 32 0x0) false) (bv 32 0x7fffff))))) (bv 32 0x1) (bv 32 0x0)) (bv 32 0x4) false) (<< (ite (&& (is_zero (& (>> (var d0) (bv 32 0x17) false) (bv 32 0xff))) (! (is_zero (& (>> (var d0) (bv 32 0x0) false) (bv 32 0x7fffff))))) (bv 32 0x1) (bv 32 0x0)) (bv 32 0x5) false)))))))
|
||||
d "cmp.f d0, d0, d0" 4b000000 0x0 (set d0 (| (ite (&& (! (|| (is_nan (float 0 (var d0) )) (is_nan (float 0 (var d0) )))) (<. (float 0 (var d0) ) (float 0 (var d0) ))) (bv 32 0x1) (bv 32 0x0)) (| (<< (ite (! (|| (|| (is_nan (float 0 (var d0) )) (is_nan (float 0 (var d0) ))) (|| (<. (float 0 (var d0) ) (float 0 (var d0) )) (<. (float 0 (var d0) ) (float 0 (var d0) ))))) (bv 32 0x1) (bv 32 0x0)) (bv 32 0x1) false) (| (<< (ite (&& (! (|| (is_nan (float 0 (var d0) )) (is_nan (float 0 (var d0) )))) (<. (float 0 (var d0) ) (float 0 (var d0) ))) (bv 32 0x1) (bv 32 0x0)) (bv 32 0x2) false) (| (<< (ite (|| (is_nan (float 0 (var d0) )) (is_nan (float 0 (var d0) ))) (bv 32 0x1) (bv 32 0x0)) (bv 32 0x3) false) (| (<< (ite (&& (is_zero (& (>> (var d0) (bv 32 0x17) false) (bv 32 0xff))) (! (is_zero (& (>> (var d0) (bv 32 0x0) false) (bv 32 0x7fffff))))) (bv 32 0x1) (bv 32 0x0)) (bv 32 0x4) false) (<< (ite (&& (is_zero (& (>> (var d0) (bv 32 0x17) false) (bv 32 0xff))) (! (is_zero (& (>> (var d0) (bv 32 0x0) false) (bv 32 0x7fffff))))) (bv 32 0x1) (bv 32 0x0)) (bv 32 0x5) false)))))))
|
||||
|
|
|
|||
|
|
@ -1046,20 +1046,20 @@ ad "fldl2e" d9ea 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) fal
|
|||
ad "fldpi" d9eb 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 3 (| (<< (bv 128 0x4000c90fdaa22168) (bv 8 0x8) false) (bv 128 0xc000000000000000)) )) (fconvert ieee754-bin80 rtz (float 3 (| (<< (bv 128 0x4000c90fdaa22168) (bv 8 0x8) false) (bv 128 0xc000000000000000)) ))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
|
||||
ad "fldlg2" d9ec 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 3 (| (<< (bv 128 0x3fff9a209a84fbcf) (bv 8 0x8) false) (bv 128 0xc000000000000000)) )) (fconvert ieee754-bin80 rtz (float 3 (| (<< (bv 128 0x3fff9a209a84fbcf) (bv 8 0x8) false) (bv 128 0xc000000000000000)) ))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
|
||||
ad "fldln2" d9ed 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 3 (| (<< (bv 128 0x3ffeb17217f7d1cf) (bv 8 0x8) false) (bv 128 0x4000000000000000)) )) (fconvert ieee754-bin80 rtz (float 3 (| (<< (bv 128 0x3ffeb17217f7d1cf) (bv 8 0x8) false) (bv 128 0x4000000000000000)) ))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
|
||||
a "fucom" dde1 0x0 (seq (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st1) )))) (<. (float 2 (var st0) ) (float 2 (var st1) ))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x8) false) (& (bv 16 0xfeff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0xa) false) (& (bv 16 0xfbff) (var swd)))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st1) )))) (! (|| (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st1) ))) (|| (<. (float 2 (var st0) ) (float 2 (var st1) )) (<. (float 2 (var st1) ) (float 2 (var st0) )))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0xe) false) (& (bv 16 0xbfff) (var swd)))))
|
||||
a "fucom st(2)" dde2 0x0 (seq (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st2) )))) (<. (float 2 (var st0) ) (float 2 (var st2) ))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x8) false) (& (bv 16 0xfeff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0xa) false) (& (bv 16 0xfbff) (var swd)))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st2) )))) (! (|| (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st2) ))) (|| (<. (float 2 (var st0) ) (float 2 (var st2) )) (<. (float 2 (var st2) ) (float 2 (var st0) )))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0xe) false) (& (bv 16 0xbfff) (var swd)))))
|
||||
a "fucomp" dde9 0x0 (seq (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st1) )))) (<. (float 2 (var st0) ) (float 2 (var st1) ))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x8) false) (& (bv 16 0xfeff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0xa) false) (& (bv 16 0xfbff) (var swd)))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st1) )))) (! (|| (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st1) ))) (|| (<. (float 2 (var st0) ) (float 2 (var st1) )) (<. (float 2 (var st1) ) (float 2 (var st0) )))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0xe) false) (& (bv 16 0xbfff) (var swd)))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
|
||||
a "fucomp st(2)" ddea 0x0 (seq (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st2) )))) (<. (float 2 (var st0) ) (float 2 (var st2) ))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x8) false) (& (bv 16 0xfeff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0xa) false) (& (bv 16 0xfbff) (var swd)))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st2) )))) (! (|| (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st2) ))) (|| (<. (float 2 (var st0) ) (float 2 (var st2) )) (<. (float 2 (var st2) ) (float 2 (var st0) )))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0xe) false) (& (bv 16 0xbfff) (var swd)))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
|
||||
a "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)))))))) (! (|| (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))))) (|| (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0)))))) (<. (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0xe) false) (& (bv 16 0xbfff) (var swd)))))
|
||||
a "ficom dword [rax]" da10 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0)))))))) (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x8) false) (& (bv 16 0xfeff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0xa) false) (& (bv 16 0xfbff) (var swd)))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0)))))))) (! (|| (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))))) (|| (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0)))))) (<. (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0xe) false) (& (bv 16 0xbfff) (var swd)))))
|
||||
a "ficomp word [rax]" de18 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0)))))))) (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x8) false) (& (bv 16 0xfeff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0xa) false) (& (bv 16 0xfbff) (var swd)))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0)))))))) (! (|| (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))))) (|| (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0)))))) (<. (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0xe) false) (& (bv 16 0xbfff) (var swd)))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
|
||||
a "ficomp dword [rax]" da18 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0)))))))) (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x8) false) (& (bv 16 0xfeff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0xa) false) (& (bv 16 0xfbff) (var swd)))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0)))))))) (! (|| (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))))) (|| (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0)))))) (<. (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0xe) false) (& (bv 16 0xbfff) (var swd)))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
|
||||
a "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)))))
|
||||
|
|
|
|||
Loading…
Reference in a new issue