From f26ede98db53248e03489398e158a5646e63680b Mon Sep 17 00:00:00 2001 From: yeom Date: Wed, 17 Aug 2011 23:18:16 +0000 Subject: [PATCH] bug fix on flow-down rule: check if all of assignments done by invoking method respect the current branch constraint --- .../Analysis/SSJava/CompositeLocation.java | 12 ++ Robust/src/Analysis/SSJava/FlowDownCheck.java | 148 ++++++++++++------ .../SSJava/MethodAnnotationCheck.java | 10 +- .../src/Analysis/SSJava/SSJavaAnalysis.java | 18 ++- 4 files changed, 124 insertions(+), 64 deletions(-) diff --git a/Robust/src/Analysis/SSJava/CompositeLocation.java b/Robust/src/Analysis/SSJava/CompositeLocation.java index 23982187..5308cb67 100644 --- a/Robust/src/Analysis/SSJava/CompositeLocation.java +++ b/Robust/src/Analysis/SSJava/CompositeLocation.java @@ -35,6 +35,18 @@ public class CompositeLocation implements TypeExtension { return locTuple.size() == 0; } + public boolean startsWith(CompositeLocation prefix) { + // tests if this composite location starts with the prefix + + for (int i = 0; i < prefix.getSize(); i++) { + if (!prefix.get(i).equals(get(i))) { + return false; + } + } + return true; + + } + public String toString() { String rtr = "CompLoc["; diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java index 0dfd8892..9d41b838 100644 --- a/Robust/src/Analysis/SSJava/FlowDownCheck.java +++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java @@ -222,7 +222,7 @@ public class FlowDownCheck { MethodDescriptor md = toAnalyzeMethodNext(); if (ssjava.needTobeAnnotated(md)) { System.out.println("SSJAVA: Checking assignments: " + md); - checkMethodBody(cd, md); + checkMethodBody(cd, md, null); } } } @@ -431,9 +431,10 @@ public class FlowDownCheck { checkDeclarationInBlockNode(md, nametable, ln.getBody()); } - private void checkMethodBody(ClassDescriptor cd, MethodDescriptor md) { + private void checkMethodBody(ClassDescriptor cd, MethodDescriptor md, + CompositeLocation constraints) { BlockNode bn = state.getMethodBody(md); - checkLocationFromBlockNode(md, md.getParameterTable(), bn, null); + checkLocationFromBlockNode(md, md.getParameterTable(), bn, constraints); } private String generateErrorMessage(ClassDescriptor cd, TreeNode tn) { @@ -832,42 +833,83 @@ public class FlowDownCheck { SymbolTable nametable, MethodInvokeNode min, CompositeLocation loc, CompositeLocation constraint) { - CompositeLocation baseLocation = null; - if (min.getExpression() != null) { - baseLocation = - checkLocationFromExpressionNode(md, nametable, min.getExpression(), - new CompositeLocation(), constraint, false); - } else { + ClassDescriptor cd = md.getClassDesc(); + MethodDescriptor calleeMD = min.getMethod(); + + if (!ssjava.isTrustMethod(calleeMD)) { + CompositeLocation baseLocation = null; + if (min.getExpression() != null) { + baseLocation = + checkLocationFromExpressionNode(md, nametable, min.getExpression(), + new CompositeLocation(), constraint, false); + } else { - if (min.getMethod().isStatic()) { - String globalLocId = ssjava.getMethodLattice(md).getGlobalLoc(); - if (globalLocId == null) { - throw new Error("Method lattice does not define global variable location at " - + generateErrorMessage(md.getClassDesc(), min)); + if (min.getMethod().isStatic()) { + String globalLocId = ssjava.getMethodLattice(md).getGlobalLoc(); + if (globalLocId == null) { + throw new Error("Method lattice does not define global variable location at " + + generateErrorMessage(md.getClassDesc(), min)); + } + baseLocation = new CompositeLocation(new Location(md, globalLocId)); + } else { + String thisLocId = ssjava.getMethodLattice(md).getThisLoc(); + baseLocation = new CompositeLocation(new Location(md, thisLocId)); } - baseLocation = new CompositeLocation(new Location(md, globalLocId)); - } else { - String thisLocId = ssjava.getMethodLattice(md).getThisLoc(); - baseLocation = new CompositeLocation(new Location(md, thisLocId)); + + } + + System.out.println("\n#checkLocationFromMethodInvokeNode=" + min.printNode(0) + + " baseLocation=" + baseLocation); + + int compareResult = + CompositeLattice.compare(constraint, baseLocation, true, generateErrorMessage(cd, min)); + + if (compareResult == ComparisonResult.LESS) { + throw new Error("Method invocation does not respect the current branch constraint at " + + generateErrorMessage(cd, min)); + } else if (compareResult != ComparisonResult.GREATER) { + // if the current constraint is higher than method's THIS location + // no need to check constraints! + CompositeLocation calleeConstraint = + translateCallerLocToCalleeLoc(calleeMD, baseLocation, constraint); + checkMethodBody(calleeMD.getClassDesc(), calleeMD, calleeConstraint); } - } - checkCalleeConstraints(md, nametable, min, baseLocation, constraint); + checkCalleeConstraints(md, nametable, min, baseLocation, constraint); - checkCallerArgumentLocationConstraints(md, nametable, min, baseLocation, constraint); + checkCallerArgumentLocationConstraints(md, nametable, min, baseLocation, constraint); - if (!min.getMethod().getReturnType().isVoid()) { - // If method has a return value, compute the highest possible return - // location in the caller's perspective - CompositeLocation ceilingLoc = - computeCeilingLocationForCaller(md, nametable, min, baseLocation, constraint); - return ceilingLoc; + if (!min.getMethod().getReturnType().isVoid()) { + // If method has a return value, compute the highest possible return + // location in the caller's perspective + CompositeLocation ceilingLoc = + computeCeilingLocationForCaller(md, nametable, min, baseLocation, constraint); + return ceilingLoc; + } } return new CompositeLocation(); } + private CompositeLocation translateCallerLocToCalleeLoc(MethodDescriptor calleeMD, + CompositeLocation calleeBaseLoc, CompositeLocation constraint) { + + CompositeLocation calleeConstraint = new CompositeLocation(); + + // if (constraint.startsWith(calleeBaseLoc)) { + // if the first part of constraint loc is matched with callee base loc + Location thisLoc = new Location(calleeMD, ssjava.getMethodLattice(calleeMD).getThisLoc()); + calleeConstraint.addLocation(thisLoc); + for (int i = calleeBaseLoc.getSize(); i < constraint.getSize(); i++) { + calleeConstraint.addLocation(constraint.get(i)); + } + + // } + + return calleeConstraint; + } + private void checkCallerArgumentLocationConstraints(MethodDescriptor md, SymbolTable nametable, MethodInvokeNode min, CompositeLocation callerBaseLoc, CompositeLocation constraint) { // if parameter location consists of THIS and FIELD location, @@ -969,18 +1011,17 @@ public class FlowDownCheck { } System.out.println("\n## computeReturnLocation=" + min.getMethod() + " argList=" + argList); - CompositeLocation compLoc = md2ReturnLocGen.get(min.getMethod()).computeReturnLocation(argList); - DeltaLocation delta = new DeltaLocation(compLoc, 1); - System.out.println("##computeReturnLocation=" + delta); + CompositeLocation ceilLoc = md2ReturnLocGen.get(min.getMethod()).computeReturnLocation(argList); + System.out.println("## ReturnLocation=" + ceilLoc); - return delta; + return ceilLoc; } private void checkCalleeConstraints(MethodDescriptor md, SymbolTable nametable, MethodInvokeNode min, CompositeLocation callerBaseLoc, CompositeLocation constraint) { - - System.out.println("checkCalleeConstraints="+min.printNode(0)); + + System.out.println("checkCalleeConstraints=" + min.printNode(0)); MethodDescriptor calleemd = min.getMethod(); @@ -1014,7 +1055,7 @@ public class FlowDownCheck { for (int i = 0; i < calleemd.numParameters(); i++) { VarDescriptor calleevd = (VarDescriptor) calleemd.getParameter(i); CompositeLocation calleeLoc = d2loc.get(calleevd); - System.out.println("calleevd="+calleevd+" loc="+calleeLoc); + System.out.println("calleevd=" + calleevd + " loc=" + calleeLoc); calleeParamList.add(calleeLoc); } @@ -1033,9 +1074,9 @@ public class FlowDownCheck { || callerLoc2.get(callerLoc2.getSize() - 1).isTop()) { continue CHECK; } - - System.out.println("calleeLoc1="+calleeLoc1); - System.out.println("calleeLoc2="+calleeLoc2+"calleeParamList="+calleeParamList); + + System.out.println("calleeLoc1=" + calleeLoc1); + System.out.println("calleeLoc2=" + calleeLoc2 + "calleeParamList=" + calleeParamList); int callerResult = CompositeLattice.compare(callerLoc1, callerLoc2, true, @@ -1356,24 +1397,31 @@ public class FlowDownCheck { checkLocationFromExpressionNode(md, nametable, an.getSrc(), new CompositeLocation(), constraint, false); + srcLocation = rhsLocation; + + // if (!rhsLocation.get(rhsLocation.getSize() - 1).isTop()) { + if (constraint != null) { + inputGLBSet.add(rhsLocation); + inputGLBSet.add(constraint); + srcLocation = CompositeLattice.calculateGLB(inputGLBSet, generateErrorMessage(cd, an)); + } + // } + System.out.println("dstLocation=" + destLocation); System.out.println("rhsLocation=" + rhsLocation); + System.out.println("srcLocation=" + srcLocation); System.out.println("constraint=" + constraint); - srcLocation = rhsLocation; + if (!CompositeLattice.isGreaterThan(srcLocation, destLocation, generateErrorMessage(cd, an))) { - if (!rhsLocation.get(rhsLocation.getSize() - 1).isTop()) { + String context = ""; if (constraint != null) { - inputGLBSet.add(rhsLocation); - inputGLBSet.add(constraint); - srcLocation = CompositeLattice.calculateGLB(inputGLBSet, generateErrorMessage(cd, an)); + context = " and the current context constraint is " + constraint; } - } - 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 " - + cd.getSourceFileName() + "::" + an.getNumLine()); + + " does not respect location hierarchy on the assignment " + an.printNode(0) + context + + " at " + cd.getSourceFileName() + "::" + an.getNumLine()); } } else { @@ -2063,12 +2111,8 @@ class ReturnLocGenerator { for (int i = 0; i < args.size(); i++) { int type = (paramIdx2paramType.get(new Integer(i))).intValue(); CompositeLocation argLoc = args.get(i); - if (type == PARAMISHIGHER) { - // return loc is lower than param - DeltaLocation delta = new DeltaLocation(argLoc, 1); - inputGLB.add(delta); - } else if (type == PARAMISSAME) { - // return loc is equal or lower than param + if (type == PARAMISHIGHER || type == PARAMISSAME) { + // return loc is equal to or lower than param inputGLB.add(argLoc); } } diff --git a/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java b/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java index 989903c7..df5d779d 100644 --- a/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java +++ b/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java @@ -45,7 +45,6 @@ public class MethodAnnotationCheck { Set annotatedMDSet; Hashtable> caller2calleeSet; - Set trustWorthyMDSet; public MethodAnnotationCheck(SSJavaAnalysis ssjava, State state, TypeUtil tu) { this.ssjava = ssjava; @@ -53,11 +52,6 @@ public class MethodAnnotationCheck { this.tu = tu; caller2calleeSet = new Hashtable>(); annotatedMDSet = new HashSet(); - trustWorthyMDSet = new HashSet(); - } - - public Set getTrustWorthyMDSet() { - return trustWorthyMDSet; } public void methodAnnoatationCheck() { @@ -101,7 +95,7 @@ public class MethodAnnotationCheck { if (!visited.contains(p)) { visited.add(p); - if (!trustWorthyMDSet.contains(calleeMD)) { + if (!ssjava.isTrustMethod(calleeMD)) { // if method is annotated as "TRUST", do not need to check for // linear type & flow-down rule tovisit.add(calleeMD); @@ -133,7 +127,7 @@ public class MethodAnnotationCheck { for (int i = 0; i < methodAnnotations.size(); i++) { AnnotationDescriptor an = methodAnnotations.elementAt(i); if (an.getMarker().equals(ssjava.TRUST)) { - trustWorthyMDSet.add(md); + ssjava.addTrustMethod(md); } } } diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java index 6525be5d..d294a192 100644 --- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java +++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java @@ -68,6 +68,9 @@ public class SSJavaAnalysis { // the set of method descriptor required to check the linear type property Set linearTypeCheckMethodSet; + // the set of method descriptors annotated as "TRUST" + Set trustWorthyMDSet; + CallGraph callgraph; LinearTypeCheck checker; @@ -85,6 +88,7 @@ public class SSJavaAnalysis { this.mapSharedLocation2DescriptorSet = new Hashtable>(); this.linearTypeCheckMethodSet = new HashSet(); this.bf = bf; + trustWorthyMDSet = new HashSet(); } public void doCheck() { @@ -99,6 +103,14 @@ public class SSJavaAnalysis { doDefinitelyWrittenCheck(); } + public void addTrustMethod(MethodDescriptor md) { + trustWorthyMDSet.add(md); + } + + public boolean isTrustMethod(MethodDescriptor md) { + return trustWorthyMDSet.contains(md); + } + private void computeLinearTypeCheckMethodSet() { Set allCalledSet = callgraph.getMethodCalls(tu.getMain()); @@ -106,9 +118,7 @@ public class SSJavaAnalysis { Set trustedSet = new HashSet(); - Set trustAnnoatedSet = methodAnnotationChecker.getTrustWorthyMDSet(); - - for (Iterator iterator = trustAnnoatedSet.iterator(); iterator.hasNext();) { + for (Iterator iterator = trustWorthyMDSet.iterator(); iterator.hasNext();) { MethodDescriptor trustMethod = (MethodDescriptor) iterator.next(); Set calledFromTrustMethodSet = callgraph.getMethodCalls(trustMethod); trustedSet.add(trustMethod); @@ -122,7 +132,7 @@ public class SSJavaAnalysis { for (Iterator iterator = trustedSet.iterator(); iterator.hasNext();) { MethodDescriptor md = (MethodDescriptor) iterator.next(); Set callerSet = callgraph.getCallerSet(md); - if (!trustedSet.containsAll(callerSet) && !trustAnnoatedSet.contains(md)) { + if (!trustedSet.containsAll(callerSet) && !trustWorthyMDSet.contains(md)) { linearTypeCheckMethodSet.add(md); } } -- 2.34.1