TypeChecker.java Source File

00001 package edu.ksu.cis.bandera.specification.predicate.ast;
00002 
00003 /* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
00004  * Bandera, a Java(TM) analysis and transformation toolkit           *
00005  * Copyright (C) 2000   Robby (robby@cis.ksu.edu)                    *
00006  * All rights reserved.                                              *
00007  *                                                                   *
00008  * This work was done as a project in the SAnToS Laboratory,         *
00009  * Department of Computing and Information Sciences, Kansas State    *
00010  * University, USA (http://www.cis.ksu.edu/santos).                  *
00011  * It is understood that any modification not identified as such is  *
00012  * not covered by the preceding statement.                           *
00013  *                                                                   *
00014  * This work is free software; you can redistribute it and/or        *
00015  * modify it under the terms of the GNU Library General Public       *
00016  * License as published by the Free Software Foundation; either      *
00017  * version 2 of the License, or (at your option) any later version.  *
00018  *                                                                   *
00019  * This work is distributed in the hope that it will be useful,      *
00020  * but WITHOUT ANY WARRANTY; without even the implied warranty of    *
00021  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU *
00022  * Library General Public License for more details.                  *
00023  *                                                                   *
00024  * You should have received a copy of the GNU Library General Public *
00025  * License along with this toolkit; if not, write to the             *
00026  * Free Software Foundation, Inc., 59 Temple Place - Suite 330,      *
00027  * Boston, MA  02111-1307, USA.                                      *
00028  *                                                                   *
00029  * Java is a trademark of Sun Microsystems, Inc.                     *
00030  *                                                                   *
00031  * To submit a bug report, send a comment, or get the latest news on *
00032  * this project and other SAnToS projects, please visit the web-site *
00033  *                http://www.cis.ksu.edu/santos                      *
00034  * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
00035 import ca.mcgill.sable.soot.jimple.Local;
00036 import ca.mcgill.sable.soot.Modifier;
00037 import java.util.*;
00038 import ca.mcgill.sable.soot.SootClass;
00039 import edu.ksu.cis.bandera.specification.predicate.analysis.*;
00040 import edu.ksu.cis.bandera.specification.predicate.node.*;
00041 import edu.ksu.cis.bandera.specification.predicate.exception.*;
00042 import edu.ksu.cis.bandera.specification.predicate.datastructure.*;
00043 import edu.ksu.cis.bandera.jjjc.symboltable.*;
00044 import edu.ksu.cis.bandera.annotation.*;
00045 import edu.ksu.cis.bandera.jjjc.symboltable.Package;
00046 import edu.ksu.cis.bandera.jjjc.util.Util;
00047 public class TypeChecker extends DepthFirstAdapter {
00048     private Vector exceptions = new Vector();
00049     private Node node;
00050     private SymbolTable symbolTable;
00051     private ClassOrInterfaceType type;
00052     private Annotation annotation;
00053     private int mode;
00054     private Vector labeledStmtAnnotations;
00055     private LabeledStmtAnnotation currentAnnotation;
00056     private Type currentType;
00057     private String predName;
00058     private AnnotationManager am;
00059     private final static int EXP = 1;
00060     private final static int RETURN = 2;
00061     private final static int INVOKE = 4;
00062     private final static int LOCATION = 8;
00063     private boolean isStatic;
00064     private boolean usePrivate;
00065     private boolean ret;
00066     private StringBuffer buffer;
00067     private Vector usedTypeNames = new Vector();
00068     private Hashtable variablesUsed;
00069     private Vector params;
00070     private Vector paramTypes;
00071 /**
00072  * 
00073  * @param node edu.ksu.cis.bandera.predicate.node.AWeakArrayNavigation
00074 public void caseAWeakArrayNavigation(AWeakArrayNavigation node) {
00075     if (currentType instanceof ArrayType) {
00076         currentType = new ArrayType(((ArrayType) currentType).baseType,
00077                 ((ArrayType) currentType).nDimensions - 1);
00078     } else {
00079         int line = node.getLWeakArrayReference().getLine();
00080         int pos = node.getLWeakArrayReference().getPos();
00081         exceptions.add(new TypeException("[" + line + ", " + pos + "] not an array in array navigation"));
00082         currentType = VoidType.TYPE;
00083     }
00084     expTable.put(node, currentType);
00085 }
00086  */
00087 /**
00088  * 
00089  * @param node edu.ksu.cis.bandera.predicate.node.AWeakCastExp
00090 public void caseAWeakCastExp(AWeakCastExp node) {
00091     currentType = VoidType.TYPE;
00092     Type cast;
00093     try {
00094         cast = symbolTable.resolveType(new Name(node.getType().toString()));
00095     } catch (Exception e) {
00096         int line = node.getLWeakCastParen().getLine();
00097         int pos = node.getLWeakCastParen().getPos();
00098         exceptions.add(new TypeException("[" + line + ", " + pos + "] invalid casting type"));
00099         expTable.put(node, currentType);
00100         return;
00101     }
00102     int i;
00103     if ((i = node.getDim().toArray().length) > 0) {
00104         cast = new ArrayType(cast, i);
00105     }
00106     node.getExp().apply(this);
00107     if (!currentType.isValidCastingConversion(cast)) {
00108         int line = node.getLWeakCastParen().getLine();
00109         int pos = node.getLWeakCastParen().getPos();
00110         exceptions.add(new TypeException("[" + line + ", " + pos + "] invalid casting type"));
00111     }
00112     currentType = cast;
00113     expTable.put(node, currentType);
00114 }
00115  */
00116 /**
00117  * 
00118  * @param node edu.ksu.cis.bandera.predicate.node.AWeakObjectNavigation
00119 public void caseAWeakObjectNavigation(AWeakObjectNavigation node) {
00120     String id = node.getId().toString().trim();
00121     if ("length".equals(id) && (currentType instanceof ArrayType)) {
00122         currentType = IntType.TYPE;
00123     } else if (currentType instanceof ClassOrInterfaceType) {
00124         try {
00125             currentType = ((ClassOrInterfaceType) currentType).getField(new Name(id)).getType();
00126         } catch (Exception e) {
00127             int line = node.getWeakObjectReference().getLine();
00128             int pos = node.getWeakObjectReference().getPos();
00129             exceptions.add(new TypeException("[" + line + ", " + pos + "] field undefined"));
00130             currentType = VoidType.TYPE;
00131         }
00132     } else {
00133         int line = node.getWeakObjectReference().getLine();
00134         int pos = node.getWeakObjectReference().getPos();
00135         exceptions.add(new TypeException("[" + line + ", " + pos + "] not an object in object navigation"));
00136         currentType = VoidType.TYPE;
00137     }
00138     expTable.put(node, currentType);
00139 }
00140  */
00141 /**
00142  * 
00143  * @param node edu.ksu.cis.bandera.bpdl.node.Node
00144  * @param symbolTable edu.ksu.cis.bandera.jjjc.symboltable.SymbolTable
00145  * @param type edu.ksu.cis.bandera.jjjc.symboltable.ClassOrInterfaceType
00146  * @param annotation edu.ksu.cis.bandera.annotation.Annotation
00147  */
00148 public TypeChecker(Node node, SymbolTable symbolTable, ClassOrInterfaceType type, Annotation annotation) {
00149     this.node = node;
00150     this.symbolTable = symbolTable;
00151     this.annotation = annotation;
00152     this.type = type;
00153     if (annotation != null) {
00154         Vector v = annotation.getAllAnnotations(false);
00155         labeledStmtAnnotations = new Vector();
00156         for (Enumeration e = v.elements(); e.hasMoreElements();) {
00157             Object o = e.nextElement();
00158             if (o instanceof LabeledStmtAnnotation) labeledStmtAnnotations.add(o);
00159         }
00160     }
00161 }
00162 /**
00163  * 
00164  * @return edu.ksu.cis.bandera.predicate.node.PExp
00165  * @param name edu.ksu.cis.bandera.predicate.node.AQualifiedName
00166  */
00167 private PExp buildNavigation(AQualifiedName name) {
00168     PExp exp;
00169     if (name.getName() instanceof AQualifiedName) {
00170         exp = buildNavigation((AQualifiedName) name.getName());
00171     } else {
00172         exp = buildNavigation((ASimpleName) name.getName());
00173     }
00174     
00175     return new ANavigationExp(exp, new AStrongObjectNavigation(new TDot(), name.getId()));
00176 }
00177 /**
00178  * 
00179  * @return edu.ksu.cis.bandera.predicate.node.PExp
00180  * @param name edu.ksu.cis.bandera.predicate.node.ASimpleName
00181  */
00182 private PExp buildNavigation(ASimpleName name) {
00183     return new ANameExp(name);
00184 }
00185 /**
00186  * 
00187  * @return edu.ksu.cis.bandera.predicate.node.PExp
00188  * @param typeExp edu.ksu.cis.bandera.predicate.node.PExp
00189  * @param name java.lang.String
00190  */
00191 private PExp buildNavigation(PExp typeExp, String name) {
00192     for (StringTokenizer tokenizer = new StringTokenizer(name); tokenizer.hasMoreTokens();) {
00193         String token = (String) tokenizer.nextToken();
00194         typeExp = new ANavigationExp(typeExp, new AStrongObjectNavigation(new TDot(), new TId(token)));
00195     }
00196     return typeExp;
00197 }
00198 /**
00199  * 
00200  * @param node edu.ksu.cis.bandera.bpdl.node.ABinaryExp
00201  */
00202 public void caseABinaryExp(ABinaryExp node) {
00203     node.getLeft().apply(this);
00204     Type leftType = currentType;
00205     node.getRight().apply(this);
00206     Type rightType = currentType;
00207 
00208     PBinOp binOp = node.getBinOp();
00209     if ((binOp instanceof AAndBinOp) || (binOp instanceof AOrBinOp)) {
00210         // && ||
00211         currentType = BooleanType.TYPE;
00212         if ((leftType != BooleanType.TYPE) || (rightType != BooleanType.TYPE)) {
00213             exceptions.add(new TypeException("Expecting boolean expression"));
00214         }
00215     } else if ((binOp instanceof ABitAndBinOp) || (binOp instanceof ABitOrBinOp)
00216              || (binOp instanceof ABitXorBinOp)) {
00217         // & | ^
00218         currentType = IntType.TYPE;
00219         if ((leftType == BooleanType.TYPE) && (rightType == BooleanType.TYPE)) {
00220             currentType = BooleanType.TYPE;
00221         } else if (getIntegralType(leftType, rightType) != null) {
00222             currentType = getIntegralType(leftType, rightType);
00223         } else {
00224             exceptions.add(new TypeException("Type mismatch for binary operator " + binOp.toString().trim()));
00225         }
00226     } else if ((binOp instanceof APlusBinOp) || (binOp instanceof AMinusBinOp)
00227              || (binOp instanceof ATimesBinOp) || (binOp instanceof AStrongDivBinOp)
00228              || (binOp instanceof AStrongModBinOp)) {// || (binOp instanceof AWeakDivBinOp)
00229              //|| (binOp instanceof AWeakModBinOp)) {
00230         // + - * / % /| %% 
00231         currentType = IntType.TYPE;
00232         if (getNumericType(leftType, rightType) != null) {
00233             currentType = getNumericType(leftType, rightType);
00234         } else {
00235             exceptions.add(new TypeException("Type mismatch for binary operator " + binOp.toString().trim()));
00236         }
00237     } else if ((binOp instanceof AShiftLeftBinOp) || (binOp instanceof ASignedShiftRightBinOp)
00238             || (binOp instanceof AUnsignedShiftRightBinOp)) {
00239         // << >> >>>
00240         currentType = IntType.TYPE;
00241         if (getIntegralType(leftType, rightType) != null) {
00242             currentType = getIntegralType(leftType, rightType);
00243         } else {
00244             exceptions.add(new TypeException("Type mismatch for binary operator " + binOp.toString().trim()));
00245         }
00246     } else if ((binOp instanceof ALessBinOp) || (binOp instanceof ALessEqualBinOp)
00247              || (binOp instanceof AGreaterBinOp) || (binOp instanceof AGreaterEqualBinOp)) {
00248         // < <= > >=
00249         currentType = BooleanType.TYPE;
00250         if (getNumericType(leftType, rightType) == null) {
00251             exceptions.add(new TypeException("Type mismatch for binary operator " + binOp.toString().trim()));
00252         }
00253     } else if ((binOp instanceof AEqualBinOp) || (binOp instanceof ANotEqualBinOp)) {
00254         // == !=
00255         currentType = BooleanType.TYPE;
00256         if ((leftType == BooleanType.TYPE) && (rightType == BooleanType.TYPE)) {
00257         } else if ((leftType instanceof ReferenceType) && (rightType instanceof ReferenceType)) {
00258         } else if (getNumericType(leftType, rightType) == null) {
00259             exceptions.add(new TypeException("Type mismatch for binary operator " + binOp.toString().trim()));
00260         }
00261     }
00262 }
00263 /**
00264  * 
00265  * @param node edu.ksu.cis.bandera.predicate.node.ABitComplementExp
00266  */
00267 public void caseABitComplementExp(ABitComplementExp node) {
00268     node.getExp().apply(this);
00269     if (!(currentType instanceof IntegralType)) {
00270         currentType = IntType.TYPE;
00271         exceptions.add(new TypeException("Expecting boolean expression for unary operator ~"));
00272     }
00273     if (!(currentType instanceof LongType)) {
00274         currentType = IntType.TYPE;
00275     }
00276 }
00277 /**
00278  * 
00279  * @param node edu.ksu.cis.bandera.bpdl.node.ACharLiteral
00280  */
00281 public void caseACharLiteral(ACharLiteral node) {
00282     currentType = CharType.TYPE;
00283 }
00284 /**
00285  * 
00286  * @param node edu.ksu.cis.bandera.predicate.node.AComplementExp
00287  */
00288 public void caseAComplementExp(AComplementExp node) {
00289     node.getExp().apply(this);
00290     if (currentType != BooleanType.TYPE) {
00291         currentType = BooleanType.TYPE;
00292         exceptions.add(new TypeException("Expecting boolean expression for unary operator !"));
00293     }
00294 }
00295 /**
00296  * 
00297  * @param node edu.ksu.cis.bandera.bpdl.node.ADecIntLiteral
00298  */
00299 public void caseADecIntLiteral(ADecIntLiteral node) {
00300     currentType = IntType.TYPE;
00301 }
00302 /**
00303  * 
00304  * @param node edu.ksu.cis.bandera.bpdl.node.ADecLongLiteral
00305  */
00306 public void caseADecLongLiteral(ADecLongLiteral node) {
00307     currentType = LongType.TYPE;
00308 }
00309 /**
00310  * 
00311  * @param node edu.ksu.cis.bandera.bpdl.node.ADoubleLiteral
00312  */
00313 public void caseADoubleLiteral(ADoubleLiteral node) {
00314     currentType = DoubleType.TYPE;
00315 }
00316 /**
00317  * 
00318  * @param node edu.ksu.cis.bandera.predicate.node.AEndOfLineComment
00319  */
00320 public void caseAEndOfLineComment(AEndOfLineComment node) {
00321     String s = node.toString().trim();
00322     s = s.substring(2, s.length());
00323     buffer.append(s.trim() + " ");
00324 }
00325 /**
00326  * 
00327  * @param node edu.ksu.cis.bandera.bpdl.node.AExpressionPropositionDefinition
00328  */
00329 public void caseAExpressionPropositionDefinition(AExpressionPropositionDefinition node) {
00330     usePrivate = false;
00331     variablesUsed = new Hashtable();
00332     buffer = new StringBuffer();
00333     if (node.getComment() != null) {
00334         for (Iterator i = node.getComment().iterator(); i.hasNext();) {
00335             ((PComment) i.next()).apply(this);
00336         }
00337     }
00338     isStatic = !(node.getParams() instanceof AInstanceParams);
00339     params = new Vector();
00340     paramTypes = new Vector();
00341     
00342     if (node.getParams() != null) {
00343         node.getParams().apply(this);
00344     }
00345     if (annotation != null) {
00346         exceptions.add(new BadPredicateDefinitionException("Expression predicate cannot be in method/constructor level"));
00347     } else {
00348         mode = EXP;
00349         node.getColonExp().apply(this);
00350         if (currentType != BooleanType.TYPE) {
00351             exceptions.add(new BadPredicateDefinitionException("Expression predicate should be type boolean"));
00352         }
00353     }
00354     String name = predName + "." + node.getId().toString().trim();
00355     
00356     try {
00357         Predicate p = PredicateFactory.createExpressionPredicate(new Name(name), type, node, params, paramTypes, isStatic, variablesUsed, node.getColonExp() != null ? ((AColonExp) node.getColonExp()).getExp() : null, buffer.toString(), exceptions);
00358         p.setUsePrivate(usePrivate);
00359     } catch (Exception e) {
00360         exceptions.add(e);
00361     }
00362     exceptions = new Vector();
00363     usedTypeNames = new Vector();
00364 }
00365 /**
00366  * 
00367  * @param node edu.ksu.cis.bandera.bpdl.node.AFalseLiteral
00368  */
00369 public void caseAFalseLiteral(AFalseLiteral node) {
00370     currentType = BooleanType.TYPE;
00371 }
00372 /**
00373  * 
00374  * @param node edu.ksu.cis.bandera.bpdl.node.AFloatLiteral
00375  */
00376 public void caseAFloatLiteral(AFloatLiteral node) {
00377     currentType = FloatType.TYPE;
00378 }
00379 /**
00380  * 
00381  * @param node edu.ksu.cis.bandera.bpdl.node.AHexIntLiteral
00382  */
00383 public void caseAHexIntLiteral(AHexIntLiteral node) {
00384     currentType = IntType.TYPE;
00385 }
00386 /**
00387  * 
00388  * @param node edu.ksu.cis.bandera.bpdl.node.AHexLongLiteral
00389  */
00390 public void caseAHexLongLiteral(AHexLongLiteral node) {
00391     currentType = LongType.TYPE;
00392 }
00393 /**
00394  * 
00395  * @param node edu.ksu.cis.bandera.predicate.node.AInstanceofExp
00396  */
00397 public void caseAInstanceofExp(AInstanceofExp node) {
00398     currentType = BooleanType.TYPE;
00399     node.getExp().apply(this);
00400     boolean flag = false;
00401     try {
00402         Type type = symbolTable.resolveClassOrInterfaceType(new Name(node.getType().toString()));
00403         if ((type instanceof ReferenceType) && (currentType instanceof ReferenceType))
00404             flag = true;
00405     } catch (Exception e) {
00406         exceptions.add(e);
00407     }
00408     if (!flag) {
00409         exceptions.add(new TypeException("Invalid type in instanceof expression"));
00410     }
00411 }
00412 /**
00413  * 
00414  * @param node edu.ksu.cis.bandera.bpdl.node.AInvokePropositionDefinition
00415  */
00416 public void caseAInvokePropositionDefinition(AInvokePropositionDefinition node) {
00417     usePrivate = false;
00418     variablesUsed = new Hashtable();
00419     buffer = new StringBuffer();
00420     if (node.getComment() != null) {
00421         for (Iterator i = node.getComment().iterator(); i.hasNext();) {
00422             ((PComment) i.next()).apply(this);
00423         }
00424     }
00425     String name = predName + "." + node.getId().toString().trim();
00426     params = new Vector();
00427     paramTypes = new Vector();
00428     
00429     if (node.getParams() != null) {
00430         node.getParams().apply(this);
00431     }
00432     if (annotation == null) {
00433         exceptions.add(new BadPredicateDefinitionException("Invoke predicate cannot be in class level"));
00434     } else {
00435         mode = INVOKE;
00436         
00437         if (annotation instanceof MethodDeclarationAnnotation) {
00438             int modifiers = ((MethodDeclarationAnnotation) annotation).getSootMethod().getModifiers();
00439             if (Modifier.isStatic(modifiers)) {
00440                 isStatic = true;
00441                 if (node.getParams() instanceof AInstanceParams) {
00442                     exceptions.add(new BadPredicateDefinitionException("Cannot define instance invoke predicate in a static method"));
00443                 }
00444             } else {
00445                 isStatic = false;
00446                 if (!(node.getParams() instanceof AInstanceParams)) {
00447                     exceptions.add(new BadPredicateDefinitionException("Cannot define static invoke predicate in an instance method"));
00448                 }
00449             }
00450             if (Modifier.isNative(modifiers)) {
00451                 exceptions.add(new BadPredicateDefinitionException("Invoke predicate cannot be in native method"));
00452                 try {
00453                     Predicate p = PredicateFactory.createInvokePredicate(new Name(name), type, annotation, node, params, paramTypes, isStatic, variablesUsed, node.getColonExp() != null ? ((AColonExp) node.getColonExp()).getExp() : null, buffer.toString(), exceptions);
00454                     p.setUsePrivate(usePrivate);
00455                 } catch (Exception e) {
00456                     exceptions.add(e);
00457                 }
00458                 exceptions = new Vector();
00459                 usedTypeNames = new Vector();
00460                 return;
00461             }
00462         }
00463         if (node.getColonExp() != null) {
00464             node.getColonExp().apply(this);
00465             if (currentType != BooleanType.TYPE) {
00466                 exceptions.add(new BadPredicateDefinitionException("Invoke predicate constraint should be type boolean"));
00467             }
00468         }
00469     }
00470     try {
00471         Predicate p = PredicateFactory.createInvokePredicate(new Name(name), type, annotation, node, params, paramTypes, isStatic, variablesUsed, node.getColonExp() != null ? ((AColonExp) node.getColonExp()).getExp() : null, buffer.toString(), exceptions);
00472         p.setUsePrivate(usePrivate);
00473     } catch (Exception e) {
00474         exceptions.add(e);
00475     }
00476     exceptions = new Vector();
00477     usedTypeNames = new Vector();
00478 }
00479 /**
00480  * 
00481  * @param node edu.ksu.cis.bandera.predicate.node.ALiteralExp
00482  */
00483 public void caseALiteralExp(ALiteralExp node) {
00484     super.caseALiteralExp(node);
00485 }
00486 /**
00487  * 
00488  * @param node edu.ksu.cis.bandera.bpdl.node.ALocationPropositionDefinition
00489  */
00490 public void caseALocationPropositionDefinition(ALocationPropositionDefinition node) {
00491     usePrivate = false;
00492     variablesUsed = new Hashtable();
00493     buffer = new StringBuffer();
00494     if (node.getComment() != null) {
00495         for (Iterator i = node.getComment().iterator(); i.hasNext();) {
00496             ((PComment) i.next()).apply(this);
00497         }
00498     }
00499     String name = predName + "." + node.getId().toString().trim();
00500     params = new Vector();
00501     paramTypes = new Vector();
00502     
00503     if (node.getParams() != null) {
00504         node.getParams().apply(this);
00505     }
00506     if (annotation == null) {
00507         exceptions.add(new BadPredicateDefinitionException("Location predicate cannot be in class level"));
00508     } else {
00509         mode = LOCATION;
00510         if (annotation instanceof MethodDeclarationAnnotation) {
00511             int modifiers = ((MethodDeclarationAnnotation) annotation).getSootMethod().getModifiers();
00512             if (Modifier.isStatic(modifiers)) {
00513                 isStatic = true;
00514                 if (node.getParams() instanceof AInstanceParams) {
00515                     exceptions.add(new BadPredicateDefinitionException("Cannot define instance invoke predicate in a static method"));
00516                 }
00517             } else {
00518                 isStatic = false;
00519                 if (!(node.getParams() instanceof AInstanceParams)) {
00520                     exceptions.add(new BadPredicateDefinitionException("Cannot define static invoke predicate in an instance method"));
00521                 }
00522             }
00523             if (Modifier.isNative(modifiers) || Modifier.isAbstract(modifiers)) {
00524                 exceptions.add(new BadPredicateDefinitionException("Location predicate cannot be in abstract/native method"));
00525                 try {
00526                     Predicate p = PredicateFactory.createLocationPredicate(new Name(name), type, annotation, node, node.getLabel().toString().trim(), params, paramTypes, isStatic, variablesUsed, node.getColonExp() != null ? ((AColonExp) node.getColonExp()).getExp() : null, buffer.toString(), exceptions);
00527                     p.setUsePrivate(usePrivate);
00528                 } catch (Exception e) {
00529                     exceptions.add(e);
00530                 }
00531                 exceptions = new Vector();
00532                 usedTypeNames = new Vector();
00533                 return;
00534             }
00535         }
00536         String label = node.getLabel().toString().trim();
00537         boolean found = false;
00538         for (Enumeration e = labeledStmtAnnotations.elements(); e.hasMoreElements();) {
00539             LabeledStmtAnnotation lsa = (LabeledStmtAnnotation) e.nextElement();
00540             if (lsa.getId().equals(label)) {
00541                 currentAnnotation = lsa;
00542                 found = true;
00543                 break;
00544             }
00545         }
00546         if (!found) {
00547             exceptions.add(new BadPredicateDefinitionException("Invalid label '" + label + "'"));
00548             try {
00549                 Predicate p = PredicateFactory.createLocationPredicate(new Name(name), type, annotation, node, node.getLabel().toString().trim(), params, paramTypes, isStatic, variablesUsed, node.getColonExp() != null ? ((AColonExp) node.getColonExp()).getExp() : null, buffer.toString(), exceptions);
00550                 p.setUsePrivate(usePrivate);
00551             } catch (Exception e) {
00552                 exceptions.add(e);
00553             }
00554             exceptions = new Vector();
00555             usedTypeNames = new Vector();
00556             return;
00557         }
00558         if (node.getColonExp() != null) {
00559             node.getColonExp().apply(this);
00560             if (currentType != BooleanType.TYPE) {
00561                 exceptions.add(new BadPredicateDefinitionException("Location predicate constraint should be of type boolean"));
00562             }
00563         }
00564     }
00565     try {
00566         Predicate p = PredicateFactory.createLocationPredicate(new Name(name), type, annotation, node, node.getLabel().toString().trim(), params, paramTypes, isStatic, variablesUsed, node.getColonExp() != null ? ((AColonExp) node.getColonExp()).getExp() : null, buffer.toString(), exceptions);
00567         p.setUsePrivate(usePrivate);
00568     } catch (Exception e) {
00569         exceptions.add(e);
00570     }
00571     exceptions = new Vector();
00572     usedTypeNames = new Vector();
00573 }
00574 /**
00575  * 
00576  * @param node edu.ksu.cis.bandera.predicate.node.ANameExp
00577  */
00578 public void caseANameExp(ANameExp node) {
00579     if (node.getName() instanceof ASimpleName) {
00580         Hashtable visibleLocals = getDeclaredLocals();
00581         String local = node.getName().toString().trim();
00582         if (params.contains(local)) {
00583             currentType = (Type) paramTypes.elementAt(params.indexOf(local));
00584             variablesUsed.put(node, local);
00585         } else {
00586             Name localOrFieldName = new Name(local);
00587             Local lcl = (Local) visibleLocals.get(local);
00588             if (lcl != null) {
00589                 try {
00590                     currentType = Util.convertType(lcl.getType(), symbolTable);
00591                     variablesUsed.put(node, lcl);
00592                 } catch (Exception e) {
00593                     exceptions.add(e);
00594                 }
00595             } else {
00596                 try {
00597                     Field f = type.getField(localOrFieldName);
00598                     currentType = f.getType();
00599                     if (isStatic && !java.lang.reflect.Modifier.isStatic(f.getModifiers())) {
00600                         TId id = ((ASimpleName) node.getName()).getId();
00601                         exceptions.add(new BadPredicateDefinitionException("Cannot refer to instance field '" + id.toString().trim() + "' in a static predicate"));
00602                     } else {
00603                         if (java.lang.reflect.Modifier.isPrivate(f.getModifiers())) {
00604                             usePrivate = true;
00605                         }
00606                         variablesUsed.put(node, f);
00607                     }
00608                 } catch (Exception e) {
00609                     try {
00610                         currentType = symbolTable.resolveType(new Name(node.getName().toString()));
00611                     } catch (Exception e2) {
00612                         currentType = VoidType.TYPE;
00613                         exceptions.add(new TypeException("Unresolved name expression '" + localOrFieldName.toString() + "' in " + type.getFullyQualifiedName()));
00614                     }
00615                 }
00616             }
00617         }
00618     } else {
00619         Name name = new Name(node.getName().toString()).getSuperName();
00620         ClassOrInterfaceType type = null;
00621         PName typeName = ((AQualifiedName) node.getName()).getName();
00622         while (!name.isSimpleName()) {
00623             try {
00624                 type = (ClassOrInterfaceType) symbolTable.resolveType(name);
00625                 break;
00626             } catch (Exception e) {
00627                 name = name.getSuperName();
00628                 typeName = ((AQualifiedName) typeName).getName();
00629             }
00630         }
00631         if (type == null) {
00632             try {
00633                 type = (ClassOrInterfaceType) symbolTable.resolveType(name);
00634             } catch (Exception e) {
00635                 try {
00636                     currentType = (ClassOrInterfaceType) symbolTable.resolveType(new Name(node.getName().toString()));
00637                     usedTypeNames.add(node);
00638                     return;
00639                 } catch (Exception e2) {
00640                     PExp exp = buildNavigation((AQualifiedName) node.getName());
00641                     node.replaceBy(exp);
00642                     exp.apply(this);
00643                     return;
00644                 }
00645             }
00646         }
00647         String nameExp = new Name(node.getName().toString()).toString();
00648         nameExp = nameExp.substring(type.getFullyQualifiedName().length() + 1);
00649         PExp exp = buildNavigation(new ANameExp(typeName), nameExp);
00650         node.replaceBy(exp);
00651         exp.apply(this);
00652     }
00653 }
00654 /**
00655  * 
00656  * @param node edu.ksu.cis.bandera.predicate.node.ANegativeExp
00657  */
00658 public void caseANegativeExp(ANegativeExp node) {
00659     node.getExp().apply(this);
00660     if (!(currentType instanceof NumericType)) {
00661         currentType = IntType.TYPE;
00662         exceptions.add(new TypeException("Expecting numeric expression for unary operator -"));
00663     }
00664 }
00665 /**
00666  * 
00667  * @param node edu.ksu.cis.bandera.bpdl.node.ANullLiteral
00668  */
00669 public void caseANullLiteral(ANullLiteral node) {
00670     currentType = NullType.TYPE;
00671 }
00672 /**
00673  * 
00674  * @param node edu.ksu.cis.bandera.bpdl.node.AOctIntLiteral
00675  */
00676 public void caseAOctIntLiteral(AOctIntLiteral node) {
00677     currentType = IntType.TYPE;
00678 }
00679 /**
00680  * 
00681  * @param node edu.ksu.cis.bandera.bpdl.node.AOctLongLiteral
00682  */
00683 public void caseAOctLongLiteral(AOctLongLiteral node) {
00684     currentType = LongType.TYPE;
00685 }
00686 /**
00687  * 
00688  * @param node edu.ksu.cis.bandera.specification.predicate.node.AParamParamList
00689  */
00690 public void caseAParamParamList(AParamParamList node) {
00691     Type type;
00692     try {
00693         type = symbolTable.resolveType(new Name(node.getName().toString()));
00694     } catch (Exception e) {
00695         exceptions.add(new TypeException("Invalid parameter type"));
00696         return;
00697     }
00698     int i;
00699     if ((i = node.getDim().toArray().length) > 0) {
00700         type = new ArrayType(type, i);
00701     }
00702 
00703     paramTypes.add(type);
00704     params.add(node.getId().toString().trim());
00705 }
00706 /**
00707  * 
00708  * @param node edu.ksu.cis.bandera.specification.predicate.node.AParamsParamList
00709  */
00710 public void caseAParamsParamList(AParamsParamList node) {
00711     node.getParamList().apply(this);
00712     Type type;
00713     try {
00714         type = symbolTable.resolveType(new Name(node.getName().toString()));
00715     } catch (Exception e) {
00716         exceptions.add(new TypeException("Invalid parameter type"));
00717         return;
00718     }
00719     int i;
00720     if ((i = node.getDim().toArray().length) > 0) {
00721         type = new ArrayType(type, i);
00722     }
00723 
00724     paramTypes.add(type);
00725     params.add(node.getId().toString().trim());
00726 }
00727 /**
00728  * 
00729  * @param node edu.ksu.cis.bandera.predicate.node.AParenExp
00730  */
00731 public void caseAParenExp(AParenExp node) {
00732     super.caseAParenExp(node);
00733 }
00734 /**
00735  * 
00736  * @param node edu.ksu.cis.bandera.predicate.node.AQuestionExp
00737  */
00738 public void caseAQuestionExp(AQuestionExp node) {
00739     node.getExp().apply(this);
00740     if (currentType != BooleanType.TYPE) {
00741         exceptions.add(new TypeException("Expecting a boolean expression for ?: expression"));
00742     }
00743     node.getTrueExp().apply(this);
00744     Type trueType = currentType;
00745     node.getFalseExp().apply(this);
00746     Type falseType = currentType;
00747 
00748     boolean flag = true;
00749     if (trueType == falseType) {
00750         currentType = trueType;
00751     } else if (trueType instanceof NumericType) {
00752         if (((trueType == ByteType.TYPE) && (falseType == ShortType.TYPE))
00753                 || ((trueType == ShortType.TYPE) && (falseType == ByteType.TYPE))) {
00754             currentType = ShortType.TYPE;
00755         } else if (((trueType == ByteType.TYPE) || (trueType == ShortType.TYPE)
00756                 || (trueType == CharType.TYPE)) && (falseType == IntType.TYPE)
00757                 && (node.getFalseExp() instanceof ALiteralExp)) {
00758             currentType = trueType;
00759         } else if (((falseType == ByteType.TYPE) || (falseType == ShortType.TYPE)
00760                 || (falseType == CharType.TYPE)) && (trueType == IntType.TYPE)
00761                 && (node.getTrueExp() instanceof ALiteralExp)) {
00762             currentType = falseType;
00763         } else {
00764             currentType = getNumericType(trueType, falseType);
00765         }
00766     } else if ((trueType == NullType.TYPE) && (falseType instanceof ReferenceType)) {
00767         currentType = trueType;
00768     } else if ((trueType instanceof ReferenceType) && (falseType == NullType.TYPE)) {
00769         currentType = falseType;
00770     } else if ((trueType instanceof ReferenceType) && (falseType instanceof ReferenceType)) {
00771         if (trueType.isValidIdentityConversion(falseType)
00772                 && trueType.isValidWideningConversion(falseType)) {
00773             currentType = falseType;
00774         } else if (falseType.isValidIdentityConversion(trueType)
00775                 && falseType.isValidWideningConversion(trueType)) {
00776             currentType = trueType;
00777         } else flag = false;
00778     } else {
00779         flag = false;
00780     }
00781 
00782     if (!flag) {
00783         currentType = VoidType.TYPE;
00784         exceptions.add(new TypeException("Type mismatch in question expression"));
00785     }
00786 }
00787 /**
00788  * 
00789  * @param node edu.ksu.cis.bandera.bpdl.node.AReturnPropositionDefinition
00790  */
00791 public void caseAReturnPropositionDefinition(AReturnPropositionDefinition node) {
00792     usePrivate = false;
00793     variablesUsed = new Hashtable();
00794     buffer = new StringBuffer();
00795     if (node.getComment() != null) {
00796         for (Iterator i = node.getComment().iterator(); i.hasNext();) {
00797             ((PComment) i.next()).apply(this);
00798         }
00799     }
00800     String name = predName + "." + node.getId().toString().trim();
00801     params = new Vector();
00802     paramTypes = new Vector();
00803     
00804     if (node.getParams() != null) {
00805         node.getParams().apply(this);
00806     }
00807     if (annotation == null) {
00808         exceptions.add(new BadPredicateDefinitionException("Return predicate cannot be in class level"));
00809     } else {
00810         mode = RETURN;
00811         ret = false;
00812         
00813         if (annotation instanceof MethodDeclarationAnnotation) {
00814             int modifiers = ((MethodDeclarationAnnotation) annotation).getSootMethod().getModifiers();
00815             if (Modifier.isStatic(modifiers)) {
00816                 isStatic = true;
00817                 if (node.getParams() instanceof AInstanceParams) {
00818                     exceptions.add(new BadPredicateDefinitionException("Cannot define instance invoke predicate in a static method"));
00819                 }
00820             } else {
00821                 isStatic = false;
00822                 if (!(node.getParams() instanceof AInstanceParams)) {
00823                     exceptions.add(new BadPredicateDefinitionException("Cannot define static invoke predicate in an instance method"));
00824                 }
00825             }
00826             if (Modifier.isNative(modifiers)) {
00827                 exceptions.add(new BadPredicateDefinitionException("Return predicate cannot be in abstract/native method"));
00828                 try {
00829                     Predicate p = PredicateFactory.createReturnPredicate(new Name(name), type, annotation, node, params, paramTypes, isStatic, ret, variablesUsed, node.getColonExp() != null ? ((AColonExp) node.getColonExp()).getExp() : null, buffer.toString(), exceptions);
00830                     p.setUsePrivate(usePrivate);
00831                 } catch (Exception e) {
00832                     exceptions.add(e);
00833                 }
00834                 exceptions = new Vector();
00835                 usedTypeNames = new Vector();
00836                 return;
00837             }
00838         }
00839         
00840         if (node.getColonExp() != null) {
00841             node.getColonExp().apply(this);
00842             if (currentType != BooleanType.TYPE) {
00843                 exceptions.add(new BadPredicateDefinitionException("Return predicate constraint should be type boolean"));
00844             }
00845         }
00846     }
00847     try {
00848         Predicate p = PredicateFactory.createReturnPredicate(new Name(name), type, annotation, node, params, paramTypes, isStatic, ret, variablesUsed, node.getColonExp() != null ? ((AColonExp) node.getColonExp()).getExp() : null, buffer.toString(), exceptions);
00849         p.setUsePrivate(usePrivate);
00850     } catch (Exception e) {
00851         exceptions.add(e);
00852     }
00853     exceptions = new Vector();
00854     usedTypeNames = new Vector();
00855 }
00856 /**
00857  * 
00858  * @param node edu.ksu.cis.bandera.predicate.node.AReturnValueExp
00859  */
00860 public void caseAReturnValueExp(AReturnValueExp node) {
00861     if (mode != RETURN) {
00862         exceptions.add(new BadPredicateDefinitionException("Can only have " + node.getRetVal().toString() + "in return predicate"));
00863         currentType = VoidType.TYPE;
00864         return;
00865     }
00866 
00867     if (annotation instanceof ConstructorDeclarationAnnotation) {
00868         exceptions.add(new BadPredicateDefinitionException("Cannot use " + node.getRetVal().toString() + "in a constructor return predicate"));
00869         currentType = VoidType.TYPE;
00870         return;
00871     }
00872 
00873     currentType = ((MethodDeclarationAnnotation) annotation).getMethod().getReturnType();
00874     ret = true;
00875 }
00876 /**
00877  * 
00878  * @param node edu.ksu.cis.bandera.bpdl.node.AStringLiteral
00879  */
00880 public void caseAStringLiteral(AStringLiteral node) {
00881     try {
00882         currentType = Package.getClassOrInterfaceType(new Name("java.lang.String"));
00883     } catch (Exception e) {
00884         exceptions.add(e);
00885     }
00886 }
00887 /**
00888  * 
00889  * @param node edu.ksu.cis.bandera.predicate.node.AStrongArrayNavigation
00890  */
00891 public void caseAStrongArrayNavigation(AStrongArrayNavigation node) {
00892     Type baseType = currentType;
00893     node.getExp().apply(this);
00894     if (currentType instanceof IntegralType) {
00895         if (baseType instanceof ArrayType) {
00896             if (((ArrayType) baseType).nDimensions == 1) {
00897                 currentType = ((ArrayType) baseType).baseType;
00898             } else {
00899                 currentType = new ArrayType(((ArrayType) baseType).baseType, ((ArrayType) baseType).nDimensions - 1);
00900             }
00901         } else {
00902             exceptions.add(new TypeException("Not an array in array access"));
00903             currentType = VoidType.TYPE;
00904         }
00905     } else {
00906         exceptions.add(new TypeException("Not a numeric type in array access"));
00907         currentType = VoidType.TYPE;
00908     }
00909 }
00910 /**
00911  * 
00912  * @param node edu.ksu.cis.bandera.predicate.node.AStrongCastExp
00913  */
00914 public void caseAStrongCastExp(AStrongCastExp node) {
00915     currentType = VoidType.TYPE;
00916     Type cast;
00917     try {
00918         cast = symbolTable.resolveType(new Name(node.getType().toString()));
00919     } catch (Exception e) {
00920         exceptions.add(new TypeException("Invalid casting type"));
00921         return;
00922     }
00923     int i;
00924     if ((i = node.getDim().toArray().length) > 0) {
00925         cast = new ArrayType(cast, i);
00926     }
00927     node.getExp().apply(this);
00928     if (!currentType.isValidCastingConversion(cast)) {
00929         exceptions.add(new TypeException("Invalid casting type"));
00930     }
00931     variablesUsed.put(node, cast);
00932     currentType = cast;
00933 }
00934 /**
00935  * 
00936  * @param node edu.ksu.cis.bandera.predicate.node.AStrongObjectNavigation
00937  */
00938 public void caseAStrongObjectNavigation(AStrongObjectNavigation node) {
00939     String id = node.getId().toString().trim();
00940     if ("length".equals(id) && (currentType instanceof ArrayType)) {
00941         currentType = IntType.TYPE;
00942     } else if (currentType instanceof ClassOrInterfaceType) {
00943         try {
00944             Field f = ((ClassOrInterfaceType) currentType).getField(new Name(id));
00945             currentType = f.getType();
00946             variablesUsed.put(node, f);
00947             if (usedTypeNames.contains(((ANavigationExp) node.parent()).getExp())) {
00948                 if (!f.isAccessible(type)) {
00949                     exceptions.add(new TypeException("Field '"
00950                             + currentType.getFullyQualifiedName() + "." +  f.getName()
00951                             + "' is from accessible from '" + type.getFullyQualifiedName()));
00952                     currentType = VoidType.TYPE;
00953                 }
00954             }
00955         } catch (Exception e) {
00956             exceptions.add(new TypeException("Field undefined"));
00957             currentType = VoidType.TYPE;
00958         }
00959     } else {
00960         exceptions.add(new TypeException("Not an object in field access"));
00961         currentType = VoidType.TYPE;
00962     }
00963 }
00964 /**
00965  * 
00966  * @param node edu.ksu.cis.bandera.predicate.node.AThisExp
00967  */
00968 public void caseAThisExp(AThisExp node) {
00969     if (isStatic) {
00970         exceptions.add(new BadPredicateDefinitionException("Cannot have " + node.getThis().toString() + "in non-static predicate"));
00971         currentType = NullType.TYPE;
00972         return;
00973     }
00974     variablesUsed.put(node, "this");
00975     if (annotation instanceof MethodDeclarationAnnotation) {
00976         try {
00977             currentType =
00978                     ((MethodDeclarationAnnotation) annotation).getMethod().getDeclaringClassOrInterface();
00979         } catch (Exception e) {}
00980     } else if (annotation instanceof ConstructorDeclarationAnnotation) {
00981         try {
00982             currentType =
00983                     ((ConstructorDeclarationAnnotation) annotation).getConstructor().getDeclaringClassOrInterface();
00984         } catch (Exception e) {}
00985     } else {
00986         currentType = type;
00987     }
00988 }
00989 /**
00990  * 
00991  * @param node edu.ksu.cis.bandera.bpdl.node.ATrueLiteral
00992  */
00993 public void caseATrueLiteral(ATrueLiteral node) {
00994     currentType = BooleanType.TYPE;
00995 }
00996 /**
00997  * 
00998  * @param node edu.ksu.cis.bandera.bpdl.node.AUnit
00999  */
01000 public void caseAUnit(AUnit node) {
01001     if(node.getName() != null) {
01002         predName = new Name(node.getName().toString()).toString().trim();
01003     } else {
01004         if (annotation != null) {
01005             if (annotation instanceof MethodDeclarationAnnotation) {
01006                 MethodDeclarationAnnotation mda = (MethodDeclarationAnnotation) annotation;
01007                 try {
01008                     predName = mda.getMethod().getDeclaringClassOrInterface().getFullyQualifiedName()
01009                             + "." + mda.getMethod().getName().toString();
01010                 } catch (Exception e) {
01011                     throw new RuntimeException("Fatal Error");
01012                 }
01013             } else {
01014                 ConstructorDeclarationAnnotation cda = (ConstructorDeclarationAnnotation) annotation;
01015                 try {
01016                     predName = cda.getConstructor().getDeclaringClassOrInterface().getFullyQualifiedName()
01017                             + "." + cda.getConstructor().getDeclaringClassOrInterface().getName().getLastIdentifier();
01018                 } catch (Exception e) {
01019                     throw new RuntimeException("Fatal Error");
01020                 }
01021             }
01022         } else {
01023             predName = type.getFullyQualifiedName();
01024         }
01025     }
01026     super.caseAUnit(node);
01027 }
01028 /**
01029  * 
01030  */
01031 public void check() {
01032     node.apply(this);
01033 }
01034 /**
01035  * 
01036  * @return java.util.Hashtable
01037  */
01038 private Hashtable getDeclaredLocals() {
01039     if (mode == LOCATION) {
01040         Hashtable visibleLocals;
01041         if (annotation instanceof MethodDeclarationAnnotation) {
01042             visibleLocals = ((MethodDeclarationAnnotation) annotation).getParameterLocals();
01043         } else {
01044             visibleLocals = ((ConstructorDeclarationAnnotation) annotation).getParameterLocals();
01045         }
01046         for (Enumeration e = currentAnnotation.getDeclaredLocalVariables().elements();
01047                 e.hasMoreElements();) {
01048             Local l = (Local) e.nextElement();
01049             visibleLocals.put(l.getName().trim(), l);
01050         }
01051         return visibleLocals;
01052     } else if (mode != EXP) {
01053         if (annotation instanceof MethodDeclarationAnnotation) {
01054             return ((MethodDeclarationAnnotation) annotation).getParameterLocals();
01055         } else {
01056             return ((ConstructorDeclarationAnnotation) annotation).getParameterLocals();
01057         }
01058     } else {
01059         return new Hashtable();
01060     }
01061 }
01062 /**
01063  * 
01064  * @return edu.ksu.cis.bandera.jjjc.symboltable.Type
01065  * @param leftType edu.ksu.cis.bandera.jjjc.symboltable.Type
01066  * @param rightType edu.ksu.cis.bandera.jjjc.symboltable.Type
01067  */
01068 private Type getIntegralType(Type leftType, Type rightType) {
01069     if (!(leftType instanceof IntegralType) || !(rightType instanceof IntegralType))
01070         return null;
01071     if ((leftType == LongType.TYPE) || (rightType == LongType.TYPE))
01072         return LongType.TYPE;
01073     else if ((leftType instanceof IntegralType) || (rightType instanceof IntegralType))
01074         return IntType.TYPE;
01075     else return null;
01076 }
01077 /**
01078  * 
01079  * @return edu.ksu.cis.bandera.jjjc.symboltable.Type
01080  * @param leftType edu.ksu.cis.bandera.jjjc.symboltable.Type
01081  * @param rightType edu.ksu.cis.bandera.jjjc.symboltable.Type
01082  */
01083 private Type getNumericType(Type leftType, Type rightType) {
01084     if (!(leftType instanceof NumericType) || !(rightType instanceof NumericType))
01085         return null;
01086     if ((leftType == LongType.TYPE) || (rightType == LongType.TYPE))
01087         return LongType.TYPE;
01088     else if ((leftType == FloatType.TYPE) || (rightType == FloatType.TYPE))
01089         return FloatType.TYPE;
01090     else if ((leftType == DoubleType.TYPE) || (rightType == DoubleType.TYPE))
01091         return DoubleType.TYPE;
01092     else if ((leftType instanceof IntegralType) || (rightType instanceof IntegralType))
01093         return IntType.TYPE;
01094     else return null;
01095 }
01096 }