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    }