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

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

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

git-svn-id: ​svn://vsl.cis.udel.edu/civl/trunk@5664 fb995dde-84ed-4084-dfe6-e5aef3e2452c
  • Property mode set to 100644
File size: 33.8 KB
Line 
1parser grammar AcslParser;
2
3/*
4 * Grammar for ACSL: an ANSI/ISO C Specification Language,
5 * with additional CIVL-C extensions.
6 * Based on ACSL 1.12.
7 * https://frama-c.com/acsl.html
8 *
9 * Author: Manchun Zheng, University of Delaware
10 * Author: Stephen F. Siegel, University of Delaware
11 * Last changed: May 2018
12 */
13
14options
15{
16 language=Java;
17 tokenVocab=PreprocessorParser;
18 output=AST;
19 backtrack = true; // TODO: get rid of this
20}
21
22tokens{
23 ABSENT;
24 ABSENT_EVENT_SENDTO;
25 ABSENT_EVENT_SENDFROM;
26 ABSENT_EVENT_ENTER;
27 ABSENT_EVENT_EXIT;
28 ABSTRACT_DECLARATOR;
29 ACCESS_ACSL;
30 ALLOC;
31 ANYACT;
32 ARGUMENT_LIST;
33 ARRAY_SUFFIX;
34 ASSUMES_ACSL;
35 ASSIGNS_ACSL;
36 ASSERT_ACSL;
37 BEHAVIOR;
38 BEHAVIOR_BODY;
39 BEHAVIOR_COMPLETE;
40 BEHAVIOR_DISJOINT;
41 BEQUIV_ACSL;
42 BIMPLIES_ACSL;
43 BINDER;
44 BINDER_LIST;
45 BOOLEAN;
46 BOTH;
47 C_TYPE;
48 CALL_ACSL;
49 CAST;
50 CLAUSE_NORMAL;
51 CLAUSE_BEHAVIOR;
52 CLAUSE_COMPLETE;
53 COL;
54 CONTRACT;
55 DEPENDSON;
56 DIRECT_ABSTRACT_DECLARATOR;
57 ENSURES_ACSL;
58 EVENT_BASE;
59 EVENT_PLUS;
60 EVENT_SUB;
61 EVENT_INTS;
62 EVENT_LIST;
63 EVENT_PARENTHESIZED;
64 EXECUTES_WHEN;
65 EXISTS_ACSL;
66 FALSE_ACSL;
67 FORALL_ACSL;
68 FREES;
69 FUNC_CALL;
70 FUNC_CONTRACT;
71 FUNC_CONTRACT_BLOCK;
72 ID_LIST;
73 INDEX;
74 INTEGER;
75 INTER;
76 LAMBDA_ACSL;
77 LOGIC_FUNCTIONS;
78 LOGIC_FUNCTION_CLAUSE;
79 LOGIC_TYPE;
80 LOOP_ALLOC;
81 LOOP_ASSIGNS;
82 LOOP_BEHAVIOR;
83 LOOP_CLAUSE;
84 LOOP_CONTRACT;
85 LOOP_CONTRACT_BLOCK;
86 LOOP_FREE;
87 LOOP_INVARIANT;
88 LOOP_VARIANT;
89 MAX;
90 MIN;
91 MPI_AGREE;
92 MPI_COLLECTIVE;
93 MPI_COMM_RANK;
94 MPI_COMM_SIZE;
95 MPI_CONSTANT;
96 MPI_EMPTY_IN;
97 MPI_EMPTY_OUT;
98 MPI_EQUALS;
99 MPI_EXPRESSION;
100 MPI_EXTENT;
101 MPI_OFFSET;
102 MPI_VALID;
103 MPI_REGION;
104 MPI_REDUCE;
105 MPI_ABSENT;
106 NOTHING;
107 NULL_ACSL;
108 NUMOF;
109 OBJECT_OF;
110 OLD;
111 OPERATOR;
112 P2P;
113 POINTER;
114 PROD;
115 PURE;
116 PREDICATE_CLAUSE;
117 LOGIC_FUNCTION_BODY; /* shared by both predicate and logic function */
118 QUANTIFIED;
119 QUANTIFIED_EXT;
120 READ_ACSL;
121 READS_ACSL;
122 REAL_ACSL;
123 RELCHAIN; // a chain of relational expressions
124 RESULT_ACSL;
125 REMOTE_ACCESS;
126 REQUIRES_ACSL;
127 SET_BINDERS;
128 SET_SIMPLE;
129 SIZEOF_EXPR;
130 SIZEOF_TYPE;
131 SPECIFIER_QUALIFIER_LIST;
132 SUM;
133 TERM_PARENTHESIZED;
134 TERMINATES;
135 TRUE_ACSL;
136 TYPE_BUILTIN;
137 TYPE_ID;
138 UNION_ACSL;
139 VALID;
140 VAR_ID;
141 VAR_ID_BASE;
142 VAR_ID_SQUARE;
143 VAR_ID_STAR;
144 WAITSFOR;
145 WRITE_ACSL;
146}
147
148@header
149{
150package dev.civl.abc.front.c.parse;
151}
152
153contract
154 : loop_contract
155 | function_contract
156 | logic_function_contract
157 | assert_contract
158 ;
159
160/* Section 2.4.2 Loop Annotations */
161loop_contract
162 : loop_contract_block
163 ->^(LOOP_CONTRACT loop_contract_block)
164 ;
165
166loop_contract_block
167 : lc+=loop_clause* lb+=loop_behavior* lv=loop_variant?
168 ->^(LOOP_CONTRACT_BLOCK $lc* $lb* $lv?)
169 ;
170
171loop_clause
172 : loop_invariant SEMI
173 ->^(LOOP_CLAUSE loop_invariant)
174 | loop_assigns SEMI
175 ->^(LOOP_CLAUSE loop_assigns)
176 | loop_allocation SEMI
177 ->^(LOOP_CLAUSE loop_allocation)
178 ;
179
180loop_invariant
181 : loop_key invariant_key term
182 ->^(LOOP_INVARIANT term)
183 ;
184
185loop_assigns
186 : loop_key assigns_key argumentExpressionList
187 ->^(LOOP_ASSIGNS assigns_key argumentExpressionList)
188 ;
189
190loop_allocation
191 : loop_key alloc_key argumentExpressionList (COMMA term)?
192 ->^(LOOP_ALLOC argumentExpressionList term?)
193 | loop_key frees_key argumentExpressionList
194 ->^(LOOP_FREE argumentExpressionList)
195 ;
196
197loop_behavior
198 : FOR ilist=id_list COLON lc+=loop_clause*
199 ->^(LOOP_BEHAVIOR $ilist $lc*)
200 ;
201
202loop_variant
203 : loop_key variant_key term
204 ->^(LOOP_VARIANT term)
205 | loop_key variant_key term FOR IDENTIFIER
206 ->^(LOOP_VARIANT term IDENTIFIER)
207 ;
208
209/* sec. 2.3 Function contracts */
210function_contract
211 : pure_function? full_contract_block
212 -> ^(FUNC_CONTRACT full_contract_block pure_function?)
213 ;
214
215/* sec. 2.6.1 Predicate and (Logic) Function
216 * definitions. Semantically, predicates are logic functions as
217 * well. */
218logic_function_contract
219 : (a+=logic_function_clause*) -> ^(LOGIC_FUNCTIONS $a*)
220 ;
221
222logic_function_clause
223 : logic_specifier_key type_expr a=IDENTIFIER b=logic_function_body SEMI
224 -> ^(LOGIC_FUNCTION_CLAUSE type_expr $a $b)
225 | predicate_key a=IDENTIFIER b=logic_function_body SEMI
226 -> ^(PREDICATE_CLAUSE $a $b)
227 ;
228
229/* simple ACSL assertion */
230assert_contract
231 : assert_key term SEMI -> ^(ASSERT_ACSL term)
232 ;
233
234/* ACSL logic function (predicate) declaration, either binder is
235 * absent or body is absent. They cannot be both absent. */
236/* binders (optional) = function-body */
237logic_function_body
238 : LPAREN binders RPAREN ASSIGN term
239 -> ^(LOGIC_FUNCTION_BODY binders term)
240 | LPAREN binders RPAREN
241 -> ^(LOGIC_FUNCTION_BODY binders ABSENT)
242 | ASSIGN term
243 -> ^(LOGIC_FUNCTION_BODY ABSENT term)
244 ;
245
246pure_function
247 : pure_key SEMI
248 ;
249
250/* a full contract block non-terminal represents an ACSL contract
251 * block for a function */
252full_contract_block
253 : (f+=function_clause)* (m+=contract_block)*
254 (c+=completeness_clause_block)*
255 -> ^(FUNC_CONTRACT_BLOCK $f* $m* $c*)
256 ;
257
258/* a partial contract block non-terminal represents an ACSL contract
259 * block inside an MPI collective block. There is no nested MPI
260 * collective block allowed */
261partial_contract_block
262 : (f+=function_clause)* (b+=named_behavior_block)*
263 (c+=completeness_clause_block)*
264 -> ^(FUNC_CONTRACT_BLOCK $f* $b* $c*)
265 ;
266
267/* a block in contracts, either an mpi collective block or a behavior
268* block. Behavior blocks are allowed to be inside an mpi collective
269* block while an mpi collective block will not belong to a behavior
270* block. An mpi collective block appears after a behavior block marks
271* the end of the behavior block. */
272contract_block
273 : mpi_collective_block
274 | named_behavior_block completeness_clause_block?
275 ;
276
277function_clause
278 : requires_clause SEMI-> ^(CLAUSE_NORMAL requires_clause)
279 | terminates_clause SEMI-> ^(CLAUSE_NORMAL terminates_clause)
280 | simple_clause SEMI -> ^(CLAUSE_NORMAL simple_clause)
281 ;
282
283named_behavior_block
284 : named_behavior -> ^(CLAUSE_BEHAVIOR named_behavior)
285 ;
286
287completeness_clause_block
288 : completeness_clause SEMI -> ^(CLAUSE_COMPLETE completeness_clause)
289 ;
290
291requires_clause
292 : requires_key term -> ^(REQUIRES_ACSL requires_key term)
293 ;
294
295terminates_clause
296 : terminates_key term -> ^(TERMINATES terminates_key term)
297 ;
298
299binders
300 : binder (COMMA binder)*
301 ->^(BINDER_LIST binder+)
302 ;
303
304binder
305 : type_expr variable_ident (COMMA variable_ident)*
306 ->^(BINDER type_expr variable_ident+)
307 ;
308
309type_expr
310 : logic_type_expr ->^(LOGIC_TYPE logic_type_expr)
311 | specifierQualifierList abstractDeclarator
312 -> ^(C_TYPE specifierQualifierList abstractDeclarator)
313 ;
314
315/* Start of C-like type name syntax */
316specifierQualifierList
317 : c_basic_type+
318 -> ^(SPECIFIER_QUALIFIER_LIST c_basic_type+)
319 ;
320
321abstractDeclarator
322 : pointer
323 -> ^(ABSTRACT_DECLARATOR pointer ABSENT)
324 | directAbstractDeclarator
325 -> ^(ABSTRACT_DECLARATOR ABSENT directAbstractDeclarator)
326 | pointer directAbstractDeclarator
327 -> ^(ABSTRACT_DECLARATOR pointer directAbstractDeclarator)
328 | -> ABSENT
329 ;
330
331directAbstractDeclarator
332 : LPAREN abstractDeclarator RPAREN directAbstractDeclaratorSuffix*
333 -> ^(DIRECT_ABSTRACT_DECLARATOR abstractDeclarator
334 directAbstractDeclaratorSuffix*)
335 | directAbstractDeclaratorSuffix+
336 -> ^(DIRECT_ABSTRACT_DECLARATOR ABSENT directAbstractDeclaratorSuffix+)
337 ;
338
339pointer
340 : STAR+ -> ^(POINTER STAR+)
341 ;
342
343directAbstractDeclaratorSuffix
344 : LSQUARE assignmentExpression_opt RSQUARE
345 -> ^(ARRAY_SUFFIX LSQUARE
346 assignmentExpression_opt RSQUARE)
347 ;
348/* End of C-like type name syntax */
349
350
351logic_type_expr
352 : built_in_logic_type ->^(TYPE_BUILTIN built_in_logic_type)
353 ;
354
355c_basic_type
356 : CHAR | DOUBLE | FLOAT | INT | LONG | SHORT | VOID
357 ;
358
359built_in_logic_type
360 : boolean_type | integer_type | real_type
361 ;
362
363variable_ident
364 : STAR variable_ident_base
365 ->^(VAR_ID_STAR variable_ident_base)
366 | variable_ident_base LSQUARE RSQUARE
367 ->^(VAR_ID_SQUARE variable_ident_base)
368 | variable_ident_base
369 ->^(VAR_ID variable_ident_base)
370 ;
371
372variable_ident_base
373 : IDENTIFIER
374 ->^(IDENTIFIER)
375 | LPAREN variable_ident RPAREN
376 ->^(VAR_ID_BASE variable_ident)
377 ;
378
379guards_clause
380 : executeswhen_key term ->^(EXECUTES_WHEN executeswhen_key term)
381 ;
382
383simple_clause
384 : assigns_clause
385 | ensures_clause
386 | allocation_clause
387 | reads_clause
388 | depends_clause
389 | guards_clause
390 | waitsfor_clause
391 ;
392
393assigns_clause
394 : assigns_key argumentExpressionList ->^(ASSIGNS_ACSL assigns_key argumentExpressionList)
395 ;
396
397ensures_clause
398 : ensures_key term ->^(ENSURES_ACSL ensures_key term)
399 ;
400
401allocation_clause
402 : alloc_key argumentExpressionList ->^(ALLOC alloc_key argumentExpressionList)
403 | frees_key argumentExpressionList ->^(FREES frees_key argumentExpressionList)
404 ;
405
406reads_clause
407 : reads_key argumentExpressionList ->^(READS_ACSL reads_key argumentExpressionList)
408 ;
409
410waitsfor_clause
411 : waitsfor_key argumentExpressionList -> ^(WAITSFOR waitsfor_key argumentExpressionList)
412 ;
413
414depends_clause
415 : dependson_key event_list ->^(DEPENDSON dependson_key event_list)
416 ;
417
418event_list
419 : event (COMMA event)* -> ^(EVENT_LIST event+)
420 ;
421
422event
423 : event_base PLUS event_base
424 -> ^(EVENT_PLUS event_base event_base)
425 | event_base SUB event_base
426 -> ^(EVENT_SUB event_base event_base)
427 | event_base AMPERSAND event_base
428 -> ^(EVENT_INTS event_base event_base)
429 | event_base
430 -> ^(EVENT_BASE event_base)
431 ;
432
433event_base
434 : read_key LPAREN argumentExpressionList RPAREN
435 -> ^(READ_ACSL read_key argumentExpressionList)
436 | write_key LPAREN argumentExpressionList RPAREN
437 -> ^(WRITE_ACSL write_key argumentExpressionList)
438 | access_key LPAREN argumentExpressionList RPAREN
439 -> ^(ACCESS_ACSL access_key argumentExpressionList)
440 | call_key LPAREN IDENTIFIER (COMMA argumentExpressionList)? RPAREN
441 -> ^(CALL_ACSL call_key IDENTIFIER argumentExpressionList?)
442 | nothing_key
443 | anyact_key
444 | LPAREN event RPAREN
445 -> ^(EVENT_PARENTHESIZED event)
446 ;
447
448/* ACSL-MPI extensions: constructors */
449mpi_collective_block
450 : mpicollective_key LPAREN IDENTIFIER COMMA kind=mpi_collective_kind RPAREN COLON
451 c=partial_contract_block -> ^(MPI_COLLECTIVE mpicollective_key IDENTIFIER $kind $c)
452 ;
453
454
455
456/* sec. 2.3.3 contracts with named behaviors */
457named_behavior
458 : behavior_key IDENTIFIER COLON behavior_body
459 -> ^(BEHAVIOR behavior_key IDENTIFIER behavior_body)
460 ;
461
462behavior_body
463 : (b+=behavior_clause SEMI)+ -> ^(BEHAVIOR_BODY $b+)
464 ;
465
466behavior_clause
467 : assumes_clause
468 | requires_clause
469 | simple_clause
470 ;
471
472assumes_clause
473 : assumes_key term ->^(ASSUMES_ACSL assumes_key term)
474 ;
475
476completeness_clause
477 : completes_key behaviors_key id_list
478 -> ^(BEHAVIOR_COMPLETE completes_key behaviors_key id_list)
479 | disjoint_key behaviors_key id_list
480 -> ^(BEHAVIOR_DISJOINT disjoint_key behaviors_key id_list)
481 ;
482
483id_list
484 :
485 | IDENTIFIER (COMMA IDENTIFIER)* -> ^(ID_LIST IDENTIFIER+)
486 ;
487
488/* C11 section 6.5 Expressions: Grammar here is organized with a
489 * backwards order against the order of sub-sections in C11 standard,
490 * because it's a more viewful way to illustrate how expressions will
491 * be derived
492 */
493
494 /* ****************************** Expressions ******************************* */
495
496// SFS: why is this called a "term"? Why not "formula"?
497term
498 : quantifierExpression | assignmentExpression
499 ;
500
501quantifierExpression
502 : forall_key binders SEMI term
503 -> ^(QUANTIFIED forall_key binders term)
504 | exists_key binders SEMI term
505 -> ^(QUANTIFIED exists_key binders term)
506 | lambda_key binders SEMI term
507 -> ^(LAMBDA_ACSL lambda_key binders term)
508 ;
509
510/* SFS: Does ACSL have an assignment expression?
511 * 6.5.16
512 * assignment-expression
513 * conditional-expression
514 * unary-expression assignment-operator assignment-expression
515 * Tree:
516 * Root: OPERATOR
517 * Child 0: ASSIGN, in ACSL other side-effective assign operators
518 * are not allowed
519 * Child 1: ARGUMENT_LIST
520 * Child 1.0: unaryExpression
521 * Child 1.1: assignmentExpression
522 */
523assignmentExpression
524 : (unaryExpression ASSIGN)=> unaryExpression ASSIGN assignmentExpression
525 -> ^(OPERATOR ASSIGN
526 ^(ARGUMENT_LIST unaryExpression assignmentExpression))
527 | conditionalExpression
528 ;
529
530assignmentExpression_opt
531 : -> ABSENT
532 | assignmentExpression
533 ;
534
535/* 6.5.15
536 * In C11 it is
537 * conditional-expression:
538 * logical-OR-expression
539 * logical-OR-expression ? expression : conditional-expression
540 *
541 * Note: "a?b:c?d:e". Is it (1) "(a?b:c)?d:e" or (2) "a?b:(c?d:e)".
542 * Answer is (2), it is "right associative".
543 *
544 * Note: the order matters in the two alternatives below.
545 * The alternatives are tried in order from first to last.
546 * Therefore it is necessary for the non-empty to appear first.
547 * Else the empty will always be matched.
548 */
549conditionalExpression
550 : a=logicalEquivExpression
551 ( QMARK b=conditionalExpression COLON
552 (c=quantifierExpression | c=conditionalExpression)
553 -> ^(OPERATOR QMARK ^(ARGUMENT_LIST $a $b $c))
554 | -> $a
555 )
556 ;
557
558/* ACSL Logical equivalence: a<==>b.
559 * Left associative: a<==>b<==>c means (a<==>b)<==>c.
560 */
561logicalEquivExpression
562 : (a=logicalImpliesExpression -> $a)
563 ( EQUIV_ACSL (b=quantifierExpression | b=logicalImpliesExpression)
564 -> ^(OPERATOR EQUIV_ACSL ^(ARGUMENT_LIST $logicalEquivExpression $b))
565 )*
566 ;
567
568/* ACSL logical implies expression: a==>b.
569 * NOTE: *RIGHT* associative: a==>b==>c is a==>(b==>c).
570 */
571logicalImpliesExpression
572 : a=logicalOrExpression
573 ( op=(IMPLIES|IMPLIES_ACSL) (b=quantifierExpression | b=logicalImpliesExpression)
574 -> ^(OPERATOR $op ^(ARGUMENT_LIST $a $b))
575 | -> $a
576 )
577 ;
578
579/* logical-OR-expression: a||b.
580 * Left associative: a||b||c is (a||b)||c.
581 */
582logicalOrExpression
583 : (a=logicalXorExpression -> $a)
584 ( OR (b=quantifierExpression | b=logicalXorExpression)
585 -> ^(OPERATOR OR ^(ARGUMENT_LIST $logicalOrExpression $b))
586 )*
587 ;
588
589/* ACSL logical exclusive or: a^^b.
590 * Left associative.
591 */
592logicalXorExpression
593 : (a=logicalAndExpression -> $a)
594 ( XOR_ACSL (b=quantifierExpression | b=logicalAndExpression)
595 -> ^(OPERATOR XOR_ACSL ^(ARGUMENT_LIST $logicalXorExpression $b))
596 )*
597 ;
598
599/* 6.5.13, logical and: a && b.
600 * Left associative.
601 */
602logicalAndExpression
603 : (a=bitwiseEquivExpression -> $a)
604 ( AND (b=quantifierExpression | b=bitwiseEquivExpression)
605 -> ^(OPERATOR AND ^(ARGUMENT_LIST $logicalAndExpression $b))
606 )*
607 ;
608
609/* ACSL bitwise equivalence: a <--> b.
610 * Left associative.
611 */
612bitwiseEquivExpression
613 : (a=bitwiseImpliesExpression -> $a)
614 ( bitequiv_op b=bitwiseImpliesExpression
615 -> ^(OPERATOR BEQUIV_ACSL ^(ARGUMENT_LIST $bitwiseEquivExpression $b))
616 )*
617 ;
618
619/* ACSL bitwise implies: a-->b.
620 * RIGHT associative
621 */
622bitwiseImpliesExpression
623 : a=inclusiveOrExpression
624 ( op=bitimplies_op b=bitwiseImpliesExpression
625 -> ^(OPERATOR BIMPLIES_ACSL ^(ARGUMENT_LIST $a $b))
626 | -> $a
627 )
628 ;
629
630// TODO: SFS: look at this, it doesn't make sense...
631/* 6.5.12 *
632 * Bitwise inclusive OR
633 * inclusive-OR-expression:
634 * exclusive-OR-expression
635 * inclusive-OR-expression | exclusive-OR-expression
636 *
637 * Note: the syntatic predicate before BITOR is to solve the ambiguity with
638 * set expressions because ACSL type names are parsed as IDENTIFIER tokens.
639 * For example, {a|integer | integer a; a<10}.
640 * The first | is a bitor operator and the first "integer" is some variable name.
641 * Without the predicate, the grammar would consider the second | as an bitor operator
642 * and crashes, because "integer" is an IDENTIFIER token and it thinkgs that the second
643 * "integer" is an identifier expression.
644 */
645inclusiveOrExpression
646 : ( exclusiveOrExpression -> exclusiveOrExpression )
647 ( {!(input.LA(2)==IDENTIFIER && input.LA(3)==IDENTIFIER)}?BITOR y=exclusiveOrExpression
648 -> ^(OPERATOR BITOR ^(ARGUMENT_LIST $inclusiveOrExpression $y))
649 )*
650 ;
651
652/* 6.5.11 *
653 * Bitwise exclusive OR
654 * exclusive-OR-expression:
655 * AND-expression
656 * exclusive-OR-expression ^ AND-expression
657 */
658exclusiveOrExpression
659 : ( andExpression -> andExpression )
660 ( BITXOR y=andExpression
661 -> ^(OPERATOR BITXOR ^(ARGUMENT_LIST $exclusiveOrExpression $y))
662 )*
663 ;
664
665/* 6.5.10 *
666 * Bitwise AND
667 * AND-expression
668 * equality-expression
669 * AND-expression & equality-expression
670 */
671andExpression
672 : ( relationalExpression -> relationalExpression )
673 ( AMPERSAND y=relationalExpression
674 -> ^(OPERATOR AMPERSAND ^(ARGUMENT_LIST $andExpression $y))
675 )*
676 ;
677
678
679/*
680 Note on ACSL relational expressions, from the ACSL manual:
681 The construct t1 relop1 t2 relop2 t3 · · · tk
682 with several consecutive comparison operators is a shortcut
683 (t1 relop1 t2) && (t2 relop2 t3) && ···.
684 It is required that the relopi operators must be in the same “direction”,
685 i.e. they must all belong either to {<, <=, ==} or to {>,>=,==}.
686 Expressions such as x < y > z or x != y != z are not allowed.
687
688 Also, <,<=,>=,> have higher precedence than == and !=. Though
689 not sure what that means, so ignoring it.
690
691 "a<b==c" means "a<b && b==c".
692
693 a<b<c<d : (and (a<b) (and (b<c) (c<d)))
694
695 Grammar: The following works but doesn't check for illegal expressions.
696 Better: create a new node RELCHAIN
697 args: a < b <= c < d, in order, then check and assemble in Java code.
698
699relationalExpression
700 : x=shiftExpression
701 ( r=relChain[(Tree)$x.tree] -> $r
702 | -> $x
703 )
704 ;
705
706// t is the tree of a single shiftExpression, t < y (< ...)
707relChain[Tree t]
708 : r=relOp y=shiftExpression
709 ( z=relChain[(Tree)$y.tree]
710 -> ^(OPERATOR AND ^(ARGUMENT_LIST
711 ^(OPERATOR $r ^(ARGUMENT_LIST {$t} $y))
712 $z))
713 | -> ^(OPERATOR $r ^(ARGUMENT_LIST {$t} $y))
714 )
715 ;
716*/
717
718/* A relational operator */
719relOp: EQUALS | NEQ | LT | LTE | GT | GTE ;
720
721/* A relational expression or chain of such expressions.
722 * Returns a tree with root RELCHAIN and then the sequence
723 * that alternates shiftExpression, relational operator,
724 * and begins and ends with a shiftExpression.
725 */
726relationalExpression
727 : x=shiftExpression
728 ( (s+=relOp s+=shiftExpression)+ -> ^(RELCHAIN $x $s*)
729 | -> $x
730 )
731 ;
732
733
734/* 6.5.7 *
735 * In C11:
736 * shift-expression:
737 * additive-expression
738 * shift-expression <</>> additive-expression
739 *
740 * CIVL-C extends C11 with a range-expression. see range-expression
741 * shift-expression:
742 * range-expression:
743 * shift-expression <</>> range-expression
744 */
745shiftExpression
746 : (rangeExpression -> rangeExpression)
747 ( SHIFTLEFT y=rangeExpression
748 -> ^(OPERATOR SHIFTLEFT ^(ARGUMENT_LIST $shiftExpression $y))
749 | SHIFTRIGHT y=rangeExpression
750 -> ^(OPERATOR SHIFTRIGHT ^(ARGUMENT_LIST $shiftExpression $y))
751 )*
752 ;
753
754/* 6.5.6.5 *
755 *
756 * CIVL-C range expression "lo .. hi" or "lo .. hi # step"
757 * a + b .. c + d is equivalent to (a + b) .. (c + d)
758 * (*,/,%) > (+,-) > range > shift > ...
759 */
760rangeExpression
761 : x=additiveExpression
762 ( DOTDOT s=rangeSuffix -> ^(DOTDOT $x $s)
763 | -> $x
764 )
765 ;
766
767rangeSuffix
768 : additiveExpression (HASH! additiveExpression)?
769 ;
770
771/* 6.5.6 *
772 * additive-expression:
773 * multiplicative-expression
774 * additive-expression +/- multiplicative-expression
775 */
776additiveExpression
777 : (multiplicativeExpression -> multiplicativeExpression)
778 ( PLUS y=multiplicativeExpression
779 -> ^(OPERATOR PLUS ^(ARGUMENT_LIST $additiveExpression $y))
780 | SUB y=multiplicativeExpression
781 -> ^(OPERATOR SUB ^(ARGUMENT_LIST $additiveExpression $y))
782 )*
783 ;
784
785/* 6.5.5 *
786 * In C11:
787 * multiplicative-expression:
788 * cast-expression
789 * multiplicative-expression STAR/DIV/MOD cast-expression
790 */
791multiplicativeExpression
792 : (castExpression -> castExpression)
793 ( STAR y=castExpression
794 -> ^(OPERATOR STAR ^(ARGUMENT_LIST $multiplicativeExpression $y))
795 | DIV y=castExpression
796 -> ^(OPERATOR DIV ^(ARGUMENT_LIST $multiplicativeExpression $y))
797 | MOD y=castExpression
798 -> ^(OPERATOR MOD ^(ARGUMENT_LIST $multiplicativeExpression $y))
799 )*
800 ;
801
802/* 6.5.4 *
803 * cast-expression:
804 * unary-expression
805 * (type-name) cast-expression
806 *
807 */
808// ambiguity 1: (expr) is a unary expression and looks like (typeName).
809// ambiguity 2: (typeName){...} is a compound literal and looks like cast
810castExpression
811 : (LPAREN type_expr RPAREN)=> l=LPAREN type_expr RPAREN castExpression
812 -> ^(CAST type_expr castExpression)
813 | unaryExpression
814 ;
815
816/* 6.5.3 *
817 * unary-expression:
818 * postfix-expression
819 * ++/--/sizeof unary-expression
820 * unary-operator cast-expression
821 * sizeof (type-name)
822 */
823unaryExpression
824 : postfixExpression
825 | unary_op (b=castExpression | b=quantifierExpression)
826 -> ^(OPERATOR unary_op ^(ARGUMENT_LIST $b))
827 | (SIZEOF LPAREN type_expr)=> SIZEOF LPAREN type_expr RPAREN
828 -> ^(SIZEOF_TYPE type_expr)
829 | SIZEOF unaryExpression
830 -> ^(SIZEOF_EXPR unaryExpression)
831 | union_key LPAREN argumentExpressionList RPAREN
832 -> ^(UNION_ACSL union_key argumentExpressionList RPAREN)
833 | inter_key LPAREN argumentExpressionList RPAREN
834 -> ^(INTER inter_key argumentExpressionList RPAREN)
835 | valid_key LPAREN term RPAREN
836 -> ^(VALID valid_key term RPAREN)
837 | extendedQuantification ->^(QUANTIFIED_EXT extendedQuantification)
838 | object_of_key LPAREN term RPAREN -> ^(OBJECT_OF object_of_key LPAREN term RPAREN)
839 | mpi_expression -> ^(MPI_EXPRESSION mpi_expression)
840 | old_key LPAREN term RPAREN
841 -> ^(OLD old_key term RPAREN)
842 ;
843
844extendedQuantification
845 : sum_key LPAREN term COMMA term COMMA term RPAREN
846 -> ^(SUM sum_key term+)
847 | max_key LPAREN term COMMA term COMMA term RPAREN
848 -> ^(MAX max_key term+)
849 | min_key LPAREN term COMMA term COMMA term RPAREN
850 -> ^(MIN min_key term+)
851 | product_key LPAREN term COMMA term COMMA term RPAREN
852 -> ^(PROD product_key term+)
853 | numof_key LPAREN term COMMA term COMMA term RPAREN
854 -> ^(NUMOF numof_key term+)
855 ;
856
857/* 6.5.2 *
858 * postfix-expression:
859 * primary-expression
860 * postfix-expression [expression]
861 * postfix-expression (argument-expression-list)
862 * postfix-expression . identifier
863 * postfix-expression -> identifier
864 * postfix-expression ++
865 * postfix-expression --
866 * (type-name) {initializer-list}
867 * (type-name) {initializer-list, }
868 */
869postfixExpression
870 : (primaryExpression -> primaryExpression)
871 // array index operator:
872 ( l=LSQUARE term RSQUARE
873 -> ^(OPERATOR
874 INDEX[$l]
875 ^(ARGUMENT_LIST $postfixExpression term)
876 RSQUARE)
877 | // function call:
878 LPAREN argumentExpressionList RPAREN
879 -> ^(FUNC_CALL $postfixExpression argumentExpressionList
880 )
881 | DOT IDENTIFIER
882 -> ^(DOT $postfixExpression IDENTIFIER)
883 | ARROW IDENTIFIER
884 -> ^(ARROW $postfixExpression IDENTIFIER)
885 )*
886 ;
887
888/* 6.5.2 */
889argumentExpressionList
890 : -> ^(ARGUMENT_LIST)
891 | assignmentExpression (COMMA assignmentExpression)*
892 -> ^(ARGUMENT_LIST assignmentExpression+)
893 ;
894
895/* 6.5.1 */
896primaryExpression
897 : constant
898 | IDENTIFIER
899 | STRING_LITERAL
900 | LCURLY term BITOR binders (SEMI term)? RCURLY
901 ->^(SET_BINDERS term binders term?)
902 | LCURLY term RCURLY
903 ->^(SET_SIMPLE term)
904 | LPAREN term RPAREN
905 -> ^(TERM_PARENTHESIZED term)
906 | remoteExpression
907 ;
908
909
910/* 6.5.0.1 *
911 * remote-expression:
912 * REMOTE_ACCESS ( identifier , shiftExpression ).
913 * A remote-expression should be used in the same way as a variable
914 * identifier.
915 */
916remoteExpression
917 : remote_key LPAREN a=shiftExpression COMMA b=term RPAREN
918 -> ^(REMOTE_ACCESS remote_key $a $b)
919 ;
920
921/* 6.6 */
922constantExpression
923 : conditionalExpression
924 ;
925
926constant
927 : INTEGER_CONSTANT
928 | FLOATING_CONSTANT
929 | CHARACTER_CONSTANT
930 | true_key | false_key | result_key | nothing_key | ELLIPSIS
931 | SELF | null_key
932 | mpi_constant -> ^(MPI_CONSTANT mpi_constant)
933 ;
934
935/* ACSL-MPI extensions Expressions and Constants */
936mpi_expression
937 : mpiemptyin_key LPAREN term RPAREN
938 -> ^(MPI_EMPTY_IN mpiemptyin_key term)
939 | mpiemptyout_key LPAREN term RPAREN
940 -> ^(MPI_EMPTY_OUT mpiemptyout_key term)
941 | mpiagree_key LPAREN a=term RPAREN
942 -> ^(MPI_AGREE mpiagree_key $a)
943 | mpiregion_key LPAREN a=term COMMA b=term COMMA c=term RPAREN
944 -> ^(MPI_REGION mpiregion_key $a $b $c)
945 | mpireduce_key LPAREN a=term COMMA b=term COMMA c=term COMMA d=term RPAREN
946 -> ^(MPI_REDUCE mpireduce_key $a $b $c $d)
947 | mpiequals_key LPAREN a=term COMMA b=term RPAREN
948 -> ^(MPI_EQUALS mpiequals_key $a $b)
949 | mpiextent_key LPAREN a=primaryExpression RPAREN
950 -> ^(MPI_EXTENT mpiextent_key $a)
951 | mpioffset_key LPAREN a=term COMMA b=term COMMA c=term RPAREN
952 -> ^(MPI_OFFSET mpioffset_key $a $b $c)
953 | mpivalid_key LPAREN a=term COMMA b=term COMMA c=term RPAREN
954 -> ^(MPI_VALID mpivalid_key $a $b $c)
955 | absent_key a=absent_event after_key b=absent_event until_key c=absent_event
956 -> ^(MPI_ABSENT $a $b $c)
957 ;
958
959absent_event
960: absent_event_sendto_key LPAREN a=term COMMA b=term RPAREN
961 -> ^(ABSENT_EVENT_SENDTO $a $b)
962 | absent_event_sendfrom_key LPAREN a=term COMMA b=term RPAREN
963 -> ^(ABSENT_EVENT_SENDFROM $a $b)
964 | absent_event_enter_key a=absent_event_optional_argument
965 -> ^(ABSENT_EVENT_ENTER $a)
966 | absent_event_exit_key a=absent_event_optional_argument
967 -> ^(ABSENT_EVENT_EXIT $a)
968;
969
970absent_event_optional_argument
971 : LPAREN term RPAREN
972 -> ^(TERM_PARENTHESIZED term)
973 | -> ABSENT
974 ;
975
976mpi_constant
977 : mpicommrank_key | mpicommsize_key
978 ;
979
980mpi_collective_kind
981 : col_key | p2p_key | both_key
982 ;
983
984bitimplies_op
985 : MINUSMINUS GT
986 ;
987
988bitequiv_op
989 : LT MINUSMINUS GT
990 ;
991
992unary_op
993 : PLUS | SUB | NOT | TILDE | STAR | AMPERSAND
994 ;
995
996/* rules for ACSL types */
997boolean_type
998 : {input.LT(1).getText().equals("boolean")}? IDENTIFIER
999 -> ^(BOOLEAN IDENTIFIER)
1000 ;
1001
1002integer_type
1003 : {input.LT(1).getText().equals("integer")}? IDENTIFIER
1004 -> ^(INTEGER IDENTIFIER)
1005 ;
1006
1007real_type
1008 : {input.LT(1).getText().equals("real")}? IDENTIFIER
1009 -> ^(REAL_ACSL IDENTIFIER)
1010 ;
1011
1012/* rules for ACSL contract clause keywords */
1013
1014alloc_key
1015 : {input.LT(1).getText().equals("allocates")}? IDENTIFIER
1016 ;
1017
1018assigns_key
1019 : {input.LT(1).getText().equals("assigns")}? IDENTIFIER
1020 ;
1021
1022assumes_key
1023 : {input.LT(1).getText().equals("assumes")}? IDENTIFIER
1024 ;
1025
1026assert_key
1027 : {input.LT(1).getText().equals("assert")}? IDENTIFIER
1028 ;
1029
1030behaviors_key
1031 : {input.LT(1).getText().equals("behaviors")}? IDENTIFIER
1032 ;
1033
1034behavior_key
1035 : {input.LT(1).getText().equals("behavior")}? IDENTIFIER
1036 ;
1037
1038completes_key
1039 : {input.LT(1).getText().equals("complete")}? IDENTIFIER
1040 ;
1041
1042decreases_key
1043 : {input.LT(1).getText().equals("decreases")}? IDENTIFIER
1044 ;
1045
1046disjoint_key
1047 : {input.LT(1).getText().equals("disjoint")}? IDENTIFIER
1048 ;
1049
1050ensures_key
1051 : {input.LT(1).getText().equals("ensures")}? IDENTIFIER
1052 ;
1053
1054frees_key
1055 : {input.LT(1).getText().equals("frees")}? IDENTIFIER
1056 ;
1057
1058invariant_key
1059 : {input.LT(1).getText().equals("invariant")}? IDENTIFIER
1060 ;
1061
1062loop_key
1063 : {input.LT(1).getText().equals("loop")}? IDENTIFIER
1064 ;
1065
1066requires_key
1067 : {input.LT(1).getText().equals("requires")}? IDENTIFIER
1068 ;
1069
1070terminates_key
1071 : {input.LT(1).getText().equals("terminates")}? IDENTIFIER
1072 ;
1073
1074variant_key
1075 : {input.LT(1).getText().equals("variant")}? IDENTIFIER
1076 ;
1077
1078waitsfor_key
1079 : {input.LT(1).getText().equals("waitsfor")}? IDENTIFIER
1080 ;
1081
1082predicate_key
1083 : {input.LT(1).getText().equals("predicate")}? IDENTIFIER
1084 ;
1085
1086logic_specifier_key
1087 : {input.LT(1).getText().equals("logic")}? IDENTIFIER
1088 ;
1089
1090/* ACSL terms keywords */
1091/* keywords of terms */
1092empty_key
1093 : {input.LT(1).getText().equals("\\empty")}? EXTENDED_IDENTIFIER
1094 ;
1095
1096exists_key
1097 : {input.LT(1).getText().equals("\\exists")}? EXTENDED_IDENTIFIER
1098 -> ^(EXISTS_ACSL EXTENDED_IDENTIFIER)
1099 ;
1100
1101false_key
1102 : {input.LT(1).getText().equals("\\false")}? EXTENDED_IDENTIFIER
1103 -> ^(FALSE_ACSL EXTENDED_IDENTIFIER)
1104 ;
1105
1106forall_key
1107 : {input.LT(1).getText().equals("\\forall")}? EXTENDED_IDENTIFIER
1108 -> ^(FORALL_ACSL EXTENDED_IDENTIFIER)
1109 ;
1110
1111inter_key
1112 : {input.LT(1).getText().equals("\\inter")}? EXTENDED_IDENTIFIER
1113 ;
1114
1115let_key
1116 : {input.LT(1).getText().equals("\\let")}? EXTENDED_IDENTIFIER
1117 ;
1118
1119nothing_key
1120 : {input.LT(1).getText().equals("\\nothing")}? EXTENDED_IDENTIFIER
1121 -> ^(NOTHING EXTENDED_IDENTIFIER)
1122 ;
1123
1124null_key
1125 : {input.LT(1).getText().equals("\\null")}? EXTENDED_IDENTIFIER
1126 -> ^(NULL_ACSL EXTENDED_IDENTIFIER)
1127 ;
1128
1129old_key
1130 : {input.LT(1).getText().equals("\\old")}? EXTENDED_IDENTIFIER
1131 ;
1132
1133result_key
1134 : {input.LT(1).getText().equals("\\result")}? EXTENDED_IDENTIFIER
1135 -> ^(RESULT_ACSL EXTENDED_IDENTIFIER)
1136 ;
1137
1138true_key
1139 : {input.LT(1).getText().equals("\\true")}? EXTENDED_IDENTIFIER
1140 -> ^(TRUE_ACSL EXTENDED_IDENTIFIER)
1141 ;
1142
1143union_key
1144 : {input.LT(1).getText().equals("\\union")}? EXTENDED_IDENTIFIER
1145 ;
1146
1147valid_key
1148 : {input.LT(1).getText().equals("\\valid")}? EXTENDED_IDENTIFIER
1149 ;
1150
1151with_key
1152 : {input.LT(1).getText().equals("\\with")}? EXTENDED_IDENTIFIER
1153 ;
1154
1155/* ACSL CIVL extension */
1156executeswhen_key
1157 : {input.LT(1).getText().equals("executes_when")}? IDENTIFIER
1158 ;
1159
1160pure_key
1161 : {input.LT(1).getText().equals("pure")}? IDENTIFIER
1162 -> ^(PURE IDENTIFIER)
1163 ;
1164
1165reads_key
1166 : {input.LT(1).getText().equals("reads")}? IDENTIFIER
1167 ;
1168
1169remote_key
1170 : {input.LT(1).getText().equals("\\on")}? EXTENDED_IDENTIFIER
1171 ;
1172
1173/* ACSL dependence-specification extension */
1174
1175access_key
1176 : {input.LT(1).getText().equals("\\access")}? EXTENDED_IDENTIFIER
1177// -> ^(ACCESS_ACSL EXTENDED_IDENTIFIER)
1178 ;
1179
1180anyact_key
1181 : {input.LT(1).getText().equals("\\anyact")}? EXTENDED_IDENTIFIER
1182 -> ^(ANYACT EXTENDED_IDENTIFIER)
1183 ;
1184
1185
1186call_key
1187 : {input.LT(1).getText().equals("\\call")}? EXTENDED_IDENTIFIER
1188 ;
1189
1190dependson_key
1191 : {input.LT(1).getText().equals("depends_on")}? IDENTIFIER
1192 ;
1193
1194object_of_key
1195 : {input.LT(1).getText().equals("\\object_of")}? EXTENDED_IDENTIFIER
1196 ;
1197
1198read_key
1199 : {input.LT(1).getText().equals("\\read")}? EXTENDED_IDENTIFIER
1200// -> ^(READ_ACSL EXTENDED_IDENTIFIER)
1201 ;
1202
1203region_of_key
1204 : {input.LT(1).getText().equals("\\region_of")}? EXTENDED_IDENTIFIER
1205 ;
1206
1207write_key
1208 : {input.LT(1).getText().equals("\\write")}? EXTENDED_IDENTIFIER
1209// -> ^(WRITE_ACSL EXTENDED_IDENTIFIER)
1210 ;
1211
1212/* ACSL MPI-extension keywords */
1213
1214both_key
1215 : {input.LT(1).getText().equals("BOTH")}? IDENTIFIER
1216 -> ^(BOTH IDENTIFIER)
1217 ;
1218
1219col_key
1220 : {input.LT(1).getText().equals("COL")}? IDENTIFIER
1221 -> ^(COL IDENTIFIER)
1222 ;
1223
1224p2p_key
1225 : {input.LT(1).getText().equals("P2P")}? IDENTIFIER
1226 -> ^(P2P IDENTIFIER)
1227 ;
1228
1229mpiagree_key
1230 : {input.LT(1).getText().equals("\\mpi_agree")}? EXTENDED_IDENTIFIER
1231// -> ^(MPI_AGREE EXTENDED_IDENTIFIER)
1232 ;
1233
1234mpicollective_key
1235 : {input.LT(1).getText().equals("\\mpi_collective")}? EXTENDED_IDENTIFIER
1236// -> ^(MPI_COLLECTIVE EXTENDED_IDENTIFIER)
1237 ;
1238
1239mpicommsize_key
1240 : {input.LT(1).getText().equals("\\mpi_comm_size")}? EXTENDED_IDENTIFIER
1241 -> ^(MPI_COMM_SIZE EXTENDED_IDENTIFIER)
1242 ;
1243
1244mpicommrank_key
1245 : {input.LT(1).getText().equals("\\mpi_comm_rank")}? EXTENDED_IDENTIFIER
1246 -> ^(MPI_COMM_RANK EXTENDED_IDENTIFIER)
1247 ;
1248
1249mpiemptyin_key
1250 : {input.LT(1).getText().equals("\\mpi_empty_in")}? EXTENDED_IDENTIFIER
1251// -> ^(MPI_EMPTY_IN EXTENDED_IDENTIFIER)
1252 ;
1253
1254mpiemptyout_key
1255 : {input.LT(1).getText().equals("\\mpi_empty_out")}? EXTENDED_IDENTIFIER
1256// -> ^(MPI_EMPTY_OUT EXTENDED_IDENTIFIER)
1257 ;
1258
1259mpiequals_key
1260 : {input.LT(1).getText().equals("\\mpi_equals")}? EXTENDED_IDENTIFIER
1261// -> ^(MPI_EQUALS EXTENDED_IDENTIFIER)
1262 ;
1263
1264mpiextent_key
1265 : {input.LT(1).getText().equals("\\mpi_extent")}? EXTENDED_IDENTIFIER
1266// -> ^(MPI_EXTENT EXTENDED_IDENTIFIER)
1267 ;
1268
1269mpioffset_key
1270 : {input.LT(1).getText().equals("\\mpi_offset")}? EXTENDED_IDENTIFIER
1271// -> ^(MPI_OFFSET EXTENDED_IDENTIFIER)
1272 ;
1273
1274mpivalid_key
1275 : {input.LT(1).getText().equals("\\mpi_valid")}? EXTENDED_IDENTIFIER
1276 ;
1277
1278mpiregion_key
1279 : {input.LT(1).getText().equals("\\mpi_region")}? EXTENDED_IDENTIFIER
1280 ;
1281
1282mpireduce_key
1283 : {input.LT(1).getText().equals("\\mpi_reduce")}? EXTENDED_IDENTIFIER
1284 ;
1285
1286absent_key
1287 : {input.LT(1).getText().equals("\\absentof")}? EXTENDED_IDENTIFIER
1288 ;
1289
1290after_key
1291 : {input.LT(1).getText().equals("\\after")}? EXTENDED_IDENTIFIER
1292 ;
1293
1294until_key
1295 : {input.LT(1).getText().equals("\\until")}? EXTENDED_IDENTIFIER
1296 ;
1297
1298absent_event_sendto_key
1299 : {input.LT(1).getText().equals("\\sendto")}? EXTENDED_IDENTIFIER
1300 ;
1301
1302absent_event_sendfrom_key
1303 : {input.LT(1).getText().equals("\\sendfrom")}? EXTENDED_IDENTIFIER
1304 ;
1305
1306absent_event_enter_key
1307 : {input.LT(1).getText().equals("\\enter")}? EXTENDED_IDENTIFIER
1308 ;
1309
1310absent_event_exit_key
1311 : {input.LT(1).getText().equals("\\exit")}? EXTENDED_IDENTIFIER
1312 ;
1313
1314/** ACSL higher-order keywords */
1315lambda_key
1316 : {input.LT(1).getText().equals("\\lambda")}? EXTENDED_IDENTIFIER
1317 ;
1318
1319sum_key
1320 : {input.LT(1).getText().equals("\\sum")}? EXTENDED_IDENTIFIER
1321 ;
1322
1323max_key
1324 : {input.LT(1).getText().equals("\\max")}? EXTENDED_IDENTIFIER
1325 ;
1326
1327min_key
1328 : {input.LT(1).getText().equals("\\min")}? EXTENDED_IDENTIFIER
1329 ;
1330
1331product_key
1332 : {input.LT(1).getText().equals("\\product")}? EXTENDED_IDENTIFIER
1333 ;
1334
1335numof_key
1336 : {input.LT(1).getText().equals("\\numof")}? EXTENDED_IDENTIFIER
1337 ;
Note: See TracBrowser for help on using the repository browser.