Introduction

The Fortran programming language is one of the oldest high-level programming languages and one of the first to be widely adopted for scientific computing. Additionally, several numerical computation libraries, including BLAS [17], which are developed in Fortran, have significantly contributed to the widespread use of Fortran in domains such as numerical computing and high-performance computing. Compared with mainstream high-level programming languages such as C++ and Java, Fortran possesses a distinctive set of features, such as powerful array manipulation and abundant intrinsic functions for numerical computation.

However, Fortran programs are prone to potential runtime errors related to numerical aspects such as divisionby-zero and arithmetic overflow due to the large number of numerical operations. Researchers have dedicated efforts to the analysis and verification of Fortran programs. Previous research on the analysis of Fortran programs can be mainly classified into three categories: Firstly, approaches such as f2c [3] and FABLE [11] convert Fortran programs to other high-level language programs and verify them using verifiers over the converted high-level language programs. Secondly, approaches such as SMACK [7] and CIVL [8] translate Fortran programs to Intermediate Representation (IR), which is then verified using verifiers for IR, mainly based on model checking. Additionally, some static analyzers such as FORTRAN-lint [13], ftnchek [12] and Coverity [14] detect certain generic defects, such as dead code and variable usage problems, using pre-defined patterns.

Fortran programs are characterized by the extensive use of floating-point operations, which are crucial for achieving high precision and scale in numerical computing tasks, such as solving differential equations. Every floating-point type has a specific finite precision and cannot represent all real numbers exactly, leading to inherent and pervasive rounding errors in Fortran programs. If rounding errors are not accounted for during the analysis of Fortran programs, the analysis results may be unsound. However, the aforementioned approaches neglect to account for rounding errors during the analysis of Fortran programs.

In this paper, we propose an approach to abstract floatingpoint operations soundly in Fortran programs, which considers rounding errors when analyzing programs. Our approach abstracts floating-point expressions in programs into expressions with interval coefficients under real-number semantics and then linearizes them into expressions with scalar coefficients. This abstraction aims to eliminate rounding errors by floating-point operations during program analysis, which enables analyzers to perform sound analysis under the abstract interpretation framework. We develop a Fortran program analyzer on top of the Inference Kernel for Open Static Analyzers (IKOS [10]) to implement the proposed approach, named F-IKOS. F-IKOS utilizes Flang [5] to translate Fortran programs into LLVM Intermediate Representation (LLVM IR) and then leverages IKOS to analyze the LLVM IR. The core of F-IKOS is IKOS, which is a static analyzer based on abstract interpretation. IKOS can use abstract domains from the Apron [6] numerical abstract domain library to analyze programs. However, it mainly detects runtime errors in machine integer types and cannot infer invariants on floating-point types [1]. In our implementation, we first extended IKOS to support floating-point types, and then applied the proposed approach to handle floating-point operations soundly. With these extensions, F-IKOS can analyze floating-point types in Fortran programs and obtain sound analysis results. We conducted experiments over benchmarks consisting of representative Fortran programs and the evaluation results demonstrate the efficiency, effectiveness, and utility of the analyzer F-IKOS. The main contributions of this work are as follows:

• We proposed an approach to soundly abstract floating-point operations in Fortran programs, accounting for rounding errors during program analy-sis. • We developed F-IKOS, a static analyzer for Fortran programs, to implement the proposed approach. F-IKOS can soundly analyze floating-point types in Fortran programs. • Evaluation shows that F-IKOS can handle the complex syntax of Fortran programs and produce sound analysis results, outperforming other relevant Fortran analyzers.

The rest of the paper is organized as follows. Section 2 describes background. Section 3 presents the overview of our analyzer F-IKOS. Section 4 presents the proposed abstraction of floating-point expressions. Section 5 presents our analyzer implementation together with experimental results. Section 6 discusses some related work and Section 7 concludes.

Background

The Fortran Programming Language

The Fortran programming language is a well-established high-level language with many syntax standards, such as Fortran 77 and Fortran 90. Fortran has similarities to other high-level programming languages. For example, Fortran includes common control structures such as conditional statements and looping control structures. However, Fortran programs often emphasize numerical computation tasks more than logical control functions. This is reflected by the fact that Fortran has a wealth of intrinsic functions, such as the trigonometric functions sin, cos, asin, and acos.

