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