From: yeom Date: Fri, 8 Jul 2011 18:51:11 +0000 (+0000) Subject: changes toward intraprocedural analysis X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=484e9bd327c7fe5d5cf96bbead147c80aaef6380;p=IRC.git changes toward intraprocedural analysis --- diff --git a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java index 39c5ee26..7cc86f16 100644 --- a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java +++ b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java @@ -63,14 +63,14 @@ public class DefinitelyWrittenCheck { // 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; + private Hashtable, Set>> mapMethodDescriptorToCompleteClearingSummary; // maps a method descriptor to the merged incoming caller's current // overwritten status - private Hashtable>> mapMethodDescriptorToInitialClearingSummary; + private Hashtable, Set>> mapMethodDescriptorToInitialClearingSummary; // maps a flat node to current partial results - private Hashtable>> mapFlatNodeToClearingSummary; + private Hashtable, Set>> mapFlatNodeToClearingSummary; private FlatNode ssjavaLoopEntrance; private LoopFinder ssjavaLoop; @@ -79,6 +79,8 @@ public class DefinitelyWrittenCheck { private Set> calleeUnionBoundReadSet; private Set> calleeIntersectBoundOverWriteSet; + private TempDescriptor LOCAL; + public DefinitelyWrittenCheck(SSJavaAnalysis ssjava, State state) { this.state = state; this.ssjava = ssjava; @@ -92,19 +94,21 @@ public class DefinitelyWrittenCheck { new Hashtable, Hashtable>>(); this.calleeUnionBoundReadSet = new HashSet>(); this.calleeIntersectBoundOverWriteSet = new HashSet>(); + this.mapMethodDescriptorToCompleteClearingSummary = - new Hashtable>>(); + new Hashtable, Set>>(); this.mapMethodDescriptorToInitialClearingSummary = - new Hashtable>>(); + new Hashtable, Set>>(); this.mapFlatNodeToClearingSummary = - new Hashtable>>(); + new Hashtable, Set>>(); + this.LOCAL = new TempDescriptor("LOCAL"); } public void definitelyWrittenCheck() { if (!ssjava.getAnnotationRequireSet().isEmpty()) { methodReadOverWriteAnalysis(); writtenAnalyis(); -// sharedLocationAnalysis(); + sharedLocationAnalysis(); } } @@ -131,7 +135,7 @@ public class DefinitelyWrittenCheck { MethodDescriptor md = methodDescriptorsToVisitStack.pop(); FlatMethod fm = state.getMethodFlat(md); - sharedLocation_analyzeMethod(fm, (fm.equals(methodContainingSSJavaLoop))); + sharedLocation_analyzeMethod(fm, (md.equals(methodContainingSSJavaLoop))); if (true) { @@ -159,7 +163,8 @@ public class DefinitelyWrittenCheck { private void sharedLocation_analyzeMethod(FlatMethod fm, boolean onlyVisitSSJavaLoop) { if (state.SSJAVADEBUG) { - System.out.println("Definitely written for shared locations Analyzing: " + fm); + System.out.println("Definitely written for shared locations Analyzing: " + fm + " " + + onlyVisitSSJavaLoop); } // intraprocedural analysis @@ -176,19 +181,22 @@ public class DefinitelyWrittenCheck { FlatNode fn = flatNodesToVisit.iterator().next(); flatNodesToVisit.remove(fn); - Hashtable> curr = new Hashtable>(); + Hashtable, Set> curr = + new Hashtable, Set>(); for (int i = 0; i < fn.numPrev(); i++) { FlatNode prevFn = fn.getPrev(i); - Hashtable> in = mapFlatNodeToClearingSummary.get(prevFn); + Hashtable, Set> in = + mapFlatNodeToClearingSummary.get(prevFn); if (in != null) { mergeSharedAnaylsis(curr, in); } } - sharedLocation_nodeActions(fn, curr); + sharedLocation_nodeActions(fn, curr, onlyVisitSSJavaLoop); - Hashtable> clearingPrev = mapFlatNodeToClearingSummary.get(fn); + Hashtable, Set> clearingPrev = + mapFlatNodeToClearingSummary.get(fn); if (!curr.equals(clearingPrev)) { mapFlatNodeToClearingSummary.put(fn, curr); @@ -207,14 +215,34 @@ public class DefinitelyWrittenCheck { } - private void sharedLocation_nodeActions(FlatNode fn, Hashtable> curr) { + private void sharedLocation_nodeActions(FlatNode fn, + Hashtable, Set> curr, boolean isSSJavaLoop) { TempDescriptor lhs; TempDescriptor rhs; FieldDescriptor fld; - - System.out.println("fn="+fn); switch (fn.kind()) { + + case FKind.FlatOpNode: { + FlatOpNode fon = (FlatOpNode) fn; + lhs = fon.getDest(); + rhs = fon.getLeft(); + + if (fon.getOp().getOp() == Operation.ASSIGN) { + if (rhs.getType().isImmutable() && isSSJavaLoop) { + // in ssjavaloop, we need to take care about reading local variables! + NTuple rhsHeapPath = new NTuple(); + NTuple lhsHeapPath = new NTuple(); + rhsHeapPath.add(LOCAL); + lhsHeapPath.add(LOCAL); + readLocation(curr, rhsHeapPath, rhs); + writeLocation(curr, lhsHeapPath, lhs); + } + } + + } + break; + case FKind.FlatFieldNode: case FKind.FlatElementNode: { @@ -229,7 +257,7 @@ public class DefinitelyWrittenCheck { fldHeapPath.add(fld); if (fld.getType().isImmutable()) { - readLocation(fn, fldHeapPath, curr); + // readLocation(f curr); } // propagate rhs's heap path to the lhs @@ -248,7 +276,7 @@ public class DefinitelyWrittenCheck { // write(field) NTuple lhsHeapPath = computePath(lhs); NTuple fldHeapPath = new NTuple(lhsHeapPath.getList()); - writeLocation(curr, fldHeapPath, fld); + // writeLocation(curr, fldHeapPath, fld, getLocation(fld)); } break; @@ -261,28 +289,63 @@ public class DefinitelyWrittenCheck { } - private void writeLocation(Hashtable> curr, - NTuple fldHeapPath, FieldDescriptor fld) { + private Location getLocation(Descriptor d) { + + if (d instanceof FieldDescriptor) { + return (Location) ((FieldDescriptor) d).getType().getExtension(); + } else { + assert d instanceof TempDescriptor; + CompositeLocation comp = (CompositeLocation) ((TempDescriptor) d).getType().getExtension(); + return comp.get(comp.getSize() - 1); + } + + } + + private SharedLocState getSharedLocState(Hashtable, Set> curr, + NTuple hp, Location loc) { - Location fieldLoc = (Location) fld.getType().getExtension(); - if (ssjava.isSharedLocation(fieldLoc)) { + Set set = curr.get(hp); + if (set == null) { + set = new HashSet(); + curr.put(hp, set); + } - 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)); + SharedLocState state = null; + for (Iterator iterator = set.iterator(); iterator.hasNext();) { + SharedLocState e = (SharedLocState) iterator.next(); + if (e.getLoc().equals(loc)) { + state = e; + break; } - ((Set) v.get(1)).add(fld); } + + if (state == null) { + state = new SharedLocState(loc); + set.add(state); + } + + return state; } - private void readLocation(FlatNode fn, NTuple fldHeapPath, - Hashtable> curr) { - // TODO Auto-generated method stub + private void writeLocation(Hashtable, Set> curr, + NTuple hp, Descriptor d) { + Location loc = getLocation(d); + if (ssjava.isSharedLocation(loc)) { + SharedLocState state = getSharedLocState(curr, hp, loc); + state.addVar(d); + } + } + + private void readLocation(Hashtable, Set> curr, + NTuple hp, Descriptor d) { + // remove reading var x from written set + + Location loc = getLocation(d); + if (ssjava.isSharedLocation(loc)) { + SharedLocState state = getSharedLocState(curr, hp, loc); + state.removeVar(d); + } } private void writtenAnalyis() { @@ -890,8 +953,8 @@ public class DefinitelyWrittenCheck { } - private void mergeSharedAnaylsis(Hashtable> curr, - Hashtable> in) { + private void mergeSharedAnaylsis(Hashtable, Set> curr, + Hashtable, Set> in) { } diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java index 7978daa1..108ad0dc 100644 --- a/Robust/src/Analysis/SSJava/FlowDownCheck.java +++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java @@ -405,7 +405,7 @@ public class FlowDownCheck { Set glbInputSet = new HashSet(); glbInputSet.add(condLoc); -// glbInputSet.add(updateLoc); + // glbInputSet.add(updateLoc); CompositeLocation glbLocOfForLoopCond = CompositeLattice.calculateGLB(glbInputSet); @@ -414,21 +414,21 @@ public class FlowDownCheck { // compute glb of body including loop body and update statement glbInputSet.clear(); - + if (blockLoc == null) { // when there is no statement in the loop body - - if(updateLoc==null){ + + if (updateLoc == null) { // also there is no update statement in the loop body return glbLocOfForLoopCond; } glbInputSet.add(updateLoc); - - }else{ + + } else { glbInputSet.add(blockLoc); glbInputSet.add(updateLoc); } - + CompositeLocation loopBodyLoc = CompositeLattice.calculateGLB(glbInputSet); if (!CompositeLattice.isGreaterThan(glbLocOfForLoopCond, loopBodyLoc)) { @@ -1036,6 +1036,12 @@ public class FlowDownCheck { addLocationType(vd.getType(), deltaLoc); } else { CompositeLocation compLoc = parseLocationDeclaration(md, n, locDec); + + Location lastElement = compLoc.get(compLoc.getSize() - 1); + if (ssjava.isSharedLocation(lastElement)) { + ssjava.mapSharedLocation2Descriptor(lastElement, vd); + } + d2loc.put(vd, compLoc); addLocationType(vd.getType(), compLoc); } @@ -1183,6 +1189,11 @@ public class FlowDownCheck { + cd.getSourceFileName() + "."); } Location loc = new Location(cd, locationID); + + if (ssjava.isSharedLocation(loc)) { + ssjava.mapSharedLocation2Descriptor(loc, fd); + } + addLocationType(fd.getType(), loc); } diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java index 80a81e9c..1402a41f 100644 --- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java +++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java @@ -16,7 +16,9 @@ import IR.Descriptor; import IR.MethodDescriptor; import IR.State; import IR.TypeUtil; +import IR.Flat.BuildFlat; import IR.Flat.FlatMethod; +import IR.Flat.TempDescriptor; public class SSJavaAnalysis { @@ -50,6 +52,9 @@ public class SSJavaAnalysis { // method set that does not have loop termination analysis Hashtable skipLoopTerminate; + // map shared location to its descriptors + Hashtable> mapSharedLocation2DescriptorSet; + CallGraph callgraph; public SSJavaAnalysis(State state, TypeUtil tu, CallGraph callgraph) { @@ -61,6 +66,7 @@ public class SSJavaAnalysis { this.md2lattice = new Hashtable>(); this.annotationRequireSet = new HashSet(); this.skipLoopTerminate = new Hashtable(); + this.mapSharedLocation2DescriptorSet = new Hashtable>(); } public void doCheck() { @@ -310,9 +316,17 @@ public class SSJavaAnalysis { } public boolean isSharedLocation(Location loc) { - SSJavaLattice lattice = getLattice(loc.getDescriptor()); return lattice.getSpinLocSet().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); } + } diff --git a/Robust/src/Analysis/SSJava/SharedLocState.java b/Robust/src/Analysis/SSJava/SharedLocState.java new file mode 100644 index 00000000..d55bd573 --- /dev/null +++ b/Robust/src/Analysis/SSJava/SharedLocState.java @@ -0,0 +1,56 @@ +package Analysis.SSJava; + +import java.util.HashSet; +import java.util.Set; + +import IR.Descriptor; + +public class SharedLocState { + + Location loc; + Set varSet; + boolean flag; + + public SharedLocState(Location loc) { + this.loc = loc; + this.varSet = new HashSet(); + this.flag = false; + } + + public void addVar(Descriptor d) { + varSet.add(d); + } + + public void removeVar(Descriptor d) { + varSet.remove(d); + } + + public Location getLoc() { + return loc; + } + + public String toString() { + return "<" + loc + "," + varSet + "," + flag + ">"; + } + + public void setLoc(Location loc) { + this.loc = loc; + } + + public Set getVarSet() { + return varSet; + } + + public void setVarSet(Set varSet) { + this.varSet = varSet; + } + + public boolean isFlag() { + return flag; + } + + public void setFlag(boolean flag) { + this.flag = flag; + } + +}