Besides, Fortran has a rich set of convenient array operations. Fortran supports flexible array boundaries, such as 𝑖𝑛𝑡𝑒𝑔𝑒𝑟 ∶∶ 𝑣(−3 ∶ 3), indicating that the index of array 𝑣 ranges from -3 to 3. It also provides a range of intrinsic functions for arrays, including sum and product, as well as matmul and dot_product for computing matrix products and dot products. Fortran inherently supports multidimensional arrays and offers mechanisms for array slicing and reshaping. For instance, the reshape function facilitates altering the number of dimensions and the size of each dimension within an array. Due to these characteristics, Fortran is widely used in scientific and high-performance computing.

The Floating-point Representation

The floating-point representation adheres to the IEEE-754 standard. Many high-precision real numbers, cannot be exactly represented by floating-point numbers. The IEEE-754 standard provides four rounding modes: nearest, zero, −∞, and +∞, to approximate real numbers using floatingpoint numbers. This approximation can introduce rounding errors, which result in inexactness.

Due to rounding errors, mathematical properties followed by real number operations do not hold in floating-point operations. We illustrate it with an example. To distinguish between real and floating-point numbers and their respective operators, we employ 𝑟𝑛𝑑(⋅) to represent floating-point numbers in machines and denote real number operators using symbols +, −, ×, /, while denoting floating-point operators using ⊕ 𝑓 ,𝑟 , ⊖ 𝑓 ,𝑟 , ⊗ 𝑓 ,𝑟 , ⊘ 𝑓 ,𝑟 where the subscripts 𝑓 , 𝑟 denote different precision and rounding modes. Real numbers like 0.1, 0.2, and 0.3 cannot be exactly represented by machines.

Under real number semantics, the equation 0.1 + 0.2 = 0.3 holds. But in machines, 𝑟𝑛𝑑(0.1) ⊕ 𝑓 ,𝑟 𝑟𝑛𝑑(0.2) is not equal to 𝑟𝑛𝑑(0.3). Furthermore, the law of association and distribution is not always true in floating-point operations. E.g., it may happen that (𝑟𝑛𝑑(𝑎)⊕ 𝑓 ,𝑟 𝑟𝑛𝑑(𝑏))⊕ 𝑓 ,𝑟 𝑟𝑛𝑑(𝑐) ≠ 𝑟𝑛𝑑(𝑎)⊕ 𝑓 ,𝑟 (𝑟𝑛𝑑(𝑏)⊕ 𝑓 ,𝑟 𝑟𝑛𝑑(𝑐))

Rounding Model of IEEE-754

A simplified rounding model of the IEEE-754 standard follows the equation below:

𝑟𝑛𝑑(𝑥) = 𝑥 × (1 + 𝑒) + 𝑑

where |𝑒| ≤ 𝜖, |𝑑| ≤ 𝛿, and 𝑒 × 𝑑 = 0. When 𝑥 is a normalized number, it holds that 𝑑 = 0, and when 𝑥 is a denormalized number, it holds that 𝑒 = 0. Here, 𝜖 denotes the maximum relative error for normalized numbers, and 𝛿 describes the maximum absolute error for denormalized numbers for specific precision of floating-point numbers.

Linearization

An interval linear expression is an expression where the coefficients may be intervals instead of scalars. For instance,

𝑧 = [𝑏 1 , 𝑐 1 ]𝑥 + [𝑏 2 , 𝑐 2 ]𝑦

Interval linear expressions, in which the coefficients are intervals, can be abstracted into linear expressions with scalar coefficients. This process is linearization, and it is defined as follows:

Definition 1 (Linearization). An interval linear expression ∑ 𝑖 [𝑎 𝑖 , 𝑏 𝑖 ] × 𝑥 𝑖 + [𝑐, 𝑑] can be linearized into a linear expression ∑ 𝑖 𝑒 𝑖 ×𝑥 𝑖 +[𝑐 ′ , 𝑑 ′ ], where 𝑒 𝑖 ∈ [𝑎 𝑖 , 𝑏 𝑖 ] and satisfying

