public class FlowDownCheck {
static State state;
+ static SSJavaAnalysis ssjava;
+
HashSet toanalyze;
- Hashtable<Descriptor, Location> td2loc; // mapping from 'type descriptor'
- // to 'location'
+ Hashtable<Descriptor, Location> d2loc; // mapping from 'descriptor'
+ // to 'location'
Hashtable<String, ClassDescriptor> id2cd; // mapping from 'locID' to 'class
- // descriptor'
- public FlowDownCheck(State state) {
+ public FlowDownCheck(SSJavaAnalysis ssjava, State state) {
+ this.ssjava = ssjava;
this.state = state;
this.toanalyze = new HashSet();
- this.td2loc = new Hashtable<Descriptor, Location>();
- init();
+ this.d2loc = new Hashtable<Descriptor, Location>();
+ // init();
}
- public void init() {
- id2cd = new Hashtable<String, ClassDescriptor>();
- Hashtable cd2lattice = state.getCd2LocationOrder();
-
- Set cdSet = cd2lattice.keySet();
- for (Iterator iterator = cdSet.iterator(); iterator.hasNext();) {
- ClassDescriptor cd = (ClassDescriptor) iterator.next();
- Lattice<String> lattice = (Lattice<String>) cd2lattice.get(cd);
-
- Set<String> locIdSet = lattice.getKeySet();
- for (Iterator iterator2 = locIdSet.iterator(); iterator2.hasNext();) {
- String locID = (String) iterator2.next();
- id2cd.put(locID, cd);
- }
- }
-
- }
+ // public void init() {
+ // id2cd = new Hashtable<String, ClassDescriptor>();
+ // Hashtable cd2lattice = state.getCd2LocationOrder();
+ //
+ // Set cdSet = cd2lattice.keySet();
+ // for (Iterator iterator = cdSet.iterator(); iterator.hasNext();) {
+ // ClassDescriptor cd = (ClassDescriptor) iterator.next();
+ // Lattice<String> lattice = (Lattice<String>) cd2lattice.get(cd);
+ //
+ // Set<String> locIdSet = lattice.getKeySet();
+ // for (Iterator iterator2 = locIdSet.iterator(); iterator2.hasNext();) {
+ // String locID = (String) iterator2.next();
+ // id2cd.put(locID, cd);
+ // }
+ // }
+ //
+ // }
public void flowDownCheck() {
SymbolTable classtable = state.getClassSymbolTable();
// post-processing for delta location
// for a nested delta location, assigning a concrete reference to delta
// operand
- Set<Descriptor> tdSet = td2loc.keySet();
+ Set<Descriptor> tdSet = d2loc.keySet();
for (Iterator iterator = tdSet.iterator(); iterator.hasNext();) {
Descriptor td = (Descriptor) iterator.next();
- Location loc = td2loc.get(td);
+ Location loc = d2loc.get(td);
if (loc.getType() == Location.DELTA) {
// if it contains delta reference pointing to another location element
DeltaLocation delta = (DeltaLocation) locElement;
Descriptor refType = delta.getRefLocationId();
if (refType != null) {
- Location refLoc = td2loc.get(refType);
+ Location refLoc = d2loc.get(refType);
assert (refLoc instanceof CompositeLocation);
CompositeLocation refCompLoc = (CompositeLocation) refLoc;
}
public Hashtable getMap() {
- return td2loc;
+ return d2loc;
}
private void checkDeclarationInMethodBody(ClassDescriptor cd, MethodDescriptor md) {
SymbolTable nametable, DeclarationNode dn) {
VarDescriptor vd = dn.getVarDescriptor();
- Location destLoc = td2loc.get(vd);
+ Location destLoc = d2loc.get(vd);
ClassDescriptor localCD = md.getClassDesc();
if (dn.getExpression() != null) {
CompositeLocation baseLoc = null;
if (min.getBaseName() != null) {
if (nametable.contains(min.getBaseName().getSymbol())) {
- Location loc = td2loc.get(nametable.get(min.getBaseName().getSymbol()));
+ Location loc = d2loc.get(nametable.get(min.getBaseName().getSymbol()));
if (loc != null) {
baseLoc = convertCompositeLocation(loc, cd);
}
CompositeLocation argGLBLoc = null;
if (inputGLBSet.size() > 0) {
argGLBLoc = CompositeLattice.calculateGLB(cd, inputGLBSet, cd);
+ System.out.println("baseLoc=" + baseLoc + " argGLBLoc=" + argGLBLoc);
if (baseLoc != null) {
if (!CompositeLattice.isGreaterThan(argGLBLoc, baseLoc, cd)) {
throw new Error("The base location of method invocation " + min.printNode(0)
ClassDescriptor calleecd = min.getMethod().getClassDesc();
VarDescriptor calleevd = (VarDescriptor) min.getMethod().getParameter(i);
- Location calleeLoc1 = td2loc.get(calleevd);
+ Location calleeLoc1 = d2loc.get(calleevd);
if (!callerArg1.getLocation(cd).isTop()) {
// here, check if ordering relations among caller's args respect
checkLocationFromExpressionNode(md, nametable, argExp, new CompositeLocation(cd));
VarDescriptor calleevd2 = (VarDescriptor) min.getMethod().getParameter(currentIdx);
- Location calleeLoc2 = td2loc.get(calleevd2);
+ Location calleeLoc2 = d2loc.get(calleevd2);
boolean callerResult = CompositeLattice.isGreaterThan(callerArg1, callerArg2, cd);
boolean calleeResult =
CompositeLattice.isGreaterThan(calleeLoc1, calleeLoc2, calleecd);
Location localLoc = null;
if (d instanceof VarDescriptor) {
VarDescriptor vd = (VarDescriptor) d;
- localLoc = td2loc.get(vd);
+ localLoc = d2loc.get(vd);
} else if (d instanceof FieldDescriptor) {
FieldDescriptor fd = (FieldDescriptor) d;
- localLoc = td2loc.get(fd);
+ localLoc = d2loc.get(fd);
}
assert (localLoc != null);
if (!left.getType().isPrimitive()) {
FieldDescriptor fd = fan.getField();
- Location fieldLoc = td2loc.get(fd);
+ Location fieldLoc = d2loc.get(fd);
// in the case of "this.field", need to get rid of 'this' location from
// the composite location
destLocation =
srcLocation = checkLocationFromExpressionNode(md, nametable, an.getDest(), srcLocation);
- if (!((Set<String>) state.getCd2LocationPropertyMap().get(new Pair(cd, "spin")))
+ if (!ssjava.getClassLattice(cd).getSpinLocSet()
.contains(destLocation.getLocation(cd).getLocIdentifier())) {
throw new Error("Location " + destLocation + " is not allowed to have spinning values at "
+ cd.getSourceFileName() + ":" + an.getNumLine());
if (ad.getMarker().equals(SSJavaAnalysis.LOC)) {
String locationID = ad.getValue();
// check if location is defined
- Lattice<String> lattice = (Lattice<String>) state.getCd2LocationOrder().get(cd);
+ SSJavaLattice<String> lattice = ssjava.getClassLattice(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, loc);
+ d2loc.put(vd, loc);
addTypeLocation(vd.getType(), loc);
} else if (ad.getMarker().equals(SSJavaAnalysis.DELTA)) {
}
- td2loc.put(vd, compLoc);
+ d2loc.put(vd, compLoc);
addTypeLocation(vd.getType(), compLoc);
}
if (ad.getMarker().equals(SSJavaAnalysis.LOC)) {
String locationID = ad.getValue();
// check if location is defined
- Lattice<String> lattice = (Lattice<String>) state.getCd2LocationOrder().get(cd);
+ SSJavaLattice<String> lattice = ssjava.getClassLattice(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(fd, loc);
+ d2loc.put(fd, loc);
addTypeLocation(fd.getType(), loc);
} else if (ad.getMarker().equals(SSJavaAnalysis.DELTA)) {
deltaLoc.addDeltaOperand(loc);
}
compLoc.addLocation(deltaLoc);
- td2loc.put(fd, compLoc);
+ d2loc.put(fd, compLoc);
addTypeLocation(fd.getType(), compLoc);
}
assert (priorityLoc1.getClassDescriptor().equals(priorityLoc2.getClassDescriptor()));
ClassDescriptor cd = priorityLoc1.getClassDescriptor();
- Lattice<String> locationOrder = (Lattice<String>) state.getCd2LocationOrder().get(cd);
+
+ SSJavaLattice<String> locationOrder = ssjava.getClassLattice(cd);
if (priorityLoc1.getLocIdentifier().equals(priorityLoc2.getLocIdentifier())) {
// have the same level of local hierarchy
- Set<String> spinSet =
- (Set<String>) state.getCd2LocationPropertyMap().get(new Pair(cd, "spin"));
+ Set<String> spinSet = ssjava.getClassLattice(cd).getSpinLocSet();
+
if (spinSet != null && spinSet.contains(priorityLoc1.getLocIdentifier())) {
// this location can be spinning
return ComparisonResult.GREATER;
System.out.println("lattice comparison:" + loc1.getLocIdentifier() + " ? "
+ loc2.getLocIdentifier());
- locationOrder = (Lattice<String>) state.getCd2LocationOrder().get(cd1);
+ locationOrder = ssjava.getClassLattice(cd1);
if (loc1.getLocIdentifier().equals(loc2.getLocIdentifier())) {
// have the same level of local hierarchy
numEqualLoc++;
locIdentifierSet.add(locElement.getLocIdentifier());
}
- Lattice<String> locOrder = (Lattice<String>) state.getCd2LocationOrder().get(priorityCD);
+ Lattice<String> locOrder = ssjava.getClassLattice(priorityCD);
String glbLocIdentifer = locOrder.getGLB(locIdentifierSet);
Location priorityGLB = new Location(priorityCD, glbLocIdentifer);
LocalLocIdSet.add(locElement.getLocIdentifier());
}
- Lattice<String> localOrder = (Lattice<String>) state.getCd2LocationOrder().get(localCD);
+ Lattice<String> localOrder = ssjava.getClassLattice(localCD);
Location localGLBLoc = new Location(localCD, localOrder.getGLB(LocalLocIdSet));
glbCompLoc.addLocation(localGLBLoc);
}
package Analysis.SSJava;
import java.util.Hashtable;
+import java.util.Iterator;
+import java.util.Set;
+import java.util.StringTokenizer;
+import java.util.Vector;
+import IR.AnnotationDescriptor;
+import IR.ClassDescriptor;
+import IR.MethodDescriptor;
import IR.State;
-import IR.Flat.TempDescriptor;
-import IR.Tree.TreeNode;
public class SSJavaAnalysis {
- public static final String LOC="LOC";
+ public static final String LATTICE = "LATTICE";
+ public static final String METHODDEFAULT = "METHODDEFAULT";
+ public static final String THISLOC = "THISLOC";
+ public static final String GLOBALLOC = "GLOBALLOC";
+ public static final String LOC = "LOC";
public static final String DELTA = "delta";
State state;
FlowDownCheck flowDownChecker;
- Hashtable<TempDescriptor, Location> td2Loc;
+
+ // class -> field lattice
+ Hashtable<ClassDescriptor, SSJavaLattice<String>> cd2lattice;
+
+ // class -> default local variable lattice
+ Hashtable<ClassDescriptor, MethodLattice<String>> cd2methodDefault;
+
+ // method -> local variable lattice
+ Hashtable<MethodDescriptor, MethodLattice<String>> md2lattice;
public SSJavaAnalysis(State state) {
this.state = state;
- this.td2Loc = new Hashtable<TempDescriptor, Location>();
+ cd2lattice = new Hashtable<ClassDescriptor, SSJavaLattice<String>>();
+ cd2methodDefault = new Hashtable<ClassDescriptor, MethodLattice<String>>();
+ md2lattice = new Hashtable<MethodDescriptor, MethodLattice<String>>();
}
public void doCheck() {
+ parseLocationAnnotation();
doFlowDownCheck();
doLoopCheck();
}
public void doFlowDownCheck() {
- flowDownChecker = new FlowDownCheck(state);
+ flowDownChecker = new FlowDownCheck(this, state);
flowDownChecker.flowDownCheck();
}
checker.definitelyWrittenCheck();
}
+ private void parseLocationAnnotation() {
+ Iterator it = state.getClassSymbolTable().getDescriptorsIterator();
+ while (it.hasNext()) {
+ ClassDescriptor cd = (ClassDescriptor) it.next();
+ // parsing location hierarchy declaration for the class
+ Vector<AnnotationDescriptor> classAnnotations = cd.getModifier().getAnnotations();
+ for (int i = 0; i < classAnnotations.size(); i++) {
+ AnnotationDescriptor an = classAnnotations.elementAt(i);
+ String marker = an.getMarker();
+ if (marker.equals(LATTICE)) {
+ SSJavaLattice<String> locOrder = new SSJavaLattice<String>("_top_", "_bottom_");
+ cd2lattice.put(cd, locOrder);
+ parseClassLatticeDefinition(cd, an.getValue(), locOrder);
+ } else if (marker.equals(METHODDEFAULT)) {
+ MethodLattice<String> locOrder = new MethodLattice<String>("_top_", "_bottom_");
+ cd2methodDefault.put(cd, locOrder);
+ parseMethodLatticeDefinition(cd, an.getValue(), locOrder);
+ }
+ }
+ if (!cd2lattice.containsKey(cd)) {
+ throw new Error("Class " + cd.getSymbol()
+ + " doesn't have any location hierarchy declaration at " + cd.getSourceFileName());
+ }
+
+ for (Iterator method_it = cd.getMethods(); method_it.hasNext();) {
+ MethodDescriptor md = (MethodDescriptor) method_it.next();
+ // parsing location hierarchy declaration for the method
+ Vector<AnnotationDescriptor> methodAnnotations = cd.getModifier().getAnnotations();
+ for (int i = 0; i < methodAnnotations.size(); i++) {
+ AnnotationDescriptor an = methodAnnotations.elementAt(i);
+ if (an.getMarker().equals(LATTICE)) {
+ MethodLattice<String> locOrder = new MethodLattice<String>("_top_", "_bottom_");
+ cd2lattice.put(cd, locOrder);
+ parseMethodLatticeDefinition(cd, an.getValue(), locOrder);
+ }
+ }
+ }
+
+ }
+ }
+
+ private void parseMethodLatticeDefinition(ClassDescriptor cd, String value,
+ MethodLattice<String> locOrder) {
+
+ value = value.replaceAll(" ", ""); // remove all blank spaces
+
+ StringTokenizer tokenizer = new StringTokenizer(value, ",");
+
+ while (tokenizer.hasMoreTokens()) {
+ String orderElement = tokenizer.nextToken();
+ int idx = orderElement.indexOf("<");
+ if (idx > 0) {// relative order element
+ String lowerLoc = orderElement.substring(0, idx);
+ String higherLoc = orderElement.substring(idx + 1);
+ locOrder.put(higherLoc, lowerLoc);
+ if (locOrder.isIntroducingCycle(higherLoc)) {
+ throw new Error("Error: the order relation " + lowerLoc + " < " + higherLoc
+ + " introduces a cycle.");
+ }
+ } else if (orderElement.startsWith(THISLOC + "=")) {
+ String thisLoc = orderElement.substring(8);
+ locOrder.setThisLoc(thisLoc);
+ } else if (orderElement.startsWith(GLOBALLOC + "=")) {
+ String globalLoc = orderElement.substring(10);
+ locOrder.setGlobalLoc(globalLoc);
+ } else if (orderElement.contains("*")) {
+ // spin loc definition
+ locOrder.addSpinLoc(orderElement);
+ } else {
+ // single element
+ locOrder.put(orderElement);
+ }
+ }
+
+ // sanity checks
+ if (locOrder.getThisLoc() != null && !locOrder.containsKey(locOrder.getThisLoc())) {
+ throw new Error("Variable 'this' location '" + locOrder.getThisLoc()
+ + "' is not defined in the default local variable lattice at " + cd.getSourceFileName());
+ }
+
+ if (locOrder.getGlobalLoc() != null && !locOrder.containsKey(locOrder.getGlobalLoc())) {
+ throw new Error("Variable global location '" + locOrder.getGlobalLoc()
+ + "' is not defined in the default local variable lattice at " + cd.getSourceFileName());
+ }
+ }
+
+ private void parseClassLatticeDefinition(ClassDescriptor cd, String value,
+ SSJavaLattice<String> locOrder) {
+
+ value = value.replaceAll(" ", ""); // remove all blank spaces
+
+ StringTokenizer tokenizer = new StringTokenizer(value, ",");
+
+ while (tokenizer.hasMoreTokens()) {
+ String orderElement = tokenizer.nextToken();
+ int idx = orderElement.indexOf("<");
+
+ if (idx > 0) {// relative order element
+ String lowerLoc = orderElement.substring(0, idx);
+ String higherLoc = orderElement.substring(idx + 1);
+ locOrder.put(higherLoc, lowerLoc);
+ if (locOrder.isIntroducingCycle(higherLoc)) {
+ throw new Error("Error: the order relation " + lowerLoc + " < " + higherLoc
+ + " introduces a cycle.");
+ }
+ } else if (orderElement.contains("*")) {
+ // spin loc definition
+ locOrder.addSpinLoc(orderElement);
+ } else {
+ // single element
+ locOrder.put(orderElement);
+ }
+ }
+
+ // sanity check
+ Set<String> spinLocSet = locOrder.getSpinLocSet();
+ for (Iterator iterator = spinLocSet.iterator(); iterator.hasNext();) {
+ String spinLoc = (String) iterator.next();
+ if (!locOrder.containsKey(spinLoc)) {
+ throw new Error("Spin location '" + spinLoc
+ + "' is not defined in the default local variable lattice at " + cd.getSourceFileName());
+ }
+ }
+ }
+
+ public Hashtable<ClassDescriptor, SSJavaLattice<String>> getCd2lattice() {
+ return cd2lattice;
+ }
+
+ public Hashtable<ClassDescriptor, MethodLattice<String>> getCd2methodDefault() {
+ return cd2methodDefault;
+ }
+
+ public Hashtable<MethodDescriptor, MethodLattice<String>> getMd2lattice() {
+ return md2lattice;
+ }
+
+ public SSJavaLattice<String> getClassLattice(ClassDescriptor cd) {
+ return cd2lattice.get(cd);
+ }
+
}
projects / IRC.git / commitdiff