Efficient Generation of Error-Inducing Floating-Point Inputs via Symbolic Execution
Efficient Generation of Error-Inducing Floating-Point Inputs via Symbolic Execution
复制标题
DOI：
10.1145/3377811.3380359
复制
发表时间：
2020-06
期刊：
影响因子：
--
通讯作者：
Hui Guo;Cindy Rubio-González
中科院分区：
文献类型：
--
作者：
Hui Guo;Cindy Rubio-González
浮点数被广泛用于软件中，以模拟实数运算。不幸的是，浮点会导致舍入错误，这些错误会在执行过程中传播和积累。在评估浮点代码的精度时，生成输入以最大化数值误差是至关重要的。在本文中，我们制定的问题，产生高错误诱导浮点输入作为一个代码覆盖率最大化的问题，使用符号执行解决。具体来说，我们定义了不准确检查来检测大的精度损失和取消。我们在战略程序位置注入这些检查，以构建专门的分支，当被给定的输入覆盖时，可能会导致结果中的大错误。我们应用符号执行来生成执行这些专门分支的输入，并描述使我们的方法实用的优化。我们实现了一个名为FPGen的工具，并提出了一个评价21数值程序，包括矩阵计算和统计库。我们发现，FPGen暴露了这些程序中的20个错误，并触发了平均超过2个数量级的错误。
Floating point is widely used in software to emulate arithmetic over reals. Unfortunately, floating point leads to rounding errors that propagate and accumulate during execution. Generating inputs to maximize the numerical error is critical when evaluating the accuracy of floating-point code. In this paper, we formulate the problem of generating high error-inducing floating-point inputs as a code coverage maximization problem solved using symbolic execution. Specifically, we define inaccuracy checks to detect large precision loss and cancellation. We inject these checks at strategic program locations to construct specialized branches that, when covered by a given input, are likely to lead to large errors in the result. We apply symbolic execution to generate inputs that exercise these specialized branches, and describe optimizations that make our approach practical. We implement a tool named FPGen and present an evaluation on 21 numerical programs including matrix computation and statistics libraries. We show that FPGen exposes errors for 20 of these programs and triggers errors that are, on average, over 2 orders of magnitude larger than the state of the art.