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 f loating-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
I don’t know how to obtain F-IKOS, but it is an offshoot of
They tested their tool on the FortranTip codes (among other codes).
The readme of the repo now has an example of the floating point analysis f-ikos can do. Given the code
real function cap(x)
implicit none
real, intent(in) :: x
real :: y
y = x
! Cap the value of y based on certain conditions
if (10.0 > y) then
y = 10.0
else if (15.0 < y) then
y = 20.0
else
y = y / (y - x)
end if
cap = y
end function cap
it says
# Summary:
Total number of checks : 18
Total number of unreachable checks : 0
Total number of safe checks : 17
Total number of definite unsafe checks: 1
Total number of warnings : 0
The program is definitely UNSAFE
# Results
cap.f90: In function 'cap_':
cap.f90:12:1: error: division by zero
y = y / (y - x)
^
Just out of curiosity, what is the report if you change “y = x” to “y = x + 0.1”? (I assume you can run the program - the prerequisites looked rather daunting, but I merely glanced at the list )
And what happens if you do: y = x + 1.0e-10?
It does look interesting …
Thanks for your answer. I will have to get a closer look at the results :). However, the article that describes F-IKOS gave rise to a few questions as well:
While complex numbers are - from a porgramming point of view - “just” combinations of two real numbers, the article does not mention them at all. Does F-IKOS handle these?
On page 31 I found the statement “The reason for these false positives lies in the differences between Fortran arrays and common high-level language arrays.” Could you explain that in some detail? Besides syntax (which should be solved prior to F-IKOS’s analysis) and the flexibility in indices I cannot think of any difference that comes into play.
In the past I have come across interval arithmetic as a means to analyse the accuracy of program results. One drawback was that these intervals would grow and grow during the course of the calculation and ultimately would lead to so large intervals that the result was meaningless. I guess that is different for static analyses?
Have you tried F-IKOS on such commonly used packages like BLAS and LAPACK and others/
(among other codes).