From 2f6f2cfdce8a7777a1d4c9db675cd8211337a8fa Mon Sep 17 00:00:00 2001 From: Dhruv Maroo Date: Sun, 11 Jun 2023 23:08:40 +0800 Subject: [PATCH] Fix ROR and update instruction asm tests --- librz/analysis/arch/x86/x86_il.c | 2 +- test/db/asm/x86_16 | 10 +- test/db/asm/x86_32 | 176 ++++++++++++++--------------- test/db/asm/x86_64 | 184 +++++++++++++++---------------- 4 files changed, 186 insertions(+), 186 deletions(-) diff --git a/librz/analysis/arch/x86/x86_il.c b/librz/analysis/arch/x86/x86_il.c index 92796cdd0e..b912f41f70 100644 --- a/librz/analysis/arch/x86/x86_il.c +++ b/librz/analysis/arch/x86/x86_il.c @@ -3089,7 +3089,7 @@ IL_LIFTER(rcr) { } \ RzILOpEffect *count = SETL("_cnt", x86_il_get_op(1)); \ RzILOpEffect *masked = SETL("_masked", LOGAND(VARL("_cnt_mask"), VARL("_cnt"))); \ - RzILOpEffect *temp_count = SETL("_tmp_cnt", MOD(VARL("_masked"), UN(size, BITS_PER_BYTE * size))); + RzILOpEffect *temp_count = SETL("_tmp_cnt", MOD(VARL("_masked"), UN(cnt_size, BITS_PER_BYTE * size))); /** * ROL diff --git a/test/db/asm/x86_16 b/test/db/asm/x86_16 index 114da834dd..d46d8d5dc0 100644 --- a/test/db/asm/x86_16 +++ b/test/db/asm/x86_16 @@ -5,8 +5,8 @@ ad "aam" d40a 0x0 (seq (set temp_al (cast 8 false (var ax))) (set ax (| (& (var ad "aam 0x42" d442 0x0 (seq (set temp_al (cast 8 false (var ax))) (set ax (| (& (var ax) (~ (bv 16 0xff00))) (<< (cast 16 false (div (var temp_al) (bv 8 0x42))) (bv 8 0x8) false))) (set adjusted (mod (var temp_al) (bv 8 0x42))) (set ax (| (& (var ax) (~ (bv 16 0xff))) (cast 16 false (var adjusted)))) (set _result (var adjusted)) (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)))) ad "aas" 3f 0x0 (seq (branch (|| (! (ule (& (cast 8 false (var ax)) (bv 8 0xf)) (bv 8 0x9))) (var af)) (seq (set ax (- (var ax) (bv 16 0x6))) (set ax (| (& (var ax) (~ (bv 16 0xff00))) (<< (cast 16 false (- (cast 8 false (>> (var ax) (bv 8 0x8) false)) (bv 8 0x1))) (bv 8 0x8) false))) (set af true) (set cf true)) (seq (set af false) (set cf false))) (set ax (| (& (var ax) (~ (bv 16 0xff))) (cast 16 false (& (cast 8 false (var ax)) (bv 8 0xf)))))) adB "cbw" 98 -d "call 0" e8fdff 0x0 (seq (set _cs (cast 16 false (var cs))) (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 _cs))) (set _pc (bv 16 0x3)) (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 _pc))) (jmp (bv 16 0x0))) -d "enter 8, 0" c8080000 0x0 (seq (set _alloc_sz (cast 16 false (bv 16 0x8))) (set _nest_lvl (mod (cast 8 false (bv 16 0x0)) (bv 8 0x20))) (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 _frame_tmp (var sp)) (branch (is_zero (var _nest_lvl)) nop (seq (branch (! (ule (var _nest_lvl) (bv 8 0x1))) (seq (set _itr (bv 8 0x1)) (repeat (&& (ule (var _itr) (var _nest_lvl)) (! (== (var _itr) (var _nest_lvl)))) (seq (set bp (- (var bp) (bv 16 0x2))) (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 (loadw 0 16 (var bp)))) (set _itr (+ (var _itr) (bv 8 0x1)))))) nop) (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 _frame_tmp))))) (set sp (- (var sp) (cast 16 false (var _alloc_sz)))) (set bp (cast 16 false (cast 15 false (var _frame_tmp))))) +d "call 0" e8fdff 0x0 (seq (set _cs (cast 16 false (var cs))) (set final (- (var sp) (bv 16 0x2))) (storew 0 (var final) (cast 16 false (var _cs))) (set sp (var final)) (set _pc (bv 16 0x3)) (set final (- (var sp) (bv 16 0x2))) (storew 0 (var final) (cast 16 false (var _pc))) (set sp (var final)) (jmp (bv 16 0x0))) +d "enter 8, 0" c8080000 0x0 (seq (set _alloc_sz (cast 16 false (bv 16 0x8))) (set _nest_lvl (mod (cast 8 false (bv 16 0x0)) (bv 8 0x20))) (set final (- (var sp) (bv 16 0x2))) (storew 0 (var final) (cast 16 false (var bp))) (set sp (var final)) (set _frame_tmp (var sp)) (branch (is_zero (var _nest_lvl)) nop (seq (branch (! (ule (var _nest_lvl) (bv 8 0x1))) (seq (set _itr (bv 8 0x1)) (repeat (&& (ule (var _itr) (var _nest_lvl)) (! (== (var _itr) (var _nest_lvl)))) (seq (set bp (- (var bp) (bv 16 0x2))) (set final (- (var sp) (bv 16 0x2))) (storew 0 (var final) (cast 16 false (loadw 0 16 (var bp)))) (set sp (var final)) (set _itr (+ (var _itr) (bv 8 0x1)))))) nop) (set final (- (var sp) (bv 16 0x2))) (storew 0 (var final) (cast 16 false (var _frame_tmp))) (set sp (var final)))) (set sp (- (var sp) (cast 16 false (var _alloc_sz)))) (set bp (cast 16 false (cast 15 false (var _frame_tmp))))) a "jmp 0x0" ebfe 0x0 (jmp (cast 16 false (bv 16 0x0))) a "jmp 0x10" eb0e 0x0 (jmp (cast 16 false (bv 16 0x10))) a "jmp 0x34" eb32 0x0 (jmp (cast 16 false (bv 16 0x34))) @@ -21,9 +21,9 @@ ad "loop 0xff92" e290 0x0 (seq (set cx (- (var cx) (bv 16 0x1))) (branch (! (is_ a "mov al, [0xbeef]" a0efbe 0x0 (set ax (| (& (var ax) (~ (bv 16 0xff))) (cast 16 false (loadw 0 8 (bv 16 0xbeef))))) a "mov ax, [0xbeef]" a1efbe 0x0 (set ax (loadw 0 16 (bv 16 0xbeef))) d "popf" 9d 0x0 (seq (set _flags (loadw 0 16 (+ (+ (cast 16 false (var sp)) (bv 16 0x0)) (<< (cast 16 false (var ss)) (bv 8 0x4) false)))) (set cf (lsb (var _flags))) (set _flags (>> (var _flags) (bv 8 0x2) false)) (set pf (lsb (var _flags))) (set _flags (>> (var _flags) (bv 8 0x2) false)) (set af (lsb (var _flags))) (set _flags (>> (var _flags) (bv 8 0x2) false)) (set zf (lsb (var _flags))) (set _flags (>> (var _flags) (bv 8 0x1) false)) (set sf (lsb (var _flags))) (set _flags (>> (var _flags) (bv 8 0x1) false)) (set tf (lsb (var _flags))) (set _flags (>> (var _flags) (bv 8 0x1) false)) (set if (lsb (var _flags))) (set _flags (>> (var _flags) (bv 8 0x1) false)) (set df (lsb (var _flags))) (set _flags (>> (var _flags) (bv 8 0x1) false)) (set of (lsb (var _flags))) (set _flags (>> (var _flags) (bv 8 0x3) false)) (set nt (lsb (var _flags))) (set sp (+ (var sp) (bv 16 0x2)))) -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)))) +ad "push ax" 50 0x0 (seq (set final (- (var sp) (bv 16 0x4))) (storew 0 (var final) (cast 16 false (var ax))) (set sp (var final))) +d "pushf" 9c 0x0 (seq (set final (- (var sp) (bv 16 0x2))) (storew 0 (var final) (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))))) (set sp (var final))) +d "pushaw" 60 0x0 (seq (set _sp (var sp)) (set final (- (var sp) (bv 16 0x2))) (storew 0 (var final) (cast 16 false (var ax))) (set sp (var final)) (set final (- (var sp) (bv 16 0x2))) (storew 0 (var final) (cast 16 false (var cx))) (set sp (var final)) (set final (- (var sp) (bv 16 0x2))) (storew 0 (var final) (cast 16 false (var dx))) (set sp (var final)) (set final (- (var sp) (bv 16 0x2))) (storew 0 (var final) (cast 16 false (var bx))) (set sp (var final)) (set final (- (var sp) (bv 16 0x2))) (storew 0 (var final) (cast 16 false (var _sp))) (set sp (var final)) (set final (- (var sp) (bv 16 0x2))) (storew 0 (var final) (cast 16 false (var bp))) (set sp (var final)) (set final (- (var sp) (bv 16 0x2))) (storew 0 (var final) (cast 16 false (var si))) (set sp (var final)) (set final (- (var sp) (bv 16 0x2))) (storew 0 (var final) (cast 16 false (var di))) (set sp (var final))) 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 diff --git a/test/db/asm/x86_32 b/test/db/asm/x86_32 index d024d84f37..2c116eb996 100644 --- a/test/db/asm/x86_32 +++ b/test/db/asm/x86_32 @@ -1,4 +1,4 @@ -d "lea edx, [0x2c4b]" 8d154b2c0000 0x0 (set edx (bv 32 0x2c4b)) +d "lea edx, [0x2c4b]" 8d154b2c0000 0x0 (set edx (cast 32 false (bv 32 0x2c4b))) d "aaa" 37 0x0 (seq (branch (|| (! (ule (& (cast 8 false (var eax)) (bv 8 0xf)) (bv 8 0x9))) (var af)) (seq (set eax (| (& (var eax) (~ (bv 32 0xffff))) (cast 32 false (+ (cast 16 false (var eax)) (bv 16 0x106))))) (set af true) (set cf true)) (seq (set af false) (set cf false))) (set eax (| (& (var eax) (~ (bv 32 0xff))) (cast 32 false (& (cast 8 false (var eax)) (bv 8 0xf)))))) d "aad" d50a 0x0 (seq (set temp_al (cast 8 false (var eax))) (set temp_ah (cast 8 false (>> (var eax) (bv 8 0x8) false))) (set adjusted (& (+ (var temp_al) (* (var temp_ah) (bv 8 0xa))) (bv 8 0xff))) (set eax (| (& (var eax) (~ (bv 32 0xff))) (cast 32 false (var adjusted)))) (set eax (| (& (var eax) (~ (bv 32 0xff00))) (<< (cast 32 false (bv 8 0x0)) (bv 8 0x8) false))) (set _result (var adjusted)) (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)))) d "aad 0x69" d569 0x0 (seq (set temp_al (cast 8 false (var eax))) (set temp_ah (cast 8 false (>> (var eax) (bv 8 0x8) false))) (set adjusted (& (+ (var temp_al) (* (var temp_ah) (bv 8 0x69))) (bv 8 0xff))) (set eax (| (& (var eax) (~ (bv 32 0xff))) (cast 32 false (var adjusted)))) (set eax (| (& (var eax) (~ (bv 32 0xff00))) (<< (cast 32 false (bv 8 0x0)) (bv 8 0x8) false))) (set _result (var adjusted)) (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)))) @@ -137,8 +137,8 @@ d "divsd xmm0, qword [eax]" f20f5e00 d "divss xmm0, dword [eax]" f30f5e00 d "emms" 0f77 ad "endbr32" f30f1efb -d "enter 2, 0" c8020000 0x0 (seq (set _alloc_sz (cast 16 false (bv 32 0x2))) (set _nest_lvl (mod (cast 8 false (bv 32 0x0)) (bv 8 0x20))) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var ebp))) (set _frame_tmp (var esp)) (branch (is_zero (var _nest_lvl)) nop (seq (branch (! (ule (var _nest_lvl) (bv 8 0x1))) (seq (set _itr (bv 8 0x1)) (repeat (&& (ule (var _itr) (var _nest_lvl)) (! (== (var _itr) (var _nest_lvl)))) (seq (set ebp (- (var ebp) (bv 32 0x4))) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (loadw 0 32 (var ebp)))) (set _itr (+ (var _itr) (bv 8 0x1)))))) nop) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var _frame_tmp))))) (set esp (- (var esp) (cast 32 false (var _alloc_sz)))) (set ebp (var _frame_tmp))) -d "enter 8, 0" 66c8080000 0x0 (seq (set _alloc_sz (cast 16 false (bv 16 0x8))) (set _nest_lvl (mod (cast 8 false (bv 16 0x0)) (bv 8 0x20))) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 16 false (cast 16 false (var ebp)))) (set _frame_tmp (var esp)) (branch (is_zero (var _nest_lvl)) nop (seq (branch (! (ule (var _nest_lvl) (bv 8 0x1))) (seq (set _itr (bv 8 0x1)) (repeat (&& (ule (var _itr) (var _nest_lvl)) (! (== (var _itr) (var _nest_lvl)))) (seq (set ebp (- (var ebp) (bv 32 0x2))) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 16 false (loadw 0 16 (var ebp)))) (set _itr (+ (var _itr) (bv 8 0x1)))))) nop) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 16 false (var _frame_tmp))))) (set esp (- (var esp) (cast 32 false (var _alloc_sz)))) (set ebp (| (& (var ebp) (~ (bv 32 0xffff))) (cast 32 false (cast 16 false (cast 15 false (var _frame_tmp))))))) +d "enter 2, 0" c8020000 0x0 (seq (set _alloc_sz (cast 16 false (bv 32 0x2))) (set _nest_lvl (mod (cast 8 false (bv 32 0x0)) (bv 8 0x20))) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var ebp))) (set esp (var final)) (set _frame_tmp (var esp)) (branch (is_zero (var _nest_lvl)) nop (seq (branch (! (ule (var _nest_lvl) (bv 8 0x1))) (seq (set _itr (bv 8 0x1)) (repeat (&& (ule (var _itr) (var _nest_lvl)) (! (== (var _itr) (var _nest_lvl)))) (seq (set ebp (- (var ebp) (bv 32 0x4))) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (loadw 0 32 (var ebp)))) (set esp (var final)) (set _itr (+ (var _itr) (bv 8 0x1)))))) nop) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var _frame_tmp))) (set esp (var final)))) (set esp (- (var esp) (cast 32 false (var _alloc_sz)))) (set ebp (var _frame_tmp))) +d "enter 8, 0" 66c8080000 0x0 (seq (set _alloc_sz (cast 16 false (bv 16 0x8))) (set _nest_lvl (mod (cast 8 false (bv 16 0x0)) (bv 8 0x20))) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 16 false (cast 16 false (var ebp)))) (set esp (var final)) (set _frame_tmp (var esp)) (branch (is_zero (var _nest_lvl)) nop (seq (branch (! (ule (var _nest_lvl) (bv 8 0x1))) (seq (set _itr (bv 8 0x1)) (repeat (&& (ule (var _itr) (var _nest_lvl)) (! (== (var _itr) (var _nest_lvl)))) (seq (set ebp (- (var ebp) (bv 32 0x2))) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 16 false (loadw 0 16 (var ebp)))) (set esp (var final)) (set _itr (+ (var _itr) (bv 8 0x1)))))) nop) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 16 false (var _frame_tmp))) (set esp (var final)))) (set esp (- (var esp) (cast 32 false (var _alloc_sz)))) (set ebp (| (& (var ebp) (~ (bv 32 0xffff))) (cast 32 false (cast 16 false (cast 15 false (var _frame_tmp))))))) d "femms" 0f0e d "fxrstor [eax]" 0fae08 d "fxsave [eax]" 0fae00 @@ -224,7 +224,7 @@ d "lcall [eax]" ff18 d "lddqu xmm0, xmmword [eax]" f20ff000 d "ldmxcsr dword [eax]" 0fae10 d "lds eax, [eax]" c500 0x0 (set eax (+ (+ (var eax) (bv 32 0x0)) (<< (cast 32 false (var ds)) (bv 8 0x4) false))) -d "lea eax, [eax]" 8d00 0x0 (set eax (+ (var eax) (bv 32 0x0))) +d "lea eax, [eax]" 8d00 0x0 (set eax (cast 32 false (+ (var eax) (bv 32 0x0)))) ad "leave" c9 0x0 (seq (set esp (var ebp)) (set esp (+ (var esp) (bv 32 0x4))) (set ebp (loadw 0 32 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false))))) d "leave" 66c9 0x0 (seq (set esp (var ebp)) (set esp (+ (var esp) (bv 32 0x2))) (set ebp (| (& (var ebp) (~ (bv 32 0xffff))) (cast 32 false (loadw 0 16 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false))))))) d "les eax, [eax]" c400 0x0 (set eax (+ (+ (var eax) (bv 32 0x0)) (<< (cast 32 false (var es)) (bv 8 0x4) false))) @@ -406,24 +406,24 @@ d "psubusb mm0, qword [eax]" 0fd800 d "psubusw mm0, qword [eax]" 0fd900 d "punpckhqdq xmm0, xmmword [eax]" 660f6d00 d "punpcklqdq xmm0, xmmword [eax]" 660f6c00 -d "push 0" 6a00 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (bv 32 0x0)))) -d "push cs" 0e 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var cs)))) -d "push ds" 1e 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var ds)))) -d "push dword [eax]" ff30 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (loadw 0 32 (+ (var eax) (bv 32 0x0)))))) -d "push eax" 50 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var eax)))) -d "push ebp" 55 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var ebp)))) -d "push ebx" 53 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var ebx)))) -d "push ecx" 51 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var ecx)))) -d "push edi" 57 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var edi)))) -d "push edx" 52 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var edx)))) -d "push es" 06 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var es)))) -d "push esi" 56 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var esi)))) -d "push esp" 54 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var esp)))) -d "push fs" 0fa0 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var fs)))) -d "push gs" 0fa8 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var gs)))) -d "push ss" 16 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var ss)))) -d "pushal" 60 0x0 (seq (set _esp (var esp)) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var eax))) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var ecx))) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var edx))) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var ebx))) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var _esp))) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var ebp))) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var esi))) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var edi)))) -d "pushfd" 9c 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (ite false (bv 32 0x1) (bv 32 0x0)) (bv 32 0x1) false) (ite (var nt) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x2) false) (bv 32 0x3)) (bv 32 0x1) false) (ite (var of) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x1) false) (ite (var df) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x1) false) (ite (var if) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x1) false) (ite (var tf) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x1) false) (ite (var zf) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x1) false) (ite (var zf) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x2) false) (ite (var af) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x2) false) (ite (var pf) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x1) false) (bv 32 0x1)) (bv 32 0x1) false) (ite (var cf) (bv 32 0x1) (bv 32 0x0)))))) +d "push 0" 6a00 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (bv 32 0x0))) (set esp (var final))) +d "push cs" 0e 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var cs))) (set esp (var final))) +d "push ds" 1e 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var ds))) (set esp (var final))) +d "push dword [eax]" ff30 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (loadw 0 32 (+ (var eax) (bv 32 0x0))))) (set esp (var final))) +d "push eax" 50 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var eax))) (set esp (var final))) +d "push ebp" 55 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var ebp))) (set esp (var final))) +d "push ebx" 53 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var ebx))) (set esp (var final))) +d "push ecx" 51 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var ecx))) (set esp (var final))) +d "push edi" 57 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var edi))) (set esp (var final))) +d "push edx" 52 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var edx))) (set esp (var final))) +d "push es" 06 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var es))) (set esp (var final))) +d "push esi" 56 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var esi))) (set esp (var final))) +d "push esp" 54 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var esp))) (set esp (var final))) +d "push fs" 0fa0 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var fs))) (set esp (var final))) +d "push gs" 0fa8 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var gs))) (set esp (var final))) +d "push ss" 16 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var ss))) (set esp (var final))) +d "pushal" 60 0x0 (seq (set _esp (var esp)) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var eax))) (set esp (var final)) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var ecx))) (set esp (var final)) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var edx))) (set esp (var final)) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var ebx))) (set esp (var final)) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var _esp))) (set esp (var final)) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var ebp))) (set esp (var final)) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var esi))) (set esp (var final)) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var edi))) (set esp (var final))) +d "pushfd" 9c 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (ite false (bv 32 0x1) (bv 32 0x0)) (bv 32 0x1) false) (ite (var nt) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x2) false) (bv 32 0x3)) (bv 32 0x1) false) (ite (var of) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x1) false) (ite (var df) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x1) false) (ite (var if) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x1) false) (ite (var tf) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x1) false) (ite (var zf) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x1) false) (ite (var zf) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x2) false) (ite (var af) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x2) false) (ite (var pf) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x1) false) (bv 32 0x1)) (bv 32 0x1) false) (ite (var cf) (bv 32 0x1) (bv 32 0x0))))) (set esp (var final))) d "pxor mm0, qword [eax]" 0fef00 d "rdmsr" 0f32 d "rdpmc" 0f33 @@ -1063,11 +1063,11 @@ aB "bt edx, 59" 0fbae23b aB "bt ebp, -20" 0fbae5e0 aB "btr dword [eax], eax" 0fb300 aB "bts dword [eax], eax" 0fab00 -a "call 0x8049100" e8fb900408 0x0 (seq (set _cs (cast 32 false (var cs))) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var _cs))) (set _pc (bv 32 0x5)) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var _pc))) (jmp (bv 32 0x8049100))) -a "call 4" e8ffffffff 0x0 (seq (set _cs (cast 32 false (var cs))) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var _cs))) (set _pc (bv 32 0x5)) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var _pc))) (jmp (bv 32 0x4))) -a "call 5" e800000000 0x0 (seq (set _cs (cast 32 false (var cs))) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var _cs))) (set _pc (bv 32 0x5)) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var _pc))) (jmp (bv 32 0x5))) -a "call dword [eax]" ff10 0x0 (seq (set _cs (cast 32 false (var cs))) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var _cs))) (set _pc (bv 32 0x2)) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var _pc))) (jmp (loadw 0 32 (+ (var eax) (bv 32 0x0))))) -a "call ebx" ffd3 0x0 (seq (set _cs (cast 32 false (var cs))) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var _cs))) (set _pc (bv 32 0x2)) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var _pc))) (jmp (var ebx))) +a "call 0x8049100" e8fb900408 0x0 (seq (set _cs (cast 32 false (var cs))) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var _cs))) (set esp (var final)) (set _pc (bv 32 0x5)) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var _pc))) (set esp (var final)) (jmp (bv 32 0x8049100))) +a "call 4" e8ffffffff 0x0 (seq (set _cs (cast 32 false (var cs))) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var _cs))) (set esp (var final)) (set _pc (bv 32 0x5)) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var _pc))) (set esp (var final)) (jmp (bv 32 0x4))) +a "call 5" e800000000 0x0 (seq (set _cs (cast 32 false (var cs))) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var _cs))) (set esp (var final)) (set _pc (bv 32 0x5)) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var _pc))) (set esp (var final)) (jmp (bv 32 0x5))) +a "call dword [eax]" ff10 0x0 (seq (set _cs (cast 32 false (var cs))) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var _cs))) (set esp (var final)) (set _pc (bv 32 0x2)) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var _pc))) (set esp (var final)) (jmp (loadw 0 32 (+ (var eax) (bv 32 0x0))))) +a "call ebx" ffd3 0x0 (seq (set _cs (cast 32 false (var cs))) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var _cs))) (set esp (var final)) (set _pc (bv 32 0x2)) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var _pc))) (set esp (var final)) (jmp (var ebx))) a "bnd call ebx" f2ffd3 a "cbw" 6698 a "cdq" 99 @@ -1376,21 +1376,21 @@ aB "lcall [eax]" ff18 aB "lddqu xmm0, xmmword [eax]" f20ff000 aB "ldmxcsr [eax]" 0fae10 aB "lds eax, [eax]" c500 -a "lea eax, [4]" 8d0504000000 0x0 (set eax (bv 32 0x4)) -a "lea eax, [eax+4]" 8d4004 0x0 (set eax (+ (var eax) (bv 32 0x4))) -a "lea eax, [eax]" 8d00 0x0 (set eax (+ (var eax) (bv 32 0x0))) -a "lea eax, [ebp+24]" 8d4518 0x0 (set eax (+ (var ebp) (bv 32 0x18))) -a "lea eax, [ebx+24]" 8d4318 0x0 (set eax (+ (var ebx) (bv 32 0x18))) -a "lea eax, [ebx+4]" 8d4304 0x0 (set eax (+ (var ebx) (bv 32 0x4))) -a "lea eax, [ecx]" 8d01 0x0 (set eax (+ (var ecx) (bv 32 0x0))) -a "lea eax, [esp]" 8d0424 0x0 (set eax (+ (var esp) (bv 32 0x0))) -a "lea ebx, [4]" 8d1d04000000 0x0 (set ebx (bv 32 0x4)) -a "lea ebx, [eax+24]" 8d5818 0x0 (set ebx (+ (var eax) (bv 32 0x18))) -a "lea ebx, [eax+4]" 8d5804 0x0 (set ebx (+ (var eax) (bv 32 0x4))) -a "lea ebx, [ebp+324]" 8d9d44010000 0x0 (set ebx (+ (var ebp) (bv 32 0x144))) -a "lea ebx, [ebp]" 8d5d00 0x0 (set ebx (+ (var ebp) (bv 32 0x0))) -a "lea edx, [0x4422221d]" 8d151d222244 0x0 (set edx (bv 32 0x4422221d)) -a "lea edx, 0x2c4b" 8d154b2c0000 0x0 (set edx (bv 32 0x2c4b)) +a "lea eax, [4]" 8d0504000000 0x0 (set eax (cast 32 false (bv 32 0x4))) +a "lea eax, [eax+4]" 8d4004 0x0 (set eax (cast 32 false (+ (var eax) (bv 32 0x4)))) +a "lea eax, [eax]" 8d00 0x0 (set eax (cast 32 false (+ (var eax) (bv 32 0x0)))) +a "lea eax, [ebp+24]" 8d4518 0x0 (set eax (cast 32 false (+ (var ebp) (bv 32 0x18)))) +a "lea eax, [ebx+24]" 8d4318 0x0 (set eax (cast 32 false (+ (var ebx) (bv 32 0x18)))) +a "lea eax, [ebx+4]" 8d4304 0x0 (set eax (cast 32 false (+ (var ebx) (bv 32 0x4)))) +a "lea eax, [ecx]" 8d01 0x0 (set eax (cast 32 false (+ (var ecx) (bv 32 0x0)))) +a "lea eax, [esp]" 8d0424 0x0 (set eax (cast 32 false (+ (var esp) (bv 32 0x0)))) +a "lea ebx, [4]" 8d1d04000000 0x0 (set ebx (cast 32 false (bv 32 0x4))) +a "lea ebx, [eax+24]" 8d5818 0x0 (set ebx (cast 32 false (+ (var eax) (bv 32 0x18)))) +a "lea ebx, [eax+4]" 8d5804 0x0 (set ebx (cast 32 false (+ (var eax) (bv 32 0x4)))) +a "lea ebx, [ebp+324]" 8d9d44010000 0x0 (set ebx (cast 32 false (+ (var ebp) (bv 32 0x144)))) +a "lea ebx, [ebp]" 8d5d00 0x0 (set ebx (cast 32 false (+ (var ebp) (bv 32 0x0)))) +a "lea edx, [0x4422221d]" 8d151d222244 0x0 (set edx (cast 32 false (bv 32 0x4422221d))) +a "lea edx, 0x2c4b" 8d154b2c0000 0x0 (set edx (cast 32 false (bv 32 0x2c4b))) a "les eax, [eax]" c400 0x0 (set eax (+ (+ (var eax) (bv 32 0x0)) (<< (cast 32 false (var es)) (bv 8 0x4) false))) a "les eax, [eax+12]" c4400c 0x0 (set eax (+ (+ (var eax) (bv 32 0xc)) (<< (cast 32 false (var es)) (bv 8 0x4) false))) a "les eax, [eax-233]" c48017ffffff 0x0 (set eax (+ (+ (var eax) (bv 32 0xffffff17)) (<< (cast 32 false (var es)) (bv 8 0x4) false))) @@ -1867,36 +1867,36 @@ aB "punpckldq xmm0, xmmword [eax]" 660f6200 aB "punpcklqdq xmm0, xmmword [eax]" 660f6c00 aB "punpcklwd mm0, qword [eax]" 0f6100 aB "punpcklwd xmm0, xmmword [eax]" 660f6100 -a "push 0" 6a00 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (bv 32 0x0)))) -a "pushal" 60 0x0 (seq (set _esp (var esp)) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var eax))) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var ecx))) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var edx))) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var ebx))) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var _esp))) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var ebp))) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var esi))) (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var edi)))) -a "push cs" 0e 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var cs)))) -a "push ds" 1e 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var ds)))) -a "push dword [eax+8]" ff7008 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (loadw 0 32 (+ (var eax) (bv 32 0x8)))))) -a "push dword [eax]" ff30 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (loadw 0 32 (+ (var eax) (bv 32 0x0)))))) -a "push dword [ebp+4]" ff7504 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (loadw 0 32 (+ (var ebp) (bv 32 0x4)))))) -a "push dword [ebp]" ff7500 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (loadw 0 32 (+ (var ebp) (bv 32 0x0)))))) -a "push dword [ebx+4]" ff7304 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (loadw 0 32 (+ (var ebx) (bv 32 0x4)))))) -a "push dword [ecx]" ff31 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (loadw 0 32 (+ (var ecx) (bv 32 0x0)))))) -a "push dword [edi]" ff37 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (loadw 0 32 (+ (var edi) (bv 32 0x0)))))) -a "push dword [esi+4]" ff7604 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (loadw 0 32 (+ (var esi) (bv 32 0x4)))))) -a "push dword [esi]" ff36 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (loadw 0 32 (+ (var esi) (bv 32 0x0)))))) -a "push dword [esp+4]" ff742404 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (loadw 0 32 (+ (var esp) (bv 32 0x4)))))) -a "push dword [esp]" ff3424 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (loadw 0 32 (+ (var esp) (bv 32 0x0)))))) -a "push [esp+4]" ff742404 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (loadw 0 32 (+ (var esp) (bv 32 0x4)))))) -a "push [esp]" ff3424 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (loadw 0 32 (+ (var esp) (bv 32 0x0)))))) -a "push eax" 50 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var eax)))) -a "push ebp" 55 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var ebp)))) -a "push ebx" 53 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var ebx)))) -a "push ecx" 51 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var ecx)))) -a "push edi" 57 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var edi)))) -a "push edx" 52 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var edx)))) -a "push es" 06 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var es)))) -a "push esi" 56 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var esi)))) -a "push esp" 54 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var esp)))) -a "pushfd" 9c 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (ite false (bv 32 0x1) (bv 32 0x0)) (bv 32 0x1) false) (ite (var nt) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x2) false) (bv 32 0x3)) (bv 32 0x1) false) (ite (var of) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x1) false) (ite (var df) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x1) false) (ite (var if) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x1) false) (ite (var tf) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x1) false) (ite (var zf) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x1) false) (ite (var zf) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x2) false) (ite (var af) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x2) false) (ite (var pf) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x1) false) (bv 32 0x1)) (bv 32 0x1) false) (ite (var cf) (bv 32 0x1) (bv 32 0x0)))))) -a "push fs" 0fa0 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var fs)))) -a "push gs" 0fa8 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var gs)))) -a "push ss" 16 0x0 (seq (set esp (- (var esp) (bv 32 0x4))) (storew 0 (+ (+ (cast 32 false (var esp)) (bv 32 0x0)) (<< (cast 32 false (var ss)) (bv 8 0x4) false)) (cast 32 false (var ss)))) +a "push 0" 6a00 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (bv 32 0x0))) (set esp (var final))) +a "pushal" 60 0x0 (seq (set _esp (var esp)) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var eax))) (set esp (var final)) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var ecx))) (set esp (var final)) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var edx))) (set esp (var final)) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var ebx))) (set esp (var final)) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var _esp))) (set esp (var final)) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var ebp))) (set esp (var final)) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var esi))) (set esp (var final)) (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var edi))) (set esp (var final))) +a "push cs" 0e 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var cs))) (set esp (var final))) +a "push ds" 1e 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var ds))) (set esp (var final))) +a "push dword [eax+8]" ff7008 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (loadw 0 32 (+ (var eax) (bv 32 0x8))))) (set esp (var final))) +a "push dword [eax]" ff30 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (loadw 0 32 (+ (var eax) (bv 32 0x0))))) (set esp (var final))) +a "push dword [ebp+4]" ff7504 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (loadw 0 32 (+ (var ebp) (bv 32 0x4))))) (set esp (var final))) +a "push dword [ebp]" ff7500 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (loadw 0 32 (+ (var ebp) (bv 32 0x0))))) (set esp (var final))) +a "push dword [ebx+4]" ff7304 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (loadw 0 32 (+ (var ebx) (bv 32 0x4))))) (set esp (var final))) +a "push dword [ecx]" ff31 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (loadw 0 32 (+ (var ecx) (bv 32 0x0))))) (set esp (var final))) +a "push dword [edi]" ff37 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (loadw 0 32 (+ (var edi) (bv 32 0x0))))) (set esp (var final))) +a "push dword [esi+4]" ff7604 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (loadw 0 32 (+ (var esi) (bv 32 0x4))))) (set esp (var final))) +a "push dword [esi]" ff36 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (loadw 0 32 (+ (var esi) (bv 32 0x0))))) (set esp (var final))) +a "push dword [esp+4]" ff742404 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (loadw 0 32 (+ (var esp) (bv 32 0x4))))) (set esp (var final))) +a "push dword [esp]" ff3424 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (loadw 0 32 (+ (var esp) (bv 32 0x0))))) (set esp (var final))) +a "push [esp+4]" ff742404 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (loadw 0 32 (+ (var esp) (bv 32 0x4))))) (set esp (var final))) +a "push [esp]" ff3424 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (loadw 0 32 (+ (var esp) (bv 32 0x0))))) (set esp (var final))) +a "push eax" 50 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var eax))) (set esp (var final))) +a "push ebp" 55 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var ebp))) (set esp (var final))) +a "push ebx" 53 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var ebx))) (set esp (var final))) +a "push ecx" 51 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var ecx))) (set esp (var final))) +a "push edi" 57 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var edi))) (set esp (var final))) +a "push edx" 52 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var edx))) (set esp (var final))) +a "push es" 06 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var es))) (set esp (var final))) +a "push esi" 56 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var esi))) (set esp (var final))) +a "push esp" 54 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var esp))) (set esp (var final))) +a "pushfd" 9c 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (ite false (bv 32 0x1) (bv 32 0x0)) (bv 32 0x1) false) (ite (var nt) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x2) false) (bv 32 0x3)) (bv 32 0x1) false) (ite (var of) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x1) false) (ite (var df) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x1) false) (ite (var if) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x1) false) (ite (var tf) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x1) false) (ite (var zf) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x1) false) (ite (var zf) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x2) false) (ite (var af) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x2) false) (ite (var pf) (bv 32 0x1) (bv 32 0x0))) (bv 32 0x1) false) (bv 32 0x1)) (bv 32 0x1) false) (ite (var cf) (bv 32 0x1) (bv 32 0x0))))) (set esp (var final))) +a "push fs" 0fa0 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var fs))) (set esp (var final))) +a "push gs" 0fa8 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var gs))) (set esp (var final))) +a "push ss" 16 0x0 (seq (set final (- (var esp) (bv 32 0x4))) (storew 0 (var final) (cast 32 false (var ss))) (set esp (var final))) aB "pxor mm0, qword [eax]" 0fef00 aB "pxor xmm0, xmmword [eax]" 660fef00 aB "rcpps xmm0, xmmword [eax]" 0f5300 @@ -1921,18 +1921,18 @@ ad "rcr byte [eax], cl" d218 0x0 (seq (set _dest (loadw 0 8 (+ (var eax) (bv 32 ad "rcr byte [eax], 1" d018 0x0 (seq (set _dest (loadw 0 8 (+ (var eax) (bv 32 0x0)))) (set _tmp_cnt (mod (cast 5 false (bv 8 0x1)) (bv 5 0x9))) (set _cnt_mask (cast 5 false (bv 8 0x1))) (branch (== (var _cnt_mask) (bv 5 0x1)) (set of (^^ (msb (var _dest)) (var cf))) nop) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (lsb (var _dest))) (set _dest (+ (>> (var _dest) (bv 8 0x1) false) (<< (ite (var cf) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false))) (set cf (var _tmp_cf)) (set _tmp_cnt (- (var _tmp_cnt) (bv 5 0x1))))) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) ad "rcr dword [eax], cl" d318 0x0 (seq (set _dest (loadw 0 32 (+ (var eax) (bv 32 0x0)))) (set _tmp_cnt (cast 5 false (cast 8 false (var ecx)))) (set _cnt_mask (cast 5 false (cast 8 false (var ecx)))) (branch (== (var _cnt_mask) (bv 5 0x1)) (set of (^^ (msb (var _dest)) (var cf))) nop) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (lsb (var _dest))) (set _dest (+ (>> (var _dest) (bv 8 0x1) false) (<< (ite (var cf) (bv 32 0x1) (bv 32 0x0)) (bv 8 0x4) false))) (set cf (var _tmp_cf)) (set _tmp_cnt (- (var _tmp_cnt) (bv 5 0x1))))) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) ad "rcr dword [eax], 1" d118 0x0 (seq (set _dest (loadw 0 32 (+ (var eax) (bv 32 0x0)))) (set _tmp_cnt (cast 5 false (bv 32 0x1))) (set _cnt_mask (cast 5 false (bv 32 0x1))) (branch (== (var _cnt_mask) (bv 5 0x1)) (set of (^^ (msb (var _dest)) (var cf))) nop) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (lsb (var _dest))) (set _dest (+ (>> (var _dest) (bv 8 0x1) false) (<< (ite (var cf) (bv 32 0x1) (bv 32 0x0)) (bv 8 0x4) false))) (set cf (var _tmp_cf)) (set _tmp_cnt (- (var _tmp_cnt) (bv 5 0x1))))) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) -ad "rol byte [eax], 0" c00000 0x0 (seq (set _dest (loadw 0 8 (+ (var eax) (bv 32 0x0)))) (set _cnt_mask (bv 8 0x1f)) (set _cnt (bv 8 0x0)) (set _masked (& (var _cnt_mask) (var _cnt))) (set _tmp_cnt (mod (var _masked) (bv 8 0x1))) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (msb (var _dest))) (set _dest (+ (<< (var _dest) (bv 8 0x1) false) (ite (var _tmp_cf) (bv 8 0x1) (bv 8 0x0)))) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (! (is_zero (var _masked))) (set cf (lsb (var _dest))) nop) (branch (== (var _masked) (bv 8 0x1)) (set of (^^ (msb (var _dest)) (var cf))) nop) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) -ad "rol byte [eax], 1" d000 0x0 (seq (set _dest (loadw 0 8 (+ (var eax) (bv 32 0x0)))) (set _cnt_mask (bv 8 0x1f)) (set _cnt (bv 8 0x1)) (set _masked (& (var _cnt_mask) (var _cnt))) (set _tmp_cnt (mod (var _masked) (bv 8 0x1))) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (msb (var _dest))) (set _dest (+ (<< (var _dest) (bv 8 0x1) false) (ite (var _tmp_cf) (bv 8 0x1) (bv 8 0x0)))) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (! (is_zero (var _masked))) (set cf (lsb (var _dest))) nop) (branch (== (var _masked) (bv 8 0x1)) (set of (^^ (msb (var _dest)) (var cf))) nop) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) -ad "rol byte [eax], cl" d200 0x0 (seq (set _dest (loadw 0 8 (+ (var eax) (bv 32 0x0)))) (set _cnt_mask (bv 8 0x1f)) (set _cnt (cast 8 false (var ecx))) (set _masked (& (var _cnt_mask) (var _cnt))) (set _tmp_cnt (mod (var _masked) (bv 8 0x1))) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (msb (var _dest))) (set _dest (+ (<< (var _dest) (bv 8 0x1) false) (ite (var _tmp_cf) (bv 8 0x1) (bv 8 0x0)))) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (! (is_zero (var _masked))) (set cf (lsb (var _dest))) nop) (branch (== (var _masked) (bv 8 0x1)) (set of (^^ (msb (var _dest)) (var cf))) nop) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) -ad "rol dword [eax], 0" c10000 0x0 (seq (set _dest (loadw 0 32 (+ (var eax) (bv 32 0x0)))) (set _cnt_mask (bv 8 0x1f)) (set _cnt (bv 8 0x0)) (set _masked (& (var _cnt_mask) (var _cnt))) (set _tmp_cnt (mod (var _masked) (bv 8 0x4))) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (msb (var _dest))) (set _dest (+ (<< (var _dest) (bv 8 0x1) false) (ite (var _tmp_cf) (bv 32 0x1) (bv 32 0x0)))) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (! (is_zero (var _masked))) (set cf (lsb (var _dest))) nop) (branch (== (var _masked) (bv 8 0x1)) (set of (^^ (msb (var _dest)) (var cf))) nop) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) -ad "rol dword [eax], 1" d100 0x0 (seq (set _dest (loadw 0 32 (+ (var eax) (bv 32 0x0)))) (set _cnt_mask (bv 32 0x1f)) (set _cnt (bv 32 0x1)) (set _masked (& (var _cnt_mask) (var _cnt))) (set _tmp_cnt (mod (var _masked) (bv 32 0x4))) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (msb (var _dest))) (set _dest (+ (<< (var _dest) (bv 8 0x1) false) (ite (var _tmp_cf) (bv 32 0x1) (bv 32 0x0)))) (set _tmp_cnt (- (var _tmp_cnt) (bv 32 0x1))))) (branch (! (is_zero (var _masked))) (set cf (lsb (var _dest))) nop) (branch (== (var _masked) (bv 32 0x1)) (set of (^^ (msb (var _dest)) (var cf))) nop) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) -ad "rol dword [eax], cl" d300 0x0 (seq (set _dest (loadw 0 32 (+ (var eax) (bv 32 0x0)))) (set _cnt_mask (bv 8 0x1f)) (set _cnt (cast 8 false (var ecx))) (set _masked (& (var _cnt_mask) (var _cnt))) (set _tmp_cnt (mod (var _masked) (bv 8 0x4))) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (msb (var _dest))) (set _dest (+ (<< (var _dest) (bv 8 0x1) false) (ite (var _tmp_cf) (bv 32 0x1) (bv 32 0x0)))) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (! (is_zero (var _masked))) (set cf (lsb (var _dest))) nop) (branch (== (var _masked) (bv 8 0x1)) (set of (^^ (msb (var _dest)) (var cf))) nop) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) -ad "ror byte [eax], 0" c00800 0x0 (seq (set _dest (loadw 0 8 (+ (var eax) (bv 32 0x0)))) (set _cnt_mask (bv 8 0x1f)) (set _cnt (bv 8 0x0)) (set _masked (& (var _cnt_mask) (var _cnt))) (set _tmp_cnt (mod (var _masked) (bv 8 0x1))) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (lsb (var _dest))) (set _dest (+ (>> (var _dest) (bv 8 0x1) false) (<< (ite (var _tmp_cf) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false))) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (! (is_zero (var _masked))) (set cf (msb (var _dest))) nop) (branch (== (var _masked) (bv 8 0x1)) (set of (^^ (msb (var _dest)) (msb (<< (var _dest) (bv 8 0x1) false)))) nop) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) -ad "ror byte [eax], 1" d008 0x0 (seq (set _dest (loadw 0 8 (+ (var eax) (bv 32 0x0)))) (set _cnt_mask (bv 8 0x1f)) (set _cnt (bv 8 0x1)) (set _masked (& (var _cnt_mask) (var _cnt))) (set _tmp_cnt (mod (var _masked) (bv 8 0x1))) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (lsb (var _dest))) (set _dest (+ (>> (var _dest) (bv 8 0x1) false) (<< (ite (var _tmp_cf) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false))) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (! (is_zero (var _masked))) (set cf (msb (var _dest))) nop) (branch (== (var _masked) (bv 8 0x1)) (set of (^^ (msb (var _dest)) (msb (<< (var _dest) (bv 8 0x1) false)))) nop) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) -ad "ror byte [eax], cl" d208 0x0 (seq (set _dest (loadw 0 8 (+ (var eax) (bv 32 0x0)))) (set _cnt_mask (bv 8 0x1f)) (set _cnt (cast 8 false (var ecx))) (set _masked (& (var _cnt_mask) (var _cnt))) (set _tmp_cnt (mod (var _masked) (bv 8 0x1))) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (lsb (var _dest))) (set _dest (+ (>> (var _dest) (bv 8 0x1) false) (<< (ite (var _tmp_cf) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false))) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (! (is_zero (var _masked))) (set cf (msb (var _dest))) nop) (branch (== (var _masked) (bv 8 0x1)) (set of (^^ (msb (var _dest)) (msb (<< (var _dest) (bv 8 0x1) false)))) nop) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) -ad "ror dword [eax], 0" c10800 0x0 (seq (set _dest (loadw 0 32 (+ (var eax) (bv 32 0x0)))) (set _cnt_mask (bv 8 0x1f)) (set _cnt (bv 8 0x0)) (set _masked (& (var _cnt_mask) (var _cnt))) (set _tmp_cnt (mod (var _masked) (bv 8 0x4))) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (lsb (var _dest))) (set _dest (+ (>> (var _dest) (bv 8 0x1) false) (<< (ite (var _tmp_cf) (bv 32 0x1) (bv 32 0x0)) (bv 8 0x4) false))) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (! (is_zero (var _masked))) (set cf (msb (var _dest))) nop) (branch (== (var _masked) (bv 8 0x1)) (set of (^^ (msb (var _dest)) (msb (<< (var _dest) (bv 8 0x1) false)))) nop) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) -ad "ror dword [eax], 1" d108 0x0 (seq (set _dest (loadw 0 32 (+ (var eax) (bv 32 0x0)))) (set _cnt_mask (bv 32 0x1f)) (set _cnt (bv 32 0x1)) (set _masked (& (var _cnt_mask) (var _cnt))) (set _tmp_cnt (mod (var _masked) (bv 32 0x4))) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (lsb (var _dest))) (set _dest (+ (>> (var _dest) (bv 8 0x1) false) (<< (ite (var _tmp_cf) (bv 32 0x1) (bv 32 0x0)) (bv 8 0x4) false))) (set _tmp_cnt (- (var _tmp_cnt) (bv 32 0x1))))) (branch (! (is_zero (var _masked))) (set cf (msb (var _dest))) nop) (branch (== (var _masked) (bv 32 0x1)) (set of (^^ (msb (var _dest)) (msb (<< (var _dest) (bv 8 0x1) false)))) nop) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) -ad "ror dword [eax], cl" d308 0x0 (seq (set _dest (loadw 0 32 (+ (var eax) (bv 32 0x0)))) (set _cnt_mask (bv 8 0x1f)) (set _cnt (cast 8 false (var ecx))) (set _masked (& (var _cnt_mask) (var _cnt))) (set _tmp_cnt (mod (var _masked) (bv 8 0x4))) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (lsb (var _dest))) (set _dest (+ (>> (var _dest) (bv 8 0x1) false) (<< (ite (var _tmp_cf) (bv 32 0x1) (bv 32 0x0)) (bv 8 0x4) false))) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (! (is_zero (var _masked))) (set cf (msb (var _dest))) nop) (branch (== (var _masked) (bv 8 0x1)) (set of (^^ (msb (var _dest)) (msb (<< (var _dest) (bv 8 0x1) false)))) nop) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) +ad "rol byte [eax], 0" c00000 0x0 (seq (set _dest (loadw 0 8 (+ (var eax) (bv 32 0x0)))) (set _cnt_mask (bv 8 0x1f)) (set _cnt (bv 8 0x0)) (set _masked (& (var _cnt_mask) (var _cnt))) (set _tmp_cnt (mod (var _masked) (bv 8 0x8))) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (msb (var _dest))) (set _dest (+ (<< (var _dest) (bv 8 0x1) false) (ite (var _tmp_cf) (bv 8 0x1) (bv 8 0x0)))) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (! (is_zero (var _masked))) (set cf (lsb (var _dest))) nop) (branch (== (var _masked) (bv 8 0x1)) (set of (^^ (msb (var _dest)) (var cf))) nop) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) +ad "rol byte [eax], 1" d000 0x0 (seq (set _dest (loadw 0 8 (+ (var eax) (bv 32 0x0)))) (set _cnt_mask (bv 8 0x1f)) (set _cnt (bv 8 0x1)) (set _masked (& (var _cnt_mask) (var _cnt))) (set _tmp_cnt (mod (var _masked) (bv 8 0x8))) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (msb (var _dest))) (set _dest (+ (<< (var _dest) (bv 8 0x1) false) (ite (var _tmp_cf) (bv 8 0x1) (bv 8 0x0)))) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (! (is_zero (var _masked))) (set cf (lsb (var _dest))) nop) (branch (== (var _masked) (bv 8 0x1)) (set of (^^ (msb (var _dest)) (var cf))) nop) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) +ad "rol byte [eax], cl" d200 0x0 (seq (set _dest (loadw 0 8 (+ (var eax) (bv 32 0x0)))) (set _cnt_mask (bv 8 0x1f)) (set _cnt (cast 8 false (var ecx))) (set _masked (& (var _cnt_mask) (var _cnt))) (set _tmp_cnt (mod (var _masked) (bv 8 0x8))) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (msb (var _dest))) (set _dest (+ (<< (var _dest) (bv 8 0x1) false) (ite (var _tmp_cf) (bv 8 0x1) (bv 8 0x0)))) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (! (is_zero (var _masked))) (set cf (lsb (var _dest))) nop) (branch (== (var _masked) (bv 8 0x1)) (set of (^^ (msb (var _dest)) (var cf))) nop) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) +ad "rol dword [eax], 0" c10000 0x0 (seq (set _dest (loadw 0 32 (+ (var eax) (bv 32 0x0)))) (set _cnt_mask (bv 8 0x1f)) (set _cnt (bv 8 0x0)) (set _masked (& (var _cnt_mask) (var _cnt))) (set _tmp_cnt (mod (var _masked) (bv 8 0x20))) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (msb (var _dest))) (set _dest (+ (<< (var _dest) (bv 8 0x1) false) (ite (var _tmp_cf) (bv 32 0x1) (bv 32 0x0)))) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (! (is_zero (var _masked))) (set cf (lsb (var _dest))) nop) (branch (== (var _masked) (bv 8 0x1)) (set of (^^ (msb (var _dest)) (var cf))) nop) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) +ad "rol dword [eax], 1" d100 0x0 (seq (set _dest (loadw 0 32 (+ (var eax) (bv 32 0x0)))) (set _cnt_mask (bv 32 0x1f)) (set _cnt (bv 32 0x1)) (set _masked (& (var _cnt_mask) (var _cnt))) (set _tmp_cnt (mod (var _masked) (bv 32 0x20))) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (msb (var _dest))) (set _dest (+ (<< (var _dest) (bv 8 0x1) false) (ite (var _tmp_cf) (bv 32 0x1) (bv 32 0x0)))) (set _tmp_cnt (- (var _tmp_cnt) (bv 32 0x1))))) (branch (! (is_zero (var _masked))) (set cf (lsb (var _dest))) nop) (branch (== (var _masked) (bv 32 0x1)) (set of (^^ (msb (var _dest)) (var cf))) nop) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) +ad "rol dword [eax], cl" d300 0x0 (seq (set _dest (loadw 0 32 (+ (var eax) (bv 32 0x0)))) (set _cnt_mask (bv 8 0x1f)) (set _cnt (cast 8 false (var ecx))) (set _masked (& (var _cnt_mask) (var _cnt))) (set _tmp_cnt (mod (var _masked) (bv 8 0x20))) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (msb (var _dest))) (set _dest (+ (<< (var _dest) (bv 8 0x1) false) (ite (var _tmp_cf) (bv 32 0x1) (bv 32 0x0)))) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (! (is_zero (var _masked))) (set cf (lsb (var _dest))) nop) (branch (== (var _masked) (bv 8 0x1)) (set of (^^ (msb (var _dest)) (var cf))) nop) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) +ad "ror byte [eax], 0" c00800 0x0 (seq (set _dest (loadw 0 8 (+ (var eax) (bv 32 0x0)))) (set _cnt_mask (bv 8 0x1f)) (set _cnt (bv 8 0x0)) (set _masked (& (var _cnt_mask) (var _cnt))) (set _tmp_cnt (mod (var _masked) (bv 8 0x8))) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (lsb (var _dest))) (set _dest (+ (>> (var _dest) (bv 8 0x1) false) (<< (ite (var _tmp_cf) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false))) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (! (is_zero (var _masked))) (set cf (msb (var _dest))) nop) (branch (== (var _masked) (bv 8 0x1)) (set of (^^ (msb (var _dest)) (msb (<< (var _dest) (bv 8 0x1) false)))) nop) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) +ad "ror byte [eax], 1" d008 0x0 (seq (set _dest (loadw 0 8 (+ (var eax) (bv 32 0x0)))) (set _cnt_mask (bv 8 0x1f)) (set _cnt (bv 8 0x1)) (set _masked (& (var _cnt_mask) (var _cnt))) (set _tmp_cnt (mod (var _masked) (bv 8 0x8))) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (lsb (var _dest))) (set _dest (+ (>> (var _dest) (bv 8 0x1) false) (<< (ite (var _tmp_cf) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false))) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (! (is_zero (var _masked))) (set cf (msb (var _dest))) nop) (branch (== (var _masked) (bv 8 0x1)) (set of (^^ (msb (var _dest)) (msb (<< (var _dest) (bv 8 0x1) false)))) nop) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) +ad "ror byte [eax], cl" d208 0x0 (seq (set _dest (loadw 0 8 (+ (var eax) (bv 32 0x0)))) (set _cnt_mask (bv 8 0x1f)) (set _cnt (cast 8 false (var ecx))) (set _masked (& (var _cnt_mask) (var _cnt))) (set _tmp_cnt (mod (var _masked) (bv 8 0x8))) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (lsb (var _dest))) (set _dest (+ (>> (var _dest) (bv 8 0x1) false) (<< (ite (var _tmp_cf) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false))) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (! (is_zero (var _masked))) (set cf (msb (var _dest))) nop) (branch (== (var _masked) (bv 8 0x1)) (set of (^^ (msb (var _dest)) (msb (<< (var _dest) (bv 8 0x1) false)))) nop) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) +ad "ror dword [eax], 0" c10800 0x0 (seq (set _dest (loadw 0 32 (+ (var eax) (bv 32 0x0)))) (set _cnt_mask (bv 8 0x1f)) (set _cnt (bv 8 0x0)) (set _masked (& (var _cnt_mask) (var _cnt))) (set _tmp_cnt (mod (var _masked) (bv 8 0x20))) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (lsb (var _dest))) (set _dest (+ (>> (var _dest) (bv 8 0x1) false) (<< (ite (var _tmp_cf) (bv 32 0x1) (bv 32 0x0)) (bv 8 0x4) false))) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (! (is_zero (var _masked))) (set cf (msb (var _dest))) nop) (branch (== (var _masked) (bv 8 0x1)) (set of (^^ (msb (var _dest)) (msb (<< (var _dest) (bv 8 0x1) false)))) nop) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) +ad "ror dword [eax], 1" d108 0x0 (seq (set _dest (loadw 0 32 (+ (var eax) (bv 32 0x0)))) (set _cnt_mask (bv 32 0x1f)) (set _cnt (bv 32 0x1)) (set _masked (& (var _cnt_mask) (var _cnt))) (set _tmp_cnt (mod (var _masked) (bv 32 0x20))) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (lsb (var _dest))) (set _dest (+ (>> (var _dest) (bv 8 0x1) false) (<< (ite (var _tmp_cf) (bv 32 0x1) (bv 32 0x0)) (bv 8 0x4) false))) (set _tmp_cnt (- (var _tmp_cnt) (bv 32 0x1))))) (branch (! (is_zero (var _masked))) (set cf (msb (var _dest))) nop) (branch (== (var _masked) (bv 32 0x1)) (set of (^^ (msb (var _dest)) (msb (<< (var _dest) (bv 8 0x1) false)))) nop) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) +ad "ror dword [eax], cl" d308 0x0 (seq (set _dest (loadw 0 32 (+ (var eax) (bv 32 0x0)))) (set _cnt_mask (bv 8 0x1f)) (set _cnt (cast 8 false (var ecx))) (set _masked (& (var _cnt_mask) (var _cnt))) (set _tmp_cnt (mod (var _masked) (bv 8 0x20))) (repeat (! (is_zero (var _tmp_cnt))) (seq (set _tmp_cf (lsb (var _dest))) (set _dest (+ (>> (var _dest) (bv 8 0x1) false) (<< (ite (var _tmp_cf) (bv 32 0x1) (bv 32 0x0)) (bv 8 0x4) false))) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (! (is_zero (var _masked))) (set cf (msb (var _dest))) nop) (branch (== (var _masked) (bv 8 0x1)) (set of (^^ (msb (var _dest)) (msb (<< (var _dest) (bv 8 0x1) false)))) nop) (storew 0 (+ (var eax) (bv 32 0x0)) (var _dest))) aB "roundpd xmm0, xmm0, 0" 660f3a09c000 aB "roundps xmm0, xmm0, 0" 660f3a08c000 aB "roundsd xmm0, xmm0, 0" 660f3a0bc000 @@ -1961,10 +1961,10 @@ a "sfence" 0faef8 a "sgdt [eax]" 0f0100 aB "shld dword [eax], eax, 0" 0fa40000 aB "shld dword [eax], eax, cl" 0fa500 -ad "sar edx, 5" c1fa05 0x0 (seq (set _cnt (bv 8 0x5)) (set _cnt_mask (bv 8 0x1f)) (set _masked (& (var _cnt) (var _cnt_mask))) (set _tmp_cnt (var _masked)) (set _dest (var edx)) (set _tmp_dest (var _dest)) (repeat (! (is_zero (var _tmp_cnt))) (seq (set cf (lsb (var _dest))) (set _dest (>> (var _dest) (bv 8 0x1) (msb (var _dest)))) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (== (var _masked) (bv 8 0x1)) (set of false) nop) (set edx (var _dest)) (set _result (var _dest)) (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)))) -ad "sal edx, 5" c1f205 0x0 (seq (set _cnt (bv 8 0x5)) (set _cnt_mask (bv 8 0x1f)) (set _masked (& (var _cnt) (var _cnt_mask))) (set _tmp_cnt (var _masked)) (set _dest (var edx)) (set _tmp_dest (var _dest)) (repeat (! (is_zero (var _tmp_cnt))) (seq (set cf (msb (var _dest))) (set _dest (<< (var _dest) (bv 8 0x1) false)) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (== (var _masked) (bv 8 0x1)) (set of (^^ (msb (var _dest)) (var cf))) nop) (set edx (var _dest)) (set _result (var _dest)) (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)))) -ad "shl edx, 5" c1e205 0x0 (seq (set _cnt (bv 8 0x5)) (set _cnt_mask (bv 8 0x1f)) (set _masked (& (var _cnt) (var _cnt_mask))) (set _tmp_cnt (var _masked)) (set _dest (var edx)) (set _tmp_dest (var _dest)) (repeat (! (is_zero (var _tmp_cnt))) (seq (set cf (msb (var _dest))) (set _dest (<< (var _dest) (bv 8 0x1) false)) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (== (var _masked) (bv 8 0x1)) (set of (^^ (msb (var _dest)) (var cf))) nop) (set edx (var _dest)) (set _result (var _dest)) (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)))) -ad "shr edx, 5" c1ea05 0x0 (seq (set _cnt (bv 8 0x5)) (set _cnt_mask (bv 8 0x1f)) (set _masked (& (var _cnt) (var _cnt_mask))) (set _tmp_cnt (var _masked)) (set _dest (var edx)) (set _tmp_dest (var _dest)) (repeat (! (is_zero (var _tmp_cnt))) (seq (set cf (lsb (var _dest))) (set _dest (>> (var _dest) (bv 8 0x1) false)) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (== (var _masked) (bv 8 0x1)) (set of (msb (var _tmp_dest))) nop) (set edx (var _dest)) (set _result (var _dest)) (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)))) +ad "sar edx, 5" c1fa05 0x0 (seq (set _cnt (bv 8 0x5)) (set _cnt_mask (bv 8 0x1f)) (set _masked (& (var _cnt) (var _cnt_mask))) (set _tmp_cnt (var _masked)) (set _dest (var edx)) (set _tmp_dest (var _dest)) (repeat (! (is_zero (var _tmp_cnt))) (seq (set cf (lsb (var _dest))) (set _dest (>> (var _dest) (bv 8 0x1) (msb (var _dest)))) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (== (var _masked) (bv 8 0x1)) (set of false) nop) (set edx (var _dest)) (branch (is_zero (var _cnt)) nop (seq (set _result (var _dest)) (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)))))) +ad "sal edx, 5" c1f205 0x0 (seq (set _cnt (bv 8 0x5)) (set _cnt_mask (bv 8 0x1f)) (set _masked (& (var _cnt) (var _cnt_mask))) (set _tmp_cnt (var _masked)) (set _dest (var edx)) (set _tmp_dest (var _dest)) (repeat (! (is_zero (var _tmp_cnt))) (seq (set cf (msb (var _dest))) (set _dest (<< (var _dest) (bv 8 0x1) false)) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (== (var _masked) (bv 8 0x1)) (set of (^^ (msb (var _dest)) (var cf))) nop) (set edx (var _dest)) (branch (is_zero (var _cnt)) nop (seq (set _result (var _dest)) (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)))))) +ad "shl edx, 5" c1e205 0x0 (seq (set _cnt (bv 8 0x5)) (set _cnt_mask (bv 8 0x1f)) (set _masked (& (var _cnt) (var _cnt_mask))) (set _tmp_cnt (var _masked)) (set _dest (var edx)) (set _tmp_dest (var _dest)) (repeat (! (is_zero (var _tmp_cnt))) (seq (set cf (msb (var _dest))) (set _dest (<< (var _dest) (bv 8 0x1) false)) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (== (var _masked) (bv 8 0x1)) (set of (^^ (msb (var _dest)) (var cf))) nop) (set edx (var _dest)) (branch (is_zero (var _cnt)) nop (seq (set _result (var _dest)) (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)))))) +ad "shr edx, 5" c1ea05 0x0 (seq (set _cnt (bv 8 0x5)) (set _cnt_mask (bv 8 0x1f)) (set _masked (& (var _cnt) (var _cnt_mask))) (set _tmp_cnt (var _masked)) (set _dest (var edx)) (set _tmp_dest (var _dest)) (repeat (! (is_zero (var _tmp_cnt))) (seq (set cf (lsb (var _dest))) (set _dest (>> (var _dest) (bv 8 0x1) false)) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (== (var _masked) (bv 8 0x1)) (set of (msb (var _tmp_dest))) nop) (set edx (var _dest)) (branch (is_zero (var _cnt)) nop (seq (set _result (var _dest)) (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)))))) aB "shrd dword [eax], eax, 0" 0fac0000 aB "shrd dword [eax], eax, cl" 0fad00 aB "shufpd xmm0, xmmword [eax], 0x0" 660fc60000 diff --git a/test/db/asm/x86_64 b/test/db/asm/x86_64 index 5cc195d7bb..642ebc08b9 100644 --- a/test/db/asm/x86_64 +++ b/test/db/asm/x86_64 @@ -1,7 +1,7 @@ -a "lea rax, [0x1000]" 488d05f90f0000 0x0 (set rax (+ (bv 64 0x7) (bv 64 0xff9))) -d "lea rax, [rip + 0xff9]" 488d05f90f0000 0x0 (set rax (+ (bv 64 0x7) (bv 64 0xff9))) +a "lea rax, [0x1000]" 488d05f90f0000 0x0 (set rax (cast 64 false (+ (bv 64 0x7) (bv 64 0xff9)))) +d "lea rax, [rip + 0xff9]" 488d05f90f0000 0x0 (set rax (cast 64 false (+ (bv 64 0x7) (bv 64 0xff9)))) ad "leave" c9 0x0 (seq (set rsp (var rbp)) (set rsp (+ (var rsp) (bv 64 0x8))) (set rbp (loadw 0 64 (+ (var rsp) (bv 64 0x0))))) -d "leave" 66c9 0x0 (seq (set rsp (var rbp)) (set rsp (+ (var rsp) (bv 64 0x4))) (set rbp (| (& (var rbp) (~ (bv 64 0xffffffff))) (cast 64 false (loadw 0 32 (+ (var rsp) (bv 64 0x0))))))) +d "leave" 66c9 0x0 (seq (set rsp (var rbp)) (set rsp (+ (var rsp) (bv 64 0x4))) (set rbp (cast 64 false (loadw 0 32 (+ (var rsp) (bv 64 0x0)))))) ad "nop" 90 0x0 nop ad "ret" c3 0x0 (seq (set rsp (+ (var rsp) (bv 64 0x8))) (set rsp (loadw 0 64 (+ (var rsp) (bv 64 0x0))))) a "add r13, r15" 4d01fd 0x0 (seq (set op1 (var r13)) (set op2 (var r15)) (set sum (+ (var op1) (var op2))) (set r13 (cast 64 false (var sum))) (set _result (var sum)) (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 sum)) (set _x (var op1)) (set _y (var op2)) (set cf (|| (|| (&& (msb (var _x)) (msb (var _y))) (&& (! (msb (var _result))) (msb (var _y)))) (&& (msb (var _x)) (! (msb (var _result)))))) (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 _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result)))))))) @@ -11,7 +11,7 @@ a "add rax, r8" 4c01c0 0x0 (seq (set op1 (var rax)) (set op2 (var r8)) (set sum a "add r10, r9" 4d01ca 0x0 (seq (set op1 (var r10)) (set op2 (var r9)) (set sum (+ (var op1) (var op2))) (set r10 (cast 64 false (var sum))) (set _result (var sum)) (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 sum)) (set _x (var op1)) (set _y (var op2)) (set cf (|| (|| (&& (msb (var _x)) (msb (var _y))) (&& (! (msb (var _result))) (msb (var _y)))) (&& (msb (var _x)) (! (msb (var _result)))))) (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 _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result)))))))) a "add rax, rcx" 4801c8 0x0 (seq (set op1 (var rax)) (set op2 (var rcx)) (set sum (+ (var op1) (var op2))) (set rax (var sum)) (set _result (var sum)) (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 sum)) (set _x (var op1)) (set _y (var op2)) (set cf (|| (|| (&& (msb (var _x)) (msb (var _y))) (&& (! (msb (var _result))) (msb (var _y)))) (&& (msb (var _x)) (! (msb (var _result)))))) (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 _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result)))))))) aB "and dword [ebp + 128], eax" 48218580000000 -a "call rbx" ffd3 0x0 (seq (set rsp (- (var rsp) (bv 64 0x8))) (storew 0 (+ (var rsp) (bv 64 0x0)) (cast 64 false (bv 64 0x2))) (jmp (var rbx))) +a "call rbx" ffd3 0x0 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (bv 64 0x2))) (set rsp (var final)) (jmp (var rbx))) a "cdqe" 4898 0x0 empty d "cmp qword [rax], 0x21" 48833821 0x0 (seq (set op1 (loadw 0 64 (+ (var rax) (bv 64 0x0)))) (set op2 (bv 64 0x21)) (set sub (- (var op1) (var op2))) (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))))))) (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)))) a "cmp rax, 33" 4883f821 0x0 (seq (set op1 (var rax)) (set op2 (bv 64 0x21)) (set sub (- (var op1) (var op2))) (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))))))) (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)))) @@ -21,28 +21,28 @@ a "cmp rdx, rsi" 4839f2 0x0 (seq (set op1 (var rdx)) (set op2 (var rsi)) (set su a "cmpsb" a6 0x0 (seq (set _src1 (loadw 0 8 (var rsi))) (set _src2 (loadw 0 8 (var rdi))) (set _temp (- (var _src1) (var _src2))) (set _result (var _temp)) (set _x (var _src1)) (set _y (var _src2)) (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))))))) (set _result (var _temp)) (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))) (branch (var df) (seq (set rsi (- (var rsi) (bv 64 0x1))) (set rdi (- (var rdi) (bv 64 0x1)))) (seq (set rsi (+ (var rsi) (bv 64 0x1))) (set rdi (+ (var rdi) (bv 64 0x1)))))) a "cmpsd" a7 0x0 (seq (set _src1 (loadw 0 32 (var rsi))) (set _src2 (loadw 0 32 (var rdi))) (set _temp (- (var _src1) (var _src2))) (set _result (var _temp)) (set _x (var _src1)) (set _y (var _src2)) (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))))))) (set _result (var _temp)) (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))) (branch (var df) (seq (set rsi (- (var rsi) (bv 64 0x4))) (set rdi (- (var rdi) (bv 64 0x4)))) (seq (set rsi (+ (var rsi) (bv 64 0x4))) (set rdi (+ (var rdi) (bv 64 0x4)))))) a "cmpsw" 66a7 0x0 (seq (set _src1 (loadw 0 16 (var rsi))) (set _src2 (loadw 0 16 (var rdi))) (set _temp (- (var _src1) (var _src2))) (set _result (var _temp)) (set _x (var _src1)) (set _y (var _src2)) (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))))))) (set _result (var _temp)) (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))) (branch (var df) (seq (set rsi (- (var rsi) (bv 64 0x2))) (set rdi (- (var rdi) (bv 64 0x2)))) (seq (set rsi (+ (var rsi) (bv 64 0x2))) (set rdi (+ (var rdi) (bv 64 0x2)))))) -d "cmpsd dword [esi], dword ptr [edi]" 67a7 0x0 (seq (set _src1 (loadw 0 32 (cast 64 false (cast 32 false (var rsi))))) (set _src2 (loadw 0 32 (cast 64 false (cast 32 false (var rdi))))) (set _temp (- (var _src1) (var _src2))) (set _result (var _temp)) (set _x (var _src1)) (set _y (var _src2)) (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))))))) (set _result (var _temp)) (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))) (branch (var df) (seq (set rsi (| (& (var rsi) (~ (bv 64 0xffffffff))) (cast 64 false (- (cast 32 false (var rsi)) (bv 32 0x4))))) (set rdi (| (& (var rdi) (~ (bv 64 0xffffffff))) (cast 64 false (- (cast 32 false (var rdi)) (bv 32 0x4)))))) (seq (set rsi (| (& (var rsi) (~ (bv 64 0xffffffff))) (cast 64 false (+ (cast 32 false (var rsi)) (bv 32 0x4))))) (set rdi (| (& (var rdi) (~ (bv 64 0xffffffff))) (cast 64 false (+ (cast 32 false (var rdi)) (bv 32 0x4)))))))) +d "cmpsd dword [esi], dword ptr [edi]" 67a7 0x0 (seq (set _src1 (loadw 0 32 (cast 64 false (cast 32 false (var rsi))))) (set _src2 (loadw 0 32 (cast 64 false (cast 32 false (var rdi))))) (set _temp (- (var _src1) (var _src2))) (set _result (var _temp)) (set _x (var _src1)) (set _y (var _src2)) (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))))))) (set _result (var _temp)) (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))) (branch (var df) (seq (set rsi (cast 64 false (- (cast 32 false (var rsi)) (bv 32 0x4)))) (set rdi (cast 64 false (- (cast 32 false (var rdi)) (bv 32 0x4))))) (seq (set rsi (cast 64 false (+ (cast 32 false (var rsi)) (bv 32 0x4)))) (set rdi (cast 64 false (+ (cast 32 false (var rdi)) (bv 32 0x4))))))) d "cmpsq qword [rsi], qword ptr [rdi]" 48a7 0x0 (seq (set _src1 (loadw 0 64 (var rsi))) (set _src2 (loadw 0 64 (var rdi))) (set _temp (- (var _src1) (var _src2))) (set _result (var _temp)) (set _x (var _src1)) (set _y (var _src2)) (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))))))) (set _result (var _temp)) (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))) (branch (var df) (seq (set rsi (- (var rsi) (bv 64 0x8))) (set rdi (- (var rdi) (bv 64 0x8)))) (seq (set rsi (+ (var rsi) (bv 64 0x8))) (set rdi (+ (var rdi) (bv 64 0x8)))))) a "lodsb" ac 0x0 (seq (set rax (| (& (var rax) (~ (bv 64 0xff))) (cast 64 false (loadw 0 8 (var rsi))))) (branch (var df) (set rsi (- (var rsi) (bv 64 0x1))) (set rsi (+ (var rsi) (bv 64 0x1))))) -a "lodsd" ad 0x0 (seq (set rax (| (& (var rax) (~ (bv 64 0xffffffff))) (cast 64 false (loadw 0 32 (var rsi))))) (branch (var df) (set rsi (- (var rsi) (bv 64 0x4))) (set rsi (+ (var rsi) (bv 64 0x4))))) +a "lodsd" ad 0x0 (seq (set rax (cast 64 false (loadw 0 32 (var rsi)))) (branch (var df) (set rsi (- (var rsi) (bv 64 0x4))) (set rsi (+ (var rsi) (bv 64 0x4))))) a "lodsw" 66ad 0x0 (seq (set rax (| (& (var rax) (~ (bv 64 0xffff))) (cast 64 false (loadw 0 16 (var rsi))))) (branch (var df) (set rsi (- (var rsi) (bv 64 0x2))) (set rsi (+ (var rsi) (bv 64 0x2))))) -d "lodsd eax, dword [esi]" 67ad 0x0 (seq (set rax (| (& (var rax) (~ (bv 64 0xffffffff))) (cast 64 false (loadw 0 32 (cast 64 false (cast 32 false (var rsi))))))) (branch (var df) (set rsi (| (& (var rsi) (~ (bv 64 0xffffffff))) (cast 64 false (- (cast 32 false (var rsi)) (bv 32 0x4))))) (set rsi (| (& (var rsi) (~ (bv 64 0xffffffff))) (cast 64 false (+ (cast 32 false (var rsi)) (bv 32 0x4))))))) +d "lodsd eax, dword [esi]" 67ad 0x0 (seq (set rax (cast 64 false (loadw 0 32 (cast 64 false (cast 32 false (var rsi)))))) (branch (var df) (set rsi (cast 64 false (- (cast 32 false (var rsi)) (bv 32 0x4)))) (set rsi (cast 64 false (+ (cast 32 false (var rsi)) (bv 32 0x4)))))) d "lodsq rax, qword [rsi]" 48ad 0x0 (seq (set rax (loadw 0 64 (var rsi))) (branch (var df) (set rsi (- (var rsi) (bv 64 0x8))) (set rsi (+ (var rsi) (bv 64 0x8))))) -d "loop 0" 67e2fd 0x0 (seq (set rcx (| (& (var rcx) (~ (bv 64 0xffffffff))) (cast 64 false (- (cast 32 false (var rcx)) (bv 32 0x1))))) (branch (! (is_zero (cast 32 false (var rcx)))) (jmp (bv 64 0x3)) nop)) +d "loop 0" 67e2fd 0x0 (seq (set rcx (cast 64 false (- (cast 32 false (var rcx)) (bv 32 0x1)))) (branch (! (is_zero (cast 32 false (var rcx)))) (jmp (bv 64 0x3)) nop)) a "movsb" a4 0x0 (seq (storew 0 (var rdi) (loadw 0 8 (var rsi))) (branch (var df) (seq (set rsi (- (var rsi) (bv 64 0x1))) (set rdi (- (var rdi) (bv 64 0x1)))) (seq (set rsi (+ (var rsi) (bv 64 0x1))) (set rdi (+ (var rdi) (bv 64 0x1)))))) a "movsd" a5 0x0 (seq (storew 0 (var rdi) (loadw 0 32 (var rsi))) (branch (var df) (seq (set rsi (- (var rsi) (bv 64 0x4))) (set rdi (- (var rdi) (bv 64 0x4)))) (seq (set rsi (+ (var rsi) (bv 64 0x4))) (set rdi (+ (var rdi) (bv 64 0x4)))))) a "movsw" 66a5 0x0 (seq (storew 0 (var rdi) (loadw 0 16 (var rsi))) (branch (var df) (seq (set rsi (- (var rsi) (bv 64 0x2))) (set rdi (- (var rdi) (bv 64 0x2)))) (seq (set rsi (+ (var rsi) (bv 64 0x2))) (set rdi (+ (var rdi) (bv 64 0x2)))))) -d "movsd dword [edi], dword ptr [esi]" 67a5 0x0 (seq (storew 0 (cast 64 false (cast 32 false (var rdi))) (loadw 0 32 (cast 64 false (cast 32 false (var rsi))))) (branch (var df) (seq (set rsi (| (& (var rsi) (~ (bv 64 0xffffffff))) (cast 64 false (- (cast 32 false (var rsi)) (bv 32 0x4))))) (set rdi (| (& (var rdi) (~ (bv 64 0xffffffff))) (cast 64 false (- (cast 32 false (var rdi)) (bv 32 0x4)))))) (seq (set rsi (| (& (var rsi) (~ (bv 64 0xffffffff))) (cast 64 false (+ (cast 32 false (var rsi)) (bv 32 0x4))))) (set rdi (| (& (var rdi) (~ (bv 64 0xffffffff))) (cast 64 false (+ (cast 32 false (var rdi)) (bv 32 0x4)))))))) +d "movsd dword [edi], dword ptr [esi]" 67a5 0x0 (seq (storew 0 (cast 64 false (cast 32 false (var rdi))) (loadw 0 32 (cast 64 false (cast 32 false (var rsi))))) (branch (var df) (seq (set rsi (cast 64 false (- (cast 32 false (var rsi)) (bv 32 0x4)))) (set rdi (cast 64 false (- (cast 32 false (var rdi)) (bv 32 0x4))))) (seq (set rsi (cast 64 false (+ (cast 32 false (var rsi)) (bv 32 0x4)))) (set rdi (cast 64 false (+ (cast 32 false (var rdi)) (bv 32 0x4))))))) d "movsq qword [rdi], qword ptr [rsi]" 48a5 0x0 (seq (storew 0 (var rdi) (loadw 0 64 (var rsi))) (branch (var df) (seq (set rsi (- (var rsi) (bv 64 0x8))) (set rdi (- (var rdi) (bv 64 0x8)))) (seq (set rsi (+ (var rsi) (bv 64 0x8))) (set rdi (+ (var rdi) (bv 64 0x8)))))) a "stosb" aa 0x0 (seq (storew 0 (var rdi) (cast 8 false (var rax))) (branch (var df) (set rdi (- (var rdi) (bv 64 0x1))) (set rdi (+ (var rdi) (bv 64 0x1))))) a "stosd" ab 0x0 (seq (storew 0 (var rdi) (cast 32 false (var rax))) (branch (var df) (set rdi (- (var rdi) (bv 64 0x4))) (set rdi (+ (var rdi) (bv 64 0x4))))) a "stosw" 66ab 0x0 (seq (storew 0 (var rdi) (cast 16 false (var rax))) (branch (var df) (set rdi (- (var rdi) (bv 64 0x2))) (set rdi (+ (var rdi) (bv 64 0x2))))) -d "stosd dword [edi], eax" 67ab 0x0 (seq (storew 0 (cast 64 false (cast 32 false (var rdi))) (cast 32 false (var rax))) (branch (var df) (set rdi (| (& (var rdi) (~ (bv 64 0xffffffff))) (cast 64 false (- (cast 32 false (var rdi)) (bv 32 0x4))))) (set rdi (| (& (var rdi) (~ (bv 64 0xffffffff))) (cast 64 false (+ (cast 32 false (var rdi)) (bv 32 0x4))))))) +d "stosd dword [edi], eax" 67ab 0x0 (seq (storew 0 (cast 64 false (cast 32 false (var rdi))) (cast 32 false (var rax))) (branch (var df) (set rdi (cast 64 false (- (cast 32 false (var rdi)) (bv 32 0x4)))) (set rdi (cast 64 false (+ (cast 32 false (var rdi)) (bv 32 0x4)))))) d "stosq qword [rdi], rax" 48ab 0x0 (seq (storew 0 (var rdi) (var rax)) (branch (var df) (set rdi (- (var rdi) (bv 64 0x8))) (set rdi (+ (var rdi) (bv 64 0x8))))) a "scasb" ae 0x0 (seq (set _reg (cast 8 false (var rax))) (set _src (loadw 0 8 (var rdi))) (set _temp (- (var _reg) (var _src))) (set _result (var _temp)) (set _x (var _reg)) (set _y (var _src)) (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))))))) (set _result (var _temp)) (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))) (branch (var df) (set rdi (- (var rdi) (bv 64 0x1))) (set rdi (+ (var rdi) (bv 64 0x1))))) a "scasd" af 0x0 (seq (set _reg (cast 32 false (var rax))) (set _src (loadw 0 32 (var rdi))) (set _temp (- (var _reg) (var _src))) (set _result (var _temp)) (set _x (var _reg)) (set _y (var _src)) (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))))))) (set _result (var _temp)) (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))) (branch (var df) (set rdi (- (var rdi) (bv 64 0x4))) (set rdi (+ (var rdi) (bv 64 0x4))))) a "scasw" 66af 0x0 (seq (set _reg (cast 16 false (var rax))) (set _src (loadw 0 16 (var rdi))) (set _temp (- (var _reg) (var _src))) (set _result (var _temp)) (set _x (var _reg)) (set _y (var _src)) (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))))))) (set _result (var _temp)) (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))) (branch (var df) (set rdi (- (var rdi) (bv 64 0x2))) (set rdi (+ (var rdi) (bv 64 0x2))))) -d "scasd eax, dword [edi]" 67af 0x0 (seq (set _reg (cast 32 false (var rax))) (set _src (loadw 0 32 (cast 64 false (cast 32 false (var rdi))))) (set _temp (- (var _reg) (var _src))) (set _result (var _temp)) (set _x (var _reg)) (set _y (var _src)) (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))))))) (set _result (var _temp)) (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))) (branch (var df) (set rdi (| (& (var rdi) (~ (bv 64 0xffffffff))) (cast 64 false (- (cast 32 false (var rdi)) (bv 32 0x4))))) (set rdi (| (& (var rdi) (~ (bv 64 0xffffffff))) (cast 64 false (+ (cast 32 false (var rdi)) (bv 32 0x4))))))) +d "scasd eax, dword [edi]" 67af 0x0 (seq (set _reg (cast 32 false (var rax))) (set _src (loadw 0 32 (cast 64 false (cast 32 false (var rdi))))) (set _temp (- (var _reg) (var _src))) (set _result (var _temp)) (set _x (var _reg)) (set _y (var _src)) (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))))))) (set _result (var _temp)) (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))) (branch (var df) (set rdi (cast 64 false (- (cast 32 false (var rdi)) (bv 32 0x4)))) (set rdi (cast 64 false (+ (cast 32 false (var rdi)) (bv 32 0x4)))))) d "scasq rax, qword [rdi]" 48af 0x0 (seq (set _reg (var rax)) (set _src (loadw 0 64 (var rdi))) (set _temp (- (var _reg) (var _src))) (set _result (var _temp)) (set _x (var _reg)) (set _y (var _src)) (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))))))) (set _result (var _temp)) (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))) (branch (var df) (set rdi (- (var rdi) (bv 64 0x8))) (set rdi (+ (var rdi) (bv 64 0x8))))) ad "mul rax" 48f7e0 0x0 (seq (set _mul (* (cast 128 false (var rax)) (cast 128 false (var rax)))) (set rdx (cast 64 false (>> (var _mul) (bv 8 0x40) false))) (set rax (cast 64 false (var _mul))) (branch (is_zero (>> (var _mul) (bv 8 0x40) false)) (seq (set of false) (set cf false)) (seq (set of true) (set cf true)))) ad "div rax" 48f7f0 0x0 (seq (set _src (cast 128 false (var rax))) (branch (is_zero (var _src)) nop (seq (set _rdxrax (| (<< (cast 128 false (var rdx)) (bv 8 0x40) false) (cast 128 false (var rax)))) (set _temp (cast 64 false (div (var _rdxrax) (var _src)))) (branch (! (ule (var _temp) (bv 64 0xffffffffffffffff))) nop (seq (set rax (| (& (var rax) (~ (bv 64 0xffff))) (cast 64 false (var _temp)))) (set rdx (| (& (var rdx) (~ (bv 64 0xffff))) (cast 64 false (mod (var _rdxrax) (var _src)))))))))) @@ -52,43 +52,43 @@ a "inc rdx" 48ffc2 0x0 (seq (set _op (var rdx)) (set _result (+ (var _op) (bv 64 d "jrcxz 0x39" e303 0x34 (branch (is_zero (var rcx)) (jmp (bv 64 0x39)) nop) d "jecxz 0x4a" 67e303 0x44 (branch (is_zero (cast 32 false (var rcx))) (jmp (bv 64 0x4a)) nop) a "jmp rbx" ffe3 0x0 (jmp (cast 64 false (var rbx))) -a "lea rax, [rax+0]" 488d00 0x0 (set rax (+ (var rax) (bv 64 0x0))) -a "lea rax, [rax+1]" 488d4001 0x0 (set rax (+ (var rax) (bv 64 0x1))) -a "lea rax, [rax-0]" 488d00 0x0 (set rax (+ (var rax) (bv 64 0x0))) -a "lea rax, [rax-1]" 488d40ff 0x0 (set rax (+ (var rax) (bv 64 0xffffffffffffffff))) -a "lea rax, [rax]" 488d00 0x0 (set rax (+ (var rax) (bv 64 0x0))) -d "lea eax, [rax]" 8d00 0x0 (set rax (| (& (var rax) (~ (bv 64 0xffffffff))) (cast 64 false (+ (var rax) (bv 64 0x0))))) -d "lea rax, [eax]" 67488d00 0x0 (set rax (+ (cast 64 false (cast 32 false (var rax))) (bv 64 0x0))) +a "lea rax, [rax+0]" 488d00 0x0 (set rax (cast 64 false (+ (var rax) (bv 64 0x0)))) +a "lea rax, [rax+1]" 488d4001 0x0 (set rax (cast 64 false (+ (var rax) (bv 64 0x1)))) +a "lea rax, [rax-0]" 488d00 0x0 (set rax (cast 64 false (+ (var rax) (bv 64 0x0)))) +a "lea rax, [rax-1]" 488d40ff 0x0 (set rax (cast 64 false (+ (var rax) (bv 64 0xffffffffffffffff)))) +a "lea rax, [rax]" 488d00 0x0 (set rax (cast 64 false (+ (var rax) (bv 64 0x0)))) +d "lea eax, [rax]" 8d00 0x0 (set rax (cast 64 false (cast 32 false (+ (var rax) (bv 64 0x0))))) +d "lea rax, [eax]" 67488d00 0x0 (set rax (cast 64 false (+ (cast 64 false (cast 32 false (var rax))) (bv 64 0x0)))) aB "lea rax,[rel -10]" 488d06f6ffffff aB "lea rax,[rel 0]" 488d0500000000 aB "lea rax,[rel 10]" 488d050a000000 -a "lea rax,[rip+0]" 488d0500000000 0x0 (set rax (+ (bv 64 0x7) (bv 64 0x0))) -a "lea rax,[rip+10]" 488d050a000000 0x0 (set rax (+ (bv 64 0x7) (bv 64 0xa))) -a "lea rax,[rip-0]" 488d0500000000 0x0 (set rax (+ (bv 64 0x7) (bv 64 0x0))) -a "lea rax,[rip-10]" 488d05f6ffffff 0x0 (set rax (+ (bv 64 0x7) (bv 64 0xfffffffffffffff6))) -a "lea rax,[rip]" 488d0500000000 0x0 (set rax (+ (bv 64 0x7) (bv 64 0x0))) -a "lea rdi,[rip+0x1011]" 488d3d11100000 0x0 (set rdi (+ (bv 64 0x7) (bv 64 0x1011))) +a "lea rax,[rip+0]" 488d0500000000 0x0 (set rax (cast 64 false (+ (bv 64 0x7) (bv 64 0x0)))) +a "lea rax,[rip+10]" 488d050a000000 0x0 (set rax (cast 64 false (+ (bv 64 0x7) (bv 64 0xa)))) +a "lea rax,[rip-0]" 488d0500000000 0x0 (set rax (cast 64 false (+ (bv 64 0x7) (bv 64 0x0)))) +a "lea rax,[rip-10]" 488d05f6ffffff 0x0 (set rax (cast 64 false (+ (bv 64 0x7) (bv 64 0xfffffffffffffff6)))) +a "lea rax,[rip]" 488d0500000000 0x0 (set rax (cast 64 false (+ (bv 64 0x7) (bv 64 0x0)))) +a "lea rdi,[rip+0x1011]" 488d3d11100000 0x0 (set rdi (cast 64 false (+ (bv 64 0x7) (bv 64 0x1011)))) aB "lea rax, [0x803]" 488d042503080000 aB "lea rax, 0x803" 488d042503080000 a "mov [rsi], rbx" 48891e 0x0 (storew 0 (+ (var rsi) (bv 64 0x0)) (var rbx)) -ad "mov eax, 0" b800000000 0x0 (set rax (| (& (var rax) (~ (bv 64 0xffffffff))) (cast 64 false (bv 32 0x0)))) -ad "mov ecx, 0x7fffffff" b9ffffff7f 0x0 (set rcx (| (& (var rcx) (~ (bv 64 0xffffffff))) (cast 64 false (bv 32 0x7fffffff)))) -a "mov esi, -0x80000000" be00000080 0x0 (set rsi (| (& (var rsi) (~ (bv 64 0xffffffff))) (cast 64 false (bv 32 0x80000000)))) -ad "mov esi, 0x80000000" be00000080 0x0 (set rsi (| (& (var rsi) (~ (bv 64 0xffffffff))) (cast 64 false (bv 32 0x80000000)))) -a "mov edi, -1" bfffffffff 0x0 (set rdi (| (& (var rdi) (~ (bv 64 0xffffffff))) (cast 64 false (bv 32 0xffffffff)))) -ad "mov edi, 0xffffffff" bfffffffff 0x0 (set rdi (| (& (var rdi) (~ (bv 64 0xffffffff))) (cast 64 false (bv 32 0xffffffff)))) -a "mov rax, 0x1122334455667788" 48b88877665544332211 0x0 empty +ad "mov eax, 0" b800000000 0x0 (set rax (cast 64 false (bv 32 0x0))) +ad "mov ecx, 0x7fffffff" b9ffffff7f 0x0 (set rcx (cast 64 false (bv 32 0x7fffffff))) +a "mov esi, -0x80000000" be00000080 0x0 (set rsi (cast 64 false (bv 32 0x80000000))) +ad "mov esi, 0x80000000" be00000080 0x0 (set rsi (cast 64 false (bv 32 0x80000000))) +a "mov edi, -1" bfffffffff 0x0 (set rdi (cast 64 false (bv 32 0xffffffff))) +ad "mov edi, 0xffffffff" bfffffffff 0x0 (set rdi (cast 64 false (bv 32 0xffffffff))) +a "mov rax, 0x1122334455667788" 48b88877665544332211 0x0 (set rax (bv 64 0x1122334455667788)) a "mov rax, 3" 48c7c003000000 0x0 (set rax (bv 64 0x3)) a "mov rax, 33" 48c7c021000000 0x0 (set rax (bv 64 0x21)) ad "mov rax, 0x7fffffff" 48c7c0ffffff7f 0x0 (set rax (bv 64 0x7fffffff)) -a "mov rax, 0x80000000" 48b80000008000000000 0x0 empty -ad "movabs rax, 0x80000000" 48b80000008000000000 0x0 empty -a "mov rax, 0xdeadbeef" 48b8efbeadde00000000 0x0 empty -ad "movabs rax, 0xdeadbeef" 48b8efbeadde00000000 0x0 empty -a "mov rax, 0xffffffff" 48b8ffffffff00000000 0x0 empty -ad "movabs rax, 0xffffffff" 48b8ffffffff00000000 0x0 empty -a "mov rax, 0x100000000" 48b80000000001000000 0x0 empty -ad "movabs rax, 0x100000000" 48b80000000001000000 0x0 empty +a "mov rax, 0x80000000" 48b80000008000000000 0x0 (set rax (bv 64 0x80000000)) +ad "movabs rax, 0x80000000" 48b80000008000000000 0x0 (set rax (bv 64 0x80000000)) +a "mov rax, 0xdeadbeef" 48b8efbeadde00000000 0x0 (set rax (bv 64 0xdeadbeef)) +ad "movabs rax, 0xdeadbeef" 48b8efbeadde00000000 0x0 (set rax (bv 64 0xdeadbeef)) +a "mov rax, 0xffffffff" 48b8ffffffff00000000 0x0 (set rax (bv 64 0xffffffff)) +ad "movabs rax, 0xffffffff" 48b8ffffffff00000000 0x0 (set rax (bv 64 0xffffffff)) +a "mov rax, 0x100000000" 48b80000000001000000 0x0 (set rax (bv 64 0x100000000)) +ad "movabs rax, 0x100000000" 48b80000000001000000 0x0 (set rax (bv 64 0x100000000)) ad "mov rax, 0" 48c7c000000000 0x0 (set rax (bv 64 0x0)) a "mov rax, -1" 48c7c0ffffffff 0x0 (set rax (bv 64 0xffffffffffffffff)) a "mov rax, -0x1" 48c7c0ffffffff 0x0 (set rax (bv 64 0xffffffffffffffff)) @@ -100,17 +100,17 @@ a "mov rax, -2" 48c7c0feffffff 0x0 (set rax (bv 64 0xfffffffffffffffe)) ad "mov rax, 0xfffffffffffffffe" 48c7c0feffffff 0x0 (set rax (bv 64 0xfffffffffffffffe)) a "mov rax, -0x80000000" 48c7c000000080 0x0 (set rax (bv 64 0xffffffff80000000)) ad "mov rax, 0xffffffff80000000" 48c7c000000080 0x0 (set rax (bv 64 0xffffffff80000000)) -a "mov rax, -0x80000001" 48b8ffffff7fffffffff 0x0 empty -ad "movabs rax, 0xffffffff7fffffff" 48b8ffffff7fffffffff 0x0 empty +a "mov rax, -0x80000001" 48b8ffffff7fffffffff 0x0 (set rax (bv 64 0xffffffff7fffffff)) +ad "movabs rax, 0xffffffff7fffffff" 48b8ffffff7fffffffff 0x0 (set rax (bv 64 0xffffffff7fffffff)) ad "mov r9, 0x7fffffff" 49c7c1ffffff7f 0x0 (set r9 (cast 64 false (bv 64 0x7fffffff))) -a "mov r10, 0x80000000" 49ba0000008000000000 0x0 empty -ad "movabs r10, 0x80000000" 49ba0000008000000000 0x0 empty -a "mov r11, 0x100000000" 49bb0000000001000000 0x0 empty -ad "movabs r11, 0x100000000" 49bb0000000001000000 0x0 empty +a "mov r10, 0x80000000" 49ba0000008000000000 0x0 (set r10 (cast 64 false (bv 64 0x80000000))) +ad "movabs r10, 0x80000000" 49ba0000008000000000 0x0 (set r10 (cast 64 false (bv 64 0x80000000))) +a "mov r11, 0x100000000" 49bb0000000001000000 0x0 (set r11 (cast 64 false (bv 64 0x100000000))) +ad "movabs r11, 0x100000000" 49bb0000000001000000 0x0 (set r11 (cast 64 false (bv 64 0x100000000))) a "mov r14, -0x80000000" 49c7c600000080 0x0 (set r14 (cast 64 false (bv 64 0xffffffff80000000))) ad "mov r14, 0xffffffff80000000" 49c7c600000080 0x0 (set r14 (cast 64 false (bv 64 0xffffffff80000000))) -a "mov r15, -0x80000001" 49bfffffff7fffffffff 0x0 empty -ad "movabs r15, 0xffffffff7fffffff" 49bfffffff7fffffffff 0x0 empty +a "mov r15, -0x80000001" 49bfffffff7fffffffff 0x0 (set r15 (cast 64 false (bv 64 0xffffffff7fffffff))) +ad "movabs r15, 0xffffffff7fffffff" 49bfffffff7fffffffff 0x0 (set r15 (cast 64 false (bv 64 0xffffffff7fffffff))) a "mov rax, [rax+0]" 488b00 0x0 (set rax (loadw 0 64 (+ (var rax) (bv 64 0x0)))) a "mov rax, [rax+1]" 488b4001 0x0 (set rax (loadw 0 64 (+ (var rax) (bv 64 0x1)))) a "mov rax, [rax-0]" 488b00 0x0 (set rax (loadw 0 64 (+ (var rax) (bv 64 0x0)))) @@ -125,20 +125,20 @@ a "mov rax,[rip-0]" 488b0500000000 0x0 (set rax (loadw 0 64 (+ (bv 64 0x7) (bv 6 a "mov rax,[rip-10]" 488b05f6ffffff 0x0 (set rax (loadw 0 64 (+ (bv 64 0x7) (bv 64 0xfffffffffffffff6)))) a "mov rax,[rip]" 488b0500000000 0x0 (set rax (loadw 0 64 (+ (bv 64 0x7) (bv 64 0x0)))) a "mov rbx, 3" 48c7c303000000 0x0 (set rbx (bv 64 0x3)) -a "mov edx, [rbp-4]" 8b55fc 0x0 (set rdx (| (& (var rdx) (~ (bv 64 0xffffffff))) (cast 64 false (loadw 0 32 (+ (var rbp) (bv 64 0xfffffffffffffffc)))))) +a "mov edx, [rbp-4]" 8b55fc 0x0 (set rdx (cast 64 false (loadw 0 32 (+ (var rbp) (bv 64 0xfffffffffffffffc))))) a "mov rbx, rax" 4889c3 0x0 (set rbx (var rax)) -a "mov rcx, -0x1122334455667788" 48b9788899aabbccddee 0x0 empty +a "mov rcx, -0x1122334455667788" 48b9788899aabbccddee 0x0 (set rcx (bv 64 0xeeddccbbaa998878)) aB "mov rcx, -0x112233445566778899" 00 a "mov rsi, rbx" 4889de 0x0 (set rsi (var rbx)) a "mov rcx, r9" 4c89c9 0x0 (set rcx (var r9)) a "mov r10, rax" 4989c2 0x0 (set r10 (cast 64 false (var rax))) a "mov r12, r9" 4d89cc 0x0 (set r12 (cast 64 false (var r9))) a "mov rcx, rbp" 4889e9 0x0 (set rcx (var rbp)) -a "mov al, [0xbeef]" a0efbe000000000000 0x0 empty -a "mov ax, [0xbeef]" 66a1efbe000000000000 0x0 empty -a "mov eax, [0xbeef]" a1efbe000000000000 0x0 empty -a "mov rax, [0xbeef]" 48a1efbe000000000000 0x0 empty -a "mov rax, [0x1122334455667788]" 48a18877665544332211 0x0 empty +a "mov al, [0xbeef]" a0efbe000000000000 0x0 (set rax (| (& (var rax) (~ (bv 64 0xff))) (cast 64 false (loadw 0 8 (bv 64 0xbeef))))) +a "mov ax, [0xbeef]" 66a1efbe000000000000 0x0 (set rax (| (& (var rax) (~ (bv 64 0xffff))) (cast 64 false (loadw 0 16 (bv 64 0xbeef))))) +a "mov eax, [0xbeef]" a1efbe000000000000 0x0 (set rax (cast 64 false (loadw 0 32 (bv 64 0xbeef)))) +a "mov rax, [0xbeef]" 48a1efbe000000000000 0x0 (set rax (loadw 0 64 (bv 64 0xbeef))) +a "mov rax, [0x1122334455667788]" 48a18877665544332211 0x0 (set rax (loadw 0 64 (bv 64 0x1122334455667788))) a "mov rax, [rax + 0xbeef]" 488b80efbe0000 0x0 (set rax (loadw 0 64 (+ (var rax) (bv 64 0xbeef)))) a "mov rax, [rbx + 0xbeef]" 488b83efbe0000 0x0 (set rax (loadw 0 64 (+ (var rbx) (bv 64 0xbeef)))) a "mov rcx, [rbx + 0xbeef]" 488b8befbe0000 0x0 (set rcx (loadw 0 64 (+ (var rbx) (bv 64 0xbeef)))) @@ -152,12 +152,12 @@ a "pop rax" 58 0x0 (seq (set rax (loadw 0 64 (+ (var rsp) (bv 64 0x0)))) (set rs ad "pop r8" 4158 0x0 (seq (set r8 (cast 64 false (loadw 0 64 (+ (var rsp) (bv 64 0x0))))) (set rsp (+ (var rsp) (bv 64 0x8)))) ad "pop r15" 415f 0x0 (seq (set r15 (cast 64 false (loadw 0 64 (+ (var rsp) (bv 64 0x0))))) (set rsp (+ (var rsp) (bv 64 0x8)))) d "popfq" 9d 0x0 (seq (set _flags (loadw 0 64 (+ (var rsp) (bv 64 0x0)))) (set cf (lsb (var _flags))) (set _flags (>> (var _flags) (bv 8 0x2) false)) (set pf (lsb (var _flags))) (set _flags (>> (var _flags) (bv 8 0x2) false)) (set af (lsb (var _flags))) (set _flags (>> (var _flags) (bv 8 0x2) false)) (set zf (lsb (var _flags))) (set _flags (>> (var _flags) (bv 8 0x1) false)) (set sf (lsb (var _flags))) (set _flags (>> (var _flags) (bv 8 0x1) false)) (set tf (lsb (var _flags))) (set _flags (>> (var _flags) (bv 8 0x1) false)) (set if (lsb (var _flags))) (set _flags (>> (var _flags) (bv 8 0x1) false)) (set df (lsb (var _flags))) (set _flags (>> (var _flags) (bv 8 0x1) false)) (set of (lsb (var _flags))) (set _flags (>> (var _flags) (bv 8 0x3) false)) (set nt (lsb (var _flags))) (set rsp (+ (var rsp) (bv 64 0x8)))) -d "pushfq" 9c 0x0 (seq (set rsp (- (var rsp) (bv 64 0x8))) (storew 0 (+ (var rsp) (bv 64 0x0)) (cast 64 false (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (ite false (bv 64 0x1) (bv 64 0x0)) (bv 64 0x1) false) (ite (var nt) (bv 64 0x1) (bv 64 0x0))) (bv 64 0x2) false) (bv 64 0x3)) (bv 64 0x1) false) (ite (var of) (bv 64 0x1) (bv 64 0x0))) (bv 64 0x1) false) (ite (var df) (bv 64 0x1) (bv 64 0x0))) (bv 64 0x1) false) (ite (var if) (bv 64 0x1) (bv 64 0x0))) (bv 64 0x1) false) (ite (var tf) (bv 64 0x1) (bv 64 0x0))) (bv 64 0x1) false) (ite (var zf) (bv 64 0x1) (bv 64 0x0))) (bv 64 0x1) false) (ite (var zf) (bv 64 0x1) (bv 64 0x0))) (bv 64 0x2) false) (ite (var af) (bv 64 0x1) (bv 64 0x0))) (bv 64 0x2) false) (ite (var pf) (bv 64 0x1) (bv 64 0x0))) (bv 64 0x1) false) (bv 64 0x1)) (bv 64 0x1) false) (ite (var cf) (bv 64 0x1) (bv 64 0x0)))))) +d "pushfq" 9c 0x0 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (| (<< (ite false (bv 64 0x1) (bv 64 0x0)) (bv 64 0x1) false) (ite (var nt) (bv 64 0x1) (bv 64 0x0))) (bv 64 0x2) false) (bv 64 0x3)) (bv 64 0x1) false) (ite (var of) (bv 64 0x1) (bv 64 0x0))) (bv 64 0x1) false) (ite (var df) (bv 64 0x1) (bv 64 0x0))) (bv 64 0x1) false) (ite (var if) (bv 64 0x1) (bv 64 0x0))) (bv 64 0x1) false) (ite (var tf) (bv 64 0x1) (bv 64 0x0))) (bv 64 0x1) false) (ite (var zf) (bv 64 0x1) (bv 64 0x0))) (bv 64 0x1) false) (ite (var zf) (bv 64 0x1) (bv 64 0x0))) (bv 64 0x2) false) (ite (var af) (bv 64 0x1) (bv 64 0x0))) (bv 64 0x2) false) (ite (var pf) (bv 64 0x1) (bv 64 0x0))) (bv 64 0x1) false) (bv 64 0x1)) (bv 64 0x1) false) (ite (var cf) (bv 64 0x1) (bv 64 0x0))))) (set rsp (var final))) aB "prefetcht1 [eax]" 670f1810 aB "prefetcht1 [rax]" 0f1810 aB "prefetcht1 byte [eax]" 670f1810 aB "prefetcht1 byte [rax]" 0f1810 -a "shl rdx, 5" 48c1e205 0x0 (seq (set _cnt (bv 8 0x5)) (set _cnt_mask (bv 8 0x3f)) (set _masked (& (var _cnt) (var _cnt_mask))) (set _tmp_cnt (var _masked)) (set _dest (var rdx)) (set _tmp_dest (var _dest)) (repeat (! (is_zero (var _tmp_cnt))) (seq (set cf (msb (var _dest))) (set _dest (<< (var _dest) (bv 8 0x1) false)) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (== (var _masked) (bv 8 0x1)) (set of (^^ (msb (var _dest)) (var cf))) nop) (set rdx (var _dest)) (set _result (var _dest)) (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 "shl rdx, 5" 48c1e205 0x0 (seq (set _cnt (bv 8 0x5)) (set _cnt_mask (bv 8 0x3f)) (set _masked (& (var _cnt) (var _cnt_mask))) (set _tmp_cnt (var _masked)) (set _dest (var rdx)) (set _tmp_dest (var _dest)) (repeat (! (is_zero (var _tmp_cnt))) (seq (set cf (msb (var _dest))) (set _dest (<< (var _dest) (bv 8 0x1) false)) (set _tmp_cnt (- (var _tmp_cnt) (bv 8 0x1))))) (branch (== (var _masked) (bv 8 0x1)) (set of (^^ (msb (var _dest)) (var cf))) nop) (set rdx (var _dest)) (branch (is_zero (var _cnt)) nop (seq (set _result (var _dest)) (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 "sub rax, 44" 4883e82c 0x0 (seq (set op1 (var rax)) (set op2 (bv 64 0x2c)) (set sub (- (var op1) (var op2))) (set rax (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 rax, rbx" 4829d8 0x0 (seq (set op1 (var rax)) (set op2 (var rbx)) (set sub (- (var op1) (var op2))) (set rax (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 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)))))))) @@ -183,29 +183,29 @@ a "repz monitor" f30f01c8 a "repe vmcall" f30f01c1 a "repne sfence" f20faef8 a "rep rdpmc" f30f33 -a "mov eax, 33" b821000000 0x0 (set rax (| (& (var rax) (~ (bv 64 0xffffffff))) (cast 64 false (bv 32 0x21)))) +a "mov eax, 33" b821000000 0x0 (set rax (cast 64 false (bv 32 0x21))) a "mov rax, 33" 48c7c021000000 0x0 (set rax (bv 64 0x21)) a "mov dword ptr [rbp+4],0" c7450400000000 0x0 (storew 0 (+ (var rbp) (bv 64 0x4)) (bv 32 0x0)) a "mov qword ptr [rbp+4],0" 48c7450400000000 0x0 (storew 0 (+ (var rbp) (bv 64 0x4)) (bv 64 0x0)) a "mov [rbp+4],0" 48c7450400000000 0x0 (storew 0 (+ (var rbp) (bv 64 0x4)) (bv 64 0x0)) a "mov [ebp+4],0" 67c7450400000000 0x0 (storew 0 (+ (cast 64 false (cast 32 false (var rbp))) (bv 64 0x4)) (bv 32 0x0)) -ad "push r8" 4150 0x0 (seq (set rsp (- (var rsp) (bv 64 0x8))) (storew 0 (+ (var rsp) (bv 64 0x0)) (cast 64 false (var r8)))) -ad "push r9" 4151 0x0 (seq (set rsp (- (var rsp) (bv 64 0x8))) (storew 0 (+ (var rsp) (bv 64 0x0)) (cast 64 false (var r9)))) -ad "push r10" 4152 0x0 (seq (set rsp (- (var rsp) (bv 64 0x8))) (storew 0 (+ (var rsp) (bv 64 0x0)) (cast 64 false (var r10)))) -ad "push r11" 4153 0x0 (seq (set rsp (- (var rsp) (bv 64 0x8))) (storew 0 (+ (var rsp) (bv 64 0x0)) (cast 64 false (var r11)))) -ad "push r12" 4154 0x0 (seq (set rsp (- (var rsp) (bv 64 0x8))) (storew 0 (+ (var rsp) (bv 64 0x0)) (cast 64 false (var r12)))) -ad "push r13" 4155 0x0 (seq (set rsp (- (var rsp) (bv 64 0x8))) (storew 0 (+ (var rsp) (bv 64 0x0)) (cast 64 false (var r13)))) -ad "push r14" 4156 0x0 (seq (set rsp (- (var rsp) (bv 64 0x8))) (storew 0 (+ (var rsp) (bv 64 0x0)) (cast 64 false (var r14)))) -ad "push r15" 4157 0x0 (seq (set rsp (- (var rsp) (bv 64 0x8))) (storew 0 (+ (var rsp) (bv 64 0x0)) (cast 64 false (var r15)))) +ad "push r8" 4150 0x0 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (var r8))) (set rsp (var final))) +ad "push r9" 4151 0x0 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (var r9))) (set rsp (var final))) +ad "push r10" 4152 0x0 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (var r10))) (set rsp (var final))) +ad "push r11" 4153 0x0 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (var r11))) (set rsp (var final))) +ad "push r12" 4154 0x0 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (var r12))) (set rsp (var final))) +ad "push r13" 4155 0x0 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (var r13))) (set rsp (var final))) +ad "push r14" 4156 0x0 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (var r14))) (set rsp (var final))) +ad "push r15" 4157 0x0 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (var r15))) (set rsp (var final))) -ad "call r8" 41ffd0 0x0 (seq (set rsp (- (var rsp) (bv 64 0x8))) (storew 0 (+ (var rsp) (bv 64 0x0)) (cast 64 false (bv 64 0x3))) (jmp (var r8))) -ad "call r9" 41ffd1 0x0 (seq (set rsp (- (var rsp) (bv 64 0x8))) (storew 0 (+ (var rsp) (bv 64 0x0)) (cast 64 false (bv 64 0x3))) (jmp (var r9))) -ad "call r10" 41ffd2 0x0 (seq (set rsp (- (var rsp) (bv 64 0x8))) (storew 0 (+ (var rsp) (bv 64 0x0)) (cast 64 false (bv 64 0x3))) (jmp (var r10))) -ad "call r11" 41ffd3 0x0 (seq (set rsp (- (var rsp) (bv 64 0x8))) (storew 0 (+ (var rsp) (bv 64 0x0)) (cast 64 false (bv 64 0x3))) (jmp (var r11))) -ad "call r12" 41ffd4 0x0 (seq (set rsp (- (var rsp) (bv 64 0x8))) (storew 0 (+ (var rsp) (bv 64 0x0)) (cast 64 false (bv 64 0x3))) (jmp (var r12))) -ad "call r13" 41ffd5 0x0 (seq (set rsp (- (var rsp) (bv 64 0x8))) (storew 0 (+ (var rsp) (bv 64 0x0)) (cast 64 false (bv 64 0x3))) (jmp (var r13))) -ad "call r14" 41ffd6 0x0 (seq (set rsp (- (var rsp) (bv 64 0x8))) (storew 0 (+ (var rsp) (bv 64 0x0)) (cast 64 false (bv 64 0x3))) (jmp (var r14))) -ad "call r15" 41ffd7 0x0 (seq (set rsp (- (var rsp) (bv 64 0x8))) (storew 0 (+ (var rsp) (bv 64 0x0)) (cast 64 false (bv 64 0x3))) (jmp (var r15))) +ad "call r8" 41ffd0 0x0 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (bv 64 0x3))) (set rsp (var final)) (jmp (var r8))) +ad "call r9" 41ffd1 0x0 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (bv 64 0x3))) (set rsp (var final)) (jmp (var r9))) +ad "call r10" 41ffd2 0x0 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (bv 64 0x3))) (set rsp (var final)) (jmp (var r10))) +ad "call r11" 41ffd3 0x0 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (bv 64 0x3))) (set rsp (var final)) (jmp (var r11))) +ad "call r12" 41ffd4 0x0 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (bv 64 0x3))) (set rsp (var final)) (jmp (var r12))) +ad "call r13" 41ffd5 0x0 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (bv 64 0x3))) (set rsp (var final)) (jmp (var r13))) +ad "call r14" 41ffd6 0x0 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (bv 64 0x3))) (set rsp (var final)) (jmp (var r14))) +ad "call r15" 41ffd7 0x0 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (bv 64 0x3))) (set rsp (var final)) (jmp (var r15))) a "mov dword ptr [rax],0x1" c70001000000 0x0 (storew 0 (+ (var rax) (bv 64 0x0)) (bv 32 0x1)) a "mov qword [rax], 0x1" 48c70001000000 0x0 (storew 0 (+ (var rax) (bv 64 0x0)) (bv 64 0x1)) a "mov [rax], 0x1" 48c70001000000 0x0 (storew 0 (+ (var rax) (bv 64 0x0)) (bv 64 0x1)) @@ -807,7 +807,7 @@ aB "mov rsp, qword[r12 - 0x12]" 498b6424ee aB "mov qword[r12], rsp" 49892424 aB "mov qword[r8 + 0x20], rax" 49894020 aB "mov r12, qword[r12]" 4d8b2424 -a "mov eax,r12d" 4489e0 0x0 (set rax (| (& (var rax) (~ (bv 64 0xffffffff))) (cast 64 false (cast 32 false (var r12))))) +a "mov eax,r12d" 4489e0 0x0 (set rax (cast 64 false (cast 32 false (var r12)))) ad "movabs r12, 1" 49bc0100000000000000 a "inc al" fec0 0x0 (seq (set _op (cast 8 false (var rax))) (set _result (+ (var _op) (bv 8 0x1))) (set rax (| (& (var rax) (~ (bv 64 0xff))) (cast 64 false (var _result)))) (set _result (var _result)) (set _x (var _op)) (set _y (bv 8 0x1)) (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 _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (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 "inc BYTE PTR [r12]" 41fe0424 0x0 (seq (set _op (loadw 0 8 (+ (cast 64 false (var r12)) (bv 64 0x0)))) (set _result (+ (var _op) (bv 8 0x1))) (storew 0 (+ (cast 64 false (var r12)) (bv 64 0x0)) (var _result)) (set _result (var _result)) (set _x (var _op)) (set _y (bv 8 0x1)) (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 _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (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)))) @@ -844,12 +844,12 @@ a "inc DWORD PTR [rsp]" ff0424 0x0 (seq (set _op (loadw 0 32 (+ (var rsp) (bv 64 a "inc DWORD PTR [rsp+0x10]" ff442410 0x0 (seq (set _op (loadw 0 32 (+ (var rsp) (bv 64 0x10)))) (set _result (+ (var _op) (bv 32 0x1))) (storew 0 (+ (var rsp) (bv 64 0x10)) (var _result)) (set _result (var _result)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (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 "inc DWORD PTR [rsp+rax*4+0x400]" ff848400040000 0x0 (seq (set _op (loadw 0 32 (+ (+ (var rsp) (* (var rax) (bv 64 0x4))) (bv 64 0x400)))) (set _result (+ (var _op) (bv 32 0x1))) (storew 0 (+ (+ (var rsp) (* (var rax) (bv 64 0x4))) (bv 64 0x400)) (var _result)) (set _result (var _result)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (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 "inc DWORD PTR [rsp+rbp*4+0x2b8]" ff84acb8020000 0x0 (seq (set _op (loadw 0 32 (+ (+ (var rsp) (* (var rbp) (bv 64 0x4))) (bv 64 0x2b8)))) (set _result (+ (var _op) (bv 32 0x1))) (storew 0 (+ (+ (var rsp) (* (var rbp) (bv 64 0x4))) (bv 64 0x2b8)) (var _result)) (set _result (var _result)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (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 "inc eax" ffc0 0x0 (seq (set _op (cast 32 false (var rax))) (set _result (+ (var _op) (bv 32 0x1))) (set rax (| (& (var rax) (~ (bv 64 0xffffffff))) (cast 64 false (var _result)))) (set _result (var _result)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (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 "inc ebp" ffc5 0x0 (seq (set _op (cast 32 false (var rbp))) (set _result (+ (var _op) (bv 32 0x1))) (set rbp (| (& (var rbp) (~ (bv 64 0xffffffff))) (cast 64 false (var _result)))) (set _result (var _result)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (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 "inc ebx" ffc3 0x0 (seq (set _op (cast 32 false (var rbx))) (set _result (+ (var _op) (bv 32 0x1))) (set rbx (| (& (var rbx) (~ (bv 64 0xffffffff))) (cast 64 false (var _result)))) (set _result (var _result)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (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 "inc ecx" ffc1 0x0 (seq (set _op (cast 32 false (var rcx))) (set _result (+ (var _op) (bv 32 0x1))) (set rcx (| (& (var rcx) (~ (bv 64 0xffffffff))) (cast 64 false (var _result)))) (set _result (var _result)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (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 "inc edi" ffc7 0x0 (seq (set _op (cast 32 false (var rdi))) (set _result (+ (var _op) (bv 32 0x1))) (set rdi (| (& (var rdi) (~ (bv 64 0xffffffff))) (cast 64 false (var _result)))) (set _result (var _result)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (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 "inc edx" ffc2 0x0 (seq (set _op (cast 32 false (var rdx))) (set _result (+ (var _op) (bv 32 0x1))) (set rdx (| (& (var rdx) (~ (bv 64 0xffffffff))) (cast 64 false (var _result)))) (set _result (var _result)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (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 "inc eax" ffc0 0x0 (seq (set _op (cast 32 false (var rax))) (set _result (+ (var _op) (bv 32 0x1))) (set rax (cast 64 false (var _result))) (set _result (var _result)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (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 "inc ebp" ffc5 0x0 (seq (set _op (cast 32 false (var rbp))) (set _result (+ (var _op) (bv 32 0x1))) (set rbp (cast 64 false (var _result))) (set _result (var _result)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (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 "inc ebx" ffc3 0x0 (seq (set _op (cast 32 false (var rbx))) (set _result (+ (var _op) (bv 32 0x1))) (set rbx (cast 64 false (var _result))) (set _result (var _result)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (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 "inc ecx" ffc1 0x0 (seq (set _op (cast 32 false (var rcx))) (set _result (+ (var _op) (bv 32 0x1))) (set rcx (cast 64 false (var _result))) (set _result (var _result)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (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 "inc edi" ffc7 0x0 (seq (set _op (cast 32 false (var rdi))) (set _result (+ (var _op) (bv 32 0x1))) (set rdi (cast 64 false (var _result))) (set _result (var _result)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (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 "inc edx" ffc2 0x0 (seq (set _op (cast 32 false (var rdx))) (set _result (+ (var _op) (bv 32 0x1))) (set rdx (cast 64 false (var _result))) (set _result (var _result)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (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 "inc QWORD PTR [r10]" 49ff02 0x0 (seq (set _op (loadw 0 64 (+ (cast 64 false (var r10)) (bv 64 0x0)))) (set _result (+ (var _op) (bv 64 0x1))) (storew 0 (+ (cast 64 false (var r10)) (bv 64 0x0)) (var _result)) (set _result (var _result)) (set _x (var _op)) (set _y (bv 64 0x1)) (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 _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (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 "inc QWORD PTR [r10+rax*1]" 49ff0402 0x0 (seq (set _op (loadw 0 64 (+ (+ (cast 64 false (var r10)) (* (var rax) (bv 64 0x1))) (bv 64 0x0)))) (set _result (+ (var _op) (bv 64 0x1))) (storew 0 (+ (+ (cast 64 false (var r10)) (* (var rax) (bv 64 0x1))) (bv 64 0x0)) (var _result)) (set _result (var _result)) (set _x (var _op)) (set _y (bv 64 0x1)) (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 _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (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 "inc QWORD PTR [r11]" 49ff03 0x0 (seq (set _op (loadw 0 64 (+ (cast 64 false (var r11)) (bv 64 0x0)))) (set _result (+ (var _op) (bv 64 0x1))) (storew 0 (+ (cast 64 false (var r11)) (bv 64 0x0)) (var _result)) (set _result (var _result)) (set _x (var _op)) (set _y (bv 64 0x1)) (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 _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))) (set _result (var _result)) (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)))) @@ -938,12 +938,12 @@ a "dec DWORD PTR [rsp]" ff0c24 0x0 (seq (set _op (loadw 0 32 (+ (var rsp) (bv 64 a "dec DWORD PTR [rsp+0x10]" ff4c2410 0x0 (seq (set _op (loadw 0 32 (+ (var rsp) (bv 64 0x10)))) (set _dec (- (var _op) (bv 32 0x1))) (storew 0 (+ (var rsp) (bv 64 0x10)) (var _dec)) (set _result (var _dec)) (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 _dec)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 "dec DWORD PTR [rsp+rax*4+0x400]" ff8c8400040000 0x0 (seq (set _op (loadw 0 32 (+ (+ (var rsp) (* (var rax) (bv 64 0x4))) (bv 64 0x400)))) (set _dec (- (var _op) (bv 32 0x1))) (storew 0 (+ (+ (var rsp) (* (var rax) (bv 64 0x4))) (bv 64 0x400)) (var _dec)) (set _result (var _dec)) (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 _dec)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 "dec DWORD PTR [rsp+rbp*4+0x2b8]" ff8cacb8020000 0x0 (seq (set _op (loadw 0 32 (+ (+ (var rsp) (* (var rbp) (bv 64 0x4))) (bv 64 0x2b8)))) (set _dec (- (var _op) (bv 32 0x1))) (storew 0 (+ (+ (var rsp) (* (var rbp) (bv 64 0x4))) (bv 64 0x2b8)) (var _dec)) (set _result (var _dec)) (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 _dec)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 "dec eax" ffc8 0x0 (seq (set _op (cast 32 false (var rax))) (set _dec (- (var _op) (bv 32 0x1))) (set rax (| (& (var rax) (~ (bv 64 0xffffffff))) (cast 64 false (var _dec)))) (set _result (var _dec)) (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 _dec)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 "dec ebp" ffcd 0x0 (seq (set _op (cast 32 false (var rbp))) (set _dec (- (var _op) (bv 32 0x1))) (set rbp (| (& (var rbp) (~ (bv 64 0xffffffff))) (cast 64 false (var _dec)))) (set _result (var _dec)) (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 _dec)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 "dec ebx" ffcb 0x0 (seq (set _op (cast 32 false (var rbx))) (set _dec (- (var _op) (bv 32 0x1))) (set rbx (| (& (var rbx) (~ (bv 64 0xffffffff))) (cast 64 false (var _dec)))) (set _result (var _dec)) (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 _dec)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 "dec ecx" ffc9 0x0 (seq (set _op (cast 32 false (var rcx))) (set _dec (- (var _op) (bv 32 0x1))) (set rcx (| (& (var rcx) (~ (bv 64 0xffffffff))) (cast 64 false (var _dec)))) (set _result (var _dec)) (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 _dec)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 "dec edi" ffcf 0x0 (seq (set _op (cast 32 false (var rdi))) (set _dec (- (var _op) (bv 32 0x1))) (set rdi (| (& (var rdi) (~ (bv 64 0xffffffff))) (cast 64 false (var _dec)))) (set _result (var _dec)) (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 _dec)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 "dec edx" ffca 0x0 (seq (set _op (cast 32 false (var rdx))) (set _dec (- (var _op) (bv 32 0x1))) (set rdx (| (& (var rdx) (~ (bv 64 0xffffffff))) (cast 64 false (var _dec)))) (set _result (var _dec)) (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 _dec)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 "dec eax" ffc8 0x0 (seq (set _op (cast 32 false (var rax))) (set _dec (- (var _op) (bv 32 0x1))) (set rax (cast 64 false (var _dec))) (set _result (var _dec)) (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 _dec)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 "dec ebp" ffcd 0x0 (seq (set _op (cast 32 false (var rbp))) (set _dec (- (var _op) (bv 32 0x1))) (set rbp (cast 64 false (var _dec))) (set _result (var _dec)) (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 _dec)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 "dec ebx" ffcb 0x0 (seq (set _op (cast 32 false (var rbx))) (set _dec (- (var _op) (bv 32 0x1))) (set rbx (cast 64 false (var _dec))) (set _result (var _dec)) (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 _dec)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 "dec ecx" ffc9 0x0 (seq (set _op (cast 32 false (var rcx))) (set _dec (- (var _op) (bv 32 0x1))) (set rcx (cast 64 false (var _dec))) (set _result (var _dec)) (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 _dec)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 "dec edi" ffcf 0x0 (seq (set _op (cast 32 false (var rdi))) (set _dec (- (var _op) (bv 32 0x1))) (set rdi (cast 64 false (var _dec))) (set _result (var _dec)) (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 _dec)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 "dec edx" ffca 0x0 (seq (set _op (cast 32 false (var rdx))) (set _dec (- (var _op) (bv 32 0x1))) (set rdx (cast 64 false (var _dec))) (set _result (var _dec)) (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 _dec)) (set _x (var _op)) (set _y (bv 32 0x1)) (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 "dec QWORD PTR [r10]" 49ff0a 0x0 (seq (set _op (loadw 0 64 (+ (cast 64 false (var r10)) (bv 64 0x0)))) (set _dec (- (var _op) (bv 64 0x1))) (storew 0 (+ (cast 64 false (var r10)) (bv 64 0x0)) (var _dec)) (set _result (var _dec)) (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 _dec)) (set _x (var _op)) (set _y (bv 64 0x1)) (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 "dec QWORD PTR [r10+rax*1]" 49ff0c02 0x0 (seq (set _op (loadw 0 64 (+ (+ (cast 64 false (var r10)) (* (var rax) (bv 64 0x1))) (bv 64 0x0)))) (set _dec (- (var _op) (bv 64 0x1))) (storew 0 (+ (+ (cast 64 false (var r10)) (* (var rax) (bv 64 0x1))) (bv 64 0x0)) (var _dec)) (set _result (var _dec)) (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 _dec)) (set _x (var _op)) (set _y (bv 64 0x1)) (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 "dec QWORD PTR [r11]" 49ff0b 0x0 (seq (set _op (loadw 0 64 (+ (cast 64 false (var r11)) (bv 64 0x0)))) (set _dec (- (var _op) (bv 64 0x1))) (storew 0 (+ (cast 64 false (var r11)) (bv 64 0x0)) (var _dec)) (set _result (var _dec)) (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 _dec)) (set _x (var _op)) (set _y (bv 64 0x1)) (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)))))))) @@ -1002,10 +1002,10 @@ a "bswap r15" 490fcf a "bswap eax" 0fc8 a "bswap r15d" 410fcf ad "endbr64" f30f1efa -d "enter 8, 0" c8080000 0x0 (seq (set _alloc_sz (cast 16 false (bv 64 0x8))) (set _nest_lvl (mod (cast 8 false (bv 64 0x0)) (bv 8 0x20))) (set rsp (- (var rsp) (bv 64 0x8))) (storew 0 (+ (var rsp) (bv 64 0x0)) (cast 64 false (var rbp))) (set _frame_tmp (var rsp)) (branch (is_zero (var _nest_lvl)) nop (seq (branch (! (ule (var _nest_lvl) (bv 8 0x1))) (seq (set _itr (bv 8 0x1)) (repeat (&& (ule (var _itr) (var _nest_lvl)) (! (== (var _itr) (var _nest_lvl)))) (seq (set rbp (- (var rbp) (bv 64 0x8))) (set rsp (- (var rsp) (bv 64 0x8))) (storew 0 (+ (var rsp) (bv 64 0x0)) (cast 64 false (loadw 0 64 (var rbp)))) (set _itr (+ (var _itr) (bv 8 0x1)))))) nop) (set rsp (- (var rsp) (bv 64 0x8))) (storew 0 (+ (var rsp) (bv 64 0x0)) (cast 64 false (var _frame_tmp))))) (set rsp (- (var rsp) (cast 64 false (var _alloc_sz)))) (set rbp (var _frame_tmp))) -d "enter 8, 0" 66c8080000 0x0 (seq (set _alloc_sz (cast 16 false (bv 32 0x8))) (set _nest_lvl (mod (cast 8 false (bv 32 0x0)) (bv 8 0x20))) (set rsp (- (var rsp) (bv 64 0x8))) (storew 0 (+ (var rsp) (bv 64 0x0)) (cast 64 false (cast 32 false (var rbp)))) (set _frame_tmp (var rsp)) (branch (is_zero (var _nest_lvl)) nop (seq (branch (! (ule (var _nest_lvl) (bv 8 0x1))) (seq (set _itr (bv 8 0x1)) (repeat (&& (ule (var _itr) (var _nest_lvl)) (! (== (var _itr) (var _nest_lvl)))) (seq (set rbp (- (var rbp) (bv 64 0x4))) (set rsp (- (var rsp) (bv 64 0x8))) (storew 0 (+ (var rsp) (bv 64 0x0)) (cast 64 false (loadw 0 32 (var rbp)))) (set _itr (+ (var _itr) (bv 8 0x1)))))) nop) (set rsp (- (var rsp) (bv 64 0x8))) (storew 0 (+ (var rsp) (bv 64 0x0)) (cast 64 false (var _frame_tmp))))) (set rsp (- (var rsp) (cast 64 false (var _alloc_sz)))) (set rbp (| (& (var rbp) (~ (bv 64 0xffffffff))) (cast 64 false (var _frame_tmp))))) -ad "xchg eax, r8d" 4190 0x0 (seq (set _temp (cast 32 false (var rax))) (set rax (| (& (var rax) (~ (bv 64 0xffffffff))) (cast 64 false (cast 32 false (var r8))))) (set r8 (cast 64 false (var _temp)))) -a "xchg r8d, eax" 4190 0x0 (seq (set _temp (cast 32 false (var rax))) (set rax (| (& (var rax) (~ (bv 64 0xffffffff))) (cast 64 false (cast 32 false (var r8))))) (set r8 (cast 64 false (var _temp)))) +d "enter 8, 0" c8080000 0x0 (seq (set _alloc_sz (cast 16 false (bv 64 0x8))) (set _nest_lvl (mod (cast 8 false (bv 64 0x0)) (bv 8 0x20))) (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (var rbp))) (set rsp (var final)) (set _frame_tmp (var rsp)) (branch (is_zero (var _nest_lvl)) nop (seq (branch (! (ule (var _nest_lvl) (bv 8 0x1))) (seq (set _itr (bv 8 0x1)) (repeat (&& (ule (var _itr) (var _nest_lvl)) (! (== (var _itr) (var _nest_lvl)))) (seq (set rbp (- (var rbp) (bv 64 0x8))) (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (loadw 0 64 (var rbp)))) (set rsp (var final)) (set _itr (+ (var _itr) (bv 8 0x1)))))) nop) (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (var _frame_tmp))) (set rsp (var final)))) (set rsp (- (var rsp) (cast 64 false (var _alloc_sz)))) (set rbp (var _frame_tmp))) +d "enter 8, 0" 66c8080000 0x0 (seq (set _alloc_sz (cast 16 false (bv 32 0x8))) (set _nest_lvl (mod (cast 8 false (bv 32 0x0)) (bv 8 0x20))) (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (cast 32 false (var rbp)))) (set rsp (var final)) (set _frame_tmp (var rsp)) (branch (is_zero (var _nest_lvl)) nop (seq (branch (! (ule (var _nest_lvl) (bv 8 0x1))) (seq (set _itr (bv 8 0x1)) (repeat (&& (ule (var _itr) (var _nest_lvl)) (! (== (var _itr) (var _nest_lvl)))) (seq (set rbp (- (var rbp) (bv 64 0x4))) (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (loadw 0 32 (var rbp)))) (set rsp (var final)) (set _itr (+ (var _itr) (bv 8 0x1)))))) nop) (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (var _frame_tmp))) (set rsp (var final)))) (set rsp (- (var rsp) (cast 64 false (var _alloc_sz)))) (set rbp (cast 64 false (var _frame_tmp)))) +ad "xchg eax, r8d" 4190 0x0 (seq (set _temp (cast 32 false (var rax))) (set rax (cast 64 false (cast 32 false (var r8)))) (set r8 (cast 64 false (var _temp)))) +a "xchg r8d, eax" 4190 0x0 (seq (set _temp (cast 32 false (var rax))) (set rax (cast 64 false (cast 32 false (var r8)))) (set r8 (cast 64 false (var _temp)))) ad "xchg rax, rdx" 4892 0x0 (seq (set _temp (var rax)) (set rax (var rdx)) (set rdx (var _temp))) a "xchg rdx, rax" 4892 0x0 (seq (set _temp (var rax)) (set rax (var rdx)) (set rdx (var _temp))) ad "xchg rax, r8" 4990 0x0 (seq (set _temp (var rax)) (set rax (var r8)) (set r8 (cast 64 false (var _temp)))) @@ -1018,8 +1018,8 @@ ad "xchg r8d, r15d" 4587f8 0x0 (seq (set _temp (cast 32 false (var r8))) (set r8 ad "xchg r15d, r8d" 4587c7 0x0 (seq (set _temp (cast 32 false (var r15))) (set r15 (cast 64 false (cast 32 false (var r8)))) (set r8 (cast 64 false (var _temp)))) ad "xchg rdx, r8" 4c87c2 0x0 (seq (set _temp (var rdx)) (set rdx (var r8)) (set r8 (cast 64 false (var _temp)))) ad "xchg r15, rdx" 4987d7 0x0 (seq (set _temp (var r15)) (set r15 (cast 64 false (var rdx))) (set rdx (var _temp))) -d "call qword [rip + 0x3a8f3e]" 48ff153e8f3a00 0x0 (seq (set rsp (- (var rsp) (bv 64 0x8))) (storew 0 (+ (var rsp) (bv 64 0x0)) (cast 64 false (bv 64 0x7))) (jmp (loadw 0 64 (+ (bv 64 0x7) (bv 64 0x3a8f3e))))) -d "call qword [rip + 0x1d638f]" 48ff158f631d00 0x0 (seq (set rsp (- (var rsp) (bv 64 0x8))) (storew 0 (+ (var rsp) (bv 64 0x0)) (cast 64 false (bv 64 0x7))) (jmp (loadw 0 64 (+ (bv 64 0x7) (bv 64 0x1d638f))))) +d "call qword [rip + 0x3a8f3e]" 48ff153e8f3a00 0x0 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (bv 64 0x7))) (set rsp (var final)) (jmp (loadw 0 64 (+ (bv 64 0x7) (bv 64 0x3a8f3e))))) +d "call qword [rip + 0x1d638f]" 48ff158f631d00 0x0 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (bv 64 0x7))) (set rsp (var final)) (jmp (loadw 0 64 (+ (bv 64 0x7) (bv 64 0x1d638f))))) a "fmul st2, st0" dcca a "fdiv st0, st1" d8f1 a "fdiv st(0), st(1)" d8f1