针对OCaml C Stubs的定向静态分析：清除代码中的灵魂角色
摘要：迁移到OCaml 5需要更新许多C绑定，因为不再支持裸指针。在C中编写OCaml用户自定义原语是必要的，但是不安全且容易出错。它既不能受益于OCaml的类型检查，也不能受益于C的类型检查，现有的C静态分析器也不知道OCaml的GC安全规则，并且仅根据现有的宏无法推断它们。另一种选择是自动生成C存根，这需要正确地管理值的生命周期。拥有一个针对OCaml到C接口的静态分析器在OCaml 5移植工作之外也是有用的。 通过一些实际的C绑定中存在的错误示例，介绍了一种静态分析器来查找这些已知的错误类别。该工具使用OCaml的抽象解析和类型化树，并生成一个头文件和一个调用者模型。与OCaml运行时的简化模型一起，这些模型被用作静态分析框架Goblint的输入。开发了一种分析方法来跟踪OCaml值的解引用，结合现有的框架报告不正确的解引用。还展示了如何扩展分析来覆盖更多的安全属性。 这些工具和运行时模型是通用的，并可以与其他静态分析工具一起重复使用。
作者：Edwin T"or"ok
论文ID：2307.14909
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-07-31