Targeted Static Analysis for OCaml C Stubs: Eliminating gremlins from the code
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.
Sat 9 SepDisplayed time zone: Pacific Time (US & Canada) change
09:00 - 10:30
|Eio 1.0 – Effects-based IO for OCaml 5|
Thomas Leonard Tarides, Patrick Ferris University of Cambridge, UK, Christiano Haesbaert Tarides, Lucas Pluvinage Tarides, Vesa Karvonen Tarides, Sudha Parimala Tarides, KC Sivaramakrishnan IIT Madras and Tarides, Vincent Balat Tarides, Anil Madhavapeddy University of Cambridge, UKFile Attached
|Modern DSL compiler architecture in OCaml our experience with CatalaRemote|
|Runtime Detection of Data Races in OCaml with ThreadSanitizerRemote|
|Targeted Static Analysis for OCaml C Stubs: Eliminating gremlins from the codeRemote|
Edwin Török XenServer, Cloud Software GroupFile Attached