fixed problems with CDL.cup
[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 void syntax_error (java_cup.runtime.Symbol current) {
61
62                 CUP$CDLParser$actions.errors = true;
63                 Symbol symbol = (Symbol) current;
64                 report_error("CDL: Syntax error at line " + (symbol.line + 1)
65                 + ", column " + LineCount.getColumn(symbol.left) + ": " + current.value, current);
66         }
67
68         public void report_fatal_error (String message, Object info) {
69                 
70                  done_parsing();
71                  report_error(message, info);
72                  CUP$CDLParser$actions.errors = true;
73         }
74
75         public int curPos () {
76                 return cur_token.left;
77         }
78
79         public int curLine (int back) {
80                 Stack st = new Stack();
81                 int i;
82
83                 for (i = 0; i < back; i++) {
84                         st.push(stack.pop());
85                 }
86
87                 java_cup.runtime.Symbol s;
88                 s = (java_cup.runtime.Symbol) st.peek();
89
90                 for (i = 0; i < back; i++) {
91                         stack.push(st.pop());
92                 }
93
94                 return LineCount.getLine(s.left);
95         }
96         
97 :}
98
99 // TERMINALS /////////////////////////////////////////////////////////////
100
101     terminal BAD;
102
103     terminal String ID;
104     terminal String DECIMAL;
105     terminal String CHAR;
106     terminal String STRING;
107
108     terminal OPENBRACE;
109     terminal CLOSEBRACE;
110     terminal OPENPAREN;
111     terminal CLOSEPAREN; 
112     terminal OPENBRACKET;
113     terminal CLOSEBRACKET;
114
115     terminal ADD; 
116     terminal SUB; 
117     terminal MULT; 
118     terminal DIV;
119
120     terminal NOT;
121     terminal LT;
122     terminal GT;
123     terminal LE;
124     terminal GE;
125     terminal EQ;
126     terminal NE;
127
128
129     terminal FORALL;
130     terminal IN;
131     terminal INTEST;
132
133     terminal COMMA;
134     terminal SIZEOF;
135
136     terminal DOT;
137     terminal DOTINV;
138
139     terminal AND;
140     terminal OR;
141
142     terminal LITERAL;
143
144     terminal IMPLIES;
145     terminal TRUE;
146     terminal ISVALID;
147     terminal FOR;
148     terminal TO;
149     terminal CAST;
150
151     terminal PARAM;
152     terminal STRUCTURE;
153     terminal RESERVED;
154     terminal BIT;
155     terminal BYTE;
156     terminal SHORT;
157       
158     terminal LABEL;
159     terminal INT;
160     terminal SUBTYPE;
161     terminal OF;
162
163     terminal SEMICOLON;
164     terminal COLON;
165
166     terminal SET;
167     terminal ARROW;
168     terminal MANY;
169     terminal BAR;
170
171     terminal PARTITION;
172     terminal ELEMENT;
173     terminal DELAY;
174     terminal STATIC;
175
176     terminal NULL;
177     terminal CRASH;
178
179 // NON-TERMINALS /////////////////////////////////////////////////////////
180
181 /*
182                 TYPE                    NAME
183 ------------------------------------------------------------------------*/
184 nonterminal     ParseNode               constraints;
185 nonterminal     ParseNode               constraint;
186 nonterminal     ParseNode               optcrash;
187 nonterminal     ParseNode               quantifiers;
188 nonterminal     ParseNode               quantifier;
189 nonterminal     ParseNode               set;
190 nonterminal     ParseNode               listofliterals;
191 nonterminal     ParseNode               literal;
192 nonterminal     ParseNode               body;
193 nonterminal     ParseNode               predicate;
194 nonterminal     ParseNode               setexpr;
195
196 nonterminal     ParseNode               compare;
197 nonterminal     ParseNode               expr;
198 nonterminal     ParseNode               operator;
199
200
201
202 precedence left OR;
203 precedence left AND;
204 precedence right EQ, NE; 
205 precedence right LT, LE, GE, GT;
206 precedence left ADD, SUB;
207 precedence left MULT, DIV;
208 precedence left NOT;
209 precedence left DOT, DOTINV;
210
211 // PRODUCTION RULES  /////////////////////////////////////////////////////
212
213 constraints ::=
214             
215         constraints:constraints constraint:constraint
216         {:
217         debugMessage(PRODSTRING);
218         constraints.addChild(constraint);
219         RESULT = constraints;
220         :}
221         
222         | constraint:constraint
223         {:
224         debugMessage(PRODSTRING);
225         ParseNode constraints = new ParseNode("constraints", parser.curLine(1));
226         constraints.addChild(constraint);
227         RESULT = constraints;
228         :}
229         ;
230
231 constraint ::=
232             
233         optcrash:crash OPENBRACKET quantifiers:quantifiers CLOSEBRACKET COMMA body:body SEMICOLON
234         {:
235         debugMessage(PRODSTRING);
236         ParseNode constraint = new ParseNode("constraint", parser.curLine(7));
237         if (crash != null) {
238                 constraint.addChild(crash);
239         }
240         if (quantifiers != null) {
241                 constraint.addChild(quantifiers);
242         }
243         constraint.addChild(body);
244         RESULT = constraint;
245         :}
246         ;
247
248 optcrash ::=
249
250          CRASH
251          {:
252          debugMessage(PRODSTRING);
253          RESULT = new ParseNode("crash", parser.curLine(1));
254          :}
255
256          | /* nothing */
257          {:
258          debugMessage(PRODSTRING);
259          RESULT = null;
260          :}
261          ;
262
263 quantifiers ::=
264             
265         quantifiers:quantifiers COMMA quantifier:quantifier
266         {:
267         debugMessage(PRODSTRING);
268         quantifiers.addChild(quantifier);
269         RESULT = quantifiers;
270         :}
271             
272         | quantifier:quantifier
273         {:
274         debugMessage(PRODSTRING);
275         ParseNode quantifiers = new ParseNode("quantifiers", parser.curLine(1));
276         quantifiers.addChild(quantifier);
277         RESULT = quantifiers;
278         :}
279             
280         | 
281         {:
282         debugMessage(PRODSTRING);
283         RESULT = null;
284         :}
285         ;       
286
287 quantifier ::= 
288            
289         FORALL ID:var IN set:set
290         {:
291         debugMessage(PRODSTRING);
292         ParseNode q = new ParseNode("quantifier", parser.curLine(4));
293         q.addChild("forall", parser.curLine(4));
294         q.addChild("var", parser.curLine(3)).addChild(var);
295         q.addChild(set);
296         RESULT = q;
297         :}
298         ;
299
300 set ::=
301     
302         ID:setname
303         {:
304         debugMessage(PRODSTRING);
305         ParseNode set = new ParseNode("set", parser.curLine(1));
306         set.addChild("name").addChild(setname);
307         RESULT = set;
308         :}
309
310         | OPENBRACE listofliterals:list CLOSEBRACE
311         {:
312         debugMessage(PRODSTRING);
313         ParseNode set = new ParseNode("set", parser.curLine(3));
314         set.addChild(list);
315         RESULT = set;
316         :}
317         ;
318     
319 listofliterals ::=
320                
321         listofliterals:list COMMA literal:literal
322         {:
323         debugMessage(PRODSTRING);
324         list.addChild(literal);
325         RESULT = list;
326         :}
327                
328         | literal:literal
329         {: 
330         debugMessage(PRODSTRING);
331         ParseNode list = new ParseNode("listofliterals", parser.curLine(1));
332         list.addChild(literal);
333         RESULT = list;
334         :}
335         ;
336
337 body ::=
338
339         body:body1 AND body:body2
340         {:
341         debugMessage(PRODSTRING);
342         ParseNode body = new ParseNode("body", parser.curLine(3));
343         body.addChild("and").addChild("left", parser.curLine(3)).addChild(body1);
344         body.getChild("and").addChild("right", parser.curLine(1)).addChild(body2);
345         RESULT = body;
346         :}
347      
348         | body:body1 OR body:body2
349         {:
350         debugMessage(PRODSTRING);
351         ParseNode body = new ParseNode("body", parser.curLine(3));
352         body.addChild("or").addChild("left", parser.curLine(3)).addChild(body1);
353         body.getChild("or").addChild("right", parser.curLine(1)).addChild(body2);
354         RESULT = body;
355         :}
356      
357         | NOT body:body1
358         {:
359         debugMessage(PRODSTRING);
360         ParseNode body = new ParseNode("body", parser.curLine(2));
361         body.addChild("not").addChild(body1);
362         RESULT = body;
363         :}
364      
365         | OPENPAREN body:body CLOSEPAREN
366         {:
367         debugMessage(PRODSTRING);
368         RESULT = body;
369         :}
370      
371         | predicate:predicate
372         {:
373         debugMessage(PRODSTRING);
374         ParseNode body = new ParseNode("body", parser.curLine(1));
375         body.addChild(predicate);
376         RESULT = body;
377         :}
378         ;
379
380 predicate ::=
381
382         ID:var IN setexpr:setexpr
383         {:
384         debugMessage(PRODSTRING);
385         ParseNode inclusion = (new ParseNode("predicate", parser.curLine(3))).addChild("inclusion");
386         inclusion.addChild("quantifiervar", parser.curLine(3)).addChild(var);
387         inclusion.addChild(setexpr);
388         RESULT = inclusion.getRoot();
389         :}
390      
391         | SIZEOF OPENPAREN setexpr:setexpr CLOSEPAREN compare:compare DECIMAL:dec
392         {:
393         ParseNode sizeof = (new ParseNode("predicate", parser.curLine(4))).addChild("sizeof");
394         sizeof.addChild(setexpr);
395         sizeof.addChild("compare", parser.curLine(2)).addChild(compare);
396         sizeof.addChild("decimal", parser.curLine(1)).addChild(dec);
397         RESULT = sizeof.getRoot();
398         :}
399
400         | ID:var DOT ID:relation compare:compare expr:expr
401         {:
402         debugMessage(PRODSTRING);
403         ParseNode comparison = (new ParseNode("predicate", parser.curLine(3))).addChild("comparison");
404         comparison.addChild("compare", parser.curLine(2)).addChild(compare);
405         comparison.addChild("relation", parser.curLine(3)).addChild(relation);
406         comparison.addChild("quantifier", parser.curLine(5)).addChild(var);
407         comparison.addChild(expr);
408         RESULT = comparison.getRoot();
409         :}
410         ;
411
412 setexpr ::=
413         
414         ID:setname
415         {:
416         debugMessage(PRODSTRING);
417         ParseNode set = new ParseNode("setexpr", parser.curLine(1));
418         set.addChild("set").addChild(setname);
419         RESULT = set;
420         :}
421
422         | ID:var DOT ID:relation
423         {:
424         debugMessage(PRODSTRING);
425         ParseNode set = new ParseNode("setexpr", parser.curLine(3));
426         set.addChild("dot").addChild("quantifiervar", parser.curLine(3)).addChild(var);
427         set.getChild("dot").addChild("relation", parser.curLine(1)).addChild(relation);
428         RESULT = set;
429         :}
430
431         | ID:var DOTINV ID:relation
432         {:
433         debugMessage(PRODSTRING);
434         ParseNode set = new ParseNode("setexpr", parser.curLine(3));
435         set.addChild("dotinv").addChild("quantifiervar", parser.curLine(3)).addChild(var);
436         set.getChild("dotinv").addChild("relation", parser.curLine(1)).addChild(relation);
437         RESULT = set;
438         :}
439         ;
440         
441 expr ::=
442         
443         ID:var
444         {:
445         debugMessage(PRODSTRING);
446         ParseNode expr = new ParseNode("expr", parser.curLine(1));      
447         expr.addChild("var").addChild(var);
448         RESULT = expr;
449         :}
450         
451         | OPENPAREN expr:expr CLOSEPAREN 
452         {:
453         debugMessage(PRODSTRING);
454         RESULT = expr;
455         :}     
456         
457         | LITERAL OPENPAREN literal:literal CLOSEPAREN
458         {:
459         debugMessage(PRODSTRING);
460         ParseNode expr = new ParseNode("expr", parser.curLine(4));
461         expr.addChild(literal);
462         RESULT = expr;
463         :}
464         
465         | expr:expr DOT ID:relname
466         {:
467         debugMessage(PRODSTRING);
468         ParseNode relation = (new ParseNode("expr", parser.curLine(3))).addChild("relation");
469         relation.addChild(expr);
470         relation.addChild("name").addChild(relname);
471         RESULT = relation.getRoot();
472         :}
473         
474         | expr:expr DOTINV ID:relname
475         {:
476         debugMessage(PRODSTRING);
477         ParseNode relation = (new ParseNode("expr", parser.curLine(3))).addChild("relation");
478         relation.addChild(expr);
479         relation.addChild("name").addChild(relname);
480         relation.addChild("inv");
481         RESULT = relation.getRoot();
482         :}
483              
484         | expr:expr1 operator:operator expr:expr2
485         {:
486         debugMessage(PRODSTRING);
487         ParseNode op = (new ParseNode("expr", parser.curLine(3))).addChild("operator");
488         op.addChild("op").addChild(operator);
489         op.addChild("left", parser.curLine(3)).addChild(expr1);
490         op.addChild("right", parser.curLine(1)).addChild(expr2);
491         RESULT = op.getRoot();
492         :}
493
494         | SIZEOF OPENPAREN setexpr:setexpr CLOSEPAREN
495         {:
496         ParseNode sizeof = (new ParseNode("expr", parser.curLine(4))).addChild("sizeof");
497         sizeof.addChild(setexpr);
498         RESULT = sizeof.getRoot();
499         :}
500         ;
501
502 operator ::=
503           
504         ADD 
505         {:
506         debugMessage(PRODSTRING);
507         RESULT = new ParseNode("add", parser.curLine(1));
508         :}
509           
510         | SUB
511         {:
512         debugMessage(PRODSTRING);
513         RESULT = new ParseNode("sub", parser.curLine(1));
514         :}
515           
516         | MULT
517         {:
518         debugMessage(PRODSTRING);
519         RESULT = new ParseNode("mult", parser.curLine(1));
520         :}
521           
522         | DIV
523         {:
524         debugMessage(PRODSTRING);
525         RESULT = new ParseNode("div", parser.curLine(1));
526         :}
527         ;
528
529 compare ::= 
530
531         LT
532         {:
533         debugMessage(PRODSTRING);
534         RESULT = new ParseNode("lt", parser.curLine(1));
535         :}
536
537         | GT
538         {:
539         debugMessage(PRODSTRING);
540         RESULT = new ParseNode("gt", parser.curLine(1));
541         :}
542
543         | LE
544         {:
545         debugMessage(PRODSTRING);
546         RESULT = new ParseNode("le", parser.curLine(1));
547         :}
548
549         | GE
550         {:
551         debugMessage(PRODSTRING);
552         RESULT = new ParseNode("ge", parser.curLine(1));
553         :}
554
555         | EQ
556         {:
557         debugMessage(PRODSTRING);
558         RESULT = new ParseNode("eq", parser.curLine(1));
559         :}
560
561         | NE
562         {:
563         debugMessage(PRODSTRING);
564         RESULT = new ParseNode("ne", parser.curLine(1));
565         :}
566         ;
567         
568 literal ::=
569          
570         TRUE
571         {:
572         debugMessage(PRODSTRING);
573         RESULT = (new ParseNode("literal", parser.curLine(1))).addChild("boolean").addChild("true").getRoot();
574         :}
575          
576         | DECIMAL:dec
577         {:
578         debugMessage(PRODSTRING);
579         RESULT = (new ParseNode("literal", parser.curLine(1))).addChild("decimal").addChild(dec).getRoot();
580         :}
581          
582         | STRING:str
583         {:
584         debugMessage(PRODSTRING);
585         RESULT = (new ParseNode("literal", parser.curLine(1))).addChild("string").addChild(str).getRoot();
586         :}
587          
588         | CHAR:chr
589         {:
590         debugMessage(PRODSTRING);
591         RESULT = (new ParseNode("literal", parser.curLine(1))).addChild("char").addChild(chr).getRoot();
592         :}
593          
594         | ID:literal
595         {:
596         debugMessage(PRODSTRING);
597         RESULT = (new ParseNode("literal", parser.curLine(1))).addChild("token").addChild(literal).getRoot();
598         :}
599         ;