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 }