Targeted Static Analysis for OCaml C Stubs: eliminating gremlins from the code

TL;DR

This paper presents a static analysis tool for OCaml C stubs that detects safety bugs related to OCaml's garbage collector and value lifetimes, aiding in safer code migration and development.

Contribution

It introduces a static analyser that works on OCaml's internal representations to automatically identify common C binding bugs, enhancing safety and correctness.

Findings

Detects known classes of bugs in OCaml C bindings

Integrates with Goblint static analysis framework

Reusable tools and models for broader static analysis applications

Abstract

Migration to OCaml 5 requires updating a lot of C bindings due to the removal of naked pointer support. Writing OCaml user-defined primitives in C is a necessity, but is unsafe and error-prone. It does not benefit from either OCaml's or C's type checking, and existing C static analysers are not aware of the OCaml GC safety rules, and cannot infer them from existing macros alone.The alternative is automatically generating C stubs, which requires correctly managing value lifetimes. Having a static analyser for OCaml to C interfaces is useful outside the OCaml 5 porting effort too. After some motivating examples of real bugs in C bindings a static analyser is presented that finds these known classes of bugs. The tool works on the OCaml abstract parse and typed trees, and generates a header file and a caller model. Together with a simplified model of the OCaml runtime this is used as input to a static analysis framework, Goblint. An analysis is developed that tracks dereferences of OCaml values, and together with the existing framework reports incorrect dereferences. An example is shown how to extend the analysis to cover more safety properties. The tools and runtime models are generic and could be reused with other static analysis tools.