Peek is a first step toward adding support for assembly-level program analyses, transformations, and optimizations in CompCert. Currently, Peek focuses on x86 peephole transformations implemented and verified in Coq. Peek is designed to provide a modular interface requiring that each peephole optimization satisfy only local correctness properties. Our primary result establishes that, assuming the C calling convention, any peephole optimization satisfying these local properties preserves global program meaning.
[ bib | project | paper ] Back
This file was generated by bibtex2html 1.97.