Targeted Static Analysis for OCaml C Stubs: Eliminating gremlins from the code
summary
Migrates OCaml C bindings by parsing OCaml parsetrees and typed trees to auto-generate a C header generator and a caller model, then feeds a simplified runtime-lock model and wrappers into the Goblint static analysis framework to detect GC-safety bugs like invalid dereferences and data races introduced when the runtime lock is released. The prototype runs on real codebases, integrates with Dune and CI, and finishes analysis jobs in about ten minutes per repository file set.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:03OCaml C bindings risks
- 3:11Bugs in OCaml C bindings
- 5:20Header files for type safety
- 6:45Data races detection
- 9:54OCaml types limitations
- 11:48Assertions for C stubs
- 13:53OCaml runtime modeling
- 15:19Results and integration
- 17:08Analyzer implementation
- 18:55GitHub Actions SARIF
- 19:17Q&A
related talks
43mEverything I learned about static analysis and program safety in C++
01h 01m“Static Analysis and C++: More Than Lint"
21mTowards Compiler-Guided Static Analysis
15mDuplo: A Framework for OCaml Post-Link Optimisation
19mA Library Modeling Language for the Static Analysis of C Programs
28mA Mechanically Verified Garbage Collector for OCaml
51mCompile-time tools supporting generic programming in C++
14mCoSSJIT: Combining Static Analysis and Speculation in JIT Compilers