Skip to content

Instantly share code, notes, and snippets.

@whitequark

whitequark/concolic.py

Last active April 18, 2025 11:25
Show Gist options
  • Save whitequark/e8c7ffab0208d1b033aae715488881d6 to your computer and use it in GitHub Desktop.
Save whitequark/e8c7ffab0208d1b033aae715488881d6 to your computer and use it in GitHub Desktop.
Download ZIP
concolic execution engine written for https://crackmes.one/crackme/67f9bdc38f555589f3530a85
Raw
concolic.py
# /// script
# requires-python = "~=3.11"
# dependencies = [
# "colored==2.3.0",
# "z3-solver==4.14.1.0"
# ]
# ///
import os
import sys
import code
import traceback
import readline
import datetime
import z3
import colored as cl
from data import vm_code, vm_data
from parse import parse, disasm
def meow(locals):
print()
code.InteractiveConsole(locals).interact()
key = [z3.BitVec(f'k{n:02x}', 8) for n in range(0x20)]
goal = 0x30b # 'Welcome home :)'
fail = 0x31c # 'Have you forgotten it :('
pc = 0x169
# uncomment this to make it work; lack of state merging makes starting at 0x169 require
# a search of like 6**32 states, most of which are unsat
pc = 0x18e
fl = False, False, -1
reg = [(0, -1) for _ in range(0x10)]
reg[4] = (0x20, -1)
mem = [(b, -1) for b in vm_data]
mem[0x40:0x60] = [(b, -1) for b in key]
# mem[0x40:0x60] = [(z3.BitVecVal(b, 8), -1) for b in b"()v3Ng34nce_I5_4n_1D10T5_g4m3_()"]
# mem[0x40:0x60] = [(b, -1) for b in b"()v3Ng34nce_I5_4n_1D10T5_g4m3_()"]
# mem[0x40] = (z3.BitVecVal(ord('('), 8), -1)
stp = 0
out = ""
sym = set()
act = set()
stack = [
(pc, fl, reg, mem, stp, act)
]
hashes = set()
solver = z3.SolverFor("QF_BV") # actually faster than the default!
def bind(val):
return val
const = z3.FreshConst(val.sort())
solver.add(const == z3.simplify(val))
return const
def format_val(val, fmt="", slow=os.getenv("VERBOSE") is not None):
if isinstance(val, int):
return format(val, fmt)
elif slow:
# val = z3.simplify(val)
if isinstance(val, z3.BitVecNumRef):
return f"{val.as_long():{fmt}}"
else:
return f"{val.sexpr()}"
else:
return f"{{...}}"
smt2 = []
def add_smt2():
smt2.append(list(act))
def save_smt2():
with open("concolic.smt2", "w") as f:
f.write(f"(set-option :produce-models true)\n")
f.write(f"(set-logic QF_BV)\n")
f.write(solver.to_smt2().replace("(check-sat)\n", ""))
for act in smt2:
f.write(f"(check-sat-assuming ({' '.join(map(lambda x: x.sexpr(), act))}))\n")
f.write(f"(get-value ((concat {' '.join(map(lambda x: x.sexpr(), key))})))\n")
def solve_with(active):
return solver.check(*act)
def get_key():
try:
model = solver.model()
except:
return ""
chars = ""
for bv in key:
k = z3.simplify(model[bv])
if isinstance(k, z3.BitVecNumRef):
chars += chr(k.as_long())
else:
chars += "."
return chars
def execute(pc, step, instr):
global fl, reg, mem, stp, act, key
# for val, val_pc in reg:
# if isinstance(val, int):
# assert val in range(0, 0x100000000)
# elif isinstance(val, z3.BitVecRef):
# assert val.size() == 32
# else:
# assert False, f"Invalid type {val!r}"
# for val, val_pc in mem:
# if isinstance(val, int):
# assert val in range(0, 0x100)
# elif isinstance(val, z3.BitVecRef):
# assert val.size() == 8
# else:
# assert False, f"Invalid type {val!r}"
opcode, modeA, operA, modeB, operB = parse(instr)
if modeA == 0:
def getA():
val, pc = reg[operA]
if isinstance(val, z3.BitVecRef):
assert val.size() == 32
print(f"\tr{operA:X}\t= {format_val(val, '08x')} ; from {pc:x}")
return val
def setA(val):
if isinstance(val, z3.BitVecRef):
assert val.size() == 32
elif isinstance(val, int):
val = val & 0xffffffff
print(f"\t{cl.Fore.red}r{operA:X}\t← {format_val(val, '08x')}{cl.Style.reset}")
reg[operA] = val, pc
elif modeA == 1:
def getA():
val, pc = mem[operA]
if isinstance(val, z3.BitVecRef):
assert val.size() == 8
val = z3.ZeroExt(24, val)
print(f"\t[{operA:X}]\t= {format_val(val, '02x')} ; from {pc:x}")
return val
def setA(val):
if isinstance(val, z3.BitVecRef):
assert val.size() == 32
val = bind(z3.Extract(7, 0, val))
elif isinstance(val, int):
val = val & 0xff
print(f"\t{cl.Fore.red}[{operA:02X}]\t← {format_val(val, '02x')}{cl.Style.reset}")
mem[operA] = val, pc
else:
assert False, "Undefined modeB"
if modeB == 0:
def getB():
val, pc = reg[operB]
if isinstance(val, z3.BitVecRef):
assert val.size() == 32
print(f"\tr{operB:X}\t= {format_val(val, '08x')} ; from {pc:x}")
return val
elif modeB == 1:
def getB():
val, pc = mem[operB]
if isinstance(val, z3.BitVecRef):
assert val.size() == 8
val = z3.ZeroExt(24, val)
print(f"\t[{operB:X}]\t= {format_val(val, '02x')} ; from {pc:x}")
return val
elif modeB == 2:
def getB():
return operB
else:
assert False
match opcode:
case 0x0: # mov
setA(getB())
case 0x1: # movi
valB = getB()
if modeA == 0:
if isinstance(valB, int):
val, val_pc = mem[valB]
if isinstance(val, int):
setA(val)
else:
setA(z3.ZeroExt(24, val))
else:
addr = z3.Extract(7, 0, valB)
if True:
all_mem = z3.Concat(*[
z3.BitVecVal(val, 8) if isinstance(val, int) else val
for val, val_pc in reversed(mem)
])
data = z3.Extract(7, 0, z3.LShR(all_mem,
z3.Concat(z3.ZeroExt(8 * 255 - 3, addr), z3.BitVecVal(0, 3))))
elif True:
addr = z3.simplify(addr)
assert addr.decl().name() == 'concat'
assert addr.arg(0).as_long() == 8
assert addr.arg(0).size() == 4
all_mem = z3.Concat(*[
z3.BitVecVal(val, 8) if isinstance(val, int) else val
for val, val_pc in reversed(mem[0x80:0x90])
])
addr = z3.Extract(3, 0, addr)
data = z3.Extract(7, 0, z3.LShR(all_mem,
z3.Concat(z3.ZeroExt(8 * 15 + 1, addr), z3.BitVecVal(0, 3))))
else:
addr = z3.simplify(addr)
assert addr.decl().name() == 'concat'
assert addr.arg(0).as_long() == 8
assert addr.arg(0).size() == 4
data = z3.BitVecVal(0, 8)
for idx, (val, val_pc) in enumerate(mem):
if idx in range(0x80, 0x90):
data = z3.If(addr == idx, val, data)
setA(z3.ZeroExt(24, data))
elif modeA == 1:
addr, addr_pc = mem[operA]
assert isinstance(addr, int)
print(f"\t[{format_val(addr, '02X')}]\t= {format_val(valB, '02x')}")
if isinstance(valB, int):
mem[addr] = valB, pc
else:
mem[addr] = bind(z3.Extract(7, 0, valB)), pc
case 0x2: # add
setA(getA() + getB())
case 0x3: # sub
setA(getA() - getB())
case 0x4: # mul
assert False, "Multiplication never actually used"
setA(getA() * getB())
case 0x5: # mod
valA, valB = getA(), getB()
assert bin(valB).count("1") == 1, "(Non-power-of-2) modulo never actually used"
if isinstance(valA, int) and isinstance(valB, int):
setA(valA % valB)
else:
setA(z3.URem(valA, valB))
case 0xb: # and
setA(getA() & getB())
case 0xc: # or
setA(getA() | getB())
case 0xd: # xor
setA(getA() ^ getB())
case 0xe: # shl
setA(getA() << getB())
case 0xf: # ushr
valA, valB = getA(), getB()
if isinstance(valA, int) and isinstance(valB, int):
setA(valA >> valB)
else:
setA(z3.LShR(valA, valB))
case 0x6: # write
assert modeA == 1 and modeB == 2
# chars = chr(getA()) * getB()
# print(f" write\t{chars!r}")
case 0x7: # read
assert modeA == 1 and modeB == 0
for offset in range(getB()):
key.append(val := z3.BitVec(f'k{offset:02x}', 8))
print(f" [{operA + offset:02x}]\t= {val!r}")
# solver.add((val >= 0x30) & (val <= 0x39))
# mem[operA + offset] = val, pc
mem[operA + offset] = z3.BitVecVal(b"()v3Ng34nce_I5_4n_1D10T5_g4m3_()"[offset], 8), pc
# solver.add(key[0] == 0x33)
# solver.add(key[1] == 0x32)
# solver.add(z3.Concat(*key) == int.from_bytes(b"()v3Ng34nce_I5_4n_1D10T5_g4m3_()"))
case 0x9: # cmp
valA, valB = getA(), getB()
fl_eq = (valA == valB)
if isinstance(valA, int) and isinstance(valB, int):
fl_lt = (valA < valB)
else:
fl_lt = z3.ULT(valA, valB)
print(f"\tfl\t← {format_val(fl_eq, 'd')}, {format_val(fl_lt, 'd')}")
fl = fl_eq, fl_lt, pc
case 0xa: # br
fl_eq, fl_lt, fl_pc = fl
match getB():
case 0x40:
taken = True
case 0x20:
taken = False
case 0x04:
print(f"\tfl.lt\t= {format_val(fl_lt, 'd')} ; from {fl_pc:x}")
taken = fl_lt
case 0x02:
print(f"\tfl.eq\t= {format_val(fl_eq, 'd')} ; from {fl_pc:x}")
print(f"\tfl.lt\t= {format_val(fl_lt, 'd')} ; from {fl_pc:x}")
if isinstance(fl_eq, bool) and isinstance(fl_lt, bool):
taken = not fl_lt and not fl_eq
else:
taken = z3.And(z3.Not(fl_lt), z3.Not(fl_eq))
case 0x01:
print(f"\tfl.eq\t= {format_val(fl_eq, 'd')} ; from {fl_pc:x}")
taken = fl_eq
case _:
assert False, "Branch condition must be one-hot immediate"
target = getA()
if isinstance(taken, z3.BoolRef):
print(f" {cl.Fore.cyan}split {format_val(taken)} "
f"(t={target:x} f={pc + 1:x}){cl.Style.reset}")
sym.add(act_t := z3.Bool(f"{step}:{pc:x}#t"))
solver.add(z3.Implies(act_t, taken == True))
stack.append((target, fl, list(reg), list(mem), stp + 1, {*act, act_t}))
sym.add(act_f := z3.Bool(f"{step}:{pc:x}#f"))
solver.add(z3.Implies(act_f, taken == False))
stack.append((pc + 1, fl, list(reg), list(mem), stp + 1, {*act, act_f}))
return
assert isinstance(taken, bool)
if taken:
color = cl.Fore.yellow if target > pc else cl.Fore.magenta
print(f"\t{color}pc\t← {target:x}{cl.Style.reset}")
return target
return pc + 1
# c == 0x28
# c == 0x29
# c == 0x5f
# 0x7a - c < 0x1a : c > 0x60
# 0x5a - c < 0x1a : c > 0x40
# 0x39 - c < 0x0a : c > 0x30
# goal = 0x187
result = []
while stack:
pc, fl, reg, mem, stp, act = stack.pop()
header = ' '.join(sorted((f'{var}' for var in act), key=lambda s: int(s.split(':')[0])))
print(f"\n{cl.Fore.cyan}{{{header}}}{cl.Style.reset}")
# if solve_with(act) == z3.sat:
# print(f' {cl.Fore.hot_pink_2}{cl.Style.bold}sat {get_key()}{cl.Style.reset}')
while True:
# if pc in range(0x2ad, 0x30a, 3):
# add_smt2()
# if pc == 0x2ad: save_smt2("concolic1.smt2"); #pc = 0x30a
# if pc == 0x2b0: save_smt2("concolic2.smt2"); #pc = 0x30a
# if pc == 0x2b3: save_smt2("concolic3.smt2"); #pc = 0x30a
# if pc == 0x2b6: save_smt2("concolic4.smt2"); #pc = 0x30a
instr = vm_code[pc]
print(f"{stp}:\t{cl.Fore.green}{disasm(pc, *parse(instr))}{cl.Style.reset}\t"
f"; bn: {0x100+(pc<<2):x}; stack: {len(stack)}")
if pc == goal:
print(f"\t {cl.Fore.white}goal{cl.Style.reset}")
add_smt2(); save_smt2()
# print(mem[0x40][0].sexpr())
result = solve_with(act)
print(f"{result} {get_key()!r}")
if result == z3.sat:
stack.clear()
break # success
else:
break # impossibility
if pc == fail:
print(f"\t {cl.Style.bold}fail{cl.Style.reset}")
break # failure
pc = execute(pc, stp, instr); stp += 1
if pc is None:
break
for line_addr in range(0x40, 0x60, 0x20):
print(f"{line_addr:02x} |", end="")
for byte_addr in range(line_addr, line_addr + 0x20):
byte, byte_pc = mem[byte_addr]
if z3.is_bv_value(byte):
byte = z3.simplify(byte)
if z3.is_const(byte):
byte = byte.as_long()
if isinstance(byte, int):
print(f" {byte:02x}", end="")
else:
print(f" ??", end="")
print()
Raw
data.py
vm_code = [995601494, 961915476, 3635759284, 241344097, 2330401257, 3184602320, 592360013, 3652537271, 3736293042, 2748265408, 7115374, 2714579148, 1881006354, 1678374667, 1127142191, 3917838728, 3299366572, 460819062, 1981540116, 1227151904, 3635759284, 2330335980, 1981538330, 3249296301, 124491626, 1260837671, 1028762962, 1546702397, 1227217188, 3449839009, 2582972918, 3266203823, 3502064060, 1429783865, 726055493, 792903497, 460818805, 276660604, 2731422671, 4271009425, 4018372232, 224435810, 3619309243, 1011920209, 2865183684, 327123574, 1429849402, 1611461133, 4204161687, 3901061252, 575648588, 2048322333, 2246645738, 2764584393, 3518841278, 828219482, 1210374183, 2632977393, 928687448, 2798270155, 4271009683, 3316143275, 2815112646, 2616593143, 1045671506, 23892079, 460818806, 2014701844, 642496074, 845062749, 1028763484, 3934747526, 3399900071, 3817763469, 3466747055, 2263554026, 124491370, 625521739, 3619374524, 2380274913, 1346158909, 1327685153, 2566130421, 527667058, 4237323665, 2967282142, 73963109, 3201445587, 1728837130, 1881006366, 3383057312, 1310973730, 3967843713, 3518841278, 4170542740, 2482962684, 2932031426, 1761998855, 1396621885, 1761933824, 4271074962, 642496328, 2748264907, 4137379482, 1981540120, 2881894596, 7114861, 2649820400, 2666663673, 592425290, 1761999108, 3934681991, 1546701883, 3834214284, 2666663667, 3184602320, 3518841264, 74028136, 327057532, 2213417711, 1310908195, 1244125996, 3817762955, 1678374152, 224435553, 3585689010, 3117754580, 1293998881, 1580452918, 427067509, 4154091416, 4036780191, 1277222434, 1862467331, 2229868012, 2449277951, 7115117, 4103693722, 3184537299, 1745156101, 1244060455, 1227217190, 393971324, 3753004212, 3232584108, 3249295789, 928687705, 4237388950, 90740334, 541962572, 1062448722, 4187318678, 2466185974, 3951524227, 1695151368, 1260902950, 2566129911, 961849683, 1998251036, 4254100625, 1914626847, 1110430508, 2881960641, 2633043442, 4154089883, 2449277690, 1778907910, 140810598, 2683440881, 2397249250, 310280829, 2748199887, 1260903204, 3702607024, 3801052044, 1379844154, 592360015, 3834213512, 1160369450, 3518841776, 258187106, 393906043, 410290295, 3784143744, 709344070, 3850925449, 2666663665, 811377233, 2983993565, 310281087, 1611526414, 3901062024, 3767300237, 2380340448, 327058045, 3784143753, 3502064060, 3552527037, 157587559, 4221004950, 3449839529, 659207755, 174496612, 2098261014, 327123581, 1227151393, 1628238345, 2313492964, 1862467331, 3034064091, 3282981027, 3901061508, 2566195444, 1645212428, 1828781581, 4237323409, 3416742566, 3349829289, 1076679201, 2632977649, 3316143529, 4170541462, 3669379259, 3333052075, 1964565785, 3333052073, 1479920432, 1897717789, 3383056551, 2848209095, 477137777, 2397183465, 3801052046, 1346158910, 3602532025, 1981539609, 2831431877, 978823765, 978758229, 2115235093, 90739817, 3316143529, 3266204321, 4287786131, 2865183686, 3767300493, 878224471, 1143592744, 3518775485, 861840223, 1661923853, 4287786143, 1045671762, 3050906840, 2229802215, 2246645736, 1011985744, 3917773189, 2263488233, 3552460984, 1998317338, 675592518, 1661989644, 2229801961, 2466120179, 3201511378, 608744779, 3801051531, 2179797484, 4070466461, 1914691864, 1045671762, 3736227773, 2616658421, 3017679583, 3568846263, 2984059871, 1745221892, 3767300495, 1210440491, 1463469627, 377128821, 978757716, 3333052075, 1127142189, 1761933836, 3702541489, 3702607026, 709344326, 642430244, 1496582709, 1260791591, 4187261589, 3483600034, 2649821168, 3266225583, 3984631937, 3201497043, 3151429335, 3502015421, 4220939671, 124412267, 343429241, 1728785418, 659254090, 995600470, 2948788163, 3552484543, 2714561229, 3901070212, 510889074, 124407147, 3201563602, 1045605715, 4187339156, 3619333304, 1546701105, 3184537553, 1210399268, 1914647582, 3767381900, 541938508, 4070553758, 3050947800, 2098259985, 845128798, 393965690, 1931411742, 2065054487, 2599815671, 895055704, 3067803355, 4254166672, 276648316, 3067802587, 1310932258, 477195120, 2599932918, 2865182918, 2162999789, 1761944580, 894977625, 541962828, 3535770558, 776099907, 3884685194, 3502020541, 293430140, 895042648, 3719384752, 2499399928, 1412962617, 1778789639, 3399924903, 40846190, 3535708351, 592360527, 3767301005, 168692270, 225719408, 4254100369, 2038264189, 1482511266, 2393547821, 791356628, 2945090933, 2709818235, 1281910647, 3183001336, 406404917, 420023311, 4167724884, 347127473, 2839166725, 2684619269, 883336024, 3227806309, 2223408309, 1097888373, 2839363367, 1240261352, 3284189913, 655824146, 4033111678, 2684685057, 2054715973, 740040217, 529238401, 629182084, 1033410520, 791291093, 523908277, 488118247, 2759888875, 2069779039, 2449673991, 3614670194, 2954107732, 3284584505, 991826060, 707732271, 1516133630, 3454856928, 453708553, 2979305092, 2190644112, 3972647897, 3790150123, 499961037, 152166673, 4225749982, 3378336077, 2216767269, 4025149930, 1482447964, 2998319798, 4109694452, 3688878815, 622930537, 507393341, 2444278717, 3519070923, 842216753, 2518885843, 3057796166, 774842413, 45527481, 404494300, 1383299186, 1885365355, 3974685567, 2544283051, 891560239, 1049594762, 1566136230, 3404718378, 960312002, 3353537836, 800833467, 2436184884, 83887232, 840111893, 3369655004, 3631050594, 2907261773, 1785621230, 2225447330, 975843118, 2127285819, 1637126544, 854847990, 2869887055, 100861827, 3888562880, 1719039090, 78754625, 3873695587, 35858212, 2643233160, 3019900175, 4282334522, 1364480148, 4292795102, 4192792044, 1401061511, 2341179273, 2442499989, 3048256800, 4058048229, 2302230333, 1788844444, 955841278, 3854681280, 1702196080, 1708446416, 769253341, 1351651990, 237645611, 3502294725, 11581108, 3661576509, 2825415278, 220802088, 3013780647, 3714869864, 82966512, 837940215, 2427761077, 85267216, 2268475442, 2237687394, 1267370124, 2709815685, 102109203, 2418026020, 1922470034, 703130350, 1041964570, 3653881804, 580097431, 2188800119, 96847811, 570884614, 2121164907, 2569613101, 4111472145, 4113839666, 2055107902, 856889360, 740827832, 1987279595, 387128812, 3097334626, 389168142, 3570782680, 507133501, 3853628857, 3655127843, 3606313996, 705626116, 4014687499, 909587258, 3690986489, 3565258121, 1599755685, 1180855709, 3336760816, 1067161051, 4059100413, 2996212372, 4054098092, 2324660336, 2878243185, 2393548211, 397655539, 3183327664, 975117086, 3649931653, 218630135, 2979371626, 3029442225, 1358298037, 4160156411, 1130783331, 2868837110, 4244239878, 2241900383, 873471799, 347193329, 1027422512, 1816677448, 1175656219, 3081944397, 3336760605, 1732463725, 10791652, 2391706243, 2427826614, 3955211191, 505026021, 2928313717, 389233670, 3632034364, 3772835053, 991894299, 3649931653, 3435775542, 3046154095, 36055402, 1976622736, 151522570, 2459145624, 1366390645, 3199117480, 792672309, 2643297668, 3489727495, 2026491086, 1759109073, 4164435262, 2576375963, 3013307295, 1736413050, 3871525059, 3589404912, 1240261548, 4227854592, 2258873692, 2613031403, 3173590062, 1155657696, 1593570809, 3180960152, 1664497190, 2829886035, 237708680, 322321207, 1643510013, 983470234, 774582123, 2861207177, 151849029, 3707566591, 808728884, 353443822, 2326765904, 1231839757, 169483294, 992619823, 2829144485, 824826158, 17430796, 2191157916, 305541687, 3269911527, 2878309006, 2028855525, 3227872097, 2964634187, 4124106353, 2911405193, 3746186842, 3206157342, 993933950, 1816938575, 1044070003, 1901155410, 1229734220, 556018395, 2208803160, 1985109035, 3199183275, 2898115256, 1887013245, 3385926102, 1364764765, 402780423, 2053003871, 4192000477, 3741054714, 4033112428, 145597353, 3537296342, 707731920, 1197698460, 3707303536, 319952415, 2679881650, 2885614318, 1094992260, 3097074836, 690760444, 2225382048, 3064439714, 1465822808, 2676389506, 3164116377, 360746384, 1993530582, 3503675605, 757671894, 3471500309, 2208737343, 2677776219, 2629679536, 3672038158, 3972909248, 152575517, 4110224889, 3353292761, 423440444, 2232491009, 3846196804, 2542967917, 3939418193, 2241962673, 3746187626, 2044580825, 1296582327, 1215128466, 570886648, 1968267086, 3662022298, 1475542256, 397655479, 549256659, 3846196802, 4267332702, 3227328267, 111390113, 1441923061, 1827713842, 1458765040, 1841874636, 4084149180, 1926748629, 347127476, 445039560, 2785152000, 865507474, 3545106462, 1033475995, 3531045235, 3966842374, 3897377615, 2419407665, 1760869533, 262907305, 2886206988, 43964204, 10791590, 2044515032, 2467185731, 1441923059, 532395455, 10344052, 3846196802, 2604544058, 1878245244, 1358232310, 1425080052, 1088262184, 680297102, 44542371, 934012294, 2335055916, 2902984204, 1322491073, 10857383, 44476578, 2600883756, 881893010, 815111057, 2283095168, 2027803615, 3829419588, 3377792980, 562334342, 3514071664, 3377727409, 3564142194, 1375009520, 3156309268, 1274012141, 747144844, 2249936576, 1290397675, 3227872097, 478271243, 4200550749, 2819359240, 1017247409, 2469804084, 612470661, 1456182239, 3547756660, 229156524, 4217847448, 3071417360, 4250490717, 4017236181, 1492972286, 1707200453, 934015151, 596019332, 2801995015, 1539742230, 2987858197, 2401969455, 1961407785, 3665719420, 4183642969, 934016334, 714047885, 3429459821, 1844555397, 713982092, 3155695132, 2368218632, 3753026739, 527592563, 2213465071, 1828723713, 2881941191, 2948785347, 2483020286, 2163020524, 2330445542, 811365469, 4287804563, 1429743161, 3635759796, 224434785, 2031364885, 3084591321, 0, 3753096370, 293431164, 3017732575, 4220946583, 1362936637, 2649867248, 327112574, 1778854150, 1127141679, 3249320877, 861894494, 3266282670, 241386338, 174542694, 4154177177, 1396580415, 3151426007, 3117689813, 4271092114, 1947808792, 1227152165, 845129054, 3151423703, 3884609928, 0, 0]
vm_data = b'ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789()\xd4\xce\xccmf\xa4\xa6\x97.^\xa0D\xd6\x8b\xc5dl\x04\xc6B>_\x10\x83IJ}\xb0\xdb\x85\x165\xcc<\xb4\xf1\xb5\xb7\x9a\xa3\x14\xcb%U~\xbe\x84n\xbb\xa4\x8e\x9c=\x96\xc2\xd8\xa8DY\x03vm\x05$\xc7\xf2~\xa9\xe3\xdb\xb0\x04,m1\x1a\x96OX\x85\x80@ \x10\x08\x04\x02\x01\x7f\xbf\xdf\xef\xf7\xfb\xfd\xfe\x14\xd6\x8c\x9e\x0c\x80\xcf\x909\xe2\x86C\x16\xf7\x84\x18R*\xefs\xaa\xc1H\xe1\xe5o\xc6\xdf\xcc\x96^\x02\xb5\xab\xe7\x8f&\xe7\x99O\x84\x8f\x97\xe2\x1a\xed\xaeK(D\xd8\x1b\x83b\x05\xfb\xd5k#\x86\x06\xe4\xc7\xce\xdd}\x8c\x18#\x11\xb2\xec\xfa\x8e\xfe\x16\xc6pl"\x008\xe0\x97\xbfO\xe6\xa8.,:\n\\/_ '
Raw
parse.py
def parse(instr):
instr = 0xffffffff & ((((instr >> 0x10) & 0xff) * 0x1010101) ^ instr)
opcode = instr >> 0x1c
modeA = (instr >> 0x1b) & 1
operA = (instr >> 8) & 0xff
modeB = (instr >> 0x19) & 3
operB = (instr >> 0) & 0xff
# print(f"{instr:08x}: op={opcode:1x} mA={modeA} rA={operA} mB={modeB} rB={operB}")
return (opcode, modeA, operA, modeB, operB)
mnemonics = "mov movi add sub mul mod write read und cmp br and or xor shl ushr".split()
def disasm(addr, opcode, modeA, operA, modeB, operB):
if modeA == 0:
dst = f"r{operA:X}"
elif modeA == 1:
dst = f"[{operA:02X}]"
if modeB == 0:
src = f"r{operB:X}"
elif modeB == 1:
src = f"[{operB:02X}]"
elif modeB == 2:
src = f"{operB:02X}"
if opcode == 0x1:
if modeA == 0:
src = f"[{src}]"
elif modeA == 1:
dst = f"[{dst}]"
return f"{addr:<5x} {mnemonics[opcode]:8} {dst:8} {src}"
if __name__ == "__main__":
from data import vm_code
for addr, instr in enumerate(vm_code):
print(disasm(addr, *parse(instr)))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment