changes on NameNode checking

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index 85a70c4d7e2dff6b77bfa94b26d50c2fcfb45b16..4589aaca24fe1ceea100100b0e069d8be49aeeb1 100644 (file)
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -410,8 +410,8 @@ public class FlowDownCheck {
       // declaration annotation
       CompositeLocation returnLocAt = md2ReturnLoc.get(md);
 
       // declaration annotation
       CompositeLocation returnLocAt = md2ReturnLoc.get(md);
 

-      if (CompositeLattice.compare(returnLocAt, expLoc,
-          generateErrorMessage(md.getClassDesc(), rn))!=ComparisonResult.LESS) {
+      if (CompositeLattice
+          .compare(returnLocAt, expLoc, generateErrorMessage(md.getClassDesc(), rn)) != ComparisonResult.LESS) {

         throw new Error(
             "Return value location is not equal or higher than the declaraed return location at "
                 + md.getClassDesc().getSourceFileName() + "::" + rn.getNumLine());
         throw new Error(
             "Return value location is not equal or higher than the declaraed return location at "
                 + md.getClassDesc().getSourceFileName() + "::" + rn.getNumLine());


@@ -907,7 +907,7 @@ public class FlowDownCheck {
     if (on.getRight() != null) {
       System.out.println("right loc=" + rightLoc + " from " + on.getRight().kind());
     }
     if (on.getRight() != null) {
       System.out.println("right loc=" + rightLoc + " from " + on.getRight().kind());
     }

-    
+

     Operation op = on.getOp();
 
     switch (op.getOp()) {
     Operation op = on.getOp();
 
     switch (op.getOp()) {


@@ -966,11 +966,9 @@ public class FlowDownCheck {
   private CompositeLocation checkLocationFromNameNode(MethodDescriptor md, SymbolTable nametable,
       NameNode nn, CompositeLocation loc) {
 
   private CompositeLocation checkLocationFromNameNode(MethodDescriptor md, SymbolTable nametable,
       NameNode nn, CompositeLocation loc) {
 

-

     NameDescriptor nd = nn.getName();
     if (nd.getBase() != null) {
       loc = checkLocationFromExpressionNode(md, nametable, nn.getExpression(), loc);
     NameDescriptor nd = nn.getName();
     if (nd.getBase() != null) {
       loc = checkLocationFromExpressionNode(md, nametable, nn.getExpression(), loc);

-      // addTypeLocation(nn.getExpression().getType(), loc);

     } else {
       String varname = nd.toString();
       if (varname.equals("this")) {
     } else {
       String varname = nd.toString();
       if (varname.equals("this")) {


@@ -1031,17 +1029,41 @@ public class FlowDownCheck {
       SymbolTable nametable, FieldAccessNode fan, CompositeLocation loc) {
 
     ExpressionNode left = fan.getExpression();
       SymbolTable nametable, FieldAccessNode fan, CompositeLocation loc) {
 
     ExpressionNode left = fan.getExpression();

-    loc = checkLocationFromExpressionNode(md, nametable, left, loc);
+    TypeDescriptor ltd = left.getType();

 
 

+    FieldDescriptor fd = fan.getField();
+
+    if (ltd.isClassNameRef()) {
+      // using a class name directly
+      if (fd.isStatic() && fd.isFinal()) {
+        loc.addLocation(Location.createTopLocation(md));
+        return loc;
+      }
+    }
+
+    loc = checkLocationFromExpressionNode(md, nametable, left, loc);

     if (!left.getType().isPrimitive()) {
     if (!left.getType().isPrimitive()) {

-      FieldDescriptor fd = fan.getField();
-      Location fieldLoc = (Location) fd.getType().getExtension();
+      Location fieldLoc = getFieldLocation(fd);

       loc.addLocation(fieldLoc);
     }
 
     return loc;
   }
 
       loc.addLocation(fieldLoc);
     }
 
     return loc;
   }
 

+  private Location getFieldLocation(FieldDescriptor fd) {
+
+    Location fieldLoc = (Location) fd.getType().getExtension();
+
+    // handle the case that method annotation checking skips checking field
+    // declaration
+    if (fieldLoc == null) {
+      fieldLoc = checkFieldDeclaration(fd.getClassDescriptor(), fd);
+    }
+
+    return fieldLoc;
+
+  }
+

   private CompositeLocation checkLocationFromAssignmentNode(MethodDescriptor md,
       SymbolTable nametable, AssignmentNode an, CompositeLocation loc) {
 
   private CompositeLocation checkLocationFromAssignmentNode(MethodDescriptor md,
       SymbolTable nametable, AssignmentNode an, CompositeLocation loc) {
 


@@ -1066,11 +1088,12 @@ public class FlowDownCheck {
       }
       srcLocation = new CompositeLocation();
       srcLocation = checkLocationFromExpressionNode(md, nametable, an.getSrc(), srcLocation);
       }
       srcLocation = new CompositeLocation();
       srcLocation = checkLocationFromExpressionNode(md, nametable, an.getSrc(), srcLocation);

-      // System.out.println(" an= " + an.printNode(0) + " an.getSrc()=" +
-      // an.getSrc().getClass()
-      // + " at " + cd.getSourceFileName() + "::" + an.getNumLine());
-      // System.out.println("srcLocation=" + srcLocation);
-      // System.out.println("dstLocation=" + destLocation);
+      
+//      System.out.println(" an= " + an.printNode(0) + " an.getSrc()=" + an.getSrc().getClass()
+//          + " at " + cd.getSourceFileName() + "::" + an.getNumLine());
+//      System.out.println("srcLocation=" + srcLocation);
+//      System.out.println("dstLocation=" + destLocation);
+      

       if (!CompositeLattice.isGreaterThan(srcLocation, destLocation, generateErrorMessage(cd, an))) {
         throw new Error("The value flow from " + srcLocation + " to " + destLocation
             + " does not respect location hierarchy on the assignment " + an.printNode(0) + " at "
       if (!CompositeLattice.isGreaterThan(srcLocation, destLocation, generateErrorMessage(cd, an))) {
         throw new Error("The value flow from " + srcLocation + " to " + destLocation
             + " does not respect location hierarchy on the assignment " + an.printNode(0) + " at "


@@ -1261,7 +1284,7 @@ public class FlowDownCheck {
     // TODO
   }
 
     // TODO
   }
 

-  private void checkFieldDeclaration(ClassDescriptor cd, FieldDescriptor fd) {
+  private Location checkFieldDeclaration(ClassDescriptor cd, FieldDescriptor fd) {

 
     Vector<AnnotationDescriptor> annotationVec = fd.getType().getAnnotationMarkers();
 
 
     Vector<AnnotationDescriptor> annotationVec = fd.getType().getAnnotationMarkers();
 


@@ -1278,9 +1301,9 @@ public class FlowDownCheck {
     }
 
     AnnotationDescriptor ad = annotationVec.elementAt(0);
     }
 
     AnnotationDescriptor ad = annotationVec.elementAt(0);

+    Location loc = null;

 
     if (ad.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) {
 
     if (ad.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) {

-

       if (ad.getMarker().equals(SSJavaAnalysis.LOC)) {
         String locationID = ad.getValue();
         // check if location is defined
       if (ad.getMarker().equals(SSJavaAnalysis.LOC)) {
         String locationID = ad.getValue();
         // check if location is defined


@@ -1290,7 +1313,7 @@ public class FlowDownCheck {
               + " is not defined in the field lattice of class " + cd.getSymbol() + " at"
               + cd.getSourceFileName() + ".");
         }
               + " is not defined in the field lattice of class " + cd.getSymbol() + " at"
               + cd.getSourceFileName() + ".");
         }

-        Location loc = new Location(cd, locationID);
+        loc = new Location(cd, locationID);

 
         if (ssjava.isSharedLocation(loc)) {
           ssjava.mapSharedLocation2Descriptor(loc, fd);
 
         if (ssjava.isSharedLocation(loc)) {
           ssjava.mapSharedLocation2Descriptor(loc, fd);


@@ -1301,6 +1324,7 @@ public class FlowDownCheck {
       }
     }
 
       }
     }
 

+    return loc;

   }
 
   private void addLocationType(TypeDescriptor type, CompositeLocation loc) {
   }
 
   private void addLocationType(TypeDescriptor type, CompositeLocation loc) {

diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
index 21ae3920f1146231f9a47a998c2d44ee79f54cda..80468a94ab9ef69733dfd916d09ba717d023d8d4 100644 (file)
--- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
+++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
@@ -285,6 +285,10 @@ public class SSJavaAnalysis {
     return annotationRequireClassSet.contains(cd);
   }
 
     return annotationRequireClassSet.contains(cd);
   }
 

+  public void addAnnotationRequire(ClassDescriptor cd) {
+    annotationRequireClassSet.add(cd);
+  }
+

   public void addAnnotationRequire(MethodDescriptor md) {
 
     // if a method requires to be annotated, class containg that method also
   public void addAnnotationRequire(MethodDescriptor md) {
 
     // if a method requires to be annotated, class containg that method also