基于sat求解的面向对象程序类型分析

类型分析是面向对象程序分析中的重要环节，精确的类型分析能够提高其它程序分析的精度。由于传统精确分析方法固有的高复杂性，现有的类型分析大都使用粗糙的分析方法。提出了一种基于sat求解的面向对象程序类型分析方法。该方法用命题逻辑表示类型在变量间的传递关系，将程序抽象成命题公式，并使用高效的sat求解器求解，从而获得变量运行时的类型集合。该方法是流敏感的，并且具有良好的伸缩性，既可以进行快速但精度低的上下文不敏感分析，也可以进行较慢但精度高的上下文敏感分析。