001 /* Copyright 2000, 2001, Compaq Computer Corporation */
002
003 package escjava.translate;
004
005 /** This class contains a number of sanity checks of guarded commands.
006 **/
007
008 import java.util.Enumeration;
009
010 import javafe.util.Set;
011 import javafe.util.Assert;
012
013 import javafe.ast.*;
014 import escjava.ast.*;
015 import escjava.ast.TagConstants;
016
017 import escjava.Main;
018
019
020 public class GCSanity {
021 public static void check(/*@ non_null */ GuardedCmd g) {
022 if (! Main.options().noVarCheckDeclsAndUses) {
023 Set edci = new Set();
024 Set cdni = new Set();
025 Set euei = new Set();
026 Set uuei = new Set();
027 Set sp = new Set();
028 checkDeclsAndUses(g, edci, cdni, euei, uuei, "", sp);
029 }
030 }
031
032 /** Checks that there are no duplicate definitions of local variables,
033 * including implicit outermost declarations and considering dynamic
034 * inflections. Also checks that dynamic-inflection prefixes are unique.
035 *
036 * @param edci ever declared with current inflection
037 * @param cdni currently declared with nonempty inflection
038 * @param euei ever used with empty inflection
039 * @param uuei unusable with empty inflection
040 * @param inflection current inflection
041 * @param sp seen prefixes (except "")
042 **/
043
044 private static void checkDeclsAndUses(/*@ non_null */ GuardedCmd g,
045 /*@ non_null */ Set edci,
046 /*@ non_null */ Set cdni,
047 /*@ non_null */ Set euei,
048 /*@ non_null */ Set uuei,
049 /*@ non_null */ String inflection,
050 /*@ non_null */ Set sp) {
051 switch (g.getTag()) {
052 case TagConstants.SKIPCMD:
053 case TagConstants.RAISECMD:
054 break;
055
056 case TagConstants.LOOPCMD:
057 {
058 LoopCmd lp = (LoopCmd)g;
059 checkDeclsAndUses(lp.desugared,
060 edci, cdni, euei, uuei,
061 inflection, sp);
062 break;
063 }
064
065 case TagConstants.CALL:
066 {
067 Call call = (Call)g;
068 checkDeclsAndUses(call.desugared,
069 edci, cdni, euei, uuei,
070 inflection, sp);
071 break;
072 }
073
074 case TagConstants.ASSERTCMD:
075 case TagConstants.ASSUMECMD:
076 {
077 ExprCmd ec = (ExprCmd)g;
078 checkUses(ec.pred, cdni, euei, uuei);
079 break;
080 }
081
082 case TagConstants.GETSCMD:
083 case TagConstants.RESTOREFROMCMD:
084 {
085 AssignCmd ac = (AssignCmd)g;
086 checkUses(ac.v, cdni, euei, uuei);
087 if (ac.rhs != null) checkUses(ac.rhs, cdni, euei, uuei);
088 break;
089 }
090
091 case TagConstants.SUBGETSCMD:
092 {
093 SubGetsCmd ac = (SubGetsCmd)g;
094 checkUses(ac.v, cdni, euei, uuei);
095 checkUses(ac.index, cdni, euei, uuei);
096 if (ac.rhs != null) checkUses(ac.rhs, cdni, euei, uuei);
097 break;
098 }
099
100 case TagConstants.SUBSUBGETSCMD:
101 {
102 SubSubGetsCmd ac = (SubSubGetsCmd)g;
103 checkUses(ac.v, cdni, euei, uuei);
104 checkUses(ac.index1, cdni, euei, uuei);
105 checkUses(ac.index2, cdni, euei, uuei);
106 if (ac.rhs != null) checkUses(ac.rhs, cdni, euei, uuei);
107 break;
108 }
109
110 case TagConstants.VARINCMD:
111 {
112 VarInCmd vc = (VarInCmd)g;
113 boolean emptyInflection = inflection.length() == 0;
114 /*-@ uninitialized */ boolean[] previouslyInCdni = null;
115 if (! emptyInflection) {
116 previouslyInCdni = new boolean[vc.v.size()];
117 }
118 for (int i = 0; i < vc.v.size(); i++) {
119 GenericVarDecl vd = (GenericVarDecl)vc.v.elementAt(i);
120 Assert.notFalse(! edci.add(vd));
121 if (emptyInflection) {
122 Assert.notFalse(! euei.contains(vd));
123 } else {
124 previouslyInCdni[i] = cdni.add(vd);
125 }
126 }
127 checkDeclsAndUses(vc.g, edci, cdni, euei, uuei,
128 inflection, sp);
129 for (int i = 0; i < vc.v.size(); i++) {
130 GenericVarDecl vd = (GenericVarDecl)vc.v.elementAt(i);
131 if (emptyInflection) {
132 uuei.add(vd);
133 } else if (! previouslyInCdni[i]) {
134 cdni.remove(vd);
135 }
136 }
137 break;
138 }
139
140 case TagConstants.DYNINSTCMD:
141 {
142 DynInstCmd dc = (DynInstCmd)g;
143 Set edciNew = new Set();
144 String infl = inflection + "-" + dc.s;
145 Assert.notFalse(! sp.add(infl.intern()));
146 checkDeclsAndUses(dc.g, edciNew, cdni, euei, uuei, infl, sp);
147 break;
148 }
149
150 case TagConstants.SEQCMD:
151 {
152 SeqCmd sc = (SeqCmd)g;
153 for (int i = 0; i < sc.cmds.size(); i++) {
154 checkDeclsAndUses(sc.cmds.elementAt(i),
155 edci, cdni, euei, uuei,
156 inflection, sp);
157 }
158 break;
159 }
160
161 case TagConstants.TRYCMD:
162 case TagConstants.CHOOSECMD:
163 {
164 CmdCmdCmd tc = (CmdCmdCmd)g;
165 checkDeclsAndUses(tc.g1, edci, cdni, euei, uuei,
166 inflection, sp);
167 checkDeclsAndUses(tc.g2, edci, cdni, euei, uuei,
168 inflection, sp);
169 break;
170 }
171
172 default:
173 //@ unreachable;
174 Assert.fail("Fall thru on "+g);
175 break;
176 }
177 }
178
179 private static void checkUses(/*@ non_null */ Expr e,
180 /*@ non_null */ Set cdni,
181 /*@ non_null */ Set euei,
182 /*@ non_null */ Set uuei) {
183 for (Enumeration freeVars = Substitute.freeVars(e).elements();
184 freeVars.hasMoreElements(); ) {
185 GenericVarDecl v = (GenericVarDecl)freeVars.nextElement();
186 if (! cdni.contains(v)) {
187 Assert.notFalse(! uuei.contains(v));
188 euei.add(v);
189 }
190 }
191 }
192 }