Is there a tool like FRAMA_C for Fortran?

1

The cover article in August 2021 Communications of the ACM is entitled The Dogged Pursuit of Bug-free C Programs.

It describes an ambitious and comprehensive tool to verify the correctness of C programs. In addition to analyzing the code, it uses annotations in ACSL (ANSI C Specification Language) to express pre-conditions, post-conditions, loop invariants, etc.

The article remarks that there is ongoing work to extend the project to C++ and Rust.

The much more rigid semantics of Fortran pointers compared to C pointers of C++ references suggest that many of the analyses would be simpler for Fortran than for C or C++.

Is there a tool like FRAMA-C for Fortran? Is there a project underway to add Fortran support to FRAMA-C?

2 Likes
2

There are several possibilities, I guess, but I had not heard of FRAMA_C myself. A good tool to get at least code checking beyond what compilers normally do is fpt from Simcon - WinFPT and ftp - Fortran Engineering - Summary.

The title of the article indicates far-stretching ambition. How do you make sure a program does not contain bugs? You would have to specify exactly what it is supposed to do. I guess what is meant is no bugs like accessing array elements outside the proper range or division by zero and the like.

3

No Frama-C tool for Fortran at the moment. But after looking at the program derivation literature, modern Fortran would make a very good language to incorporate into a computational approach to mathematics education and formal methods.

I pretty much agree with Matthias Felleisen (author of Racket, a Scheme derived programming language) and have been looking at how his materials might be adapted to incorporating Fortran into high school and undergraduate mathematics.

Matthias Felleisen, Shriram Krishnamurthi Why Computer Science Doesn’t Matter
Communications of the ACM, Vol. 52 No. 7, Pages 37-40
10.1145/1538788.1538803

Blockquote
Any attempt to align programming with mathematics will fail unless the programming language is as close to school mathematics as possible. The goal of an alignment is to transfer skills from programming to mathematics and vice versa.

4

Les Hatton wrote about safer subsets of C and Fortran, including a 1992 paper

Fortran, C or C++ for geophysical software development?
Abstract
Historically, Fortran has been used for most of the major software
development in the geophysical environment since the emergence of digital
seismic data processing. Today, largely as a result of an extraordinarily
protracted attempt to modernise the language, its position is challenged by
a number of competing languages. These include C, recently standardised
by the I.S.O., and C++ now being standardised by the A.N.S.I. committee
X3J16. Given that standardisation is one of the most important forces in
modern computing as exemplified by the emergence of P.O.S.C. in the
petroleum exploration industry, a discussion of this much aired question
seemed timely. This paper discusses the advantages and disadvantages of
these languages with particular emphasis on the reliability of the software
produced using them and the notion of the “safe subset”. The paper
concludes by defining a safe(r) subset of the Fortran 77 language. It is
intended that further safe(r) subsets be defined in future papers. Note that
the use of the parenthesised (r) in safe is deliberate. There is no truly safe
subset of a high-level language as errors occur in compilers and chip
firmware also but use of so-called safe features greatly improves the overall
reliability and reduces the maintenance costs.

His paper covered Fortran 77, and his site lists some feedback from standards committee member @vsnyder. The numbers refer to a list from the paper starting on page 12.

All my work was done for Fortran 77. Significant things have happened to Fortran since 1990. Van Snyder (21-Jun-2001, 7-Mar-2005) contributed this important feedback with respect to Fortran 90, 95 and 2003:-

ASSIGN, assigned GO TO and assigned format are deleted from Fortran 95. (1.40) Non-integer DO variables are deleted from Fortran 95. (1.26) The PAUSE statement is deleted from Fortran 95. (1.36) The H edit descriptor is deleted from Fortran 95. (1.6)

Most compilers have options to announce unreachable code, unreferenced labels, declared but not used variables, and referenced but not defined variables. Encourage use of those options. Encourage use of tools that detect such things in case ones compiler doesn’t.

Recommend in (1.6) to use character variables instead.

Most of the problems you mention with respect to calling sequences (e.g.1.10,1.22, 2.10) are solved by using explicit interfaces (introduced in Fortran 90). Module procedures (introduced in Fortran 90) always have explicit interface. Their use should be preferred to external procedures. Where external procedures are used, it is good practice to specify an explicit interface instead of using an EXTERNAL statement or (worse yet) no declaration at all. This is not, however, always possible. A particularly difficult case is in interfacing to C functions that expect a “void*” argument, and deduce the type of it from the run-time (!) values of other arguments. I hope you caution against doing such things in your “Safer C” book. [Ed … I didn’t cover cross-language calling because it is usually implementation-defined at best and usually fraught with danger.]

