Is anyone here using Symbolic Execution for something <i>besides</i> source code verification?<p>I’m attempting to use the technique right now in the context of writing an execution tracer for a bytecode VM runtime, where I want to “recover” ABI types for arbitrary bytecode (that I don’t have the source to), in order to emit traces that describe what’s going on in high-level terms (e.g. “foo[x][y].z = 3” rather than “$329f = ($329f & (~(1 << 32) << 8)) | (%r25 & 0xff)”.)<p>So I’m doing a static-analysis pass of the bytecode (essentially a decompilation pass) which symbolically executes math ops to build up symbolic formulae representing the math being done, and to associate program-counter positions in the bytecode with value bindings in the formulae; and then I’m feeding those associations to the runtime tracer, so that it can notice when it’s on an “interesting” PC position and feed its current register/stack value into an instance of the associated formula, for me to emit once I get all the bindings of the formula filled in.<p>So far I haven’t found any texts or papers talking about using symbolic execution in this context (to recover information lost due to previous compilation, in a pass “within” a tracer, JIT, transpiler, or anything else that starts with bytecode or IR), which is kind of annoying. Anyone have any resources? Projects that use this technique? (I’m thinking that this is something you’d see done in sufficiently-advanced game-console emulators, as a “deoptimization” pass to recover structure to help dynamic recompilation optimize better.)<p>Also, related question: if I’ve got a stack machine, and <i>all</i> the jumps in the ISA are indirect jumps (but with literal values pushed on the stack), is there any way to recover the edges between basic blocks <i>without</i> doing a symbolic exec over the stack ops (i.e. to discover, among all the DUPs and SWAPs and such, which constant stack-slot the jump op is actually receiving)? I’m pretty sure there is a “weaker” method, but I’m stymied here by my lack of compiler-theory education; everything I google about dominance hierarchies and such assumes you’re starting with a model of a register machine with direct jumps (where the edges are context-free extractable from the jump ops).