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

Remove unnecessary local variable in IL for test instruction

Browse source
This commit is contained in:
Dhruv Maroo 2023-03-01 07:48:39 +05:30 committed by Anton Kochkov
parent 5211e1835b
commit aa7781b098
4 changed files with 30 additions and 31 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
librz/analysis/arch/x86/x86_il.c
View file

@ -3467,11 +3467,10 @@ IL_LIFTER(sub) {
* Encoding: I, MI, MR
*/
IL_LIFTER(test) {
RzILOpEffect *res = SETL("_res", LOGAND(x86_il_get_op(0), x86_il_get_op(1)));
RzILOpEffect *res_flags = x86_il_set_result_flags(VARL("_res"));
RzILOpEffect *res_flags = x86_il_set_result_flags(LOGAND(x86_il_get_op(0), x86_il_get_op(1)));
RzILOpEffect *arith_flags = SEQ2(SETG(EFLAGS(CF), IL_FALSE), SETG(EFLAGS(OF), IL_FALSE));
return SEQ3(res, res_flags, arith_flags);
return SEQ2(res_flags, arith_flags);
}
/**

4
test/db/asm/x86_16
View file

@ -24,8 +24,8 @@ d "popf" 9d 0x0 (seq (set _flags (loadw 0 16 (+ (+ (cast 16 false (var sp)) (bv
ad "push ax" 50 0x0 (seq (set sp (- (var sp) (bv 16 0x4))) (storew 0 (+ (+ (cast 16 false (var sp)) (bv 16 0x0)) (<< (cast 16 false (var ss)) (bv 8 0x4) false)) (cast 16 false (var ax))))
d "pushf" 9c 0x0 (seq (set sp (- (var sp) (bv 16 0x2))) (storew 0 (+ (+ (cast 16 false (var sp)) (bv 16 0x0)) (<< (cast 16 false (var ss)) (bv 8 0x4) false)) (cast 16 false (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 16 0x1) false) (ite (var nt) (bv 16 0x1) (bv 16 0x0))) (bv 16 0x2) false) (bv 16 0x3)) (bv 16 0x1) false) (ite (var of) (bv 16 0x1) (bv 16 0x0))) (bv 16 0x1) false) (ite (var df) (bv 16 0x1) (bv 16 0x0))) (bv 16 0x1) false) (ite (var if) (bv 16 0x1) (bv 16 0x0))) (bv 16 0x1) false) (ite (var tf) (bv 16 0x1) (bv 16 0x0))) (bv 16 0x1) false) (ite (var zf) (bv 16 0x1) (bv 16 0x0))) (bv 16 0x1) false) (ite (var zf) (bv 16 0x1) (bv 16 0x0))) (bv 16 0x2) false) (ite (var af) (bv 16 0x1) (bv 16 0x0))) (bv 16 0x2) false) (ite (var pf) (bv 16 0x1) (bv 16 0x0))) (bv 16 0x1) false) (bv 16 0x1)) (bv 16 0x1) false) (ite (var cf) (bv 16 0x1) (bv 16 0x0))))))
d "pushaw" 60 0x0 (seq (set _sp (var sp)) (set sp (- (var sp) (bv 16 0x2))) (storew 0 (+ (+ (cast 16 false (var sp)) (bv 16 0x0)) (<< (cast 16 false (var ss)) (bv 8 0x4) false)) (cast 16 false (var ax))) (set sp (- (var sp) (bv 16 0x2))) (storew 0 (+ (+ (cast 16 false (var sp)) (bv 16 0x0)) (<< (cast 16 false (var ss)) (bv 8 0x4) false)) (cast 16 false (var cx))) (set sp (- (var sp) (bv 16 0x2))) (storew 0 (+ (+ (cast 16 false (var sp)) (bv 16 0x0)) (<< (cast 16 false (var ss)) (bv 8 0x4) false)) (cast 16 false (var dx))) (set sp (- (var sp) (bv 16 0x2))) (storew 0 (+ (+ (cast 16 false (var sp)) (bv 16 0x0)) (<< (cast 16 false (var ss)) (bv 8 0x4) false)) (cast 16 false (var bx))) (set sp (- (var sp) (bv 16 0x2))) (storew 0 (+ (+ (cast 16 false (var sp)) (bv 16 0x0)) (<< (cast 16 false (var ss)) (bv 8 0x4) false)) (cast 16 false (var _sp))) (set sp (- (var sp) (bv 16 0x2))) (storew 0 (+ (+ (cast 16 false (var sp)) (bv 16 0x0)) (<< (cast 16 false (var ss)) (bv 8 0x4) false)) (cast 16 false (var bp))) (set sp (- (var sp) (bv 16 0x2))) (storew 0 (+ (+ (cast 16 false (var sp)) (bv 16 0x0)) (<< (cast 16 false (var ss)) (bv 8 0x4) false)) (cast 16 false (var si))) (set sp (- (var sp) (bv 16 0x2))) (storew 0 (+ (+ (cast 16 false (var sp)) (bv 16 0x0)) (<< (cast 16 false (var ss)) (bv 8 0x4) false)) (cast 16 false (var di))))
a "test bl, 0x12" f6c312 0x0 (seq (set _res (& (cast 8 false (var bx)) (bv 8 0x12))) (set _result (var _res)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test bx, 0x1234" f7c33412 0x0 (seq (set _res (& (var bx) (bv 16 0x1234))) (set _result (var _res)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test bl, 0x12" f6c312 0x0 (seq (set _result (& (cast 8 false (var bx)) (bv 8 0x12))) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test bx, 0x1234" f7c33412 0x0 (seq (set _result (& (var bx) (bv 16 0x1234))) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
aB "test byte [bx], 0x12" f60712
aB "test word [bx], 0x1234" f7073412
a "xlatb" d7 0x0 (set ax (| (& (var ax) (~ (bv 16 0xff))) (cast 16 false (loadw 0 8 (+ (+ (+ (var bx) (bv 16 0x0)) (<< (cast 16 false (var ds)) (bv 8 0x4) false)) (cast 16 false (cast 8 false (var ax))))))))

34
test/db/asm/x86_32
View file

@ -500,15 +500,15 @@ d "syscall" 0f05
d "sysenter" 0f34
d "sysexit" 0f35
d "sysret" 0f07
d "test al, 0" a800 0x0 (seq (set _res (& (cast 8 false (var eax)) (bv 8 0x0))) (set _result (var _res)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
d "test byte [eax], 0" f60000 0x0 (seq (set _res (& (loadw 0 8 (+ (var eax) (bv 32 0x0))) (bv 8 0x0))) (set _result (var _res)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
d "test byte [eax], 0" f60800 0x0 (seq (set _res (& (loadw 0 8 (+ (var eax) (bv 32 0x0))) (bv 8 0x0))) (set _result (var _res)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
d "test byte [eax], al" 8400 0x0 (seq (set _res (& (loadw 0 8 (+ (var eax) (bv 32 0x0))) (cast 8 false (var eax)))) (set _result (var _res)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
d "test dword [eax], 0" f70000000000 0x0 (seq (set _res (& (loadw 0 32 (+ (var eax) (bv 32 0x0))) (bv 32 0x0))) (set _result (var _res)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
d "test dword [eax], 0" f70000000000 0x0 (seq (set _res (& (loadw 0 32 (+ (var eax) (bv 32 0x0))) (bv 32 0x0))) (set _result (var _res)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
d "test dword [eax], 0" f70800000000 0x0 (seq (set _res (& (loadw 0 32 (+ (var eax) (bv 32 0x0))) (bv 32 0x0))) (set _result (var _res)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
d "test dword [eax], eax" 8500 0x0 (seq (set _res (& (loadw 0 32 (+ (var eax) (bv 32 0x0))) (var eax))) (set _result (var _res)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
d "test eax, 0" a900000000 0x0 (seq (set _res (& (var eax) (bv 32 0x0))) (set _result (var _res)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
d "test al, 0" a800 0x0 (seq (set _result (& (cast 8 false (var eax)) (bv 8 0x0))) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
d "test byte [eax], 0" f60000 0x0 (seq (set _result (& (loadw 0 8 (+ (var eax) (bv 32 0x0))) (bv 8 0x0))) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
d "test byte [eax], 0" f60800 0x0 (seq (set _result (& (loadw 0 8 (+ (var eax) (bv 32 0x0))) (bv 8 0x0))) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
d "test byte [eax], al" 8400 0x0 (seq (set _result (& (loadw 0 8 (+ (var eax) (bv 32 0x0))) (cast 8 false (var eax)))) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
d "test dword [eax], 0" f70000000000 0x0 (seq (set _result (& (loadw 0 32 (+ (var eax) (bv 32 0x0))) (bv 32 0x0))) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
d "test dword [eax], 0" f70000000000 0x0 (seq (set _result (& (loadw 0 32 (+ (var eax) (bv 32 0x0))) (bv 32 0x0))) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
d "test dword [eax], 0" f70800000000 0x0 (seq (set _result (& (loadw 0 32 (+ (var eax) (bv 32 0x0))) (bv 32 0x0))) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
d "test dword [eax], eax" 8500 0x0 (seq (set _result (& (loadw 0 32 (+ (var eax) (bv 32 0x0))) (var eax))) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
d "test eax, 0" a900000000 0x0 (seq (set _result (& (var eax) (bv 32 0x0))) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
d "ud2" 0f0b
d "unpckhpd xmm0, xmmword [eax]" 660f1500
d "unpcklpd xmm0, xmmword [eax]" 660f1400
@ -2018,14 +2018,14 @@ a "syscall" 0f05
a "sysenter" 0f34
a "sysexit" 0f35
a "sysret" 0f07
a "test al, 0" f6c000 0x0 (seq (set _res (& (cast 8 false (var eax)) (bv 8 0x0))) (set _result (var _res)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test byte [eax], 0" f60000 0x0 (seq (set _res (& (loadw 0 8 (+ (var eax) (bv 32 0x0))) (bv 8 0x0))) (set _result (var _res)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test byte [eax], al" 8400 0x0 (seq (set _res (& (loadw 0 8 (+ (var eax) (bv 32 0x0))) (cast 8 false (var eax)))) (set _result (var _res)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test dword [eax], 0" f70000000000 0x0 (seq (set _res (& (loadw 0 32 (+ (var eax) (bv 32 0x0))) (bv 32 0x0))) (set _result (var _res)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test dword [eax], eax" 8500 0x0 (seq (set _res (& (loadw 0 32 (+ (var eax) (bv 32 0x0))) (var eax))) (set _result (var _res)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test eax, 0" f7c000000000 0x0 (seq (set _res (& (var eax) (bv 32 0x0))) (set _result (var _res)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test eax, ebx" 85d8 0x0 (seq (set _res (& (var eax) (var ebx))) (set _result (var _res)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test edx, esi" 85f2 0x0 (seq (set _res (& (var edx) (var esi))) (set _result (var _res)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test al, 0" f6c000 0x0 (seq (set _result (& (cast 8 false (var eax)) (bv 8 0x0))) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test byte [eax], 0" f60000 0x0 (seq (set _result (& (loadw 0 8 (+ (var eax) (bv 32 0x0))) (bv 8 0x0))) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test byte [eax], al" 8400 0x0 (seq (set _result (& (loadw 0 8 (+ (var eax) (bv 32 0x0))) (cast 8 false (var eax)))) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test dword [eax], 0" f70000000000 0x0 (seq (set _result (& (loadw 0 32 (+ (var eax) (bv 32 0x0))) (bv 32 0x0))) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test dword [eax], eax" 8500 0x0 (seq (set _result (& (loadw 0 32 (+ (var eax) (bv 32 0x0))) (var eax))) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test eax, 0" f7c000000000 0x0 (seq (set _result (& (var eax) (bv 32 0x0))) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test eax, ebx" 85d8 0x0 (seq (set _result (& (var eax) (var ebx))) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test edx, esi" 85f2 0x0 (seq (set _result (& (var edx) (var esi))) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
aB "ucomisd xmm0, qword [eax]" 660f2e00
aB "ucomiss xmm0, dword [eax]" 0f2e00
a "ud2" 0f0b

18
test/db/asm/x86_64
View file

@ -163,15 +163,15 @@ a "sub rax, rbx" 4829d8 0x0 (seq (set op1 (var rax)) (set op2 (var rbx)) (set su
a "sub r9, rbx" 4929d9 0x0 (seq (set op1 (var r9)) (set op2 (var rbx)) (set sub (- (var op1) (var op2))) (set r9 (cast 64 false (var sub))) (set _result (var sub)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set _result (var sub)) (set _x (var op1)) (set _y (var op2)) (set cf (|| (|| (&& (! (msb (var _x))) (msb (var _y))) (&& (msb (var _y)) (msb (var _result)))) (&& (msb (var _result)) (! (msb (var _x)))))) (set of (|| (&& (&& (! (msb (var _result))) (msb (var _x))) (! (msb (var _y)))) (&& (&& (msb (var _result)) (! (msb (var _x)))) (msb (var _y))))) (set af (|| (|| (&& (! (msb (cast 4 false (var _x)))) (msb (cast 4 false (var _y)))) (&& (msb (cast 4 false (var _y))) (msb (cast 4 false (var _result))))) (&& (msb (cast 4 false (var _result))) (! (msb (cast 4 false (var _x))))))))
a "sub rcx, r10" 4c29d1 0x0 (seq (set op1 (var rcx)) (set op2 (var r10)) (set sub (- (var op1) (var op2))) (set rcx (var sub)) (set _result (var sub)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set _result (var sub)) (set _x (var op1)) (set _y (var op2)) (set cf (|| (|| (&& (! (msb (var _x))) (msb (var _y))) (&& (msb (var _y)) (msb (var _result)))) (&& (msb (var _result)) (! (msb (var _x)))))) (set of (|| (&& (&& (! (msb (var _result))) (msb (var _x))) (! (msb (var _y)))) (&& (&& (msb (var _result)) (! (msb (var _x)))) (msb (var _y))))) (set af (|| (|| (&& (! (msb (cast 4 false (var _x)))) (msb (cast 4 false (var _y)))) (&& (msb (cast 4 false (var _y))) (msb (cast 4 false (var _result))))) (&& (msb (cast 4 false (var _result))) (! (msb (cast 4 false (var _x))))))))
a "sub r12, r11" 4d29dc 0x0 (seq (set op1 (var r12)) (set op2 (var r11)) (set sub (- (var op1) (var op2))) (set r12 (cast 64 false (var sub))) (set _result (var sub)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set _result (var sub)) (set _x (var op1)) (set _y (var op2)) (set cf (|| (|| (&& (! (msb (var _x))) (msb (var _y))) (&& (msb (var _y)) (msb (var _result)))) (&& (msb (var _result)) (! (msb (var _x)))))) (set of (|| (&& (&& (! (msb (var _result))) (msb (var _x))) (! (msb (var _y)))) (&& (&& (msb (var _result)) (! (msb (var _x)))) (msb (var _y))))) (set af (|| (|| (&& (! (msb (cast 4 false (var _x)))) (msb (cast 4 false (var _y)))) (&& (msb (cast 4 false (var _y))) (msb (cast 4 false (var _result))))) (&& (msb (cast 4 false (var _result))) (! (msb (cast 4 false (var _x))))))))
a "test ebx, 0x12345678" f7c378563412 0x0 (seq (set _res (& (cast 32 false (var rbx)) (bv 32 0x12345678))) (set _result (var _res)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test rbx, 0x12345678" 48f7c378563412 0x0 (seq (set _res (& (var rbx) (bv 64 0x12345678))) (set _result (var _res)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test dword [eax], 0x12345678" 67f70078563412 0x0 (seq (set _res (& (loadw 0 32 (+ (cast 64 false (cast 32 false (var rax))) (bv 64 0x0))) (bv 32 0x12345678))) (set _result (var _res)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test dword [rax], 0x12345678" f70078563412 0x0 (seq (set _res (& (loadw 0 32 (+ (var rax) (bv 64 0x0))) (bv 32 0x12345678))) (set _result (var _res)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test qword [rcx], 0x12345678" 48f70178563412 0x0 (seq (set _res (& (loadw 0 64 (+ (var rcx) (bv 64 0x0))) (bv 64 0x12345678))) (set _result (var _res)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test rax, rbx" 4885d8 0x0 (seq (set _res (& (var rax) (var rbx))) (set _result (var _res)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test rcx, rcx" 4885c9 0x0 (seq (set _res (& (var rcx) (var rcx))) (set _result (var _res)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test rdx, rsi" 4885f2 0x0 (seq (set _res (& (var rdx) (var rsi))) (set _result (var _res)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test r8, r8" 4d85c0 0x0 (seq (set _res (& (var r8) (var r8))) (set _result (var _res)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test ebx, 0x12345678" f7c378563412 0x0 (seq (set _result (& (cast 32 false (var rbx)) (bv 32 0x12345678))) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test rbx, 0x12345678" 48f7c378563412 0x0 (seq (set _result (& (var rbx) (bv 64 0x12345678))) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test dword [eax], 0x12345678" 67f70078563412 0x0 (seq (set _result (& (loadw 0 32 (+ (cast 64 false (cast 32 false (var rax))) (bv 64 0x0))) (bv 32 0x12345678))) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test dword [rax], 0x12345678" f70078563412 0x0 (seq (set _result (& (loadw 0 32 (+ (var rax) (bv 64 0x0))) (bv 32 0x12345678))) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test qword [rcx], 0x12345678" 48f70178563412 0x0 (seq (set _result (& (loadw 0 64 (+ (var rcx) (bv 64 0x0))) (bv 64 0x12345678))) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test rax, rbx" 4885d8 0x0 (seq (set _result (& (var rax) (var rbx))) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test rcx, rcx" 4885c9 0x0 (seq (set _result (& (var rcx) (var rcx))) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test rdx, rsi" 4885f2 0x0 (seq (set _result (& (var rdx) (var rsi))) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "test r8, r8" 4d85c0 0x0 (seq (set _result (& (var r8) (var r8))) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set cf false) (set of false))
a "xor [rax], rax" 483100 0x0 (seq (set _xor (^ (loadw 0 64 (+ (var rax) (bv 64 0x0))) (var rax))) (storew 0 (+ (var rax) (bv 64 0x0)) (var _xor)) (set of false) (set cf false) (set _result (var _xor)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))))
a "xor [rsi], rbx" 48311e 0x0 (seq (set _xor (^ (loadw 0 64 (+ (var rsi) (bv 64 0x0))) (var rbx))) (storew 0 (+ (var rsi) (bv 64 0x0)) (var _xor)) (set of false) (set cf false) (set _result (var _xor)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))))
a "xor rax, rax" 4831c0 0x0 (seq (set _xor (^ (var rax) (var rax))) (set rax (var _xor)) (set of false) (set cf false) (set _result (var _xor)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))))