[russellsprouts]

Very cool!

I did something related in the past: https://github.com/RussellSprouts/6502-enumerator. It uses C++ templates to share an emulator implementation between z3-powered symbolic execution and actual execution. It was meant to find equivalence between random instruction sequences for peephole optimization, rather than optimizing a specific input sequence.

Shadow instructions are very interesting and cursed. I've seen them used in very limited circumstances for NOP-slides for timing code: https://www.pagetable.com/?p=669. It would be fun to see it applied in otherwise normal code. My enumerator wouldn't support this -- it didn't execute actual 6502 instructions from bytes -- it had its own internal representation for `the first arbitrary absolute pointer` or `the second arbitrary immediate constant`. These would either be initialized with random concrete values or z3 variables.

[Aransentin]

Your project was very much something I looked into when designing this! Fun to see you commenting.

But yes, different goals. I did look into using z3, but quickly found out that it's pretty slow compared to just checking if a test case passes when ran through the candidate program.

[guenthert]

Interesting project and well written. That only made me miss some links to prior art more though.

iirc, there was a superoptimizer (I belief the term was coined and motivated in that article) in the early nineties for M68k. https://dl.acm.org/doi/pdf/10.1145/36206.36194 might have been that.