Sciweavers

Share
PLDI
2015
ACM

Synthesis of machine code from semantics

4 years 12 months ago
Synthesis of machine code from semantics
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 divideand-conquer strategy to break the input QFBV formula into independent sub-formulas, and synthesize instructions for the subformulas. 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-andconquer strategy redu...
Venkatesh Srinivasan, Thomas W. Reps
Added 16 Apr 2016
Updated 16 Apr 2016
Type Journal
Year 2015
Where PLDI
Authors Venkatesh Srinivasan, Thomas W. Reps
Comments (0)
books