CIVL: Fortran Front End Overview

Back:DeveloperPage

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

Completed

• 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

Goal	Status
Phase. 1
1.1 Basic OpenMP directives	Completed
1.2 Basic CIVL primitives	TODO
1.3 Commonly used Fortran features	Completed
1.4 Basic OpenMP SIMD directives	In-progress
Phase. 2
2.1 Simplification on pass-by-ref	In-progress
2.2 Advanced OpenMP directives	In-progress
2.3 Advanced CIVL primitives	TODO
2.4 Array section/slicing	In-progress
Phase.3
3.1 MPI remote memory access	TODO
3.2 Testing and documentation	TODO
3.3 Apply CIVL on SciDAC apps	TODO

Completed

In-progress

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

TODO list

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

3. Evaluation