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

main
Last change on this file was b3cd4ba, checked in by Alex Wilton <awilton@…>, 3 months ago

Changed syntax of $sum to be more like $forall

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