Verifying Fortran Programs with CIVL
Verifying Fortran Programs with CIVL
复制标题
使用 CIVL 验证 Fortran 程序
DOI：
10.1007/978-3-030-99524-9_6
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Siegel, Stephen F.
中科院分区：
文献类型：
--
作者：
Wu, Wenhao;Hückelheim, Jan;Hovland, Paul D.;Siegel, Stephen F.
Fortran广泛应用于计算科学、工程和高性能计算领域。本文提出了对CIVL验证框架的扩展，用于检查Fortran程序的正确性。与之前的工作不同，在验证之前将Fortran转换为C， LLVM IR或其他中间格式，我们的工作允许CIVL直接使用Fortran源文件。我们扩展了解析、翻译和分析阶段，以支持Fortran特有的功能，如数组切片和重塑，并查找Fortran特有的程序违规，如参数混叠规则违规、变量和函数属性的无效使用，或由于Fortran未指定表达式求值顺序而导致的缺陷。我们在验证基准套件和从实际应用程序中提取的内核上演示了我们的工具的有用性。
Fortran is widely used in computational science, engineering, and high performance computing. This paper presents an extension to the CIVL verification framework to check correctness properties of Fortran programs. Unlike previous work that translates Fortran to C, LLVM IR, or other intermediate formats before verification, our work allows CIVL to directly consume Fortran source files. We extended the parsing, translation, and analysis phases to support Fortran-specific features such as array slicing and reshaping, and to find program violations that are specific to Fortran, such as argument aliasing rule violations, invalid use of variable and function attributes, or defects due to Fortran’s unspecified expression evaluation order. We demonstrate the usefulness of our tool on a verification benchmark suite and kernels extracted from a real world application.