In a modern instruction set like x86-64 there are many many many ways to accomplish the same task using a series of old simple instructions all the way up to the complex SIMD instructions. If one wanted to determine the semantic equivalence of a series of instructions, could this be done rationally or must it only be done experimentally?
For the sake of simplicity I am restricting the number of instructions in a series to something like ten.
The naive way to solve the problem would be to generate all of the potential inputs and experimentally check the results.
A slightly smarter way might be to determine the edges of the input states and only test those.
But I'm wondering if there's a way to represent each of the assembly instructions (and series of instructions) as a data structure that could be compared. Is this a tractable problem? Or is this clearly something like the halting problem?
Intuitively this feels like something similar to what happens inside a compiler.