Reasoning about floating-point arithmetic is notoriously hard. While static and dynamic analysis techniques or program repair have made significant progress, more work is still needed to make them relevant to real-world code. On the critical path to that goal is understanding what real-world floating-point code looks like. To close that knowledge gap, this paper presents the first large-scale empirical study of floating-point arithmetic usage across public GitHub repositories. We focus on statically typed languages to allow our study to scale to millions of repositories. We follow state-of the art mining practices including random sampling and filtering based on only intrinsic properties to avoid bias, and identify floating-point usage by searching for keywords in the source code, and programming language constructs (e.g., loops) by parsing the code. Our evaluation supports the claim often made in papers that floating-point arithmetic is widely used. Comparing statistics such as size and usage of certain constructs and functions, we find that benchmarks used in literature to evaluate automated reasoning techniques for floating-point arithmetic are in certain aspects representative of 'real-world' code, but not in all. We publish a dataset of 10 million real-world floating-point functions extracted from our study. We demonstrate in a case study how it may be used to identify new floating-point benchmarks and help future techniques for floating-point arithmetic to be designed and evaluated to match actual users' expectations.

翻译：浮点运算的推理众所周知是困难的。尽管静态与动态分析技术或程序修复已取得显著进展，但要使这些技术适用于实际代码仍需要更多工作。实现该目标的关键路径在于理解真实世界中的浮点代码究竟是什么样的。为填补这一知识空白，本文首次对公开 GitHub 仓库中的浮点运算使用情况进行了大规模实证研究。我们聚焦于静态类型语言，以使研究能够扩展到数百万个仓库。我们遵循最先进的挖掘实践，包括随机抽样和仅基于内在属性的过滤以避免偏差，并通过在源代码中搜索关键词来识别浮点数的使用，同时通过解析代码来识别编程语言结构（例如循环）。我们的评估支持了论文中经常提出的主张，即浮点运算被广泛使用。通过比较代码规模、特定结构和函数的使用情况等统计数据，我们发现文献中用于评估浮点运算自动推理技术的基准测试在某些方面能代表“真实世界”代码，但并非在所有方面都能代表。我们发布了从研究中提取的 1000 万个真实世界浮点函数的数据集。我们通过一个案例研究展示了如何利用该数据集识别新的浮点基准测试，并帮助未来的浮点运算技术得以设计和评估，以符合实际用户的期望。