From: yeom Date: Fri, 11 Nov 2011 01:36:58 +0000 (+0000) Subject: working on the written check. X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=1d48db027be382416453caa04e46d6a121c1d1d8;p=IRC.git working on the written check. --- diff --git a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java index aa7a697f..f9e4bb00 100644 --- a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java +++ b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java @@ -3,6 +3,7 @@ package Analysis.SSJava; import java.io.BufferedWriter; import java.io.FileWriter; import java.io.IOException; +import java.util.Enumeration; import java.util.HashSet; import java.util.Hashtable; import java.util.Iterator; @@ -49,7 +50,7 @@ public class DefinitelyWrittenCheck { // maps a flat node to its WrittenSet: this keeps all heap path overwritten // previously. - private Hashtable>> mapFlatNodeToWrittenSet; + private Hashtable>> mapFlatNodeToMustWriteSet; // maps a temp descriptor to its heap path // each temp descriptor has a unique heap path since we do not allow any @@ -58,21 +59,30 @@ public class DefinitelyWrittenCheck { // maps a flat method to the READ that is the set of heap path that is // expected to be written before method invocation - private Hashtable>> mapFlatMethodToRead; + private Hashtable>> mapFlatMethodToReadSet; - // maps a flat method to the OVERWRITE that is the set of heap path that is - // overwritten on every possible path during method invocation - private Hashtable>> mapFlatMethodToOverWrite; + // maps a flat method to the must-write set that is the set of heap path that + // is overwritten on every possible path during method invocation + private Hashtable>> mapFlatMethodToMustWriteSet; - // maps a flat method to the WRITE that is the set of heap path that is - // written to - private Hashtable>> mapFlatMethodToWrite; + // maps a flat method to the may-wirte set that is the set of heap path that + // might be written to + private Hashtable>> mapFlatMethodToMayWriteSet; + + // maps a call site to the read set contributed by all callees + private Hashtable>> mapFlatNodeToBoundReadSet; + + // maps a call site to the must write set contributed by all callees + private Hashtable>> mapFlatNodeToBoundMustWriteSet; + + // maps a call site to the may read set contributed by all callees + private Hashtable>> mapFlatNodeToBoundMayWriteSet; // points to method containing SSJAVA Loop private MethodDescriptor methodContainingSSJavaLoop; // maps a flatnode to definitely written analysis mapping M - private Hashtable, Hashtable>> definitelyWrittenResults; + private Hashtable, Set>> mapFlatNodetoEventLoopMap; // maps a method descriptor to its current summary during the analysis // then analysis reaches fixed-point, this mapping will have the final summary @@ -116,28 +126,30 @@ public class DefinitelyWrittenCheck { private Set loopIncElements; private Set> calleeUnionBoundReadSet; - private Set> calleeIntersectBoundOverWriteSet; - private Set> calleeBoundWriteSet; + private Set> calleeIntersectBoundMustWriteSet; + private Set> calleeUnionBoundMayWriteSet; private Hashtable mapDescToLocation; private TempDescriptor LOCAL; + public static int MAXAGE = 1; + public DefinitelyWrittenCheck(SSJavaAnalysis ssjava, State state) { this.state = state; this.ssjava = ssjava; this.callGraph = ssjava.getCallGraph(); - this.mapFlatNodeToWrittenSet = new Hashtable>>(); + this.mapFlatNodeToMustWriteSet = new Hashtable>>(); this.mapDescriptorToSetDependents = new Hashtable>(); this.mapHeapPath = new Hashtable>(); - this.mapFlatMethodToRead = new Hashtable>>(); - this.mapFlatMethodToOverWrite = new Hashtable>>(); - this.mapFlatMethodToWrite = new Hashtable>>(); - this.definitelyWrittenResults = - new Hashtable, Hashtable>>(); + this.mapFlatMethodToReadSet = new Hashtable>>(); + this.mapFlatMethodToMustWriteSet = new Hashtable>>(); + this.mapFlatMethodToMayWriteSet = new Hashtable>>(); + this.mapFlatNodetoEventLoopMap = + new Hashtable, Set>>(); this.calleeUnionBoundReadSet = new HashSet>(); - this.calleeIntersectBoundOverWriteSet = new HashSet>(); - this.calleeBoundWriteSet = new HashSet>(); + this.calleeIntersectBoundMustWriteSet = new HashSet>(); + this.calleeUnionBoundMayWriteSet = new HashSet>(); this.mapMethodDescriptorToCompleteClearingSummary = new Hashtable(); @@ -152,14 +164,20 @@ public class DefinitelyWrittenCheck { this.possibleCalleeReadSummarySetToCaller = new HashSet(); this.mapMethodDescriptorToReadSummary = new Hashtable(); this.mapFlatNodeToReadSummary = new Hashtable(); + this.mapFlatNodeToBoundReadSet = new Hashtable>>(); + this.mapFlatNodeToBoundMustWriteSet = new Hashtable>>(); + this.mapFlatNodeToBoundMayWriteSet = new Hashtable>>(); } public void definitelyWrittenCheck() { if (!ssjava.getAnnotationRequireSet().isEmpty()) { - methodReadOverWriteAnalysis(); - writtenAnalyis(); - sharedLocationAnalysis(); - checkSharedLocationResult(); + identifyMainEventLoop(); + methodReadWriteSetAnalysis(); + methodReadWriteSetAnalysisToEventLoopBody(); + eventLoopAnalysis(); + computeSharedCoverSet(); + // sharedLocationAnalysis(); + // checkSharedLocationResult(); } } @@ -232,7 +250,7 @@ public class DefinitelyWrittenCheck { // verify that all concrete locations of shared location are cleared out at // the same time once per the out-most loop - computeReadSharedDescriptorSet(); + computeSharedCoverSet(); if (state.SSJAVADEBUG) { writeReadMapFile(); @@ -877,7 +895,7 @@ public class DefinitelyWrittenCheck { return boundHeapPath; } - private void computeReadSharedDescriptorSet() { + private void computeSharedCoverSet() { LinkedList descriptorListToAnalyze = (LinkedList) sortedDescriptors.clone(); @@ -886,6 +904,8 @@ public class DefinitelyWrittenCheck { // dependency in the call graph methodDescriptorsToVisitStack.clear(); + descriptorListToAnalyze.removeFirst(); + Set methodDescriptorToVistSet = new HashSet(); methodDescriptorToVistSet.addAll(descriptorListToAnalyze); @@ -1271,88 +1291,35 @@ public class DefinitelyWrittenCheck { return state; } - private void writtenAnalyis() { + private void eventLoopAnalysis() { // perform second stage analysis: intraprocedural analysis ensure that // all // variables are definitely written in-between the same read - // First, identify ssjava loop entrace - FlatMethod fm = state.getMethodFlat(methodContainingSSJavaLoop); - Set flatNodesToVisit = new HashSet(); - flatNodesToVisit.add(fm); - - LoopFinder loopFinder = new LoopFinder(fm); - - while (!flatNodesToVisit.isEmpty()) { - FlatNode fn = flatNodesToVisit.iterator().next(); - flatNodesToVisit.remove(fn); - - String label = (String) state.fn2labelMap.get(fn); - if (label != null) { - - if (label.equals(ssjava.SSJAVA)) { - ssjavaLoopEntrance = fn; - break; - } - } - - for (int i = 0; i < fn.numNext(); i++) { - FlatNode nn = fn.getNext(i); - flatNodesToVisit.add(nn); - } - } - - 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(); - - if (debugcount > 0) { - throw new Error(); - } - - } - - private void writtenAnalysis_analyzeLoop() { - Set flatNodesToVisit = new HashSet(); flatNodesToVisit.add(ssjavaLoopEntrance); - loopIncElements = (Set) ssjavaLoop.loopIncElements(); - while (!flatNodesToVisit.isEmpty()) { FlatNode fn = (FlatNode) flatNodesToVisit.iterator().next(); flatNodesToVisit.remove(fn); - Hashtable, Hashtable> prev = - definitelyWrittenResults.get(fn); + Hashtable, Set> prev = mapFlatNodetoEventLoopMap.get(fn); - Hashtable, Hashtable> curr = - new Hashtable, Hashtable>(); + Hashtable, Set> curr = + new Hashtable, Set>(); for (int i = 0; i < fn.numPrev(); i++) { FlatNode nn = fn.getPrev(i); - Hashtable, Hashtable> dwIn = - definitelyWrittenResults.get(nn); - if (dwIn != null) { - merge(curr, dwIn); + Hashtable, Set> in = mapFlatNodetoEventLoopMap.get(nn); + if (in != null) { + union(curr, in); } } - writtenAnalysis_nodeAction(fn, curr, ssjavaLoopEntrance); + eventLoopAnalysis_nodeAction(fn, curr, ssjavaLoopEntrance); // if a new result, schedule forward nodes for analysis if (!curr.equals(prev)) { - definitelyWrittenResults.put(fn, curr); + mapFlatNodetoEventLoopMap.put(fn, curr); for (int i = 0; i < fn.numNext(); i++) { FlatNode nn = fn.getNext(i); @@ -1365,56 +1332,87 @@ public class DefinitelyWrittenCheck { } } - private void writtenAnalysis_nodeAction(FlatNode fn, - Hashtable, Hashtable> curr, FlatNode loopEntrance) { + private void union(Hashtable, Set> curr, + Hashtable, Set> in) { + + Set> inKeySet = in.keySet(); + for (Iterator iterator = inKeySet.iterator(); iterator.hasNext();) { + NTuple inKey = (NTuple) iterator.next(); + Set inSet = in.get(inKey); + + Set currSet = curr.get(inKey); + + if (currSet == null) { + currSet = new HashSet(); + curr.put(inKey, currSet); + } + currSet.addAll(inSet); + } + + } + + private void eventLoopAnalysis_nodeAction(FlatNode fn, + Hashtable, Set> curr, FlatNode loopEntrance) { + + Hashtable, Set> KILLSet = + new Hashtable, Set>(); + Hashtable, Set> GENSet = + new Hashtable, Set>(); if (fn.equals(loopEntrance)) { // it reaches loop entrance: changes all flag to true Set> keySet = curr.keySet(); for (Iterator iterator = keySet.iterator(); iterator.hasNext();) { NTuple key = (NTuple) iterator.next(); - Hashtable pair = curr.get(key); - if (pair != null) { - Set pairKeySet = pair.keySet(); - for (Iterator iterator2 = pairKeySet.iterator(); iterator2.hasNext();) { - FlatNode pairKey = (FlatNode) iterator2.next(); - pair.put(pairKey, Boolean.TRUE); - } + Set writeAgeSet = curr.get(key); + + Set incSet = new HashSet(); + incSet.addAll(writeAgeSet); + writeAgeSet.clear(); + + for (Iterator iterator2 = incSet.iterator(); iterator2.hasNext();) { + WriteAge writeAge = (WriteAge) iterator2.next(); + WriteAge newWriteAge = writeAge.copy(); + newWriteAge.inc(); + writeAgeSet.add(newWriteAge); } + } + // System.out.println("EVENT LOOP ENTRY=" + curr); + } else { TempDescriptor lhs; TempDescriptor rhs; FieldDescriptor fld; switch (fn.kind()) { + case FKind.FlatOpNode: { FlatOpNode fon = (FlatOpNode) fn; lhs = fon.getDest(); rhs = fon.getLeft(); - NTuple rhsHeapPath = computePath(rhs); - if (!rhs.getType().isImmutable()) { - mapHeapPath.put(lhs, rhsHeapPath); - } else { - if (fon.getOp().getOp() == Operation.ASSIGN) { - // read(rhs) - readValue(fn, rhsHeapPath, curr); - } - // write(lhs) - NTuple lhsHeapPath = computePath(lhs); - removeHeapPath(curr, lhsHeapPath); - } - } - break; + if (!lhs.getSymbol().startsWith("neverused")) { + NTuple rhsHeapPath = computePath(rhs); + if (!rhs.getType().isImmutable()) { + mapHeapPath.put(lhs, rhsHeapPath); + } else { + // write(lhs) + // NTuple lhsHeapPath = computePath(lhs); + NTuple path = new NTuple(); + path.add(lhs); - case FKind.FlatLiteralNode: { - FlatLiteralNode fln = (FlatLiteralNode) fn; - lhs = fln.getDst(); + // System.out.println("WRITE VARIABLE=" + path + " from=" + lhs); - // write(lhs) - NTuple lhsHeapPath = computePath(lhs); - removeHeapPath(curr, lhsHeapPath); + computeKILLSetForWrite(curr, path, KILLSet); + computeGENSetForWrite(path, GENSet); + + // System.out.println("#VARIABLE WRITE:" + fn); + // System.out.println("#KILLSET=" + KILLSet); + // System.out.println("#GENSet=" + GENSet); + + } + } } break; @@ -1435,32 +1433,20 @@ public class DefinitelyWrittenCheck { fld = getArrayField(td); } - if (fld.isFinal() /* && fld.isStatic() */) { - // if field is final and static, no need to check - break; - } - // read field NTuple srcHeapPath = mapHeapPath.get(rhs); - NTuple fldHeapPath; if (srcHeapPath != null) { fldHeapPath = new NTuple(srcHeapPath.getList()); } else { // if srcHeapPath is null, it is static reference - System.out.println("##"); - System.out.println("rhs=" + rhs + " fd=" + fld); fldHeapPath = new NTuple(); fldHeapPath.add(rhs); } fldHeapPath.add(fld); - if (fld.getType().isImmutable()) { - readValue(fn, fldHeapPath, curr); - } - - // propagate rhs's heap path to the lhs - mapHeapPath.put(lhs, fldHeapPath); + Set writeAgeSet = curr.get(fldHeapPath); + checkWriteAgeSet(writeAgeSet, fldHeapPath, fn); } break; @@ -1484,7 +1470,13 @@ public class DefinitelyWrittenCheck { NTuple lhsHeapPath = computePath(lhs); NTuple fldHeapPath = new NTuple(lhsHeapPath.getList()); fldHeapPath.add(fld); - removeHeapPath(curr, fldHeapPath); + + computeKILLSetForWrite(curr, fldHeapPath, KILLSet); + computeGENSetForWrite(fldHeapPath, GENSet); + + // System.out.println("FIELD WRITE:" + fn); + // System.out.println("KILLSET=" + KILLSet); + // System.out.println("GENSet=" + GENSet); } break; @@ -1492,41 +1484,104 @@ public class DefinitelyWrittenCheck { case FKind.FlatCall: { FlatCall fc = (FlatCall) fn; - bindHeapPathCallerArgWithCaleeParam(fc); - // add in which hp is an element of - // READ_bound set - // of callee: callee has 'read' requirement! - - for (Iterator iterator = calleeUnionBoundReadSet.iterator(); iterator.hasNext();) { - NTuple read = (NTuple) iterator.next(); - Hashtable gen = curr.get(read); - if (gen == null) { - gen = new Hashtable(); - curr.put(read, gen); - } - Boolean currentStatus = gen.get(fn); - if (currentStatus == null) { - gen.put(fn, Boolean.FALSE); - } else { - checkFlag(currentStatus.booleanValue(), fn, read); - } - } + generateKILLSetForFlatCall(fc, curr, KILLSet); + generateGENSetForFlatCall(fc, GENSet); + + // System.out.println("FLATCALL:" + fn); + // System.out.println("KILLSET=" + KILLSet); + // System.out.println("GENSet=" + GENSet); - // removes if hp is an element of - // OVERWRITE_bound - // set of callee. it means that callee will overwrite it - for (Iterator iterator = calleeIntersectBoundOverWriteSet.iterator(); iterator.hasNext();) { - NTuple write = (NTuple) iterator.next(); - removeHeapPath(curr, write); - } } break; } + + computeNewMapping(curr, KILLSet, GENSet); + // System.out.println("#######" + curr); + + } + + } + + private void checkWriteAgeSet(Set writeAgeSet, NTuple path, FlatNode fn) { + if (writeAgeSet != null) { + for (Iterator iterator = writeAgeSet.iterator(); iterator.hasNext();) { + WriteAge writeAge = (WriteAge) iterator.next(); + if (writeAge.getAge() >= MAXAGE) { + throw new Error( + "Memory location, which is reachable through references " + + path + + ", who comes back to the same read statement without being overwritten at the out-most iteration at " + + methodContainingSSJavaLoop.getClassDesc().getSourceFileName() + "::" + + fn.getNumLine()); + } + } + } + } + + private void generateGENSetForFlatCall(FlatCall fc, + Hashtable, Set> GENSet) { + + Set> boundMayWriteSet = mapFlatNodeToBoundMayWriteSet.get(fc); + + for (Iterator iterator = boundMayWriteSet.iterator(); iterator.hasNext();) { + NTuple key = (NTuple) iterator.next(); + // TODO: shared location + Set set = new HashSet(); + set.add(new WriteAge(0)); + GENSet.put(key, set); + } + + } + + private void generateKILLSetForFlatCall(FlatCall fc, + Hashtable, Set> curr, + Hashtable, Set> KILLSet) { + + Set> boundMustWriteSet = mapFlatNodeToBoundMustWriteSet.get(fc); + + for (Iterator iterator = boundMustWriteSet.iterator(); iterator.hasNext();) { + NTuple key = (NTuple) iterator.next(); + // TODO: shared location + if (curr.get(key) != null) { + KILLSet.put(key, curr.get(key)); + } } } + private void computeNewMapping(Hashtable, Set> curr, + Hashtable, Set> KILLSet, + Hashtable, Set> GENSet) { + + for (Enumeration> e = KILLSet.keys(); e.hasMoreElements();) { + NTuple key = e.nextElement(); + + Set writeAgeSet = curr.get(key); + if (writeAgeSet == null) { + writeAgeSet = new HashSet(); + curr.put(key, writeAgeSet); + } + writeAgeSet.removeAll(KILLSet.get(key)); + } + + for (Enumeration> e = GENSet.keys(); e.hasMoreElements();) { + NTuple key = e.nextElement(); + curr.put(key, GENSet.get(key)); + } + + } + + private void computeGENSetForWrite(NTuple fldHeapPath, + Hashtable, Set> GENSet) { + + // generate write age 0 for the field being written to + Set writeAgeSet = new HashSet(); + writeAgeSet.add(new WriteAge(0)); + GENSet.put(fldHeapPath, writeAgeSet); + + } + private void readValue(FlatNode fn, NTuple hp, Hashtable, Hashtable> curr) { Hashtable gen = curr.get(hp); @@ -1543,8 +1598,8 @@ public class DefinitelyWrittenCheck { } - private void removeHeapPath(Hashtable, Hashtable> curr, - NTuple hp) { + private void computeKILLSetForWrite(Hashtable, Set> curr, + NTuple hp, Hashtable, Set> KILLSet) { // removes all of heap path that starts with prefix 'hp' // since any reference overwrite along heap path gives overwriting side @@ -1554,7 +1609,7 @@ public class DefinitelyWrittenCheck { for (Iterator> iter = keySet.iterator(); iter.hasNext();) { NTuple key = iter.next(); if (key.startsWith(hp)) { - curr.put(key, new Hashtable()); + KILLSet.put(key, curr.get(key)); } } @@ -1562,24 +1617,22 @@ public class DefinitelyWrittenCheck { private void bindHeapPathCallerArgWithCaleeParam(FlatCall fc) { // compute all possible callee set - // transform all READ/OVERWRITE set from the any possible - // callees to the - // caller + // transform all READ/WRITE set from the any possible + // callees to the caller calleeUnionBoundReadSet.clear(); - calleeIntersectBoundOverWriteSet.clear(); - calleeBoundWriteSet.clear(); + calleeIntersectBoundMustWriteSet.clear(); + calleeUnionBoundMayWriteSet.clear(); if (ssjava.isSSJavaUtil(fc.getMethod().getClassDesc())) { // ssjava util case! // have write effects on the first argument TempDescriptor arg = fc.getArg(0); NTuple argHeapPath = computePath(arg); - calleeIntersectBoundOverWriteSet.add(argHeapPath); + calleeIntersectBoundMustWriteSet.add(argHeapPath); + calleeUnionBoundMayWriteSet.add(argHeapPath); } else { MethodDescriptor mdCallee = fc.getMethod(); - // FlatMethod fmCallee = state.getMethodFlat(mdCallee); Set setPossibleCallees = new HashSet(); - // setPossibleCallees.addAll(callGraph.getMethods(mdCallee, typeDesc)); setPossibleCallees.addAll(callGraph.getMethods(mdCallee)); // create mapping from arg idx to its heap paths @@ -1610,24 +1663,26 @@ public class DefinitelyWrittenCheck { // binding caller's args and callee's params - Set> calleeReadSet = mapFlatMethodToRead.get(calleeFlatMethod); + Set> calleeReadSet = mapFlatMethodToReadSet.get(calleeFlatMethod); if (calleeReadSet == null) { calleeReadSet = new HashSet>(); - mapFlatMethodToRead.put(calleeFlatMethod, calleeReadSet); + mapFlatMethodToReadSet.put(calleeFlatMethod, calleeReadSet); } - Set> calleeOverWriteSet = mapFlatMethodToOverWrite.get(calleeFlatMethod); + Set> calleeMustWriteSet = + mapFlatMethodToMustWriteSet.get(calleeFlatMethod); - if (calleeOverWriteSet == null) { - calleeOverWriteSet = new HashSet>(); - mapFlatMethodToOverWrite.put(calleeFlatMethod, calleeOverWriteSet); + if (calleeMustWriteSet == null) { + calleeMustWriteSet = new HashSet>(); + mapFlatMethodToMustWriteSet.put(calleeFlatMethod, calleeMustWriteSet); } - Set> calleeWriteSet = mapFlatMethodToWrite.get(calleeFlatMethod); + Set> calleeMayWriteSet = + mapFlatMethodToMayWriteSet.get(calleeFlatMethod); - if (calleeWriteSet == null) { - calleeWriteSet = new HashSet>(); - mapFlatMethodToWrite.put(calleeFlatMethod, calleeWriteSet); + if (calleeMayWriteSet == null) { + calleeMayWriteSet = new HashSet>(); + mapFlatMethodToMayWriteSet.put(calleeFlatMethod, calleeMayWriteSet); } Hashtable mapParamIdx2ParamTempDesc = @@ -1647,16 +1702,17 @@ public class DefinitelyWrittenCheck { // union of the current read set and the current callee's // read set calleeUnionBoundReadSet.addAll(calleeBoundReadSet); - Set> calleeBoundOverWriteSet = - bindSet(calleeOverWriteSet, mapParamIdx2ParamTempDesc, mapArgIdx2CallerArgHeapPath); + + Set> calleeBoundMustWriteSet = + bindSet(calleeMustWriteSet, mapParamIdx2ParamTempDesc, mapArgIdx2CallerArgHeapPath); // intersection of the current overwrite set and the current // callee's // overwrite set - merge(calleeIntersectBoundOverWriteSet, calleeBoundOverWriteSet); + merge(calleeIntersectBoundMustWriteSet, calleeBoundMustWriteSet); Set> boundWriteSetFromCallee = - bindSet(calleeWriteSet, mapParamIdx2ParamTempDesc, mapArgIdx2CallerArgHeapPath); - calleeBoundWriteSet.addAll(boundWriteSetFromCallee); + bindSet(calleeMayWriteSet, mapParamIdx2ParamTempDesc, mapArgIdx2CallerArgHeapPath); + calleeUnionBoundMayWriteSet.addAll(boundWriteSetFromCallee); } } @@ -1667,7 +1723,7 @@ public class DefinitelyWrittenCheck { if (booleanValue) { // the definitely written analysis only takes care about locations that // are written to inside of the SSJava loop - for (Iterator iterator = calleeBoundWriteSet.iterator(); iterator.hasNext();) { + for (Iterator iterator = calleeUnionBoundMayWriteSet.iterator(); iterator.hasNext();) { NTuple write = (NTuple) iterator.next(); if (hp.startsWith(write)) { // it has write effect! @@ -1685,39 +1741,55 @@ public class DefinitelyWrittenCheck { } } - private void merge(Hashtable, Hashtable> curr, - Hashtable, Hashtable> in) { + private void identifyMainEventLoop() { + // First, identify ssjava loop entrace - Set> inKeySet = in.keySet(); - for (Iterator iterator = inKeySet.iterator(); iterator.hasNext();) { - NTuple inKey = (NTuple) iterator.next(); - Hashtable inPair = in.get(inKey); + // no need to analyze method having ssjava loop + methodContainingSSJavaLoop = ssjava.getMethodContainingSSJavaLoop(); - Set pairKeySet = inPair.keySet(); - for (Iterator iterator2 = pairKeySet.iterator(); iterator2.hasNext();) { - FlatNode pairKey = (FlatNode) iterator2.next(); - Boolean inFlag = inPair.get(pairKey); + FlatMethod fm = state.getMethodFlat(methodContainingSSJavaLoop); + Set flatNodesToVisit = new HashSet(); + flatNodesToVisit.add(fm); - Hashtable currPair = curr.get(inKey); - if (currPair == null) { - currPair = new Hashtable(); - curr.put(inKey, currPair); - } + LoopFinder loopFinder = new LoopFinder(fm); + + while (!flatNodesToVisit.isEmpty()) { + FlatNode fn = flatNodesToVisit.iterator().next(); + flatNodesToVisit.remove(fn); + + String label = (String) state.fn2labelMap.get(fn); + if (label != null) { - Boolean currFlag = currPair.get(pairKey); - // by default, flag is set by false - if (currFlag == null) { - currFlag = Boolean.FALSE; + if (label.equals(ssjava.SSJAVA)) { + ssjavaLoopEntrance = fn; + break; } - currFlag = Boolean.valueOf(inFlag.booleanValue() | currFlag.booleanValue()); - currPair.put(pairKey, currFlag); } + for (int i = 0; i < fn.numNext(); i++) { + FlatNode nn = fn.getNext(i); + flatNodesToVisit.add(nn); + } } + 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; + + loopIncElements = (Set) ssjavaLoop.loopIncElements(); + } - private void methodReadOverWriteAnalysis() { + private void methodReadWriteSetAnalysis() { // perform method READ/OVERWRITE analysis Set methodDescriptorsToAnalyze = new HashSet(); methodDescriptorsToAnalyze.addAll(ssjava.getAnnotationRequireSet()); @@ -1727,15 +1799,13 @@ public class DefinitelyWrittenCheck { LinkedList descriptorListToAnalyze = (LinkedList) sortedDescriptors.clone(); - // no need to analyze method having ssjava loop - // methodContainingSSJavaLoop = descriptorListToAnalyze.removeFirst(); - methodContainingSSJavaLoop = ssjava.getMethodContainingSSJavaLoop(); - // current descriptors to visit in fixed-point interprocedural analysis, // prioritized by // dependency in the call graph methodDescriptorsToVisitStack.clear(); + descriptorListToAnalyze.removeFirst(); + Set methodDescriptorToVistSet = new HashSet(); methodDescriptorToVistSet.addAll(descriptorListToAnalyze); @@ -1751,20 +1821,20 @@ public class DefinitelyWrittenCheck { FlatMethod fm = state.getMethodFlat(md); Set> readSet = new HashSet>(); - Set> overWriteSet = new HashSet>(); - Set> writeSet = new HashSet>(); + Set> mustWriteSet = new HashSet>(); + Set> mayWriteSet = new HashSet>(); - methodReadOverWrite_analyzeMethod(fm, readSet, overWriteSet, writeSet); + methodReadWriteSet_analyzeMethod(fm, readSet, mustWriteSet, mayWriteSet); - Set> prevRead = mapFlatMethodToRead.get(fm); - Set> prevOverWrite = mapFlatMethodToOverWrite.get(fm); - Set> prevWrite = mapFlatMethodToWrite.get(fm); + Set> prevRead = mapFlatMethodToReadSet.get(fm); + Set> prevMustWrite = mapFlatMethodToMustWriteSet.get(fm); + Set> prevMayWrite = mapFlatMethodToMayWriteSet.get(fm); - if (!(readSet.equals(prevRead) && overWriteSet.equals(prevOverWrite) && writeSet - .equals(prevWrite))) { - mapFlatMethodToRead.put(fm, readSet); - mapFlatMethodToOverWrite.put(fm, overWriteSet); - mapFlatMethodToWrite.put(fm, writeSet); + if (!(readSet.equals(prevRead) && mustWriteSet.equals(prevMustWrite) && mayWriteSet + .equals(prevMayWrite))) { + mapFlatMethodToReadSet.put(fm, readSet); + mapFlatMethodToMustWriteSet.put(fm, mustWriteSet); + mapFlatMethodToMayWriteSet.put(fm, mayWriteSet); // results for callee changed, so enqueue dependents caller for // further @@ -1785,38 +1855,75 @@ public class DefinitelyWrittenCheck { } - private void methodReadOverWrite_analyzeMethod(FlatMethod fm, Set> readSet, - Set> overWriteSet, Set> writeSet) { + private void methodReadWriteSet_analyzeMethod(FlatMethod fm, Set> readSet, + Set> mustWriteSet, Set> mayWriteSet) { if (state.SSJAVADEBUG) { System.out.println("SSJAVA: Definitely written Analyzing: " + fm); } + methodReadWriteSet_analyzeBody(fm, readSet, mustWriteSet, mayWriteSet, null); + + } + + private void methodReadWriteSetAnalysisToEventLoopBody() { + + // perform method read/write analysis for Event Loop Body + + FlatMethod flatMethodContainingSSJavaLoop = state.getMethodFlat(methodContainingSSJavaLoop); + + if (state.SSJAVADEBUG) { + System.out.println("SSJAVA: Definitely written Event Loop Analyzing: " + + flatMethodContainingSSJavaLoop); + } + + Set> readSet = new HashSet>(); + Set> mustWriteSet = new HashSet>(); + Set> mayWriteSet = new HashSet>(); + + mapFlatMethodToReadSet.put(flatMethodContainingSSJavaLoop, readSet); + mapFlatMethodToMustWriteSet.put(flatMethodContainingSSJavaLoop, mustWriteSet); + mapFlatMethodToMayWriteSet.put(flatMethodContainingSSJavaLoop, mayWriteSet); + + loopIncElements = (Set) ssjavaLoop.loopIncElements(); + + methodReadWriteSet_analyzeBody(ssjavaLoopEntrance, readSet, mustWriteSet, mayWriteSet, + loopIncElements); + + } + + private void methodReadWriteSet_analyzeBody(FlatNode startNode, Set> readSet, + Set> mustWriteSet, Set> mayWriteSet, + Set bodyNodeSet) { + // intraprocedural analysis Set flatNodesToVisit = new HashSet(); - flatNodesToVisit.add(fm); + flatNodesToVisit.add(startNode); while (!flatNodesToVisit.isEmpty()) { FlatNode fn = flatNodesToVisit.iterator().next(); flatNodesToVisit.remove(fn); - Set> curr = new HashSet>(); + Set> currMustWriteSet = new HashSet>(); for (int i = 0; i < fn.numPrev(); i++) { FlatNode prevFn = fn.getPrev(i); - Set> in = mapFlatNodeToWrittenSet.get(prevFn); + Set> in = mapFlatNodeToMustWriteSet.get(prevFn); if (in != null) { - merge(curr, in); + merge(currMustWriteSet, in); } } - methodReadOverWrite_nodeActions(fn, curr, readSet, overWriteSet, writeSet); + methodReadWriteSet_nodeActions(fn, currMustWriteSet, readSet, mustWriteSet, mayWriteSet); - Set> writtenSetPrev = mapFlatNodeToWrittenSet.get(fn); - if (!curr.equals(writtenSetPrev)) { - mapFlatNodeToWrittenSet.put(fn, curr); + Set> mustSetPrev = mapFlatNodeToMustWriteSet.get(fn); + if (!currMustWriteSet.equals(mustSetPrev)) { + mapFlatNodeToMustWriteSet.put(fn, currMustWriteSet); for (int i = 0; i < fn.numNext(); i++) { FlatNode nn = fn.getNext(i); - flatNodesToVisit.add(nn); + if (bodyNodeSet == null || bodyNodeSet.contains(nn)) { + flatNodesToVisit.add(nn); + } + } } @@ -1824,9 +1931,9 @@ public class DefinitelyWrittenCheck { } - private void methodReadOverWrite_nodeActions(FlatNode fn, Set> writtenSet, - Set> readSet, Set> overWriteSet, - Set> writeSet) { + private void methodReadWriteSet_nodeActions(FlatNode fn, + Set> currMustWriteSet, Set> readSet, + Set> mustWriteSet, Set> mayWriteSet) { TempDescriptor lhs; TempDescriptor rhs; FieldDescriptor fld; @@ -1856,6 +1963,10 @@ public class DefinitelyWrittenCheck { NTuple rhsHeapPath = mapHeapPath.get(rhs); if (rhsHeapPath != null) { mapHeapPath.put(lhs, mapHeapPath.get(rhs)); + } else { + NTuple heapPath = new NTuple(); + heapPath.add(rhs); + mapHeapPath.put(lhs, heapPath); } } @@ -1865,7 +1976,7 @@ public class DefinitelyWrittenCheck { case FKind.FlatElementNode: case FKind.FlatFieldNode: { - // y=x.f; + // x=y.f; if (fn.kind() == FKind.FlatFieldNode) { FlatFieldNode ffn = (FlatFieldNode) fn; @@ -1880,8 +1991,8 @@ public class DefinitelyWrittenCheck { fld = getArrayField(td); } - if (fld.isFinal() /* && fld.isStatic() */) { - // if field is final and static, no need to check + if (fld.isFinal()) { + // if field is final no need to check break; } @@ -1898,7 +2009,7 @@ public class DefinitelyWrittenCheck { // read (x.f) if (fld.getType().isImmutable()) { // if WT doesnot have hp(x.f), add hp(x.f) to READ - if (!writtenSet.contains(readingHeapPath)) { + if (!currMustWriteSet.contains(readingHeapPath)) { readSet.add(readingHeapPath); } } @@ -1929,6 +2040,7 @@ public class DefinitelyWrittenCheck { // set up heap path NTuple lhsHeapPath = mapHeapPath.get(lhs); + if (lhsHeapPath != null) { // if lhs heap path is null, it means that it is not reachable from // callee's parameters. so just ignore it @@ -1938,9 +2050,9 @@ public class DefinitelyWrittenCheck { // write(x.f) // need to add hp(y) to WT - writtenSet.add(newHeapPath); + currMustWriteSet.add(newHeapPath); + mayWriteSet.add(newHeapPath); - writeSet.add(newHeapPath); } } @@ -1952,28 +2064,32 @@ public class DefinitelyWrittenCheck { bindHeapPathCallerArgWithCaleeParam(fc); + mapFlatNodeToBoundReadSet.put(fn, calleeUnionBoundReadSet); + mapFlatNodeToBoundMustWriteSet.put(fn, calleeIntersectBoundMustWriteSet); + mapFlatNodeToBoundMayWriteSet.put(fn, calleeUnionBoundMayWriteSet); + // add heap path, which is an element of READ_bound set and is not // an // element of WT set, to the caller's READ set for (Iterator iterator = calleeUnionBoundReadSet.iterator(); iterator.hasNext();) { NTuple read = (NTuple) iterator.next(); - if (!writtenSet.contains(read)) { + if (!currMustWriteSet.contains(read)) { readSet.add(read); } } // add heap path, which is an element of OVERWRITE_bound set, to the // caller's WT set - for (Iterator iterator = calleeIntersectBoundOverWriteSet.iterator(); iterator.hasNext();) { + for (Iterator iterator = calleeIntersectBoundMustWriteSet.iterator(); iterator.hasNext();) { NTuple write = (NTuple) iterator.next(); - writtenSet.add(write); + currMustWriteSet.add(write); } // add heap path, which is an element of WRITE_BOUND set, to the // caller's writeSet - for (Iterator iterator = calleeBoundWriteSet.iterator(); iterator.hasNext();) { + for (Iterator iterator = calleeUnionBoundMayWriteSet.iterator(); iterator.hasNext();) { NTuple write = (NTuple) iterator.next(); - writeSet.add(write); + mayWriteSet.add(write); } } @@ -1981,7 +2097,7 @@ public class DefinitelyWrittenCheck { case FKind.FlatExit: { // merge the current written set with OVERWRITE set - merge(overWriteSet, writtenSet); + merge(mustWriteSet, currMustWriteSet); } break; @@ -2068,7 +2184,7 @@ public class DefinitelyWrittenCheck { private void merge(Set> curr, Set> in) { if (curr.isEmpty()) { - // WrittenSet has a special initial value which covers all possible + // set has a special initial value which covers all possible // elements // For the first time of intersection, we can take all previous set curr.addAll(in); diff --git a/Robust/src/Analysis/SSJava/WriteAge.java b/Robust/src/Analysis/SSJava/WriteAge.java new file mode 100644 index 00000000..83aefdb2 --- /dev/null +++ b/Robust/src/Analysis/SSJava/WriteAge.java @@ -0,0 +1,53 @@ +package Analysis.SSJava; + +public class WriteAge { + + private int writeAge; + + public WriteAge(int age) { + this.writeAge = age; + } + + public int getAge() { + return writeAge; + } + + public WriteAge copy() { + return new WriteAge(writeAge); + } + + public void inc() { + if (writeAge <= DefinitelyWrittenCheck.MAXAGE) { + writeAge++; + } + } + + public int hashCode() { + return 31 + writeAge; + } + + public boolean equals(Object obj) { + if (this == obj) { + return true; + } + if (obj == null) { + return false; + } + if (!(obj instanceof WriteAge)) { + return false; + } + WriteAge other = (WriteAge) obj; + if (writeAge != other.writeAge) { + return false; + } + return true; + } + + public String toString() { + if (writeAge > DefinitelyWrittenCheck.MAXAGE) { + return "many"; + } + return Integer.toString(writeAge); + } + +} diff --git a/Robust/src/Tests/ssJava/written/makefile b/Robust/src/Tests/ssJava/written/makefile new file mode 100644 index 00000000..b6d1119d --- /dev/null +++ b/Robust/src/Tests/ssJava/written/makefile @@ -0,0 +1,26 @@ +BUILDSCRIPT=../../../buildscript + +PROGRAM=test +SOURCE_FILES=test.java + +BSFLAGS= -32bit -ssjava -ssjavadebug -printlinenum -mainclass $(PROGRAM) -heapsize-mb 1000 -garbagestats -joptimize -optimize -debug #-nooptimize #src-after-pp #-debug + +default: $(PROGRAM)s.bin + +$(PROGRAM)s.bin: $(SOURCE_FILES) makefile + $(BUILDSCRIPT) $(BSFLAGS) -o $(PROGRAM)s -builddir sing $(SOURCE_FILES) + +clean: + rm -f $(PROGRAM)s.bin + rm -fr sing + rm -f tmp.c + rm -f *~ + rm -f *.dot + rm -f *.png + rm -f *.txt + rm -f aliases.txt + rm -f mlpReport*txt + rm -f results*txt + rm -f *log + rm -f coreprof.dat + rm -f trace.out diff --git a/Robust/src/Tests/ssJava/written/test.java b/Robust/src/Tests/ssJava/written/test.java new file mode 100644 index 00000000..ec18b175 --- /dev/null +++ b/Robust/src/Tests/ssJava/written/test.java @@ -0,0 +1,52 @@ +@LATTICE("L