article · ACM SIGPLAN Notices · 2015

Synthesis of machine code from semantics

Cited by 5Abstract and details only

Abstract

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.

Cite this paper

APA 7

Srinivasan, V., & Reps, T. (2015). Synthesis of machine code from semantics. ACM SIGPLAN Notices, 50(6), 596–607. https://doi.org/10.1145/2813885.2737960

MLA 9

Srinivasan, Venkatesh, and Thomas Reps. “Synthesis of machine code from semantics.” ACM SIGPLAN Notices, vol. 50, no. 6, 2015, pp. 596–607, https://doi.org/10.1145/2813885.2737960.

Chicago

Srinivasan, Venkatesh, and Thomas Reps. 2015. “Synthesis of machine code from semantics.” ACM SIGPLAN Notices 50 (6): 596–607. https://doi.org/10.1145/2813885.2737960.

Harvard

Srinivasan, V. and Reps, T. (2015) ‘Synthesis of machine code from semantics’, ACM SIGPLAN Notices, 50(6), pp. 596–607. Available at: https://doi.org/10.1145/2813885.2737960.

BibTeX

@article{srinivasan2015synthesis,
  title = {{Synthesis of machine code from semantics}},
  author = {Srinivasan, Venkatesh and Reps, Thomas},
  journal = {ACM SIGPLAN Notices},
  volume = {50},
  number = {6},
  pages = {596--607},
  year = {2015},
  doi = {10.1145/2813885.2737960}
}

Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.