Synthesis of Machine Code from Semantics
Venkatesh Srinivasan† and Thomas Reps†,‡
In this paper, we present a technique to synthesize machine-code
instructions from a semantic specification, given as a
Quantifier-Free Bit-Vector (QFBV) logic formula.
Our technique uses an instantiation of the Counter-Example Guided
Inductive Synthesis (CEGIS) framework, in combination
with search-space pruning heuristics to synthesize
instruction-sequences. To counter the exponential cost inherent in
enumerative synthesis, our technique uses a divide-and-conquer
strategy to break the input QFBV formula into independent sub-formulas,
and synthesize instructions for the sub-formulas. Synthesizers
created by our technique could be used to create semantics-based
binary rewriting tools such as optimizers, partial evaluators,
program obfuscators/de-obfuscators, etc.
Our experiments for Intel's IA-32 instruction set show that, in
comparison to our baseline algorithm, our search-space pruning
heuristics reduce the synthesis time by a factor of 473, and our
divide-and-conquer strategy reduces the synthesis time by a further 3
to 5 orders of magnitude.
(Click here to access the paper:
PDF.)
†University of Wisconsin
‡GrammaTech, Inc.