From 3cc80ebdf6feb3d663d446ff4e330a9a178463fd Mon Sep 17 00:00:00 2001 From: yeom Date: Wed, 18 May 2011 23:34:37 +0000 Subject: [PATCH] more changes. --- .../Analysis/SSJava/CompositeLocation.java | 130 +----------------- Robust/src/Analysis/SSJava/FlowDownCheck.java | 33 ++--- .../src/Analysis/SSJava/SSJavaAnalysis.java | 4 +- Robust/src/Tests/ssJava/flowdown/test.java | 64 ++++++++- 4 files changed, 79 insertions(+), 152 deletions(-) diff --git a/Robust/src/Analysis/SSJava/CompositeLocation.java b/Robust/src/Analysis/SSJava/CompositeLocation.java index 0dd524db..8f396a57 100644 --- a/Robust/src/Analysis/SSJava/CompositeLocation.java +++ b/Robust/src/Analysis/SSJava/CompositeLocation.java @@ -30,139 +30,13 @@ public class CompositeLocation implements TypeExtension { public Location get(int idx) { return locTuple.get(idx); } - - public boolean isEmpty(){ - return locTuple.size()==0; - } - - // public void addLocationSet(Set set) { - // - // for (Iterator iterator = set.iterator(); iterator.hasNext();) { - // Location location = (Location) iterator.next(); - // locTuple.addElement(location); - // } - // - // } - - // public Location getLocation(ClassDescriptor cd) { - // - // // need to get more optimization version later - // Set locSet = getBaseLocationSet(); - // for (Iterator iterator = locSet.iterator(); iterator.hasNext();) { - // Location location = (Location) iterator.next(); - // if (location.getClassDescriptor().equals(cd)) { - // return location; - // } - // } - // - // return null; - // - // } - - // public Map getCd2Loc() { - // - // Map cd2loc = new Hashtable(); - // - // Set baseLocSet = getBaseLocationSet(); - // for (Iterator iterator = baseLocSet.iterator(); iterator.hasNext();) { - // Location location = (Location) iterator.next(); - // cd2loc.put(location.getClassDescriptor(), location); - // } - // - // return cd2loc; - // - // } - - public NTuple getBaseLocationTuple() { - - return locTuple; - - // NTuple baseLocationTuple = new NTuple(); - // int tupleSize = locTuple.size(); - // for (int i = 0; i < tupleSize; i++) { - // Location locElement = locTuple.at(i); - // - // if (locElement instanceof DeltaLocation) { - // // baseLocationSet.addAll(((DeltaLocation) - // // locElement).getDeltaOperandLocationVec()); - // baseLocationTuple.addAll(((DeltaLocation) - // locElement).getBaseLocationTuple()); - // } else { - // baseLocationTuple.addElement(locElement); - // } - // } - // return baseLocationTuple; + public boolean isEmpty() { + return locTuple.size() == 0; } - // public List getBaseLocationList() { - // - // Set baseLocationSet = new HashSet(); - // int tupleSize = locTuple.size(); - // for (int i = 0; i < tupleSize; i++) { - // Location locElement = locTuple.at(i); - // - // if (locElement instanceof DeltaLocation) { - // // baseLocationSet.addAll(((DeltaLocation) - // // locElement).getDeltaOperandLocationVec()); - // baseLocationSet.addAll(((DeltaLocation) locElement).getBaseLocationSet()); - // } else { - // baseLocationSet.add(locElement); - // } - // } - // return baseLocationSet; - // } - - // public int getNumofDelta() { - // - // int result = 0; - // - // if (locTuple.size() == 1) { - // Location locElement = locTuple.at(0); - // if (locElement instanceof DeltaLocation) { - // result++; - // result += getNumofDelta((DeltaLocation) locElement); - // } - // } - // return result; - // } - - // public int getNumofDelta(DeltaLocation delta) { - // int result = 0; - // - // if (delta.getDeltaOperandLocationVec().size() == 1) { - // Location locElement = delta.getDeltaOperandLocationVec().at(0); - // if (locElement instanceof DeltaLocation) { - // result++; - // result += getNumofDelta((DeltaLocation) locElement); - // } - // } - // - // return result; - // } - - // public void removieLocation(ClassDescriptor cd) { - // for (int i = 0; i < locTuple.size(); i++) { - // if (locTuple.at(i).getClassDescriptor().equals(cd)) { - // locTuple.removeAt(i); - // return; - // } - // } - // } - public String toString() { - // for better representation - // if compositeLoc has only one single location, - // just print out single location - // if(locTuple.size()==1){ - // Location locElement=locTuple.at(0); - // if(locElement instanceof Location){ - // return locElement.toString(); - // } - // } - String rtr = "CompLoc["; int tupleSize = locTuple.size(); diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java index 54a17f44..3edbd818 100644 --- a/Robust/src/Analysis/SSJava/FlowDownCheck.java +++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java @@ -781,7 +781,7 @@ public class FlowDownCheck { NameDescriptor nd = nn.getName(); if (nd.getBase() != null) { loc = checkLocationFromExpressionNode(md, nametable, nn.getExpression(), loc); - addTypeLocation(nn.getExpression().getType(), loc); + // addTypeLocation(nn.getExpression().getType(), loc); } else { String varname = nd.toString(); @@ -862,20 +862,14 @@ public class FlowDownCheck { } else { destLocation = srcLocation = checkLocationFromExpressionNode(md, nametable, an.getDest(), srcLocation); - // TODO - // if (!((Set) state.getCd2LocationPropertyMap().get(new Pair(cd, - // "spin"))) - // .contains(destLocation.getLocation(cd).getLocIdentifier())) { - // throw new Error("Location " + destLocation + - // " is not allowed to have spinning values at " - // + cd.getSourceFileName() + ":" + an.getNumLine()); - // } + + if (!CompositeLattice.isGreaterThan(srcLocation, destLocation)) { + throw new Error("Location " + destLocation + + " is not allowed to have the value flow that moves within the same location at " + + cd.getSourceFileName() + "::" + an.getNumLine()); + } } - // if (an.getSrc() != null) { - // addTypeLocation(an.getSrc().getType(), srcLocation); - // } - // addTypeLocation(an.getDest().getType(), destLocation); return destLocation; } @@ -956,9 +950,6 @@ public class FlowDownCheck { SSJavaLattice localLattice = CompositeLattice.getLatticeByDescriptor(md); Location localLoc = new Location(md, localLocId); if (localLattice == null || (!localLattice.containsKey(localLocId))) { - System.out.println("md=" + md); - System.out.println("localLattice=" + localLattice + " l=" + localLocId); - System.out.println("localLattice leemtn=" + localLattice.table); throw new Error("Location " + localLocId + " is not defined in the local variable lattice at " + md.getClassDesc().getSourceFileName() + "::" + n.getNumLine() + "."); @@ -1042,7 +1033,7 @@ public class FlowDownCheck { // d2loc.put(fd, loc); addTypeLocation(fd.getType(), loc); - } + } } } @@ -1063,8 +1054,6 @@ public class FlowDownCheck { public static boolean isGreaterThan(CompositeLocation loc1, CompositeLocation loc2) { - // System.out.println("\nisGreaterThan=" + loc1 + " ? " + loc2); - int baseCompareResult = compareBaseLocationSet(loc1, loc2); if (baseCompareResult == ComparisonResult.EQUAL) { if (compareDelta(loc1, loc2) == ComparisonResult.GREATER) { @@ -1133,10 +1122,16 @@ public class FlowDownCheck { } if (loc1.getLocIdentifier().equals(loc2.getLocIdentifier())) { + // check if the current location is the spinning location + if (lattice1.getSpinLocSet().contains(loc1.getLocIdentifier())) { + return ComparisonResult.GREATER; + } numOfTie++; continue; } else if (lattice1.isGreaterThan(loc1.getLocIdentifier(), loc2.getLocIdentifier())) { return ComparisonResult.GREATER; + } else { + return ComparisonResult.LESS; } } diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java index 838e5103..50d35f7c 100644 --- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java +++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java @@ -127,7 +127,7 @@ public class SSJavaAnalysis { locOrder.setGlobalLoc(globalLoc); } else if (orderElement.contains("*")) { // spin loc definition - locOrder.addSpinLoc(orderElement); + locOrder.addSpinLoc(orderElement.substring(0,orderElement.length()-1)); } else { // single element locOrder.put(orderElement); @@ -167,7 +167,7 @@ public class SSJavaAnalysis { } } else if (orderElement.contains("*")) { // spin loc definition - locOrder.addSpinLoc(orderElement); + locOrder.addSpinLoc(orderElement.substring(0,orderElement.length()-1)); } else { // single element locOrder.put(orderElement); diff --git a/Robust/src/Tests/ssJava/flowdown/test.java b/Robust/src/Tests/ssJava/flowdown/test.java index f17f3f5b..b0e75dad 100644 --- a/Robust/src/Tests/ssJava/flowdown/test.java +++ b/Robust/src/Tests/ssJava/flowdown/test.java @@ -27,13 +27,26 @@ public class test{ } public void doit2(){ - @LOC("methodH,testL") int localVarL; - + @LOC("methodH,testL") int localVarL; // value flows from the field [local.methodH,field.testH] // to the local variable [local.methodL] localVarL=fieldH; } + public void doit3(){ + @LOC("methodT,testL")int localVar=fooM.a+fooM.b; + // GLB(fooM.a,fooM.b)=LOC[methodT,testM,FB] + // LOC[lovalVar]=[methodT,testL] < GLB(fooM.a,fooM.b) + } + + // creating composite location by object references + public void doit4(){ + @LOC("methodT,testM,FC,BB") int localVar=fooM.bar.a; + //LOC(fooM.bar.a)=[methodT,testM,FC,BA] + //localVar can flow into lower location of fooM.bar.a + fooM.bar.c=localVar; //[methodT,testM,FC,BB] < [methodT,testM,FC,BA] + } + // method has its own local variable lattice @LATTICE("mL [mH,testM] } + @LATTICE("mL50000){ + // value can be flowing back to the varSpin + // since 'varSpin' is location allowing value to move within + // the same abstract location + varSpin=varSpin+varH; + } + varL=varSpin; + } + + @LATTICE("mL