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

1.23 2.0 main test-branch
Last change on this file since 7ffcb1b was c74ec20, checked in by Stephen Siegel <siegel@…>, 2 years ago

Add attribute string support to abstract functions in ABC
Add support in CIVL & SARL for some special attributes (e.g., "partial-order")

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