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

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

Appendix A. FORTRAN 2018 parse rules

A.1. Overview

Supported rule coverage summary
Chp.	#Supported	#Unsupported	#Total
Chp.5	0 (0.0%)	16 (100.0%)	16
Chp.6	0 (0.0%)	11 (100.0%)	11
Chp.7	0 (0.0%)	76 (100.0%)	76
Chp.8	0 (0.0%)	74 (100.0%)	74
Chp.9	0 (0.0%)	42 (100.0%)	42
Chp.10	0 (0.0%)	55 (100.0%)	55
Chp.11	0 (0.0%)	82 (100.0%)	82
Chp.12	0 (0.0%)	31 (100.0%)	31
Chp.13	0 (0.0%)	21 (100.0%)	21
Chp.14	0 (0.0%)	22 (100.0%)	22
Chp.15	0 (0.0%)	44 (100.0%)	44
Ext.CIVL	0 (0.0%)	0 (100.0%)	0
Total	0 (0.0%)	474 (100.0%)	474

A.2. Details

RuleID	Rule Name	Status
Chapter.5
R501	program
R502	program unit
R503	external subprogram
R504	specification part
R505	implicit part
R506	implicit part stmt
R507	declaration construct
R508	specification construct
R509	execution part
R510	execution part construct
R511	internal subprogram part
R512	internal subprogram
R513	other specification stmt
R514	executable construct
R515	action stmt
R516	keyword
Chapter.6
R601	alphanumeric character
R602	underscore
R603	name
R604	constant
R605	literal constant
R606	named constant
R607	int constant
R608	intrinsic operator
R609	defined operator
R610	extended intrinsic op
R611	label
Chapter.7
R701	type param value
R702	type spec
R703	declaration type spec
R704	intrinsictype spec
R705	integer type spec
R706	kind selector
R707	signed int literal constant
R708	int literal constant
R709	kind param
R710	signed digit string
R711	digit string
R712	sign
R713	signed real literal constant
R714	real literal constant
R715	significand
R716	exponent letter
R717	exponent
R718	complex literal constant
R719	real part
R720	imag part
R721	char selector
R722	length selector
R723	char length
R724	char literal constant
R725	logical literal constant
R726	derived type def
R727	derived type stmt
R728	type attr spec
R729	private or sequence
R730	end type stmt
R731	sequence stmt
R732	type param def stmt
R733	type param decl
R734	type param attr spec
R735	component part
R736	component def stmt
R737	data component def stmt
R738	component attr spec
R739	component decl
R740	component array spec
R741	proc component def stmt
R742	proc component attr spec
R743	component initialization
R744	initial data target
R745	private components stmt
R746	type bound procedure part
R747	binding private stmt
R748	type bound procedure stmt
R749	type bound procedure stmt
R750	type bound proc decl
R751	type bound generic stmt
R752	binding attr
R753	final procedure stmt
R754	derived type spec
R755	type param spec
R756	structure constructor
R757	component spec
R758	component data source
R759	enum def
R760	enum def stmt
R761	enumerator def stmt
R762	enumerator
R763	end enum stmt
R764	boz literal constant
R765	binary constant
R766	octal constant
R767	hex constant
R768	hex digit
R769	array constructor
R770	ac spec
R771	lbracket
R772	rbracket
R773	ac value
R774	ac implied do
R775	ac implied do control
R776	ac do variable
Chapter.8
R801	type declaration stmt
R802	attr spec
R803	entity decl
R804	object name
R805	initialization
R806	null init
R807	access spec
R808	language binding spec
R809	coarray spec
R810	deferred coshape spec
R811	explicit coshape spec
R812	lower cobound
R813	upper cobound
R814	dimension spec
R815	array spec
R816	eplicit shape spec
R817	lower bound
R818	upper bound
R819	assumed shape spec
R820	deferred shape spec
R821	assumed implied spec
R822	assumed size spec
R823	implied shape or assumed size spec
R824	implied shape spec
R825	assumed rank spec
R826	intent spec
R827	access stmt
R828	access id
R829	allocatable stmt
R830	allocatable decl
R831	asynchronous stmt
R832	bind stmt
R833	bind entity
R834	codimension stmt
R835	codimension decl
R836	contiguous stmt
R837	data stmt
R838	data stmt set
R839	data stmt object
R840	data implied do
R841	data i do object
R842	data i do variable
R843	data stmt value
R844	data stmt repeat
R845	data stmt constant
R846	int constant subobject
R847	constant subobject
R848	dimension stmt
R849	intent stmt
R850	optional stmt
R851	parameter stmt
R852	named constant def
R853	pinter stmt
R854	pointer decl
R855	protected stmt
R856	save stmt
R857	saved entity
R858	proc pointer name
R859	target stmt
R860	target decl
R861	value stmt
R862	volatile stmt
R863	implicit stmt
R864	implicit spec
R865	letter spec
R866	implicit none spec
R867	import stmt
R868	namelist stmt
R869	namelist group object
R870	equivalence stmt
R871	euivalence set
R872	equivalence object
R873	common stmt
R874	common block object
Chapter.9
R901	designator
R902	variable
R903	variable name
R904	logical variable
R905	char variable
R906	default char variable
R907	int variable
R908	substring
R909	parent string
R910	substring range
R911	data ref
R912	part ref
R913	structure component
R914	coindexed named object
R915	complex part designator
R916	type param inquiry
R917	array element
R918	array section
R919	subscript
R920	section subscript
R921	subscript triplet
R922	stride
R923	vector subscript
R924	image selector
R925	cosubscript
R926	image selector spec
R927	allocate stmt
R928	alloc opt
R929	errmsg variable
R930	source expr
R931	allocation
R932	allocate object
R933	allocate shape spec
R934	lower bound expr
R935	upper bound expr
R936	allocate coarray spec
R937	allocate coshape spec
R938	nullify stmt
R939	pointer object
R940	deallocate stmt
R941	dealloc opt
R942	stat variable
Chapter.10
R1001	primary
R1002	level 1 expr
R1003	defined unary op
R1004	mult operand
R1005	add operand
R1006	level 2 expr
R1007	power op
R1008	mult op
R1009	add op
R1010	level 3 expr
R1011	concat op
R1012	level 4 expr
R1013	rel op
R1014	and operand
R1015	or operand
R1016	equiv operand
R1017	level 5 expr
R1018	not op
R1019	and op
R1020	or op
R1021	equiv op
R1022	expr
R1023	defined binary op
R1024	logical expr
R1025	default char expr
R1026	int expr
R1027	numeric expr
R1028	specification expr
R1029	constant expr
R1030	default char constant expr
R1031	int constant expr
R1032	assignment stmt
R1033	pointer assignment stmt
R1034	data pointer object
R1035	bounds spec
R1036	bounds remapping
R1037	data target
R1038	proc pointer object
R1039	proc component ref
R1040	proc target
R1041	where stmt
R1042	where construct
R1043	where construct stmt
R1044	where body construct
R1045	where assignment stmt
R1046	mask expr
R1047	masked elsewhere stmt
R1048	elsewhere stmt
R1049	end where stmt
R1050	forall construct
R1051	forall construct stmt
R1052	forall body construct
R1053	forall assignment stmt
R1054	end forall stmt
R1055	forall stmt
Chapter.11
R1101	block
R1102	associate construct
R1103	associate stmt
R1104	association
R1105	selector
R1106	end associate stmt
R1107	block construct
R1108	block stmt
R1109	block specification part
R1110	end block stmt
R1111	change team construct
R1112	change team stmt
R1113	coarray association
R1114	end change team stmt
R1115	team value
R1116	critical construct
R1117	critical stmt
R1118	end critical stmt
R1119	do construct
R1120	do stmt
R1121	label do stmt
R1122	nonlabel do stmt
R1123	loop control
R1124	do variable
R1125	concurrent header
R1126	concurrent control
R1127	concurrent limit
R1128	concurrent step
R1129	concurrent locality
R1130	locality spec
R1131	end do
R1132	end do stmt
R1133	cycle stmt
R1134	if construct
R1135	if then stmt
R1136	else if stmt
R1137	else stmt
R1138	end if stmt
R1139	if stmt
R1140	case construct
R1141	select case stmt
R1142	case stmt
R1143	end select stmt
R1144	case expr
R1145	case selector
R1146	case value range
R1147	case value
R1148	select rank construct
R1149	select rank stmt
R1150	select rank case stmt
R1151	end select rank stmt
R1152	select type construct
R1153	select type stmt
R1154	type guard stmt
R1155	end select type stmt
R1156	exit stmt
R1157	goto stmt
R1158	computed goto stmt
R1159	continue stmt
R1160	stop stmt
R1161	error stop stmt
R1162	stop code
R1163	fail image stmt
R1164	sync all stmt
R1165	sync stat
R1166	sync images stmt
R1167	image set
R1168	sync memory stmt
R1169	sync team stmt
R1170	event post stmt
R1171	event variable
R1172	event wait stmt
R1173	event wait spec
R1174	until spec
R1175	form team stmt
R1176	team number
R1177	team variable
R1178	form team spec
R1179	lock stmt
R1180	lock stat
R1181	unlcok stmt
R1182	lock variable
Chapter.12
R1201	io unit
R1202	file until number
R1203	internal file variable
R1204	open stmt
R1205	connect spec
R1206	file name expr
R1207	iomsg variable
R1208	close stmt
R1209	close spec
R1210	read stmt
R1211	write stmt
R1212	print stmt
R1213	io control spec
R1214	id variable
R1215	format
R1216	input item
R1217	output item
R1218	io implied do
R1219	io implied do object
R1220	io implied do control
R1221	dtv type spec
R1222	wait stmt
R1223	wait spec
R1224	backspace stmt
R1225	endfile stmt
R1226	rewind stmt
R1227	position spec
R1228	flush stmt
R1229	flush spec
R1230	inquire stmt
R1231	inquire spec
Chapter.13
R1301	format stmt
R1302	format specification
R1303	format items
R1304	format item
R1305	unlimited format item
R1306	r
R1307	data edit spec
R1308	w
R1309	m
R1310	d
R1311	e
R1312	v
R1313	control edit spec
R1314	k
R1315	position edit spec
R1316	n
R1317	sign edit desc
R1318	blank interp edit desc
R1319	round edit desc
R1320	decimal edit desc
R1321	char string edit spec
Chapter.14
R1401	main program
R1402	program stmt
R1403	end program stmt
R1404	module
R1405	module stmt
R1406	end module stmt
R1407	module subprogram part
R1408	module subprogram
R1409	use stmt
R1410	module nature
R1411	rename
R1412	only
R1413	only use stmt
R1414	local defined operator
R1415	use defined operator
R1416	submodule
R1417	submodule stmt
R1418	parent identifier
R1419	end submodule stmt
R1420	block data
R1421	block data stmt
R1422	end block data stmt
Chapter.15
R1501	interface block
R1502	interface specification
R1503	interface stmt
R1504	end interface stmt
R1505	interface body
R1506	procedure stmt
R1507	specific procedure
R1508	generic spec
R1509	defined io generic spec
R1510	generic stmt
R1511	external stmt
R1512	procedure declaration stmt
R1513	proc interface
R1514	proc attr spec
R1515	proc decl
R1516	interface name
R1517	proc pointer init
R1518	initial proc target
R1519	intrinsic stmt
R1520	function reference
R1521	call stmt
R1522	procedure designator
R1523	actual arg spec
R1524	actual arg
R1525	alt return spec
R1526	prefix
R1527	prefix spec
R1528	proc language binding spec
R1529	function subprogram
R1530	function stmt
R1531	dummy arg stmt
R1532	suffix
R1533	end function stmt
R1534	subroutine subprogram
R1535	subroutine stmt
R1536	dymmy arg
R1537	end subroutine stmt
R1538	separate module subprogram
R1539	mp subprogram stmt
R1540	end mp subprogram stmt
R1541	entry stmt
R1542	return stmt
R1543	contains stmt
R1544	stmt fucntion stmt
CIVL extensions
R898	pragma stmt

Appendix B. OpenMP directives

B.1. Supported

B.2. Developing

B.3. Scheduled

B.4. Excluded