From: yeom <yeom>
Date: Fri, 20 May 2011 18:51:22 +0000 (+0000)
Subject: fix bugs on the flow down rule and start annotating ssjava class library again
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=d652086ece80e8083f30aab3e48346b87bf3ff9e;p=IRC.git
fix bugs on the flow down rule and start annotating ssjava class library again
---
diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index 65240aa1..de46e711 100644
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -265,7 +265,9 @@ public class FlowDownCheck {
// matter what it is going to return.
loc.addLocation(Location.createBottomLocation(md));
} else {
- loc = checkLocationFromExpressionNode(md, nametable, returnExp, loc);
+ // by default, return node has "bottom" location
+ // loc = checkLocationFromExpressionNode(md, nametable, returnExp, loc);
+ loc.addLocation(Location.createBottomLocation(md));
}
return loc;
}
@@ -475,7 +477,7 @@ public class FlowDownCheck {
break;
case Kind.MethodInvokeNode:
- compLoc = checkLocationFromMethodInvokeNode(md, nametable, (MethodInvokeNode) en);
+ compLoc = checkLocationFromMethodInvokeNode(md, nametable, (MethodInvokeNode) en, loc);
break;
case Kind.TertiaryNode:
@@ -556,30 +558,7 @@ public class FlowDownCheck {
}
private CompositeLocation checkLocationFromMethodInvokeNode(MethodDescriptor md,
- SymbolTable nametable, MethodInvokeNode min) {
-
- // Location baseLoc = null;
- // if (min.getBaseName() != null) {
- // Descriptor d = nametable.get(min.getBaseName().getSymbol());
- // if (d instanceof VarDescriptor) {
- // CompositeLocation varLoc = (CompositeLocation) ((VarDescriptor)
- // d).getType().getExtension();
- // return varLoc;
- // } else {
- // // it is field descriptor
- // assert (d instanceof FieldDescriptor);
- // CompositeLocation fieldLoc =
- // (CompositeLocation) min.getExpression().getType().getExtension();
- // return fieldLoc;
- // }
- // } else {
- // // method invocation starting from this
- // MethodLattice<String> methodLattice = ssjava.getMethodLattice(md);
- // System.out.println("md=" + md + " lattice=" + methodLattice);
- // String thisLocId = methodLattice.getThisLoc();
- // baseLoc = new Location(md, thisLocId);
- // }
- // System.out.println("BASE LOC=" + baseLoc);
+ SymbolTable nametable, MethodInvokeNode min, CompositeLocation loc) {
if (min.numArgs() > 1) {
// caller needs to guarantee that it passes arguments in regarding to
@@ -627,7 +606,6 @@ public class FlowDownCheck {
}
// all arguments should be higher than the location of return value
-
Set<CompositeLocation> inputGLBSet = new HashSet<CompositeLocation>();
for (int i = 0; i < min.numArgs(); i++) {
ExpressionNode en = min.getArg(i);
@@ -636,12 +614,39 @@ public class FlowDownCheck {
inputGLBSet.add(callerArg);
}
- if (inputGLBSet.size() > 0) {
- return CompositeLattice.calculateGLB(inputGLBSet);
+ // if (inputGLBSet.size() > 0) {
+ // return CompositeLattice.calculateGLB(inputGLBSet);
+ // } else {
+ // // if there are no arguments,
+ // // method invocation from the same class
+ // CompositeLocation compLoc = new CompositeLocation();
+ // return compLoc;
+ // }
+
+ Location baseLoc = null;
+ if (min.getBaseName() != null) {
+ Descriptor d = nametable.get(min.getBaseName().getSymbol());
+ if (d instanceof VarDescriptor) {
+ CompositeLocation varLoc = (CompositeLocation) ((VarDescriptor) d).getType().getExtension();
+ return varLoc;
+ } else {
+ // it is field descriptor
+ assert (d instanceof FieldDescriptor);
+ Location fieldLoc = (Location) min.getExpression().getType().getExtension();
+ CompositeLocation compLoc = new CompositeLocation();
+ MethodLattice<String> methodLattice = ssjava.getMethodLattice(md);
+ Location thisLoc = new Location(md, methodLattice.getThisLoc());
+ compLoc.addLocation(thisLoc);
+ compLoc.addLocation(fieldLoc);
+ return compLoc;
+ }
} else {
- // if there are no arguments,
- // method invocation from the same class
+ // method invocation starting from this
+ MethodLattice<String> methodLattice = ssjava.getMethodLattice(md);
+ String thisLocId = methodLattice.getThisLoc();
+ baseLoc = new Location(md, thisLocId);
CompositeLocation compLoc = new CompositeLocation();
+ compLoc.addLocation(baseLoc);
return compLoc;
}
@@ -658,12 +663,12 @@ public class FlowDownCheck {
CompositeLocation arrayLoc =
checkLocationFromExpressionNode(md, nametable, aan.getExpression(), new CompositeLocation());
- addTypeLocation(aan.getExpression().getType(), arrayLoc);
+ // addTypeLocation(aan.getExpression().getType(), arrayLoc);
glbInputSet.add(arrayLoc);
CompositeLocation indexLoc =
checkLocationFromExpressionNode(md, nametable, aan.getIndex(), new CompositeLocation());
glbInputSet.add(indexLoc);
- addTypeLocation(aan.getIndex().getType(), indexLoc);
+ // addTypeLocation(aan.getIndex().getType(), indexLoc);
CompositeLocation glbLoc = CompositeLattice.calculateGLB(glbInputSet);
return glbLoc;
@@ -714,11 +719,9 @@ public class FlowDownCheck {
// addTypeLocation(on.getRight().getType(), rightLoc);
}
- // System.out.println("checking op node=" + on.printNode(0));
- // System.out.println("left loc=" + leftLoc + " from " +
- // on.getLeft().getClass());
- // System.out.println("right loc=" + rightLoc + " from " +
- // on.getRight().getClass());
+// System.out.println("checking op node=" + on.printNode(0));
+// System.out.println("left loc=" + leftLoc + " from " + on.getLeft().getClass());
+// System.out.println("right loc=" + rightLoc + " from " + on.getRight().getClass());
Operation op = on.getOp();
@@ -788,7 +791,12 @@ public class FlowDownCheck {
if (varname.equals("this")) {
// 'this' itself!
MethodLattice<String> methodLattice = ssjava.getMethodLattice(md);
- Location locElement = new Location(md, methodLattice.getThisLoc());
+ String thisLocId = methodLattice.getThisLoc();
+ if (thisLocId == null) {
+ throw new Error("The location for 'this' is not defined at "
+ + md.getClassDesc().getSourceFileName() + "::" + nn.getNumLine());
+ }
+ Location locElement = new Location(md, thisLocId);
loc.addLocation(locElement);
return loc;
}
@@ -1210,16 +1218,9 @@ public class FlowDownCheck {
String glbOfPriorityLoc = locOrder.getGLB(priorityLocIdentifierSet);
glbCompLoc.addLocation(new Location(priorityDescriptor, glbOfPriorityLoc));
-
Set<CompositeLocation> compSet = locId2CompLocSet.get(glbOfPriorityLoc);
- if (compSet.size() == 1) {
- // if GLB(x1,x2)==x1 or x2 : GLB case 2,3
- CompositeLocation comp = compSet.iterator().next();
- for (int i = 1; i < comp.getSize(); i++) {
- glbCompLoc.addLocation(comp.get(i));
- }
- } else if (compSet.size() == 0) {
+ if (compSet == null) {
// when GLB(x1,x2)!=x1 and !=x2 : GLB case 4
// mean that the result is already lower than <x1,y1> and <x2,y2>
// assign TOP to the rest of the location elements
@@ -1228,29 +1229,37 @@ public class FlowDownCheck {
glbCompLoc.addLocation(Location.createTopLocation(inputComp.get(i).getDescriptor()));
}
} else {
- // when GLB(x1,x2)==x1 and x2 : GLB case 1
- // if more than one location shares the same priority GLB
- // need to calculate the rest of GLB loc
-
- int compositeLocSize = compSet.iterator().next().getSize();
-
- Set<String> glbInputSet = new HashSet<String>();
- Descriptor currentD = null;
- for (int i = 1; i < compositeLocSize; i++) {
- for (Iterator iterator = compSet.iterator(); iterator.hasNext();) {
- CompositeLocation compositeLocation = (CompositeLocation) iterator.next();
- Location currentLoc = compositeLocation.get(i);
- currentD = currentLoc.getDescriptor();
- // making set of the current location sharing the same idx
- glbInputSet.add(currentLoc.getLocIdentifier());
+ if (compSet.size() == 1) {
+ // if GLB(x1,x2)==x1 or x2 : GLB case 2,3
+ CompositeLocation comp = compSet.iterator().next();
+ for (int i = 1; i < comp.getSize(); i++) {
+ glbCompLoc.addLocation(comp.get(i));
}
- // calculate glb for the current lattice
+ } else {
+ // when GLB(x1,x2)==x1 and x2 : GLB case 1
+ // if more than one location shares the same priority GLB
+ // need to calculate the rest of GLB loc
+
+ int compositeLocSize = compSet.iterator().next().getSize();
+
+ Set<String> glbInputSet = new HashSet<String>();
+ Descriptor currentD = null;
+ for (int i = 1; i < compositeLocSize; i++) {
+ for (Iterator iterator = compSet.iterator(); iterator.hasNext();) {
+ CompositeLocation compositeLocation = (CompositeLocation) iterator.next();
+ Location currentLoc = compositeLocation.get(i);
+ currentD = currentLoc.getDescriptor();
+ // making set of the current location sharing the same idx
+ glbInputSet.add(currentLoc.getLocIdentifier());
+ }
+ // calculate glb for the current lattice
- SSJavaLattice<String> currentLattice = getLatticeByDescriptor(currentD);
- String currentGLBLocId = currentLattice.getGLB(glbInputSet);
- glbCompLoc.addLocation(new Location(currentD, currentGLBLocId));
- }
+ SSJavaLattice<String> currentLattice = getLatticeByDescriptor(currentD);
+ String currentGLBLocId = currentLattice.getGLB(glbInputSet);
+ glbCompLoc.addLocation(new Location(currentD, currentGLBLocId));
+ }
+ }
}
return glbCompLoc;
diff --git a/Robust/src/ClassLibrary/SSJava/String.java b/Robust/src/ClassLibrary/SSJava/String.java
index 3111820d..6b85b662 100644
--- a/Robust/src/ClassLibrary/SSJava/String.java
+++ b/Robust/src/ClassLibrary/SSJava/String.java
@@ -1,15 +1,66 @@
-//@LATTICE("data<proc,proc<c,c<in,in*,c*,proc*,data*")
-@LATTICE("V<C, V<O")
-@DEFAULTMETHOD("O<V,V<I,V<C,THIS=O")
+@LATTICE("String_V<String_C, String_V<String_O")
+@METHODDEFAULT("StringDM_O<StringDM_V,StringDM_V<StringDM_C,StringDM_C<StringDM_I,THISLOC=StringDM_O,StringDM_C*")
public class String {
- @LOC("V") char value[];
- @LOC("C") int count;
- @LOC("O") int offset;
- @LOC("V") private int cachedHashcode;
+ @LOC("String_V") char value[];
+ @LOC("String_C") int count;
+ @LOC("String_O") int offset;
+ @LOC("String_V") private int cachedHashcode;
private String() {
}
+
+ public String(@LOC("StringDM_I") char c) {
+ @LOC("StringDM_V") char[] str = new char[1];
+ str[0] = c;
+ String(str);
+ }
+
+ public String(@LOC("StringDM_I") char str[]) {
+ @LOC("StringDM_V") char charstr[]=new char[str.length];
+ for(@LOC("StringDM_C") int i=0; i<str.length; i++)
+ charstr[i]=str[i];
+ this.value=charstr;
+ this.count=str.length;
+ this.offset=0;
+ }
+
+ @LATTICE("StringM1_O<StringM1_V,StringM1_V<StringM1_C,StringM1_C<StringM1_I,THISLOC=StringM1_I,StringM1_C*")
+ public String concat(@LOC("StringM1_I") String str) {
+ @LOC("StringM1_O") String newstr=new String(); // create new one, it has OUT location
+ @LOC("StringM1_C") int newCount=this.count+str.count;
+
+ @LOC("StringM1_V") char charstr[]=new char[newCount];
+
+ // here, for loop introduces indirect flow from [C] to [V]
+ for(@LOC("StringM1_C") int i=0; i<count; i++) {
+ // value flows from GLB(THISLOC,C,THISLOC.V)=(THISLOC,TOP) to [V]
+ charstr[i]=value[i+offset];
+ }
+ for(@LOC("StringM1_C") int i=0; i<str.count; i++) {
+ charstr[i+count]=str.value[i+str.offset];
+ }
+
+ newstr.value=charstr;
+ // LOC(newstr.value)=[O,STRING_V]
+ // LOC(charstr)=[V]
+ // [O,STRING_V] < [V]
+
+ return newstr;
+ }
-
+ public boolean equals(@LOC("StringDM_I") Object o) {
+ if (o.getType()!=getType()) // values are coming from [StringDM_I] and [THISLOC]
+ return false;
+ @LOC("StringDM_V") String s=(String)o;
+ if (s.count!=count)
+ return false;
+ for(@LOC("StringDM_C") int i=0; i<count; i++) {
+ if (s.value[i+s.offset]!=value[i+offset])
+ return false;
+ }
+ return true;
+ }
+
+
}
diff --git a/Robust/src/Tests/ssJava/flowdown/test.java b/Robust/src/Tests/ssJava/flowdown/test.java
index 605957b3..46dfb95d 100644
--- a/Robust/src/Tests/ssJava/flowdown/test.java
+++ b/Robust/src/Tests/ssJava/flowdown/test.java
@@ -140,6 +140,7 @@ class Foo{
}
@LATTICE("BC<BB,BB<BA,BB*")
+@METHODDEFAULT("BARMD_L<BARMD_H,THISLOC=BARMD_H")
class Bar{
@LOC("BA") int a;
@LOC("BB") int b2;