From c8ce61c6d5b0c24a0d6ff309fb5c92b1cd4d55d2 Mon Sep 17 00:00:00 2001 From: yeom Date: Fri, 8 Jul 2011 01:49:50 +0000 Subject: [PATCH] start implementing shared location analysis --- .../SSJava/DefinitelyWrittenCheck.java | 251 ++++++++++++++++-- .../src/Analysis/SSJava/SSJavaAnalysis.java | 17 ++ 2 files changed, 253 insertions(+), 15 deletions(-) diff --git a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java index 65027b5b..39c5ee26 100644 --- a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java +++ b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java @@ -6,8 +6,10 @@ import java.util.Iterator; import java.util.LinkedList; import java.util.Set; import java.util.Stack; +import java.util.Vector; import Analysis.CallGraph.CallGraph; +import Analysis.Loops.LoopFinder; import IR.Descriptor; import IR.FieldDescriptor; import IR.MethodDescriptor; @@ -58,6 +60,22 @@ public class DefinitelyWrittenCheck { // maps a flatnode to definitely written analysis mapping M private Hashtable, Hashtable>> definitelyWrittenResults; + // maps a method descriptor to its current summary during the analysis + // then analysis reaches fixed-point, this mapping will have the final summary + // for each method descriptor + private Hashtable>> mapMethodDescriptorToCompleteClearingSummary; + + // maps a method descriptor to the merged incoming caller's current + // overwritten status + private Hashtable>> mapMethodDescriptorToInitialClearingSummary; + + // maps a flat node to current partial results + private Hashtable>> mapFlatNodeToClearingSummary; + + private FlatNode ssjavaLoopEntrance; + private LoopFinder ssjavaLoop; + private Set loopIncElements; + private Set> calleeUnionBoundReadSet; private Set> calleeIntersectBoundOverWriteSet; @@ -74,13 +92,197 @@ public class DefinitelyWrittenCheck { new Hashtable, Hashtable>>(); this.calleeUnionBoundReadSet = new HashSet>(); this.calleeIntersectBoundOverWriteSet = new HashSet>(); + this.mapMethodDescriptorToCompleteClearingSummary = + new Hashtable>>(); + this.mapMethodDescriptorToInitialClearingSummary = + new Hashtable>>(); + this.mapFlatNodeToClearingSummary = + new Hashtable>>(); } public void definitelyWrittenCheck() { if (!ssjava.getAnnotationRequireSet().isEmpty()) { methodReadOverWriteAnalysis(); writtenAnalyis(); +// sharedLocationAnalysis(); + } + } + + private void sharedLocationAnalysis() { + // verify that all concrete locations of shared location are cleared out at + // the same time once per the out-most loop + + Set methodDescriptorsToAnalyze = new HashSet(); + methodDescriptorsToAnalyze.addAll(ssjava.getAnnotationRequireSet()); + + LinkedList sortedDescriptors = topologicalSort(methodDescriptorsToAnalyze); + + Stack methodDescriptorsToVisitStack = new Stack(); + Set methodDescriptorToVistSet = new HashSet(); + methodDescriptorToVistSet.addAll(sortedDescriptors); + + while (!sortedDescriptors.isEmpty()) { + MethodDescriptor md = sortedDescriptors.removeLast(); + methodDescriptorsToVisitStack.add(md); + } + + // analyze scheduled methods until there are no more to visit + while (!methodDescriptorsToVisitStack.isEmpty()) { + MethodDescriptor md = methodDescriptorsToVisitStack.pop(); + FlatMethod fm = state.getMethodFlat(md); + + sharedLocation_analyzeMethod(fm, (fm.equals(methodContainingSSJavaLoop))); + + if (true) { + + // results for callee changed, so enqueue dependents caller for + // further analysis + Iterator depsItr = getDependents(md).iterator(); + while (depsItr.hasNext()) { + MethodDescriptor methodNext = depsItr.next(); + if (!methodDescriptorsToVisitStack.contains(methodNext) + && methodDescriptorToVistSet.contains(methodNext)) { + methodDescriptorsToVisitStack.add(methodNext); + } + + } + + } + + } + + Set flatNodesToVisit = new HashSet(); + flatNodesToVisit.add(ssjavaLoopEntrance); + + } + + private void sharedLocation_analyzeMethod(FlatMethod fm, boolean onlyVisitSSJavaLoop) { + + if (state.SSJAVADEBUG) { + System.out.println("Definitely written for shared locations Analyzing: " + fm); + } + + // intraprocedural analysis + Set flatNodesToVisit = new HashSet(); + Set visited = new HashSet(); + + if (onlyVisitSSJavaLoop) { + flatNodesToVisit.add(ssjavaLoopEntrance); + } else { + flatNodesToVisit.add(fm); + } + + while (!flatNodesToVisit.isEmpty()) { + FlatNode fn = flatNodesToVisit.iterator().next(); + flatNodesToVisit.remove(fn); + + Hashtable> curr = new Hashtable>(); + + for (int i = 0; i < fn.numPrev(); i++) { + FlatNode prevFn = fn.getPrev(i); + Hashtable> in = mapFlatNodeToClearingSummary.get(prevFn); + if (in != null) { + mergeSharedAnaylsis(curr, in); + } + } + + sharedLocation_nodeActions(fn, curr); + + Hashtable> clearingPrev = mapFlatNodeToClearingSummary.get(fn); + + if (!curr.equals(clearingPrev)) { + mapFlatNodeToClearingSummary.put(fn, curr); + + for (int i = 0; i < fn.numNext(); i++) { + FlatNode nn = fn.getNext(i); + + if (!onlyVisitSSJavaLoop || (onlyVisitSSJavaLoop && loopIncElements.contains(nn))) { + flatNodesToVisit.add(nn); + } + + } + } + + } + + } + + private void sharedLocation_nodeActions(FlatNode fn, Hashtable> curr) { + + TempDescriptor lhs; + TempDescriptor rhs; + FieldDescriptor fld; + + System.out.println("fn="+fn); + switch (fn.kind()) { + case FKind.FlatFieldNode: + case FKind.FlatElementNode: { + + FlatFieldNode ffn = (FlatFieldNode) fn; + lhs = ffn.getDst(); + rhs = ffn.getSrc(); + fld = ffn.getField(); + + // read field + NTuple srcHeapPath = mapHeapPath.get(rhs); + NTuple fldHeapPath = new NTuple(srcHeapPath.getList()); + fldHeapPath.add(fld); + + if (fld.getType().isImmutable()) { + readLocation(fn, fldHeapPath, curr); + } + + // propagate rhs's heap path to the lhs + mapHeapPath.put(lhs, fldHeapPath); + + } + break; + + case FKind.FlatSetFieldNode: + case FKind.FlatSetElementNode: { + + FlatSetFieldNode fsfn = (FlatSetFieldNode) fn; + lhs = fsfn.getDst(); + fld = fsfn.getField(); + + // write(field) + NTuple lhsHeapPath = computePath(lhs); + NTuple fldHeapPath = new NTuple(lhsHeapPath.getList()); + writeLocation(curr, fldHeapPath, fld); + + } + break; + + case FKind.FlatCall: { + + } + break; } + + } + + private void writeLocation(Hashtable> curr, + NTuple fldHeapPath, FieldDescriptor fld) { + + Location fieldLoc = (Location) fld.getType().getExtension(); + if (ssjava.isSharedLocation(fieldLoc)) { + + Vector v = curr.get(fieldLoc); + if (v == null) { + v = new Vector(); + curr.put(fieldLoc, v); + v.add(0, fldHeapPath); + v.add(1, new HashSet()); + v.add(2, new Boolean(false)); + } + ((Set) v.get(1)).add(fld); + } + } + + private void readLocation(FlatNode fn, NTuple fldHeapPath, + Hashtable> curr) { + // TODO Auto-generated method stub + } private void writtenAnalyis() { @@ -93,7 +295,7 @@ public class DefinitelyWrittenCheck { Set flatNodesToVisit = new HashSet(); flatNodesToVisit.add(fm); - FlatNode entrance = null; + LoopFinder loopFinder = new LoopFinder(fm); while (!flatNodesToVisit.isEmpty()) { FlatNode fn = flatNodesToVisit.iterator().next(); @@ -103,7 +305,7 @@ public class DefinitelyWrittenCheck { if (label != null) { if (label.equals(ssjava.SSJAVA)) { - entrance = fn; + ssjavaLoopEntrance = fn; break; } } @@ -114,16 +316,29 @@ public class DefinitelyWrittenCheck { } } - assert entrance != null; + assert ssjavaLoopEntrance != null; + + // assume that ssjava loop is top-level loop in method, not nested loop + Set nestedLoop = loopFinder.nestedLoops(); + for (Iterator loopIter = nestedLoop.iterator(); loopIter.hasNext();) { + LoopFinder lf = (LoopFinder) loopIter.next(); + if (lf.loopEntrances().iterator().next().equals(ssjavaLoopEntrance)) { + ssjavaLoop = lf; + } + } + + assert ssjavaLoop != null; - writtenAnalysis_analyzeLoop(entrance); + writtenAnalysis_analyzeLoop(); } - private void writtenAnalysis_analyzeLoop(FlatNode entrance) { + private void writtenAnalysis_analyzeLoop() { Set flatNodesToVisit = new HashSet(); - flatNodesToVisit.add(entrance); + flatNodesToVisit.add(ssjavaLoopEntrance); + + loopIncElements = (Set) ssjavaLoop.loopIncElements(); while (!flatNodesToVisit.isEmpty()) { FlatNode fn = (FlatNode) flatNodesToVisit.iterator().next(); @@ -143,7 +358,7 @@ public class DefinitelyWrittenCheck { } } - writtenAnalysis_nodeAction(fn, curr, entrance); + writtenAnalysis_nodeAction(fn, curr, ssjavaLoopEntrance); // if a new result, schedule forward nodes for analysis if (!curr.equals(prev)) { @@ -151,7 +366,10 @@ public class DefinitelyWrittenCheck { for (int i = 0; i < fn.numNext(); i++) { FlatNode nn = fn.getNext(i); - flatNodesToVisit.add(nn); + if (loopIncElements.contains(nn)) { + flatNodesToVisit.add(nn); + } + } } } @@ -506,13 +724,11 @@ public class DefinitelyWrittenCheck { // intraprocedural analysis Set flatNodesToVisit = new HashSet(); - Set visited = new HashSet(); flatNodesToVisit.add(fm); while (!flatNodesToVisit.isEmpty()) { FlatNode fn = flatNodesToVisit.iterator().next(); flatNodesToVisit.remove(fn); - visited.add(fn); Set> curr = new HashSet>(); @@ -526,11 +742,11 @@ public class DefinitelyWrittenCheck { methodReadOverWrite_nodeActions(fn, curr, readSet, overWriteSet); - mapFlatNodeToWrittenSet.put(fn, curr); - - for (int i = 0; i < fn.numNext(); i++) { - FlatNode nn = fn.getNext(i); - if (!visited.contains(nn)) { + Set> writtenSetPrev = mapFlatNodeToWrittenSet.get(fn); + if (!curr.equals(writtenSetPrev)) { + mapFlatNodeToWrittenSet.put(fn, curr); + for (int i = 0; i < fn.numNext(); i++) { + FlatNode nn = fn.getNext(i); flatNodesToVisit.add(nn); } } @@ -674,6 +890,11 @@ public class DefinitelyWrittenCheck { } + private void mergeSharedAnaylsis(Hashtable> curr, + Hashtable> in) { + + } + private void merge(Set> curr, Set> in) { if (curr.isEmpty()) { // WrittenSet has a special initial value which covers all possible diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java index ac27f7c3..80a81e9c 100644 --- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java +++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java @@ -12,6 +12,7 @@ import Analysis.Loops.LoopOptimize; import Analysis.Loops.LoopTerminate; import IR.AnnotationDescriptor; import IR.ClassDescriptor; +import IR.Descriptor; import IR.MethodDescriptor; import IR.State; import IR.TypeUtil; @@ -298,4 +299,20 @@ public class SSJavaAnalysis { 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.getSpinLocSet().contains(loc.getLocIdentifier()); + + } } -- 2.34.1