Context Navigation

CivlCParser.g@ cd08cf9

1.23 2.0 acw/focus-triggers main test-branch

Last change on this file since cd08cf9 was cd08cf9, checked in by Stephen Siegel <siegel@…>, 21 months ago

Fixed two front-end bugs. First was to add a new file implicit_defs.h which
is always loaded when translating any translation unit. It currently contains
one macro definition, attribute. Others may be added later. This was
so it could parse PETSc headers which use that feature a lot. We define
the macro to return nothing, so the attributes are just ignored.

Second was a problem with parsing certain typedefs. The logic for distinguishing
between a typedef name and identifier was wrong and has been fixed. It's a bit
complicated, but comments in CivlCParser.g explain the grammar changes.

Other minor changes.

git-svn-id: svn://vsl.cis.udel.edu/civl/trunk@5926 fb995dde-84ed-4084-dfe6-e5aef3e2452c

Property mode set to 100644

File size: 53.1 KB

Line
1	/* Grammar for programming CIVL-C.
2	* Based on C11 grammar.
3	*
4	* Author: Stephen F. Siegel, University of Delaware
5	*
6	* This grammar assumes the input token stream is the result of
7	* translation phase 7, as specified in the C11 Standard.
8	* In particular, all the preprocessing has already been
9	* done.
10	*
11	* In addition to the Standard, I borrowed from the older
12	* C grammar included with the ANTLR distribution.
13	*
14	*/
15	parser grammar CivlCParser;
16
17	options
18	{
19	language=Java;
20	tokenVocab=PreprocessorParser;
21	output=AST;
22	//backtrack=true;
23	}
24
25	tokens
26	{
27	ABSENT; // represents missing syntactic element
28	ANNOTATION; // like //@.../n or /@ ... /
29	ABSTRACT_DECLARATOR; // declarator without identifier
30	ARGUMENT_LIST; // list of arguments to an operator
31	ARRAY_ELEMENT_DESIGNATOR; // [idx]=expr
32	ARRAY_SUFFIX; // [..] used in declarator
33	BLOCK_ITEM_LIST; // list of block items
34	BOUND_VARIABLE_DECLARATION;// bound varialbe declaration
35	BOUND_VARIABLE_DECLARATION_LIST;// bound varialbe declaration list
36	BOUND_VARIABLE_NAME_LIST; // bound varialbe name list
37	BOUND_VARIABLE_RANGE; // bound varialbe declaration with range
38	BOUND_VARIABLE_RANGE_LIST;// bound varialbe declaration with range list
39	CALL; // function call
40	CASE_LABELED_STATEMENT; // case CONST: stmt
41	CAST; // type cast operator
42	COMPOUND_LITERAL; // literal for structs, etc.
43	COMPOUND_STATEMENT; // { ... }
44	CONTRACT; // procedure contracts
45	DECLARATION; // a declaration
46	DECLARATION_LIST; // list of declarations
47	DECLARATION_SPECIFIERS; // list of declaration specifiers
48	DECLARATOR; // a declarator
49	DEFAULT_LABELED_STATEMENT;// default: stmt
50	DERIVATIVE_EXPRESSION; // complete derivative expression
51	DESIGNATED_INITIALIZER; // used in compound initializer
52	DESIGNATION; // designation, used in compound initializer
53	DIRECT_ABSTRACT_DECLARATOR; // direct declarator sans identifier
54	DIRECT_DECLARATOR; // declarator after removing leading *s
55	ENUMERATION_CONSTANT; // use of enumeration constant
56	ENUMERATOR; // identifier and optional int constant
57	ENUMERATOR_LIST; // list of enumerators in enum type definition
58	EXPR; // symbol indicating "expression"
59	EXPRESSION_STATEMENT; // expr; (expression used as stmt)
60	FIELD_DESIGNATOR; // .id=expr
61	FUNCTION_DEFINITION; // function definition (contains body)
62	FUNCTION_SUFFIX; // (..) used in declarator
63	GENERIC_ASSOCIATION; // a generic association
64	GENERIC_ASSOC_LIST; // generic association list
65	IDENTIFIER_LABELED_STATEMENT; // label: stmt
66	IDENTIFIER_LIST; // list of parameter names only in function decl
67	INDEX; // array subscript operator
68	INITIALIZER_LIST; // initializer list in compound initializer
69	INIT_DECLARATOR; // initializer-declaration pair
70	INIT_DECLARATOR_LIST; // list of initializer-declarator pairs
71	INTERVAL; // a closed real interval [a,b] (used by $uniform)
72	INTERVAL_SEQ; // a sequence of INTERVAL
73	LIB_NAME; // name of a library
74	OPERATOR; // symbol indicating an operator
75	PARAMETER_DECLARATION; // parameter declaration in function decl
76	PARAMETER_LIST; // list of parameter decls in function decl
77	PARAMETER_TYPE_LIST; // parameter list and optional "..."
78	PARENTHESIZED_EXPRESSION; // ( expr )
79	PARTIAL; // CIVL-C partial derivative operator
80	PARTIAL_LIST; // list of partial operators
81	POINTER; // * used in declarator
82	POST_DECREMENT; // expr--
83	POST_INCREMENT; // expr++
84	PRE_DECREMENT; // --expr
85	PRE_INCREMENT; // ++expr
86	PROGRAM; // whole program (linking translation units)
87	QUANTIFIED; // quantified expression
88	SCALAR_INITIALIZER; // initializer for scalar variable
89	SPECIFIER_QUALIFIER_LIST; // list of type specifiers and qualifiers
90	STATEMENT; // a statement
91	STATEMENT_EXPRESSION; // a statement expression (GNU C extension)
92	STRUCT_DECLARATION; // a field declaration
93	STRUCT_DECLARATION_LIST; // list of field declarations
94	STRUCT_DECLARATOR; // a struct/union declarator
95	STRUCT_DECLARATOR_LIST; // list of struct/union declarators
96	TOKEN_LIST; // list of tokens, e.g., in pragma
97	TRANSLATION_UNIT; // final result of translation
98	TYPE; // symbol indicating "type"
99	TYPEDEF_NAME; // use of typedef name
100	TYPEOF_EXPRESSION;
101	TYPEOF_TYPE;
102	TYPE_NAME; // type specification without identifier
103	TYPE_QUALIFIER_LIST; // list of type qualifiers
104	}
105
106	scope Symbols {
107	Set<String> types; // to keep track of typedefs
108	Set<String> enumerationConstants; // to keep track of enum constants
109	boolean isFunctionDefinition; // "function scope": entire function definition
110	}
111
112	scope DeclarationScope {
113	boolean isTypedef; // is the current declaration a typedef
114	}
115
116	@header
117	{
118	package dev.civl.abc.front.c.parse;
119
120	import java.util.Set;
121	import java.util.HashSet;
122	import dev.civl.abc.front.IF.RuntimeParseException;
123	}
124
125	@members {
126	public void setSymbols_stack(Stack<ScopeSymbols> symbols){
127	this.Symbols_stack = new Stack();
128	while(!symbols.isEmpty()){
129	ScopeSymbols current = symbols.pop();
130	Symbols_scope mySymbols = new Symbols_scope();
131
132	mySymbols.types = current.types;
133	mySymbols.enumerationConstants = current.enumerationConstants;
134	Symbols_stack.add(mySymbols);
135	}
136	}
137
138	@Override
139	public String getSourceName() { return null; }
140
141	@Override
142	public void displayRecognitionError(String[] tokenNames, RecognitionException e) {
143	String hdr = getErrorHeader(e);
144	String msg = getErrorMessage(e, tokenNames);
145
146	throw new RuntimeParseException(hdr+" "+msg, e.token);
147	}
148
149	@Override
150	public void emitErrorMessage(String msg) { // don't try to recover!
151	throw new RuntimeParseException(msg);
152	}
153
154	// Is name the name of a type defined by an earlier typedef?
155	// Look through the symbol stack to find out.
156	boolean isTypeName(String name) {
157	for (Object scope : Symbols_stack)
158	if (((Symbols_scope)scope).types.contains(name)) {
159	return true;
160	}
161	return false;
162	}
163
164	// Looks in the symbol stack to determine whether name is the name
165	// of an enumeration constant.
166	boolean isEnumerationConstant(String name) {
167	boolean answer = false;
168
169	for (Object scope : Symbols_stack) {
170	if (((Symbols_scope)scope).enumerationConstants.contains(name)) {
171	answer=true;
172	break;
173	}
174	}
175	return answer;
176	}
177
178	/* This function returns true iff the current sequence of tokens has
179	the form X1 X2 X3, where
180
181	(1) X1 is an identifier, '*', or '(',
182	(2) if X1 is an identifier then X2 is a ';', ',' '[', or '(', and
183	(3) if X1 is an identifier and X2 is '(' then X3 is not '(' or '*'
184
185	Assume this token sequence begins either a
186	type-specifier-or-qualifier or the first declarator in a
187	typedef declaration. Then this function returns true iff the
188	sequence begins the first declarator. Hence it can be used to
189	determine when the type-specifier-or-qualifier list ends and
190	the declarator list begins.
191	*/
192	boolean indicatesDeclarator() {
193	Token token1 = input.LT(1);
194	int type1 = token1.getType();
195	if (type1 == STAR \|\| type1 == LPAREN) return true;
196	if (type1 != IDENTIFIER) return false;
197	Token token2 = input.LT(2);
198	int type2 = token2.getType();
199	if (type2 == SEMI \|\| type2 == COMMA \|\| type2 == LSQUARE)
200	return true;
201	if (type2 != LPAREN) return false;
202	Token token3 = input.LT(3);
203	int type3 = token3.getType();
204	return type3 != LPAREN && type3 != STAR;
205	}
206	}
207
208	/* *********************** A.2.1: Expressions *********************** */
209
210	/*
211	Operator precedence is dealt with in the usual way by creating
212	a "chain" of rules. This defines an increasing sequence of
213	languages, culminating in the language for all expressions.
214
215	Quantified expressions are kind of special and we start with them.
216	They are not included in the "chain". The problem is that we want
217	them to have the lowest precedence, so for example
218	$forall (int i) p && q
219	is parsed as
220	$forall (int i) (p && q)
221	However we also want to allow expressions such as
222	p && $forall (int i) q
223	This means that a quantified expression can occur as the right
224	argument of &&, but not as the left argument.
225	*/
226
227
228	/* One of the CIVL-C first-order quantifiers.
229	* UNIFORM represents uniform continuity.
230	*/
231	quantifier
232	: FORALL \| EXISTS \| UNIFORM
233	;
234
235	/* A CIVL-C quantified expression using $exists, $forall, or $uniform.
236	* Examples:
237	* $forall (int i) a[i]==i
238	* $forall (int i \| 0<=i && i<n) a[i]==b[i]
239	* An optional interval sequence is allowed for $uniform. That's
240	* an experimental feature that may go away.
241	*/
242	quantifiedExpression
243	: quantifier intervalSeq LPAREN boundVariableDeclarationList
244	( BITOR
245	(restrict=conditionalExpression \| restrict=quantifiedExpression)
246	RPAREN
247	body1=expression
248	-> ^(QUANTIFIED quantifier boundVariableDeclarationList
249	$body1 $restrict intervalSeq)
250	\| RPAREN
251	body2=expression
252	-> ^(QUANTIFIED quantifier boundVariableDeclarationList
253	$body2 ABSENT intervalSeq)
254	)
255	;
256
257	/* Constants from A.1.5.
258	* Includes several CIVL-C constants: $self, $proc_null, $state_null,
259	* $result, $here.
260	* TODO: why does this include ELLIPSIS?
261	*/
262	constant
263	: enumerationConstant
264	\| INTEGER_CONSTANT
265	\| FLOATING_CONSTANT
266	\| CHARACTER_CONSTANT
267	\| SELF
268	\| PROCNULL
269	\| STATE_NULL
270	\| RESULT
271	\| HERE
272	\| ELLIPSIS
273	;
274
275	/* Enumeration constants: an identifier that occurs in the current symbol
276	* stack's enumerationConstants fields */
277	enumerationConstant
278	: {isEnumerationConstant(input.LT(1).getText())}? IDENTIFIER ->
279	^(ENUMERATION_CONSTANT IDENTIFIER)
280	;
281
282	/* 6.5.1. C primary expressions. */
283	primaryExpression
284	: constant
285	\| IDENTIFIER
286	\| STRING_LITERAL
287	\| LPAREN compoundStatement RPAREN
288	-> ^(STATEMENT_EXPRESSION LPAREN compoundStatement RPAREN)
289	\| LPAREN expression RPAREN
290	-> ^(PARENTHESIZED_EXPRESSION LPAREN expression RPAREN)
291	\| genericSelection
292	\| derivativeExpression
293	;
294
295	/* 6.5.1.1 */
296	genericSelection
297	: GENERIC LPAREN assignmentExpression COMMA genericAssocList RPAREN
298	-> ^(GENERIC assignmentExpression genericAssocList)
299	;
300
301	/* A CIVL-C derivative expression. Some sequence
302	* of partial-differentiation operators applied to a function.
303	*/
304	derivativeExpression
305	: DERIV LSQUARE IDENTIFIER COMMA partialList RSQUARE
306	LPAREN argumentExpressionList RPAREN
307	-> ^(DERIVATIVE_EXPRESSION IDENTIFIER partialList
308	argumentExpressionList RPAREN)
309	;
310
311	/* A list of partial derivative operators. This is a CIVL-C addition.
312	*/
313	partialList
314	: partial (COMMA partial)* -> ^(PARTIAL_LIST partial+)
315	;
316
317	/* A CIVL-C partial-derivative operator */
318	partial
319	: LCURLY IDENTIFIER COMMA INTEGER_CONSTANT RCURLY
320	-> ^(PARTIAL IDENTIFIER INTEGER_CONSTANT)
321	;
322
323	/* 6.5.1.1 */
324	genericAssocList
325	: genericAssociation (COMMA genericAssociation)*
326	-> ^(GENERIC_ASSOC_LIST genericAssociation+)
327	;
328
329	/* 6.5.1.1 */
330	genericAssociation
331	: typeName COLON assignmentExpression
332	-> ^(GENERIC_ASSOCIATION typeName assignmentExpression)
333	\| DEFAULT COLON assignmentExpression
334	-> ^(GENERIC_ASSOCIATION DEFAULT assignmentExpression)
335	;
336
337	/* 6.5.2 */
338	postfixExpression
339	: (postfixExpressionRoot -> postfixExpressionRoot)
340	( // array index operator:
341	l=LSQUARE expression RSQUARE
342	-> ^(OPERATOR
343	INDEX[$l]
344	^(ARGUMENT_LIST $postfixExpression expression)
345	RSQUARE)
346	\| // function call:
347	LPAREN argumentExpressionList RPAREN
348	-> ^(CALL LPAREN $postfixExpression ABSENT argumentExpressionList
349	RPAREN ABSENT)
350	\| // CUDA kernel function call:
351	LEXCON args1=argumentExpressionList REXCON
352	LPAREN args2=argumentExpressionList RPAREN
353	-> ^(CALL LPAREN $postfixExpression $args1 $args2 RPAREN ABSENT)
354	\| DOT IDENTIFIER
355	-> ^(DOT $postfixExpression IDENTIFIER)
356	\| ARROW IDENTIFIER
357	-> ^(ARROW $postfixExpression IDENTIFIER)
358	\| p=PLUSPLUS
359	-> ^(OPERATOR POST_INCREMENT[$p]
360	^(ARGUMENT_LIST $postfixExpression))
361	\| m=MINUSMINUS
362	-> ^(OPERATOR POST_DECREMENT[$m]
363	^(ARGUMENT_LIST $postfixExpression))
364	)*
365	;
366
367	/*
368	* The "(typename) {...}" is a "compound literal".
369	* See C11 Sec. 6.5.2.5. I don't know what
370	* it means when it ends with an extra COMMA.
371	* I assume it doesn't mean anything and is just
372	* allowed as a convenience for the poor C programmer
373	* (but why?).
374	*
375	* Ambiguity: need to distinguish the compound literal
376	* "(typename) {...}" from the primaryExpression
377	* "(expression)". Presence of '{' implies it must
378	* be the compound literal.
379	*/
380	postfixExpressionRoot
381	: (LPAREN typeName RPAREN LCURLY)=>
382	LPAREN typeName RPAREN LCURLY initializerList
383	( RCURLY
384	\| COMMA RCURLY
385	)
386	-> ^(COMPOUND_LITERAL LPAREN typeName initializerList RCURLY)
387	\| primaryExpression
388	;
389
390	/* 6.5.2. A (possibly empty) comma-separated list of expressions. */
391	argumentExpressionList
392	: (a+=assignmentExpression \| a+=quantifiedExpression)
393	(COMMA (a+=assignmentExpression \| a+=quantifiedExpression))*
394	-> ^(ARGUMENT_LIST $a+)
395	\| -> ^(ARGUMENT_LIST)
396	;
397
398	/* 6.5.3. A unary expression, including many added by CIVL-C */
399	unaryExpression
400	scope DeclarationScope;
401	@init {
402	$DeclarationScope::isTypedef = false;
403	}
404	: postfixExpression
405	\| p=PLUSPLUS unaryExpression
406	-> ^(OPERATOR PRE_INCREMENT[$p]
407	^(ARGUMENT_LIST unaryExpression))
408	\| m=MINUSMINUS unaryExpression
409	-> ^(OPERATOR PRE_DECREMENT[$m]
410	^(ARGUMENT_LIST unaryExpression))
411	\| unaryOperator (a=castExpression \| a=quantifiedExpression)
412	-> ^(OPERATOR unaryOperator ^(ARGUMENT_LIST $a))
413	\| (SIZEOF LPAREN typeName)=> SIZEOF LPAREN typeName RPAREN
414	-> ^(SIZEOF TYPE typeName)
415	\| SIZEOF unaryExpression
416	-> ^(SIZEOF EXPR unaryExpression)
417	\| SCOPEOF unaryExpression
418	-> ^(SCOPEOF unaryExpression)
419	\| ALIGNOF LPAREN typeName RPAREN
420	-> ^(ALIGNOF typeName)
421	\| VALUE_AT LPAREN
422	b+=assignmentExpression COMMA
423	b+=assignmentExpression COMMA
424	(b+=assignmentExpression \| b+=quantifiedExpression) RPAREN
425	-> ^(VALUE_AT $b+ RPAREN)
426	\| spawnExpression
427	\| callsExpression
428	;
429
430	/* CIVL-C $spawn expression: $spawn f(...). */
431	spawnExpression
432	: SPAWN postfixExpressionRoot LPAREN argumentExpressionList RPAREN
433	-> ^(SPAWN LPAREN postfixExpressionRoot ABSENT
434	argumentExpressionList RPAREN)
435	;
436
437	/* A CIVL-C $calls expression, part of a function contract. */
438	callsExpression
439	: CALLS LPAREN postfixExpressionRoot LPAREN
440	argumentExpressionList RPAREN RPAREN
441	-> ^(CALLS LPAREN postfixExpressionRoot ABSENT
442	argumentExpressionList RPAREN)
443	;
444
445	/* 6.5.3. The unary operators &, *, +, -, ~, !, and $O. The $O
446	* is a CIVL-C addition used for big-O "order of" specification. */
447	unaryOperator
448	: AMPERSAND \| STAR \| PLUS \| SUB \| TILDE \| NOT \| BIG_O
449	;
450
451	/* 6.5.4: cast expressions: (typename)expr.
452	* Need to distinguish from other constructs that look like cast expressions,
453	* but aren't.
454	* ambiguity 1: (expr) is a unary expression and looks like (typeName).
455	* ambiguity 2: (typeName){...} is a compound literal and looks like cast.
456	*/
457	castExpression
458	scope DeclarationScope;
459	@init{
460	$DeclarationScope::isTypedef = false;
461	}
462	: (LPAREN typeName RPAREN ~LCURLY)=>
463	l=LPAREN typeName RPAREN castExpression
464	-> ^(CAST typeName castExpression $l)
465	\| unaryExpression
466	;
467
468	/* A CIVL-C "remote" expression: a@b. This is used in contracts in MPI
469	* programs to refer to the value of a variable on another process. */
470	remoteExpression
471	: (castExpression -> castExpression)
472	( (AT)=> AT y=castExpression
473	-> ^(OPERATOR AT ^(ARGUMENT_LIST $remoteExpression $y))
474	)*
475	;
476
477	/* 6.5.5. Multiplicative expressions: ab, a/b, and a%b. /
478	multiplicativeExpression
479	: (remoteExpression -> remoteExpression)
480	( (STAR)=> STAR y=remoteExpression
481	-> ^(OPERATOR STAR ^(ARGUMENT_LIST $multiplicativeExpression $y))
482	\| (DIV)=> DIV y=remoteExpression
483	-> ^(OPERATOR DIV ^(ARGUMENT_LIST $multiplicativeExpression $y))
484	\| (MOD)=> MOD y=remoteExpression
485	-> ^(OPERATOR MOD ^(ARGUMENT_LIST $multiplicativeExpression $y))
486	)*
487	;
488
489	/* 6.5.6. Additive expression: a+b or a-b. */
490	additiveExpression
491	: (multiplicativeExpression -> multiplicativeExpression)
492	( (PLUS)=> PLUS y=multiplicativeExpression
493	-> ^(OPERATOR PLUS ^(ARGUMENT_LIST $additiveExpression $y))
494	\| (SUB)=> SUB y=multiplicativeExpression
495	-> ^(OPERATOR SUB ^(ARGUMENT_LIST $additiveExpression $y))
496	)*
497	;
498
499	/* CIVL-C range expression "lo .. hi" or "lo .. hi # step"
500	* a + b .. c + d is equivalent to (a + b) .. (c + d). */
501	rangeExpression
502	: x=additiveExpression
503	( (DOTDOT)=> DOTDOT s=rangeSuffix -> ^(DOTDOT $x $s)
504	\| -> $x
505	)
506	;
507
508	rangeSuffix
509	: x=additiveExpression
510	( (HASH)=> HASH y=additiveExpression -> $x $y
511	\| -> $x
512	)
513	;
514
515	/* 6.5.7. A bitwise shift operation: a<<b or a>>b. */
516	shiftExpression
517	: (rangeExpression -> rangeExpression)
518	( (SHIFTLEFT)=> SHIFTLEFT y=rangeExpression
519	-> ^(OPERATOR SHIFTLEFT ^(ARGUMENT_LIST $shiftExpression $y))
520	\| (SHIFTRIGHT)=> SHIFTRIGHT y=rangeExpression
521	-> ^(OPERATOR SHIFTRIGHT ^(ARGUMENT_LIST $shiftExpression $y))
522	)*
523	;
524
525	/* 6.5.8. A relational expression involving <, >, <=, or >=. */
526	relationalExpression
527	: ( shiftExpression -> shiftExpression )
528	( (relationalOperator)=> relationalOperator
529	(y=shiftExpression)
530	-> ^(OPERATOR relationalOperator
531	^(ARGUMENT_LIST $relationalExpression $y))
532	)*
533	;
534
535	/* A relational operator other than == and !=, i.e., <, >, <=, >=. */
536	relationalOperator
537	: LT \| GT \| LTE \| GTE
538	;
539
540	/* 6.5.9. Equality and inequality: a==b and a!=b. */
541	equalityExpression
542	: ( relationalExpression -> relationalExpression )
543	( (equalityOperator)=>equalityOperator
544	(y=relationalExpression \| y=quantifiedExpression)
545	-> ^(OPERATOR equalityOperator
546	^(ARGUMENT_LIST $equalityExpression $y))
547	)*
548	;
549
550	/* Either == or !=. */
551	equalityOperator
552	: EQUALS \| NEQ
553	;
554
555	/* 6.5.10. Bitwise and: a&b. */
556	andExpression
557	: ( equalityExpression -> equalityExpression )
558	( (AMPERSAND)=> AMPERSAND y=equalityExpression
559	-> ^(OPERATOR AMPERSAND ^(ARGUMENT_LIST $andExpression $y))
560	)*
561	;
562
563	/* 6.5.11. Bitwise exclusive or: a^b. */
564	exclusiveOrExpression
565	: ( andExpression -> andExpression )
566	( (BITXOR)=> BITXOR y=andExpression
567	-> ^(OPERATOR BITXOR ^(ARGUMENT_LIST $exclusiveOrExpression $y))
568	)*
569	;
570
571	/* 6.5.12. Bitwise or: a\|b. */
572	inclusiveOrExpression
573	: ( exclusiveOrExpression -> exclusiveOrExpression )
574	( (BITOR)=> BITOR y=exclusiveOrExpression
575	-> ^(OPERATOR BITOR ^(ARGUMENT_LIST $inclusiveOrExpression $y))
576	)*
577	;
578
579	/* 6.5.13. Logical and: a && b. */
580	logicalAndExpression
581	: ( inclusiveOrExpression -> inclusiveOrExpression )
582	( (AND)=> AND (y=inclusiveOrExpression \| y=quantifiedExpression)
583	-> ^(OPERATOR AND ^(ARGUMENT_LIST $logicalAndExpression $y))
584	)*
585	;
586
587	/* 6.5.14. Logical or: a \|\| b. */
588	logicalOrExpression
589	: ( logicalAndExpression -> logicalAndExpression )
590	( (OR)=> OR (y=logicalAndExpression \| y=quantifiedExpression)
591	-> ^(OPERATOR OR ^(ARGUMENT_LIST $logicalOrExpression $y))
592	)*
593	;
594
595	/* Logical implication: a => b. Added for CIVL-C.
596	* Usually 6.5.15 would use logicalOrExpression. */
597	logicalImpliesExpression
598	: ( x=logicalOrExpression -> $x )
599	( (IMPLIES)=> IMPLIES (y=logicalImpliesExpression \| y=quantifiedExpression)
600	-> ^(OPERATOR IMPLIES ^(ARGUMENT_LIST $x $y))
601	)?
602	;
603
604	/* 6.5.15. A conditional expression, also known as if-then-else (ite)
605	* expression: a?b:c. */
606	conditionalExpression
607	: logicalImpliesExpression
608	( (QMARK)=> QMARK expression COLON
609	(y=conditionalExpression \| y=quantifiedExpression)
610	-> ^(OPERATOR QMARK
611	^(ARGUMENT_LIST
612	logicalImpliesExpression
613	expression
614	$y))
615	\| -> logicalImpliesExpression
616	)
617	;
618
619	/* A closed interval of real numbers [a,b]. Used in a $uniform expression. */
620	interval
621	: LSQUARE conditionalExpression COMMA conditionalExpression RSQUARE
622	-> ^(INTERVAL conditionalExpression conditionalExpression)
623	;
624
625	/* A (possibly empty) sequence of interval */
626	intervalSeq
627	: i+= interval i+= interval* -> ^(INTERVAL_SEQ $i+)
628	\| -> ABSENT
629	;
630
631	/* A CIVL-C array lambda expression. Examples:
632	* (int[])$lambda(int i,j \| i<j && j<n) 2*i+j
633	* (int[])$lambda(int i,j) 2*i+j
634	*/
635	arrayLambdaExpression
636	: ((LPAREN typeName RPAREN LAMBDA LPAREN
637	boundVariableDeclarationList BITOR) =>
638	LPAREN typeName RPAREN LAMBDA LPAREN
639	boundVariableDeclarationList BITOR
640	(restrict=conditionalExpression \| restrict=quantifiedExpression)
641	RPAREN
642	(cond1=assignmentExpression \| cond1=quantifiedExpression))
643	-> ^(LAMBDA typeName boundVariableDeclarationList $cond1 $restrict)
644	\| LPAREN typeName RPAREN LAMBDA LPAREN
645	boundVariableDeclarationList RPAREN
646	(cond2=assignmentExpression \| cond2=quantifiedExpression)
647	-> ^(LAMBDA typeName boundVariableDeclarationList $cond2)
648	;
649
650	boundVariableDeclarationSubList
651	: typeName IDENTIFIER (COMMA IDENTIFIER)* (COLON rangeExpression)?
652	-> ^(BOUND_VARIABLE_DECLARATION typeName
653	^(BOUND_VARIABLE_NAME_LIST IDENTIFIER+) rangeExpression?)
654	;
655
656	boundVariableDeclarationList
657	: boundVariableDeclarationSubList (SEMI boundVariableDeclarationSubList)*
658	-> ^(BOUND_VARIABLE_DECLARATION_LIST boundVariableDeclarationSubList+)
659	;
660
661
662
663	/* 6.5.16
664	* conditionalExpression or
665	* Root: OPERATOR
666	* Child 0: assignmentOperator
667	* Child 1: ARGUMENT_LIST
668	* Child 1.0: unaryExpression
669	* Child 1.1: assignmentExpression
670	*/
671	assignmentExpression
672	: (arrayLambdaExpression)=> arrayLambdaExpression
673	\| (unaryExpression assignmentOperator)=>
674	lhs=unaryExpression
675	op=assignmentOperator
676	(rhs=assignmentExpression \| rhs=quantifiedExpression)
677	-> ^(OPERATOR $op ^(ARGUMENT_LIST $lhs $rhs))
678	\| conditionalExpression
679	;
680
681	/* 6.5.16 */
682	assignmentOperator
683	: ASSIGN \| STAREQ \| DIVEQ \| MODEQ \| PLUSEQ \| SUBEQ
684	\| SHIFTLEFTEQ \| SHIFTRIGHTEQ \| BITANDEQ \| BITXOREQ \| BITOREQ
685	;
686
687	/* 6.5.17
688	* assignmentExpression or
689	* Root: OPERATOR
690	* Child 0: COMMA
691	* Child 1: ARGUMENT_LIST
692	* Child 1.0: arg0
693	* Child 1.1: arg1
694	*/
695	commaExpression
696	: ( assignmentExpression -> assignmentExpression )
697	( (COMMA)=> COMMA y=assignmentExpression
698	-> ^(OPERATOR COMMA ^(ARGUMENT_LIST $commaExpression $y))
699	)*
700	;
701
702	/* The most general class of expressions. This is the end of the chain. */
703	expression
704	: quantifiedExpression \| commaExpression
705	;
706
707	/* 6.6. Certain constructs require constant expressions.
708	* However it's too hard to recognize constant expressions in this
709	* grammar, so instead the grammar will accept any conditional
710	* expression as a constant expression, and the application will have to
711	* check whether those expressions are constant. */
712	constantExpression
713	: conditionalExpression
714	;
715
716
717	/* *********************** A.2.2: Declarations ********************** */
718
719	/* 6.7.
720	*
721	* This rule will construct either a DECLARATION, or
722	* STATICASSERT tree:
723	*
724	* Root: DECLARATION
725	* Child 0: declarationSpecifiers
726	* Child 1: initDeclaratorList or ABSENT
727	* Child 2: contract or ABSENT
728	*
729	* Root: STATICASSERT
730	* Child 0: constantExpression
731	* Child 1: stringLiteral
732	*
733	* The declarationSpecifiers rule returns a bit telling whether
734	* "typedef" occurred among the specifiers. This bit is passed
735	* to the initDeclaratorList rule, and down the call chain,
736	* where eventually an IDENTIFIER should be reached. At that point,
737	* if the bit is true, the IDENTIFIER is added to the set of typedef
738	* names.
739	*/
740	declaration
741	scope DeclarationScope;
742	@init {
743	$DeclarationScope::isTypedef = false;
744	}
745	: d=declarationSpecifiers
746	(
747	i=initDeclaratorList contract SEMI
748	-> ^(DECLARATION $d $i contract)
749	\| SEMI
750	-> ^(DECLARATION $d ABSENT ABSENT)
751	)
752	\| staticAssertDeclaration
753	;
754
755
756	/* 6.7
757	* Root: DECLARATION_SPECIFIERS
758	* Children: declarationSpecifier (any number)
759	*/
760	declarationSpecifiers
761	: l=declarationSpecifierList
762	-> ^(DECLARATION_SPECIFIERS declarationSpecifierList)
763	;
764
765	/* Tree: flat list of declarationSpecifier
766	In a typedef declaration scope, a declaration specifier cannot be
767	immediately followed by a ; , ( or [. An idenitifer that is
768	immediately followed by one of those tokens is an/the identifier being
769	defined by the typedef.
770	*/
771	declarationSpecifierList
772	: (
773	{!$DeclarationScope::isTypedef \|\| !indicatesDeclarator() }?
774	s=declarationSpecifier
775	)+
776	;
777
778	declarationSpecifier
779	: s=storageClassSpecifier
780	\| typeSpecifierOrQualifier
781	\| functionSpecifier
782	\| alignmentSpecifier
783	;
784
785	/*
786	* I factored this out of the declarationSpecifiers rule
787	* to deal with the ambiguity of "ATOMIC" in one place.
788	* "ATOMIC ( typeName )" matches atomicTypeSpecifier, which
789	* is a typeSpecifier. "ATOMIC" matches typeQualifier.
790	* When you see "ATOMIC" all you have to do is look at the
791	* next token. If it's '(', typeSpecifier is it.
792	*/
793	typeSpecifierOrQualifier
794	: (typeSpecifier)=> typeSpecifier
795	\| typeQualifier
796	;
797
798	/* 6.7
799	* Root: INIT_DECLARATOR_LIST
800	* Children: initDeclarator
801	*/
802	initDeclaratorList
803	: i+=initDeclarator (COMMA i+=initDeclarator)*
804	-> ^(INIT_DECLARATOR_LIST $i+)
805	;
806
807	/* 6.7
808	* Root: INIT_DECLARATOR
809	* Child 0: declarator
810	* Child 1: initializer or ABSENT
811	*/
812	initDeclarator
813	: d=declarator
814	( -> ^(INIT_DECLARATOR $d ABSENT)
815	\| (ASSIGN i=initializer) -> ^(INIT_DECLARATOR $d $i)
816	)
817	;
818
819	/* 6.7.1 */
820	storageClassSpecifier
821	: TYPEDEF {$DeclarationScope::isTypedef = true;}
822	\| (EXTERN \| STATIC \| THREADLOCAL \| AUTO \| REGISTER \| SHARED)
823	;
824
825	/* 6.7.2 */
826	typeSpecifier
827	: VOID \| CHAR \| SHORT \| INT \| LONG \| FLOAT \| DOUBLE
828	\| SIGNED \| UNSIGNED \| BOOL \| COMPLEX \| REAL \| RANGE
829	\| atomicTypeSpecifier
830	\| structOrUnionSpecifier
831	\| enumSpecifier
832	\| typedefName
833	\| domainSpecifier
834	\| typeofSpecifier
835	\| memSpecifier
836	;
837
838	/* GNU C extension:
839	* 6.6 Referring to a Type with typeof
840	* Another way to refer to the type of an expression is with typeof.
841	* The syntax of using of this keyword looks like sizeof, but the construct acts
842	* semantically like a type name defined with typedef.
843	* There are two ways of writing the argument to typeof: with an expression or with a type.
844	* Here is an example with an expression:
845	* typeof (x[0](1))
846	* This assumes that x is an array of pointers to functions; the type described is that of
847	* the values of the functions.
848	* Here is an example with a typename as the argument:
849	* typeof (int *)
850	* */
851	typeofSpecifier
852	: TYPEOF LPAREN
853	( commaExpression RPAREN
854	-> ^(TYPEOF_EXPRESSION LPAREN commaExpression RPAREN)
855	\| typeName RPAREN
856	-> ^(TYPEOF_TYPE LPAREN typeName RPAREN)
857	)
858	;
859
860	/* 6.7.2.1
861	* Root: STRUCT or UNION
862	* Child 0: IDENTIFIER (the tag) or ABSENT
863	* Child 1: structDeclarationList or ABSENT
864	*/
865	structOrUnionSpecifier
866	: structOrUnion
867	( IDENTIFIER LCURLY structDeclarationList RCURLY
868	-> ^(structOrUnion IDENTIFIER structDeclarationList RCURLY)
869	\| LCURLY structDeclarationList RCURLY
870	-> ^(structOrUnion ABSENT structDeclarationList RCURLY)
871	\| IDENTIFIER
872	-> ^(structOrUnion IDENTIFIER ABSENT)
873	)
874	;
875
876	/* 6.7.2.1 */
877	structOrUnion
878	: STRUCT \| UNION
879	;
880
881	/* 6.7.2.1
882	* Root: STRUCT_DECLARATION_LIST
883	* Children: structDeclaration
884	*/
885	structDeclarationList
886	: structDeclaration*
887	-> ^(STRUCT_DECLARATION_LIST structDeclaration*)
888	;
889
890	/* 6.7.2.1
891	* Two possible trees:
892	*
893	* Root: STRUCT_DECLARATION
894	* Child 0: specifierQualifierList
895	* Child 1: structDeclaratorList or ABSENT
896	*
897	* or
898	*
899	* staticAssertDeclaration (root: STATICASSERT)
900	*/
901	structDeclaration
902	scope DeclarationScope;
903	@init {
904	$DeclarationScope::isTypedef = false;
905	}
906	: s=specifierQualifierList
907	( -> ^(STRUCT_DECLARATION $s ABSENT)
908	\| structDeclaratorList
909	-> ^(STRUCT_DECLARATION $s structDeclaratorList)
910	)
911	SEMI
912	\| staticAssertDeclaration
913	;
914
915	/* 6.7.2.1
916	* Root: SPECIFIER_QUALIFIER_LIST
917	* Children: typeSpecifierOrQualifier
918	*/
919	specifierQualifierList
920	: typeSpecifierOrQualifier+
921	-> ^(SPECIFIER_QUALIFIER_LIST typeSpecifierOrQualifier+)
922	;
923
924	/* 6.7.2.1
925	* Root: STRUCT_DECLARATOR_LIST
926	* Children: structDeclarator (at least 1)
927	*/
928	structDeclaratorList
929	: s+=structDeclarator (COMMA s+=structDeclarator)*
930	-> ^(STRUCT_DECLARATOR_LIST $s+)
931	;
932
933	/* 6.7.2.1
934	* Root: STRUCT_DECLARATOR
935	* Child 0: declarator or ABSENT
936	* Child 1: constantExpression or ABSENT
937	*/
938	structDeclarator
939	: declarator
940	( -> ^(STRUCT_DECLARATOR declarator ABSENT)
941	\| COLON constantExpression
942	-> ^(STRUCT_DECLARATOR declarator constantExpression)
943	)
944	\| COLON constantExpression
945	-> ^(STRUCT_DECLARATOR ABSENT constantExpression)
946	;
947
948	/* 6.7.2.2
949	* Root: ENUM
950	* Child 0: IDENTIFIER (tag) or ABSENT
951	* Child 1: enumeratorList
952	*/
953	enumSpecifier
954	: ENUM
955	( IDENTIFIER
956	-> ^(ENUM IDENTIFIER ABSENT)
957	\| IDENTIFIER LCURLY enumeratorList COMMA? RCURLY
958	-> ^(ENUM IDENTIFIER enumeratorList)
959	\| LCURLY enumeratorList COMMA? RCURLY
960	-> ^(ENUM ABSENT enumeratorList)
961	)
962	;
963
964	/* 6.7.2.2
965	* Root: ENUMERATOR_LIST
966	* Children: enumerator
967	*/
968	enumeratorList
969	: enumerator (COMMA enumerator)*
970	-> ^(ENUMERATOR_LIST enumerator+)
971	;
972
973	/* 6.7.2.2
974	* Root: ENUMERATOR
975	* Child 0: IDENTIFIER
976	* Child 1: constantExpression or ABSENT
977	*/
978	enumerator
979	: IDENTIFIER
980	{
981	$Symbols::enumerationConstants.add($IDENTIFIER.text);
982	}
983	( -> ^(ENUMERATOR IDENTIFIER ABSENT)
984	\| (ASSIGN constantExpression)
985	-> ^(ENUMERATOR IDENTIFIER constantExpression)
986	)
987	;
988
989	/* 6.7.2.4 */
990	atomicTypeSpecifier
991	: ATOMIC LPAREN typeName RPAREN
992	-> ^(ATOMIC typeName)
993	;
994
995	/* 6.7.3 */
996	typeQualifier
997	: CONST \| RESTRICT \| VOLATILE \| ATOMIC \| INPUT \| OUTPUT
998	;
999
1000	/* 6.7.4. Added CIVL $atomic_f, indicating
1001	* a function should be executed atomically. CIVL's
1002	* $abstract specifier also included for abstract functions.
1003	* CIVL's $system specifier indicates a system function, with
1004	* additional field to denote the corresponding library.
1005	*/
1006	functionSpecifier
1007	: INLINE \| NORETURN
1008	\| abstractSpecifier
1009	\| PURE -> ^(PURE)
1010	\| STATE_F -> ^(STATE_F)
1011	\| ((SYSTEM libraryName) => SYSTEM libraryName) -> ^(SYSTEM libraryName)
1012	\| SYSTEM -> ^(SYSTEM ABSENT)
1013	\| FATOMIC -> ^(FATOMIC)
1014	\| DEVICE
1015	\| GLOBAL
1016	\| differentiableSpecifier
1017	;
1018
1019	abstractSpecifier
1020	: ABSTRACT ( -> ^(ABSTRACT)
1021	\| CONTIN LPAREN INTEGER_CONSTANT RPAREN
1022	-> ^(ABSTRACT INTEGER_CONSTANT)
1023	\| LPAREN STRING_LITERAL RPAREN
1024	-> ^(ABSTRACT STRING_LITERAL)
1025	)
1026	;
1027
1028	differentiableSpecifier
1029	: DIFFERENTIABLE LPAREN INTEGER_CONSTANT COMMA intervalSeq RPAREN
1030	->
1031	^(DIFFERENTIABLE INTEGER_CONSTANT intervalSeq)
1032	;
1033
1034	libraryName
1035	: LSQUARE i0=IDENTIFIER i1+=(SUB \| IDENTIFIER)* RSQUARE
1036	->^(LIB_NAME $i0 $i1*)
1037	;
1038
1039
1040	/* 6.7.5
1041	* Root: ALIGNAS
1042	* Child 0: TYPE or EXPR
1043	* Child 1: typeName (if Child 0 is TYPE) or constantExpression
1044	* (if Child 0 is EXPR)
1045	*/
1046	alignmentSpecifier
1047	: ALIGNAS LPAREN
1048	( typeName RPAREN
1049	-> ^(ALIGNAS TYPE typeName)
1050	\| constantExpression RPAREN
1051	-> ^(ALIGNAS EXPR constantExpression)
1052	)
1053	;
1054
1055	/* 6.7.6
1056	* Root: DECLARATOR
1057	* Child 0: pointer or ABSENT
1058	* Child 1: directDeclarator
1059	*/
1060	declarator
1061	: d=directDeclarator
1062	-> ^(DECLARATOR ABSENT $d)
1063	\| pointer d=directDeclarator
1064	-> ^(DECLARATOR pointer $d)
1065	;
1066
1067	/* 6.7.6
1068	* Root: DIRECT_DECLARATOR
1069	* Child 0: directDeclaratorPrefix
1070	* Children 1..: list of directDeclaratorSuffix (may be empty)
1071	*/
1072	directDeclarator
1073	: p=directDeclaratorPrefix
1074	( -> ^(DIRECT_DECLARATOR $p)
1075	\| s+=directDeclaratorSuffix+ ->^(DIRECT_DECLARATOR $p $s+)
1076	)
1077	;
1078
1079	/*
1080	* Tree: either an IDENTIFIER or a declarator.
1081	*/
1082	directDeclaratorPrefix
1083	: IDENTIFIER
1084	{
1085	if ($DeclarationScope::isTypedef) {
1086	$Symbols::types.add($IDENTIFIER.text);
1087	}
1088	}
1089	\| LPAREN! declarator RPAREN!
1090	;
1091
1092
1093	directDeclaratorSuffix
1094	: directDeclaratorArraySuffix
1095	\| directDeclaratorFunctionSuffix
1096	;
1097
1098	/*
1099	* Root: ARRAY_SUFFIX
1100	* child 0: LSQUARE (for source information)
1101	* child 1: STATIC or ABSENT
1102	* child 2: TYPE_QUALIFIER_LIST
1103	* child 3: expression (array extent),
1104	* "*" (unspecified variable length), or ABSENT
1105	* child 4: RSQUARE (for source information)
1106	*/
1107	directDeclaratorArraySuffix
1108	: LSQUARE
1109	( typeQualifierList_opt assignmentExpression_opt RSQUARE
1110	-> ^(ARRAY_SUFFIX LSQUARE ABSENT typeQualifierList_opt
1111	assignmentExpression_opt RSQUARE)
1112	\| STATIC typeQualifierList_opt assignmentExpression RSQUARE
1113	-> ^(ARRAY_SUFFIX LSQUARE STATIC typeQualifierList_opt
1114	assignmentExpression RSQUARE)
1115	\| typeQualifierList STATIC assignmentExpression RSQUARE
1116	-> ^(ARRAY_SUFFIX LSQUARE STATIC typeQualifierList
1117	assignmentExpression RSQUARE)
1118	\| typeQualifierList_opt STAR RSQUARE
1119	-> ^(ARRAY_SUFFIX LSQUARE ABSENT typeQualifierList_opt
1120	STAR RSQUARE)
1121	)
1122	;
1123
1124	/*
1125	* Root: FUNCTION_SUFFIX
1126	* child 0: LPAREN (for source information)
1127	* child 1: either parameterTypeList or identifierList or ABSENT
1128	* child 2: RPAREN (for source information)
1129	*/
1130	directDeclaratorFunctionSuffix
1131	scope DeclarationScope;
1132	@init {
1133	$DeclarationScope::isTypedef = false;
1134	}
1135	: LPAREN
1136	( parameterTypeList RPAREN
1137	-> ^(FUNCTION_SUFFIX LPAREN parameterTypeList RPAREN)
1138	\| identifierList RPAREN
1139	-> ^(FUNCTION_SUFFIX LPAREN identifierList RPAREN)
1140	\| RPAREN -> ^(FUNCTION_SUFFIX LPAREN ABSENT RPAREN)
1141	)
1142	;
1143
1144	/*
1145	* Root: TYPE_QUALIFIER_LIST
1146	* Children: typeQualifier
1147	*/
1148	typeQualifierList_opt
1149	: typeQualifier* -> ^(TYPE_QUALIFIER_LIST typeQualifier*)
1150	;
1151
1152	/*
1153	* Tree: assignmentExpression or ABSENT
1154	*/
1155	assignmentExpression_opt
1156	: -> ABSENT
1157	\| assignmentExpression
1158	;
1159
1160	/* 6.7.6
1161	* Root: POINTER
1162	* children: STAR
1163	*/
1164	pointer
1165	: pointer_part+ -> ^(POINTER pointer_part+)
1166	;
1167
1168	/*
1169	* Root: STAR
1170	* child 0: TYPE_QUALIFIER_LIST
1171	*/
1172	pointer_part
1173	: STAR typeQualifierList_opt
1174	-> ^(STAR typeQualifierList_opt)
1175	;
1176
1177	/* 6.7.6
1178	* Root: TYPE_QUALIFIER_LIST
1179	* children: typeQualifier
1180	*/
1181	typeQualifierList
1182	: typeQualifier+ -> ^(TYPE_QUALIFIER_LIST typeQualifier+)
1183	;
1184
1185	/* 6.7.6
1186	* Root: PARAMETER_TYPE_LIST
1187	* child 0: parameterList (at least 1 parameter declaration)
1188	* child 1: ELLIPSIS or ABSENT
1189	*
1190	* If the parameterTypeList occurs in a function prototype
1191	* (that is not part of a function definition), it defines
1192	* a new scope (a "function prototype scope"). If it occurs
1193	* in a function definition, it does not define a new scope.
1194	*/
1195
1196	parameterTypeList
1197	: {$Symbols::isFunctionDefinition}? parameterTypeListWithoutScope
1198	\| parameterTypeListWithScope
1199	;
1200
1201	parameterTypeListWithScope
1202	scope Symbols;
1203	@init {
1204	$Symbols::types = new HashSet<String>();
1205	$Symbols::enumerationConstants = new HashSet<String>();
1206	$Symbols::isFunctionDefinition = false;
1207	}
1208	: parameterTypeListWithoutScope
1209	;
1210
1211	parameterTypeListWithoutScope
1212	: parameterList
1213	( -> ^(PARAMETER_TYPE_LIST parameterList ABSENT)
1214	\| COMMA ELLIPSIS
1215	-> ^(PARAMETER_TYPE_LIST parameterList ELLIPSIS)
1216	)
1217	;
1218
1219	/* 6.7.6
1220	* Root: PARAMETER_LIST
1221	* children: parameterDeclaration
1222	*/
1223	parameterList
1224	: parameterDeclaration (COMMA parameterDeclaration)*
1225	-> ^(PARAMETER_LIST parameterDeclaration+)
1226	;
1227
1228	/* 6.7.6
1229	* Root: PARAMETER_DECLARATION
1230	* Child 0: declarationSpecifiers
1231	* Child 1: declarator, or abstractDeclarator, or ABSENT
1232	*/
1233	parameterDeclaration
1234	scope DeclarationScope;
1235	@init {
1236	$DeclarationScope::isTypedef = false;
1237	}
1238	: declarationSpecifiers
1239	( -> ^(PARAMETER_DECLARATION declarationSpecifiers ABSENT)
1240	\| declaratorOrAbstractDeclarator
1241	-> ^(PARAMETER_DECLARATION
1242	declarationSpecifiers declaratorOrAbstractDeclarator)
1243	)
1244	;
1245
1246
1247	// this has non-LL* decision due to recursive rule invocations
1248	// reachable from alts 1,2... E.g., both can start with pointer.
1249	declaratorOrAbstractDeclarator
1250	: (declarator)=> declarator
1251	\| abstractDeclarator
1252	;
1253
1254
1255	/* 6.7.6
1256	* Root: IDENTIFIER_LIST
1257	* children: IDENTIFIER (at least 1)
1258	*/
1259	identifierList
1260	: IDENTIFIER ( COMMA IDENTIFIER )*
1261	-> ^(IDENTIFIER_LIST IDENTIFIER+)
1262	;
1263
1264	/* 6.7.6. This is how a type is described without attaching
1265	* it to an identifier.
1266	* Root: TYPE_NAME
1267	* child 0: specifierQualifierList
1268	* child 1: abstractDeclarator or ABSENT
1269	*/
1270	typeName
1271	: specifierQualifierList
1272	( -> ^(TYPE_NAME specifierQualifierList ABSENT)
1273	\| abstractDeclarator
1274	-> ^(TYPE_NAME specifierQualifierList abstractDeclarator)
1275	)
1276	;
1277
1278	/* 6.7.7. Abstract declarators are like declarators without
1279	* the IDENTIFIER.
1280	*
1281	* Root: ABSTRACT_DECLARATOR
1282	* Child 0. pointer (may be ABSENT). Some number of *s with possible
1283	* type qualifiers.
1284	* Child 1. directAbstractDeclarator (may be ABSENT).
1285	*/
1286	abstractDeclarator
1287	: pointer
1288	-> ^(ABSTRACT_DECLARATOR pointer ABSENT)
1289	\| directAbstractDeclarator
1290	-> ^(ABSTRACT_DECLARATOR ABSENT directAbstractDeclarator)
1291	\| pointer directAbstractDeclarator
1292	-> ^(ABSTRACT_DECLARATOR pointer directAbstractDeclarator)
1293	;
1294
1295	/* 6.7.7
1296	*
1297	* Root: DIRECT_ABSTRACT_DECLARATOR
1298	* Child 0. abstract declarator or ABSENT.
1299	* Children 1..: any number of direct abstract declarator suffixes
1300	*
1301	* Note that the difference between this and a directDeclarator
1302	* is that Child 0 of a direct declarator would be either
1303	* an IDENTIFIER or a declarator, but never ABSENT.
1304	*/
1305	directAbstractDeclarator
1306	: LPAREN abstractDeclarator RPAREN directAbstractDeclaratorSuffix*
1307	-> ^(DIRECT_ABSTRACT_DECLARATOR abstractDeclarator
1308	directAbstractDeclaratorSuffix*)
1309	\| directAbstractDeclaratorSuffix+
1310	-> ^(DIRECT_ABSTRACT_DECLARATOR ABSENT directAbstractDeclaratorSuffix+)
1311	;
1312
1313
1314	/* 6.7.8
1315	* Root: TYPEDEF_NAME
1316	* Child 0: IDENTIFIER
1317	*
1318	* Ambiguity: example:
1319	* typedef int foo;
1320	* typedef int foo;
1321	*
1322	* This is perfectly legal: you can define a typedef twice
1323	* as long as both definitions are equivalent. However,
1324	* the first definition causes foo to be entered into the type name
1325	* table, so when parsing the second definition, foo is
1326	* interpreted as a typedefName (a type specifier), and the
1327	* declaration would have empty declarator. This is not
1328	* what you want, so you have to forbid it somehow. I do this
1329	* by requiring that if you are "in" a typedef, a typedef name
1330	* cannot be immediately followed by a semicolon. This is sound
1331	* because the C11 Standard requires at least one declarator
1332	* to be present in a typedef. See declarationSpecifierList.
1333	*/
1334	typedefName
1335	: {isTypeName(input.LT(1).getText())}? IDENTIFIER
1336	-> ^(TYPEDEF_NAME IDENTIFIER)
1337	;
1338
1339	/* 6.7.7
1340	* Two possibilities:
1341	*
1342	* Root: ARRAY_SUFFIX
1343	* Child 0: STATIC or ABSENT
1344	* Child 1: typeQualifierList or ABSENT
1345	* Child 2: expression or STAR or ABSENT
1346	*
1347	* Root: FUNCTION_SUFFIX
1348	* Child 0: parameterTypeList or ABSENT
1349	*/
1350	directAbstractDeclaratorSuffix
1351	: LSQUARE
1352	( typeQualifierList_opt assignmentExpression_opt RSQUARE
1353	-> ^(ARRAY_SUFFIX LSQUARE ABSENT typeQualifierList_opt
1354	assignmentExpression_opt)
1355	\| STATIC typeQualifierList_opt assignmentExpression RSQUARE
1356	-> ^(ARRAY_SUFFIX LSQUARE STATIC typeQualifierList_opt
1357	assignmentExpression)
1358	\| typeQualifierList STATIC assignmentExpression RSQUARE
1359	-> ^(ARRAY_SUFFIX LSQUARE STATIC typeQualifierList assignmentExpression)
1360	\| STAR RSQUARE
1361	-> ^(ARRAY_SUFFIX LSQUARE ABSENT ABSENT STAR)
1362	)
1363	\| LPAREN
1364	( parameterTypeList RPAREN
1365	-> ^(FUNCTION_SUFFIX LPAREN parameterTypeList RPAREN)
1366	\| RPAREN
1367	-> ^(FUNCTION_SUFFIX LPAREN ABSENT RPAREN)
1368	)
1369	;
1370
1371	/* 6.7.9 */
1372	initializer
1373	: assignmentExpression -> ^(SCALAR_INITIALIZER assignmentExpression)
1374	\| LCURLY initializerList
1375	( RCURLY
1376	\| COMMA RCURLY
1377	)
1378	-> initializerList
1379	;
1380
1381	/* 6.7.9 */
1382	initializerList
1383	: designatedInitializer (COMMA designatedInitializer)*
1384	-> ^(INITIALIZER_LIST designatedInitializer+)
1385	;
1386
1387	designatedInitializer
1388	: initializer
1389	-> ^(DESIGNATED_INITIALIZER ABSENT initializer)
1390	\| designation initializer
1391	-> ^(DESIGNATED_INITIALIZER designation initializer)
1392	;
1393
1394	/* 6.7.9 */
1395	designation
1396	: designatorList ASSIGN -> ^(DESIGNATION designatorList)
1397	;
1398
1399	/* 6.7.9 */
1400	designatorList
1401	: designator+
1402	;
1403
1404	/* 6.7.9 */
1405	designator
1406	: LSQUARE constantExpression RSQUARE
1407	-> ^(ARRAY_ELEMENT_DESIGNATOR constantExpression)
1408	\| DOT IDENTIFIER
1409	-> ^(FIELD_DESIGNATOR IDENTIFIER)
1410	;
1411
1412	/* 6.7.10 */
1413	staticAssertDeclaration
1414	: STATICASSERT LPAREN constantExpression COMMA STRING_LITERAL
1415	RPAREN SEMI
1416	-> ^(STATICASSERT constantExpression STRING_LITERAL)
1417	;
1418
1419	/* CIVL-C $domain or $domain(n) type */
1420	domainSpecifier
1421	: DOMAIN
1422	( -> ^(DOMAIN)
1423	\| LPAREN INTEGER_CONSTANT RPAREN -> ^(DOMAIN INTEGER_CONSTANT RPAREN)
1424	)
1425	;
1426
1427	/* CIVL-C $mem type */
1428	memSpecifier
1429	: MEM_TYPE -> ^(MEM_TYPE);
1430
1431
1432	/* *** A.2.3: Statements *** */
1433
1434	/* 6.8 */
1435	statement
1436	: labeledStatement -> ^(STATEMENT labeledStatement)
1437	\| compoundStatement -> ^(STATEMENT compoundStatement)
1438	\| expressionStatement -> ^(STATEMENT expressionStatement)
1439	\| selectionStatement -> ^(STATEMENT selectionStatement)
1440	\| iterationStatement -> ^(STATEMENT iterationStatement)
1441	\| jumpStatement -> ^(STATEMENT jumpStatement)
1442	\| whenStatement -> ^(STATEMENT whenStatement)
1443	\| chooseStatement -> ^(STATEMENT chooseStatement)
1444	\| atomicStatement -> ^(STATEMENT atomicStatement)
1445	\| runStatement -> ^(STATEMENT runStatement)
1446	\| withStatement -> ^(STATEMENT withStatement)
1447	\| updateStatement -> ^(STATEMENT updateStatement)
1448	\| asmStatement -> ^(STATEMENT asmStatement)
1449	;
1450
1451	statementWithScope
1452	scope Symbols;
1453	@init {
1454	$Symbols::types = new HashSet<String>();
1455	$Symbols::enumerationConstants = new HashSet<String>();
1456	$Symbols::isFunctionDefinition = false;
1457	}
1458	: statement
1459	\| pragma+ statement -> ^(STATEMENT ^(COMPOUND_STATEMENT ABSENT ^(BLOCK_ITEM_LIST pragma+ statement) ABSENT))
1460	;
1461
1462	/* 6.8.1
1463	* Three possible trees:
1464	*
1465	* Root: IDENTIFIER_LABELED_STATEMENT
1466	* Child 0: IDENTIFIER
1467	* Child 1: statement
1468	*
1469	* Root: CASE_LABELED_STATEMENT
1470	* Child 0: CASE
1471	* Child 1: constantExpression
1472	* Child 2: statement
1473	*
1474	* Root: DEFAULT_LABELED_STATEMENT
1475	* Child 0: DEFAULT
1476	* Child 1: statement
1477	*/
1478	labeledStatement
1479	: IDENTIFIER COLON statement
1480	-> ^(IDENTIFIER_LABELED_STATEMENT IDENTIFIER statement)
1481	\| CASE constantExpression COLON statement
1482	-> ^(CASE_LABELED_STATEMENT CASE constantExpression statement)
1483	\| DEFAULT COLON statement
1484	-> ^(DEFAULT_LABELED_STATEMENT DEFAULT statement)
1485	;
1486
1487	/* 6.8.2
1488	* Root: BLOCK
1489	* Child 0: LCURLY (for source information)
1490	* Child 1: blockItemList or ABSENT
1491	* Child 2: RCURLY (for source information)
1492	*/
1493	compoundStatement
1494	scope Symbols;
1495	scope DeclarationScope;
1496	@init {
1497	$Symbols::types = new HashSet<String>();
1498	$Symbols::enumerationConstants = new HashSet<String>();
1499	$Symbols::isFunctionDefinition = false;
1500	$DeclarationScope::isTypedef = false;
1501	}
1502	: LCURLY
1503	( RCURLY
1504	-> ^(COMPOUND_STATEMENT LCURLY ABSENT RCURLY)
1505	\| blockItemList RCURLY
1506	-> ^(COMPOUND_STATEMENT LCURLY blockItemList RCURLY)
1507	)
1508	;
1509
1510	/* 6.8.2 */
1511	blockItemList
1512	: blockItem+ -> ^(BLOCK_ITEM_LIST blockItem+)
1513	;
1514
1515
1516
1517	/* 6.8.3
1518	* Root: EXPRESSION_STATEMENT
1519	* Child 0: expression or ABSENT
1520	* Child 1: SEMI (for source information)
1521	*/
1522	expressionStatement
1523	: expression SEMI -> ^(EXPRESSION_STATEMENT expression SEMI)
1524	\| SEMI -> ^(EXPRESSION_STATEMENT ABSENT SEMI)
1525	;
1526
1527	/* 6.8.4
1528	* Two possible trees:
1529	*
1530	* Root: IF
1531	* Child 0: expression
1532	* Child 1: statement (true branch)
1533	* Child 2: statement or ABSENT (false branch)
1534	*
1535	* Root: SWITCH
1536	* Child 0: expression
1537	* Child 1: statement
1538	*/
1539	selectionStatement
1540	scope Symbols;
1541	@init {
1542	$Symbols::types = new HashSet<String>();
1543	$Symbols::enumerationConstants = new HashSet<String>();
1544	$Symbols::isFunctionDefinition = false;
1545	}
1546	: IF LPAREN expression RPAREN s1=statementWithScope
1547	( (ELSE)=> ELSE s2=statementWithScope
1548	-> ^(IF expression $s1 $s2)
1549	\| -> ^(IF expression $s1 ABSENT)
1550	)
1551	\| SWITCH LPAREN expression RPAREN s=statementWithScope
1552	-> ^(SWITCH expression $s)
1553	;
1554
1555	/* 6.8.5
1556	* Three possible trees:
1557	*
1558	* Root: WHILE
1559	* Child 0: expression
1560	* Child 1: statement
1561	*
1562	* Root: DO
1563	* Child 0: statement
1564	* Child 1: expression
1565	*
1566	* Root: FOR
1567	* Child 0: clause-1: declaration, expression, or ABSENT
1568	* (for loop initializer)
1569	* Child 1: expression or ABSENT (condition)
1570	* Child 2: expression or ABSENT (incrementer)
1571	* Child 3: statement (body)
1572	*
1573	*/
1574	iterationStatement
1575	scope Symbols;
1576	@init {
1577	$Symbols::types = new HashSet<String>();
1578	$Symbols::enumerationConstants = new HashSet<String>();
1579	$Symbols::isFunctionDefinition = false;
1580	}
1581	: WHILE LPAREN expression RPAREN invariant_opt
1582	s=statementWithScope
1583	-> ^(WHILE expression $s invariant_opt)
1584	\| DO s=statementWithScope WHILE LPAREN expression RPAREN
1585	invariant_opt SEMI
1586	-> ^(DO $s expression invariant_opt)
1587	\| FOR LPAREN
1588	(
1589	d=declaration e1=expression_opt SEMI e2=expression_opt
1590	RPAREN i=invariant_opt s=statementWithScope
1591	-> ^(FOR $d $e1 $e2 $s $i)
1592	\| e0=expression_opt SEMI e1=expression_opt SEMI
1593	e2=expression_opt RPAREN i=invariant_opt
1594	s=statementWithScope
1595	-> ^(FOR $e0 $e1 $e2 $s $i)
1596	)
1597	\| (f=CIVLFOR \| f=PARFOR) LPAREN
1598	t=typeName_opt v=identifierList COLON e=expression RPAREN
1599	i=invariant_opt s=statementWithScope
1600	-> ^($f $t $v $e $s $i)
1601	;
1602
1603	expression_opt
1604	: expression
1605	\| -> ABSENT
1606	;
1607
1608	invariant_opt
1609	: -> ABSENT
1610	\| INVARIANT LPAREN expression RPAREN
1611	-> ^(INVARIANT expression)
1612	;
1613
1614	typeName_opt
1615	: typeName
1616	\| -> ABSENT
1617	;
1618
1619	/* 6.8.6
1620	* Four possible trees:
1621	*
1622	* Root: GOTO
1623	* Child 0: IDENTIFIER
1624	* Child 1: SEMI (for source information)
1625	*
1626	* Root: CONTINUE
1627	* Child 0: SEMI (for source information)
1628	*
1629	* Root: BREAK
1630	* Child 0: SEMI (for source information)
1631	*
1632	* Root: RETURN
1633	* Child 0: expression or ABSENT
1634	* Child 1: SEMI (for source information)
1635	*/
1636	jumpStatement
1637	: GOTO IDENTIFIER SEMI -> ^(GOTO IDENTIFIER SEMI)
1638	\| CONTINUE SEMI -> ^(CONTINUE SEMI)
1639	\| BREAK SEMI -> ^(BREAK SEMI)
1640	\| RETURN expression_opt SEMI -> ^(RETURN expression_opt SEMI)
1641	;
1642
1643	/*
1644	* A pragma, which is represented as an identifier
1645	* (the first token following # pragma), followed
1646	* by a sequence of tokens.
1647	*
1648	* Root: PRAGMA
1649	* child 0: IDENTIFIER (first token following # pragma)
1650	* child 1: TOKEN_LIST (chilren are list of tokens following identifier)
1651	* child 2: NEWLINE (character which ends the pragma)
1652	*/
1653	pragma
1654	: PPRAGMA IDENTIFIER NEWLINE
1655	-> ^(PPRAGMA IDENTIFIER ^(TOKEN_LIST) NEWLINE)
1656	\| PPRAGMA IDENTIFIER inlineList NEWLINE
1657	-> ^(PPRAGMA IDENTIFIER ^(TOKEN_LIST inlineList) NEWLINE)
1658	;
1659
1660	/* inlineList : nonempty list of tokens not including NEWLINE */
1661	inlineList : (~ NEWLINE)+ ;
1662
1663
1664	/* Annotations
1665	* Root: ANNOTATION
1666	* child 0 : INLINE_ANNOTATION_START or ANNOTATION_START
1667	* child 1 : TOKEN_LIST (children are list of tokens comprising annotation body)
1668	* child 2 : ANNOTATION_END or NEWLINE (marking end of annotation)
1669	*/
1670
1671	annotation
1672	: INLINE_ANNOTATION_START
1673	( NEWLINE
1674	-> ^(ANNOTATION INLINE_ANNOTATION_START ^(TOKEN_LIST) NEWLINE)
1675	\| inlineList NEWLINE
1676	-> ^(ANNOTATION INLINE_ANNOTATION_START ^(TOKEN_LIST inlineList) NEWLINE)
1677	)
1678	\| ANNOTATION_START ANNOTATION_END
1679	-> ^(ANNOTATION ANNOTATION_START ^(TOKEN_LIST) ANNOTATION_END)
1680	\| ANNOTATION_START annotationBody ANNOTATION_END
1681	-> ^(ANNOTATION ANNOTATION_START ^(TOKEN_LIST annotationBody) ANNOTATION_END)
1682	;
1683
1684	annotationBody : (~ ANNOTATION_END)+ ;
1685
1686
1687	/* CIVL-C $run statement. This statement invokes an
1688	* asynchronous exeuction on the given statement.
1689	* Syntax: $run stmt.
1690	*
1691	* Root: RUN
1692	* Child 0: statement
1693	*/
1694	runStatement
1695	: RUN statement -> ^(RUN statement)
1696	;
1697
1698	/* CIVL-C $with statement. This statement is used to execute
1699	* a statement in an alternative state.
1700	*/
1701	withStatement
1702	: WITH LPAREN assignmentExpression RPAREN statement
1703	-> ^(WITH assignmentExpression statement)
1704	;
1705
1706	updateStatement
1707	: UPDATE LPAREN assignmentExpression RPAREN
1708	postfixExpressionRoot LPAREN argumentExpressionList RPAREN SEMI
1709	-> ^(UPDATE assignmentExpression
1710	^(CALL ABSENT postfixExpressionRoot ABSENT argumentExpressionList RPAREN)
1711	)
1712	;
1713
1714	balancedToken
1715	: ~(LPAREN \| RPAREN)
1716	\| LPAREN balancedToken* RPAREN
1717	;
1718
1719	asmStatement
1720	: ASM VOLATILE? GOTO? LPAREN
1721	balancedToken*
1722	RPAREN SEMI
1723	-> ^(ASM VOLATILE? GOTO? ^(TOKEN_LIST balancedToken*))
1724	;
1725
1726	/* CIVL-C $when statement. This is a guarded command.
1727	* Syntax: $when (expr) stmt, where expr is a boolean
1728	* expression (guard).
1729	*
1730	* Root: WHEN
1731	* Child 0: expression
1732	* Child 1: statement
1733	*/
1734	whenStatement
1735	: WHEN LPAREN expression RPAREN statement
1736	-> ^(WHEN expression statement)
1737	;
1738
1739	/* CIVL-C $choose statement. This is a non-deterministic
1740	* selection statement. Syntax: $choose { stmt stmt ... }.
1741	*
1742	* Root: CHOOSE
1743	* Children: 1 or more statement
1744	*/
1745	chooseStatement
1746	: CHOOSE LCURLY statement+ RCURLY
1747	-> ^(CHOOSE statement+)
1748	;
1749
1750	/* CIVL-C $atomic statement. Syntax:
1751	* $atomic stmt.
1752	*
1753	* Root: CIVLATOMIC
1754	* Child 0: statement
1755	*/
1756	atomicStatement
1757	: CIVLATOMIC s=statementWithScope
1758	-> ^(CIVLATOMIC $s)
1759	;
1760
1761	/* 6.9.1
1762	*
1763	* Root: FUNCTION_DEFINITION
1764	* Child 0: declarationSpecifiers
1765	* Child 1: declarator
1766	* Child 2: declarationList or ABSENT (formal parameters)
1767	* Child 3: compound statement (body)
1768	* Child 4: contract
1769	*/
1770	functionDefinition
1771	scope Symbols; // "function scope"
1772	scope DeclarationScope;
1773	@init {
1774	$Symbols::types = new HashSet<String>();
1775	$Symbols::enumerationConstants = new HashSet<String>();
1776	$Symbols::isFunctionDefinition = true;
1777	$DeclarationScope::isTypedef = false;
1778	}
1779	: declarator
1780	contract
1781	declarationList_opt
1782	compoundStatement
1783	-> ^(FUNCTION_DEFINITION ^(DECLARATION_SPECIFIERS) declarator
1784	declarationList_opt compoundStatement contract
1785	)
1786	\| declarationSpecifiers
1787	declarator
1788	contract
1789	declarationList_opt
1790	compoundStatement
1791	-> ^(FUNCTION_DEFINITION declarationSpecifiers declarator
1792	declarationList_opt compoundStatement contract
1793	)
1794	;
1795
1796
1797	/* 6.9.1
1798	* Root: DECLARATION_LIST
1799	* Children: declaration (any number)
1800	*/
1801	declarationList_opt
1802	: declaration* -> ^(DECLARATION_LIST declaration*)
1803	;
1804
1805	/* An item in a CIVL-C contract.
1806	*
1807	* Root: REQUIRES or ENSURES
1808	* Child: expression
1809	*/
1810	contractItem
1811	: separationLogicItem
1812	\| porItem
1813	;
1814
1815	separationLogicItem
1816	:
1817	REQUIRES LCURLY expression RCURLY -> ^(REQUIRES expression RCURLY)
1818	\| ENSURES LCURLY expression RCURLY -> ^(ENSURES expression RCURLY)
1819
1820	;
1821	porItem
1822	:
1823	DEPENDS (LSQUARE expression RSQUARE)? LCURLY argumentExpressionList RCURLY -> ^(DEPENDS expression? argumentExpressionList)
1824	\| GUARD (LSQUARE expression RSQUARE)? LCURLY argumentExpressionList RCURLY -> ^(GUARD expression? argumentExpressionList)
1825	\| ASSIGNS (LSQUARE expression RSQUARE)? LCURLY argumentExpressionList RCURLY -> ^(ASSIGNS expression? argumentExpressionList)
1826	\| READS (LSQUARE expression RSQUARE)? LCURLY argumentExpressionList RCURLY -> ^(READS expression? argumentExpressionList )
1827	;
1828
1829	/* A CIVL-C contract: sequence of 0 or more
1830	* contract items.
1831	*
1832	* Root: CONTRACT
1833	* Children: 0 or more contractItem
1834	*/
1835	contract
1836	: contractItem* -> ^(CONTRACT contractItem*)
1837	;
1838
1839
1840	/* A block item which can be called from the external world.
1841	* This requires a scope.
1842	*/
1843	blockItemWithScope
1844	scope DeclarationScope;
1845	@init {
1846	$DeclarationScope::isTypedef = false;
1847	}
1848	: blockItem;
1849
1850	/* A block item: a declaration, function definition,
1851	* or statement. Note that in C, a function definition
1852	* is not a block item, but in CIVL-C it is.
1853	*/
1854	blockItem
1855	:(declarator contract declarationList_opt LCURLY)=>
1856	functionDefinition
1857	\| (declarationSpecifiers declarator contract declarationList_opt LCURLY)=>
1858	functionDefinition
1859	\| declaration
1860	\| pragma
1861	\| annotation
1862	\| statement
1863	;
1864
1865	/* 6.9
1866	* Root: TRANSLATION_UNIT
1867	* Children: blockItem
1868	*
1869	* Note that this accepts more than what C allows.
1870	* C only allows "external declarations". This rule
1871	* allows any block item, and block items include
1872	* function definitions as well as statements,
1873	* declarations, etc. These are permissible in the
1874	* CIVL-C language. To enforce C's stricter restrictions,
1875	* do some checks on the tree after parsing completes.
1876	*/
1877	translationUnit
1878	scope Symbols; // the global scope
1879	scope DeclarationScope; // just to have an outermost one with isTypedef false
1880	@init {
1881	$Symbols::types = new HashSet<String>();
1882	$Symbols::enumerationConstants = new HashSet<String>();
1883	$Symbols::isFunctionDefinition = false;
1884	$DeclarationScope::isTypedef = false;
1885	}
1886	: blockItem* EOF
1887	-> ^(TRANSLATION_UNIT blockItem*)
1888	;

Note: See TracBrowser for help on using the repository browser.

Download in other formats:

Original Format