source: CIVL/mods/dev.civl.abc/grammar/c/CivlCParser_alt.g

main
Last change on this file was aad342c, checked in by Stephen Siegel <siegel@…>, 3 years ago

Performing huge refactor to incorporate ABC, GMC, and SARL into CIVL repo and use Java modules.

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