bug fix on flow-down rule: check if all of assignments done by invoking method respec...

diff --git a/Robust/src/Analysis/SSJava/CompositeLocation.java b/Robust/src/Analysis/SSJava/CompositeLocation.java
index 23982187337f057d6806bf3498e30f38b8ba87f1..5308cb67ddaf4f9017dd8c95cbdd799911cc784d 100644 (file)
--- a/Robust/src/Analysis/SSJava/CompositeLocation.java
+++ b/Robust/src/Analysis/SSJava/CompositeLocation.java
@@ -35,6 +35,18 @@ public class CompositeLocation implements TypeExtension {
     return locTuple.size() == 0;
   }
 
+  public boolean startsWith(CompositeLocation prefix) {
+    // tests if this composite location starts with the prefix
+
+    for (int i = 0; i < prefix.getSize(); i++) {
+      if (!prefix.get(i).equals(get(i))) {
+        return false;
+      }
+    }
+    return true;
+
+  }
+
   public String toString() {
 
     String rtr = "CompLoc[";

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index 0dfd8892705f417e8fcaa73e615b361ac67a91d5..9d41b8388f24bbbc74d000ac7f51185411ab546f 100644 (file)
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -222,7 +222,7 @@ public class FlowDownCheck {
         MethodDescriptor md = toAnalyzeMethodNext();
         if (ssjava.needTobeAnnotated(md)) {
           System.out.println("SSJAVA: Checking assignments: " + md);
-          checkMethodBody(cd, md);
+          checkMethodBody(cd, md, null);
         }
       }
     }
@@ -431,9 +431,10 @@ public class FlowDownCheck {
     checkDeclarationInBlockNode(md, nametable, ln.getBody());
   }
 
