From e5b2a0989e82014b8cec2ef1d7044457f04fd4df Mon Sep 17 00:00:00 2001 From: yeom Date: Fri, 13 May 2011 23:55:21 +0000 Subject: [PATCH] take out all of ssjava stuff from state class and start re-organizing codes to reflect recent changes(separate lattices for fields and local vars, default lattice, ...) --- Robust/src/Analysis/SSJava/FlowDownCheck.java | 98 +++++----- Robust/src/Analysis/SSJava/MethodLattice.java | 30 +++ .../src/Analysis/SSJava/SSJavaAnalysis.java | 173 +++++++++++++++++- Robust/src/Analysis/SSJava/SSJavaLattice.java | 25 +++ Robust/src/IR/State.java | 20 -- 5 files changed, 273 insertions(+), 73 deletions(-) create mode 100644 Robust/src/Analysis/SSJava/MethodLattice.java create mode 100644 Robust/src/Analysis/SSJava/SSJavaLattice.java diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java index eda6e0d6..3206ee7d 100644 --- a/Robust/src/Analysis/SSJava/FlowDownCheck.java +++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java @@ -48,36 +48,38 @@ import Util.Pair; public class FlowDownCheck { static State state; + static SSJavaAnalysis ssjava; + HashSet toanalyze; - Hashtable td2loc; // mapping from 'type descriptor' - // to 'location' + Hashtable d2loc; // mapping from 'descriptor' + // to 'location' Hashtable 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(); - init(); + this.d2loc = new Hashtable(); + // init(); } - public void init() { - id2cd = new Hashtable(); - Hashtable cd2lattice = state.getCd2LocationOrder(); - - Set cdSet = cd2lattice.keySet(); - for (Iterator iterator = cdSet.iterator(); iterator.hasNext();) { - ClassDescriptor cd = (ClassDescriptor) iterator.next(); - Lattice lattice = (Lattice) cd2lattice.get(cd); - - Set 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(); + // Hashtable cd2lattice = state.getCd2LocationOrder(); + // + // Set cdSet = cd2lattice.keySet(); + // for (Iterator iterator = cdSet.iterator(); iterator.hasNext();) { + // ClassDescriptor cd = (ClassDescriptor) iterator.next(); + // Lattice lattice = (Lattice) cd2lattice.get(cd); + // + // Set 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(); @@ -109,10 +111,10 @@ 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 = 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 @@ -124,7 +126,7 @@ public class FlowDownCheck { 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; @@ -162,7 +164,7 @@ public class FlowDownCheck { } public Hashtable getMap() { - return td2loc; + return d2loc; } private void checkDeclarationInMethodBody(ClassDescriptor cd, MethodDescriptor md) { @@ -420,7 +422,7 @@ public class FlowDownCheck { 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) { @@ -601,7 +603,7 @@ public class FlowDownCheck { 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); } @@ -622,6 +624,7 @@ public class FlowDownCheck { 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) @@ -643,7 +646,7 @@ public class FlowDownCheck { 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 @@ -655,7 +658,7 @@ public class FlowDownCheck { 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); @@ -848,10 +851,10 @@ public class FlowDownCheck { 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); @@ -874,7 +877,7 @@ public class FlowDownCheck { 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 @@ -916,7 +919,7 @@ public class FlowDownCheck { destLocation = srcLocation = checkLocationFromExpressionNode(md, nametable, an.getDest(), srcLocation); - if (!((Set) 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()); @@ -955,13 +958,13 @@ public class FlowDownCheck { if (ad.getMarker().equals(SSJavaAnalysis.LOC)) { String locationID = ad.getValue(); // check if location is defined - Lattice lattice = (Lattice) state.getCd2LocationOrder().get(cd); + SSJavaLattice 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)) { @@ -1014,7 +1017,7 @@ public class FlowDownCheck { } - td2loc.put(vd, compLoc); + d2loc.put(vd, compLoc); addTypeLocation(vd.getType(), compLoc); } @@ -1070,13 +1073,13 @@ public class FlowDownCheck { if (ad.getMarker().equals(SSJavaAnalysis.LOC)) { String locationID = ad.getValue(); // check if location is defined - Lattice lattice = (Lattice) state.getCd2LocationOrder().get(cd); + SSJavaLattice 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)) { @@ -1103,7 +1106,7 @@ public class FlowDownCheck { deltaLoc.addDeltaOperand(loc); } compLoc.addLocation(deltaLoc); - td2loc.put(fd, compLoc); + d2loc.put(fd, compLoc); addTypeLocation(fd.getType(), compLoc); } @@ -1184,13 +1187,14 @@ public class FlowDownCheck { assert (priorityLoc1.getClassDescriptor().equals(priorityLoc2.getClassDescriptor())); ClassDescriptor cd = priorityLoc1.getClassDescriptor(); - Lattice locationOrder = (Lattice) state.getCd2LocationOrder().get(cd); + + SSJavaLattice locationOrder = ssjava.getClassLattice(cd); if (priorityLoc1.getLocIdentifier().equals(priorityLoc2.getLocIdentifier())) { // have the same level of local hierarchy - Set spinSet = - (Set) state.getCd2LocationPropertyMap().get(new Pair(cd, "spin")); + Set spinSet = ssjava.getClassLattice(cd).getSpinLocSet(); + if (spinSet != null && spinSet.contains(priorityLoc1.getLocIdentifier())) { // this location can be spinning return ComparisonResult.GREATER; @@ -1229,7 +1233,7 @@ public class FlowDownCheck { System.out.println("lattice comparison:" + loc1.getLocIdentifier() + " ? " + loc2.getLocIdentifier()); - locationOrder = (Lattice) state.getCd2LocationOrder().get(cd1); + locationOrder = ssjava.getClassLattice(cd1); if (loc1.getLocIdentifier().equals(loc2.getLocIdentifier())) { // have the same level of local hierarchy numEqualLoc++; @@ -1296,7 +1300,7 @@ public class FlowDownCheck { locIdentifierSet.add(locElement.getLocIdentifier()); } - Lattice locOrder = (Lattice) state.getCd2LocationOrder().get(priorityCD); + Lattice locOrder = ssjava.getClassLattice(priorityCD); String glbLocIdentifer = locOrder.getGLB(locIdentifierSet); Location priorityGLB = new Location(priorityCD, glbLocIdentifer); @@ -1329,7 +1333,7 @@ public class FlowDownCheck { LocalLocIdSet.add(locElement.getLocIdentifier()); } - Lattice localOrder = (Lattice) state.getCd2LocationOrder().get(localCD); + Lattice localOrder = ssjava.getClassLattice(localCD); Location localGLBLoc = new Location(localCD, localOrder.getGLB(LocalLocIdSet)); glbCompLoc.addLocation(localGLBLoc); } diff --git a/Robust/src/Analysis/SSJava/MethodLattice.java b/Robust/src/Analysis/SSJava/MethodLattice.java new file mode 100644 index 00000000..39a9b461 --- /dev/null +++ b/Robust/src/Analysis/SSJava/MethodLattice.java @@ -0,0 +1,30 @@ +package Analysis.SSJava; + +import Util.Lattice; + +public class MethodLattice extends SSJavaLattice { + + private T thisLoc; + private T globalLoc; + + public MethodLattice(T top, T bottom) { + super(top, bottom); + } + + public void setThisLoc(T thisLoc) { + this.thisLoc = thisLoc; + } + + public T getThisLoc() { + return thisLoc; + } + + public void setGlobalLoc(T globalLoc) { + this.globalLoc = globalLoc; + } + + public T getGlobalLoc() { + return globalLoc; + } + +} diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java index 86e10841..58cb3bab 100644 --- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java +++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java @@ -1,31 +1,51 @@ 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 td2Loc; + + // class -> field lattice + Hashtable> cd2lattice; + + // class -> default local variable lattice + Hashtable> cd2methodDefault; + + // method -> local variable lattice + Hashtable> md2lattice; public SSJavaAnalysis(State state) { this.state = state; - this.td2Loc = new Hashtable(); + cd2lattice = new Hashtable>(); + cd2methodDefault = new Hashtable>(); + md2lattice = new Hashtable>(); } public void doCheck() { + parseLocationAnnotation(); doFlowDownCheck(); doLoopCheck(); } public void doFlowDownCheck() { - flowDownChecker = new FlowDownCheck(state); + flowDownChecker = new FlowDownCheck(this, state); flowDownChecker.flowDownCheck(); } @@ -34,4 +54,145 @@ public class SSJavaAnalysis { 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 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 locOrder = new SSJavaLattice("_top_", "_bottom_"); + cd2lattice.put(cd, locOrder); + parseClassLatticeDefinition(cd, an.getValue(), locOrder); + } else if (marker.equals(METHODDEFAULT)) { + MethodLattice locOrder = new MethodLattice("_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 methodAnnotations = cd.getModifier().getAnnotations(); + for (int i = 0; i < methodAnnotations.size(); i++) { + AnnotationDescriptor an = methodAnnotations.elementAt(i); + if (an.getMarker().equals(LATTICE)) { + MethodLattice locOrder = new MethodLattice("_top_", "_bottom_"); + cd2lattice.put(cd, locOrder); + parseMethodLatticeDefinition(cd, an.getValue(), locOrder); + } + } + } + + } + } + + private void parseMethodLatticeDefinition(ClassDescriptor cd, String value, + MethodLattice 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 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 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> getCd2lattice() { + return cd2lattice; + } + + public Hashtable> getCd2methodDefault() { + return cd2methodDefault; + } + + public Hashtable> getMd2lattice() { + return md2lattice; + } + + public SSJavaLattice getClassLattice(ClassDescriptor cd) { + return cd2lattice.get(cd); + } + } diff --git a/Robust/src/Analysis/SSJava/SSJavaLattice.java b/Robust/src/Analysis/SSJava/SSJavaLattice.java new file mode 100644 index 00000000..bbc257ad --- /dev/null +++ b/Robust/src/Analysis/SSJava/SSJavaLattice.java @@ -0,0 +1,25 @@ +package Analysis.SSJava; + +import java.util.HashSet; +import java.util.Set; + +import Util.Lattice; + +public class SSJavaLattice extends Lattice { + + Set spinLocSet; + + public SSJavaLattice(T top, T bottom) { + super(top, bottom); + spinLocSet = new HashSet(); + } + + public Set getSpinLocSet() { + return spinLocSet; + } + + public void addSpinLoc(T loc) { + spinLocSet.add(loc); + } + +} diff --git a/Robust/src/IR/State.java b/Robust/src/IR/State.java index f741debe..b8f30f6d 100644 --- a/Robust/src/IR/State.java +++ b/Robust/src/IR/State.java @@ -40,8 +40,6 @@ public class State { this.selfloops=new HashSet(); this.excprefetch=new HashSet(); this.classpath=new Vector(); - this.cd2locationOrderMap=new Hashtable(); - this.cd2locationPropertyMap=new Hashtable(); this.fn2labelMap=new Hashtable(); this.lines=0; } @@ -214,8 +212,6 @@ public class State { private int numtasks=0; private int numstaticblocks=0; private int arraycount=0; - public Hashtable cd2locationOrderMap; - public Hashtable cd2locationPropertyMap; public Hashtable fn2labelMap; public boolean OPTIMIZE=false; public boolean LINENUM=false; @@ -365,20 +361,4 @@ public class State { numtasks++; } - public void addLocationOrder(ClassDescriptor cd, Lattice order) { - cd2locationOrderMap.put(cd,order); - } - - public Hashtable getCd2LocationOrder() { - return cd2locationOrderMap; - } - - public void addLocationProperty(Pair key, Object value) { - cd2locationPropertyMap.put(key,value); - } - - public Hashtable getCd2LocationPropertyMap() { - return cd2locationPropertyMap; - } - } -- 2.34.1