CIVL: Fortran Front End Overview

Back:DeveloperPage

1. Goals

The FORTRAN front-end is a CIVL component generating a set of intermediate abstract syntax trees (or CIVL IR) from given FORTRAN source files, then the verifier component can check desired correctness properties of the program based on its CIVL IR.

Motivations

• Numbers of software applications (esp. scientific ones) are written in FORTRAN programming language while few verifiers support this language;
• Most concurrent APIs (e.g., MPI, OpenMP, etc.) support both bindings of C and FORTRAN;
• The transformation between C and FORTRAN programs is frequent due to software evolution.

1.1. Basic goals

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 related goals

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
2.5 Verify FLASH5 examples	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

• Support basic OpenMP directives including: for constructs, parallel constructs, reduction clause, data clauses, etc.
• Commonly used basic FORTRAN features (FortranSubset)

In-progress

• Support verifying the functional equivalence for FLASH5 project (between the original version and optimized transformation);
• Re-construct the OpenMP-to-CIVL-IR transformer supporting SIMD directives and other scheduled directives.
• Construct semantic model for array sections
• Analyze and simplify ready-only parameters to be passed-by-val.

TODO list

• Support CIVL primitives

2. Design

The FORTRAN front-end involves four sub-components:

• a general preprocessor,
• a preprocessor token to FORTRAN token convertor,
• an ANTLR generated FORTRAN parser, and
• a FORTRAN parse tree to CIVL IR transformer.

Major reasons resulting in this design are:

• The de facto standard FORTRAN preprocessor is usually implemented as a C preprocessor compatible with FORTRAN specification.
• There are conflicts caused by the difference between two language specifications (e.g., a string wrapped by ' can be accepted in Fortran, but not in C)
• CIVL uses ANTLR parser generator to construct its C preprocessor and parser in Java.
• CIVL is originally designed for verifying C programs, so that its framework is coupled with C specification.

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