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

1.23 2.0 main test-branch
Last change on this file since bb03188 was 5700d00, checked in by Stephen Siegel <siegel@…>, 19 months ago

Fixed another problem in grammar regarding how abstract declarators were parsed,
which involved a slight refactoring of typeSpecifiers.
Fixed bug in type analyzer so that if a typedef defines a function type, the conversion
to pointer is applied.

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