-rwxr-xr-x 2095 djbsort-20260127/sortverif/outsim raw
#!/usr/bin/env python3

import sys

binary = sys.argv[1]
libs = sys.argv[2:]

import angr

add_options = {
  angr.options.LAZY_SOLVES,
  angr.options.SYMBOLIC_WRITE_ADDRESSES,
  angr.options.CONSERVATIVE_READ_STRATEGY,
  angr.options.CONSERVATIVE_WRITE_STRATEGY,
  angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
  angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS,
}
remove_options = {
  angr.options.SIMPLIFY_CONSTRAINTS,
  angr.options.SIMPLIFY_EXPRS,
  angr.options.SIMPLIFY_MEMORY_READS,
  angr.options.SIMPLIFY_MEMORY_WRITES,
  angr.options.SIMPLIFY_REGISTER_READS,
  angr.options.SIMPLIFY_REGISTER_WRITES,
  angr.options.SIMPLIFY_RETS,
}

# ===== patch cpuid to enable avx2
# XXX: should share with unroll; in any case keep synchronized

prevcpuid = angr.engines.vex.heavy.dirty.CORRECT_amd64g_dirtyhelper_CPUID_avx_and_cx16

def cpuid(state,_):
  eax = state.regs.rax[31:0]
  prevcpuid(state,_)
  # substitute some haswell cpuid data:
  state.registers.store('rax',0x000306c3,size=8,condition=(eax==1))
  state.registers.store('rbx',0x04100800,size=8,condition=(eax==1))
  state.registers.store('rcx',0x7ffafbff,size=8,condition=(eax==1))
  state.registers.store('rdx',0xbfebfbff,size=8,condition=(eax==1))
  state.registers.store('rax',0x00000000,size=8,condition=(eax==7))
  state.registers.store('rbx',0x000027ab,size=8,condition=(eax==7))
  state.registers.store('rcx',0x00000000,size=8,condition=(eax==7))
  state.registers.store('rdx',0x9c000600,size=8,condition=(eax==7))
  return None,[]

angr.engines.vex.heavy.dirty.amd64g_dirtyhelper_CPUID_avx2 = cpuid

# ===== main

proj = angr.Project(binary,auto_load_libs=False,force_load_libs=libs)
state = proj.factory.full_init_state(add_options=add_options,remove_options=remove_options)
simgr = proj.factory.simgr(state)
simgr.run()
exits = simgr.deadended
assert len(exits) == 1

for p in exits[0].posix.stdout.content:
  assert p[1].op == 'BVV'
  n = p[1].args[0]
  assert p[0].op == 'BVV'
  assert p[0].size() == 8*n
  data = p[0].args[0]
  sys.stdout.buffer.write(bytes(bytearray([255&(data>>(8*i)) for i in reversed(range(n))])))