∑ 𝑖 [𝑎 𝑖 , 𝑏 𝑖 ] × 𝑥 𝑖 + [𝑐, 𝑑] ⊆ ∑ 𝑖 𝑒 𝑖 × 𝑥 𝑖 + [𝑐 ′ , 𝑑 ′ ] for all 𝑥 𝑖 ∈ [𝑥 𝑖 , 𝑥 𝑖 ]

where 𝑥 𝑖 ≤ 𝑥 𝑖 ≤ 𝑥 𝑖 .

Overview

In this section, we give an overview of our approach. We develop a static analyzer on top of IKOS [10], named F-IKOS, to perform sound analysis of floating-point types in Fortran programs. The architecture and workflow of F-IKOS are illustrated in Fig. 1, highlighting our modifications to enable the sound analysis of floating-point types in Fortran programs. Initially, F-IKOS takes Fortran programs as input and uses the parser Flang [5] to translate programs into LLVM IR. Subsequently, after optimization and processing, F-IKOS uses extended IKOS together with numerical abstract domains from Apron [6] to analyze the LLVM IR and obtain invariants of programs. Finally, potential runtime errors in programs are checked by utilizing these invariants.

Approach

Fortran programs involve numerous floating-point operations, and analyzing these programs within the abstract interpretation framework by simply treating floating-point expressions as real-number expressions may result in unsound results. This occurs because floating-point numbers in programs are rounded before being passed to abstract domains (e.g., Apron [6]). For example, within the polyhedra abstract domain, linear constraints between variables are collected is not equivalent to (𝑥 + 𝑦) under real-number semantics.

To address this challenge, Miné [19] proposes to overapproximately abstract floating-point expressions into realnumber expressions. The approach includes the following three steps:

1. Abstract the deterministic semantics of floatingpoint expressions into non-deterministic semantics on real-number expressions. 2. Convert the non-deterministic semantics of real numbers into deterministic semantics for real numbers.

Analyze programs with real-number operations us-

ing abstract domains initially designed for programs with real-number types.

In this section, we present the following three steps: sound abstraction of floating-point expressions, linearization of interval linear expressions, and the analysis of programs using abstract domains.

Abstraction of Floating-point Expressions

Abstraction of floating-point numbers. Floating-point types in Fortran programs adhere to the IEEE-754 standard.

Given the value of a floating-point number and its precision, using the rounding model outlined in Section 2.3, we can compute the relation of 𝑟𝑛𝑑(𝑥) and 𝑥 (the interval range) as follows.

When 𝑥 is a normalized number, the relation of 𝑥 and 𝑟𝑛𝑑(𝑥) can be represented as:

𝑟𝑛𝑑(𝑥) = 𝑥 × [1 − 𝜖, 1 + 𝜖](1)

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 1 illustrates the values of 𝜖 and 𝛿 for various floating-point types. To enhance generality, we express the conversion between a floating-point number and its corresponding real interval range before rounding using Formula 3. This provides an over-approximation of 𝑥 given by Formula 1 and 2 regardless of whether 𝑥 is a normalized or denormalized number.

𝑟𝑛𝑑(𝑥) = 𝑥 × ([1 − 𝜖, 1 + 𝜖]) + [−𝛿, 𝛿](3)

Abstraction of Expressions with Floating-Point Operators. Miné [19] proposes a method for abstracting expressions involving floating-point operators into real-number expressions. This approach captures rounding errors of floating-point arithmetic by over-approximating the behavior of floating-point operators using real-number semantics. Assume that 𝑟𝑛𝑑(𝑥) and 𝑟𝑛𝑑(𝑦) are two floating-point expressions, with 𝑥 and 𝑦 representing the corresponding real-number expressions. Let 𝑎 and 𝑏 be real numbers, and let 𝜖 and 𝛿 denote the relative and absolute errors, respectively, which depend on the precision of the floating-point types.

Non-linear operators (such as ⊗ 𝑓 ,𝑟 and ⊘ 𝑓 ,𝑟 ) can be handled by applying the corresponding operator on intervals after "intervalizing" the arguments [19]. The operator | ⋅ | 𝜄 is used to "intervalize" the argument by a single interval [19]. When multiplying two linear forms that have not been reduced to an interval, the operator | ⋅ |𝜄 can be applied to either argument. Similarly, operator | ⋅ | 𝜄 can be applied to the divisor to obtain a single interval before performing division.

The abstraction is described as follows [19]:

