    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package escjava.ast;
    004
    005    import javafe.ast.ASTNode;
    006    import javafe.ast.ASTDecoration;
    007    import javafe.ast.ModifierPragma;
    008    import javafe.ast.ModifierPragmaVec;
    009    import javafe.ast.GenericVarDecl;
    010    import javafe.ast.IdentifierNode;
    011    import javafe.ast.ASTDecoration;
    012    import javafe.ast.RoutineDecl;
    013    import javafe.ast.MethodDecl;
    014    import javafe.ast.ClassDecl;
    015    import javafe.ast.TypeDecl;
    016    import javafe.tc.TypeSig;
    017    import javafe.ast.Type;
    018    import javafe.ast.TypeName;
    019    import javafe.ast.ArrayType;
    020    import javafe.ast.PrimitiveType;
    021    import javafe.ast.FormalParaDecl;
    022    import javafe.ast.FormalParaDeclVec;
    023    import javafe.ast.*;
    024    import escjava.Main;
    025
    026    import javafe.util.*;
    027    import java.util.Enumeration;
    028
    029
    030    public final class Utils
    031    {
    032      /**
    033       * Finds and returns the first modifier pragma of <code>vdecl</code>
    034       * that has the tag <code>tag</code>, if any.  If none, returns
    035       * <code>null</code>.<p>
    036       *
    037       * Note, if you want to know whether a variable is
    038       * <code>non_null</code>, use method <code>NonNullPragma</code>
    039       * instead, for it properly handles inheritance of
    040       * <code>non_null</code> pragmas.
    041       **/
    042      static public ModifierPragma findModifierPragma(/*@ non_null */ GenericVarDecl vdecl,
    043                                                      int tag) {
    044        return findModifierPragma(vdecl.pmodifiers,tag);
    045      }
    046
    047      static public ModifierPragma findModifierPragma(ModifierPragmaVec mp,
    048                                                      int tag) {
    049        if (mp != null) {
    050          for (int j = 0; j < mp.size(); j++) {
    051            ModifierPragma prag= mp.elementAt(j);
    052            if (prag.getTag() == tag)
    053              return prag;
    054          }
    055        }
    056        return null;  // not present
    057      }
    058
    059      static public void removeModifierPragma(/*@ non_null */ GenericVarDecl vdecl, int tag) {
    060        removeModifierPragma(vdecl.pmodifiers,tag);
    061      }
    062
    063      static public void removeModifierPragma(ModifierPragmaVec p, int tag) {
    064        if (p != null) {
    065          for (int j = 0; j < p.size(); j++) {
    066            ModifierPragma prag= p.elementAt(j);
    067            if (prag.getTag() == tag) {
    068              p.removeElementAt(j);
    069              --j;
    070            }
    071          }
    072        }
    073      }
    074
    075      static public boolean isModel(javafe.ast.FieldDecl fd) {
    076        return isModel(fd.pmodifiers);
    077      }
    078
    079      static public boolean isModel(ModifierPragmaVec m) {
    080        if (m == null) return false;
    081        return findModifierPragma(m,TagConstants.MODEL) != null;
    082      }
    083
    084      // Used for designator expressions, as in a modifies clause.
    085      static public boolean isModel(Expr e) {
    086        if (e instanceof VariableAccess) {
    087          VariableAccess va = (VariableAccess)e;
    088          if (va.decl instanceof FieldDecl) {
    089            return isModel( (FieldDecl)va.decl );
    090          }
    091          //System.out.println("ISMODEL-VA " + va.decl.getClass());
    092        } else if (e instanceof FieldAccess) {
    093          return isModel( ((FieldAccess)e).decl );
    094        } else if (e instanceof NothingExpr) {
    095          return true;
    096        } else if (e instanceof EverythingExpr) {
    097          return false;
    098        } else if (e instanceof ArrayRefExpr) {
    099          return isModel( ((ArrayRefExpr)e).array );
    100        } else if (e instanceof ArrayRangeRefExpr) {
    101          return isModel( ((ArrayRangeRefExpr)e).array );
    102        } else if (e instanceof WildRefExpr) {
    103          return false;
    104        } else if (e instanceof NaryExpr) {
    105          // This can occur if \dttfsa is used in a modifies clause
    106          return false;
    107        } else {
    108          //System.out.println(EscPrettyPrint.inst.toString(e));
    109          //System.out.println("ISMODEL " + e.getClass());
    110          //ErrorSet.dump(null);
    111        }
    112        return false; // default
    113      }
    114
    115      static public abstract class BooleanDecoration extends ASTDecoration {
    116        private static final Object decFALSE = new Object();
    117        private static final Object decTRUE = new Object();
    118        public BooleanDecoration(String s) {
    119          super(s);
    120        }
    121        public void set(ASTNode o, boolean b) {
    122          set(o, b?decTRUE:decFALSE);
    123        }
    124        public boolean isTrue(ASTNode o) {
    125          Object res = get(o);
    126          if (res == null) {
    127            boolean b = calculate(o);
    128            set(o,b);
    129            return b;
    130          }
    131          return res == decTRUE;
    132        }
    133        public abstract boolean calculate(ASTNode o);
    134      }
    135
    136      static private BooleanDecoration pureDecoration = new BooleanDecoration("pure") {
    137          public boolean calculate(ASTNode o) {
    138            RoutineDecl rd = (RoutineDecl)o;
    139            return findPurePragma(rd) != null;
    140          }
    141        };
    142      static public boolean isPure(RoutineDecl rd) {
    143        return pureDecoration.isTrue(rd);
    144      }
    145      static public void setPure(RoutineDecl rd) {
    146        pureDecoration.set(rd,true);
    147      }
    148      static public ModifierPragma findPurePragma(RoutineDecl rd) {
    149        ModifierPragma m = null;
    150        m = findModifierPragma(rd.pmodifiers,TagConstants.PURE);
    151        if (m!=null) return m;
    152        m = findModifierPragma(rd.parent.pmodifiers,TagConstants.PURE);
    153        if (m != null) return m;
    154        if (rd instanceof MethodDecl) {
    155          MethodDecl md = (MethodDecl)rd;
    156          Set direct = javafe.tc.PrepTypeDeclaration.inst.getOverrides(md.parent, md);
    157          Enumeration e = direct.elements();
    158          while (e.hasMoreElements()) {
    159            MethodDecl directMD = (MethodDecl)e.nextElement();
    160            m = findPurePragma(directMD);
    161            if (m != null) return m;
    162          }
    163        }
    164        return null;
    165      }
    166      private static final BooleanDecoration immutableDecoration = new BooleanDecoration("immutable") {
    167          public boolean calculate(ASTNode o) {
    168            return findModifierPragma(((TypeDecl)o).pmodifiers, TagConstants.IMMUTABLE)
    169              != null ;
    170            //|| findModifierPragma(((TypeDecl)o).pmodifiers, TagConstants.PURE) != null;
    171          }
    172        };
    173      public static boolean isImmutable(TypeDecl cd) {
    174        return immutableDecoration.isTrue(cd);
    175      }
    176
    177      public static final BooleanDecoration ensuresDecoration = new BooleanDecoration("ensuresFromException") {
    178        public boolean calculate(ASTNode o) {
    179          return false;
    180        }
    181      };
    182
    183      private static final BooleanDecoration allocatesDecoration = new BooleanDecoration("allocates") {
    184        public boolean calculate(ASTNode o) {
    185          if (!(o instanceof MethodDecl)) {
    186             //System.out.println("CALLING ALLOCATES ON NOT METHOD " + Location.toString(o.getStartLoc()));
    187             return true;
    188          }
    189          MethodDecl rd = (MethodDecl)o;
    190            javafe.util.Set ov = escjava.tc.FlowInsensitiveChecks.getDirectOverrides((MethodDecl)rd);
    191            Enumeration k = ov.elements();
    192            while (k.hasMoreElements()) {
    193               if (isAllocates( (MethodDecl)k.nextElement() )) {
    194    //System.out.println("PARENT ALLOCATES " + rd.id() + " " + Location.toString(rd.getStartLoc()));
    195                   return true;
    196               }
    197            }
    198            ModifierPragmaVec mpv = rd.pmodifiers;
    199            for (int i=0; i<mpv.size(); ++i) {
    200              ModifierPragma m = mpv.elementAt(i);
    201              if (m instanceof ExprModifierPragma) {
    202                if (checkForFresh( ((ExprModifierPragma)m).expr )) {
    203    //System.out.println("ENSURES ALLOCATES " + rd.id() + " " + Location.toString(m.getStartLoc()));
    204                  return true;
    205                }
    206              } else if (m instanceof VarExprModifierPragma) {
    207                if (checkForFresh( ((VarExprModifierPragma)m).expr )) {
    208    //System.out.println("SIGNALS ALLOCATES " + rd.id() + " " + Location.toString(m.getStartLoc()));
    209                  return true;
    210                }
    211              }
    212            }
    213            return false;
    214        }
    215
    216        private boolean checkForFresh(ExprVec ev) {
    217            for (int i=0; i<ev.size(); ++i) {
    218              if (checkForFresh(ev.elementAt(i))) return true;
    219            }
    220            return false;
    221        }
    222        private boolean checkForFresh(Expr e) {
    223          if (e == null) return false;
    224          else if (e instanceof BinaryExpr) {
    225            BinaryExpr be = (BinaryExpr)e;
    226            return checkForFresh(be.left) || checkForFresh(be.right);
    227          } else if (e instanceof UnaryExpr) {
    228            UnaryExpr ue = (UnaryExpr)e;
    229            return checkForFresh(ue.expr);
    230          } else if (e instanceof NaryExpr) {
    231            NaryExpr ne = (NaryExpr)e;
    232            if (ne.op == TagConstants.FRESH) return true;
    233            return checkForFresh(ne.exprs);
    234          } else if (e instanceof MethodInvocation) {
    235            MethodInvocation mi = (MethodInvocation)e;
    236            if (mi.od instanceof ExprObjectDesignator) {
    237              if ( checkForFresh( ((ExprObjectDesignator)mi.od).expr )) return true;
    238            }
    239            return checkForFresh(mi.args);
    240          } else if (e instanceof ArrayRefExpr) {
    241            return checkForFresh( ((ArrayRefExpr)e).index) ||
    242                   checkForFresh( ((ArrayRefExpr)e).array) ;
    243          } else if (e instanceof CondExpr) {
    244            return checkForFresh( ((CondExpr)e).test ) ||
    245                   checkForFresh( ((CondExpr)e).thn  ) ||
    246                   checkForFresh( ((CondExpr)e).els  );
    247          } else if (e instanceof CastExpr) {
    248            return checkForFresh( ((CastExpr)e).expr );
    249          } else if (e instanceof ParenExpr) {
    250            return checkForFresh( ((ParenExpr)e).expr );
    251          } else if (e instanceof LabelExpr) {
    252            return checkForFresh( ((LabelExpr)e).expr );
    253          } else if (e instanceof FieldAccess) {
    254            FieldAccess fa = (FieldAccess)e;
    255            if (fa.od instanceof ExprObjectDesignator) {
    256              if ( checkForFresh( ((ExprObjectDesignator)fa.od).expr )) return true;
    257            }
    258            return false;
    259          } else if (e instanceof NewArrayExpr) {
    260            NewArrayExpr nae = (NewArrayExpr)e;
    261            return checkForFresh( nae.dims );
    262             // FIXME - what about array initializers?
    263          } else if (e instanceof NewInstanceExpr) {
    264            NewInstanceExpr nie = (NewInstanceExpr)e;
    265            return checkForFresh( nie.args );
    266          } else if (e instanceof SetCompExpr) {
    267            return checkForFresh( ((SetCompExpr)e).expr );
    268          } else if (e instanceof LiteralExpr) {
    269            return false;
    270          } else if (e instanceof VariableAccess) {
    271            return false;
    272          } else if (e instanceof ThisExpr) {
    273            return false;
    274          } else if (e instanceof ResExpr) {
    275            return false;
    276          } else if (e instanceof escjava.ast.TypeExpr) {
    277            return false;
    278          } else if (e instanceof LockSetExpr) {
    279            return false;
    280          } else if (e instanceof NotModifiedExpr) {
    281            return false;
    282          } else if (e instanceof InstanceOfExpr) {
    283            return false;
    284          } else if (e instanceof ClassLiteral) {
    285            return false;
    286          } else if (e instanceof QuantifiedExpr) {
    287            return checkForFresh( ((QuantifiedExpr)e).expr) ||
    288                   checkForFresh( ((QuantifiedExpr)e).rangeExpr) ;
    289          } else if (e instanceof GeneralizedQuantifiedExpr ) {
    290            return checkForFresh( ((GeneralizedQuantifiedExpr)e).expr) ||
    291                   checkForFresh( ((GeneralizedQuantifiedExpr)e).rangeExpr) ;
    292          } else if (e instanceof NumericalQuantifiedExpr) {
    293            return checkForFresh( ((NumericalQuantifiedExpr)e).expr) ||
    294                   checkForFresh( ((NumericalQuantifiedExpr)e).rangeExpr) ;
    295          } else {
    296            System.out.println("CLASS " + e.getClass());
    297            return true;
    298          }
    299        }
    300      };
    301      public static boolean isAllocates(RoutineDecl rd) {
    302        return allocatesDecoration.isTrue(rd);
    303      }
    304
    305      private static final BooleanDecoration functionDecoration = new BooleanDecoration("function") {
    306        public boolean calculate(ASTNode o) {
    307          RoutineDecl rd = (RoutineDecl)o;
    308          if (findModifierPragma(rd.pmodifiers,TagConstants.FUNCTION)
    309              != null) return true;
    310          if (!isPure(rd)) return false;
    311          // If non-static, the owning class must be immutable
    312          // But it can't override non-function methods
    313          // Constructors don't depend on the owning class
    314          if (!Modifiers.isStatic(rd.modifiers) && (rd instanceof MethodDecl)) {
    315            if ( ! isImmutable(rd.parent) ) return false;
    316            if (isAllocates(rd)) return false;
    317            javafe.util.Set ov = escjava.tc.FlowInsensitiveChecks.getAllOverrides((MethodDecl)rd);
    318            Enumeration i = ov.elements();
    319            while (i.hasMoreElements()) {
    320               if (!isFunction( (MethodDecl)i.nextElement() )) return false;
    321            }
    322          }
    323          // All argument types must be primitive or immutable
    324          FormalParaDeclVec args = rd.args;
    325          for (int i=0; i<args.size(); ++i) {
    326            FormalParaDecl f = args.elementAt(i);
    327            Type t = f.type;
    328            if (t instanceof TypeName) t = TypeSig.getSig((TypeName)t);
    329            if (t instanceof PrimitiveType) continue;
    330            if (t instanceof ArrayType) return false;
    331            if (t instanceof TypeSig) {
    332              if (! isImmutable(((TypeSig)t).getTypeDecl())) return false;
    333            }
    334          }
    335          return true;
    336        }
    337      };
    338    public static boolean isFunction(RoutineDecl rd) {
    339      return functionDecoration.isTrue(rd);
    340    }
    341
    342
    343      public static final ASTDecoration exceptionDecoration =
    344                                         new ASTDecoration("originalExceptions");
    345
    346      public static final ASTDecoration axiomDecoration = new ASTDecoration("axioms");
    347
    348      public static final ASTDecoration representsDecoration =
    349        new ASTDecoration("representsClauses");
    350
    351      public static final ASTDecoration owningDecl = new ASTDecoration("owningDecl");
    352      public static final ASTDecoration allSpecs = new ASTDecoration("allSpecs");
    353
    354      static public ModifierPragmaVec getAllSpecs(RoutineDecl rd) {
    355        Object o = allSpecs.get(rd);
    356        if (o != null) return (ModifierPragmaVec)o;
    357        ModifierPragmaVec result = ModifierPragmaVec.make();
    358        allSpecs.set(rd,result);
    359        result.append(rd.pmodifiers);
    360        if (rd instanceof ConstructorDecl) return result;
    361        MethodDecl rrd = (MethodDecl)rd;
    362        Type[] argtypes = rd.argTypes();
    363        TypeSig td = TypeSig.getSig(rd.parent);
    364        java.util.Iterator i = td.superInterfaces().iterator();
    365        td = td.superClass();
    366        while (td != null) {
    367          MethodDecl md = td.hasMethod(rrd.id, argtypes);
    368          if (md != null) result.append(md.pmodifiers);
    369          td = td.superClass();
    370        }
    371
    372        while (i.hasNext()) {
    373          td = (TypeSig)i.next();
    374          MethodDecl md = td.hasMethod(rrd.id, argtypes);
    375          if (md != null) result.append(md.pmodifiers);
    376        }
    377
    378        return result;
    379      }
    380
    381      public static final ASTDecoration inheritedSpecs = new ASTDecoration("inheritedSpecs");
    382
    383      static public ModifierPragmaVec getInheritedSpecs(RoutineDecl rd) {
    384        IdentifierNode fullName = IdentifierNode.make(escjava.translate.TrAnExpr.fullName(rd,false));
    385        Object o = inheritedSpecs.get(fullName);
    386        if (o != null) return (ModifierPragmaVec)o;
    387        ModifierPragmaVec result = ModifierPragmaVec.make();
    388        inheritedSpecs.set(fullName,result);
    389        return result;
    390      }
    391
    392      static public ModifierPragmaVec addInheritedSpecs(RoutineDecl rd, ModifierPragmaVec mp) {
    393        ModifierPragmaVec mpv = Utils.getInheritedSpecs(rd);
    394        mpv.append(mp);
    395        ExprModifierPragma req = null;
    396        int index = 0;
    397        for (int i=0; i<mpv.size(); ++i) {
    398          ModifierPragma m = mpv.elementAt(i);
    399          if (m.getTag() != TagConstants.REQUIRES) continue;
    400          if (req == null) { req = (ExprModifierPragma)m; index = i; continue; }
    401          req = escjava.AnnotationHandler.or(req,(ExprModifierPragma)m);
    402          mpv.setElementAt(req,index);
    403          mpv.removeElementAt(i);
    404          --i;
    405        }
    406        return mpv;
    407      }
    408
    409    }
    410