Instead of simply recommending not to use REAL R(1) (1.13), point out that a last-dimension specification of “*” for dummy arguments is provided in Fortran 77, with the meaning of “unspecified upper bound.” Suggest using assumed shape (bounds given by colons), with the warning that this may sometimes cause copy-in / copy-out argument passing.

In addition to (1.16) recommend always using IMPLICIT NONE, which is standard in Fortran 90. Delete the reference to it being nonstandard in (1.17). Recommend its use instead of IMPLICIT UNDEFINED because the latter is not standard.

Recommend in (1.24) that module variables (introduced in Fortran 90) should be used instead of COMMON.

Recommend use if IACHAR and ACHAR instead of ICHAR and CHAR in (1.39).

Some compilers now offer detection of access to undefined variables, pointers with undefined association status, or pointers with defined association status but that are not associated. Most offer bounds checking for arrays. Recommend the use of these options, at least during development (1.50)

Free-form source prohibits embedding blanks or continuations within identifiers (1.52). Recommend use of free-form source generally.

Fortran 95 specifies that DATA or initialization within a type declaration implies SAVE. There are cases where using DATA is appropriate (2.2); its use should be cautioned rather than prohibited, and the implication of SAVE should be mentioned alongside the caution (i.e., the initialization happens once, not every time the scoping unit is invoked). One example is for a “first time” flag, that indicates certain calculations for which the results are deposited into SAVE variables, e.g. involving the precision of arithmetic, need not be repeated. For objects that have immutable values that the processor can compute, recommend the PARAMETER (named constant) attribute. Fortran 90 allows specification of dummy argument usage intent, in the case that a procedure has an explicit interface. There is not a problem of using a DO index as an actual argument if the corresponding dummy argument has INTENT(IN) (2.3). BTW, your (2.3) should caution against DO loop variables being used as ACTUAL arguments (for which the corresponding dummy arguments do not have INTENT(IN)). There is no problem using a DUMMY argument for a DO index, provided it does not have INTENT(IN).

As for new features of Fortran 90, suggest that ALLOCATABLE be preferred to POINTER. There were some deficiencies of ALLOCATABLE in Fortran 90 and Fortran 95, that lead one to need to use POINTER, but these were remedied by Technical Report 15581, which has been included in Fortran 2003. Point out that TRANSFER may have unexpected performance problems. The interaction of FORALL and WHERE may be difficult to understand; caution against using them together.

Recommend using the new execution constructs of Fortran 90 (SELECT CASE, DO and DO WHILE).

1 Like
5

I want to have a mode in LFortran that ensures your code is “safe”:

By a combination of compile time and runtime checking. See the issue for a preliminary list of things to check. We can add more. It would become more like Python, where you get a nice exception and a stacktrace if something goes wrong.

The disadvantage of runtime checks is that even if you get a nice stacktrace and an error message showing where the error is, that might be too late. It would be interesting to see if we can move as many checks from runtime to compile time. It’s a project that I would very much like to pursue. I expect not every bug can be caught at compile time, as even Rust gives a runtime error if you go out of bounds (by reading and index from an input file and then accessing an array at that index).

1 Like
6

“The disadvantage of runtime checks is that it … might be too late.”

One significant “too late” problem is that the supplier no longer exists, or refuses to help you, and you don’t have source code.

The “too late” problem is precisely the reason that I proposed a units system for Ada in 1976, and have been proposing a units system for Fortran pretty much continuously for almost twenty years.

(and units checking at runtime is expensive).

1 Like
7

Brad (@everythingfunctional) and I are working on an article about it. Unit checking is definitely A Good Thing but it is Not Simple, unfortunately.

1 Like
8

