一句话:提出统一术语的类与字段不可变性模型,并在 OPAL 上实现模块化协作分析 CiFi,支持惰性初始化与泛型依赖。
不可变性推理对多线程软件等场景的缺陷预防很重要,但已有静态分析多关注单个对象与引用,类与字段层面的不可变性研究较少,术语也不统一。本文提出类与字段不可变性模型,统一既有不可变性分类的术语,并扩展到惰性初始化和依赖泛型类型参数的不可变性。基于 OPAL 静态分析框架,作者实现 CiFi——一组模块化、相互协作的分析,用于推断模型定义的多种不可变性属性。作者还构建代表性测试基准,比较 CiFi 与现有技术的精确率和召回率,并研究真实库中不可变性的普遍性,表明模型具有实用质量与相关性。
Reasoning about immutability is important for pre-venting bugs, e.g., in multi-threaded software. So far, static analysis to infer immutability properties has mostly focused on individual objects and references. Reasoning about fields and entire classes, while significantly simpler, has gained less attention. Even a consistently used terminology is missing, which makes it difficult to implement analyses that rely on immutability information. We propose a model for class and field immutability that unifies terminology for immutability flavors considered by previous work and covers new levels of immutability to handle lazy initialization and immutability dependent on generic type parameters. Using the OPAL static analysis framework, we implement CiFi, a set of modular, collaborating analyses for different flavors of immutability, inferring the properties defined in our model. Additionally, we propose a benchmark of representative test cases for class and field immutability. We use the benchmark to showcase CiFi’s precision and recall in comparison to state of the art and use CiFi to study the prevalence of immutability in real-world libraries, showcasing the practical quality and relevance of our model.