Speeding Up Machine-Code Synthesis
Venkatesh Srinivasan, Tushar Sharma, and Thomas Reps
Machine-code synthesis is the problem of searching for an instruction
sequence that implements a semantic specification, given as a formula
in quantifier-free bit-vector logic (QFBV). Instruction sets like
Intel's IA-32 have around 43,000 unique instruction schemas; this huge
instruction pool, along with the exponential cost inherent in
enumerative synthesis, results in an enormous search space for a
machine-code synthesizer: even for relatively small specifications,
the synthesizer might take several hours or days to find an
implementation. In this paper, we present several improvements to the
algorithms used in a state-of-the-art machine-code synthesizer
McSynth. In addition to a novel pruning heuristic, our improvements
incorporate a number of ideas known from the literature, which we
adapt in novel ways for the purpose of speeding up machine-code
synthesis. Our experiments for Intel's IA-32 instruction set show that
our improvements enable synthesis of code for 12 out of 14 formulas on
which McSynth times out, speeding up the synthesis time by at least
1981X, and for the remaining formulas, speeds up synthesis by 3X.
(Click here to access the paper:
PDF.)
University of Wisconsin