Signedness-Agnostic Program Analysis: Precise Integer Bounds for Low-Level Code
Signedness-Agnostic Program Analysis: Precise Integer Bounds for Low-Level Code
复制标题
与符号无关的程序分析：低级代码的精确整数界限
DOI：
10.1007/978-3-642-35182-2_9
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Peter James Stuckey
中科院分区：
文献类型：
--
作者：
J. Navas;P. Schachte;H. Søndergaard;Peter James Stuckey
许多编译器以公共后端为目标，因此无需为许多不同的源语言实现相同的分析。这导致了对LLVM代码的静态分析的兴趣。在LLVM(和类似的语言)中，大多数与变量相关的符号信息都被编译掉了。当前对LLVM代码的分析倾向于假设所有值要么都是有符号的，要么都是无符号的(除非代码指定了符号)。我们展示了程序分析如何同时考虑每个比特串是有符号的和无符号的，从而提高了精度，并针对整数界限分析的具体情况实现了这一思想。实验结果表明，该方法在不增加额外代价的情况下，具有较高的精度。事实证明，我们的方法即使在所有签名信息都可用时也是有益的，例如在分析C或Java代码时。
Many compilers target common back-ends, thereby avoiding the need to implement the same analyses for many different source languages. This has led to interest in static analysis of LLVM code. In LLVM (and similar languages) most signedness information associated with variables has been compiled away. Current analyses of LLVM code tend to assume that either all values are signed or all are unsigned (except where the code specifies the signedness). We show how program analysis can simultaneously consider each bit-string to be both signed and unsigned, thus improving precision, and we implement the idea for the specific case of integer bounds analysis. Experimental evaluation shows that this provides higher precision at little extra cost. Our approach turns out to be beneficial even when all signedness information is available, such as when analysing C or Java code.