一句话:将 SSA 翻译重新表述为抽象解释式静态分析,使其可与其它分析单遍组合并用于 C/机器码分析器。
SSA 形式是广泛使用的中间表示,支撑全局值编号、稀疏数据流分析以及基于 SMT 的抽象解释或模型检测。但 SSA 翻译本身的精度依赖于静态分析,对机器码等底层语言甚至需要预先分析,形成先有鸡还是先有蛋的问题。本文把 SSA 翻译转化为基于抽象解释的标准静态分析,从而能与其它分析在单遍中组合;组合分析通常比顺序执行各遍更精确。作者实现了一个小型数据流分析,在单遍内完成 SSA 翻译、乐观全局值编号、稀疏条件常量传播和循环不变量代码外提,并给出以 SSA 抽象域为主中间表示的、同时处理 C 与机器码的多语言静态分析器。
Static single assignment (SSA) form is a popular intermediate representation that helps implement useful static analyses, including global value numbering (GVN), sparse dataflow analyses, or SMT-based abstract interpretation or model checking. However, the precision of the SSA translation itself depends on static analyses, and a priori static analysis is even indispensable in the case of low-level input languages like machine code. To solve this chicken-and-egg problem, we propose to turn the SSA translation into a standard static analysis based on abstract interpretation. This allows the SSA translation to be combined with other static analyses in a single pass, taking advantage of the fact that it is more precise to combine analyses than applying passes in sequence. We illustrate the practicality of these results by writing a simple dataflow analysis that performs SSA translation, optimistic global value numbering, sparse conditional constant propagation, and loop-invariant code motion in a single small pass; and by presenting a multi-language static analyzer for both C and machine code that uses the SSA abstract domain as its main intermediate representation.