From 52d846e6280d4eb8c4740165f6e4513cbf9d7481 Mon Sep 17 00:00:00 2001
From: yeom <yeom>
Date: Tue, 31 May 2011 23:48:40 +0000
Subject: [PATCH] add one more checking, class inheritance: If a class B has a
 super class A, all relative orderings of class A must be respected by the
 ordering lattice of class B.

---
 Robust/src/Analysis/SSJava/FlowDownCheck.java | 48 +++++++++++++++----
 Robust/src/Util/Lattice.java                  | 27 +++++++++++
 2 files changed, 67 insertions(+), 8 deletions(-)

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index 82e3dc11..980a3266 100644
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -41,6 +41,7 @@ import IR.Tree.ReturnNode;
 import IR.Tree.SubBlockNode;
 import IR.Tree.TertiaryNode;
 import IR.Tree.TreeNode;
+import Util.Pair;
 
 public class FlowDownCheck {
 
@@ -97,6 +98,13 @@ public class FlowDownCheck {
       toanalyze.remove(cd);
 
       if (!cd.isInterface()) {
+
+        ClassDescriptor superDesc = cd.getSuperDesc();
+        if (superDesc != null && (!superDesc.isInterface())
+            && (!superDesc.getSymbol().equals("Object"))) {
+          checkOrderingInheritance(superDesc, cd);
+        }
+
         checkDeclarationInClass(cd);
         for (Iterator method_it = cd.getMethods(); method_it.hasNext();) {
           MethodDescriptor md = (MethodDescriptor) method_it.next();
@@ -133,6 +141,28 @@ public class FlowDownCheck {
 
   }
 
+  private void checkOrderingInheritance(ClassDescriptor superCd, ClassDescriptor cd) {
+    // here, we're going to check that sub class keeps same relative orderings
+    // in respect to super class
+
+    SSJavaLattice<String> superLattice = ssjava.getClassLattice(superCd);
+    SSJavaLattice<String> subLattice = ssjava.getClassLattice(cd);
+
+    Set<Pair<String, String>> superPairSet = superLattice.getOrderingPairSet();
+    Set<Pair<String, String>> subPairSet = subLattice.getOrderingPairSet();
+
+    for (Iterator iterator = superPairSet.iterator(); iterator.hasNext();) {
+      Pair<String, String> pair = (Pair<String, String>) iterator.next();
+
+      if (!subPairSet.contains(pair)) {
+        throw new Error("Subclass '" + cd + "' does not have the relative ordering '"
+            + pair.getSecond() + " < " + pair.getFirst() + "' that is defined by its superclass '"
+            + superCd + "'.");
+      }
+    }
+
+  }
+
   public Hashtable getMap() {
     return d2loc;
   }
@@ -644,7 +674,6 @@ public class FlowDownCheck {
 
   }
 
- 
   private CompositeLocation checkLocationFromArrayAccessNode(MethodDescriptor md,
       SymbolTable nametable, ArrayAccessNode aan) {
 
@@ -712,9 +741,11 @@ 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();
 
@@ -877,10 +908,11 @@ public class FlowDownCheck {
       }
       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)) {
         throw new Error("The value flow from " + srcLocation + " to " + destLocation
             + " does not respect location hierarchy on the assignment " + an.printNode(0) + " at "
diff --git a/Robust/src/Util/Lattice.java b/Robust/src/Util/Lattice.java
index cb8da73f..e22103c5 100644
--- a/Robust/src/Util/Lattice.java
+++ b/Robust/src/Util/Lattice.java
@@ -220,4 +220,31 @@ public class Lattice<T> {
     return lowerSet;
   }
 
+  public Set<Pair<T, T>> getOrderingPairSet() {
+    // return the set of pairs in the lattice
+
+    Set<Pair<T, T>> set = new HashSet<Pair<T, T>>();
+
+    Set<T> visited = new HashSet<T>();
+    Set<T> needtovisit = new HashSet<T>();
+    needtovisit.add(top);
+
+    while (!needtovisit.isEmpty()) {
+      T key = needtovisit.iterator().next();
+      Set<T> lowerSet = table.get(key);
+      if(lowerSet!=null){
+        for (Iterator iterator = lowerSet.iterator(); iterator.hasNext();) {
+          T lowerItem = (T) iterator.next();
+          set.add(new Pair(key, lowerItem));
+          if (!visited.contains(key)) {
+            needtovisit.add(lowerItem);
+          }
+        }
+      }
+      visited.add(key);
+      needtovisit.remove(key);
+    }
+    return set;
+  }
+
 }
-- 
2.34.1