Robust/src/Analysis/SSJava/SSJavaAnalysis.java

   1 package Analysis.SSJava;
   2
   3 import java.util.Hashtable;
   4 import java.util.Iterator;
   5 import java.util.Set;
   6 import java.util.StringTokenizer;
   7 import java.util.Vector;
   8
   9 import IR.AnnotationDescriptor;
  10 import IR.ClassDescriptor;
  11 import IR.MethodDescriptor;
  12 import IR.State;
  13
  14 public class SSJavaAnalysis {
  15
  16   public static final String LATTICE = "LATTICE";
  17   public static final String METHODDEFAULT = "METHODDEFAULT";
  18   public static final String THISLOC = "THISLOC";
  19   public static final String GLOBALLOC = "GLOBALLOC";
  20   public static final String LOC = "LOC";
  21   public static final String DELTA = "delta";
  22   State state;
  23   FlowDownCheck flowDownChecker;
  24
  25   // class -> field lattice
  26   Hashtable<ClassDescriptor, SSJavaLattice<String>> cd2lattice;
  27
  28   // class -> default local variable lattice
  29   Hashtable<ClassDescriptor, MethodLattice<String>> cd2methodDefault;
  30
  31   // method -> local variable lattice
  32   Hashtable<MethodDescriptor, MethodLattice<String>> md2lattice;
  33
  34   public SSJavaAnalysis(State state) {
  35     this.state = state;
  36     cd2lattice = new Hashtable<ClassDescriptor, SSJavaLattice<String>>();
  37     cd2methodDefault = new Hashtable<ClassDescriptor, MethodLattice<String>>();
  38     md2lattice = new Hashtable<MethodDescriptor, MethodLattice<String>>();
  39   }
  40
  41   public void doCheck() {
  42     parseLocationAnnotation();
  43     doFlowDownCheck();
  44     doLoopCheck();
  45   }
  46
  47   public void doFlowDownCheck() {
  48     flowDownChecker = new FlowDownCheck(this, state);
  49     flowDownChecker.flowDownCheck();
  50   }
  51
  52   public void doLoopCheck() {
  53     DefinitelyWrittenCheck checker = new DefinitelyWrittenCheck(state);
  54     checker.definitelyWrittenCheck();
  55   }
  56
  57   private void parseLocationAnnotation() {
  58     Iterator it = state.getClassSymbolTable().getDescriptorsIterator();
  59     while (it.hasNext()) {
  60       ClassDescriptor cd = (ClassDescriptor) it.next();
  61       // parsing location hierarchy declaration for the class
  62       Vector<AnnotationDescriptor> classAnnotations = cd.getModifier().getAnnotations();
  63       for (int i = 0; i < classAnnotations.size(); i++) {
  64         AnnotationDescriptor an = classAnnotations.elementAt(i);
  65         String marker = an.getMarker();
  66         if (marker.equals(LATTICE)) {
  67           SSJavaLattice<String> locOrder = new SSJavaLattice<String>("_top_", "_bottom_");
  68           cd2lattice.put(cd, locOrder);
  69           parseClassLatticeDefinition(cd, an.getValue(), locOrder);
  70         } else if (marker.equals(METHODDEFAULT)) {
  71           MethodLattice<String> locOrder = new MethodLattice<String>("_top_", "_bottom_");
  72           cd2methodDefault.put(cd, locOrder);
  73           parseMethodLatticeDefinition(cd, an.getValue(), locOrder);
  74         }
  75       }
  76       if (!cd2lattice.containsKey(cd)) {
  77         throw new Error("Class " + cd.getSymbol()
  78             + " doesn't have any location hierarchy declaration at " + cd.getSourceFileName());
  79       }
  80
  81       for (Iterator method_it = cd.getMethods(); method_it.hasNext();) {
  82         MethodDescriptor md = (MethodDescriptor) method_it.next();
  83         // parsing location hierarchy declaration for the method
  84         Vector<AnnotationDescriptor> methodAnnotations = cd.getModifier().getAnnotations();
  85         for (int i = 0; i < methodAnnotations.size(); i++) {
  86           AnnotationDescriptor an = methodAnnotations.elementAt(i);
  87           if (an.getMarker().equals(LATTICE)) {
  88             MethodLattice<String> locOrder = new MethodLattice<String>("_top_", "_bottom_");
  89             cd2lattice.put(cd, locOrder);
  90             parseMethodLatticeDefinition(cd, an.getValue(), locOrder);
  91           }
  92         }
  93       }
  94
  95     }
  96   }
  97
  98   private void parseMethodLatticeDefinition(ClassDescriptor cd, String value,
  99       MethodLattice<String> locOrder) {
 100
 101     value = value.replaceAll(" ", ""); // remove all blank spaces
 102
 103     StringTokenizer tokenizer = new StringTokenizer(value, ",");
 104
 105     while (tokenizer.hasMoreTokens()) {
 106       String orderElement = tokenizer.nextToken();
 107       int idx = orderElement.indexOf("<");
 108       if (idx > 0) {// relative order element
 109         String lowerLoc = orderElement.substring(0, idx);
 110         String higherLoc = orderElement.substring(idx + 1);
 111         locOrder.put(higherLoc, lowerLoc);
 112         if (locOrder.isIntroducingCycle(higherLoc)) {
 113           throw new Error("Error: the order relation " + lowerLoc + " < " + higherLoc
 114               + " introduces a cycle.");
 115         }
 116       } else if (orderElement.startsWith(THISLOC + "=")) {
 117         String thisLoc = orderElement.substring(8);
 118         locOrder.setThisLoc(thisLoc);
 119       } else if (orderElement.startsWith(GLOBALLOC + "=")) {
 120         String globalLoc = orderElement.substring(10);
 121         locOrder.setGlobalLoc(globalLoc);
 122       } else if (orderElement.contains("*")) {
 123         // spin loc definition
 124         locOrder.addSpinLoc(orderElement);
 125       } else {
 126         // single element
 127         locOrder.put(orderElement);
 128       }
 129     }
 130
 131     // sanity checks
 132     if (locOrder.getThisLoc() != null && !locOrder.containsKey(locOrder.getThisLoc())) {
 133       throw new Error("Variable 'this' location '" + locOrder.getThisLoc()
 134           + "' is not defined in the default local variable lattice at " + cd.getSourceFileName());
 135     }
 136
 137     if (locOrder.getGlobalLoc() != null && !locOrder.containsKey(locOrder.getGlobalLoc())) {
 138       throw new Error("Variable global location '" + locOrder.getGlobalLoc()
 139           + "' is not defined in the default local variable lattice at " + cd.getSourceFileName());
 140     }
 141   }
 142
 143   private void parseClassLatticeDefinition(ClassDescriptor cd, String value,
 144       SSJavaLattice<String> locOrder) {
 145
 146     value = value.replaceAll(" ", ""); // remove all blank spaces
 147
 148     StringTokenizer tokenizer = new StringTokenizer(value, ",");
 149
 150     while (tokenizer.hasMoreTokens()) {
 151       String orderElement = tokenizer.nextToken();
 152       int idx = orderElement.indexOf("<");
 153
 154       if (idx > 0) {// relative order element
 155         String lowerLoc = orderElement.substring(0, idx);
 156         String higherLoc = orderElement.substring(idx + 1);
 157         locOrder.put(higherLoc, lowerLoc);
 158         if (locOrder.isIntroducingCycle(higherLoc)) {
 159           throw new Error("Error: the order relation " + lowerLoc + " < " + higherLoc
 160               + " introduces a cycle.");
 161         }
 162       } else if (orderElement.contains("*")) {
 163         // spin loc definition
 164         locOrder.addSpinLoc(orderElement);
 165       } else {
 166         // single element
 167         locOrder.put(orderElement);
 168       }
 169     }
 170
 171     // sanity check
 172     Set<String> spinLocSet = locOrder.getSpinLocSet();
 173     for (Iterator iterator = spinLocSet.iterator(); iterator.hasNext();) {
 174       String spinLoc = (String) iterator.next();
 175       if (!locOrder.containsKey(spinLoc)) {
 176         throw new Error("Spin location '" + spinLoc
 177             + "' is not defined in the default local variable lattice at " + cd.getSourceFileName());
 178       }
 179     }
 180   }
 181
 182   public Hashtable<ClassDescriptor, SSJavaLattice<String>> getCd2lattice() {
 183     return cd2lattice;
 184   }
 185
 186   public Hashtable<ClassDescriptor, MethodLattice<String>> getCd2methodDefault() {
 187     return cd2methodDefault;
 188   }
 189
 190   public Hashtable<MethodDescriptor, MethodLattice<String>> getMd2lattice() {
 191     return md2lattice;
 192   }
 193
 194   public SSJavaLattice<String> getClassLattice(ClassDescriptor cd) {
 195     return cd2lattice.get(cd);
 196   }
 197
 198 }