CIVL: Fortran Front End Overview

1. Goals

FortranFrontEnd is a CIVL component generating CIVL abstract syntax trees (CIVL IR) from given FORTRAN source files so that CIVL can verify desired correctness properties for FORTRAN programs based on their CIVL IR.

Considering that:

1). most concurrent APIs (e.g., MPI, OpenMP, etc.) support bindings of both C and FORTRAN;

2). FORTRAN source code are commonly pre-processed by a general preprocessor;

3). CIVL is originally designed and developed for verifying C programs;

FORTRAN source files will be firstly pre-processed by CIVL's general preprocessor; and then a preprocessed token stream will be converted to a FORTRAN token stream; an ANTLR generated parser will process it based on FORTRAN 2018 standard; finally, the parse tree will be transformed to CIVL IR.

1.1. Base

Accomplished

• Support pre-processing FORTRAN source with a general pre-processor ​directives;

In-progress

• Support parsing ​a frequently used FORTRAN subset (of FORTRAN 2018 standard);
• Support interpreting ​supported FORTRAN behaviors in the form of CIVL IR;
• Support parsing ​a frequently used OpenMP subset (of OpenMP FORTRAN bindings);
• Support interpreting ​supported OpenMP behaviors defined and used for FORTRAN bindings in the form of CIVL IR;

TODO list

• Support OpenMP SIMD directives;
• Support CIVL primitives in FORTRAN code;

1.2. RAPIDS

In-progress

• Support verifying the functional equivalence for FLASH5 project (between the original version and optimized transformation);

2. Design

2.1. A general preprocessor

• Input: A set of FORTRAN source files
• Output: A set of preprocessor (PP) token streams.
• Functionality:
  • Macro operations
  • Conditional compilation
  • File inclusion

2.2. A PP-to-FORTRAN convertor

• Input: A PP-token stream
• Output: A FORTRAN token stream
• Functionality:
  • Token conversion (from PP-token vocabulary to FORTRAN token one)
  • Comments/whitespaces/newline filtration
  • INCLUDE statement replacement
  • Keyword identification (a lexical pre-pass procedure)

2.3. An ANTLR generated parser

• Input: A FORTRAN token stream
• Output: A FORTRAN parse tree
• Functionality:
  • Parse tree generation
  • Syntax error report.

2.4. A parse tree trasformer

• Input: A FORTRAN parse tree
• Output: A CIVL IR interpreting the semantics of given FORTRAN source files.
• Functionality:
  • Abstract syntax tree transformation (from a parse tree to CIVL IR)
  • Variable/expression type analysis required for the transformation

Appendix A. FORTRAN 2018 parse rules

A.1. Supported

A.2. Developing

A.3. Scheduled

A.4. Excluded

Appendix B. OpenMP directives

B.1. Supported

B.2. Developing

B.3. Scheduled

B.4. Excluded