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 lfoating-point types in programs, we first abstract floating-point expressions into real-number expressions with interval coeficients, and then linearize these expressions into real-number expressions with scalar coeficients. 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 eficiency and efectiveness of soundly analyzes runtime errors in complex programs, outperforming other analyzers.
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[
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 eforts
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 [
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 diferential equations. Every floating-point type
QuASoQ 2024: 12th International Workshop on Quantitative Approaches
for Open Static Analyzers (IKOS [
types, and then applied the proposed approach to handle lfoating-point operations soundly. With these extensions, FIKOS 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 eficiency, efectiveness, and utility of the analyzer F-IKOS. The main contributions of this work are as follows: • We proposed an approach to soundly abstract lfoating-point operations in Fortran programs, accounting for rounding errors during program analyCEUR Workshop
ceur-ws.org ISSN1613-0073 sis. • We developed F-IKOS, a static analyzer for Fortran programs, to implement the proposed approach. FIKOS 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.
2.1. 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 ofers 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. 2.2. 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 IEEE754 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 diferent 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 ( ()⊕ , ())⊕ , () ≠ ()⊕ , ( ()⊕ , ()) 2.3. 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.
An interval linear expression is an expression where the coeficients may be intervals instead of scalars. For instance, = [ 1, 1] + [ 2, 2]
Interval linear expressions, in which the coeficients are intervals, can be abstracted into linear expressions with scalar coeficients. 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 ≤ ≤ .
In this section, we give an overview of our approach. We
develop a static analyzer on top of IKOS [
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 [
Flang
Representation LLVM Immediate LLVM2AR Representation (AR) Floatingpoint Type
Sound of Floating
point Linearization
IKOS Library (LLVM IR)
Front-end Fixed Point Iterators . .
. Domains
Uses
Analyzer:
IKOS
Analysis result Apron Numerical
Library ⊖ , , ⊗ , , ⊘ , ), these expressions are under floating-point semantics. Directly interpreting floating-point expressions as expressions under real-number semantics introduces unsoundness to the analysis. For instance, (rnd() ⊕ , rnd( )) is not equivalent to ( + )
under real-number semantics.
To address this challenge, Miné [
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. 4.1. Abstraction of Floating-point
can be represented as: follows. () 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 When is a normalized number, the relation of and () = × [1 − , 1 + ]
() = + [− , ]
When is a denormalized number (i.e., close to zero), the relation of and ()
is given by: where denotes the maximum relative error for normalized numbers, and represents the maximum absolute error for (1) (2)
Precision single (32 bits) double (64 bits) quad (128 bits)
2−23 2−52 2−112 2−149 2−1074 2−16494 2 regardless of whether is a normalized or denormalized number.
() = × ([1 − , 1 + ]) + [− , ]
(3)
ators. Miné [
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 [
The abstraction is described as follows [
, ( ) () = × [1 − , 1 + ] + [− , ] ( ) = × [1 − , 1 + ] + [− , ] ators. where 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 operabstracted into a real-number expression as follows: The floating-point expression () ⊕ , ( ) can be Substituting these into the expression, we get ( ×([1−, 1+])+[− , ])⊕
, ( ×([1−, 1+])+[− , ]) Since ⊕ , = ( + ), we convert Formula 5 as: ((( + )([1 − , 1 + ]) + 2 × [− , ])) as:
, ( ) can be abstracted ( + )[(1 − )
2, (1 + ) 2] + [−(3 + 2) , (3 + 2) ]
By following this approach, the floating-point expression () ⊖
, ( ) real-number expression, as illustrated:
can be abstracted into its corresponding ( − )[(1 − )
2, (1 + ) 2] + [−(3 + 2) , (3 + 2) ]
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 + ] + [− , ] () ⊗ , ( ) can be converted into () ⊗
, [, ]
Given that () = × [1 − , 1 + ] + [− , ] [ 0, 0] = ( × [
0, 0]) = × [1 − , 1 + ] ⋅ [ we can express Formula 8 as follows: , ( ) , then
(8) and ⊗ , 0, 0] + [− , ] , ( × [1 − , 1 + ] ⋅ [, ] + [− , ] ⋅ [, ] ) as: Thus, the expression () ⊗ , ( ) can be abstracted ×[(1−) 2, (1+) 2]⋅[, ]+[−(1+) , (1+) ]⋅[, ]+[− , ] (4) (5) (6) (7) (9)
inequalities).
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+) ]/[, ]+[− , ]
The coeficients of variables within the real-number expressions obtained by abstraction are represented as realnumber intervals. However, many abstract domains cannot process such interval-coeficient forms, as they only support linear expressions. (10) 4.2. Linearization of Interval Linear
To enable existing numerical abstract domains (e.g.,
polyhedra abstract domain) to handle interval linear
expressions, Miné [
Drawing inspiration from [
Definition 2 (Linearization Operator).
Given an interval linear expression ∶ ( ∑ [ , ] × + [, ]) , and letting x ∶= [ , ] be the bounding box of variable x, the linearization operator is defined as (,
x) =
∑ × + [ ′, ′] interval = ( + ) × 0.5.
where is any real number in the interval [ , ], and [ ′, ′] denotes the resulting interval of ∑ [ − , − ] × [ , ] + [, ] . Generally, we choose the midpoint of the
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
a linear inequality in the form of ∑
inequality ∑ [ , ]× +[, ] ≤ 0 can be also linearized into
× + [ ′, ′] ≤ 0 in the
sense of weak solution [
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. 5.2. Research Questions and Experimental
Setup
To evaluate F-IKOS, we compare it with two most relevant
Fortran program analyzers, SMACK [
We investigate the following three research questions across the analyzers: • RQ1: How efective 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 [
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 [
programs
We analyzed 36 simple Fortran programs from the first
benchmark [
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 efectively.
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 eficiency and efectiveness, 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 eficiency and efectiveness of F-IKOS in analyzing simple Fortran programs. 5.4. 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 eficiency and efectiveness 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 ifnd 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 diferences 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 1.79s. Moreover, F-IKOS can be used to analyze Fortran programs adhering to multiple syntax standards, and the results show that F-IKOS performs better than SMACK and
Program Name
array arrary_fail compound compound_fail compound_fail_2
compute compute_fail
forloop forloop_fail
function function_fail function_fail_2 function_fail_3
hello hello_fail
inout inout_fail pointer pointer_fail
abs abs_bad array_section array_section_bad intent_inout intent_out intent_out_bad
mod_impl mod_impl_bad mod_spec mult_impl mult_impl_bad mult_spec short_circuit short_circuit_bad
truncate truncate_bad Average 5.5. 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 diferent 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 efectiveness in handling Fortran numerical programs.
In the literature, there exists several tools to analyze or
verify Fortran programs. Some tools such as f2c [
Program arguments associate_bounds bounds
boz case_insensitivity column_major compare_floats
data derived_type_composition derived_type_implied_do dimension direct_access do_loop_index do_while error_stop get_command implicit_save
intrinsic list_directed_read
loop loop_bound loop_index loop_label merge module module_parameter
open_file overlapping_arg print_implied_do_loop protected recursive_io
scratch select_case
slash sum_exit
trim type_constructor_optional
value
write_char
xrandom_int
swap_arrays
average
submod
linear_equations
temp_converter
verifiers to conduct verification. Alternatively,
FORTRANlint [
SMACK [
SMACK (s) 2.43 2.71 3.24 2.85 2.43 2.9 3.25 2.91 2.73 3.34 2.67
3.14 3.27
3.27 3.17 2.93 3.23 2.91 3.28 3.05 3.64 3.26 2.7 2.62 2.98 2.84 4.27 2.87
3.47 3.56 2.9 3.11 2.63 2.75 2.73 2.67 2.19
CIVL (s) 0.99 1.59 1.52 addressing runtime error detection. In this paper, we use F-IKOS to support the sound analysis of Fortran programs with complex features.
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 coeficients, then linearizes these expressions into real-number expressions with scalar coeficients. 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 eficiency and efectiveness than other relevant analyzers in the analysis of Fortran programs.
Program Name converter bubblesort libconstants
simpson diferentiation div expr function palindrome trapezodial 8. Acknowledgments We thank the reviewers for their constructive feedback. This work is supported by the National Key R&D Program of China (No.2022YFA1005101) and the National Natural Science Foundation of China (Nos.62032024,62102432).