source: CIVL/mods/dev.civl.abc/grammar/c/CivlCParser.g@ 1786ea9

1.23 2.0 acw/focus-triggers main test-branch
Last change on this file since 1786ea9 was 1786ea9, checked in by Stephen Siegel <siegel@…>, 21 months ago

Fixing bugs in preprocessor when it comes to second expansions.
Attempted to fix a bug in C grammar concerning typedefs.

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