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

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

Added ANTLR source to classpath of ABC for better debugging.
Changed method for printing errors in CivlCParser.g so that it doesn't print out the wrong source, or any source, since source info is already in the token.
Removed unused import in an Executor.

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