Skip to content

Commit

Permalink
Add asm tests for math constant push instructions
Browse files Browse the repository at this point in the history
  • Loading branch information
@DMaroo
DMaroo committed Jan 4, 2024
1 parent c4621c8 commit 43c3228
Showing 1 changed file with 7 additions and 0 deletions.
7 changes: 7 additions & 0 deletions test/db/asm/x86_64
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1039,6 +1039,13 @@ a "ffree st(7)" ddc7
a "frstor [eax]" dd20
a "fxch" d9c9 0x0 (seq (set tmp (float 2 (var st0) )) (set st0 (fbits (float 2 (var st0) ))) (set st0 (fbits (var tmp))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
a "fxch st2" d9ca 0x0 (seq (set tmp (float 2 (var st0) )) (set st0 (fbits (float 2 (var st0) ))) (set st0 (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 0x3fff0000000000000000) ))) (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 (>> (bv 8 0xa) (var cwd) 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 (>> (bv 8 0xa) (var cwd) 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 (>> (bv 8 0xa) (var cwd) 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 (>> (bv 8 0xa) (var cwd) 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 (>> (bv 8 0xa) (var cwd) 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)))))
Expand Down

0 comments on commit 43c3228

Please sign in to comment.