What is a secure programming language?
Debugging
See also: Section 6.3 (Compiler Bug Debugging) in "A Survey of Compiler Testing"
- Automatic Isolation of Compiler Errors
- Bugfind: A Tool for Debugging Optimizing Compilers
- Compiler Bug Isolation via Effective Witness Test Program Generation
- Debugging compilers with optimization fuel
- GCC Wiki: Finding miscompilations on large testcases
- LLVM bugpoint
- LLVM bugpoint tool: design and usage
- Reduce Your Testcases with Bugpoint and Custom Scripts
- Locating a compiler bug with git bisection
- Replay Compilation: Improving Debuggability of a Just-in-Time Compiler
- Toward Automatic Debugging of Compilers
- Type-Based Verification of Assembly Language for Compiler Debugging
- Using Mutants to Help Developers Distinguish and Debug (Compiler) Faults
History
- Advice on Structuring Compilers and Proving Them Correct
- Compiler Verification: A Bibliography
- Correctness of a Compiler for Algol-like Programs
- Correctness of a Compiler for Arithmetic Expressions
- Formalising Meaning: a History of Programming Language Semantics
Lectures
- Compiler Verification: The Next Generation
- OPLSS (Oregon Programming Languages Summer School)
Testing
See also: Testing
Readings
- An empirical comparison of compiler testing techniques
- Automatic Test Case Reduction for OpenCL
- Automated Testing of Graphics Shader Compilers
- Automatic Testing of Symbolic Execution Engines via Program Generation and Differential Testing
- Causal Distance-Metric-Based Assistance for Debugging After Compiler Fuzzing
- Checking Correctness of Code Generator Architecture Specifications
- Compiler fuzzing, part 1
- Compiler Fuzzing through Deep Learning
- Compiler Fuzzing: How Much Does It Matter?
- Coverage Prediction for Accelerating Compiler Testing
- CUDAsmith: A Fuzzer for CUDA Compilers
- DATm: Diderot's Automated Testing Model.
- Deep Differential Testing of JVM Implementations
- DeepFuzz: Automatic Generation of Syntax Valid C Programs for Fuzz Testing
- Differential Testing for Software
- Effect-Driven QuickChecking of Compilers
- Extending Equivalence Transformation Based Program Generator for Random Testing of C Compilers
- Finding and Analyzing Compiler Warning Defects
- Finding and Understanding Bugs in C Compilers
- Fuzzing with Grammars
- Fuzzing the .NET JIT Compiler
- History-Guided Configuration Diversification for Compiler Test-Program Generation
- Improving the Utility of Compiler Fuzzers
- K-CONFIG: Using Failing Test Cases to Generate Test Cases in GCC Compilers
- Learning to Accelerate Compiler Testing
- Learning to Prioritize Test Programs for Compiler Testing
- Nautilus: Fishing for Deep Bugs with Grammars
- RandIR: Differential Testing for Embedded Compilers
- ReduKtor: How We Stopped Worrying About Bugs in Kotlin Compiler
- System Under Test: LLVM - https://systemundertest.org/llvm/
- Taming compiler fuzzers
- Test-Case Reduction for C Compiler Bugs
- Testing LLVM - http://blog.regehr.org/archives/1450
- Testing Static Analyses for Precision and Soundness
- The problem with differential testing is that at least one of the compilers must get it right
Performance Optimization
- Compiler Testing via a Theory of Sound Optimisations in the C11/C++11 Memory Model
- Detecting Arithmetic Optimization Opportunities for C Compilers by Randomly Generated Equivalent Programs
- Detecting Missed Arithmetic Optimization in C Compilers by Differential Random Testing
- Evaluating the Effects of Compiler Optimizations on Mutation Testing at the Compiler IR Level
- Finding Missed Compiler Optimizations by Differential Testing
- Lost in translation: Exposing hidden compiler optimization opportunities
- Random Testing of Compilers’ Performance Based on Mixed Static and Dynamic Code Comparison
- Reinforcing Random Testing of Arithmetic Optimization of C Compilers by Scaling up Size and Number of Expressions
- Scaling up Size and Number of Expressions in Random Testing of Arithmetic Optimization of C Compilers
- The Correctness-Security Gap in Compiler Optimization
Software
- CF3: Test suite for arithmetic optimization of C compilers
- Csmith, a random generator of C programs
- C-Reduce, a C program reducer
- Fuzzing LLVM libraries and tools - https://llvm.org/docs/FuzzingLLVM.html
- Adventures in Fuzzing Instruction Selection
- Structure-aware fuzzing for Clang and LLVM with libprotobuf-mutator
- gcc-for-llvm-testing: A modified GCC test suite suitable for testing non-GCC compilers
- GraphicsFuzz: A testing framework for automatically finding and simplifying bugs in graphics shader compilers.
- kscope
- lang_tester: Rust testing framework for compilers and VMs
- 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
- Orange4
- 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
- https://github.com/intel/yarpgen
Talks
- A Year of Experience with Broad Based Continuous Testing with GCC
- Adventures in Fuzzing Instruction Selection
- Coverage-Directed Differential Testing of JVM Implementations
- Exposing Difficult Compiler Bugs With Random Testing
- FileCheck
- FileCheck Follies
- FileCheck: learning arithmetic
- Finding Missed Optimizations in LLVM (and other compilers)
- Getting Started with the LLVM Testing Infrastructure
- Testing and Qualification of Optimizing Compilers for Functional Safety
- Testing Language Implementations
Validation
Validation: Including translation validation, equivalence checking.
- Black-Box Equivalence Checking Across Compiler Optimizations
- Modeling undefined behaviour semantics for checking equivalence across compiler optimizations
- Evaluating value-graph translation validation for LLVM
- Formally Verified Compilation of Low-Level C code
- Proving the correctness of heuristically optimized code
- Semantic Program Alignment for Equivalence Checking
- Translation validation
- TACAS 1998
- Amir Pnueli, Michael Siegel, Eli Singerman
- https://dl.acm.org/citation.cfm?id=349314
- "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: From DC+ to C*
- FM-Trends 1998
- Amir Pnueli, Ofer Shtrichman, Michael Siegel
- https://dl.acm.org/citation.cfm?id=729871
- "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
- Translation Validation for Verified, Efficient and Timely Operating Systems
- Translation Validation of Bounded Exhaustive Test Cases
- Validating Optimizations of Concurrent C/C++ Programs
Verification
- A Higher-Order Abstract Syntax Approach to the Verified Compilation of Functional Programs
- A Verified Compiler for a Linear Function/Imperative Intermediate Language
- A Verified Packrat Parser Interpreter for Parsing Expression Grammars
- ALIVe: Automatic LLVM InstCombine Verifier
- Alive2: Automatic verification of LLVM optimizations
- An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code
- Blackbox Equivalence Checking of Program Optimizations
- CakeML: A Verified Implementation of ML
- https://cakeml.org/
- https://github.com/CakeML/cakeml
- Verified Compilation of CakeML to Multiple Machine-Code Targets
- Verified Compilation on a Verified Processor
- PLDI 2019
- Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, Anthony Fox
- https://cakeml.org/pldi19.pdf
- The Verified CakeML Compiler Backend
- Icing: Supporting Fast-math Style Optimizations in a Verified Compiler
- CompCert: formally-verified C compiler
- http://compcert.inria.fr/
- https://github.com/AbsInt/CompCert
- The formal verification of compilers - Xavier Leroy - DeepSpec Summer School 2017
- A Verified CompCert Front-End for a Memory Model Supporting Pointer Arithmetic and Uninitialised Data
- An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code
- Closing the Gap – The Formally Verified Optimizing Compiler CompCert
- CompCertM: CompCert with Lightweight Modular Verification and Multi-Language Linking
- CompCertS: A Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics
- Compositional CompCert
- Formal Verification of a Constant-Time Preserving C Compiler
- Lightweight Verification of Separate Compilation
- Reconciling Low-Level Features of C with Compiler Optimizations
- 2019 Ph.D. Dissertation; Jeehoon Kang
- https://sf.snu.ac.kr/jeehoon.kang/thesis/
- Chapter I, Section 2, Background: A Brief Tour of CompCert
- Chapter III, Separate Compilation and Linking
- Chapter IV, Cast between Integers and Pointers
- Verified Peephole Optimizations for CompCert
- Compilation Using Correct-by-Construction Program Synthesis
- Compositional Verification of Compiler Optimisations on Relaxed Memory
- 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
- http://sf.snu.ac.kr/crellvm/
- http://sf.snu.ac.kr/gil.hur/publications/crellvm.pdf
- http://sf.snu.ac.kr/gil.hur/publications/crellvm.zip
- https://github.com/snu-sf/crellvm-tests-parallel
- Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset
- Pilsner: A Compositionally Verified Compiler for a Higher-Order Imperative Language
- Pushing the Limits of Compiler Verification
- Self-compilation and self-verification
- The Correctness of a Code Generator for a Functional Language
- Towards Formally Verified Just-In-Time Compilation
- Vale (Verified Assembly Language for Everest)
- Vellvm: Verifying the LLVM
- Verified Compilers for a Multi-Language World
Tags:
language
reading
native
clr
llvm
language development
Last modified 03 November 2024