From bfd487e79e0075df9c722a5e0172dd4cbd9ecf49 Mon Sep 17 00:00:00 2001 From: yeom Date: Mon, 18 Apr 2011 23:51:04 +0000 Subject: [PATCH] handle the missing case in the flow down analysis: for a method invocation, check if ordering relations among caller's method arguments are relatively preserved in callee's arguments --- Robust/src/Analysis/SSJava/DeltaLocation.java | 10 +- Robust/src/Analysis/SSJava/FlowDownCheck.java | 180 +++++++++++++++--- Robust/src/Analysis/SSJava/Location.java | 4 + 3 files changed, 165 insertions(+), 29 deletions(-) diff --git a/Robust/src/Analysis/SSJava/DeltaLocation.java b/Robust/src/Analysis/SSJava/DeltaLocation.java index 4ab5a1a7..29a4a416 100644 --- a/Robust/src/Analysis/SSJava/DeltaLocation.java +++ b/Robust/src/Analysis/SSJava/DeltaLocation.java @@ -1,16 +1,14 @@ package Analysis.SSJava; -import java.util.HashSet; -import java.util.List; import java.util.Set; -import java.util.Vector; import IR.ClassDescriptor; +import IR.Descriptor; import IR.TypeDescriptor; public class DeltaLocation extends CompositeLocation { - private TypeDescriptor refOperand = null; + private Descriptor refOperand = null; public DeltaLocation(ClassDescriptor cd) { super(cd); @@ -21,12 +19,12 @@ public class DeltaLocation extends CompositeLocation { locTuple.addAll(set); } - public DeltaLocation(ClassDescriptor cd, TypeDescriptor refOperand) { + public DeltaLocation(ClassDescriptor cd, Descriptor refOperand) { super(cd); this.refOperand = refOperand; } - public TypeDescriptor getRefLocationId() { + public Descriptor getRefLocationId() { return this.refOperand; } diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java index 4fbcf36f..447397e5 100644 --- a/Robust/src/Analysis/SSJava/FlowDownCheck.java +++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java @@ -38,21 +38,22 @@ import IR.Tree.NameNode; import IR.Tree.OpNode; import IR.Tree.SubBlockNode; import IR.Tree.TertiaryNode; +import IR.Tree.TreeNode; import Util.Lattice; public class FlowDownCheck { static State state; HashSet toanalyze; - Hashtable td2loc; // mapping from 'type descriptor' - // to 'location' + Hashtable td2loc; // mapping from 'type descriptor' + // to 'location' Hashtable id2cd; // mapping from 'locID' to 'class // descriptor' public FlowDownCheck(State state) { this.state = state; this.toanalyze = new HashSet(); - this.td2loc = new Hashtable(); + this.td2loc = new Hashtable(); init(); } @@ -104,9 +105,9 @@ public class FlowDownCheck { // post-processing for delta location // for a nested delta location, assigning a concrete reference to delta // operand - Set tdSet = td2loc.keySet(); + Set tdSet = td2loc.keySet(); for (Iterator iterator = tdSet.iterator(); iterator.hasNext();) { - TypeDescriptor td = (TypeDescriptor) iterator.next(); + Descriptor td = (Descriptor) iterator.next(); Location loc = td2loc.get(td); if (loc.getType() == Location.DELTA) { @@ -117,7 +118,7 @@ public class FlowDownCheck { assert (locElement instanceof DeltaLocation); DeltaLocation delta = (DeltaLocation) locElement; - TypeDescriptor refType = delta.getRefLocationId(); + Descriptor refType = delta.getRefLocationId(); if (refType != null) { Location refLoc = td2loc.get(refType); @@ -161,6 +162,11 @@ public class FlowDownCheck { private void checkDeclarationInMethodBody(ClassDescriptor cd, MethodDescriptor md) { BlockNode bn = state.getMethodBody(md); + 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); + } checkDeclarationInBlockNode(md, md.getParameterTable(), bn); } @@ -365,7 +371,7 @@ public class FlowDownCheck { SymbolTable nametable, DeclarationNode dn) { VarDescriptor vd = dn.getVarDescriptor(); - Location destLoc = td2loc.get(vd.getType()); + Location destLoc = td2loc.get(vd); ClassDescriptor localCD = md.getClassDesc(); if (dn.getExpression() != null) { @@ -374,7 +380,6 @@ public class FlowDownCheck { checkLocationFromExpressionNode(md, nametable, dn.getExpression(), expressionLoc); if (expressionLoc != null) { - // checking location order if (!CompositeLattice.isGreaterThan(expressionLoc, destLoc, localCD)) { throw new Error("The value flow from " + expressionLoc + " to " + destLoc @@ -490,9 +495,57 @@ public class FlowDownCheck { private CompositeLocation checkLocationFromMethodInvokeNode(MethodDescriptor md, SymbolTable nametable, MethodInvokeNode min) { - // all arguments should be higher than the location of return value ClassDescriptor cd = md.getClassDesc(); + if (min.numArgs() > 1) { + + // caller needs to guarantee that it passes arguments in regarding to + // callee's hierarchy + + 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); + } + + for (int i = 0; i < min.numArgs(); i++) { + ExpressionNode en = min.getArg(i); + CompositeLocation callerArg1 = + checkLocationFromExpressionNode(md, nametable, en, new CompositeLocation(cd)); + + ClassDescriptor calleecd = min.getMethod().getClassDesc(); + VarDescriptor calleevd = (VarDescriptor) min.getMethod().getParameter(i); + Location calleeLoc1 = td2loc.get(calleevd); + + if (!callerArg1.getLocation(cd).isTop()) { + // here, check if ordering relations among caller's args respect + // ordering relations in-between callee's args + for (int currentIdx = 0; currentIdx < min.numArgs(); currentIdx++) { + if (currentIdx != i) {// skip itself + ExpressionNode argExp = min.getArg(currentIdx); + CompositeLocation callerArg2 = + checkLocationFromExpressionNode(md, nametable, argExp, new CompositeLocation(cd)); + + VarDescriptor calleevd2 = (VarDescriptor) min.getMethod().getParameter(currentIdx); + Location calleeLoc2 = td2loc.get(calleevd2); + boolean callerResult = CompositeLattice.isGreaterThan(callerArg1, callerArg2, cd); + boolean calleeResult = + CompositeLattice.isGreaterThan(calleeLoc1, calleeLoc2, calleecd); + + if (callerResult != calleeResult) { + throw new Error("Caller doesn't respect ordering relations among method arguments:" + + cd.getSourceFileName() + ":" + min.getNumLine()); + } + } + } + } + + } + + } + + // all arguments should be higher than the location of return value + // first, calculate glb of arguments Set argLocSet = new HashSet(); for (int i = 0; i < min.numArgs(); i++) { @@ -667,10 +720,10 @@ public class FlowDownCheck { Location localLoc = null; if (d instanceof VarDescriptor) { VarDescriptor vd = (VarDescriptor) d; - localLoc = td2loc.get(vd.getType()); + localLoc = td2loc.get(vd); } else if (d instanceof FieldDescriptor) { FieldDescriptor fd = (FieldDescriptor) d; - localLoc = td2loc.get(fd.getType()); + localLoc = td2loc.get(fd); } assert (localLoc != null); @@ -687,7 +740,7 @@ public class FlowDownCheck { private CompositeLocation checkLocationFromFieldAccessNode(MethodDescriptor md, SymbolTable nametable, FieldAccessNode fan, CompositeLocation loc) { FieldDescriptor fd = fan.getField(); - Location fieldLoc = td2loc.get(fd.getType()); + Location fieldLoc = td2loc.get(fd); loc.addLocation(fieldLoc); ExpressionNode left = fan.getExpression(); @@ -756,10 +809,10 @@ public class FlowDownCheck { return loc; } - private void checkDeclarationNode(MethodDescriptor md, SymbolTable nametable, DeclarationNode dn) { + private void assignLocationOfVarDescriptor(VarDescriptor vd, MethodDescriptor md, + SymbolTable nametable, TreeNode n) { ClassDescriptor cd = md.getClassDesc(); - VarDescriptor vd = dn.getVarDescriptor(); Vector annotationVec = vd.getType().getAnnotationMarkers(); // currently enforce every variable to have corresponding location @@ -787,7 +840,7 @@ public class FlowDownCheck { } Location loc = new Location(cd, locationID); - td2loc.put(vd.getType(), loc); + td2loc.put(vd, loc); } else if (ad.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) { if (ad.getMarker().equals(SSJavaAnalysis.DELTA)) { @@ -804,7 +857,7 @@ public class FlowDownCheck { if (!deltaStr.endsWith(")")) { throw new Error("The declaration of the delta location is wrong at " - + cd.getSourceFileName() + ":" + dn.getNumLine()); + + cd.getSourceFileName() + ":" + n.getNumLine()); } String locationOperand = deltaStr.substring(4, deltaStr.length() - 1); @@ -813,12 +866,12 @@ public class FlowDownCheck { if (d instanceof VarDescriptor) { VarDescriptor varDescriptor = (VarDescriptor) d; - DeltaLocation deltaLoc = new DeltaLocation(cd, varDescriptor.getType()); + DeltaLocation deltaLoc = new DeltaLocation(cd, varDescriptor); // td2loc.put(vd.getType(), compLoc); compLoc.addLocation(deltaLoc); } else if (d instanceof FieldDescriptor) { throw new Error("Applying delta operation to the field " + locationOperand - + " is not allowed at " + cd.getSourceFileName() + ":" + dn.getNumLine()); + + " is not allowed at " + cd.getSourceFileName() + ":" + n.getNumLine()); } } else { StringTokenizer token = new StringTokenizer(deltaStr, ","); @@ -840,7 +893,7 @@ public class FlowDownCheck { } - td2loc.put(vd.getType(), compLoc); + td2loc.put(vd, compLoc); System.out.println("vd=" + vd + " is assigned by " + compLoc); } @@ -848,6 +901,87 @@ public class FlowDownCheck { } + private void checkDeclarationNode(MethodDescriptor md, SymbolTable nametable, DeclarationNode dn) { + + VarDescriptor vd = dn.getVarDescriptor(); + assignLocationOfVarDescriptor(vd, md, nametable, dn); + /* + * Vector annotationVec = + * vd.getType().getAnnotationMarkers(); + * + * // 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."); } + * + * AnnotationDescriptor ad = annotationVec.elementAt(0); + * + * if (ad.getType() == AnnotationDescriptor.MARKER_ANNOTATION) { + * + * // check if location is defined String locationID = ad.getMarker(); + * Lattice lattice = (Lattice) + * state.getCd2LocationOrder().get(cd); + * + * if (lattice == null || (!lattice.containsKey(locationID))) { throw new + * Error("Location " + locationID + + * " is not defined in the location hierarchy of class " + cd.getSymbol() + + * "."); } + * + * Location loc = new Location(cd, locationID); td2loc.put(vd.getType(), + * loc); + * + * } else if (ad.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) { if + * (ad.getMarker().equals(SSJavaAnalysis.DELTA)) { + * + * CompositeLocation compLoc = new CompositeLocation(cd); + * + * if (ad.getData().length() == 0) { throw new Error("Delta function of " + + * vd.getSymbol() + " does not have any locations: " + cd.getSymbol() + + * "."); } + * + * String deltaStr = ad.getData(); if (deltaStr.startsWith("LOC(")) { + * + * if (!deltaStr.endsWith(")")) { throw new + * Error("The declaration of the delta location is wrong at " + + * cd.getSourceFileName() + ":" + dn.getNumLine()); } String locationOperand + * = deltaStr.substring(4, deltaStr.length() - 1); + * + * nametable.get(locationOperand); Descriptor d = (Descriptor) + * nametable.get(locationOperand); + * + * if (d instanceof VarDescriptor) { VarDescriptor varDescriptor = + * (VarDescriptor) d; DeltaLocation deltaLoc = new DeltaLocation(cd, + * varDescriptor.getType()); // td2loc.put(vd.getType(), compLoc); + * compLoc.addLocation(deltaLoc); } else if (d instanceof FieldDescriptor) { + * throw new Error("Applying delta operation to the field " + + * locationOperand + " is not allowed at " + cd.getSourceFileName() + ":" + + * dn.getNumLine()); } } else { StringTokenizer token = new + * StringTokenizer(deltaStr, ","); DeltaLocation deltaLoc = new + * DeltaLocation(cd); + * + * while (token.hasMoreTokens()) { String deltaOperand = token.nextToken(); + * ClassDescriptor deltaCD = id2cd.get(deltaOperand); if (deltaCD == null) { + * // delta operand is not defined in the location hierarchy throw new + * Error("Delta operand '" + deltaOperand + "' of declaration node '" + vd + + * "' is not defined by location hierarchies."); } + * + * Location loc = new Location(deltaCD, deltaOperand); + * deltaLoc.addDeltaOperand(loc); } compLoc.addLocation(deltaLoc); + * + * } + * + * td2loc.put(vd.getType(), compLoc); System.out.println("vd=" + vd + + * " is assigned by " + compLoc); + * + * } } + */ + + } + private void checkClass(ClassDescriptor cd) { // Check to see that methods respects ss property for (Iterator method_it = cd.getMethods(); method_it.hasNext();) { @@ -896,7 +1030,7 @@ public class FlowDownCheck { } Location localLoc = new Location(cd, locationID); - td2loc.put(fd.getType(), localLoc); + td2loc.put(fd, localLoc); } else if (ad.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) { if (ad.getMarker().equals(SSJavaAnalysis.DELTA)) { @@ -923,7 +1057,7 @@ public class FlowDownCheck { deltaLoc.addDeltaOperand(loc); } compLoc.addLocation(deltaLoc); - td2loc.put(fd.getType(), compLoc); + td2loc.put(fd, compLoc); } } @@ -1002,8 +1136,8 @@ public class FlowDownCheck { if (priorityLoc1.getLocIdentifier().equals(priorityLoc2.getLocIdentifier())) { // have the same level of local hierarchy - if (((Set) state.getCd2LocationPropertyMap().get(cd)).contains(priorityLoc1 - .getLocIdentifier())) { + Set spinSet = (Set) state.getCd2LocationPropertyMap().get(cd); + if (spinSet != null && spinSet.contains(priorityLoc1.getLocIdentifier())) { // this location can be spinning return ComparisonResult.GREATER; } diff --git a/Robust/src/Analysis/SSJava/Location.java b/Robust/src/Analysis/SSJava/Location.java index 7ed3d3ac..741b4448 100644 --- a/Robust/src/Analysis/SSJava/Location.java +++ b/Robust/src/Analysis/SSJava/Location.java @@ -88,5 +88,9 @@ public class Location { bottomLoc.loc = "_bottom_"; return bottomLoc; } + + public boolean isTop(){ + return type==TOP; + } } -- 2.34.1