F-IKOS: An Abstract Interpretation-based Static Analyzer for Fortran Programs Sheng Zou1,2 , Liqian Chen1,2,∗ , Guangsheng Fan1,2 , Renjie Huang1,2 and Banghu Yin3 1 College of Computer Science and Technology, National University of Defense Technology, Changsha 410073, China 2 State Key Laboratory of Complex & Critical Software Environment, Changsha 410073, China 3 College of Systems Engineering, National University of Defense Technology, Changsha 410073, China Abstract The Fortran programming language is widely utilized in numerical computation and scientific computing. Fortran programs are prone to potential runtime errors related to numerical properties due to the large number of numerical operations. In this paper, we present F-IKOS , an abstract interpretation-based static analyzer for Fortran programs on top of IKOS , which soundly handles floating-point types in Fortran programs. Firstly, we translate Fortran programs to LLVM IR using compiler front-end Flang . After that, we extend IKOS to support sound floating-point analysis and then employ it to analyze the translated LLVM IR. Particularly, when analyzing floating-point types in programs, we first abstract floating-point expressions into real-number expressions with interval coefficients, and then linearize these expressions into real-number expressions with scalar coefficients. These linear expressions are subsequently handled by abstract domains originally designed for real-number types to produce sound analysis results. We have conducted experiments on representative Fortran programs to show the efficiency and effectiveness of F-IKOS . The experimental results are encouraging: F-IKOS soundly analyzes runtime errors in complex programs, outperforming other analyzers. Keywords Fortran, Static Analysis, Abstract Interpretation, Floating-point Program Analysis 1. Introduction has a specific finite precision and cannot represent all real numbers exactly, leading to inherent and pervasive round- The Fortran programming language is one of the oldest ing errors in Fortran programs. If rounding errors are not high-level programming languages and one of the first to be accounted for during the analysis of Fortran programs, the widely adopted for scientific computing. Additionally, sev- analysis results may be unsound. However, the aforemen- eral numerical computation libraries, including BLAS[17], tioned approaches neglect to account for rounding errors which are developed in Fortran, have significantly con- during the analysis of Fortran programs. tributed to the widespread use of Fortran in domains such In this paper, we propose an approach to abstract floating- as numerical computing and high-performance computing. point operations soundly in Fortran programs, which con- Compared with mainstream high-level programming lan- siders rounding errors when analyzing programs. Our ap- guages such as C++ and Java, Fortran possesses a distinctive proach abstracts floating-point expressions in programs into set of features, such as powerful array manipulation and expressions with interval coefficients under real-number abundant intrinsic functions for numerical computation. semantics and then linearizes them into expressions with However, Fortran programs are prone to potential run- scalar coefficients. This abstraction aims to eliminate round- time errors related to numerical aspects such as division- ing errors by floating-point operations during program anal- by-zero and arithmetic overflow due to the large number of ysis, which enables analyzers to perform sound analysis numerical operations. Researchers have dedicated efforts under the abstract interpretation framework. We develop to the analysis and verification of Fortran programs. Pre- a Fortran program analyzer on top of the Inference Kernel vious research on the analysis of Fortran programs can be for Open Static Analyzers (IKOS [10]) to implement the pro- mainly classified into three categories: Firstly, approaches posed approach, named F-IKOS . F-IKOS utilizes Flang [5] such as f2c [3] and FABLE [11] convert Fortran programs to to translate Fortran programs into LLVM Intermediate Rep- other high-level language programs and verify them using resentation (LLVM IR) and then leverages IKOS to analyze verifiers over the converted high-level language programs. the LLVM IR. The core of F-IKOS is IKOS , which is a static Secondly, approaches such as SMACK [7] and CIVL [8] trans- analyzer based on abstract interpretation. IKOS can use late Fortran programs to Intermediate Representation (IR), abstract domains from the Apron [6] numerical abstract which is then verified using verifiers for IR, mainly based on domain library to analyze programs. However, it mainly model checking. Additionally, some static analyzers such detects runtime errors in machine integer types and cannot as FORTRAN-lint [13], ftnchek [12] and Coverity [14] de- infer invariants on floating-point types [1]. In our imple- tect certain generic defects, such as dead code and variable mentation, we first extended IKOS to support floating-point usage problems, using pre-defined patterns. types, and then applied the proposed approach to handle Fortran programs are characterized by the extensive use floating-point operations soundly. With these extensions, F- of floating-point operations, which are crucial for achieving IKOS can analyze floating-point types in Fortran programs high precision and scale in numerical computing tasks, such and obtain sound analysis results. We conducted experi- as solving differential equations. Every floating-point type ments over benchmarks consisting of representative Fortran programs and the evaluation results demonstrate the effi- QuASoQ 2024: 12th International Workshop on Quantitative Approaches ciency, effectiveness, and utility of the analyzer F-IKOS . The to Software Quality, December 03, 2024, Chongqing China main contributions of this work are as follows: ∗ Corresponding author. Envelope-Open zous@nudt.edu.cn (S. Zou); lqchen@nudt.edu.cn (L. Chen); • We proposed an approach to soundly abstract guangshengfan@nudt.edu.cn (G. Fan); renjiehuang@nudt.edu.cn floating-point operations in Fortran programs, ac- (R. Huang); bhyin@nudt.edu.cn (B. Yin) © 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License counting for rounding errors during program analy- Attribution 4.0 International (CC BY 4.0). CEUR ceur-ws.org Workshop ISSN 1613-0073 Proceedings 27 sis. Under real number semantics, the equation 0.1 + 0.2 = 0.3 • We developed F-IKOS , a static analyzer for Fortran holds. But in machines, 𝑟𝑛𝑑(0.1) ⊕𝑓 ,𝑟 𝑟𝑛𝑑(0.2) is not equal programs, to implement the proposed approach. F- to 𝑟𝑛𝑑(0.3). Furthermore, the law of association and distri- IKOS can soundly analyze floating-point types in bution is not always true in floating-point operations. E.g., Fortran programs. it may happen that • Evaluation shows that F-IKOS can handle the com- plex syntax of Fortran programs and produce sound (𝑟𝑛𝑑(𝑎)⊕𝑓 ,𝑟 𝑟𝑛𝑑(𝑏))⊕𝑓 ,𝑟 𝑟𝑛𝑑(𝑐) ≠ 𝑟𝑛𝑑(𝑎)⊕𝑓 ,𝑟 (𝑟𝑛𝑑(𝑏)⊕𝑓 ,𝑟 𝑟𝑛𝑑(𝑐)) analysis results, outperforming other relevant For- tran analyzers. 2.3. Rounding Model of IEEE-754 The rest of the paper is organized as follows. Section A simplified rounding model of the IEEE-754 standard fol- 2 describes background. Section 3 presents the overview lows the equation below: of our analyzer F-IKOS . Section 4 presents the proposed abstraction of floating-point expressions. Section 5 presents 𝑟𝑛𝑑(𝑥) = 𝑥 × (1 + 𝑒) + 𝑑 our analyzer implementation together with experimental where |𝑒| ≤ 𝜖, |𝑑| ≤ 𝛿, and 𝑒 × 𝑑 = 0. When 𝑥 is a normalized results. Section 6 discusses some related work and Section number, it holds that 𝑑 = 0, and when 𝑥 is a denormalized 7 concludes. number, it holds that 𝑒 = 0. Here, 𝜖 denotes the maximum relative error for normalized numbers, and 𝛿 describes the 2. Background maximum absolute error for denormalized numbers for spe- cific precision of floating-point numbers. 2.1. The Fortran Programming Language The Fortran programming language is a well-established 2.4. Linearization high-level language with many syntax standards, such as An interval linear expression is an expression where the Fortran 77 and Fortran 90. Fortran has similarities to other coefficients may be intervals instead of scalars. For instance, high-level programming languages. For example, Fortran in- cludes common control structures such as conditional state- 𝑧 = [𝑏1 , 𝑐1 ]𝑥 + [𝑏2 , 𝑐2 ]𝑦 ments and looping control structures. However, Fortran programs often emphasize numerical computation tasks Interval linear expressions, in which the coefficients are more than logical control functions. This is reflected by the intervals, can be abstracted into linear expressions with fact that Fortran has a wealth of intrinsic functions, such as scalar coefficients. This process is linearization, and it is the trigonometric functions sin, cos, asin, and acos. defined as follows: Besides, Fortran has a rich set of convenient array op- Definition 1 (Linearization). An interval linear ex- erations. Fortran supports flexible array boundaries, such pression ∑𝑖 [𝑎𝑖 , 𝑏𝑖 ] × 𝑥𝑖 + [𝑐, 𝑑] can be linearized into a linear as 𝑖𝑛𝑡𝑒𝑔𝑒𝑟 ∶∶ 𝑣(−3 ∶ 3), indicating that the index of array expression ∑𝑖 𝑒𝑖 ×𝑥𝑖 +[𝑐 ′ , 𝑑 ′ ], where 𝑒𝑖 ∈ [𝑎𝑖 , 𝑏𝑖 ] and satisfying 𝑣 ranges from -3 to 3. It also provides a range of intrinsic ∑𝑖 [𝑎𝑖 , 𝑏𝑖 ] × 𝑥𝑖 + [𝑐, 𝑑] ⊆ ∑𝑖 𝑒𝑖 × 𝑥𝑖 + [𝑐 ′ , 𝑑 ′ ] for all 𝑥𝑖 ∈ [𝑥𝑖 , 𝑥𝑖 ] functions for arrays, including sum and product, as well as where 𝑥𝑖 ≤ 𝑥𝑖 ≤ 𝑥𝑖 . matmul and dot_product for computing matrix products and dot products. Fortran inherently supports multidimen- sional arrays and offers mechanisms for array slicing and 3. Overview reshaping. For instance, the reshape function facilitates In this section, we give an overview of our approach. We altering the number of dimensions and the size of each develop a static analyzer on top of IKOS [10], named F-IKOS , dimension within an array. Due to these characteristics, to perform sound analysis of floating-point types in Fortran Fortran is widely used in scientific and high-performance programs. The architecture and workflow of F-IKOS are computing. illustrated in Fig. 1, highlighting our modifications to en- able the sound analysis of floating-point types in Fortran 2.2. The Floating-point Representation programs. Initially, F-IKOS takes Fortran programs as input and uses the parser Flang [5] to translate programs into The floating-point representation adheres to the IEEE-754 LLVM IR. Subsequently, after optimization and processing, standard. Many high-precision real numbers, cannot be F-IKOS uses extended IKOS together with numerical ab- exactly represented by floating-point numbers. The IEEE- stract domains from Apron [6] to analyze the LLVM IR and 754 standard provides four rounding modes: nearest, zero, obtain invariants of programs. Finally, potential runtime −∞, and +∞, to approximate real numbers using floating- errors in programs are checked by utilizing these invariants. point numbers. This approximation can introduce rounding errors, which result in inexactness. Due to rounding errors, mathematical properties followed 4. Approach by real number operations do not hold in floating-point op- erations. We illustrate it with an example. To distinguish be- Fortran programs involve numerous floating-point opera- tween real and floating-point numbers and their respective tions, and analyzing these programs within the abstract in- operators, we employ 𝑟𝑛𝑑(⋅) to represent floating-point num- terpretation framework by simply treating floating-point ex- bers in machines and denote real number operators using pressions as real-number expressions may result in unsound symbols +, −, ×, /, while denoting floating-point operators results. This occurs because floating-point numbers in pro- using ⊕𝑓 ,𝑟 , ⊖𝑓 ,𝑟 , ⊗𝑓 ,𝑟 , ⊘𝑓 ,𝑟 where the subscripts 𝑓 , 𝑟 denote grams are rounded before being passed to abstract domains different precision and rounding modes. Real numbers like (e.g., Apron [6]). For example, within the polyhedra abstract 0.1, 0.2, and 0.3 cannot be exactly represented by machines. domain, linear constraints between variables are collected 28 LLVM Immediate Abstract Flang LLVM2AR Fortran program Representation Representation (LLVM IR) (AR) Front-end Floating- Fixed Point Analyzer: point Type Uses Analysis result Iterators IKOS Sound Abstraction ... of Floating- point Apron Numerical Abstract Abstract Domain Linearization Domains Library IKOS Library Figure 1: Overview of F-IKOS and utilized to infer the program’s invariants. Due to the Precision 𝜖 𝛿 single (32 bits) 2−23 2−149 presence of floating-point numbers and operators (e.g., ⊕𝑓 ,𝑟 , double (64 bits) 2−52 2−1074 ⊖𝑓 ,𝑟 , ⊗𝑓 ,𝑟 , ⊘𝑓 ,𝑟 ), these expressions are under floating-point quad (128 bits) 2−112 2−16494 semantics. Directly interpreting floating-point expressions as expressions under real-number semantics introduces un- Table 1 soundness to the analysis. For instance, (rnd(𝑥) ⊕𝑓 ,𝑟 rnd(𝑦)) Related/Absolute rounding errors for various types is not equivalent to (𝑥 + 𝑦) under real-number semantics. To address this challenge, Miné [19] proposes to over- approximately abstract floating-point expressions into real- denormalized numbers for specific precision of 𝑥. Table 1 number expressions. The approach includes the following illustrates the values of 𝜖 and 𝛿 for various floating-point three steps: types. To enhance generality, we express the conversion 1. Abstract the deterministic semantics of floating- between a floating-point number and its corresponding real point expressions into non-deterministic semantics interval range before rounding using Formula 3. This pro- on real-number expressions. vides an over-approximation of 𝑥 given by Formula 1 and 2. Convert the non-deterministic semantics of real 2 regardless of whether 𝑥 is a normalized or denormalized numbers into deterministic semantics for real num- number. bers. 𝑟𝑛𝑑(𝑥) = 𝑥 × ([1 − 𝜖, 1 + 𝜖]) + [−𝛿, 𝛿] (3) 3. Analyze programs with real-number operations us- ing abstract domains initially designed for programs Abstraction of Expressions with Floating-Point Oper- with real-number types. ators. Miné [19] proposes a method for abstracting expres- In this section, we present the following three steps: sions involving floating-point operators into real-number sound abstraction of floating-point expressions, lineariza- expressions. This approach captures rounding errors of tion of interval linear expressions, and the analysis of pro- floating-point arithmetic by over-approximating the behav- grams using abstract domains. ior of floating-point operators using real-number semantics. Assume that 𝑟𝑛𝑑(𝑥) and 𝑟𝑛𝑑(𝑦) are two floating-point expressions, with 𝑥 and 𝑦 representing the corresponding 4.1. Abstraction of Floating-point real-number expressions. Let 𝑎 and 𝑏 be real numbers, and Expressions let 𝜖 and 𝛿 denote the relative and absolute errors, respec- Abstraction of floating-point numbers. Floating-point tively, which depend on the precision of the floating-point types in Fortran programs adhere to the IEEE-754 standard. types. Given the value of a floating-point number and its precision, Non-linear operators (such as ⊗𝑓 ,𝑟 and ⊘𝑓 ,𝑟 ) can be han- using the rounding model outlined in Section 2.3, we can dled by applying the corresponding operator on intervals compute the relation of 𝑟𝑛𝑑(𝑥) and 𝑥 (the interval range) as after ”intervalizing” the arguments [19]. The operator | ⋅ |𝜄 follows. is used to ”intervalize” the argument by a single interval When 𝑥 is a normalized number, the relation of 𝑥 and [19]. When multiplying two linear forms that have not been 𝑟𝑛𝑑(𝑥) can be represented as: reduced to an interval, the operator | ⋅ |𝜄 can be applied to either argument. Similarly, operator | ⋅ |𝜄 can be applied to 𝑟𝑛𝑑(𝑥) = 𝑥 × [1 − 𝜖, 1 + 𝜖] (1) the divisor to obtain a single interval before performing division. When 𝑥 is a denormalized number (i.e., close to zero), the relation of 𝑥 and 𝑟𝑛𝑑(𝑥) is given by: 𝑟𝑛𝑑(𝑥) = 𝑥 + [−𝛿, 𝛿] (2) where 𝜖 denotes the maximum relative error for normalized numbers, and 𝛿 represents the maximum absolute error for 29 The abstraction is described as follows [19]: Similarly, we apply | ⋅ |𝜄 to the divisor to obtain a single interval before performing the division. The floating-point 𝑥 ⊕𝑓 ,𝑟 𝑦 = (𝑥 + 𝑦) × [1 − 𝜖, 1 + 𝜖] + [−𝛿, 𝛿] expression 𝑟𝑛𝑑(𝑥) ⊘𝑓 ,𝑟 𝑟𝑛𝑑(𝑦) can then be abstracted into its 𝑥 ⊖𝑓 ,𝑟 𝑦 = (𝑥 − 𝑦) × [1 − 𝜖, 1 + 𝜖] + [−𝛿, 𝛿] corresponding real-number expression, as illustrated below: 𝑥 ⊗𝑓 ,𝑟 [𝑎0 , 𝑏0 ] = 𝑥 × [1 − 𝜖, 1 + 𝜖] ⋅ [𝑎0 , 𝑏0 ] + [−𝛿, 𝛿] 𝑥×[(1−𝜖)2 , (1+𝜖)2 ]/[𝑎, 𝑏]+[−(1+𝜖)𝛿, (1+𝜖)𝛿]/[𝑎, 𝑏]+[−𝛿, 𝛿] (10) [𝑎0 , 𝑏0 ] ⊗𝑓 ,𝑟 𝑥 = 𝑥 ⊗𝑓 ,𝑟 [𝑎0 , 𝑏0 ] The coefficients of variables within the real-number ex- 𝑥 ⊗𝑓 ,𝑟 𝑦 = 𝑥 × [1 − 𝜖, 1 + 𝜖] ⋅ |𝑦|𝜄 + [−𝛿, 𝛿] (4) pressions obtained by abstraction are represented as real- 𝑜𝑟 number intervals. However, many abstract domains cannot process such interval-coefficient forms, as they only support 𝑥 ⊗𝑓 ,𝑟 𝑦 = 𝑦 × [1 − 𝜖, 1 + 𝜖] ⋅ |𝑥|𝜄 + [−𝛿, 𝛿] linear expressions. 𝑥 ⊘𝑓 ,𝑟 [𝑎0 , 𝑏0 ] = 𝑥 × [1 − 𝜖, 1 + 𝜖]/[𝑎0 , 𝑏0 ] + [−𝛿, 𝛿] 𝑥 ⊘𝑓 ,𝑟 𝑦 = 𝑥 × [1 − 𝜖, 1 + 𝜖]/|𝑦|𝜄 + [−𝛿, 𝛿] 4.2. Linearization of Interval Linear Abstraction of Floating-point Expressions. In Fortran Expressions programs, variables (or constants) and operators in ex- To enable existing numerical abstract domains (e.g., poly- pressions are under floating-point semantics. We abstract hedra abstract domain) to handle interval linear expres- expressions that involve floating-point variables and per- sions, Miné [19] proposes to linearize these interval lin- form floating-point arithmetic into real-number expressions, ear expressions to linear expressions. The core idea is which involve real-number variables and real-number oper- as follows: Supposing variable 𝑥𝑖 ranges over the interval ators. [𝑥𝑖 , 𝑥𝑖 ], an interval linear expression Σ𝑖 [𝑎𝑖 , 𝑏𝑖 ] × 𝑥𝑖 + [𝑐, 𝑑] can The floating-point expression 𝑟𝑛𝑑(𝑥) ⊕𝑓 ,𝑟 𝑟𝑛𝑑(𝑦) can be be over-approximated by a linear expression of the form abstracted into a real-number expression as follows: Σ𝑖 𝑒𝑖 × 𝑥𝑖 + [𝑐 ′ , 𝑑 ′ ]. This approach converts real-number inter- val linear expressions into real-number linear expressions 𝑟𝑛𝑑(𝑥) ⊕𝑓 ,𝑟 𝑟𝑛𝑑(𝑦) with scalar coefficients. The existing numerical abstraction where domain initially designed for real-number semantics can di- 𝑟𝑛𝑑(𝑥) = 𝑥 × [1 − 𝜖, 1 + 𝜖] + [−𝛿, 𝛿] rectly analyze these expressions. We present our approach to linearize interval linear expressions. 𝑟𝑛𝑑(𝑦) = 𝑦 × [1 − 𝜖, 1 + 𝜖] + [−𝛿, 𝛿] Drawing inspiration from [2, 19], we define the lineariza- Substituting these into the expression, we get tion of interval linear expressions within real-number se- mantics as follows: (𝑥×([1−𝜖, 1+𝜖])+[−𝛿, 𝛿])⊕𝑓 ,𝑟 (𝑦 ×([1−𝜖, 1+𝜖])+[−𝛿, 𝛿]) (5) Definition 2 (Linearization Operator). Given an in- terval linear expression 𝜑 ∶ (∑𝑖 [𝑎𝑖 , 𝑏𝑖 ] × 𝑥𝑖 + [𝑐, 𝑑]), and Since 𝑥 ⊕𝑓 ,𝑟 𝑦 = 𝑟𝑛𝑑(𝑥 + 𝑦), we convert Formula 5 as: letting x ∶= [𝑥, 𝑥] be the bounding box of variable x, the 𝑟𝑛𝑑(((𝑥 + 𝑦)([1 − 𝜖, 1 + 𝜖]) + 2 × [−𝛿, 𝛿])) linearization operator is defined as 𝑑𝑒𝑓 Thus, the expression 𝑟𝑛𝑑(𝑥) ⊕𝑓 ,𝑟 𝑟𝑛𝑑(𝑦) can be abstracted 𝜁 (𝜑, x) = ∑ 𝑒𝑖 × 𝑥𝑖 + [𝑐 ′ , 𝑑 ′ ] as: 𝑖 where 𝑒𝑖 is any real number in the interval [𝑎𝑖 , 𝑏𝑖 ], and (𝑥 + 𝑦)[(1 − 𝜖)2 , (1 + 𝜖)2 ] + [−(3 + 2𝜖)𝛿, (3 + 2𝜖)𝛿] (6) [𝑐 ′ , 𝑑 ′ ] denotes the resulting interval of ∑𝑖 [𝑎𝑖 − 𝑒𝑖 , 𝑏𝑖 − 𝑒𝑖 ] × By following this approach, the floating-point expression [𝑥𝑖 , 𝑥𝑖 ] + [𝑐, 𝑑]. Generally, we choose the midpoint of the 𝑟𝑛𝑑(𝑥) ⊖𝑓 ,𝑟 𝑟𝑛𝑑(𝑦) can be abstracted into its corresponding interval 𝑒𝑖 = (𝑎𝑖 + 𝑏𝑖 ) × 0.5. real-number expression, as illustrated: We provide the proof of the soundness of the linearization operator through the following reasoning: (𝑥 − 𝑦)[(1 − 𝜖)2 , (1 + 𝜖)2 ] + [−(3 + 2𝜖)𝛿, (3 + 2𝜖)𝛿] (7) ∑ [𝑎𝑖 , 𝑏𝑖 ] × 𝑥𝑖 + [𝑐, 𝑑] When multiplying two linear forms, the operator | ⋅ |𝜄 can 𝑖 be applied to either argument to obtain an interval range ⟺ ∑ (𝑒𝑖 + [𝑎𝑖 − 𝑒𝑖 , 𝑏𝑖 − 𝑒𝑖 ]) × 𝑥𝑖 + [𝑐, 𝑑] of the argument. In this case, we apply | ⋅ |𝜄 to the second 𝑖 argument. The floating-point expression 𝑟𝑛𝑑(𝑥) ⊗𝑓 ,𝑟 𝑟𝑛𝑑(𝑦) ⟺ ∑ 𝑒𝑖 × 𝑥𝑖 + ∑[𝑎𝑖 − 𝑒𝑖 , 𝑏𝑖 − 𝑒𝑖 ] × 𝑥𝑖 + [𝑐, 𝑑] can be abstracted through the following steps: 𝑖 𝑖 Assume [𝑎, 𝑏] = |𝑟𝑛𝑑(𝑦)|𝜄 × [1 − 𝜖, 1 + 𝜖] + [−𝛿, 𝛿], then can be over-approximated as 𝑟𝑛𝑑(𝑥) ⊗𝑓 ,𝑟 𝑟𝑛𝑑(𝑦) can be converted into ∑ 𝑒𝑖 × 𝑥𝑖 + ([𝑎𝑖 − 𝑒𝑖 , 𝑏𝑖 − 𝑒𝑖 ] × [𝑥𝑖 , 𝑥𝑖 ]) + [𝑐, 𝑑] 𝑖 𝑟𝑛𝑑(𝑥) ⊗𝑓 ,𝑟 [𝑎, 𝑏] (8) since it holds that [𝑎𝑖 − 𝑒𝑖 , 𝑏𝑖 − 𝑒𝑖 ] × 𝑥𝑖 ⊆ [𝑎𝑖 − 𝑒𝑖 , 𝑏𝑖 − 𝑒𝑖 ] × [𝑥𝑖 , 𝑥𝑖 ], Given that 𝑟𝑛𝑑(𝑥) = 𝑥 × [1 − 𝜖, 1 + 𝜖] + [−𝛿, 𝛿] and 𝑥 ⊗𝑓 ,𝑟 where 𝑎𝑖 ≤ 𝑒𝑖 ≤ 𝑏𝑖 and 𝑥𝑖 ≤ 𝑥𝑖 ≤ 𝑥𝑖 . [𝑎0 , 𝑏0 ] = 𝑟𝑛𝑑(𝑥 × [𝑎0 , 𝑏0 ]) = 𝑥 × [1 − 𝜖, 1 + 𝜖] ⋅ [𝑎0 , 𝑏0 ] + [−𝛿, 𝛿], Note that following the same principle, an interval linear we can express Formula 8 as follows: inequality ∑𝑖 [𝑎𝑖 , 𝑏𝑖 ]×𝑥𝑖 +[𝑐, 𝑑] ≤ 0 can be also linearized into a linear inequality in the form of ∑𝑖 𝑒𝑖 ×𝑥𝑖 +[𝑐 ′ , 𝑑 ′ ] ≤ 0 in the 𝑟𝑛𝑑 (𝑥 × [1 − 𝜖, 1 + 𝜖] ⋅ [𝑎, 𝑏] + [−𝛿, 𝛿] ⋅ [𝑎, 𝑏]) sense of weak solution [23]. It means that a weak solution Thus, the expression 𝑟𝑛𝑑(𝑥) ⊗𝑓 ,𝑟 𝑟𝑛𝑑(𝑦) can be abstracted of an interval linear inequality ∑𝑖 [𝑎𝑖 , 𝑏𝑖 ] × 𝑥𝑖 + [𝑐, 𝑑] ≤ 0 will as: be a solution of ∑𝑖 𝑒𝑖 × 𝑥𝑖 + [𝑐 ′ , 𝑑 ′ ] ≤ 0 (but the reverse does not hold). This approach over-approximates interval linear 𝑥 ×[(1−𝜖)2 , (1+𝜖)2 ]⋅[𝑎, 𝑏]+[−(1+𝜖)𝛿, (1+𝜖)𝛿]⋅[𝑎, 𝑏]+[−𝛿, 𝛿] expressions (or inequalities) up into linear expressions (or (9) inequalities). 30 4.3. Analyze programs with existing instances. The experimental results are presented in Ta- abstract domains ble 2, where ”F-IKOS Time (s)”, ”SMACK Time(s)” and ”CIVL Time (s)” denote the execution time of F-IKOS , SMACK , and Due to the sound handling of rounding errors inherent in CIVL , respectively. In the last row of Table 2, the average floating-point operations through the above abstraction and execution time of programs is recorded. linearization procedure, we can now obtain sound results Specifically, SMACK successfully verified only 19 out of 36 using abstract domains initially designed for real-number programs. In contrast, CIVL correctly verified all 36 pro- semantics. grams, and F-IKOS successfully completed the analysis of the majority (30 out of 36). Further analysis of the unverified programs by F-IKOS reveals that most required disjunctive 5. Implementation and Evaluation invariants for successful verification, are out of the expres- siveness of the used polyhedra abstract domain, whereas 5.1. Implementation CIVL , with the help of the SMT solver (i.e., Z3), can address We have implemented a static analyzer for Fortran programs, them effectively. named F-IKOS , with over 4K LOC of C++ code by extending Furthermore, a comparative analysis of the average ex- IKOS . F-IKOS is endowed with the capability to perform ecution time reveals that F-IKOS exhibits shorter analysis sound analysis of floating-point types in Fortran programs. time, approximately 5% of SMACK ’s and 10% of CIVL ’s. The experimental results underscore F-IKOS ’s ability to achieve 5.2. Research Questions and Experimental a delicate balance between analysis efficiency and effec- tiveness, demonstrating its strengths compared to existing Setup state-of-the-art Fortran analyzers. To evaluate F-IKOS , we compare it with two most relevant RQ-1 Answer: F-IKOS undergoes comparison with Fortran program analyzers, SMACK [7] and CIVL [8]. Both SMACK and CIVL for the analysis of 36 Fortran programs. SMACK and CIVL translate Fortran programs into IR for sub- It successfully verified 30 out of 36 programs, exhibiting a sequent verification using IR-compatible verifiers, mainly shorter average execution time compared with state-of-the- based on model checking. They are designed to verify cer- art approach and about 10% of CIVL ’s. The results highlight tain program properties but do not directly detect potential the efficiency and effectiveness of F-IKOS in analyzing sim- errors in Fortran programs. ple Fortran programs. We investigate the following three research questions across the analyzers: 5.4. RQ2: Handling complex feature • RQ1: How effective is F-IKOS in analyzing simple operations Fortran programs? We analyzed 45 Fortran programs from the second bench- • RQ2: How well does F-IKOS handle complex fea- mark. The programs in this benchmark utilize features and tures of Fortran programs? intrinsic functions in Fortran that have not been previously • RQ3: How does F-IKOS perform when applied to examined. Some programs exemplify common Fortran pro- real-world Fortran programs? gramming conventions, while others involve algorithmic implementations. The inclusion of integer and floating- To address these questions, we conducted three exper- point types, along with arrays, increases the complexity of iments to evaluate the capabilities of F-IKOS . The bench- analyzing the programs. marks employed in our experiments are categorized into In addition to the Fortran 90 standard programs, some three distinct classes: programs following Fortran 77, and Fortran 95 standards are • 36 Fortran programs used by SMACK [7] and CIVL [8], also included in bold in the table. The evaluation results in which are used to evaluate F-IKOS ’s ability to handle the efficiency and effectiveness of the analyzers are shown simple syntaxs and accomplish verification tasks. in Table 3. ”F-IKOS (s)” and ”F-IKOS FP” illustrate the Exe- • 45 real-world Fortran programs extracted from open- cution Time and False Positives (FP) of F-IKOS , respectively. source repositories [22, 21], encompassing various Fortran syntax standards. The experimental results demonstrate that both SMACK • 10 artificially constructed programs, derived from and CIVL to analyze the 45 programs in benchmark and the repository [20], designed to evaluate the capabil- find that SMACK can parse 37 out of 45 programs, whereas CIVL can only parse 3 out of 45. In contrast, F-IKOS can ity of F-IKOS in detecting runtime errors associated with floating-point types. analyze all programs within an average time of 1.79s while maintaining an acceptable average of 3 false positives per All experiments were conducted on a PC running Ubuntu program. In particular, when analyzing programs that use 20.04 (16GB Memory) in the Oracle VirtualBox 6.1.30 with intrinsic functions to manipulate Fortran’s arrays, F-IKOS a 3.3GHz Intel Core i9 CPU. The abstract domain used is issues some false positives. The reason for these false pos- Polka [6], which is an implementation of the Polyhedra itives lies in the differences between Fortran arrays and abstract domain in Apron. common high-level language arrays. RQ-2 Answer: F-IKOS maintains analytical capabilities 5.3. RQ1: Verifying simple Fortran when dealing with intrinsic functions. F-IKOS successfully analyzed all Fortran programs within an average time of programs 1.79s. Moreover, F-IKOS can be used to analyze Fortran We analyzed 36 simple Fortran programs from the first programs adhering to multiple syntax standards, and the benchmark [7, 8], excluding parallel and recursive program results show that F-IKOS performs better than SMACK and 31 ID Program Name Loc F-IKOS Time (s) SMACK Time (s) CIVL Time (s) P1 array 15 0.14 3.22 2.9 P2 arrary_fail 11 0.14 2.79 3.19 P3 compound 19 0.26 3.23 1.41 P4 compound_fail 19 0.31 2.77 1.48 P5 compound_fail_2 19 0.30 3.64 1.71 P6 compute 13 0.12 3.14 1.57 P7 compute_fail 13 0.15 2.67 1.50 P8 forloop 15 0.16 3.62 1.5 P9 forloop_fail 15 0.21 2.99 1.89 P10 function 36 0.18 4.10 1.82 P11 function_fail 36 0.19 3.83 1.62 P12 function_fail_2 35 0.23 6.29 1.74 P13 function_fail_3 35 0.25 7.39 1.65 P14 hello 14 0.14 3.07 1.39 P15 hello_fail 13 0.16 2.63 1.62 P16 inout 19 0.17 2.20 1.54 P17 inout_fail 19 0.20 2.70 1.51 P18 pointer 15 0.18 3.28 1.40 P19 pointer_fail 15 0.22 2.75 1.46 P20 abs 15 - - 1.46 P21 abs_bad 15 - - 1.54 P22 array_section 29 - - 3.63 P23 array_section_bad 30 - - 3.88 P24 intent_inout 24 0.19 - 2.02 P25 intent_out 25 0.17 - 2.66 P26 intent_out_bad 24 0.21 - 2.28 P27 mod_impl 25 0.17 - 2.05 P28 mod_impl_bad 25 0.18 - 2.11 P29 mod_spec 19 0.12 - 1.48 P30 mult_impl 25 0.13 - 1.73 P31 mult_impl_bad 25 0.13 - 1.86 P32 mult_spec 21 0.16 - 1.46 P33 short_circuit 37 - - 3.57 P34 short_circuit_bad 35 - - 3.53 P35 truncate 14 0.12 - 1.42 P36 truncate_bad 14 0.14 - 1.63 Average 22 0.18 3.49 1.98 Table 2 Experimental results on 36 Fortran programs CIVL . used by machines, our analysis of Fortran programs remains sound, ensuring consistent and sound analysis results across 5.5. RQ3: Handling real-world programs different computational environments. We find that some programs require more time for analy- We evaluated the capability of F-IKOS to detect runtime sis. Two primary factors contribute to the long execution errors in larger programs from the third benchmark. To time. Firstly, our experiments utilize the polyhedra abstract objectively demonstrate F-IKOS ’s capabilities, we intention- domain, which can be computationally expensive for certain ally injected 10 division-by-zero bugs into some of these programs. Additionally, real-world programs often exhibit programs. Our evaluation metrics include both analysis distinct numerical characteristics, particularly due to the time and accuracy. The accuracy of the analysis is defined presence of loops and arrays, which demand more time- as follows: intensive processing. 𝑇𝑃 𝐴𝑐𝑐𝑢𝑟𝑎𝑐𝑦 = RQ-3 Answer: The results show that SMACK parses 7 𝑇𝑃 + 𝐹𝑃 out of 10 Fortran programs, while CIVL fails to parse any. where 𝑇 𝑃 represents the number of true positives, and 𝐹 𝑃 Moreover, neither tools can detect runtime errors in the pro- denotes the number of false positives. grams they parse. In contrast, F-IKOS soundly analyzes all The experimental results are represented in Table 4, programs and successfully detects runtime errors, demon- where ”F-IKOS TP” and ”F-IKOS FP” denote true positives strating its effectiveness in handling Fortran numerical pro- and false positives of F-IKOS , respectively. SMACK success- grams. fully parsed 7 programs, but it failed to detect runtime errors within them. CIVL couldn’t parse any of the 10 programs. In contrast, F-IKOS detected all runtime errors, achieving 6. Related Work an accuracy of 22.2%. The programs include both custom and Fortran intrinsic functions, exhibiting more complex In the literature, there exists several tools to analyze or numerical characteristics. The results demonstrate the ef- verify Fortran programs. Some tools such as f2c [3] and fectiveness of F-IKOS to detect runtime errors in numerical FABLE [11], involve converting Fortran programs into other computation programs. Regardless of the rounding mode high-level languages (such as C++) programs, and then use 32 ID Program Loc F-IKOS (s) F-IKOS FP SMACK (s) CIVL (s) P1 arguments 41 2.40 0 2.43 - P2 associate_bounds 9 0.99 0 2.71 - P3 bounds 12 0.88 8 3.24 - P4 boz 11 1.83 1 2.85 - P5 case_insensitivity 15 0.18 1 2.43 - P6 column_major 18 0.12 0 2.9 - P7 compare_floats 15 2.14 0 3.25 - P8 data 21 0.18 5 2.91 - P9 derived_type_composition 21 1.31 0 2.73 - P10 derived_type_implied_do 19 1.69 5 3.34 - P11 dimension 13 0.36 0 2.67 - P12 direct_access 28 5.16 15 - - P13 do_loop_index 18 0.17 0 3.14 0.99 P14 do_while 32 1.78 12 3.27 - P15 error_stop 20 0.26 1 - - P16 get_command 23 1.49 3 3.27 - P17 implicit_save 41 0.39 7 3.17 - P18 intrinsic 50 1.18 0 2.93 - P19 list_directed_read 20 1.65 0 3.23 - P20 loop 10 0.16 4 2.91 1.59 P21 loop_bound 32 0.59 0 3.28 - P22 loop_index 22 0.34 5 3.05 - P23 loop_label 34 4.45 15 3.64 - P24 merge 10 0.82 0 3.26 - P25 module 16 0.12 0 2.7 - P26 module_parameter 35 0.17 0 2.62 - P27 open_file 27 1.93 2 2.98 - P28 overlapping_arg 31 1.69 0 2.84 - P29 print_implied_do_loop 22 3.10 16 4.27 - P30 protected 29 0.34 0 2.87 - P31 recursive_io 37 0.51 0 - - P32 scratch 19 1.27 6 3.47 - P33 select_case 21 0.99 0 3.56 - P34 slash 15 0.85 0 2.9 - P35 sum_exit 14 0.23 5 3.11 1.52 P36 trim 9 0.26 0 2.63 - P37 type_constructor_optional 23 0.75 0 2.75 - P38 value 45 0.41 4 2.73 - P39 write_char 15 0.76 0 2.67 - P40 xrandom_int 17 4.60 4 - - P41 swap_arrays 51 5.12 2 - - P42 average 40 17.81 8 - - P43 submod 41 0.56 0 - - P44 linear_equations 27 7.29 3 - - P45 temp_converter 40 1.47 2 2.19 - Table 3 Experimental results on 45 Fortran programs verifiers to conduct verification. Alternatively, FORTRAN- addressing runtime error detection. In this paper, we use lint [13], ftnchek [12] and Coverity [14] specializes in F-IKOS to support the sound analysis of Fortran programs predefined, general-purpose defect detection within For- with complex features. tran programs, lacking the comprehensive capability to ana- lyze program properties semantically. In contrast, CamFort [15] incorporates a lightweight declarative specification lan- 7. Conclusion guage capable of both checking and inferring specifications. In this paper, we present F-IKOS , an abstract interpretation- SMACK [7] and CIVL [8] translate Fortran programs into based static analyzer designed for Fortran programs. Partic- Intermediate Representation (IR) for subsequent verification ularly, F-IKOS provides a sound analysis for floating-point using IR-compatible verifiers. Specifically, SMACK converts types in programs. F-IKOS first abstracts floating-point ex- Fortran programs to LLVM IR and then verifies LLVM IR via pressions into real-number expressions with interval coeffi- Corral [9], wherein Corral restricts the syntax of expres- cients, then linearizes these expressions into real-number ex- sions in this language to one that can be efficiently decided pressions with scalar coefficients. These linear expressions by a SMT solver. CIVL [8] converts Fortran programs to are subsequently handled by abstract domains originally CIVL-C which is an Intermediate Verification Language designed for real-number types to produce sound analy- (IVL), which is subsequently verified using model check- sis results. Evaluation of three benchmarks demonstrates ing and symbolic execution. However, their work mainly F-IKOS ’s efficiency and effectiveness than other relevant focuses on the verification of Fortran programs, without analyzers in the analysis of Fortran programs. 33 ID Program Name Loc F-IKOS (s) F-IKOS TP F-IKOS FP SMACK (s) CIVL (s) P1 converter 41 1.06 0 2 2.95 - P2 bubblesort 62 169.81 0 10 - - P3 libconstants 107 0.38 0 0 2.17 - P4 simpson 53 11.62 0 5 3.65 - P5 differentiation 39 4.48 0 5 - - P6 div 111 0.15 6 0 2.98 - P7 expr 110 0.12 2 0 3.08 - P8 function 112 12.01 2 0 3.05 - P9 palindrome 51 63.05 0 7 - - P10 trapezodial 102 18.79 0 6 3.27 - Table 4 Experimental results on 10 Fortran programs 8. Acknowledgments with FABLE, Source Code for Biology and Medicine, 7 (2012), pp. 1-11. We thank the reviewers for their constructive feedback. This [12] Mak, L., Taheri, P., An Automated Tool for Upgrading work is supported by the National Key R&D Program of Fortran Codes, Software, 1(3) (2022), pp. 299-315. China (No.2022YFA1005101) and the National Natural Sci- [13] FORTRAN-lint: a pre-compile analysis tool, URL: ence Foundation of China (Nos.62032024,62102432). https://stellar.cleanscape.net/docs_lib/data_F- lint2.pdf. [14] Coverity Fortran Syntax Analysis, URL: https://sig- References product-docs.synopsys.com/bundle/coverity- [1] Response to issues about floating-point program anal- docs/page/webhelp-files/fortran_start.html#in- ysis in IKOS, 2023. URL: https://github.com/NASA-SW- troduction. VnV/ikos/issues/224. [15] Orchard, D., Contrastin, M., Danish, M., Rice, A., Ver- [2] Liqian Chen, Sound floating-point and non-convex ifying spatial properties of array computations, Pro- static analysis using interval linear abstract domains, ceedings of the ACM on Programming Languages, 2010. National University of Defense Technology. 1(OOPSLA) (2017), pp. 1-30. [3] Feldman, Stuart I, A Fortran to C converter, ACM SIG- [16] Rakamarić, Z., Emmi, M., SMACK: Decoupling source PLAN Fortran Forum. Vol. 9. No. 2. New York, NY, language details from verifier implementations, in: USA: ACM, 1990. Computer Aided Verification: 26th International Con- [4] LLVM homepage, 2000. URL: https://llvm.org/. ference, CAV 2014, Held as Part of the Vienna Summer [5] Flang Fortran language front-end homepage. URL: of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014, https://github.com/flang-compiler/flang. Proceedings, Springer, Berlin, Heidelberg, 2014, pp. [6] Jeannet, B., Miné, A., Apron: A library of numerical 106-113. abstract domains for static analysis, in: Computer [17] BLAS (Basic Linear Algebra Subprograms), URL: Aided Verification, Springer, Berlin, Heidelberg, 2009, https://www.netlib.org/blas/. pp. 661-667. [18] Cousot, P., Cousot, R., Abstract interpretation: a uni- [7] Garzella, J.J., Baranowski, M., He, S., Rakamaric, Z., fied lattice model for static analysis of programs by Leveraging compiler intermediate representation for construction or approximation of fixpoints, in: Pro- multi- and cross-language verification, in: Verification, ceedings of the 4th ACM SIGACT-SIGPLAN Sympo- Model Checking, and Abstract Interpretation: 21st sium on Principles of Programming Languages, 1977, International Conference, VMCAI 2020, New Orleans, pp. 238-252. LA, USA, January 16-21, 2020, Proceedings, Springer, [19] Miné, A., Relational abstract domains for the detection Berlin, Heidelberg, 2020, pp. 90-111. of floating-point run-time errors, in: European Sym- [8] Wu, W., Hückelheim, J., Hovland, P.D., Siegel, S.F., Ver- posium on Programming, Springer, Berlin, Heidelberg, ifying Fortran Programs with CIVL, in: International 2004, pp. 3-17. Conference on Tools and Algorithms for the Construc- [20] fortranlib2024 homepage, URL: https://github.com/as- tion and Analysis of Systems, Springer, Berlin, Heidel- trofrog/fortranlib. berg, 2022, pp. 106-124. [21] FortranTip homepage, URL: https://github.com/Beli- [9] Lal, A., Qadeer, S., Lahiri, S.K., A solver for reachability avsky/FortranTip. modulo theories, in: Computer Aided Verification: [22] Fortran4Researchers homepage, URL: 24th International Conference, CAV 2012, Berkeley, https://github.com/WarwickRSE/Fortran4Re- CA, USA, July 7-13, 2012, Proceedings, Springer, Berlin, searchers. Heidelberg, 2012, pp. 427-443. [23] Fiedler, M., Nedoma, J., Ramík, J., Rohn, J., Zimmer- [10] Brat, G., Navas, J.A., Shi, N., Venet, A., IKOS: A frame- mann, K., Solvability of systems of interval linear equa- work for static analysis based on abstract interpreta- tions and inequalities, in: Linear Optimization Prob- tion, in: Software Engineering and Formal Methods: lems with Inexact Data, Springer, Berlin, Heidelberg, 12th International Conference, SEFM 2014, Grenoble, 2006, pp. 35-77. France, September 1–5, 2014, Proceedings, Springer, Berlin, Heidelberg, 2014, pp. 271-277. [11] Grosse-Kunstleve, R.W., Terwilliger, T.C., Sauter, N.K., Adams, P.D., Automatic Fortran to C++ conversion 34