-  private void checkMethodBody(ClassDescriptor cd, MethodDescriptor md) {
+  private void checkMethodBody(ClassDescriptor cd, MethodDescriptor md,
+      CompositeLocation constraints) {
     BlockNode bn = state.getMethodBody(md);
-    checkLocationFromBlockNode(md, md.getParameterTable(), bn, null);
+    checkLocationFromBlockNode(md, md.getParameterTable(), bn, constraints);
   }
 
   private String generateErrorMessage(ClassDescriptor cd, TreeNode tn) {
@@ -832,42 +833,83 @@ public class FlowDownCheck {
       SymbolTable nametable, MethodInvokeNode min, CompositeLocation loc,
       CompositeLocation constraint) {
 
-    CompositeLocation baseLocation = null;
-    if (min.getExpression() != null) {
-      baseLocation =
-          checkLocationFromExpressionNode(md, nametable, min.getExpression(),
-              new CompositeLocation(), constraint, false);
-    } else {
+    ClassDescriptor cd = md.getClassDesc();
+    MethodDescriptor calleeMD = min.getMethod();
+
+    if (!ssjava.isTrustMethod(calleeMD)) {
+      CompositeLocation baseLocation = null;
+      if (min.getExpression() != null) {
+        baseLocation =
+            checkLocationFromExpressionNode(md, nametable, min.getExpression(),
+                new CompositeLocation(), constraint, false);
+      } else {
 
-      if (min.getMethod().isStatic()) {
-        String globalLocId = ssjava.getMethodLattice(md).getGlobalLoc();
-        if (globalLocId == null) {
-          throw new Error("Method lattice does not define global variable location at "
-              + generateErrorMessage(md.getClassDesc(), min));
+        if (min.getMethod().isStatic()) {
+          String globalLocId = ssjava.getMethodLattice(md).getGlobalLoc();
+          if (globalLocId == null) {
+            throw new Error("Method lattice does not define global variable location at "
+                + generateErrorMessage(md.getClassDesc(), min));
+          }
+          baseLocation = new CompositeLocation(new Location(md, globalLocId));
+        } else {
+          String thisLocId = ssjava.getMethodLattice(md).getThisLoc();
+          baseLocation = new CompositeLocation(new Location(md, thisLocId));
         }
-        baseLocation = new CompositeLocation(new Location(md, globalLocId));
-      } else {
-        String thisLocId = ssjava.getMethodLattice(md).getThisLoc();
-        baseLocation = new CompositeLocation(new Location(md, thisLocId));
+
+      }
+
+      System.out.println("\n#checkLocationFromMethodInvokeNode=" + min.printNode(0)
+          + " baseLocation=" + baseLocation);
+
+      int compareResult =
+          CompositeLattice.compare(constraint, baseLocation, true, generateErrorMessage(cd, min));
+
+      if (compareResult == ComparisonResult.LESS) {
+        throw new Error("Method invocation does not respect the current branch constraint at "
+            + generateErrorMessage(cd, min));
+      } else if (compareResult != ComparisonResult.GREATER) {
+        // if the current constraint is higher than method's THIS location
+        // no need to check constraints!
+        CompositeLocation calleeConstraint =
+            translateCallerLocToCalleeLoc(calleeMD, baseLocation, constraint);
+        checkMethodBody(calleeMD.getClassDesc(), calleeMD, calleeConstraint);
       }
-    }
 
-    checkCalleeConstraints(md, nametable, min, baseLocation, constraint);
+      checkCalleeConstraints(md, nametable, min, baseLocation, constraint);
 
-    checkCallerArgumentLocationConstraints(md, nametable, min, baseLocation, constraint);
+      checkCallerArgumentLocationConstraints(md, nametable, min, baseLocation, constraint);
 
-    if (!min.getMethod().getReturnType().isVoid()) {
-      // If method has a return value, compute the highest possible return
-      // location in the caller's perspective
-      CompositeLocation ceilingLoc =
-          computeCeilingLocationForCaller(md, nametable, min, baseLocation, constraint);
-      return ceilingLoc;
+      if (!min.getMethod().getReturnType().isVoid()) {
+        // If method has a return value, compute the highest possible return
+        // location in the caller's perspective
+        CompositeLocation ceilingLoc =
+            computeCeilingLocationForCaller(md, nametable, min, baseLocation, constraint);
+        return ceilingLoc;
+      }
     }
 
     return new CompositeLocation();
 
   }
 
+  private CompositeLocation translateCallerLocToCalleeLoc(MethodDescriptor calleeMD,
+      CompositeLocation calleeBaseLoc, CompositeLocation constraint) {
+
+    CompositeLocation calleeConstraint = new CompositeLocation();
+
+    // if (constraint.startsWith(calleeBaseLoc)) {
+    // if the first part of constraint loc is matched with callee base loc
+    Location thisLoc = new Location(calleeMD, ssjava.getMethodLattice(calleeMD).getThisLoc());
+    calleeConstraint.addLocation(thisLoc);
+    for (int i = calleeBaseLoc.getSize(); i < constraint.getSize(); i++) {
+      calleeConstraint.addLocation(constraint.get(i));
+    }
+
+    // }
+
+    return calleeConstraint;
+  }
+
   private void checkCallerArgumentLocationConstraints(MethodDescriptor md, SymbolTable nametable,
       MethodInvokeNode min, CompositeLocation callerBaseLoc, CompositeLocation constraint) {
     // if parameter location consists of THIS and FIELD location,
@@ -969,18 +1011,17 @@ public class FlowDownCheck {
     }
 
     System.out.println("\n## computeReturnLocation=" + min.getMethod() + " argList=" + argList);
-    CompositeLocation compLoc = md2ReturnLocGen.get(min.getMethod()).computeReturnLocation(argList);
-    DeltaLocation delta = new DeltaLocation(compLoc, 1);
-    System.out.println("##computeReturnLocation=" + delta);
+    CompositeLocation ceilLoc = md2ReturnLocGen.get(min.getMethod()).computeReturnLocation(argList);
+    System.out.println("## ReturnLocation=" + ceilLoc);
 
-    return delta;
+    return ceilLoc;
 
   }
 
   private void checkCalleeConstraints(MethodDescriptor md, SymbolTable nametable,
       MethodInvokeNode min, CompositeLocation callerBaseLoc, CompositeLocation constraint) {
-    
-    System.out.println("checkCalleeConstraints="+min.printNode(0));
+
+    System.out.println("checkCalleeConstraints=" + min.printNode(0));
 
     MethodDescriptor calleemd = min.getMethod();
 
@@ -1014,7 +1055,7 @@ public class FlowDownCheck {
       for (int i = 0; i < calleemd.numParameters(); i++) {
         VarDescriptor calleevd = (VarDescriptor) calleemd.getParameter(i);
         CompositeLocation calleeLoc = d2loc.get(calleevd);
-        System.out.println("calleevd="+calleevd+" loc="+calleeLoc);
+        System.out.println("calleevd=" + calleevd + " loc=" + calleeLoc);
         calleeParamList.add(calleeLoc);
       }
 
@@ -1033,9 +1074,9 @@ public class FlowDownCheck {
                 || callerLoc2.get(callerLoc2.getSize() - 1).isTop()) {
               continue CHECK;
             }
-            
-            System.out.println("calleeLoc1="+calleeLoc1);
-            System.out.println("calleeLoc2="+calleeLoc2+"calleeParamList="+calleeParamList);
+
+            System.out.println("calleeLoc1=" + calleeLoc1);
+            System.out.println("calleeLoc2=" + calleeLoc2 + "calleeParamList=" + calleeParamList);
 
             int callerResult =
                 CompositeLattice.compare(callerLoc1, callerLoc2, true,
@@ -1356,24 +1397,31 @@ public class FlowDownCheck {
           checkLocationFromExpressionNode(md, nametable, an.getSrc(), new CompositeLocation(),
               constraint, false);
 
+      srcLocation = rhsLocation;
+
+      // if (!rhsLocation.get(rhsLocation.getSize() - 1).isTop()) {
+      if (constraint != null) {
+        inputGLBSet.add(rhsLocation);
+        inputGLBSet.add(constraint);
+        srcLocation = CompositeLattice.calculateGLB(inputGLBSet, generateErrorMessage(cd, an));
+      }
+      // }
+
       System.out.println("dstLocation=" + destLocation);
       System.out.println("rhsLocation=" + rhsLocation);
+      System.out.println("srcLocation=" + srcLocation);
       System.out.println("constraint=" + constraint);
 
-      srcLocation = rhsLocation;
+      if (!CompositeLattice.isGreaterThan(srcLocation, destLocation, generateErrorMessage(cd, an))) {
 
-      if (!rhsLocation.get(rhsLocation.getSize() - 1).isTop()) {
+        String context = "";
         if (constraint != null) {
-          inputGLBSet.add(rhsLocation);
-          inputGLBSet.add(constraint);
-          srcLocation = CompositeLattice.calculateGLB(inputGLBSet, generateErrorMessage(cd, an));
+          context = " and the current context constraint is " + constraint;
         }
-      }
 
-      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 "
-            + cd.getSourceFileName() + "::" + an.getNumLine());
+            + " does not respect location hierarchy on the assignment " + an.printNode(0) + context
+            + " at " + cd.getSourceFileName() + "::" + an.getNumLine());
       }
 
     } else {
@@ -2063,12 +2111,8 @@ class ReturnLocGenerator {
       for (int i = 0; i < args.size(); i++) {
         int type = (paramIdx2paramType.get(new Integer(i))).intValue();
         CompositeLocation argLoc = args.get(i);
-        if (type == PARAMISHIGHER) {
-          // return loc is lower than param
-          DeltaLocation delta = new DeltaLocation(argLoc, 1);
-          inputGLB.add(delta);
-        } else if (type == PARAMISSAME) {
-          // return loc is equal or lower than param
+        if (type == PARAMISHIGHER || type == PARAMISSAME) {
+          // return loc is equal to or lower than param
           inputGLB.add(argLoc);
         }
       }

diff --git a/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java b/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java
index 989903c7f21108c1c95fbd9dedc3b1673287d856..df5d779d92ca616b04531b4f5658eadefd899a83 100644 (file)
--- a/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java
+++ b/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java
@@ -45,7 +45,6 @@ public class MethodAnnotationCheck {
 
   Set<MethodDescriptor> annotatedMDSet;
   Hashtable<MethodDescriptor, Set<MethodDescriptor>> caller2calleeSet;
-  Set<MethodDescriptor> trustWorthyMDSet;
 
   public MethodAnnotationCheck(SSJavaAnalysis ssjava, State state, TypeUtil tu) {
     this.ssjava = ssjava;
@@ -53,11 +52,6 @@ public class MethodAnnotationCheck {
     this.tu = tu;
     caller2calleeSet = new Hashtable<MethodDescriptor, Set<MethodDescriptor>>();
     annotatedMDSet = new HashSet<MethodDescriptor>();
-    trustWorthyMDSet = new HashSet<MethodDescriptor>();
-  }
-
-  public Set<MethodDescriptor> getTrustWorthyMDSet() {
-    return trustWorthyMDSet;
   }
 
   public void methodAnnoatationCheck() {
@@ -101,7 +95,7 @@ public class MethodAnnotationCheck {
           if (!visited.contains(p)) {
             visited.add(p);
 
-            if (!trustWorthyMDSet.contains(calleeMD)) {
+            if (!ssjava.isTrustMethod(calleeMD)) {
               // if method is annotated as "TRUST", do not need to check for
               // linear type & flow-down rule
               tovisit.add(calleeMD);
@@ -133,7 +127,7 @@ public class MethodAnnotationCheck {
       for (int i = 0; i < methodAnnotations.size(); i++) {
         AnnotationDescriptor an = methodAnnotations.elementAt(i);
         if (an.getMarker().equals(ssjava.TRUST)) {
-          trustWorthyMDSet.add(md);
+          ssjava.addTrustMethod(md);
         }
       }
     }

diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
index 6525be5dbaaebd14079b764383b9948f77cf4803..d294a1928a8211b55a56d8d0072330e42518a8a8 100644 (file)
--- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
+++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
@@ -68,6 +68,9 @@ public class SSJavaAnalysis {
   // the set of method descriptor required to check the linear type property
   Set<MethodDescriptor> linearTypeCheckMethodSet;
 
+  // the set of method descriptors annotated as "TRUST"
+  Set<MethodDescriptor> trustWorthyMDSet;
+
   CallGraph callgraph;
 
   LinearTypeCheck checker;
@@ -85,6 +88,7 @@ public class SSJavaAnalysis {
     this.mapSharedLocation2DescriptorSet = new Hashtable<Location, Set<Descriptor>>();
     this.linearTypeCheckMethodSet = new HashSet<MethodDescriptor>();
     this.bf = bf;
+    trustWorthyMDSet = new HashSet<MethodDescriptor>();
   }
 
   public void doCheck() {
@@ -99,6 +103,14 @@ public class SSJavaAnalysis {
     doDefinitelyWrittenCheck();
   }
 
+  public void addTrustMethod(MethodDescriptor md) {
+    trustWorthyMDSet.add(md);
+  }
+
+  public boolean isTrustMethod(MethodDescriptor md) {
+    return trustWorthyMDSet.contains(md);
+  }
+
   private void computeLinearTypeCheckMethodSet() {
 
     Set<MethodDescriptor> allCalledSet = callgraph.getMethodCalls(tu.getMain());
@@ -106,9 +118,7 @@ public class SSJavaAnalysis {
 
     Set<MethodDescriptor> trustedSet = new HashSet<MethodDescriptor>();
 
-    Set<MethodDescriptor> trustAnnoatedSet = methodAnnotationChecker.getTrustWorthyMDSet();
-
-    for (Iterator iterator = trustAnnoatedSet.iterator(); iterator.hasNext();) {
+    for (Iterator iterator = trustWorthyMDSet.iterator(); iterator.hasNext();) {
       MethodDescriptor trustMethod = (MethodDescriptor) iterator.next();
       Set<MethodDescriptor> calledFromTrustMethodSet = callgraph.getMethodCalls(trustMethod);
       trustedSet.add(trustMethod);
@@ -122,7 +132,7 @@ public class SSJavaAnalysis {
     for (Iterator iterator = trustedSet.iterator(); iterator.hasNext();) {
       MethodDescriptor md = (MethodDescriptor) iterator.next();
       Set<MethodDescriptor> callerSet = callgraph.getCallerSet(md);
-      if (!trustedSet.containsAll(callerSet) && !trustAnnoatedSet.contains(md)) {
+      if (!trustedSet.containsAll(callerSet) && !trustWorthyMDSet.contains(md)) {
         linearTypeCheckMethodSet.add(md);
       }
     }