    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    }