6de3880a3f33ca5904d88a389df83e432477d0dd
[repair.git] / Repair / RepairCompiler / MCC / CDL.cup
1 package MCC;
2 import MCC.IR.ParseNode;
3 import MCC.IR.ParseNodeVector;
4 import java.util.*;
5
6 action code {:
7
8         public static boolean errors;
9         public static boolean debug;
10
11         // debugMessage: writes debug production message only if debug = true
12
13         void debugMessage (String production) {
14                 if (debug) {
15                         System.out.println("Applying production: " + production);
16                 }
17         }
18
19         String unescape (String str) {
20             StringBuffer sb = new StringBuffer();
21             int i;
22             // Note that we skip the first and last characters (they're "'s)
23             for (i = 1; i < str.length() - 1; i++) {
24                 if (str.charAt(i) == '\\') {
25                     i++;
26                     switch (str.charAt(i)) {
27                     case '\"':
28                         sb.append('\"');
29                         break;
30                     case '\'':
31                         sb.append('\'');
32                         break;
33                     case '\\':
34                         sb.append('\\');
35                         break;
36                     case 't':
37                         sb.append('\t');
38                         break;
39                     case 'n':
40                         sb.append('\n');
41                         break;
42                     default:
43                         System.err.print("Error in string literal: ");
44                         System.err.println(str.charAt(i));
45                         System.err.println("Aborting...");
46                         break;
47                     }
48                 } else {
49                     sb.append(str.charAt(i));
50                 }
51             }
52             return sb.toString();
53         }
54 :}
55
56 init with {: :}
57
58 parser code {:
59
60         public String filename;
61        
62         public void syntax_error (java_cup.runtime.Symbol current) {
63
64                 CUP$CDLParser$actions.errors = true;
65                 Symbol symbol = (Symbol) current;
66
67                 boolean isInteger = true;
68                 try{ 
69                    Integer.parseInt(current.value.toString());
70                 } catch(NumberFormatException e) { isInteger = false;}
71
72                 report_error(filename+":"+(symbol.line+1)+": Syntax error at column " 
73                 + (LineCount.getColumn(symbol.left)+1) +": " + current.value, current);
74
75                 /*
76                 if (current.value.equals("true") || isInteger)
77                    System.out.println("Did you mean literal("+current.value+")?");
78                 */
79
80                 System.out.println();
81                 System.exit(0);
82         }
83
84         public void report_fatal_error (String message, Object info) {
85                 
86                  done_parsing();
87                  report_error(message, info);
88                  CUP$CDLParser$actions.errors = true;
89         }
90
91         public int curPos () {
92                 return cur_token.left;
93         }
94
95         public int curLine (int back) {
96                 Stack st = new Stack();
97                 int i;
98
99                 for (i = 0; i < back; i++) {
100                         st.push(stack.pop());
101                 }
102
103                 java_cup.runtime.Symbol s;
104                 s = (java_cup.runtime.Symbol) st.peek();
105
106                 for (i = 0; i < back; i++) {
107                         stack.push(st.pop());
108                 }
109
110                 return LineCount.getLine(s.left);
111         }
112         
113 :}
114
115 // TERMINALS /////////////////////////////////////////////////////////////
116
117     terminal BAD;
118
119     terminal String ID;
120     terminal String DECIMAL;
121     terminal String CHAR;
122     terminal String STRING;
123
124     terminal OPENBRACE;
125     terminal CLOSEBRACE;
126     terminal OPENPAREN;
127     terminal CLOSEPAREN; 
128     terminal OPENBRACKET;
129     terminal CLOSEBRACKET;
130
131     terminal ADD; 
132     terminal SUB; 
133     terminal MULT; 
134     terminal DIV;
135     terminal SUM;
136
137     terminal NOT;
138     terminal LT;
139     terminal GT;
140     terminal LE;
141     terminal GE;
142     terminal EQ;
143     terminal NE;
144
145     terminal FORALL;
146     terminal IN;
147     terminal INTEST;
148
149     terminal COMMA;
150     terminal SIZEOF;
151
152     terminal DOT;
153     terminal DOTINV;
154
155     terminal AND;
156     terminal OR;
157
158     terminal LITERAL;
159
160     terminal IMPLIES;
161     terminal TRUE;
162     terminal FALSE;
163     terminal ISVALID;
164     terminal FOR;
165     terminal TO;
166     terminal CAST;
167
168     terminal PARAM;
169     terminal STRUCTURE;
170     terminal RESERVED;
171     terminal BIT;
172     terminal BYTE;
173     terminal SHORT;
174       
175     terminal LABEL;
176     terminal INT;
177     terminal SUBTYPE;
178     terminal SUBCLASS;
179     terminal OF;
180
181     terminal SEMICOLON;
182     terminal COLON;
183
184     terminal SET;
185     terminal ARROW;
186     terminal MANY;
187     terminal BAR;
188
189     terminal PARTITION;
190     terminal ELEMENT;
191     terminal DELAY;
192     terminal STATIC;
193
194     terminal NULL;
195     terminal CRASH;
196
197 // NON-TERMINALS /////////////////////////////////////////////////////////
198
199 /*
200                 TYPE                    NAME
201 ------------------------------------------------------------------------*/
202 nonterminal     ParseNode               constraints;
203 nonterminal     ParseNode               constraint;
204 nonterminal     ParseNode               optcrash;
205 nonterminal     ParseNode               quantifiers;
206 nonterminal     ParseNode               quantifier;
207 nonterminal     ParseNode               set;
208 nonterminal     ParseNode               listofliterals;
209 nonterminal     ParseNode               literal;
210 nonterminal     ParseNode               body;
211 nonterminal     ParseNode               predicate;
212 nonterminal     ParseNode               setexpr;
213
214 nonterminal     ParseNode               compare;
215 nonterminal     ParseNode               expr;
216 nonterminal     ParseNode               addsuboperator;
217 nonterminal     ParseNode               multdivoperator;
218
219
220
221 precedence left OR;
222 precedence left AND;
223 precedence left EQ, NE; 
224 precedence left LT, LE, GE, GT;
225
226 precedence left ADD, SUB;
227 precedence left MULT, DIV;
228
229 precedence left NOT;
230
231 precedence left DOT, DOTINV;
232
233 // PRODUCTION RULES  /////////////////////////////////////////////////////
234
235 constraints ::=
236             
237         constraints:constraints constraint:constraint
238         {:
239         debugMessage(PRODSTRING);
240         constraints.addChild(constraint);
241         RESULT = constraints;
242         :}
243         
244         | constraint:constraint
245         {:
246         debugMessage(PRODSTRING);
247         ParseNode constraints = new ParseNode("constraints", parser.curLine(1));
248         constraints.addChild(constraint);
249         RESULT = constraints;
250         :}
251         ;
252
253 constraint ::=
254             
255         optcrash:crash OPENBRACKET quantifiers:quantifiers CLOSEBRACKET COMMA body:body SEMICOLON
256         {:
257         debugMessage(PRODSTRING);
258         ParseNode constraint = new ParseNode("constraint", parser.curLine(7));
259         if (crash != null) {
260                 constraint.addChild(crash);
261         }
262         if (quantifiers != null) {
263                 constraint.addChild(quantifiers);
264         }
265         constraint.addChild(body);
266         RESULT = constraint;
267         :}
268         ;
269
270 optcrash ::=
271
272          CRASH
273          {:
274          debugMessage(PRODSTRING);
275          RESULT = new ParseNode("crash", parser.curLine(1));
276          :}
277
278          | /* nothing */
279          {:
280          debugMessage(PRODSTRING);
281          RESULT = null;
282          :}
283          ;
284
285 quantifiers ::=
286             
287         quantifiers:quantifiers COMMA quantifier:quantifier
288         {:
289         debugMessage(PRODSTRING);
290         quantifiers.addChild(quantifier);
291         RESULT = quantifiers;
292         :}
293             
294         | quantifier:quantifier
295         {:
296         debugMessage(PRODSTRING);
297         ParseNode quantifiers = new ParseNode("quantifiers", parser.curLine(1));
298         quantifiers.addChild(quantifier);
299         RESULT = quantifiers;
300         :}
301             
302         | 
303         {:
304         debugMessage(PRODSTRING);
305         RESULT = null;
306         :}
307         ;       
308
309 quantifier ::= 
310            
311         FORALL ID:var IN set:set
312         {:
313         debugMessage(PRODSTRING);
314         ParseNode q = new ParseNode("quantifier", parser.curLine(4));
315         q.addChild("forall", parser.curLine(4));
316         q.addChild("var", parser.curLine(3)).addChild(var);
317         q.addChild(set);
318         RESULT = q;
319         :}
320         | FORALL LT ID:r1 COMMA ID:r2 GT IN ID:relation
321         {:
322         debugMessage(PRODSTRING);
323         ParseNode q = new ParseNode("quantifier", parser.curLine(7));
324         q.addChild("relation", parser.curLine(1)).addChild(relation);
325         q.addChild("left", parser.curLine(5)).addChild(r1);
326         q.addChild("right", parser.curLine(3)).addChild(r2);
327         RESULT = q;
328         :}
329         ;
330
331 set ::=
332     
333         ID:setname
334         {:
335         debugMessage(PRODSTRING);
336         ParseNode set = new ParseNode("set", parser.curLine(1));
337         set.addChild("name").addChild(setname);
338         RESULT = set;
339         :}
340
341         | OPENBRACE listofliterals:list CLOSEBRACE
342         {:
343         debugMessage(PRODSTRING);
344         ParseNode set = new ParseNode("set", parser.curLine(3));
345         set.addChild(list);
346         RESULT = set;
347         :}
348         ;
349     
350 listofliterals ::=
351                
352         listofliterals:list COMMA literal:literal
353         {:
354         debugMessage(PRODSTRING);
355         list.addChild(literal);
356         RESULT = list;
357         :}
358                
359         | literal:literal
360         {: 
361         debugMessage(PRODSTRING);
362         ParseNode list = new ParseNode("listofliterals", parser.curLine(1));
363         list.addChild(literal);
364         RESULT = list;
365         :}
366         ;
367
368 body ::=
369
370         body:body1 AND body:body2
371         {:
372         debugMessage(PRODSTRING);
373         ParseNode body = new ParseNode("body", parser.curLine(3));
374         body.addChild("and").addChild("left", parser.curLine(3)).addChild(body1);
375         body.getChild("and").addChild("right", parser.curLine(1)).addChild(body2);
376         RESULT = body;
377         :}
378      
379         | body:body1 OR body:body2
380         {:
381         debugMessage(PRODSTRING);
382         ParseNode body = new ParseNode("body", parser.curLine(3));
383         body.addChild("or").addChild("left", parser.curLine(3)).addChild(body1);
384         body.getChild("or").addChild("right", parser.curLine(1)).addChild(body2);
385         RESULT = body;
386         :}
387      
388         | NOT body:body1
389         {:
390         debugMessage(PRODSTRING);
391         ParseNode body = new ParseNode("body", parser.curLine(2));
392         body.addChild("not").addChild(body1);
393         RESULT = body;
394         :}
395      
396         | OPENPAREN body:body CLOSEPAREN
397         {:
398         debugMessage(PRODSTRING);
399         RESULT = body;
400         :}
401      
402         | predicate:predicate
403         {:
404         debugMessage(PRODSTRING);
405         ParseNode body = new ParseNode("body", parser.curLine(1));
406         body.addChild(predicate);
407         RESULT = body;
408         :}
409         ;
410
411 predicate ::=
412
413         expr:expr IN setexpr:setexpr
414         {:
415         debugMessage(PRODSTRING);
416         ParseNode inclusion = (new ParseNode("predicate", parser.curLine(3))).addChild("inclusion");
417         inclusion.addChild(expr);
418         inclusion.addChild(setexpr);
419         RESULT = inclusion.getRoot();
420         :}
421      
422         | expr:lexpr compare:compare expr:rexpr
423         {:
424         debugMessage(PRODSTRING);
425         ParseNode comparison = (new ParseNode("predicate", parser.curLine(3))).addChild("expr").addChild("operator");
426         comparison.addChild("op").addChild(compare);
427         comparison.addChild("left", parser.curLine(2)).addChild(lexpr);
428         comparison.addChild("right", parser.curLine(2)).addChild(rexpr);
429         RESULT = comparison.getRoot();
430         :}
431
432         ;
433
434 setexpr ::=
435         
436         ID:setname
437         {:
438         debugMessage(PRODSTRING);
439         ParseNode set = new ParseNode("setexpr", parser.curLine(1));
440         set.addChild("set").addChild(setname);
441         RESULT = set;
442         :}
443
444         | ID:var DOT ID:relation
445         {:
446         debugMessage(PRODSTRING);
447         ParseNode set = new ParseNode("setexpr", parser.curLine(3));
448         set.addChild("dot").addChild("quantifiervar", parser.curLine(3)).addChild(var);
449         set.getChild("dot").addChild("relation", parser.curLine(1)).addChild(relation);
450         RESULT = set;
451         :}
452
453         | ID:var DOTINV ID:relation
454         {:
455         debugMessage(PRODSTRING);
456         ParseNode set = new ParseNode("setexpr", parser.curLine(3));
457         set.addChild("dotinv").addChild("quantifiervar", parser.curLine(3)).addChild(var);
458         set.getChild("dotinv").addChild("relation", parser.curLine(1)).addChild(relation);
459         RESULT = set;
460         :}
461
462         | setexpr:setexpr DOT ID:relation
463         {:
464         debugMessage(PRODSTRING);
465         ParseNode set = new ParseNode("setexpr", parser.curLine(3));
466         set.addChild("dotset").addChild(setexpr);
467         set.getChild("dotset").addChild("relation", parser.curLine(1)).addChild(relation);
468         RESULT = set;
469         :}
470
471         | setexpr:setexpr DOTINV ID:relation
472         {:
473         debugMessage(PRODSTRING);
474         ParseNode set = new ParseNode("setexpr", parser.curLine(3));
475         set.addChild("dotinvset").addChild(setexpr);
476         set.getChild("dotinvset").addChild("relation", parser.curLine(1)).addChild(relation);
477         RESULT = set;
478         :}
479         ;
480         
481 expr ::=
482
483         SUM OPENPAREN ID:set DOT ID:relation CLOSEPAREN
484         {:
485         debugMessage(PRODSTRING);
486         ParseNode expr = new ParseNode("expr", parser.curLine(1));      
487         expr.addChild("sumexpr", parser.curLine(3));
488         expr.getChild("sumexpr").addChild("dot").addChild("set", parser.curLine(3)).addChild(set);
489         expr.getChild("sumexpr").getChild("dot").addChild("relation", parser.curLine(1)).addChild(relation);
490         RESULT = expr;
491         :}
492
493         | ID:var
494         {:
495         debugMessage(PRODSTRING);
496         ParseNode expr = new ParseNode("expr", parser.curLine(1));      
497         expr.addChild("var").addChild(var);
498         RESULT = expr;
499         :}
500         
501         | OPENPAREN expr:expr CLOSEPAREN 
502         {:
503         debugMessage(PRODSTRING);
504         RESULT = expr;
505         :}     
506         
507         | literal:literal
508         {:
509         debugMessage(PRODSTRING);
510         ParseNode expr = new ParseNode("expr", parser.curLine(4));
511         expr.addChild(literal);
512         RESULT = expr;
513         :}
514         
515         | expr:expr DOT ID:relname
516         {:
517         debugMessage(PRODSTRING);
518         ParseNode relation = (new ParseNode("expr", parser.curLine(3))).addChild("relation");
519         relation.addChild(expr);
520         relation.addChild("name").addChild(relname);
521         RESULT = relation.getRoot();
522         :}
523         
524         | expr:expr DOTINV ID:relname
525         {:
526         debugMessage(PRODSTRING);
527         ParseNode relation = (new ParseNode("expr", parser.curLine(3))).addChild("relation");
528         relation.addChild(expr);
529         relation.addChild("name").addChild(relname);
530         relation.addChild("inv");
531         RESULT = relation.getRoot();
532         :}
533              
534         | expr:expr1 addsuboperator:operator expr:expr2
535         {:
536         debugMessage(PRODSTRING);
537         ParseNode op = (new ParseNode("expr", parser.curLine(3))).addChild("operator");
538         op.addChild("op").addChild(operator);
539         op.addChild("left", parser.curLine(3)).addChild(expr1);
540         op.addChild("right", parser.curLine(1)).addChild(expr2);
541         RESULT = op.getRoot();
542         :}
543         %prec ADD
544         | expr:expr1 multdivoperator:operator expr:expr2
545         {:
546         debugMessage(PRODSTRING);
547         ParseNode op = (new ParseNode("expr", parser.curLine(3))).addChild("operator");
548         op.addChild("op").addChild(operator);
549         op.addChild("left", parser.curLine(3)).addChild(expr1);
550         op.addChild("right", parser.curLine(1)).addChild(expr2);
551         RESULT = op.getRoot();
552         :}
553         %prec MULT
554         | SIZEOF OPENPAREN setexpr:setexpr CLOSEPAREN
555         {:
556         ParseNode sizeof = (new ParseNode("expr", parser.curLine(4))).addChild("sizeof");
557         sizeof.addChild(setexpr);
558         RESULT = sizeof.getRoot();
559         :}
560         ;
561
562 addsuboperator ::=
563           
564         ADD 
565         {:
566         debugMessage(PRODSTRING);
567         RESULT = new ParseNode("add", parser.curLine(1));
568         :}
569           
570         | SUB
571         {:
572         debugMessage(PRODSTRING);
573         RESULT = new ParseNode("sub", parser.curLine(1));
574         :}
575         ;
576 multdivoperator ::=
577         MULT
578         {:
579         debugMessage(PRODSTRING);
580         RESULT = new ParseNode("mult", parser.curLine(1));
581         :}
582         | DIV
583         {:
584         debugMessage(PRODSTRING);
585         RESULT = new ParseNode("div", parser.curLine(1));
586         :}
587         ;
588
589 compare ::= 
590
591         LT
592         {:
593         debugMessage(PRODSTRING);
594         RESULT = new ParseNode("lt", parser.curLine(1));
595         :}
596
597         | GT
598         {:
599         debugMessage(PRODSTRING);
600         RESULT = new ParseNode("gt", parser.curLine(1));
601         :}
602
603         | LE
604         {:
605         debugMessage(PRODSTRING);
606         RESULT = new ParseNode("le", parser.curLine(1));
607         :}
608
609         | GE
610         {:
611         debugMessage(PRODSTRING);
612         RESULT = new ParseNode("ge", parser.curLine(1));
613         :}
614
615         | EQ
616         {:
617         debugMessage(PRODSTRING);
618         RESULT = new ParseNode("eq", parser.curLine(1));
619         :}
620
621         | NE
622         {:
623         debugMessage(PRODSTRING);
624         RESULT = new ParseNode("ne", parser.curLine(1));
625         :}
626         ;
627         
628 literal ::=
629          
630         TRUE
631         {:
632         debugMessage(PRODSTRING);
633         RESULT = (new ParseNode("literal", parser.curLine(1))).addChild("boolean").addChild("true").getRoot();
634         :}
635          
636         | FALSE
637         {:
638         debugMessage(PRODSTRING);
639         RESULT = (new ParseNode("literal", parser.curLine(1))).addChild("boolean").addChild("false").getRoot();
640         :}
641
642         | NULL
643         {:
644         debugMessage(PRODSTRING);
645         RESULT = (new ParseNode("literal", parser.curLine(1))).addChild("decimal").addChild("0").getRoot();
646         :}
647          
648         | DECIMAL:dec
649         {:
650         debugMessage(PRODSTRING);
651         RESULT = (new ParseNode("literal", parser.curLine(1))).addChild("decimal").addChild(dec).getRoot();
652         :}
653
654         | SUB DECIMAL:dec
655         {:
656         debugMessage(PRODSTRING);
657         RESULT = (new ParseNode("literal", parser.curLine(1))).addChild("decimal").addChild("-"+dec).getRoot();
658         :}
659          
660         | STRING:str
661         {:
662         debugMessage(PRODSTRING);
663         RESULT = (new ParseNode("literal", parser.curLine(1))).addChild("string").addChild(str).getRoot();
664         :}
665          
666         | CHAR:chr
667         {:
668         debugMessage(PRODSTRING);
669         RESULT = (new ParseNode("literal", parser.curLine(1))).addChild("char").addChild(chr).getRoot();
670         :}
671          
672         | LITERAL OPENPAREN ID:literal CLOSEPAREN
673         {:
674         debugMessage(PRODSTRING);
675         RESULT = (new ParseNode("literal", parser.curLine(1))).addChild("token").addChild(literal).getRoot();
676         :}
677         ;