int popcnt = 0; for(int mask = 1; mask; popcnt += !!(mask & value_to_compute_popcnt_of), mask <<= 1);
abcdefgh
x = ((x & 0xAA) >> 1) + (x 0x55); abcdefgh AND 10101010 -------- a0c0e0g0 SHR 1 -------- 0a0c0e0g abcdefgh AND 01010101 -------- 0b0d0f0h
wwxxyyzz
x = ((x & 0xCC) >> 2) + (x & 0x33); wwxxyyzz AND 11001100 -------- ww00yy00 SHR 2 -------- 00ww00yy wwxxyyzz AND 00110011 -------- 00xx00zz
iiiijjjj
x = ((x & 0xF0) >> 4) + (x & 0x0F); iiiijjjj AND 11110000 -------- iiii0000 SHR 4 -------- 0000iiii iiiijjjj AND 00001111 -------- 0000jjjj
mov eax, ebx and eax, 55555555h shr ebx, 1 and ebx, 55555555h add ebx, eax mov eax, ebx and eax, 33333333h shr ebx, 2 and ebx, 33333333h add ebx, eax mov eax, ebx and eax, 0F0F0F0Fh shr ebx, 4 and ebx, 0F0F0F0Fh add ebx, eax mov eax, ebx and eax, 00FF00FFh shr ebx, 8 and ebx, 00FF00FFh add ebx, eax mov eax, ebx and eax, 0000FFFFh shr ebx, 16 and ebx, 0000FFFFh add ebx, eax mov eax, ebx
popcnt eax, ebx
(* Define the x86 sequences *) let hack_sequence_x86 = (* declaration of sequence (1) as X86.x86instrpref variant types *) let popcnt_sequence_x86 = (* declaration of sequence (2) as X86.x86instrpref variant types *) (* This function converts each sequence to IR *) let make_ir_sequence x86l = List.concat (List.map (X86ToIR.translate_instr 0l) x86l) (* These bindings are the IR translations *) let hack_sequence_ir = make_ir_sequence hack_sequence_x86 let popcnt_sequence_ir = make_ir_sequence popcnt_sequence_x86 (* These bindings are the results of converting the IR sequences to SSA form *) let hack_tbl, hack_sequence_ir_ssa = IRSSA.bb_to_ssa_state_out X86ToIRUtil.num_reserved_vars hack_sequence_ir let popcnt_tbl,popcnt_sequence_ir_ssa = IRSSA.bb_to_ssa_state_out X86ToIRUtil.num_reserved_vars popcnt_sequence_ir (* The postcondition says that sequence(1).eax != sequence(2).eax *) let hack_popcnt_postcondition = IRUtil.mk_not (IRUtil.mk_eq (IRUtil.mk_evar (Hashtbl.find hack_tbl X86ToIRUtil.vEax)) (IRUtil.mk_evar (Hashtbl.find popcnt_tbl X86ToIRUtil.vEax))) (* We query the theorem prover as to whether eax from the ends of the respective sequences are equal. We do this by asking the theorem prover to generate an example where they are not equal, which it is unable to do (the formula is unsatisfiable), and therefore they are equal on all inputs. *) let _ = IDA.msg "%s\n" (Z3SymbolicExecute.symbolic_execute (Z3SymbolicExecute.mk_context ()) (hack_sequence_ir_ssa@popcnt_sequence_ir_ssa) hack_popcnt_postcondition)
mov cx, word ptr [esp] add esp, 2 ror dword ptr ss:[esp], cl pushfd
pop cx ror dword ptr ss:[esp], cl pushfd
pop eax dec dword ptr ss:[esp] pushfd
lodsd dword ptr ds:[esi] sub eax, ebx xor eax, 7134B21Ah add eax, 2564E385h xor ebx, eax movzx ax, byte ptr ds:[eax] push ax
There are 31,313 total registered users.
[+] expand