From: yeom Date: Fri, 1 Jul 2011 02:11:29 +0000 (+0000) Subject: getting close to finishing the definite written analysis X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=3c22dfa50afe37717280b9b02e2bb9b3b0403ba6;p=IRC.git getting close to finishing the definite written analysis --- diff --git a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java index 5487b4b6..8033efd4 100644 --- a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java +++ b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java @@ -5,6 +5,7 @@ import java.util.Hashtable; import java.util.Iterator; import java.util.LinkedList; import java.util.Set; +import java.util.Stack; import Analysis.CallGraph.CallGraph; import IR.Descriptor; @@ -12,7 +13,9 @@ import IR.FieldDescriptor; import IR.MethodDescriptor; import IR.Operation; import IR.State; +import IR.TypeDescriptor; import IR.Flat.FKind; +import IR.Flat.FlatCall; import IR.Flat.FlatFieldNode; import IR.Flat.FlatLiteralNode; import IR.Flat.FlatMethod; @@ -49,7 +52,11 @@ public class DefinitelyWrittenCheck { // overwritten on every possible path during method invocation private Hashtable>> mapFlatMethodToOverWrite; - private Hashtable>> definitelyWrittenResults; + // points to method containing SSJAVA Loop + private MethodDescriptor methodContainingSSJavaLoop; + + // maps a flatnode to definitely written analysis mapping M + private Hashtable, Hashtable>> definitelyWrittenResults; public DefinitelyWrittenCheck(SSJavaAnalysis ssjava, State state) { this.state = state; @@ -60,50 +67,408 @@ public class DefinitelyWrittenCheck { this.mapHeapPath = new Hashtable>(); this.mapFlatMethodToRead = new Hashtable>>(); this.mapFlatMethodToOverWrite = new Hashtable>>(); + this.definitelyWrittenResults = + new Hashtable, Hashtable>>(); } public void definitelyWrittenCheck() { + methodReadOverWriteAnalysis(); + writtenAnalyis(); + } + + private void writtenAnalyis() { + // 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); + + FlatNode entrance = null; + + 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)) { + entrance = fn; + break; + } + } + + for (int i = 0; i < fn.numNext(); i++) { + FlatNode nn = fn.getNext(i); + flatNodesToVisit.add(nn); + } + } + + assert entrance != null; + + writtenAnalysis_analyzeLoop(entrance); - analyzeMethods(); } - private void analyzeMethods() { - // perform method READ/OVERWRITE analysis + private void writtenAnalysis_analyzeLoop(FlatNode entrance) { + + Set flatNodesToVisit = new HashSet(); + flatNodesToVisit.add(entrance); + + while (!flatNodesToVisit.isEmpty()) { + FlatNode fn = (FlatNode) flatNodesToVisit.iterator().next(); + flatNodesToVisit.remove(fn); + + Hashtable, Hashtable> prev = + definitelyWrittenResults.get(fn); + + Hashtable, Hashtable> curr = + new Hashtable, Hashtable>(); + 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); + } + } + + writtenAnalysis_nodeAction(fn, curr, entrance); + // definitelyWritten_nodeActions(fn, curr, entrance); + + // if a new result, schedule forward nodes for analysis + if (!curr.equals(prev)) { + definitelyWrittenResults.put(fn, curr); + + for (int i = 0; i < fn.numNext(); i++) { + FlatNode nn = fn.getNext(i); + flatNodesToVisit.add(nn); + } + } + } + } + + private void writtenAnalysis_nodeAction(FlatNode fn, + Hashtable, Hashtable> curr, FlatNode loopEntrance) { + 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); + } + } + } + } 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); + } + + if (fon.getOp().getOp() == Operation.ASSIGN) { + // read(rhs) + Hashtable gen = curr.get(rhsHeapPath); + + if (gen == null) { + gen = new Hashtable(); + curr.put(rhsHeapPath, gen); + } + Boolean currentStatus = gen.get(fn); + if (currentStatus == null) { + gen.put(fn, Boolean.FALSE); + } else { + if (!rhs.getType().isClass()) { + checkFlag(currentStatus.booleanValue(), fn); + } + } + + } + // write(lhs) + NTuple lhsHeapPath = computePath(lhs); + curr.put(lhsHeapPath, new Hashtable()); + } + break; + + case FKind.FlatLiteralNode: { + FlatLiteralNode fln = (FlatLiteralNode) fn; + lhs = fln.getDst(); + + // write(lhs) + NTuple lhsHeapPath = computePath(lhs); + curr.put(lhsHeapPath, new Hashtable()); + + + } + break; + + case FKind.FlatFieldNode: + case FKind.FlatElementNode: { + + FlatFieldNode ffn = (FlatFieldNode) fn; + lhs = ffn.getSrc(); + fld = ffn.getField(); + + // read field + NTuple srcHeapPath = mapHeapPath.get(lhs); + NTuple fldHeapPath = new NTuple(srcHeapPath.getList()); + fldHeapPath.add(fld); + Hashtable gen = curr.get(fldHeapPath); + + if (gen == null) { + gen = new Hashtable(); + curr.put(fldHeapPath, gen); + } + Boolean currentStatus = gen.get(fn); + if (currentStatus == null) { + gen.put(fn, Boolean.FALSE); + } else { + checkFlag(currentStatus.booleanValue(), fn); + } + + + } + break; + + case FKind.FlatSetFieldNode: + case FKind.FlatSetElementNode: { + + FlatSetFieldNode fsfn = (FlatSetFieldNode) fn; + lhs = fsfn.getDst(); + fld = fsfn.getField(); + + // write(field) + NTuple lhsHeapPath = mapHeapPath.get(lhs); + NTuple fldHeapPath = new NTuple(lhsHeapPath.getList()); + fldHeapPath.add(fld); + curr.put(fldHeapPath, new Hashtable()); + + + } + break; + + case FKind.FlatCall: { + + FlatCall fc = (FlatCall) fn; + + // compute all possible callee set + // transform all READ/OVERWRITE set from the any possible callees to the + // caller + MethodDescriptor mdCallee = fc.getMethod(); + FlatMethod fmCallee = state.getMethodFlat(mdCallee); + Set setPossibleCallees = new HashSet(); + TypeDescriptor typeDesc = fc.getThis().getType(); + setPossibleCallees.addAll(callGraph.getMethods(mdCallee, typeDesc)); + + // create mapping from arg idx to its heap paths + Hashtable> mapArgIdx2CallerArgHeapPath = + new Hashtable>(); + + // arg idx is starting from 'this' arg + NTuple thisHeapPath = new NTuple(); + thisHeapPath.add(fc.getThis()); + mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(0), thisHeapPath); + + for (int i = 0; i < fc.numArgs(); i++) { + TempDescriptor arg = fc.getArg(i); + NTuple argHeapPath = computePath(arg); + mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(i + 1), argHeapPath); + } + + Set> calleeUnionBoundReadSet = new HashSet>(); + Set> calleeIntersectBoundOverWriteSet = + new HashSet>(); + + for (Iterator iterator = setPossibleCallees.iterator(); iterator.hasNext();) { + MethodDescriptor callee = (MethodDescriptor) iterator.next(); + FlatMethod calleeFlatMethod = state.getMethodFlat(callee); + + // binding caller's args and callee's params + Set> calleeReadSet = mapFlatMethodToRead.get(calleeFlatMethod); + if (calleeReadSet == null) { + calleeReadSet = new HashSet>(); + mapFlatMethodToRead.put(calleeFlatMethod, calleeReadSet); + } + Set> calleeOverWriteSet = + mapFlatMethodToOverWrite.get(calleeFlatMethod); + if (calleeOverWriteSet == null) { + calleeOverWriteSet = new HashSet>(); + mapFlatMethodToOverWrite.put(calleeFlatMethod, calleeOverWriteSet); + } + + Hashtable mapParamIdx2ParamTempDesc = + new Hashtable(); + for (int i = 0; i < calleeFlatMethod.numParameters(); i++) { + TempDescriptor param = calleeFlatMethod.getParameter(i); + mapParamIdx2ParamTempDesc.put(Integer.valueOf(i), param); + } + + Set> calleeBoundReadSet = + bindSet(calleeReadSet, mapParamIdx2ParamTempDesc, mapArgIdx2CallerArgHeapPath); + // union of the current read set and the current callee's read set + calleeUnionBoundReadSet.addAll(calleeBoundReadSet); + Set> calleeBoundWriteSet = + bindSet(calleeOverWriteSet, mapParamIdx2ParamTempDesc, mapArgIdx2CallerArgHeapPath); + // intersection of the current overwrite set and the current callee's + // overwrite set + merge(calleeIntersectBoundOverWriteSet, calleeBoundWriteSet); + } + + // 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); + } + } + + // 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(); + curr.put(write, new Hashtable()); + } + } + break; + + } + + } + + } + + private void checkFlag(boolean booleanValue, FlatNode fn) { + if (booleanValue) { + throw new Error( + "There is a variable who comes back to the same read statement at the out-most iteration at " + + methodContainingSSJavaLoop.getClassDesc().getSourceFileName() + "::" + + fn.getNumLine()); + } + } + + private void merge(Hashtable, Hashtable> curr, + Hashtable, Hashtable> in) { + + Set> inKeySet = in.keySet(); + for (Iterator iterator = inKeySet.iterator(); iterator.hasNext();) { + NTuple inKey = (NTuple) iterator.next(); + Hashtable inPair = in.get(inKey); + + Set pairKeySet = inPair.keySet(); + for (Iterator iterator2 = pairKeySet.iterator(); iterator2.hasNext();) { + FlatNode pairKey = (FlatNode) iterator2.next(); + Boolean inFlag = inPair.get(pairKey); + + Hashtable currPair = curr.get(inKey); + if (currPair == null) { + currPair = new Hashtable(); + curr.put(inKey, currPair); + } + + Boolean currFlag = currPair.get(pairKey); + // by default, flag is set by false + if (currFlag == null) { + currFlag = Boolean.FALSE; + } + currFlag = Boolean.valueOf(inFlag.booleanValue() | currFlag.booleanValue()); + currPair.put(pairKey, currFlag); + } + + } + + } + + private void methodReadOverWriteAnalysis() { + // perform method READ/OVERWRITE analysis Set methodDescriptorsToAnalyze = new HashSet(); methodDescriptorsToAnalyze.addAll(ssjava.getAnnotationRequireSet()); LinkedList sortedDescriptors = topologicalSort(methodDescriptorsToAnalyze); // no need to analyze method having ssjava loop - sortedDescriptors.removeFirst(); + methodContainingSSJavaLoop = sortedDescriptors.removeFirst(); + + // current descriptors to visit in fixed-point interprocedural analysis, + // prioritized by + // dependency in the call graph + Stack methodDescriptorsToVisitStack = new Stack(); + + Set methodDescriptorToVistSet = new HashSet(); + methodDescriptorToVistSet.addAll(sortedDescriptors); - // analyze scheduled methods until there are no more to visit while (!sortedDescriptors.isEmpty()) { - // start to analyze leaf node - MethodDescriptor md = sortedDescriptors.removeLast(); - analyzeMethod(md); + MethodDescriptor md = sortedDescriptors.removeFirst(); + methodDescriptorsToVisitStack.add(md); } - } + // analyze scheduled methods until there are no more to visit + while (!methodDescriptorsToVisitStack.isEmpty()) { + // start to analyze leaf node + MethodDescriptor md = methodDescriptorsToVisitStack.pop(); + FlatMethod fm = state.getMethodFlat(md); - private void analyzeMethod(MethodDescriptor md) { - if (state.SSJAVADEBUG) { - System.out.println("Definitely written Analyzing: " + md); - } + Set> readSet = new HashSet>(); + Set> overWriteSet = new HashSet>(); - FlatMethod fm = state.getMethodFlat(md); + methodReadOverWrite_analyzeMethod(fm, readSet, overWriteSet); + + Set> prevRead = mapFlatMethodToRead.get(fm); + Set> prevOverWrite = mapFlatMethodToOverWrite.get(fm); + + if (!(readSet.equals(prevRead) && overWriteSet.equals(prevOverWrite))) { + mapFlatMethodToRead.put(fm, readSet); + mapFlatMethodToOverWrite.put(fm, overWriteSet); + + // 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> readSet = mapFlatMethodToRead.get(fm); - if (readSet == null) { - readSet = new HashSet>(); - mapFlatMethodToRead.put(fm, readSet); } - Set> overWriteSet = mapFlatMethodToOverWrite.get(fm); - if (overWriteSet == null) { - overWriteSet = new HashSet>(); - mapFlatMethodToOverWrite.put(fm, overWriteSet); + } + + private void methodReadOverWrite_analyzeMethod(FlatMethod fm, Set> readSet, + Set> overWriteSet) { + if (state.SSJAVADEBUG) { + System.out.println("Definitely written Analyzing: " + fm); } // intraprocedural analysis @@ -114,7 +479,6 @@ public class DefinitelyWrittenCheck { FlatNode fn = flatNodesToVisit.iterator().next(); flatNodesToVisit.remove(fn); - Set> prev = mapFlatNodeToWrittenSet.get(fn); Set> curr = new HashSet>(); for (int i = 0; i < fn.numPrev(); i++) { @@ -125,40 +489,20 @@ public class DefinitelyWrittenCheck { } } - analyzeFlatNode(fn, curr, readSet, overWriteSet); + methodReadOverWrite_nodeActions(fn, curr, readSet, overWriteSet); - // if a new result, schedule forward nodes for analysis - if (!curr.equals(prev)) { - mapFlatNodeToWrittenSet.put(fn, curr); + mapFlatNodeToWrittenSet.put(fn, curr); - for (int i = 0; i < fn.numNext(); i++) { - FlatNode nn = fn.getNext(i); - flatNodesToVisit.add(nn); - } + for (int i = 0; i < fn.numNext(); i++) { + FlatNode nn = fn.getNext(i); + flatNodesToVisit.add(nn); } } - System.out.println("READSET=" + mapFlatMethodToRead.get(fm)); - System.out.println("OVERWRITESET=" + mapFlatMethodToOverWrite.get(fm)); - - } - - private void merge(Set> curr, Set> in) { - - if (curr.isEmpty()) { - // WrittenSet 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); - } else { - // otherwise, current set is the intersection of the two sets - curr.retainAll(in); - } - } - private void analyzeFlatNode(FlatNode fn, Set> writtenSet, + private void methodReadOverWrite_nodeActions(FlatNode fn, Set> writtenSet, Set> readSet, Set> overWriteSet) { TempDescriptor lhs; TempDescriptor rhs; @@ -244,6 +588,92 @@ public class DefinitelyWrittenCheck { } break; + case FKind.FlatCall: { + + FlatCall fc = (FlatCall) fn; + + // compute all possible callee set + // transform all READ/OVERWRITE set from the any possible callees to the + // caller + MethodDescriptor mdCallee = fc.getMethod(); + FlatMethod fmCallee = state.getMethodFlat(mdCallee); + Set setPossibleCallees = new HashSet(); + TypeDescriptor typeDesc = fc.getThis().getType(); + setPossibleCallees.addAll(callGraph.getMethods(mdCallee, typeDesc)); + + // create mapping from arg idx to its heap paths + Hashtable> mapArgIdx2CallerArgHeapPath = + new Hashtable>(); + + // arg idx is starting from 'this' arg + NTuple thisHeapPath = new NTuple(); + thisHeapPath.add(fc.getThis()); + mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(0), thisHeapPath); + + for (int i = 0; i < fc.numArgs(); i++) { + TempDescriptor arg = fc.getArg(i); + NTuple argHeapPath = mapHeapPath.get(arg); + mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(i + 1), argHeapPath); + } + + Set> calleeUnionBoundReadSet = new HashSet>(); + Set> calleeIntersectBoundOverWriteSet = new HashSet>(); + + for (Iterator iterator = setPossibleCallees.iterator(); iterator.hasNext();) { + MethodDescriptor callee = (MethodDescriptor) iterator.next(); + FlatMethod calleeFlatMethod = state.getMethodFlat(callee); + + // binding caller's args and callee's params + Set> calleeReadSet = mapFlatMethodToRead.get(calleeFlatMethod); + if (calleeReadSet == null) { + calleeReadSet = new HashSet>(); + mapFlatMethodToRead.put(calleeFlatMethod, calleeReadSet); + } + Set> calleeOverWriteSet = mapFlatMethodToOverWrite.get(calleeFlatMethod); + if (calleeOverWriteSet == null) { + calleeOverWriteSet = new HashSet>(); + mapFlatMethodToOverWrite.put(calleeFlatMethod, calleeOverWriteSet); + } + + Hashtable mapParamIdx2ParamTempDesc = + new Hashtable(); + for (int i = 0; i < calleeFlatMethod.numParameters(); i++) { + TempDescriptor param = calleeFlatMethod.getParameter(i); + mapParamIdx2ParamTempDesc.put(Integer.valueOf(i), param); + } + + Set> calleeBoundReadSet = + bindSet(calleeReadSet, mapParamIdx2ParamTempDesc, mapArgIdx2CallerArgHeapPath); + // union of the current read set and the current callee's read set + calleeUnionBoundReadSet.addAll(calleeBoundReadSet); + + Set> calleeBoundWriteSet = + bindSet(calleeOverWriteSet, mapParamIdx2ParamTempDesc, mapArgIdx2CallerArgHeapPath); + // intersection of the current overwrite set and the current callee's + // overwrite set + merge(calleeIntersectBoundOverWriteSet, calleeBoundWriteSet); + } + + // 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)) { + readSet.add(read); + } + } + writtenSet.removeAll(calleeUnionBoundReadSet); + + // add heap path, which is an element of OVERWRITE_bound set, to the + // caller's WT set + for (Iterator iterator = calleeIntersectBoundOverWriteSet.iterator(); iterator.hasNext();) { + NTuple write = (NTuple) iterator.next(); + writtenSet.add(write); + } + + } + break; + case FKind.FlatExit: { // merge the current written set with OVERWRITE set merge(overWriteSet, writtenSet); @@ -251,10 +681,70 @@ public class DefinitelyWrittenCheck { break; } + + } + + private void merge(Set> curr, Set> in) { + + if (curr.isEmpty()) { + // WrittenSet 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); + } else { + // otherwise, current set is the intersection of the two sets + curr.retainAll(in); + } + + } + + // combine two heap path + private NTuple combine(NTuple callerIn, NTuple calleeIn) { + NTuple combined = new NTuple(); + + for (int i = 0; i < callerIn.size(); i++) { + combined.add(callerIn.get(i)); + } + + // the first element of callee's heap path represents parameter + // so we skip the first one since it is already added from caller's heap + // path + for (int i = 1; i < calleeIn.size(); i++) { + combined.add(calleeIn.get(i)); + } + + return combined; + } + + private Set> bindSet(Set> calleeSet, + Hashtable mapParamIdx2ParamTempDesc, + Hashtable> mapCallerArgIdx2HeapPath) { + + Set> boundedCalleeSet = new HashSet>(); + + Set keySet = mapCallerArgIdx2HeapPath.keySet(); + for (Iterator iterator = keySet.iterator(); iterator.hasNext();) { + Integer idx = (Integer) iterator.next(); + + NTuple callerArgHeapPath = mapCallerArgIdx2HeapPath.get(idx); + TempDescriptor calleeParam = mapParamIdx2ParamTempDesc.get(idx); + + for (Iterator iterator2 = calleeSet.iterator(); iterator2.hasNext();) { + NTuple element = (NTuple) iterator2.next(); + if (element.startsWith(calleeParam)) { + NTuple boundElement = combine(callerArgHeapPath, element); + boundedCalleeSet.add(boundElement); + } + + } + + } + return boundedCalleeSet; + } // Borrowed it from disjoint analysis - protected LinkedList topologicalSort(Set toSort) { + private LinkedList topologicalSort(Set toSort) { Set discovered = new HashSet(); @@ -279,7 +769,7 @@ public class DefinitelyWrittenCheck { // a dependent of a method decriptor d for this analysis is: // 1) a method or task that invokes d // 2) in the descriptorsToAnalyze set - protected void dfsVisit(MethodDescriptor md, Set toSort, + private void dfsVisit(MethodDescriptor md, Set toSort, LinkedList sorted, Set discovered) { discovered.add(md); @@ -310,7 +800,7 @@ public class DefinitelyWrittenCheck { // a dependent of a method decriptor d for this analysis is: // 1) a method or task that invokes d // 2) in the descriptorsToAnalyze set - protected void addDependent(MethodDescriptor callee, MethodDescriptor caller) { + private void addDependent(MethodDescriptor callee, MethodDescriptor caller) { Set deps = mapDescriptorToSetDependents.get(callee); if (deps == null) { deps = new HashSet(); @@ -319,187 +809,25 @@ public class DefinitelyWrittenCheck { mapDescriptorToSetDependents.put(callee, deps); } - private void definitelyWrittenForward(FlatNode entrance) { - - Set flatNodesToVisit = new HashSet(); - flatNodesToVisit.add(entrance); - - while (!flatNodesToVisit.isEmpty()) { - FlatNode fn = (FlatNode) flatNodesToVisit.iterator().next(); - flatNodesToVisit.remove(fn); - - Hashtable> prev = definitelyWrittenResults.get(fn); - - Hashtable> curr = - new Hashtable>(); - for (int i = 0; i < fn.numPrev(); i++) { - FlatNode nn = fn.getPrev(i); - Hashtable> dwIn = definitelyWrittenResults.get(nn); - if (dwIn != null) { - mergeResults(curr, dwIn); - } - } - - definitelyWritten_nodeActions(fn, curr, entrance); - - // if a new result, schedule forward nodes for analysis - if (!curr.equals(prev)) { - definitelyWrittenResults.put(fn, curr); - - for (int i = 0; i < fn.numNext(); i++) { - FlatNode nn = fn.getNext(i); - flatNodesToVisit.add(nn); - } - } - } - } - - private void mergeResults(Hashtable> curr, - Hashtable> in) { - - Set inKeySet = in.keySet(); - for (Iterator iterator = inKeySet.iterator(); iterator.hasNext();) { - Descriptor inKey = (Descriptor) iterator.next(); - Hashtable inPair = in.get(inKey); - - Set pairKeySet = inPair.keySet(); - for (Iterator iterator2 = pairKeySet.iterator(); iterator2.hasNext();) { - FlatNode pairKey = (FlatNode) iterator2.next(); - Boolean inFlag = inPair.get(pairKey); - - Hashtable currPair = curr.get(inKey); - if (currPair == null) { - currPair = new Hashtable(); - curr.put(inKey, currPair); - } - - Boolean currFlag = currPair.get(pairKey); - // by default, flag is set by false - if (currFlag == null) { - currFlag = Boolean.FALSE; - } - currFlag = Boolean.valueOf(inFlag.booleanValue() | currFlag.booleanValue()); - currPair.put(pairKey, currFlag); - } - + private Set getDependents(MethodDescriptor callee) { + Set deps = mapDescriptorToSetDependents.get(callee); + if (deps == null) { + deps = new HashSet(); + mapDescriptorToSetDependents.put(callee, deps); } - + return deps; } - private void definitelyWritten_nodeActions(FlatNode fn, - Hashtable> curr, FlatNode entrance) { - - if (fn == entrance) { - - Set keySet = curr.keySet(); - for (Iterator iterator = keySet.iterator(); iterator.hasNext();) { - Descriptor key = (Descriptor) 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); - } - } - } - + private NTuple computePath(TempDescriptor td) { + // generate proper path fot input td + // if td is local variable, it just generate one element tuple path + if (mapHeapPath.containsKey(td)) { + return mapHeapPath.get(td); } else { - TempDescriptor lhs; - TempDescriptor rhs; - FieldDescriptor fld; - - switch (fn.kind()) { - - case FKind.FlatOpNode: { - - FlatOpNode fon = (FlatOpNode) fn; - lhs = fon.getDest(); - rhs = fon.getLeft(); - System.out.println("\nfon=" + fon); - - if (fon.getOp().getOp() == Operation.ASSIGN) { - - // read(rhs) - Hashtable gen = curr.get(rhs); - if (gen == null) { - gen = new Hashtable(); - curr.put(rhs, gen); - } - System.out.println("READ LOC=" + rhs.getType().getExtension()); - - Boolean currentStatus = gen.get(fn); - if (currentStatus == null) { - gen.put(fn, Boolean.FALSE); - } - } - // write(lhs) - curr.put(lhs, new Hashtable()); - System.out.println("WRITING LOC=" + lhs.getType().getExtension()); - - } - break; - - case FKind.FlatLiteralNode: { - FlatLiteralNode fln = (FlatLiteralNode) fn; - lhs = fln.getDst(); - - // write(lhs) - curr.put(lhs, new Hashtable()); - - System.out.println("WRITING LOC=" + lhs.getType().getExtension()); - - } - break; - - case FKind.FlatFieldNode: - case FKind.FlatElementNode: { - - FlatFieldNode ffn = (FlatFieldNode) fn; - lhs = ffn.getSrc(); - fld = ffn.getField(); - - // read field - Hashtable gen = curr.get(fld); - if (gen == null) { - gen = new Hashtable(); - curr.put(fld, gen); - } - Boolean currentStatus = gen.get(fn); - if (currentStatus == null) { - gen.put(fn, Boolean.FALSE); - } - - System.out.println("\nffn=" + ffn); - System.out.println("READ LOCfld=" + fld.getType().getExtension()); - System.out.println("READ LOClhs=" + lhs.getType().getExtension()); - - } - break; - - case FKind.FlatSetFieldNode: - case FKind.FlatSetElementNode: { - - FlatSetFieldNode fsfn = (FlatSetFieldNode) fn; - fld = fsfn.getField(); - - // write(field) - curr.put(fld, new Hashtable()); - - System.out.println("\nfsfn=" + fsfn); - System.out.println("WRITELOC LOC=" + fld.getType().getExtension()); - - } - break; - - case FKind.FlatCall: { - - } - break; - - } + NTuple path = new NTuple(); + path.add(td); + return path; } - } -} +} \ No newline at end of file diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java index 71537e2a..970b1929 100644 --- a/Robust/src/Analysis/SSJava/FlowDownCheck.java +++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java @@ -343,17 +343,18 @@ public class FlowDownCheck { ExpressionNode returnExp = rn.getReturnExpression(); - CompositeLocation expLoc = - checkLocationFromExpressionNode(md, nametable, returnExp, new CompositeLocation()); - - // check if return value is equal or higher than RETRUNLOC of method - // declaration annotation - CompositeLocation returnLocAt = md2ReturnLoc.get(md); - - if (CompositeLattice.isGreaterThan(returnLocAt, expLoc)) { - throw new Error( - "Return value location is not equal or higher than the declaraed return location at " - + md.getClassDesc().getSourceFileName() + "::" + rn.getNumLine()); + CompositeLocation expLoc; + if (returnExp != null) { + expLoc = checkLocationFromExpressionNode(md, nametable, returnExp, new CompositeLocation()); + // check if return value is equal or higher than RETRUNLOC of method + // declaration annotation + CompositeLocation returnLocAt = md2ReturnLoc.get(md); + + if (CompositeLattice.isGreaterThan(returnLocAt, expLoc)) { + throw new Error( + "Return value location is not equal or higher than the declaraed return location at " + + md.getClassDesc().getSourceFileName() + "::" + rn.getNumLine()); + } } return new CompositeLocation(); diff --git a/Robust/src/Analysis/SSJava/NTuple.java b/Robust/src/Analysis/SSJava/NTuple.java index 30dfd39b..d69708de 100644 --- a/Robust/src/Analysis/SSJava/NTuple.java +++ b/Robust/src/Analysis/SSJava/NTuple.java @@ -66,4 +66,23 @@ public class NTuple { return elements; } + public boolean startsWith(T prefix) { + return get(0).equals(prefix); + } + + public boolean startsWith(NTuple prefix) { + + if (prefix.size() > size()) { + return false; + } + + for (int i = 0; i < prefix.size(); i++) { + if (prefix.get(i).equals(get(i))) { + return false; + } + } + return true; + + } + }