利用抽象解释自动修复溢出表达式
编程语言
2013-09-23 v1 软件工程
摘要
我们研究合成可证明不溢出的整数算术表达式或整数算术表达式间的布尔关系的问题。首先，我们使用数值抽象域推断程序变量间的数值属性。然后，我们检查这些属性是否能保证给定表达式不溢出。若不能，我们合成一个等价但不溢出的表达式，或者报告此类表达式不存在。非溢出表达式的合成取决于三个正交因素：输入表达式（例如，它是线性的、多项式的还是其他形式？）、输出表达式（例如，是否允许情况分支？）以及底层的数值抽象域——抽象域越精确，能合成的正确表达式就越多。我们考虑三种常见情况：(i) 具有整数系数和区间的线性表达式；(ii) 线性表达式的布尔表达式；以及 (iii) 带有模板的线性表达式。在第一种情况下，我们证明存在一种完整且多项式时间的算法来解决该问题。在第二种情况下，我们拥有一种不完整但多项式时间的算法，而在第三种情况下，我们拥有一种完整但在最坏情况下指数时间的算法。
引用
@article{arxiv.1309.5148,
title = {Automatic Repair of Overflowing Expressions with Abstract Interpretation},
author = {Francesco Logozzo and Matthieu Martel},
journal= {arXiv preprint arXiv:1309.5148},
year = {2013}
}
备注
In Proceedings Festschrift for Dave Schmidt, arXiv:1309.4557