From d06ba34e8da58a239f94e98a0bf38009f8eb7dda Mon Sep 17 00:00:00 2001 From: yeom Date: Thu, 7 Jul 2011 23:09:30 +0000 Subject: [PATCH] bring recent changes before starting to implement definitely written analysis for shared locations --- .../SSJava/DefinitelyWrittenCheck.java | 71 +++++++++++-------- Robust/src/Analysis/SSJava/FlowDownCheck.java | 46 +++++++----- 2 files changed, 72 insertions(+), 45 deletions(-) diff --git a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java index 2a0d0c93..65027b5b 100644 --- a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java +++ b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java @@ -159,6 +159,7 @@ public class DefinitelyWrittenCheck { 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(); @@ -250,7 +251,6 @@ public class DefinitelyWrittenCheck { break; case FKind.FlatCall: { - FlatCall fc = (FlatCall) fn; bindHeapPathCallerArgWithCaleeParam(fc); @@ -269,7 +269,7 @@ public class DefinitelyWrittenCheck { if (currentStatus == null) { gen.put(fn, Boolean.FALSE); } else { - checkFlag(currentStatus.booleanValue(), fn); + checkFlag(currentStatus.booleanValue(), fn, read); } } @@ -299,7 +299,7 @@ public class DefinitelyWrittenCheck { if (currentStatus == null) { gen.put(fn, Boolean.FALSE); } else { - checkFlag(currentStatus.booleanValue(), fn); + checkFlag(currentStatus.booleanValue(), fn, hp); } } @@ -341,8 +341,13 @@ public class DefinitelyWrittenCheck { new Hashtable>(); // arg idx is starting from 'this' arg - NTuple thisHeapPath = new NTuple(); - thisHeapPath.add(fc.getThis()); + NTuple thisHeapPath = mapHeapPath.get(fc.getThis()); + if (thisHeapPath == null) { + // method is called without creating new flat node representing 'this' + thisHeapPath = new NTuple(); + thisHeapPath.add(fc.getThis()); + } + mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(0), thisHeapPath); for (int i = 0; i < fc.numArgs(); i++) { @@ -390,12 +395,13 @@ public class DefinitelyWrittenCheck { } - private void checkFlag(boolean booleanValue, FlatNode fn) { + private void checkFlag(boolean booleanValue, FlatNode fn, NTuple hp) { if (booleanValue) { throw new Error( - "There is a variable who comes back to the same read statement without being overwritten at the out-most iteration at " - + methodContainingSSJavaLoop.getClassDesc().getSourceFileName() - + "::" + "There is a variable, which is reachable through references " + + hp + + ", who comes back to the same read statement without being overwritten at the out-most iteration at " + + methodContainingSSJavaLoop.getClassDesc().getSourceFileName() + "::" + fn.getNumLine()); } } @@ -582,20 +588,25 @@ public class DefinitelyWrittenCheck { // set up heap path NTuple srcHeapPath = mapHeapPath.get(rhs); - NTuple readingHeapPath = new NTuple(srcHeapPath.getList()); - readingHeapPath.add(fld); - mapHeapPath.put(lhs, readingHeapPath); - - // read (x.f) - if (fld.getType().isImmutable()) { - // if WT doesnot have hp(x.f), add hp(x.f) to READ - if (!writtenSet.contains(readingHeapPath)) { - readSet.add(readingHeapPath); + if (srcHeapPath != null) { + // if lhs srcHeapPath is null, it means that it is not reachable from + // callee's parameters. so just ignore it + + NTuple readingHeapPath = new NTuple(srcHeapPath.getList()); + readingHeapPath.add(fld); + mapHeapPath.put(lhs, readingHeapPath); + + // read (x.f) + if (fld.getType().isImmutable()) { + // if WT doesnot have hp(x.f), add hp(x.f) to READ + if (!writtenSet.contains(readingHeapPath)) { + readSet.add(readingHeapPath); + } } - } - // need to kill hp(x.f) from WT - writtenSet.remove(readingHeapPath); + // need to kill hp(x.f) from WT + writtenSet.remove(readingHeapPath); + } } break; @@ -611,13 +622,17 @@ public class DefinitelyWrittenCheck { // set up heap path NTuple lhsHeapPath = mapHeapPath.get(lhs); - NTuple newHeapPath = new NTuple(lhsHeapPath.getList()); - newHeapPath.add(fld); - mapHeapPath.put(fld, newHeapPath); - - // write(x.f) - // need to add hp(y) to WT - writtenSet.add(newHeapPath); + if (lhsHeapPath != null) { + // if lhs heap path is null, it means that it is not reachable from + // callee's parameters. so just ignore it + NTuple newHeapPath = new NTuple(lhsHeapPath.getList()); + newHeapPath.add(fld); + mapHeapPath.put(fld, newHeapPath); + + // write(x.f) + // need to add hp(y) to WT + writtenSet.add(newHeapPath); + } } break; diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java index b14fecfc..7978daa1 100644 --- a/Robust/src/Analysis/SSJava/FlowDownCheck.java +++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java @@ -376,7 +376,7 @@ public class FlowDownCheck { CompositeLocation condLoc = checkLocationFromExpressionNode(md, nametable, ln.getCondition(), new CompositeLocation()); - addTypeLocation(ln.getCondition().getType(), (condLoc)); + addLocationType(ln.getCondition().getType(), (condLoc)); CompositeLocation bodyLoc = checkLocationFromBlockNode(md, nametable, ln.getBody()); @@ -398,26 +398,40 @@ public class FlowDownCheck { CompositeLocation condLoc = checkLocationFromExpressionNode(md, bn.getVarTable(), ln.getCondition(), new CompositeLocation()); - addTypeLocation(ln.getCondition().getType(), condLoc); + addLocationType(ln.getCondition().getType(), condLoc); CompositeLocation updateLoc = checkLocationFromBlockNode(md, bn.getVarTable(), ln.getUpdate()); Set glbInputSet = new HashSet(); glbInputSet.add(condLoc); - glbInputSet.add(updateLoc); +// glbInputSet.add(updateLoc); CompositeLocation glbLocOfForLoopCond = CompositeLattice.calculateGLB(glbInputSet); // check location of 'forloop' body CompositeLocation blockLoc = checkLocationFromBlockNode(md, bn.getVarTable(), ln.getBody()); + // compute glb of body including loop body and update statement + glbInputSet.clear(); + if (blockLoc == null) { // when there is no statement in the loop body - return glbLocOfForLoopCond; + + if(updateLoc==null){ + // also there is no update statement in the loop body + return glbLocOfForLoopCond; + } + glbInputSet.add(updateLoc); + + }else{ + glbInputSet.add(blockLoc); + glbInputSet.add(updateLoc); } + + CompositeLocation loopBodyLoc = CompositeLattice.calculateGLB(glbInputSet); - if (!CompositeLattice.isGreaterThan(glbLocOfForLoopCond, blockLoc)) { + if (!CompositeLattice.isGreaterThan(glbLocOfForLoopCond, loopBodyLoc)) { throw new Error( "The location of the for-condition statement is lower than the for-loop body at " + cd.getSourceFileName() + ":" + ln.getCondition().getNumLine()); @@ -442,7 +456,7 @@ public class FlowDownCheck { CompositeLocation condLoc = checkLocationFromExpressionNode(md, nametable, isn.getCondition(), new CompositeLocation()); - addTypeLocation(isn.getCondition().getType(), condLoc); + addLocationType(isn.getCondition().getType(), condLoc); glbInputSet.add(condLoc); CompositeLocation locTrueBlock = checkLocationFromBlockNode(md, nametable, isn.getTrueBlock()); @@ -611,13 +625,13 @@ public class FlowDownCheck { CompositeLocation condLoc = checkLocationFromExpressionNode(md, nametable, tn.getCond(), new CompositeLocation()); - addTypeLocation(tn.getCond().getType(), condLoc); + addLocationType(tn.getCond().getType(), condLoc); CompositeLocation trueLoc = checkLocationFromExpressionNode(md, nametable, tn.getTrueExpr(), new CompositeLocation()); - addTypeLocation(tn.getTrueExpr().getType(), trueLoc); + addLocationType(tn.getTrueExpr().getType(), trueLoc); CompositeLocation falseLoc = checkLocationFromExpressionNode(md, nametable, tn.getFalseExpr(), new CompositeLocation()); - addTypeLocation(tn.getFalseExpr().getType(), falseLoc); + addLocationType(tn.getFalseExpr().getType(), falseLoc); // check if condLoc is higher than trueLoc & falseLoc if (!CompositeLattice.isGreaterThan(condLoc, trueLoc)) { @@ -769,7 +783,7 @@ public class FlowDownCheck { CompositeLocation argLoc = checkLocationFromExpressionNode(md, nametable, en, new CompositeLocation()); glbInputSet.add(argLoc); - addTypeLocation(en.getType(), argLoc); + addLocationType(en.getType(), argLoc); } // check array initializers @@ -934,7 +948,6 @@ public class FlowDownCheck { ExpressionNode left = fan.getExpression(); loc = checkLocationFromExpressionNode(md, nametable, left, loc); - // addTypeLocation(left.getType(), loc); if (!left.getType().isPrimitive()) { FieldDescriptor fd = fan.getField(); @@ -1020,11 +1033,11 @@ public class FlowDownCheck { if (locDec.startsWith(SSJavaAnalysis.DELTA)) { DeltaLocation deltaLoc = parseDeltaDeclaration(md, n, locDec); d2loc.put(vd, deltaLoc); - addTypeLocation(vd.getType(), deltaLoc); + addLocationType(vd.getType(), deltaLoc); } else { CompositeLocation compLoc = parseLocationDeclaration(md, n, locDec); d2loc.put(vd, compLoc); - addTypeLocation(vd.getType(), compLoc); + addLocationType(vd.getType(), compLoc); } } @@ -1170,21 +1183,20 @@ public class FlowDownCheck { + cd.getSourceFileName() + "."); } Location loc = new Location(cd, locationID); - // d2loc.put(fd, loc); - addTypeLocation(fd.getType(), loc); + addLocationType(fd.getType(), loc); } } } - private void addTypeLocation(TypeDescriptor type, CompositeLocation loc) { + private void addLocationType(TypeDescriptor type, CompositeLocation loc) { if (type != null) { type.setExtension(loc); } } - private void addTypeLocation(TypeDescriptor type, Location loc) { + private void addLocationType(TypeDescriptor type, Location loc) { if (type != null) { type.setExtension(loc); } -- 2.34.1