(author here.) I started the x86-sat project about a week ago, which parses Intel's pseudocode for all of the intrinsic functions and converts it into a Z3 SAT model. I got a basic prototype working in around a day, and I've done some cool things with it since.
The next logical step was obviously writing a superoptimizer. You provide it with a whitelist of intrinsics to search over, a set of inputs, a set of free variables (for things like creating constants/lookup tables), and an output, and it will recursively search over all applications of the intrinsics to find the shortest instruction sequence. This is still a toy at this point, so don't expect any miracles.
1 comment
[ 4.0 ms ] story [ 10.1 ms ] threadThe next logical step was obviously writing a superoptimizer. You provide it with a whitelist of intrinsics to search over, a set of inputs, a set of free variables (for things like creating constants/lookup tables), and an output, and it will recursively search over all applications of the intrinsics to find the shortest instruction sequence. This is still a toy at this point, so don't expect any miracles.