𝑥 ⊕ 𝑓 ,𝑟 𝑦 = (𝑥 + 𝑦) × [1 − 𝜖, 1 + 𝜖] + [−𝛿, 𝛿] 𝑥 ⊖ 𝑓 ,𝑟 𝑦 = (𝑥 − 𝑦) × [1 − 𝜖, 1 + 𝜖] + [−𝛿, 𝛿] 𝑥 ⊗ 𝑓 ,𝑟 [𝑎 0 , 𝑏 0 ] = 𝑥 × [1 − 𝜖, 1 + 𝜖] ⋅ [𝑎 0 , 𝑏 0 ] + [−𝛿, 𝛿] [𝑎 0 , 𝑏 0 ] ⊗ 𝑓 ,𝑟 𝑥 = 𝑥 ⊗ 𝑓 ,𝑟 [𝑎 0 , 𝑏 0 ] 𝑥 ⊗ 𝑓 ,𝑟 𝑦 = 𝑥 × [1 − 𝜖, 1 + 𝜖] ⋅ |𝑦| 𝜄 + [−𝛿, 𝛿] 𝑜𝑟 𝑥 ⊗ 𝑓 ,𝑟 𝑦 = 𝑦 × [1 − 𝜖, 1 + 𝜖] ⋅ |𝑥| 𝜄 + [−𝛿, 𝛿] 𝑥 ⊘ 𝑓 ,𝑟 [𝑎 0 , 𝑏 0 ] = 𝑥 × [1 − 𝜖, 1 + 𝜖]/[𝑎 0 , 𝑏 0 ] + [−𝛿, 𝛿] 𝑥 ⊘ 𝑓 ,𝑟 𝑦 = 𝑥 × [1 − 𝜖, 1 + 𝜖]/|𝑦| 𝜄 + [−𝛿, 𝛿](4)

Abstraction of Floating-point Expressions. In Fortran programs, variables (or constants) and operators in expressions are under floating-point semantics. We abstract expressions that involve floating-point variables and perform floating-point arithmetic into real-number expressions, which involve real-number variables and real-number operators.

The floating-point expression 𝑟𝑛𝑑(𝑥) ⊕ 𝑓 ,𝑟 𝑟𝑛𝑑(𝑦) can be abstracted into a real-number expression as follows:

𝑟𝑛𝑑(𝑥) ⊕ 𝑓 ,𝑟 𝑟𝑛𝑑(𝑦)

where

𝑟𝑛𝑑(𝑥) = 𝑥 × [1 − 𝜖, 1 + 𝜖] + [−𝛿, 𝛿] 𝑟𝑛𝑑(𝑦) = 𝑦 × [1 − 𝜖, 1 + 𝜖] + [−𝛿, 𝛿]

Substituting these into the expression, we get

(𝑥×([1−𝜖, 1+𝜖])+[−𝛿, 𝛿])⊕ 𝑓 ,𝑟 (𝑦 ×([1−𝜖, 1+𝜖])+[−𝛿, 𝛿])(5)

Since 𝑥 ⊕ 𝑓 ,𝑟 𝑦 = 𝑟𝑛𝑑(𝑥 + 𝑦), we convert Formula 5 as:

𝑟𝑛𝑑(((𝑥 + 𝑦)([1 − 𝜖, 1 + 𝜖]) + 2 × [−𝛿, 𝛿]))

Thus, the expression 𝑟𝑛𝑑(𝑥) ⊕ 𝑓 ,𝑟 𝑟𝑛𝑑(𝑦) can be abstracted as:

(𝑥 + 𝑦)[(1 − 𝜖) 2 , (1 + 𝜖) 2 ] + [−(3 + 2𝜖)𝛿, (3 + 2𝜖)𝛿](6)

By following this approach, the expression 𝑟𝑛𝑑(𝑥) ⊖ 𝑓 ,𝑟 𝑟𝑛𝑑(𝑦) can be abstracted into its corresponding real-number expression, as illustrated:

