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

1.23 2.0 acw/focus-triggers main test-branch
Last change on this file since bd7a43e was bd7a43e, checked in by Alex Wilton <awilton@…>, 6 months ago

Added support for $sum

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