X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;ds=sidebyside;f=Robust%2Fsrc%2FAnalysis%2FSSJava%2FSSJavaAnalysis.java;h=121e4cb5fb135c56122f1f6dfbf25f0fbf72f017;hb=d396c42d2a86460c7e220d21e5219049c177c5cf;hp=58cb3babf8c0a7cd8a67c581378e67a785c68d21;hpb=e5b2a0989e82014b8cec2ef1d7044457f04fd4df;p=IRC.git diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java index 58cb3bab..121e4cb5 100644 --- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java +++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java @@ -1,26 +1,65 @@ package Analysis.SSJava; +import java.io.BufferedWriter; +import java.io.FileWriter; +import java.io.IOException; +import java.util.ArrayList; +import java.util.Collections; +import java.util.Comparator; +import java.util.HashSet; import java.util.Hashtable; import java.util.Iterator; +import java.util.LinkedList; +import java.util.List; import java.util.Set; import java.util.StringTokenizer; import java.util.Vector; +import Analysis.CallGraph.CallGraph; +import Analysis.Loops.GlobalFieldType; +import Analysis.Loops.LoopFinder; +import Analysis.Loops.LoopOptimize; +import Analysis.Loops.LoopTerminate; import IR.AnnotationDescriptor; import IR.ClassDescriptor; +import IR.Descriptor; +import IR.FieldDescriptor; import IR.MethodDescriptor; import IR.State; +import IR.SymbolTable; +import IR.TypeUtil; +import IR.Flat.BuildFlat; +import IR.Flat.FlatMethod; +import IR.Flat.FlatNode; +import Util.Pair; public class SSJavaAnalysis { + public static final String SSJAVA = "SSJAVA"; 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 RETURNLOC = "RETURNLOC"; + public static final String PCLOC = "PCLOC"; public static final String LOC = "LOC"; - public static final String DELTA = "delta"; + public static final String DELTA = "DELTA"; + public static final String TERMINATE = "TERMINATE"; + public static final String DELEGATE = "DELEGATE"; + public static final String DELEGATETHIS = "DELEGATETHIS"; + public static final String TRUST = "TRUST"; + + public static final String TOP = "_top_"; + public static final String BOTTOM = "_bottom_"; + State state; + TypeUtil tu; FlowDownCheck flowDownChecker; + MethodAnnotationCheck methodAnnotationChecker; + BuildFlat bf; + + // set containing method requires to be annoated + Set annotationRequireSet; // class -> field lattice Hashtable> cd2lattice; @@ -31,17 +70,194 @@ public class SSJavaAnalysis { // method -> local variable lattice Hashtable> md2lattice; - public SSJavaAnalysis(State state) { + // method set that does not want to have loop termination analysis + Hashtable skipLoopTerminate; + + // map shared location to its descriptors + Hashtable> mapSharedLocation2DescriptorSet; + + // set containing a class that has at least one annoated method + Set annotationRequireClassSet; + + // the set of method descriptor required to check the linear type property + Set linearTypeCheckMethodSet; + + // the set of method descriptors annotated as "TRUST" + Set trustWorthyMDSet; + + // points to method containing SSJAVA Loop + private MethodDescriptor methodContainingSSJavaLoop; + + private FlatNode ssjavaLoopEntrance; + + // keep the field ownership from the linear type checking + Hashtable> mapMethodToOwnedFieldSet; + + Set sameHeightWriteFlatNodeSet; + + CallGraph callgraph; + + LinearTypeCheck checker; + + // maps a descriptor to its known dependents: namely + // methods or tasks that call the descriptor's method + // AND are part of this analysis (reachable from main) + private Hashtable> mapDescriptorToSetDependents; + + private LinkedList sortedDescriptors; + + public SSJavaAnalysis(State state, TypeUtil tu, BuildFlat bf, CallGraph callgraph) { this.state = state; - cd2lattice = new Hashtable>(); - cd2methodDefault = new Hashtable>(); - md2lattice = new Hashtable>(); + this.tu = tu; + this.callgraph = callgraph; + this.cd2lattice = new Hashtable>(); + this.cd2methodDefault = new Hashtable>(); + this.md2lattice = new Hashtable>(); + this.annotationRequireSet = new HashSet(); + this.annotationRequireClassSet = new HashSet(); + this.skipLoopTerminate = new Hashtable(); + this.mapSharedLocation2DescriptorSet = new Hashtable>(); + this.linearTypeCheckMethodSet = new HashSet(); + this.bf = bf; + this.trustWorthyMDSet = new HashSet(); + this.mapMethodToOwnedFieldSet = new Hashtable>(); + this.sameHeightWriteFlatNodeSet = new HashSet(); + this.mapDescriptorToSetDependents = new Hashtable>(); + this.sortedDescriptors = new LinkedList(); } public void doCheck() { - parseLocationAnnotation(); - doFlowDownCheck(); - doLoopCheck(); + doMethodAnnotationCheck(); + computeLinearTypeCheckMethodSet(); + doLinearTypeCheck(); + + init(); + + if (state.SSJAVADEBUG) { + debug_printAnnotationRequiredSet(); + } + if (state.SSJAVAINFER) { + inference(); + } else { + parseLocationAnnotation(); + doFlowDownCheck(); + doDefinitelyWrittenCheck(); + doLoopCheck(); + } + } + + private void init() { + // perform topological sort over the set of methods accessed by the main + // event loop + Set methodDescriptorsToAnalyze = new HashSet(); + methodDescriptorsToAnalyze.addAll(getAnnotationRequireSet()); + sortedDescriptors = topologicalSort(methodDescriptorsToAnalyze); + } + + public LinkedList getSortedDescriptors() { + return (LinkedList) sortedDescriptors.clone(); + } + + private void inference() { + LocationInference inferEngine = new LocationInference(this, state); + inferEngine.inference(); + } + + private void doLoopCheck() { + GlobalFieldType gft = new GlobalFieldType(callgraph, state, tu.getMain()); + LoopOptimize lo = new LoopOptimize(gft, tu); + + SymbolTable classtable = state.getClassSymbolTable(); + + List toanalyzeList = new ArrayList(); + List toanalyzeMethodList = new ArrayList(); + + toanalyzeList.addAll(classtable.getValueSet()); + Collections.sort(toanalyzeList, new Comparator() { + public int compare(ClassDescriptor o1, ClassDescriptor o2) { + return o1.getClassName().compareTo(o2.getClassName()); + } + }); + + for (int i = 0; i < toanalyzeList.size(); i++) { + ClassDescriptor cd = toanalyzeList.get(i); + + SymbolTable methodtable = cd.getMethodTable(); + toanalyzeMethodList.clear(); + toanalyzeMethodList.addAll(methodtable.getValueSet()); + Collections.sort(toanalyzeMethodList, new Comparator() { + public int compare(MethodDescriptor o1, MethodDescriptor o2) { + return o1.getSymbol().compareTo(o2.getSymbol()); + } + }); + + for (int mdIdx = 0; mdIdx < toanalyzeMethodList.size(); mdIdx++) { + MethodDescriptor md = toanalyzeMethodList.get(mdIdx); + if (needTobeAnnotated(md)) { + lo.analyze(state.getMethodFlat(md)); + doLoopTerminationCheck(lo, state.getMethodFlat(md)); + } + } + + } + + } + + 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()); + linearTypeCheckMethodSet.addAll(allCalledSet); + + Set trustedSet = new HashSet(); + + for (Iterator iterator = trustWorthyMDSet.iterator(); iterator.hasNext();) { + MethodDescriptor trustMethod = (MethodDescriptor) iterator.next(); + Set calledFromTrustMethodSet = callgraph.getMethodCalls(trustMethod); + trustedSet.add(trustMethod); + trustedSet.addAll(calledFromTrustMethodSet); + } + + linearTypeCheckMethodSet.removeAll(trustedSet); + + // if a method is called only by trusted method, no need to check linear + // type & flow down rule + for (Iterator iterator = trustedSet.iterator(); iterator.hasNext();) { + MethodDescriptor md = (MethodDescriptor) iterator.next(); + Set callerSet = callgraph.getCallerSet(md); + if (!trustedSet.containsAll(callerSet) && !trustWorthyMDSet.contains(md)) { + linearTypeCheckMethodSet.add(md); + } + } + + } + + private void doLinearTypeCheck() { + LinearTypeCheck checker = new LinearTypeCheck(this, state); + checker.linearTypeCheck(); + } + + public void debug_printAnnotationRequiredSet() { + System.out.println("SSJAVA: SSJava is checking the following methods:"); + for (Iterator iterator = annotationRequireSet.iterator(); iterator.hasNext();) { + MethodDescriptor md = iterator.next(); + System.out.println(md); + } + System.out.println(); + } + + private void doMethodAnnotationCheck() { + methodAnnotationChecker = new MethodAnnotationCheck(this, state, tu); + methodAnnotationChecker.methodAnnoatationCheck(); + methodAnnotationChecker.methodAnnoataionInheritanceCheck(); + state.setAnnotationRequireSet(annotationRequireSet); } public void doFlowDownCheck() { @@ -49,8 +265,8 @@ public class SSJavaAnalysis { flowDownChecker.flowDownCheck(); } - public void doLoopCheck() { - DefinitelyWrittenCheck checker = new DefinitelyWrittenCheck(state); + public void doDefinitelyWrittenCheck() { + DefinitelyWrittenCheck checker = new DefinitelyWrittenCheck(this, state); checker.definitelyWrittenCheck(); } @@ -64,38 +280,107 @@ public class SSJavaAnalysis { AnnotationDescriptor an = classAnnotations.elementAt(i); String marker = an.getMarker(); if (marker.equals(LATTICE)) { - SSJavaLattice locOrder = new SSJavaLattice("_top_", "_bottom_"); + SSJavaLattice locOrder = + new SSJavaLattice(SSJavaAnalysis.TOP, SSJavaAnalysis.BOTTOM); cd2lattice.put(cd, locOrder); parseClassLatticeDefinition(cd, an.getValue(), locOrder); + + if (state.SSJAVADEBUG) { + // generate lattice dot file + writeLatticeDotFile(cd, null, locOrder); + } + } else if (marker.equals(METHODDEFAULT)) { - MethodLattice locOrder = new MethodLattice("_top_", "_bottom_"); + MethodLattice locOrder = + new MethodLattice(SSJavaAnalysis.TOP, SSJavaAnalysis.BOTTOM); cd2methodDefault.put(cd, locOrder); - parseMethodLatticeDefinition(cd, an.getValue(), locOrder); + parseMethodDefaultLatticeDefinition(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); + + if (needTobeAnnotated(md)) { + Vector methodAnnotations = md.getModifiers().getAnnotations(); + if (methodAnnotations != null) { + for (int i = 0; i < methodAnnotations.size(); i++) { + AnnotationDescriptor an = methodAnnotations.elementAt(i); + if (an.getMarker().equals(LATTICE)) { + // developer explicitly defines method lattice + MethodLattice locOrder = + new MethodLattice(SSJavaAnalysis.TOP, SSJavaAnalysis.BOTTOM); + md2lattice.put(md, locOrder); + parseMethodDefaultLatticeDefinition(cd, an.getValue(), locOrder); + } else if (an.getMarker().equals(TERMINATE)) { + // developer explicitly wants to skip loop termination analysis + String value = an.getValue(); + int maxIteration = 0; + if (value != null) { + maxIteration = Integer.parseInt(value); + } + skipLoopTerminate.put(md, new Integer(maxIteration)); + } + } + } + } + + } + + } + } + + public void writeLatticeDotFile(ClassDescriptor cd, MethodDescriptor md, + SSJavaLattice locOrder) { + + String fileName = "lattice_"; + if (md != null) { + fileName += + cd.getSymbol().replaceAll("[\\W_]", "") + "_" + md.getSymbol().replaceAll("[\\W_]", ""); + } else { + fileName += cd.getSymbol().replaceAll("[\\W_]", ""); + } + + Set> pairSet = locOrder.getOrderingPairSet(); + + if (pairSet.size() > 0) { + try { + BufferedWriter bw = new BufferedWriter(new FileWriter(fileName + ".dot")); + + bw.write("digraph " + fileName + " {\n"); + + for (Iterator iterator = pairSet.iterator(); iterator.hasNext();) { + // pair is in the form of + Pair pair = (Pair) iterator.next(); + + T highLocId = pair.getFirst(); + String highLocStr, lowLocStr; + if (locOrder.isSharedLoc(highLocId)) { + highLocStr = "\"" + highLocId + "*\""; + } else { + highLocStr = highLocId.toString(); } + T lowLocId = pair.getSecond(); + if (locOrder.isSharedLoc(lowLocId)) { + lowLocStr = "\"" + lowLocId + "*\""; + } else { + lowLocStr = lowLocId.toString(); + } + bw.write(highLocId + " -> " + lowLocId + ";\n"); } + bw.write("}\n"); + bw.close(); + + } catch (IOException e) { + e.printStackTrace(); } } + } - private void parseMethodLatticeDefinition(ClassDescriptor cd, String value, + private void parseMethodDefaultLatticeDefinition(ClassDescriptor cd, String value, MethodLattice locOrder) { value = value.replaceAll(" ", ""); // remove all blank spaces @@ -119,9 +404,15 @@ public class SSJavaAnalysis { } else if (orderElement.startsWith(GLOBALLOC + "=")) { String globalLoc = orderElement.substring(10); locOrder.setGlobalLoc(globalLoc); - } else if (orderElement.contains("*")) { + } else if (orderElement.startsWith(RETURNLOC + "=")) { + String returnLoc = orderElement.substring(10); + locOrder.setReturnLoc(returnLoc); + } else if (orderElement.startsWith(PCLOC + "=")) { + String pcLoc = orderElement.substring(6); + locOrder.setPCLoc(pcLoc); + } else if (orderElement.endsWith("*")) { // spin loc definition - locOrder.addSpinLoc(orderElement); + locOrder.addSharedLoc(orderElement.substring(0, orderElement.length() - 1)); } else { // single element locOrder.put(orderElement); @@ -131,12 +422,12 @@ public class SSJavaAnalysis { // 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()); + + "' is not defined in the 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()); + + "' is not defined in the local variable lattice at " + cd.getSourceFileName()); } } @@ -161,7 +452,7 @@ public class SSJavaAnalysis { } } else if (orderElement.contains("*")) { // spin loc definition - locOrder.addSpinLoc(orderElement); + locOrder.addSharedLoc(orderElement.substring(0, orderElement.length() - 1)); } else { // single element locOrder.put(orderElement); @@ -169,7 +460,7 @@ public class SSJavaAnalysis { } // sanity check - Set spinLocSet = locOrder.getSpinLocSet(); + Set spinLocSet = locOrder.getSharedLocSet(); for (Iterator iterator = spinLocSet.iterator(); iterator.hasNext();) { String spinLoc = (String) iterator.next(); if (!locOrder.containsKey(spinLoc)) { @@ -195,4 +486,215 @@ 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); + } else { + + if (cd2methodDefault.containsKey(md.getClassDesc())) { + return cd2methodDefault.get(md.getClassDesc()); + } else { + throw new Error("Method Lattice of " + md + " is not defined."); + } + + } + } + + public boolean needToCheckLinearType(MethodDescriptor md) { + return linearTypeCheckMethodSet.contains(md); + } + + public boolean needTobeAnnotated(MethodDescriptor md) { + return annotationRequireSet.contains(md); + } + + public boolean needToBeAnnoated(ClassDescriptor cd) { + return annotationRequireClassSet.contains(cd); + } + + public void addAnnotationRequire(ClassDescriptor cd) { + annotationRequireClassSet.add(cd); + } + + 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 + if (!isSSJavaUtil(cd)) { + annotationRequireClassSet.add(cd); + annotationRequireSet.add(md); + } + } + + public Set getAnnotationRequireSet() { + return annotationRequireSet; + } + + public void doLoopTerminationCheck(LoopOptimize lo, FlatMethod fm) { + LoopTerminate lt = new LoopTerminate(this, state); + if (needTobeAnnotated(fm.getMethod())) { + lt.terminateAnalysis(fm, lo.getLoopInvariant(fm)); + } + } + + public CallGraph getCallGraph() { + return callgraph; + } + + public SSJavaLattice getLattice(Descriptor d) { + + if (d instanceof MethodDescriptor) { + return getMethodLattice((MethodDescriptor) d); + } else { + return getClassLattice((ClassDescriptor) d); + } + + } + + public boolean isSharedLocation(Location loc) { + SSJavaLattice lattice = getLattice(loc.getDescriptor()); + return lattice.getSharedLocSet().contains(loc.getLocIdentifier()); + } + + public void mapSharedLocation2Descriptor(Location loc, Descriptor d) { + Set set = mapSharedLocation2DescriptorSet.get(loc); + if (set == null) { + set = new HashSet(); + mapSharedLocation2DescriptorSet.put(loc, set); + } + set.add(d); + } + + public BuildFlat getBuildFlat() { + return bf; + } + + public MethodDescriptor getMethodContainingSSJavaLoop() { + return methodContainingSSJavaLoop; + } + + public void setMethodContainingSSJavaLoop(MethodDescriptor methodContainingSSJavaLoop) { + this.methodContainingSSJavaLoop = methodContainingSSJavaLoop; + } + + public boolean isSSJavaUtil(ClassDescriptor cd) { + if (cd.getSymbol().equals("SSJAVA")) { + return true; + } + return false; + } + + public void setFieldOnwership(MethodDescriptor md, FieldDescriptor field) { + + Set fieldSet = mapMethodToOwnedFieldSet.get(md); + if (fieldSet == null) { + fieldSet = new HashSet(); + mapMethodToOwnedFieldSet.put(md, fieldSet); + } + fieldSet.add(field); + } + + public boolean isOwnedByMethod(MethodDescriptor md, FieldDescriptor field) { + Set fieldSet = mapMethodToOwnedFieldSet.get(md); + if (fieldSet != null) { + return fieldSet.contains(field); + } + return false; + } + + public FlatNode getSSJavaLoopEntrance() { + return ssjavaLoopEntrance; + } + + public void setSSJavaLoopEntrance(FlatNode ssjavaLoopEntrance) { + this.ssjavaLoopEntrance = ssjavaLoopEntrance; + } + + public void addSameHeightWriteFlatNode(FlatNode fn) { + this.sameHeightWriteFlatNodeSet.add(fn); + } + + public boolean isSameHeightWrite(FlatNode fn) { + return this.sameHeightWriteFlatNodeSet.contains(fn); + } + + public LinkedList topologicalSort(Set toSort) { + + Set discovered = new HashSet(); + + LinkedList sorted = new LinkedList(); + + Iterator itr = toSort.iterator(); + while (itr.hasNext()) { + MethodDescriptor d = itr.next(); + + if (!discovered.contains(d)) { + dfsVisit(d, toSort, sorted, discovered); + } + } + + return sorted; + } + + // While we're doing DFS on call graph, remember + // dependencies for efficient queuing of methods + // during interprocedural analysis: + // + // a dependent of a method decriptor d for this analysis is: + // 1) a method or task that invokes d + // 2) in the descriptorsToAnalyze set + private void dfsVisit(MethodDescriptor md, Set toSort, + LinkedList sorted, Set discovered) { + + discovered.add(md); + + Iterator itr2 = callgraph.getCalleeSet(md).iterator(); + while (itr2.hasNext()) { + MethodDescriptor dCallee = (MethodDescriptor) itr2.next(); + addDependent(dCallee, md); + } + + Iterator itr = callgraph.getCallerSet(md).iterator(); + while (itr.hasNext()) { + MethodDescriptor dCaller = (MethodDescriptor) itr.next(); + // only consider callers in the original set to analyze + if (!toSort.contains(dCaller)) { + continue; + } + if (!discovered.contains(dCaller)) { + addDependent(md, // callee + dCaller // caller + ); + + dfsVisit(dCaller, toSort, sorted, discovered); + } + } + + // for leaf-nodes last now! + sorted.addLast(md); + } + + public void addDependent(MethodDescriptor callee, MethodDescriptor caller) { + Set deps = mapDescriptorToSetDependents.get(callee); + if (deps == null) { + deps = new HashSet(); + } + deps.add(caller); + mapDescriptorToSetDependents.put(callee, deps); + } + + public Set getDependents(MethodDescriptor callee) { + Set deps = mapDescriptorToSetDependents.get(callee); + if (deps == null) { + deps = new HashSet(); + mapDescriptorToSetDependents.put(callee, deps); + } + return deps; + } + }