(𝑥 − 𝑦)[(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 converted into 𝑟𝑛𝑑(𝑥) ⊗ 𝑓 ,𝑟 [𝑎, 𝑏](8)

Given that

𝑟𝑛𝑑(𝑥) = 𝑥 × [1 − 𝜖, 1 + 𝜖] + [−𝛿, 𝛿] and 𝑥 ⊗ 𝑓 ,𝑟 [𝑎 0 , 𝑏 0 ] = 𝑟𝑛𝑑(𝑥 × [𝑎 0 , 𝑏 0 ]) = 𝑥 × [1 − 𝜖, 1 + 𝜖] ⋅ [𝑎 0 , 𝑏 0 ] + [−𝛿, 𝛿],

we can express Formula 8 as follows:

𝑟𝑛𝑑 (𝑥 × [1 − 𝜖, 1 + 𝜖] ⋅ [𝑎, 𝑏] + [−𝛿, 𝛿] ⋅ [𝑎, 𝑏])

Thus, the expression 𝑟𝑛𝑑(𝑥) ⊗ 𝑓 ,𝑟 𝑟𝑛𝑑(𝑦) can be abstracted as:

𝑥 ×[(1−𝜖) 2 , (1+𝜖) 2 ]⋅[𝑎, 𝑏]+[−(1+𝜖)𝛿, (1+𝜖)𝛿]⋅[𝑎, 𝑏]+[−𝛿, 𝛿](9)

Similarly, we apply | ⋅ |𝜄 to the divisor to obtain a single interval before performing the division. The floating-point expression 𝑟𝑛𝑑(𝑥) ⊘ 𝑓 ,𝑟 𝑟𝑛𝑑(𝑦) can then be abstracted into its corresponding real-number expression, as illustrated below:

𝑥×[(1−𝜖) 2 , (1+𝜖) 2 ]

/[𝑎, 𝑏]+[−(1+𝜖)𝛿, (1+𝜖)𝛿]/[𝑎, 𝑏]+[−𝛿, 𝛿]

(10) The coefficients of variables within the real-number expressions obtained by abstraction are represented as realnumber intervals. However, many abstract domains cannot process such interval-coefficient forms, as they only support linear expressions.

Linearization of Interval Linear Expressions

To enable existing numerical abstract domains (e.g., polyhedra abstract domain) to handle interval linear expressions, Miné [19] proposes to linearize these interval linear expressions to linear expressions. We provide the proof of the soundness of the linearization operator through the following reasoning:

∑ 𝑖 [𝑎 𝑖 , 𝑏 𝑖 ] × 𝑥 𝑖 + [𝑐, 𝑑] ⟺ ∑ 𝑖 (𝑒 𝑖 + [𝑎 𝑖 − 𝑒 𝑖 , 𝑏 𝑖 − 𝑒 𝑖 ]) × 𝑥 𝑖 + [𝑐, 𝑑] ⟺ ∑ 𝑖 𝑒 𝑖 × 𝑥 𝑖 + ∑ 𝑖 [𝑎 𝑖 − 𝑒 𝑖 , 𝑏 𝑖 − 𝑒 𝑖 ] × 𝑥 𝑖 + [𝑐, 𝑑]

can be over-approximated as

∑ 𝑖 𝑒 𝑖 × 𝑥 𝑖 + ([𝑎 𝑖 − 𝑒 𝑖 , 𝑏 𝑖 − 𝑒 𝑖 ] × [𝑥 𝑖 , 𝑥 𝑖 ]) + [𝑐, 𝑑] since it holds that [𝑎 𝑖 − 𝑒 𝑖 , 𝑏 𝑖 − 𝑒 𝑖 ] × 𝑥 𝑖 ⊆ [𝑎 𝑖 − 𝑒 𝑖 , 𝑏 𝑖 − 𝑒 𝑖 ] × [𝑥 𝑖 , 𝑥 𝑖 ],

where 𝑎 𝑖 ≤ 𝑒 𝑖 ≤ 𝑏 𝑖 and 𝑥 𝑖 ≤ 𝑥 𝑖 ≤ 𝑥 𝑖 .

Note that following the same principle, an interval linear inequality ∑ 𝑖 [𝑎 𝑖 , 𝑏 𝑖 ]×𝑥 𝑖 +[𝑐, 𝑑] ≤ 0 can be also linearized into a linear inequality in the form of ∑ 𝑖 𝑒 𝑖 ×𝑥 𝑖 +[𝑐 ′ , 𝑑 ′ ] ≤ 0 in the sense of weak solution [23]. It means that a weak solution of an interval linear inequality ∑ 𝑖 [𝑎 𝑖 , 𝑏 𝑖 ] × 𝑥 𝑖 + [𝑐, 𝑑] ≤ 0 will be a solution of ∑ 𝑖 𝑒 𝑖 × 𝑥 𝑖 + [𝑐 ′ , 𝑑 ′ ] ≤ 0 (but the reverse does not hold). This approach over-approximates interval linear expressions (or inequalities) up into linear expressions (or inequalities).

Analyze programs with existing abstract domains

Due to the sound handling of rounding errors inherent in floating-point operations through the above abstraction and linearization procedure, we can now obtain sound results using abstract domains initially designed for real-number semantics.

Implementation and Evaluation

Implementation

We have implemented a static analyzer for Fortran programs, named F-IKOS, with over 4K LOC of C++ code by extending IKOS. F-IKOS is endowed with the capability to perform sound analysis of floating-point types in Fortran programs.

Research Questions and Experimental Setup

To evaluate F-IKOS, we compare it with two most relevant Fortran program analyzers, SMACK [7] and CIVL [8]. Both SMACK and CIVL translate Fortran programs into IR for subsequent verification using IR-compatible verifiers, mainly based on model checking. They are designed to verify certain program properties but do not directly detect potential errors in Fortran programs. We investigate the following three research questions across the analyzers:

• RQ1: How effective is F-IKOS in analyzing simple Fortran programs? • RQ2: How well does F-IKOS handle complex features of Fortran programs? • RQ3: How does F-IKOS perform when applied to real-world Fortran programs?

To address these questions, we conducted three experiments to evaluate the capabilities of F-IKOS. The benchmarks employed in our experiments are categorized into three distinct classes:

• 36 Fortran programs used by SMACK [7] and CIVL [8],

which are used to evaluate F-IKOS's ability to handle simple syntaxs and accomplish verification tasks. • 45 real-world Fortran programs extracted from opensource repositories [22,21], encompassing various Fortran syntax standards. • 10 artificially constructed programs, derived from the repository [20], designed to evaluate the capability of F-IKOS in detecting runtime errors associated with floating-point types.

All experiments were conducted on a PC running Ubuntu 20.04 (16GB Memory) in the Oracle VirtualBox 6.1.30 with a 3.3GHz Intel Core i9 CPU. The abstract domain used is Polka [6], which is an implementation of the Polyhedra abstract domain in Apron.

RQ1: Verifying simple Fortran programs

We analyzed 36 simple Fortran programs from the first benchmark [7,8], excluding parallel and recursive program instances. The experimental results are presented in Table 2, where "F-IKOS Time (s)", "SMACK Time(s)" and "CIVL Time (s)" denote the execution time of F-IKOS, SMACK, and CIVL, respectively. In the last row of Table 2, the average execution time of programs is recorded. Specifically, SMACK successfully verified only 19 out of 36 programs. In contrast, CIVL correctly verified all 36 programs, 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 invariants for successful verification, are out of the expressiveness of the used polyhedra abstract domain, whereas CIVL, with the help of the SMT solver (i.e., Z3), can address them effectively.

Furthermore, a comparative analysis of the average execution time reveals that F-IKOS exhibits shorter analysis time, approximately 5% of SMACK's and 10% of CIVL's. The experimental results underscore F-IKOS's ability to achieve a delicate balance between analysis efficiency and effectiveness, demonstrating its strengths compared to existing state-of-the-art Fortran analyzers.

RQ-1 Answer: F-IKOS undergoes comparison with SMACK and CIVL for the analysis of 36 Fortran programs. It successfully verified 30 out of 36 programs, exhibiting a shorter average execution time compared with state-of-theart approach and about 10% of CIVL's. The results highlight the efficiency and effectiveness of F-IKOS in analyzing simple Fortran programs.

RQ2: Handling complex feature operations

We analyzed 45 Fortran programs from the second benchmark. The programs in this benchmark utilize features and intrinsic functions in Fortran that have not been previously examined. Some programs exemplify common Fortran programming conventions, while others involve algorithmic implementations. The inclusion of integer and floatingpoint types, along with arrays, increases the complexity of analyzing the programs.

In addition to the Fortran 90 standard programs, some programs following Fortran 77, and Fortran 95 standards are also included in bold in the table. The evaluation results in the efficiency and effectiveness of the analyzers are shown in Table 3. "F-IKOS (s)" and "F-IKOS FP" illustrate the Execution Time and False Positives (FP) of F-IKOS, respectively.

The experimental results demonstrate that both SMACK and CIVL to analyze the 45 programs in benchmark and find that SMACK can parse 37 out of 45 programs, whereas CIVL can only parse 3 out of 45. In contrast, F-IKOS can analyze all programs within an average time of 1.79s while maintaining an acceptable average of 3 false positives per program. In particular, when analyzing programs that use intrinsic functions to manipulate Fortran's arrays, F-IKOS issues some false positives. The reason for these false positives lies in the differences between Fortran arrays and common high-level language arrays. RQ-2 Answer: F-IKOS maintains analytical capabilities when dealing with intrinsic functions. F-IKOS successfully analyzed all Fortran programs within an average time of

RQ3: Handling real-world programs

We evaluated the capability of F-IKOS to detect runtime errors in larger programs from the third benchmark. To objectively demonstrate F-IKOS's capabilities, we intentionally injected 10 division-by-zero bugs into some of these programs. Our evaluation metrics include both analysis time and accuracy. The accuracy of the analysis is defined as follows: 𝐴𝑐𝑐𝑢𝑟𝑎𝑐𝑦 = 𝑇 𝑃 𝑇 𝑃 + 𝐹 𝑃 where 𝑇 𝑃 represents the number of true positives, and 𝐹 𝑃 denotes the number of false positives.

The experimental results are represented in Table 4, where "F-IKOS TP" and "F-IKOS FP" denote true positives and false positives of F-IKOS, respectively. SMACK successfully 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 an accuracy of 22.2%. The programs include both custom and Fortran intrinsic functions, exhibiting more complex numerical characteristics. The results demonstrate the effectiveness of F-IKOS to detect runtime errors in numerical computation programs. Regardless of the rounding mode used by machines, our analysis of Fortran programs remains sound, ensuring consistent and sound analysis results across different computational environments.

We find that some programs require more time for analysis. Two primary factors contribute to the long execution time. Firstly, our experiments utilize the polyhedra abstract domain, which can be computationally expensive for certain programs. Additionally, real-world programs often exhibit distinct numerical characteristics, particularly due to the presence of loops and arrays, which demand more timeintensive processing.

RQ-3 Answer:

The results show that SMACK parses 7 out of 10 Fortran programs, while CIVL fails to parse any. Moreover, neither tools can detect runtime errors in the programs they parse. In contrast, F-IKOS soundly analyzes all programs and successfully detects runtime errors, demonstrating its effectiveness in handling Fortran numerical programs.

Related Work

In the literature, there exists several tools to analyze or verify Fortran programs. Some tools such as f2c [3] and FABLE [11] [13], ftnchek [12] and Coverity [14] specializes in predefined, general-purpose defect detection within Fortran programs, lacking the comprehensive capability to analyze program properties semantically. In contrast, CamFort [15] incorporates a lightweight declarative specification language capable of both checking and inferring specifications. SMACK [7] and CIVL [8] translate Fortran programs into Intermediate Representation (IR) for subsequent verification using IR-compatible verifiers. Specifically, SMACK converts Fortran programs to LLVM IR and then verifies LLVM IR via Corral [9], wherein Corral restricts the syntax of expressions in this language to one that can be efficiently decided by a SMT solver. CIVL [8] converts Fortran programs to CIVL-C which is an Intermediate Verification Language (IVL), which is subsequently verified using model checking and symbolic execution. However, their work mainly focuses on the verification of Fortran programs, without addressing runtime error detection. In this paper, we use F-IKOS to support the sound analysis of Fortran programs with complex features.

Conclusion

In this paper, we present F-IKOS, an abstract interpretationbased static analyzer designed for Fortran programs. Particularly, F-IKOS provides a sound analysis for floating-point types in programs. F-IKOS first abstracts floating-point expressions into real-number expressions with interval coefficients, then linearizes 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. Evaluation of three benchmarks demonstrates F-IKOS's efficiency and effectiveness than other relevant analyzers in the analysis of Fortran programs.

ID