The link lists these errors:

  • Array bounds checking (#367)
  • Accessing unallocated variable (#370)
  • Dangling pointers checks (#366)
  • Infinite recursion checks (#368)
  • Numerical errors / exceptions checks (#371)
  • Out of memory (#372)

Some other run-time errors that I often encounter are

  • Accessing an OPTIONAL argument that is not PRESENT
  • Opening a file for reading that does not exist
  • Reading a variable from a line of a file that has data of the wrong type
  • Reading N elements of an array from a character string that contains fewer than N values
  • An invalid format string (for example with missing parenthesis) or a format string that does not match the data read or written. When the data consists of scalars, maybe the compatibility of the data and format string can be checked at compile time.
  • Allocating an array that is already allocated, or deallocating an array that is not allocated

Gfortran, g95, and Intel Fortran do give me informative messages at run-time for these bugs.

1 Like
9

Thanks! I added those to the list at Safe mode (#369) · Issues · lfortran / lfortran · GitLab.

10

I am interested in prototyping this feature in LFortran. Let me know if you want to collaborate.

11

Can people who have used coarrays and the object-oriented features of Fortran 2003+ list the types of run-time errors that can arise?

12

“Brad (@everythingfunctional) and I are working on an article about it. Unit checking is definitely A Good Thing but it is Not Simple, unfortunately.”

Have you read my proposal from 7 July 2016?
http://vandyke.mynetgear.com/Fortran/Units-TR-19.pdf

13

“The link lists these errors… Some other run-time errors that I often encounter are…”

Have you read my paper on exceptions?
http://vandyke.mynetgear.com/Fortran/Exceptions_3.pdf
An earlier version appeared as a J3 or WG5 proposal, but I don’t remember the number.

14

Yes. It is one of a few different techniques for units handling that we are exploring. Each has their pros and cons. You can keep up with our progress on the paper so far and feel free to make suggestions here.

1 Like
15

If you would be interested in prototyping this in a compiler, please let me know. I am available to help.

16

This will certainly be of help, but like @everythingfunctional said, we are exploring a number of techniques. Having a platform to try things out is definitely worthwhile.

@vsnyder, if you would like to participate, please do.

17

@vsnyder, I have read (most of) the TR on units of measurement over te weekend and I have a number of questions regarding the proposal. I will first formulate them in a comprehensible way, rather than the scribbles on the print-out that I have now. It is definitely the most comprehensive solution among the many that circulate (for various programming languages).

18

@vsnyder (cc @everythingfunctional), I have written down my questions. I think I understand the specifications in document N2113, so I hope these questions to be to the point ;).

Questions and remarks regarding document N2113:

(Quite possibly I have overlooked one or more or even all things in the
text and are all the answers to my questions already there)

Just a few nitpicks:

  • The units kelvin and ampère should be written with lower-case.
    (page V for instance)

  • Unit names are part of the same namespace as variables and functions,
    right?

  • Can the names of units be imported via the “import” statement?

  • Use of the unit coercion function is clear, but how does one use the
    confirmation function?

Semantic/syntactic questions:

Ad 5.5
Suppose I have a function like this:

function fpoly( a, x )
    real, dimension(:), intent(in) :: a
    real, intent(in)               :: x
    real                           :: fpoly

    integer                        :: i

    fpoly = a(1)
    do i = 2,size(a)
        fpoly = fpoly + a(i) * x**(i-1)
    enddo
end function

How would I make sure that the units of the arguments are used
correctly? This solution seems a poor workaround:

! f_unit is the unit for the function result
real, unit(f_unit) :: f

f = f_unit( fpoly( unitless(a), unitless(x) ) )

Ad 5.5
Just a thought:

real, unit(length) :: x
real, unit_of(x)   :: y

in a similar vein as the length of character strings or kinds etc.

Another example (finite differences):

subroutine diffxy( p, dx, dy, dpdx, dpdy )
    real, dimension(:,:), unit(p_unit) :: p
    unit                               :: pdiff_unit = p_unit / length
    real, unit(length)                 :: dx
    real, unit_of(dy)                  :: dy  ! Both dx and dy should be expressed
                                              ! in the same unit, meter or foot, so
                                              ! not just a "length unit"
    real, unit(pdiff_unit)             :: dpdx, dpdy

end subroutine diffxy

Ad 5.5
I suspect that pointers to targets that have a unit should have the very
same unit (or equivalent). What about unlmited polymorphic variables?

Should the “select type” construct be extended to include units? (Useful
in combination with abstract units?)

Ad 5.10.2/5.10.3
Ignoring the case (lower/upper case) with input seems problematic to me:
consider milligrams (mm) and megagrams (Mg) or specific heat capacity -
J/kg/K could also be J/K/g or J/Kg (perhaps contrived, but still)

How does one define the strings to represent the units?

Arrays: What would happen if the first element has one unit (cm, say)
and the last has another unit (inch, say)? Automatic onversion? What
would be the end result?

Ad 5.11.3
Are conversions between units automatic? The notes seem to imply that
they are not automatic, but that it is a distinct possibility. However,
is it possible to unambiguously determine the resulting unit? For
instance:

real, unit(cm) :: one_cm   = cm(1.0)
real, unit(cm) :: one_inch = inch(1.0)
write(*,*) add( one_cm, one_inch )

What would be the result (expressed in what unit)? The one that is not a
conversion unit?

Is an expression like “x = one_cm + one_inch” allowed?