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

main test-branch
Last change on this file since 1aaefd4 was aad342c, checked in by Stephen Siegel <siegel@…>, 3 years ago

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

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