From 43c3228a122fcd648ed3cdbbd25bc899d5bca519 Mon Sep 17 00:00:00 2001 From: Dhruv Maroo Date: Thu, 4 Jan 2024 15:44:46 +0530 Subject: [PATCH] Add asm tests for math constant push instructions --- test/db/asm/x86_64 | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/test/db/asm/x86_64 b/test/db/asm/x86_64 index 38c815a76b6..0fc114e74ed 100644 --- a/test/db/asm/x86_64 +++ b/test/db/asm/x86_64 @@ -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)))))