Note: see also compilers
DeepFuzz: Automatic Generation of Syntax Valid C Programs for Fuzz Testing Xiao Liu, Xiaoting Li, Rupesh Prajapati, Dinghao Wu College of Information Sciences and Technology The Pennsylvania State University University Park, PA 16802, USA Abstract Compilers are among the most fundamental programming tools for building software.
- Testing
- ACM SIGPLAN Conference on Certified Programs and Proofs (CPP) - http://dblp.org/db/conf/cpp/
- Black-Box Equivalence Checking Across Compiler Transformations
- 2018 PhD thesis; Manjeet Dahiya
- Compiling with Proofs
- 1998 Ph.D. Thesis; George C. Necula
- Formal Approaches to Secure Compilation: A Survey of Fully Abstract Compilation and Related Work
- ACM Computing Surveys (CSUR) 51(6) 2019
- Marco Patrignani, Amal Ahmed, Dave Clarke
- How to prove a compiler correct - Daniel Patterson
- Operational Refinement for Compiler Correctness
- 2012 PhD Dissertation; Robert W. Dockins
- ftp://ftp.cs.princeton.edu/reports/2012/936.pdf
- OPLSS (Oregon Programming Languages Summer School)
- 2019 - https://www.cs.uoregon.edu/research/summerschool/summer19/topics.php
- Secure Compilation - Amal Ahmed
- 2017 - https://www.cs.uoregon.edu/research/summerschool/summer17/topics.php
- Correct and Secure Compilation for Multi-Language Software - Amal Ahmed
- 2016 - https://www.cs.uoregon.edu/research/summerschool/summer16/curriculum.php
- Logical relations/Compiler verification - Amal Ahmed
- 2015 - https://www.cs.uoregon.edu/research/summerschool/summer15/curriculum.html
- Logical Relations - Amal Ahmed
- 2014 - https://www.cs.uoregon.edu/research/summerschool/summer14/curriculum.html
- Software Verification - Andrew Appel
- 2013 - https://www.cs.uoregon.edu/research/summerschool/summer13/curriculum.html
- Logical Relations - Amal Ahmed
- Verifying LLVM Optimizations in Coq - Steve Zdancewic
- 2012 - https://www.cs.uoregon.edu/research/summerschool/summer12/curriculum.html
- Logical Relations - Amal Ahmed
- Compiler verification - Xavier Leroy
- 2019 - https://www.cs.uoregon.edu/research/summerschool/summer19/topics.php
- What even is compiler correctness? - https://www.williamjbowman.com/blog/2017/03/24/what-even-is-compiler-correctness/
- Write Your Compiler by Proving It Correct - http://liamoc.net/posts/2015-08-23-verified-compiler.html
History
![Generation Generation](/uploads/1/2/5/5/125537138/274276099.png)
- Compiler Verification: A Bibliography
- ACM SIGSOFT Software Engineering Notes 28(6) 2003
- Maulik A. Dave
- Compiler Verification: A Brief History - http://web.archive.org/web/20090807085152/http://www.geocities.com/compiler00/dave1.html
- Correctness of a Compiler for Algol-like Programs
- Stanford Artificial Intelligence Memo No. 48 (1967)
- Donald M. Kaplan
- Correctness of a Compiler for Arithmetic Expressions
- Mathematical Aspects of Computer Science (1) 1967
- John McCarthy and James A. Painter
- Dagstuhl Seminar 17502 – Testing and Verification of Compilers
- December 2017
- Materials: http://materials.dagstuhl.de/index.php?semnr=17502
- EMI-based Compiler Testing - http://web.cs.ucdavis.edu/~su/emi-project/
Articles
- A Systematic Impact Study for Fuzzer-Found Compiler Bugs
- 2019 arXiv
- Michaël Marcozzi, Qiyi Tang, Alastair Donaldson, Cristian Cadar
- An empirical comparison of compiler testing techniques
- International Conference on Software Engineering (ICSE 2016)
- Junjie Chen, Wenxiang Hu, Dan Hao, Yingfei Xiong, Hongyu Zhang, Lu Zhang, Bing Xie
- Automatic Test Case Reduction for OpenCL - https://dl.acm.org/citation.cfm?id=2909439
- paper: https://spiral.imperial.ac.uk/handle/10044/1/39576
- slides: http://www.iwocl.org/wp-content/uploads/iwocl-2016-automatic-test-case-reduction.pdf
- Automated Testing of Graphics Shader Compilers
- Overview of the GLFuzz transformations - https://medium.com/@afd_icl/overview-of-the-glfuzz-transformations-d530540a5a18
- Automatic Testing of Symbolic Execution Engines via Program Generation and Differential Testing - https://srg.doc.ic.ac.uk/files/papers/symex-engine-tester-ase-17.pdf
- Causal Distance-Metric-Based Assistance for Debugging After Compiler Fuzzing
- IEEE International Symposium on Software Reliability Engineering (ISSRE) 2018
- Josie Holmes and Alex Groce
- Checking Correctness of Code Generator Architecture Specifications
- Code Generation and Optimization (CGO) 2015
- N. Hasabnis, R. Qiao, R. Sekar
- Compiler fuzzing, part 1
- Compiler Fuzzing through Deep Learning
- Chris Cummins, Pavlos Petoumenos, Hugh Leather and Alastair Murray
- International Symposium on Software Testing and Analysis (ISSTA) 2018
- Compiler Testing via a Theory of Sound Optimisations in the C11/C++11 Memory Model
- Programming Language Design and Implementation (PLDI) 2013
- Robin Morisset, Pankaj Pawan, Francesco Zappa Nardelli
- Coverage Prediction for Accelerating Compiler Testing
- IEEE Transactions on Software Engineering (2019)
- Junjie Chen, Guancheng Wang, Dan Hao, Yingfei Xiong, Hongyu Zhang, Lu Zhang, Bing Xie
- DATm: Diderot's Automated Testing Model.
- 39th International Conference on Software Engineering ICSE (12th International Workshop on Automation of Software Test AST) 2017
- C. Chiw, G. Kindlmann, J. Reppy
- DeepFuzz: Automatic Generation of Syntax Valid C Programs for Fuzz Testing
- AAAI Conference on Artificial Intelligence (AAAI) 2019
- Xiao Liu, Xiaoting Li, Rupesh Prajapati, Dinghao Wu
- Detecting Arithmetic Optimization Opportunities for C Compilers by Randomly Generated Equivalent Programs
- IPSJ Transactions on System LSI Design Methodology, vol. 9, 2016; A. Hashimoto and N. Ishiura
- Detecting Missed Arithmetic Optimization in C Compilers by Differential Random Testing - http://ist.ksc.kwansei.ac.jp/~ishiura/publications/C2016-10a.pdf
- Differential Testing for Software - http://www.cs.dartmouth.edu/~mckeeman/references/DifferentialTestingForSoftware.pdf
- Effect-Driven QuickChecking of Compilers
- ICFP 2017
- Jan Midtgaard, Mathias Nygaard Justesen, Patrick Kasting, Flemming Nielson, Hanne Riis Nielson
- paper: http://janmidtgaard.dk/papers/Midtgaard-al%3AICFP17-full.pdf
- implementation: https://github.com/jmid/efftester
- talk
- Evaluating the Effects of Compiler Optimizations on Mutation Testing at the Compiler IR Level - ISSRE’16
- Finding and Analyzing Compiler Warning Defects - http://ieeexplore.ieee.org/document/7886904/
- Finding Missed Compiler Optimizations by Differential Testing
- Compiler Construction (CC) 2018
- Gergö Barany
- Missed optimizations in C compilers: https://github.com/gergo-/missed-optimizations/
- Finding and Understanding Bugs in C Compilers
- Fuzzing with Grammars - Generating Software Tests - https://www.fuzzingbook.org/html/Grammars.html
- Fuzzing the .NET JIT Compiler
- Fuzzlyn: Fuzzer for the .NET toolchains
- Improving the Utility of Compiler Fuzzers
- 2014 Ph.D. Dissertation; Yang Chen
- Learning to Accelerate Compiler Testing
- International Conference on Software Engineering (ICSE), Doctoral Symposium, 2018
- Slides (2017): http://materials.dagstuhl.de/files/17/17502/17502.JunjieChen.Slides.pdf
- Learning to Prioritize Test Programs for Compiler Testing
- International Conference on Software Engineering (ICSE 2017)
- Junjie Chen, Yanwei Bai, Dan Hao, Yingfei Xiong, Hongyu Zhang, Bing Xie
- Nautilus: Fishing for Deep Bugs with Grammars
- Network and Distributed System Security Symposium (NDSS) 2019
- Cornelius Aschermann, Tommaso Frassetto, Thorsten Holz, Patrick Jauernig, Ahmad-Reza Sadeghi, Daniel Teuchert
- testing applications: ChakraCore (the JavaScript engine of Microsoft Edge), PHP, mruby, and Lua
- RandIR: Differential Testing for Embedded Compilers - https://www.cs.purdue.edu/homes/rompf/papers/ofenbeck-scala16.pdf
- Reinforcing Random Testing of Arithmetic Optimization of C Compilers by Scaling up Size and Number of Expressions, IPSJ Transactions on System LSI Design Methodology, vol. 7, 2014. E. Nagai, A. Hashimoto, and N. Ishiura. https://www.jstage.jst.go.jp/article/ipsjtsldm/7/0/7_91/_article
- Scaling up Size and Number of Expressions in Random Testing of Arithmetic Optimization of C Compilers
- SASIMI 2013
- Some Goals for High-impact Verified Compiler Research - https://blog.regehr.org/archives/1565
- System Under Test: LLVM - https://systemundertest.org/llvm/
- Taming compiler fuzzers
- PLDI 2013
- Y. Chen, A. Groce, C. Zhang, W.-K. Wong, X. Fern, E. Eide, J. Regehr
- Fuzzers Need Taming - https://blog.regehr.org/archives/925
- Test-Case Reduction for C Compiler Bugs - https://www.cs.utah.edu/~regehr/papers/pldi12-preprint.pdf
- Testing LLVM - http://blog.regehr.org/archives/1450
- The Correctness-Security Gap in Compiler Optimization - LangSec 2015, IEEE SPW
- paper: https://research.google.com/pubs/pub43856.html
- slides: https://nebelwelt.net/publications/files/15LangSec-presentation.pdf
- talk: https://www.youtube.com/watch?v=g6LCtHz_MDc&list=PL0pRF4xvoD0kuECJuowraVIIHlT3pN1Cm&index=3
- The problem with differential testing is that at least one of the compilers must get it right - http://blog.frama-c.com/index.php?post/2013/09/25/The-problem-with-differential-testing-is-that-at-least-one-of-the-compilers-must-get-it-right
Software
- CF3: Test suite for arithmetic optimization of C compilers
- Csmith, a random generator of C programs
- Csmith testing - http://blog.frama-c.com/index.php?pages/Csmith-testing
- C-Reduce, a C program reducer
- Fuzzing LLVM libraries and tools - https://llvm.org/docs/FuzzingLLVM.html
- Adventures in Fuzzing Instruction Selection
- 2017 EuroLLVM Developers’ Meeting; Justin Bogner
- Structure-aware fuzzing for Clang and LLVM with libprotobuf-mutator
- 2017 LLVM Developers’ Meeting; Kostya Serebryany, Vitaly Buka, Matt Morehouse
- Adventures in Fuzzing Instruction Selection
- gcc-for-llvm-testing: A modified GCC test suite suitable for testing non-GCC compilers
- Using the GCC regression test suite for LLVM (and other compilers)
- GNU Tools Cauldron 2018; Simon Cook
- Repurposing GCC Regression for LLVM Based Tool Chains
- 2018 LLVM Developers’ Meeting; Jeremy Bennett
- Using the GCC regression test suite for LLVM (and other compilers)
- GraphicsFuzz: A testing framework for automatically finding and simplifying bugs in graphics shader compilers.
- kscope
- a library which recursively generates randomized code while keeping it 100% equivalent to the original one
- ldrgen: Liveness-driven random C code generator - https://github.com/gergo-/ldrgen
- llvm-mutate – mutate LLVM IR - http://eschulte.github.io/llvm-mutate/
- opt-fuzz: a simple implementation of bounded exhaustive testing for LLVM programs
- Orange3
- a tool to test C compilers with randomly generated programs; mainly targets arithmetic optimization such as constant folding.
- Orange4
- a tool to test C compilers by randomly generated programs; based on equivalent transformations on C programs and can generate wider class of C test programs than Orange3.
- OutputCheck: A tool for checking tool output inspired by LLVM's FileCheck
- prog-fuzz: Compiler/source code fuzzing tool using AFL instrumentation
- Quest: A tool for testing C compilers - https://github.com/lindig/quest
- shader-compiler-bugs: A collection of shader compiler bugs - https://github.com/mc-imperial/shader-compiler-bugs
- yarpgen: Yet Another Random Program Generator
- a random C/C++ program generator, which produces correct runnable C/C++ programs
- specifically designed to trigger compiler optimization bugs and is intended for compiler testing
Talks
- Adventures in Fuzzing Instruction Selection
- EuroLLVM 2017 - Justin Bogner
- Compiler testing: GCC Vs LLVM
- Linaro Connect Vancouver 2018 (YVR18) TCWG07; Thomas Preud’homme
- FileCheck numeric expressions: features and implementation - https://connect.linaro.org/resources/yvr18/yvr18-tcw07/
- Coverage-Directed Differential Testing of JVM Implementations - Yuting Chen, PLDI 2016
- Exposing Difficult Compiler Bugs With Random Testing
- Finding Missed Optimizations in LLVM (and other compilers)
- EuroLLVM 2018 - Gergö Barany
- Testing Language Implementations - Alastair Donaldson - Programming Language Implementation Summer School (PLISS) 2017
Validation: Including translation validation, equivalence checking.
- Black-box equivalence checking across compiler optimizations - APLAS ’17 (2017) - http://www.cse.iitd.ac.in/~sbansal/pubs/aplas17.pdf
- Modeling undefined behaviour semantics for checking equivalence across compiler optimizations - Manjeet Dahiya, Sorav Bansal. HVC 2017
- Evaluating value-graph translation validation for LLVM
- Programming and Language Design Implementation (PLDI) 2011
- Tristan, Jean-Baptiste, Paul Govereau, Greg Morrisett
- Formally Verified Compilation of Low-Level C code
- 2016 PhD Dissertation; Pierre Wilke
- Proving the correctness of heuristically optimized code
- Hanan Samet, CACM 1978
- Translation validation
- TACAS 1998
- Amir Pnueli, Michael Siegel, Eli Singerman
- 'We present the notion of translation validation as a new approach to the verification of translators (compilers, code generators). Rather than proving in advance that the compiler always produces a target code which correctly implements the source code (compiler verification), each individual translation (i.e. a run of the compiler) is followed by a validation phase which verifies that the target code produced on this run correctly implements the submitted source program.'
- Translation Validation: Automatically Proving the Correctness of Translations Involving Optimized Code
- translation validation - http://www.cs.umd.edu/~hjs/hjscat.html#sectiontranslationvalidation
- compiler testing - http://www.cs.umd.edu/~hjs/hjscat.html#sectioncompilertesting
- Translation Validation: From DC+ to C*
- FM-Trends 1998
- Amir Pnueli, Ofer Shtrichman, Michael Siegel
- 'Translation validation is an alternative to the verification of translators (compilers, code generators). Rather than proving in advance that the compiler always produces a target code which correctly implements the source code (compiler verification), each individual translation (i.e. a run of the compiler) is followed by a validation phase which verifies that the target code produced on this run correctly implements the submitted source program.'
- Translation validation for an optimizing compiler
- PLDI 2000
- George C. Necula
- Translation Validation for Verified, Efficient and Timely Operating Systems
- 2017 PhD Dissertation; Thomas Sewell
- Translation Validation of Bounded Exhaustive Test Cases - Nuno Lopes, John Regehr - https://blog.regehr.org/archives/1510
- Translation Validation with Alive - https://github.com/nunoplopes/alive/tree/newsema/tv
- Validating Optimizations of Concurrent C/C++ Programs
- CGO 2016
- Soham Chakraborty, Viktor Vafeiadis
- A Higher-Order Abstract Syntax Approach to the Verified Compilation of Functional Programs
- 2016 PhD thesis; Yuting Wang
- A Verified Compiler for a Linear Function/Imperative Intermediate Language
- 2018 PhD Thesis; Sigurd Schneider
- LVC - Linear Verified Compiler: https://www.ps.uni-saarland.de/~sdschn/LVC.html
- ALIVe: Automatic LLVM InstCombine Verifier
- online: http://rise4fun.com/Alive
- blog post: http://blog.regehr.org/archives/1170
- slides: http://llvm.org/devmtg/2014-10/Slides/Menendez-Alive.pdf
- Alive-FP: Automated Verification of Floating Point Based Peephole Optimizations in LLVM - https://www.cs.rutgers.edu/research/technical_reports/report.php?series_id=1&report_id=723
- Alive-Loops: https://github.com/rutgers-apl/alive-loops
- 'Termination checking for LLVM peephole optimizations' (ICSE 2016); David Menendez, Santosh Nagarakatte
- Alive-NJ - https://github.com/rutgers-apl/alive-nj
- LifeJacket: Verifying precise floating-point optimizations in LLVM - http://export.arxiv.org/abs/1603.09290 - https://github.com/4tXJ7f/alive
- Practical Formal Techniques and Tools for Developing LLVM's Peephole Optimizations
- 2018 PhD Thesis; David Menendez
- Precondition Inference for Peephole Optimizations in LLVM
- PLDI 2017 talk, David Menendez - https://pldi17.sigplan.org/event/pldi-2017-papers-precondition-inference-for-peephole-optimizations-in-llvm
- Provably Correct Peephole Optimizations with Alive - https://www.cs.utah.edu/~regehr/papers/pldi15.pdf
- An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code
- POPL 2019
- Yuting Wang, Pierre Wilke, Zhong Shao
- CakeML: A Verified Implementation of ML
- Verified Compilation of CakeML to Multiple Machine-Code Targets
- Certified Programs and Proofs (CPP) 2017
- Anthony Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar.
- The Verified CakeML Compiler Backend
- JFP 2019
- Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony Fox, Scott Owens, Michael Norrish
- Verified Compilation of CakeML to Multiple Machine-Code Targets
- CompCert: formally-verified C compiler
- The formal verification of compilers - Xavier Leroy - DeepSpec Summer School 2017
- An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code
- POPL 2019
- Yuting Wang, Pierre Wilke, Zhong Shao
- Stack-Aware CompCert and CompCert MC - https://certikos.github.io/compcertmc/
- Closing the Gap – The Formally Verified Optimizing Compiler CompCert
- SSS'17: Safety-critical Systems Symposium 2017
- Compositional CompCert
- POPL 2015
- Stewart, G., Beringer, L., Cuellar, S., Appel, A.W.
- Lightweight Verification of Separate Compilation
- POPL 2016
- Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis
- Verified Peephole Optimizations for CompCert
- PLDI 2016
- Eric Mullen, Daryl Zuniga, Zachary Tatlock, Dan Grossman
- Peek: a verified peephole optimizer for CompCert - https://github.com/uwplse/peek
- Compilation Using Correct-by-Construction Program Synthesis
- Clément Pit-Claudel; 2016 Master's Thesis at MIT; William A. Martin Memorial Thesis Award for Outstanding Thesis in CS
- Compositional Verification of Compiler Optimisations on Relaxed Memory
- ESOP 2018
- Mike Dodds, Mark Batty, Alexey Gotsman
- Crellvm: Verified Credible Compilation for LLVM
- Programming Languages Design and Implementation (PLDI) 2018
- Jeehoon Kang, Yoonseung Kim, Youngju Song, Juneyoung Lee, Sanghoon Park, Mark Dongyeon Shin, Yonghyun Kim, Sungkeun Cho, Joonwon Choi,Chung-Kil Hur, Kwangkeun Yi
- a verified credible compilation (or equivalently, verified translation validation) framework for LLVM
- Pilsner: A Compositionally Verified Compiler for a Higher-Order Imperative Language
- International Conference on Functional Programming (ICFP) 2015
- Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, Viktor Vafeiadis
- Pushing the Limits of Compiler Verification
- 2018 PhD Thesis; Eric Mullen
- Œuf: Verified Coq Extraction in Coq - https://github.com/uwplse/oeuf
- Peek: Verified Peephole Optimizations for CompCert - https://github.com/uwplse/peek
- Self-compilation and self-verification - Ramana Kumar
- Vale (Verified Assembly Language for Everest)
- Vellvm: Verifying the LLVM
- DeepSpec Summer School 2017; Steve Zdancewic - https://deepspec.org/event/dsss17/lecture_zdancewic.html
- Galois, Inc. Tech Talk 2018; Steve Zdancewic
- Strange Loop 2018; Steve Zdancewic
- Verified Compilers for a Multi-Language World
- Summit on Advances in Programming Languages (SNAPL) 2015
- Amal Ahmed