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

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

Cleaning up preprocessing and grammar changes.

git-svn-id: ​svn://vsl.cis.udel.edu/civl/trunk@5928 fb995dde-84ed-4084-dfe6-e5aef3e2452c
  • Property mode set to 100644
File size: 53.2 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 In a typedef declaration scope, a declaration specifier cannot be
758 immediately followed by a ; , ( or [. An identifier that is
759 immediately followed by one of those tokens is an/the identifier being
760 defined by the typedef.
761 */
762declarationSpecifierList
763 : ( { !indicatesDeclarator() }? declarationSpecifier )+
764 ;
765
766declarationSpecifier
767 : storageClassSpecifier
768 | typeSpecifierOrQualifier
769 | functionSpecifier
770 | alignmentSpecifier
771 ;
772
773/*
774 * I factored this out of the declarationSpecifiers rule
775 * to deal with the ambiguity of "ATOMIC" in one place.
776 * "ATOMIC ( typeName )" matches atomicTypeSpecifier, which
777 * is a typeSpecifier. "ATOMIC" matches typeQualifier.
778 * When you see "ATOMIC" all you have to do is look at the
779 * next token. If it's '(', typeSpecifier is it.
780 */
781typeSpecifierOrQualifier
782 : (typeSpecifier)=> typeSpecifier {$DeclarationScope::hasTypeSpec = true;}
783 | typeQualifier
784 ;
785
786/* 6.7
787 * Root: INIT_DECLARATOR_LIST
788 * Children: initDeclarator
789 */
790initDeclaratorList
791 : i+=initDeclarator (COMMA i+=initDeclarator)*
792 -> ^(INIT_DECLARATOR_LIST $i+)
793 ;
794
795/* 6.7
796 * Root: INIT_DECLARATOR
797 * Child 0: declarator
798 * Child 1: initializer or ABSENT
799 */
800initDeclarator
801 : d=declarator
802 ( -> ^(INIT_DECLARATOR $d ABSENT)
803 | (ASSIGN i=initializer) -> ^(INIT_DECLARATOR $d $i)
804 )
805 ;
806
807/* 6.7.1 */
808storageClassSpecifier
809 : TYPEDEF {$DeclarationScope::isTypedef = true;}
810 | (EXTERN | STATIC | THREADLOCAL | AUTO | REGISTER | SHARED)
811 ;
812
813/* 6.7.2 */
814typeSpecifier
815 : VOID | CHAR | SHORT | INT | LONG | FLOAT | DOUBLE
816 | SIGNED | UNSIGNED | BOOL | COMPLEX | REAL | RANGE
817 | atomicTypeSpecifier
818 | structOrUnionSpecifier
819 | enumSpecifier
820 | typedefName
821 | domainSpecifier
822 | typeofSpecifier
823 | memSpecifier
824 ;
825
826/* GNU C extension:
827 * 6.6 Referring to a Type with typeof
828 * Another way to refer to the type of an expression is with typeof.
829 * The syntax of using of this keyword looks like sizeof, but the construct acts
830 * semantically like a type name defined with typedef.
831 * There are two ways of writing the argument to typeof: with an expression or with a type.
832 * Here is an example with an expression:
833 * typeof (x[0](1))
834 * This assumes that x is an array of pointers to functions; the type described is that of
835 * the values of the functions.
836 * Here is an example with a typename as the argument:
837 * typeof (int *)
838 * */
839typeofSpecifier
840 : TYPEOF LPAREN
841 ( commaExpression RPAREN
842 -> ^(TYPEOF_EXPRESSION LPAREN commaExpression RPAREN)
843 | typeName RPAREN
844 -> ^(TYPEOF_TYPE LPAREN typeName RPAREN)
845 )
846 ;
847
848/* 6.7.2.1
849 * Root: STRUCT or UNION
850 * Child 0: IDENTIFIER (the tag) or ABSENT
851 * Child 1: structDeclarationList or ABSENT
852 */
853structOrUnionSpecifier
854 : structOrUnion
855 ( IDENTIFIER LCURLY structDeclarationList RCURLY
856 -> ^(structOrUnion IDENTIFIER structDeclarationList RCURLY)
857 | LCURLY structDeclarationList RCURLY
858 -> ^(structOrUnion ABSENT structDeclarationList RCURLY)
859 | IDENTIFIER
860 -> ^(structOrUnion IDENTIFIER ABSENT)
861 )
862 ;
863
864/* 6.7.2.1 */
865structOrUnion
866 : STRUCT | UNION
867 ;
868
869/* 6.7.2.1
870 * Root: STRUCT_DECLARATION_LIST
871 * Children: structDeclaration
872 */
873structDeclarationList
874 : structDeclaration*
875 -> ^(STRUCT_DECLARATION_LIST structDeclaration*)
876 ;
877
878/* 6.7.2.1
879 * Two possible trees:
880 *
881 * Root: STRUCT_DECLARATION
882 * Child 0: specifierQualifierList
883 * Child 1: structDeclaratorList or ABSENT
884 *
885 * or
886 *
887 * staticAssertDeclaration (root: STATICASSERT)
888 */
889structDeclaration
890scope DeclarationScope;
891@init {
892 $DeclarationScope::isTypedef = false;
893 $DeclarationScope::hasTypeSpec = false;
894}
895 : s=specifierQualifierList
896 ( -> ^(STRUCT_DECLARATION $s ABSENT)
897 | structDeclaratorList
898 -> ^(STRUCT_DECLARATION $s structDeclaratorList)
899 )
900 SEMI
901 | staticAssertDeclaration
902 ;
903
904/* 6.7.2.1
905 * Root: SPECIFIER_QUALIFIER_LIST
906 * Children: typeSpecifierOrQualifier
907 */
908specifierQualifierList
909 : typeSpecifierOrQualifier+
910 -> ^(SPECIFIER_QUALIFIER_LIST typeSpecifierOrQualifier+)
911 ;
912
913/* 6.7.2.1
914 * Root: STRUCT_DECLARATOR_LIST
915 * Children: structDeclarator (at least 1)
916 */
917structDeclaratorList
918 : s+=structDeclarator (COMMA s+=structDeclarator)*
919 -> ^(STRUCT_DECLARATOR_LIST $s+)
920 ;
921
922/* 6.7.2.1
923 * Root: STRUCT_DECLARATOR
924 * Child 0: declarator or ABSENT
925 * Child 1: constantExpression or ABSENT
926 */
927structDeclarator
928 : declarator
929 ( -> ^(STRUCT_DECLARATOR declarator ABSENT)
930 | COLON constantExpression
931 -> ^(STRUCT_DECLARATOR declarator constantExpression)
932 )
933 | COLON constantExpression
934 -> ^(STRUCT_DECLARATOR ABSENT constantExpression)
935 ;
936
937/* 6.7.2.2
938 * Root: ENUM
939 * Child 0: IDENTIFIER (tag) or ABSENT
940 * Child 1: enumeratorList
941 */
942enumSpecifier
943 : ENUM
944 ( IDENTIFIER
945 -> ^(ENUM IDENTIFIER ABSENT)
946 | IDENTIFIER LCURLY enumeratorList COMMA? RCURLY
947 -> ^(ENUM IDENTIFIER enumeratorList)
948 | LCURLY enumeratorList COMMA? RCURLY
949 -> ^(ENUM ABSENT enumeratorList)
950 )
951 ;
952
953/* 6.7.2.2
954 * Root: ENUMERATOR_LIST
955 * Children: enumerator
956 */
957enumeratorList
958 : enumerator (COMMA enumerator)*
959 -> ^(ENUMERATOR_LIST enumerator+)
960 ;
961
962/* 6.7.2.2
963 * Root: ENUMERATOR
964 * Child 0: IDENTIFIER
965 * Child 1: constantExpression or ABSENT
966 */
967enumerator
968 : IDENTIFIER
969 {
970 $Symbols::enumerationConstants.add($IDENTIFIER.text);
971 }
972 ( -> ^(ENUMERATOR IDENTIFIER ABSENT)
973 | (ASSIGN constantExpression)
974 -> ^(ENUMERATOR IDENTIFIER constantExpression)
975 )
976 ;
977
978/* 6.7.2.4 */
979atomicTypeSpecifier
980 : ATOMIC LPAREN typeName RPAREN
981 -> ^(ATOMIC typeName)
982 ;
983
984/* 6.7.3 */
985typeQualifier
986 : CONST | RESTRICT | VOLATILE | ATOMIC | INPUT | OUTPUT
987 ;
988
989/* 6.7.4. Added CIVL $atomic_f, indicating
990 * a function should be executed atomically. CIVL's
991 * $abstract specifier also included for abstract functions.
992 * CIVL's $system specifier indicates a system function, with
993 * additional field to denote the corresponding library.
994 */
995functionSpecifier
996 : INLINE | NORETURN
997 | abstractSpecifier
998 | PURE -> ^(PURE)
999 | STATE_F -> ^(STATE_F)
1000 | ((SYSTEM libraryName) => SYSTEM libraryName) -> ^(SYSTEM libraryName)
1001 | SYSTEM -> ^(SYSTEM ABSENT)
1002 | FATOMIC -> ^(FATOMIC)
1003 | DEVICE
1004 | GLOBAL
1005 | differentiableSpecifier
1006 ;
1007
1008abstractSpecifier
1009 : ABSTRACT ( -> ^(ABSTRACT)
1010 | CONTIN LPAREN INTEGER_CONSTANT RPAREN
1011 -> ^(ABSTRACT INTEGER_CONSTANT)
1012 | LPAREN STRING_LITERAL RPAREN
1013 -> ^(ABSTRACT STRING_LITERAL)
1014 )
1015 ;
1016
1017differentiableSpecifier
1018 : DIFFERENTIABLE LPAREN INTEGER_CONSTANT COMMA intervalSeq RPAREN
1019 -> ^(DIFFERENTIABLE INTEGER_CONSTANT intervalSeq)
1020 ;
1021
1022libraryName
1023 : LSQUARE i0=IDENTIFIER i1+=(SUB | IDENTIFIER)* RSQUARE
1024 -> ^(LIB_NAME $i0 $i1*)
1025 ;
1026
1027
1028/* 6.7.5
1029 * Root: ALIGNAS
1030 * Child 0: TYPE or EXPR
1031 * Child 1: typeName (if Child 0 is TYPE) or constantExpression
1032 * (if Child 0 is EXPR)
1033 */
1034alignmentSpecifier
1035 : ALIGNAS LPAREN
1036 ( typeName RPAREN
1037 -> ^(ALIGNAS TYPE typeName)
1038 | constantExpression RPAREN
1039 -> ^(ALIGNAS EXPR constantExpression)
1040 )
1041 ;
1042
1043/* 6.7.6
1044 * Root: DECLARATOR
1045 * Child 0: pointer or ABSENT
1046 * Child 1: directDeclarator
1047 */
1048declarator
1049 : d=directDeclarator
1050 -> ^(DECLARATOR ABSENT $d)
1051 | pointer d=directDeclarator
1052 -> ^(DECLARATOR pointer $d)
1053 ;
1054
1055/* 6.7.6
1056 * Root: DIRECT_DECLARATOR
1057 * Child 0: directDeclaratorPrefix
1058 * Children 1..: list of directDeclaratorSuffix (may be empty)
1059 */
1060directDeclarator
1061 : p=directDeclaratorPrefix
1062 ( -> ^(DIRECT_DECLARATOR $p)
1063 | s+=directDeclaratorSuffix+ -> ^(DIRECT_DECLARATOR $p $s+)
1064 )
1065 ;
1066
1067/*
1068 * Tree: either an IDENTIFIER or a declarator.
1069 */
1070directDeclaratorPrefix
1071 : IDENTIFIER
1072 {
1073 if ($DeclarationScope::isTypedef) {
1074 $Symbols::types.add($IDENTIFIER.text);
1075 }
1076 }
1077 | LPAREN! declarator RPAREN!
1078 ;
1079
1080
1081directDeclaratorSuffix
1082 : directDeclaratorArraySuffix
1083 | directDeclaratorFunctionSuffix
1084 ;
1085
1086/*
1087 * Root: ARRAY_SUFFIX
1088 * child 0: LSQUARE (for source information)
1089 * child 1: STATIC or ABSENT
1090 * child 2: TYPE_QUALIFIER_LIST
1091 * child 3: expression (array extent),
1092 * "*" (unspecified variable length), or ABSENT
1093 * child 4: RSQUARE (for source information)
1094 */
1095directDeclaratorArraySuffix
1096 : LSQUARE
1097 ( typeQualifierList_opt assignmentExpression_opt RSQUARE
1098 -> ^(ARRAY_SUFFIX LSQUARE ABSENT typeQualifierList_opt
1099 assignmentExpression_opt RSQUARE)
1100 | STATIC typeQualifierList_opt assignmentExpression RSQUARE
1101 -> ^(ARRAY_SUFFIX LSQUARE STATIC typeQualifierList_opt
1102 assignmentExpression RSQUARE)
1103 | typeQualifierList STATIC assignmentExpression RSQUARE
1104 -> ^(ARRAY_SUFFIX LSQUARE STATIC typeQualifierList
1105 assignmentExpression RSQUARE)
1106 | typeQualifierList_opt STAR RSQUARE
1107 -> ^(ARRAY_SUFFIX LSQUARE ABSENT typeQualifierList_opt
1108 STAR RSQUARE)
1109 )
1110 ;
1111
1112/*
1113 * Root: FUNCTION_SUFFIX
1114 * child 0: LPAREN (for source information)
1115 * child 1: either parameterTypeList or identifierList or ABSENT
1116 * child 2: RPAREN (for source information)
1117 */
1118directDeclaratorFunctionSuffix
1119scope DeclarationScope;
1120@init {
1121 $DeclarationScope::isTypedef = false;
1122 $DeclarationScope::hasTypeSpec = false;
1123}
1124 : LPAREN
1125 ( parameterTypeList RPAREN
1126 -> ^(FUNCTION_SUFFIX LPAREN parameterTypeList RPAREN)
1127 | identifierList RPAREN
1128 -> ^(FUNCTION_SUFFIX LPAREN identifierList RPAREN)
1129 | RPAREN -> ^(FUNCTION_SUFFIX LPAREN ABSENT RPAREN)
1130 )
1131 ;
1132
1133/*
1134 * Root: TYPE_QUALIFIER_LIST
1135 * Children: typeQualifier
1136 */
1137typeQualifierList_opt
1138 : typeQualifier* -> ^(TYPE_QUALIFIER_LIST typeQualifier*)
1139 ;
1140
1141/*
1142 * Tree: assignmentExpression or ABSENT
1143 */
1144assignmentExpression_opt
1145 : -> ABSENT
1146 | assignmentExpression
1147 ;
1148
1149/* 6.7.6
1150 * Root: POINTER
1151 * children: STAR
1152 */
1153pointer
1154 : pointer_part+ -> ^(POINTER pointer_part+)
1155 ;
1156
1157/*
1158 * Root: STAR
1159 * child 0: TYPE_QUALIFIER_LIST
1160 */
1161pointer_part
1162 : STAR typeQualifierList_opt -> ^(STAR typeQualifierList_opt)
1163 ;
1164
1165/* 6.7.6
1166 * Root: TYPE_QUALIFIER_LIST
1167 * children: typeQualifier
1168 */
1169typeQualifierList
1170 : typeQualifier+ -> ^(TYPE_QUALIFIER_LIST typeQualifier+)
1171 ;
1172
1173/* 6.7.6
1174 * Root: PARAMETER_TYPE_LIST
1175 * child 0: parameterList (at least 1 parameter declaration)
1176 * child 1: ELLIPSIS or ABSENT
1177 *
1178 * If the parameterTypeList occurs in a function prototype
1179 * (that is not part of a function definition), it defines
1180 * a new scope (a "function prototype scope"). If it occurs
1181 * in a function definition, it does not define a new scope.
1182 */
1183
1184parameterTypeList
1185 : {$Symbols::isFunctionDefinition}? parameterTypeListWithoutScope
1186 | parameterTypeListWithScope
1187 ;
1188
1189parameterTypeListWithScope
1190scope Symbols;
1191@init {
1192 $Symbols::types = new HashSet<String>();
1193 $Symbols::enumerationConstants = new HashSet<String>();
1194 $Symbols::isFunctionDefinition = false;
1195}
1196 : parameterTypeListWithoutScope
1197 ;
1198
1199parameterTypeListWithoutScope
1200 : parameterList
1201 ( -> ^(PARAMETER_TYPE_LIST parameterList ABSENT)
1202 | COMMA ELLIPSIS
1203 -> ^(PARAMETER_TYPE_LIST parameterList ELLIPSIS)
1204 )
1205 ;
1206
1207/* 6.7.6
1208 * Root: PARAMETER_LIST
1209 * children: parameterDeclaration
1210 */
1211parameterList
1212 : parameterDeclaration (COMMA parameterDeclaration)*
1213 -> ^(PARAMETER_LIST parameterDeclaration+)
1214 ;
1215
1216/* 6.7.6
1217 * Root: PARAMETER_DECLARATION
1218 * Child 0: declarationSpecifiers
1219 * Child 1: declarator, or abstractDeclarator, or ABSENT
1220 */
1221parameterDeclaration
1222scope DeclarationScope;
1223@init {
1224 $DeclarationScope::isTypedef = false;
1225 $DeclarationScope::hasTypeSpec = false;
1226}
1227 : declarationSpecifiers
1228 ( -> ^(PARAMETER_DECLARATION declarationSpecifiers ABSENT)
1229 | declaratorOrAbstractDeclarator
1230 -> ^(PARAMETER_DECLARATION
1231 declarationSpecifiers declaratorOrAbstractDeclarator)
1232 )
1233 ;
1234
1235
1236// this has non-LL* decision due to recursive rule invocations
1237// reachable from alts 1,2... E.g., both can start with pointer.
1238declaratorOrAbstractDeclarator
1239 : (declarator)=> declarator
1240 | abstractDeclarator
1241 ;
1242
1243
1244/* 6.7.6
1245 * Root: IDENTIFIER_LIST
1246 * children: IDENTIFIER (at least 1)
1247 */
1248identifierList
1249 : IDENTIFIER ( COMMA IDENTIFIER )* -> ^(IDENTIFIER_LIST IDENTIFIER+)
1250 ;
1251
1252/* 6.7.6. This is how a type is described without attaching
1253 * it to an identifier.
1254 * Root: TYPE_NAME
1255 * child 0: specifierQualifierList
1256 * child 1: abstractDeclarator or ABSENT
1257 */
1258typeName
1259 : specifierQualifierList
1260 ( -> ^(TYPE_NAME specifierQualifierList ABSENT)
1261 | abstractDeclarator
1262 -> ^(TYPE_NAME specifierQualifierList abstractDeclarator)
1263 )
1264 ;
1265
1266/* 6.7.7. Abstract declarators are like declarators without
1267 * the IDENTIFIER.
1268 *
1269 * Root: ABSTRACT_DECLARATOR
1270 * Child 0. pointer (may be ABSENT). Some number of *s with possible
1271 * type qualifiers.
1272 * Child 1. directAbstractDeclarator (may be ABSENT).
1273 */
1274abstractDeclarator
1275 : pointer
1276 -> ^(ABSTRACT_DECLARATOR pointer ABSENT)
1277 | directAbstractDeclarator
1278 -> ^(ABSTRACT_DECLARATOR ABSENT directAbstractDeclarator)
1279 | pointer directAbstractDeclarator
1280 -> ^(ABSTRACT_DECLARATOR pointer directAbstractDeclarator)
1281 ;
1282
1283/* 6.7.7
1284 *
1285 * Root: DIRECT_ABSTRACT_DECLARATOR
1286 * Child 0. abstract declarator or ABSENT.
1287 * Children 1..: any number of direct abstract declarator suffixes
1288 *
1289 * Note that the difference between this and a directDeclarator
1290 * is that Child 0 of a direct declarator would be either
1291 * an IDENTIFIER or a declarator, but never ABSENT.
1292 */
1293directAbstractDeclarator
1294 : LPAREN abstractDeclarator RPAREN directAbstractDeclaratorSuffix*
1295 -> ^(DIRECT_ABSTRACT_DECLARATOR abstractDeclarator
1296 directAbstractDeclaratorSuffix*)
1297 | directAbstractDeclaratorSuffix+
1298 -> ^(DIRECT_ABSTRACT_DECLARATOR ABSENT directAbstractDeclaratorSuffix+)
1299 ;
1300
1301
1302/* 6.7.8
1303 * Root: TYPEDEF_NAME
1304 * Child 0: IDENTIFIER
1305 *
1306 * A typedef name is an identifier which has been entered into
1307 * the the type name table by an earlier typedef. However note
1308 * the following exceptional scenario:
1309 *
1310 * typedef int foo;
1311 * typedef int foo;
1312 *
1313 * This is perfectly legal: you can define a typedef twice
1314 * as long as both definitions are equivalent. However,
1315 * the first definition causes foo to be entered into the type name
1316 * table, so when parsing the second definition, foo could be
1317 * interpreted as a typedefName (a type specifier), and the
1318 * declaration would have empty declarator. This is not
1319 * what you want, so you have to forbid it somehow. See
1320 * the rule for declarationSpecifiers, which uses a special
1321 * function to determine whether an identifier occurring in a
1322 * declaration can be considered a typedef.
1323 */
1324typedefName
1325 : {isTypeName(input.LT(1).getText())}? IDENTIFIER
1326 -> ^(TYPEDEF_NAME IDENTIFIER)
1327 ;
1328
1329/* 6.7.7
1330 * Two possibilities:
1331 *
1332 * Root: ARRAY_SUFFIX
1333 * Child 0: STATIC or ABSENT
1334 * Child 1: typeQualifierList or ABSENT
1335 * Child 2: expression or STAR or ABSENT
1336 *
1337 * Root: FUNCTION_SUFFIX
1338 * Child 0: parameterTypeList or ABSENT
1339 */
1340directAbstractDeclaratorSuffix
1341 : LSQUARE
1342 ( typeQualifierList_opt assignmentExpression_opt RSQUARE
1343 -> ^(ARRAY_SUFFIX LSQUARE ABSENT typeQualifierList_opt
1344 assignmentExpression_opt)
1345 | STATIC typeQualifierList_opt assignmentExpression RSQUARE
1346 -> ^(ARRAY_SUFFIX LSQUARE STATIC typeQualifierList_opt
1347 assignmentExpression)
1348 | typeQualifierList STATIC assignmentExpression RSQUARE
1349 -> ^(ARRAY_SUFFIX LSQUARE STATIC typeQualifierList assignmentExpression)
1350 | STAR RSQUARE
1351 -> ^(ARRAY_SUFFIX LSQUARE ABSENT ABSENT STAR)
1352 )
1353 | LPAREN
1354 ( parameterTypeList RPAREN
1355 -> ^(FUNCTION_SUFFIX LPAREN parameterTypeList RPAREN)
1356 | RPAREN
1357 -> ^(FUNCTION_SUFFIX LPAREN ABSENT RPAREN)
1358 )
1359 ;
1360
1361/* 6.7.9 */
1362initializer
1363 : assignmentExpression -> ^(SCALAR_INITIALIZER assignmentExpression)
1364 | LCURLY initializerList
1365 ( RCURLY
1366 | COMMA RCURLY
1367 )
1368 -> initializerList
1369 ;
1370
1371/* 6.7.9 */
1372initializerList
1373 : designatedInitializer (COMMA designatedInitializer)*
1374 -> ^(INITIALIZER_LIST designatedInitializer+)
1375 ;
1376
1377designatedInitializer
1378 : initializer
1379 -> ^(DESIGNATED_INITIALIZER ABSENT initializer)
1380 | designation initializer
1381 -> ^(DESIGNATED_INITIALIZER designation initializer)
1382 ;
1383
1384/* 6.7.9 */
1385designation
1386 : designatorList ASSIGN -> ^(DESIGNATION designatorList)
1387 ;
1388
1389/* 6.7.9 */
1390designatorList
1391 : designator+
1392 ;
1393
1394/* 6.7.9 */
1395designator
1396 : LSQUARE constantExpression RSQUARE
1397 -> ^(ARRAY_ELEMENT_DESIGNATOR constantExpression)
1398 | DOT IDENTIFIER
1399 -> ^(FIELD_DESIGNATOR IDENTIFIER)
1400 ;
1401
1402/* 6.7.10 */
1403staticAssertDeclaration
1404 : STATICASSERT LPAREN constantExpression COMMA STRING_LITERAL
1405 RPAREN SEMI
1406 -> ^(STATICASSERT constantExpression STRING_LITERAL)
1407 ;
1408
1409/* CIVL-C $domain or $domain(n) type */
1410domainSpecifier
1411 : DOMAIN
1412 ( -> ^(DOMAIN)
1413 | LPAREN INTEGER_CONSTANT RPAREN -> ^(DOMAIN INTEGER_CONSTANT RPAREN)
1414 )
1415 ;
1416
1417/* CIVL-C $mem type */
1418memSpecifier
1419 : MEM_TYPE -> ^(MEM_TYPE);
1420
1421
1422/* ***** A.2.3: Statements ***** */
1423
1424/* 6.8 */
1425statement
1426 : labeledStatement -> ^(STATEMENT labeledStatement)
1427 | compoundStatement -> ^(STATEMENT compoundStatement)
1428 | expressionStatement -> ^(STATEMENT expressionStatement)
1429 | selectionStatement -> ^(STATEMENT selectionStatement)
1430 | iterationStatement -> ^(STATEMENT iterationStatement)
1431 | jumpStatement -> ^(STATEMENT jumpStatement)
1432 | whenStatement -> ^(STATEMENT whenStatement)
1433 | chooseStatement -> ^(STATEMENT chooseStatement)
1434 | atomicStatement -> ^(STATEMENT atomicStatement)
1435 | runStatement -> ^(STATEMENT runStatement)
1436 | withStatement -> ^(STATEMENT withStatement)
1437 | updateStatement -> ^(STATEMENT updateStatement)
1438 | asmStatement -> ^(STATEMENT asmStatement)
1439 ;
1440
1441statementWithScope
1442scope Symbols;
1443@init {
1444 $Symbols::types = new HashSet<String>();
1445 $Symbols::enumerationConstants = new HashSet<String>();
1446 $Symbols::isFunctionDefinition = false;
1447}
1448 : statement
1449 | pragma+ statement -> ^(STATEMENT ^(COMPOUND_STATEMENT ABSENT ^(BLOCK_ITEM_LIST pragma+ statement) ABSENT))
1450 ;
1451
1452/* 6.8.1
1453 * Three possible trees:
1454 *
1455 * Root: IDENTIFIER_LABELED_STATEMENT
1456 * Child 0: IDENTIFIER
1457 * Child 1: statement
1458 *
1459 * Root: CASE_LABELED_STATEMENT
1460 * Child 0: CASE
1461 * Child 1: constantExpression
1462 * Child 2: statement
1463 *
1464 * Root: DEFAULT_LABELED_STATEMENT
1465 * Child 0: DEFAULT
1466 * Child 1: statement
1467 */
1468labeledStatement
1469 : IDENTIFIER COLON statement
1470 -> ^(IDENTIFIER_LABELED_STATEMENT IDENTIFIER statement)
1471 | CASE constantExpression COLON statement
1472 -> ^(CASE_LABELED_STATEMENT CASE constantExpression statement)
1473 | DEFAULT COLON statement
1474 -> ^(DEFAULT_LABELED_STATEMENT DEFAULT statement)
1475 ;
1476
1477/* 6.8.2
1478 * Root: BLOCK
1479 * Child 0: LCURLY (for source information)
1480 * Child 1: blockItemList or ABSENT
1481 * Child 2: RCURLY (for source information)
1482 */
1483compoundStatement
1484scope Symbols;
1485scope DeclarationScope;
1486@init {
1487 $Symbols::types = new HashSet<String>();
1488 $Symbols::enumerationConstants = new HashSet<String>();
1489 $Symbols::isFunctionDefinition = false;
1490 $DeclarationScope::isTypedef = false;
1491 $DeclarationScope::hasTypeSpec = false;
1492}
1493 : LCURLY
1494 ( RCURLY
1495 -> ^(COMPOUND_STATEMENT LCURLY ABSENT RCURLY)
1496 | blockItemList RCURLY
1497 -> ^(COMPOUND_STATEMENT LCURLY blockItemList RCURLY)
1498 )
1499 ;
1500
1501/* 6.8.2 */
1502blockItemList
1503 : blockItem+ -> ^(BLOCK_ITEM_LIST blockItem+)
1504 ;
1505
1506/* 6.8.3
1507 * Root: EXPRESSION_STATEMENT
1508 * Child 0: expression or ABSENT
1509 * Child 1: SEMI (for source information)
1510 */
1511expressionStatement
1512 : expression SEMI -> ^(EXPRESSION_STATEMENT expression SEMI)
1513 | SEMI -> ^(EXPRESSION_STATEMENT ABSENT SEMI)
1514 ;
1515
1516/* 6.8.4
1517 * Two possible trees:
1518 *
1519 * Root: IF
1520 * Child 0: expression
1521 * Child 1: statement (true branch)
1522 * Child 2: statement or ABSENT (false branch)
1523 *
1524 * Root: SWITCH
1525 * Child 0: expression
1526 * Child 1: statement
1527 */
1528selectionStatement
1529scope Symbols;
1530@init {
1531 $Symbols::types = new HashSet<String>();
1532 $Symbols::enumerationConstants = new HashSet<String>();
1533 $Symbols::isFunctionDefinition = false;
1534}
1535 : IF LPAREN expression RPAREN s1=statementWithScope
1536 ( (ELSE)=> ELSE s2=statementWithScope
1537 -> ^(IF expression $s1 $s2)
1538 | -> ^(IF expression $s1 ABSENT)
1539 )
1540 | SWITCH LPAREN expression RPAREN s=statementWithScope
1541 -> ^(SWITCH expression $s)
1542 ;
1543
1544/* 6.8.5
1545 * Three possible trees:
1546 *
1547 * Root: WHILE
1548 * Child 0: expression
1549 * Child 1: statement
1550 *
1551 * Root: DO
1552 * Child 0: statement
1553 * Child 1: expression
1554 *
1555 * Root: FOR
1556 * Child 0: clause-1: declaration, expression, or ABSENT
1557 * (for loop initializer)
1558 * Child 1: expression or ABSENT (condition)
1559 * Child 2: expression or ABSENT (incrementer)
1560 * Child 3: statement (body)
1561 *
1562 */
1563iterationStatement
1564scope Symbols;
1565@init {
1566 $Symbols::types = new HashSet<String>();
1567 $Symbols::enumerationConstants = new HashSet<String>();
1568 $Symbols::isFunctionDefinition = false;
1569}
1570 : WHILE LPAREN expression RPAREN invariant_opt
1571 s=statementWithScope
1572 -> ^(WHILE expression $s invariant_opt)
1573 | DO s=statementWithScope WHILE LPAREN expression RPAREN
1574 invariant_opt SEMI
1575 -> ^(DO $s expression invariant_opt)
1576 | FOR LPAREN
1577 (
1578 d=declaration e1=expression_opt SEMI e2=expression_opt
1579 RPAREN i=invariant_opt s=statementWithScope
1580 -> ^(FOR $d $e1 $e2 $s $i)
1581 | e0=expression_opt SEMI e1=expression_opt SEMI
1582 e2=expression_opt RPAREN i=invariant_opt
1583 s=statementWithScope
1584 -> ^(FOR $e0 $e1 $e2 $s $i)
1585 )
1586 | (f=CIVLFOR | f=PARFOR) LPAREN
1587 t=typeName_opt v=identifierList COLON e=expression RPAREN
1588 i=invariant_opt s=statementWithScope
1589 -> ^($f $t $v $e $s $i)
1590 ;
1591
1592expression_opt
1593 : expression
1594 | -> ABSENT
1595 ;
1596
1597invariant_opt
1598 : -> ABSENT
1599 | INVARIANT LPAREN expression RPAREN
1600 -> ^(INVARIANT expression)
1601 ;
1602
1603typeName_opt
1604 : typeName
1605 | -> ABSENT
1606 ;
1607
1608/* 6.8.6
1609 * Four possible trees:
1610 *
1611 * Root: GOTO
1612 * Child 0: IDENTIFIER
1613 * Child 1: SEMI (for source information)
1614 *
1615 * Root: CONTINUE
1616 * Child 0: SEMI (for source information)
1617 *
1618 * Root: BREAK
1619 * Child 0: SEMI (for source information)
1620 *
1621 * Root: RETURN
1622 * Child 0: expression or ABSENT
1623 * Child 1: SEMI (for source information)
1624 */
1625jumpStatement
1626 : GOTO IDENTIFIER SEMI -> ^(GOTO IDENTIFIER SEMI)
1627 | CONTINUE SEMI -> ^(CONTINUE SEMI)
1628 | BREAK SEMI -> ^(BREAK SEMI)
1629 | RETURN expression_opt SEMI -> ^(RETURN expression_opt SEMI)
1630 ;
1631
1632/*
1633 * A pragma, which is represented as an identifier
1634 * (the first token following # pragma), followed
1635 * by a sequence of tokens.
1636 *
1637 * Root: PRAGMA
1638 * child 0: IDENTIFIER (first token following # pragma)
1639 * child 1: TOKEN_LIST (chilren are list of tokens following identifier)
1640 * child 2: NEWLINE (character which ends the pragma)
1641 */
1642pragma
1643 : PPRAGMA IDENTIFIER NEWLINE
1644 -> ^(PPRAGMA IDENTIFIER ^(TOKEN_LIST) NEWLINE)
1645 | PPRAGMA IDENTIFIER inlineList NEWLINE
1646 -> ^(PPRAGMA IDENTIFIER ^(TOKEN_LIST inlineList) NEWLINE)
1647 ;
1648
1649/* inlineList : nonempty list of tokens not including NEWLINE */
1650inlineList : (~ NEWLINE)+ ;
1651
1652/* Annotations
1653 * Root: ANNOTATION
1654 * child 0 : INLINE_ANNOTATION_START or ANNOTATION_START
1655 * child 1 : TOKEN_LIST (children are list of tokens comprising annotation body)
1656 * child 2 : ANNOTATION_END or NEWLINE (marking end of annotation)
1657 */
1658
1659annotation
1660 : INLINE_ANNOTATION_START
1661 ( NEWLINE
1662 -> ^(ANNOTATION INLINE_ANNOTATION_START ^(TOKEN_LIST) NEWLINE)
1663 | inlineList NEWLINE
1664 -> ^(ANNOTATION INLINE_ANNOTATION_START ^(TOKEN_LIST inlineList) NEWLINE)
1665 )
1666 | ANNOTATION_START ANNOTATION_END
1667 -> ^(ANNOTATION ANNOTATION_START ^(TOKEN_LIST) ANNOTATION_END)
1668 | ANNOTATION_START annotationBody ANNOTATION_END
1669 -> ^(ANNOTATION ANNOTATION_START ^(TOKEN_LIST annotationBody) ANNOTATION_END)
1670 ;
1671
1672annotationBody : (~ ANNOTATION_END)+ ;
1673
1674/* CIVL-C $run statement. This statement invokes an
1675 * asynchronous exeuction on the given statement.
1676 * Syntax: $run stmt.
1677 *
1678 * Root: RUN
1679 * Child 0: statement
1680 */
1681runStatement
1682 : RUN statement -> ^(RUN statement)
1683 ;
1684
1685/* CIVL-C $with statement. This statement is used to execute
1686 * a statement in an alternative state.
1687 */
1688withStatement
1689 : WITH LPAREN assignmentExpression RPAREN statement
1690 -> ^(WITH assignmentExpression statement)
1691 ;
1692
1693updateStatement
1694 : UPDATE LPAREN assignmentExpression RPAREN
1695 postfixExpressionRoot LPAREN argumentExpressionList RPAREN SEMI
1696 -> ^(UPDATE assignmentExpression
1697 ^(CALL ABSENT postfixExpressionRoot ABSENT argumentExpressionList RPAREN)
1698 )
1699 ;
1700
1701balancedToken
1702 : ~(LPAREN | RPAREN)
1703 | LPAREN balancedToken* RPAREN
1704 ;
1705
1706asmStatement
1707 : ASM VOLATILE? GOTO? LPAREN
1708 balancedToken*
1709 RPAREN SEMI
1710 -> ^(ASM VOLATILE? GOTO? ^(TOKEN_LIST balancedToken*))
1711 ;
1712
1713/* CIVL-C $when statement. This is a guarded command.
1714 * Syntax: $when (expr) stmt, where expr is a boolean
1715 * expression (guard).
1716 *
1717 * Root: WHEN
1718 * Child 0: expression
1719 * Child 1: statement
1720 */
1721whenStatement
1722 : WHEN LPAREN expression RPAREN statement
1723 -> ^(WHEN expression statement)
1724 ;
1725
1726/* CIVL-C $choose statement. This is a non-deterministic
1727 * selection statement. Syntax: $choose { stmt stmt ... }.
1728 *
1729 * Root: CHOOSE
1730 * Children: 1 or more statement
1731 */
1732chooseStatement
1733 : CHOOSE LCURLY statement+ RCURLY -> ^(CHOOSE statement+)
1734 ;
1735
1736/* CIVL-C $atomic statement. Syntax:
1737 * $atomic stmt.
1738 *
1739 * Root: CIVLATOMIC
1740 * Child 0: statement
1741 */
1742atomicStatement
1743 : CIVLATOMIC s=statementWithScope -> ^(CIVLATOMIC $s)
1744 ;
1745
1746/* 6.9.1
1747 *
1748 * Root: FUNCTION_DEFINITION
1749 * Child 0: declarationSpecifiers
1750 * Child 1: declarator
1751 * Child 2: declarationList or ABSENT (formal parameters)
1752 * Child 3: compound statement (body)
1753 * Child 4: contract
1754 */
1755functionDefinition
1756scope Symbols; // "function scope"
1757scope DeclarationScope;
1758@init {
1759 $Symbols::types = new HashSet<String>();
1760 $Symbols::enumerationConstants = new HashSet<String>();
1761 $Symbols::isFunctionDefinition = true;
1762 $DeclarationScope::isTypedef = false;
1763 $DeclarationScope::hasTypeSpec = false;
1764}
1765 : declarator
1766 contract
1767 declarationList_opt
1768 compoundStatement
1769 -> ^(FUNCTION_DEFINITION ^(DECLARATION_SPECIFIERS) declarator
1770 declarationList_opt compoundStatement contract
1771 )
1772 | declarationSpecifiers
1773 declarator
1774 contract
1775 declarationList_opt
1776 compoundStatement
1777 -> ^(FUNCTION_DEFINITION declarationSpecifiers declarator
1778 declarationList_opt compoundStatement contract
1779 )
1780 ;
1781
1782
1783/* 6.9.1
1784 * Root: DECLARATION_LIST
1785 * Children: declaration (any number)
1786 */
1787declarationList_opt
1788 : declaration* -> ^(DECLARATION_LIST declaration*)
1789 ;
1790
1791/* An item in a CIVL-C contract.
1792 *
1793 * Root: REQUIRES or ENSURES
1794 * Child: expression
1795 */
1796contractItem
1797 : separationLogicItem
1798 | porItem
1799 ;
1800
1801separationLogicItem
1802 :
1803 REQUIRES LCURLY expression RCURLY -> ^(REQUIRES expression RCURLY)
1804 | ENSURES LCURLY expression RCURLY -> ^(ENSURES expression RCURLY)
1805
1806 ;
1807porItem
1808 :
1809 DEPENDS (LSQUARE expression RSQUARE)? LCURLY argumentExpressionList RCURLY
1810 -> ^(DEPENDS expression? argumentExpressionList)
1811 | GUARD (LSQUARE expression RSQUARE)? LCURLY argumentExpressionList RCURLY
1812 -> ^(GUARD expression? argumentExpressionList)
1813 | ASSIGNS (LSQUARE expression RSQUARE)? LCURLY argumentExpressionList RCURLY
1814 -> ^(ASSIGNS expression? argumentExpressionList)
1815 | READS (LSQUARE expression RSQUARE)? LCURLY argumentExpressionList RCURLY
1816 -> ^(READS expression? argumentExpressionList )
1817 ;
1818
1819/* A CIVL-C contract: sequence of 0 or more
1820 * contract items.
1821 *
1822 * Root: CONTRACT
1823 * Children: 0 or more contractItem
1824 */
1825contract
1826 : contractItem* -> ^(CONTRACT contractItem*)
1827 ;
1828
1829
1830/* A block item which can be called from the external world.
1831 * This requires a scope.
1832 */
1833blockItemWithScope
1834scope DeclarationScope;
1835@init {
1836 $DeclarationScope::isTypedef = false;
1837 $DeclarationScope::hasTypeSpec = false;
1838}
1839 : blockItem;
1840
1841/* A block item: a declaration, function definition,
1842 * or statement. Note that in C, a function definition
1843 * is not a block item, but in CIVL-C it is.
1844 */
1845blockItem
1846 : (declarator contract declarationList_opt LCURLY)=>
1847 functionDefinition
1848 | (declarationSpecifiers declarator contract declarationList_opt LCURLY)=>
1849 functionDefinition
1850 | declaration
1851 | pragma
1852 | annotation
1853 | statement
1854 ;
1855
1856/* 6.9
1857 * Root: TRANSLATION_UNIT
1858 * Children: blockItem
1859 *
1860 * Note that this accepts more than what C allows.
1861 * C only allows "external declarations". This rule
1862 * allows any block item, and block items include
1863 * function definitions as well as statements,
1864 * declarations, etc. These are permissible in the
1865 * CIVL-C language. To enforce C's stricter restrictions,
1866 * do some checks on the tree after parsing completes.
1867 */
1868translationUnit
1869scope Symbols; // the global scope
1870scope DeclarationScope; // just to have an outermost one with isTypedef false
1871@init {
1872 $Symbols::types = new HashSet<String>();
1873 $Symbols::enumerationConstants = new HashSet<String>();
1874 $Symbols::isFunctionDefinition = false;
1875 $DeclarationScope::isTypedef = false;
1876 $DeclarationScope::hasTypeSpec = false;
1877}
1878 : blockItem* EOF -> ^(TRANSLATION_UNIT blockItem*)
1879 ;
Note: See TracBrowser for help on using the repository browser.