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

【Abstract】 Type analysis plays an important role in object-oriented program analysis.Accurate type analysis will improve the precision of other program analyses.However,due to the inherent high complexity of traditional type analysis,people generally make rapid but coarse analyses.This paper presented a new type analysis method of object-oriented program based on SAT solver,in which we show transfer relationship among variables by the proposition logic method,abstract programs into proposition formulas and adopt highly effective SAT solver so that we can obtain variable run-time types through decoding the results.This method is flow-sensitive with good flexibility,that is to say,it can not only make rapid but rough context-insensitive analysis,but also comparatively slow but highly accurate context-sensitive one.更多还原