From 40e9b64bbc6a8a2c1feacba48f30b7059238e912 Mon Sep 17 00:00:00 2001 From: yeom Date: Wed, 20 Jul 2011 21:50:05 +0000 Subject: [PATCH] fixes on method annoatation checking: when a method needs to be annotated, all of its parent method needs to be annotated. If a parent method is abstract, at least needs to have annotations for method declaration. --- Robust/src/Analysis/SSJava/FlowDownCheck.java | 194 +++++++++++------- .../SSJava/MethodAnnotationCheck.java | 30 ++- .../src/Analysis/SSJava/SSJavaAnalysis.java | 7 +- .../ssJava/mp3decoder/LayerIDecoder.java | 6 +- .../src/Tests/ssJava/mp3decoder/Obuffer.java | 4 +- .../src/Tests/ssJava/mp3decoder/Subband.java | 13 +- 6 files changed, 169 insertions(+), 85 deletions(-) diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java index 4589aaca..41439daa 100644 --- a/Robust/src/Analysis/SSJava/FlowDownCheck.java +++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java @@ -100,16 +100,17 @@ public class FlowDownCheck { // desciptor' & 'location' toanalyze.addAll(classtable.getValueSet()); toanalyze.addAll(state.getTaskSymbolTable().getValueSet()); + while (!toanalyze.isEmpty()) { Object obj = toanalyze.iterator().next(); ClassDescriptor cd = (ClassDescriptor) obj; toanalyze.remove(cd); - if (ssjava.needToBeAnnoated(cd) && (!cd.isInterface())) { + if (ssjava.needToBeAnnoated(cd)) { ClassDescriptor superDesc = cd.getSuperDesc(); - if (superDesc != null && (!superDesc.isInterface()) - && (!superDesc.getSymbol().equals("Object"))) { + + if (superDesc != null && (!superDesc.getSymbol().equals("Object"))) { checkOrderingInheritance(superDesc, cd); } @@ -151,7 +152,8 @@ public class FlowDownCheck { SSJavaLattice subLattice = ssjava.getClassLattice(cd); if (superLattice != null) { - + // if super class doesn't define lattice, then we don't need to check its + // subclass if (subLattice == null) { throw new Error("If a parent class '" + superCd + "' has a ordering lattice, its subclass '" + cd + "' should have one."); @@ -169,10 +171,32 @@ public class FlowDownCheck { + "' that is defined by its superclass '" + superCd + "'."); } } + } + + MethodLattice superMethodDefaultLattice = ssjava.getMethodDefaultLattice(superCd); + MethodLattice subMethodDefaultLattice = ssjava.getMethodDefaultLattice(cd); + + if (superMethodDefaultLattice != null) { + if (subMethodDefaultLattice == null) { + throw new Error("When a parent class '" + superCd + + "' defines a default method lattice, its subclass '" + cd + "' should define one."); + } + + Set> superPairSet = superMethodDefaultLattice.getOrderingPairSet(); + Set> subPairSet = subMethodDefaultLattice.getOrderingPairSet(); + + for (Iterator iterator = superPairSet.iterator(); iterator.hasNext();) { + Pair pair = (Pair) iterator.next(); + + if (!subPairSet.contains(pair)) { + throw new Error("Subclass '" + cd + "' does not have the relative ordering '" + + pair.getSecond() + " < " + pair.getFirst() + + "' that is defined by its superclass '" + superCd + + "' in the method default lattice."); + } + } } - // if super class doesn't define lattice, then we don't need to check its - // subclass } @@ -183,9 +207,9 @@ public class FlowDownCheck { private void checkDeclarationInMethodBody(ClassDescriptor cd, MethodDescriptor md) { BlockNode bn = state.getMethodBody(md); - // parsing returnloc annotation if (ssjava.needTobeAnnotated(md)) { + // parsing returnloc annotation Vector methodAnnotations = md.getModifiers().getAnnotations(); if (methodAnnotations != null) { for (int i = 0; i < methodAnnotations.size(); i++) { @@ -198,44 +222,42 @@ public class FlowDownCheck { md2ReturnLoc.put(md, returnLocComp); } } - if (!md.getReturnType().isVoid() && !md2ReturnLoc.containsKey(md)) { throw new Error("Return location is not specified for the method " + md + " at " + cd.getSourceFileName()); } - } - } - List paramList = new ArrayList(); + List paramList = new ArrayList(); - boolean hasReturnValue = (!md.getReturnType().isVoid()); - if (hasReturnValue) { - MethodLattice methodLattice = ssjava.getMethodLattice(md); - String thisLocId = methodLattice.getThisLoc(); - if (thisLocId == null) { - throw new Error("Method '" + md + "' does not have the definition of 'this' location at " - + md.getClassDesc().getSourceFileName()); + boolean hasReturnValue = (!md.getReturnType().isVoid()); + if (hasReturnValue) { + MethodLattice methodLattice = ssjava.getMethodLattice(md); + String thisLocId = methodLattice.getThisLoc(); + if (thisLocId == null) { + throw new Error("Method '" + md + "' does not have the definition of 'this' location at " + + md.getClassDesc().getSourceFileName()); + } + CompositeLocation thisLoc = new CompositeLocation(new Location(md, thisLocId)); + paramList.add(thisLoc); } - CompositeLocation thisLoc = new CompositeLocation(new Location(md, thisLocId)); - paramList.add(thisLoc); - } - for (int i = 0; i < md.numParameters(); i++) { - // process annotations on method parameters - VarDescriptor vd = (VarDescriptor) md.getParameter(i); - assignLocationOfVarDescriptor(vd, md, md.getParameterTable(), bn); - if (hasReturnValue) { - paramList.add(d2loc.get(vd)); + for (int i = 0; i < md.numParameters(); i++) { + // process annotations on method parameters + VarDescriptor vd = (VarDescriptor) md.getParameter(i); + assignLocationOfVarDescriptor(vd, md, md.getParameterTable(), bn); + if (hasReturnValue) { + paramList.add(d2loc.get(vd)); + } } - } - if (hasReturnValue) { - md2ReturnLocGen.put(md, new ReturnLocGenerator(md2ReturnLoc.get(md), paramList, - generateErrorMessage(cd, null))); + if (hasReturnValue) { + md2ReturnLocGen.put(md, new ReturnLocGenerator(md2ReturnLoc.get(md), paramList, + generateErrorMessage(cd, null))); + } + checkDeclarationInBlockNode(md, md.getParameterTable(), bn); } - checkDeclarationInBlockNode(md, md.getParameterTable(), bn); } private void checkDeclarationInBlockNode(MethodDescriptor md, SymbolTable nametable, BlockNode bn) { @@ -403,15 +425,26 @@ public class FlowDownCheck { ExpressionNode returnExp = rn.getReturnExpression(); - CompositeLocation expLoc; + CompositeLocation returnValueLoc; if (returnExp != null) { - expLoc = checkLocationFromExpressionNode(md, nametable, returnExp, new CompositeLocation()); + returnValueLoc = + checkLocationFromExpressionNode(md, nametable, returnExp, new CompositeLocation()); + // check if return value is equal or higher than RETRUNLOC of method // declaration annotation - CompositeLocation returnLocAt = md2ReturnLoc.get(md); + CompositeLocation declaredReturnLoc = md2ReturnLoc.get(md); - if (CompositeLattice - .compare(returnLocAt, expLoc, generateErrorMessage(md.getClassDesc(), rn)) != ComparisonResult.LESS) { + System.out.println("\nreturnLocAt=" + declaredReturnLoc); + System.out.println("returnValueLoc=" + returnValueLoc); + System.out.println("COMPARE RESULT=" + + CompositeLattice.compare(declaredReturnLoc, returnValueLoc, + generateErrorMessage(md.getClassDesc(), rn))); + + int compareResult = + CompositeLattice.compare(returnValueLoc, declaredReturnLoc, + generateErrorMessage(md.getClassDesc(), rn)); + + if (compareResult == ComparisonResult.LESS || compareResult == ComparisonResult.INCOMPARABLE) { throw new Error( "Return value location is not equal or higher than the declaraed return location at " + md.getClassDesc().getSourceFileName() + "::" + rn.getNumLine()); @@ -563,13 +596,15 @@ public class FlowDownCheck { private CompositeLocation checkLocationFromDeclarationNode(MethodDescriptor md, SymbolTable nametable, DeclarationNode dn) { - System.out.println("DeclarationNode=" + dn.printNode(0) + " " + System.out.println("##DeclarationNode=" + dn.printNode(0) + " " + generateErrorMessage(md.getClassDesc(), dn)); VarDescriptor vd = dn.getVarDescriptor(); CompositeLocation destLoc = d2loc.get(vd); + System.out.println("##DeclarationNode destLoc=" + destLoc + " of vd=" + vd + " of md=" + md); + if (dn.getExpression() != null) { CompositeLocation expressionLoc = checkLocationFromExpressionNode(md, nametable, dn.getExpression(), @@ -772,9 +807,9 @@ public class FlowDownCheck { } System.out.println("##"); - System.out.println("min.getMethod()=" + min.getMethod()); - System.out.println("md2ReturnLocGen.get(min.getMethod())=" - + md2ReturnLocGen.get(min.getMethod())); + System.out.println("min.getMethod()=" + min.getMethod() + " argList=" + argList); + System.out.println("computeReturnLocation=" + + md2ReturnLocGen.get(min.getMethod()).computeReturnLocation(argList)); return md2ReturnLocGen.get(min.getMethod()).computeReturnLocation(argList); @@ -783,6 +818,8 @@ public class FlowDownCheck { private void checkCalleeConstraints(MethodDescriptor md, SymbolTable nametable, MethodInvokeNode min) { + System.out.println("checkCalleeConstraints " + generateErrorMessage(md.getClassDesc(), min)); + if (min.numArgs() > 1) { // caller needs to guarantee that it passes arguments in regarding to // callee's hierarchy @@ -808,12 +845,16 @@ public class FlowDownCheck { VarDescriptor calleevd2 = (VarDescriptor) min.getMethod().getParameter(currentIdx); CompositeLocation calleeLoc2 = d2loc.get(calleevd2); + System.out.println("#callerResult=" + callerArg1 + " " + callerArg2); + System.out.println("#calleeResult=" + calleeLoc1 + " " + calleeLoc2); + int callerResult = CompositeLattice.compare(callerArg1, callerArg2, generateErrorMessage(md.getClassDesc(), min)); int calleeResult = CompositeLattice.compare(calleeLoc1, calleeLoc2, generateErrorMessage(md.getClassDesc(), min)); + if (calleeResult == ComparisonResult.GREATER && callerResult != ComparisonResult.GREATER) { // If calleeLoc1 is higher than calleeLoc2 @@ -1088,12 +1129,13 @@ public class FlowDownCheck { } srcLocation = new CompositeLocation(); srcLocation = checkLocationFromExpressionNode(md, nametable, an.getSrc(), srcLocation); - -// System.out.println(" an= " + an.printNode(0) + " an.getSrc()=" + an.getSrc().getClass() -// + " at " + cd.getSourceFileName() + "::" + an.getNumLine()); -// System.out.println("srcLocation=" + srcLocation); -// System.out.println("dstLocation=" + destLocation); - + + // System.out.println(" an= " + an.printNode(0) + " an.getSrc()=" + + // an.getSrc().getClass() + // + " at " + cd.getSourceFileName() + "::" + an.getNumLine()); + // System.out.println("srcLocation=" + srcLocation); + // System.out.println("dstLocation=" + destLocation); + if (!CompositeLattice.isGreaterThan(srcLocation, destLocation, generateErrorMessage(cd, an))) { throw new Error("The value flow from " + srcLocation + " to " + destLocation + " does not respect location hierarchy on the assignment " + an.printNode(0) + " at " @@ -1120,41 +1162,39 @@ public class FlowDownCheck { ClassDescriptor cd = md.getClassDesc(); Vector annotationVec = vd.getType().getAnnotationMarkers(); - if (!md.getModifiers().isAbstract()) { - // currently enforce every variable to have corresponding location - if (annotationVec.size() == 0) { - throw new Error("Location is not assigned to variable " + vd.getSymbol() - + " in the method " + md.getSymbol() + " of the class " + cd.getSymbol()); - } - - if (annotationVec.size() > 1) { // variable can have at most one location - throw new Error(vd.getSymbol() + " has more than one location."); - } + // currently enforce every variable to have corresponding location + if (annotationVec.size() == 0) { + throw new Error("Location is not assigned to variable " + vd.getSymbol() + " in the method " + + md.getSymbol() + " of the class " + cd.getSymbol()); + } - AnnotationDescriptor ad = annotationVec.elementAt(0); + if (annotationVec.size() > 1) { // variable can have at most one location + throw new Error(vd.getSymbol() + " has more than one location."); + } - if (ad.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) { + AnnotationDescriptor ad = annotationVec.elementAt(0); - if (ad.getMarker().equals(SSJavaAnalysis.LOC)) { - String locDec = ad.getValue(); // check if location is defined + if (ad.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) { - if (locDec.startsWith(SSJavaAnalysis.DELTA)) { - DeltaLocation deltaLoc = parseDeltaDeclaration(md, n, locDec); - d2loc.put(vd, deltaLoc); - addLocationType(vd.getType(), deltaLoc); - } else { - CompositeLocation compLoc = parseLocationDeclaration(md, n, locDec); + if (ad.getMarker().equals(SSJavaAnalysis.LOC)) { + String locDec = ad.getValue(); // check if location is defined - Location lastElement = compLoc.get(compLoc.getSize() - 1); - if (ssjava.isSharedLocation(lastElement)) { - ssjava.mapSharedLocation2Descriptor(lastElement, vd); - } + if (locDec.startsWith(SSJavaAnalysis.DELTA)) { + DeltaLocation deltaLoc = parseDeltaDeclaration(md, n, locDec); + d2loc.put(vd, deltaLoc); + addLocationType(vd.getType(), deltaLoc); + } else { + CompositeLocation compLoc = parseLocationDeclaration(md, n, locDec); - d2loc.put(vd, compLoc); - addLocationType(vd.getType(), compLoc); + Location lastElement = compLoc.get(compLoc.getSize() - 1); + if (ssjava.isSharedLocation(lastElement)) { + ssjava.mapSharedLocation2Descriptor(lastElement, vd); } + d2loc.put(vd, compLoc); + addLocationType(vd.getType(), compLoc); } + } } @@ -1361,7 +1401,7 @@ public class FlowDownCheck { public static int compare(CompositeLocation loc1, CompositeLocation loc2, String msg) { - // System.out.println("compare=" + loc1 + " " + loc2); + System.out.println("compare=" + loc1 + " " + loc2); int baseCompareResult = compareBaseLocationSet(loc1, loc2, false, msg); if (baseCompareResult == ComparisonResult.EQUAL) { @@ -1691,6 +1731,12 @@ class ReturnLocGenerator { // compute GLB of arguments subset that are same or higher than return // location CompositeLocation glb = CompositeLattice.calculateGLB(inputGLB); + + System.out.println("### computeReturnLocation"); + System.out.println("### args=" + args); + System.out.println("### calculateGLB=" + inputGLB); + System.out.println("### glb=" + glb); + return glb; } } diff --git a/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java b/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java index f8145c56..d1914e02 100644 --- a/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java +++ b/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java @@ -92,7 +92,6 @@ public class MethodAnnotationCheck { if (calleeMD.getClassDesc().isInterface()) { calleeMD.getClassDesc(); - } tovisit.add(calleeMD); @@ -150,6 +149,35 @@ public class MethodAnnotationCheck { } } } + + // need to check super classess if the current method is inherited from + // them, all of ancestor method should be annoated + ClassDescriptor currentCd = cd; + ClassDescriptor superCd = tu.getSuper(currentCd); + while (!superCd.getSymbol().equals("Object")) { + Set possiblematches = superCd.getMethodTable().getSet(md.getSymbol()); + for (Iterator methodit = possiblematches.iterator(); methodit.hasNext();) { + MethodDescriptor matchmd = (MethodDescriptor) methodit.next(); + if (md.matches(matchmd)) { + ssjava.addAnnotationRequire(matchmd); + } + } + currentCd = superCd; + superCd = tu.getSuper(currentCd); + } + + Set superIFSet = tu.getSuperIFs(cd); + for (Iterator iterator = superIFSet.iterator(); iterator.hasNext();) { + ClassDescriptor parentInterface = (ClassDescriptor) iterator.next(); + Set possiblematches = parentInterface.getMethodTable().getSet(md.getSymbol()); + for (Iterator methodit = possiblematches.iterator(); methodit.hasNext();) { + MethodDescriptor matchmd = (MethodDescriptor) methodit.next(); + if (md.matches(matchmd)) { + ssjava.addAnnotationRequire(matchmd); + } + } + } + } } diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java index 80468a94..17db8a82 100644 --- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java +++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java @@ -269,6 +269,10 @@ public class SSJavaAnalysis { return cd2lattice.get(cd); } + public MethodLattice getMethodDefaultLattice(ClassDescriptor cd) { + return cd2methodDefault.get(cd); + } + public MethodLattice getMethodLattice(MethodDescriptor md) { if (md2lattice.containsKey(md)) { return md2lattice.get(md); @@ -291,9 +295,10 @@ public class SSJavaAnalysis { public void addAnnotationRequire(MethodDescriptor md) { + ClassDescriptor cd = md.getClassDesc(); // if a method requires to be annotated, class containg that method also // requires to be annotated - annotationRequireClassSet.add(md.getClassDesc()); + annotationRequireClassSet.add(cd); annotationRequireSet.add(md); } diff --git a/Robust/src/Tests/ssJava/mp3decoder/LayerIDecoder.java b/Robust/src/Tests/ssJava/mp3decoder/LayerIDecoder.java index dfc39286..b3572bf1 100644 --- a/Robust/src/Tests/ssJava/mp3decoder/LayerIDecoder.java +++ b/Robust/src/Tests/ssJava/mp3decoder/LayerIDecoder.java @@ -189,7 +189,7 @@ * and in derived class for intensity stereo mode */ @LATTICE("S