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 =
  68               new SSJavaLattice<String>(SSJavaLattice.TOP, SSJavaLattice.BOTTOM);
  69           cd2lattice.put(cd, locOrder);
  70           parseClassLatticeDefinition(cd, an.getValue(), locOrder);
  71         } else if (marker.equals(METHODDEFAULT)) {
  72           MethodLattice<String> locOrder =
  73               new MethodLattice<String>(SSJavaLattice.TOP, SSJavaLattice.BOTTOM);
  74           cd2methodDefault.put(cd, locOrder);
  75           parseMethodLatticeDefinition(cd, an.getValue(), locOrder);
  76         }
  77       }
  78       if (!cd2lattice.containsKey(cd)) {
  79         throw new Error("Class " + cd.getSymbol()
  80             + " doesn't have any location hierarchy declaration at " + cd.getSourceFileName());
  81       }
  82
  83       for (Iterator method_it = cd.getMethods(); method_it.hasNext();) {
  84         MethodDescriptor md = (MethodDescriptor) method_it.next();
  85         // parsing location hierarchy declaration for the method
  86         Vector<AnnotationDescriptor> methodAnnotations = md.getModifiers().getAnnotations();
  87         if (methodAnnotations != null) {
  88           for (int i = 0; i < methodAnnotations.size(); i++) {
  89             AnnotationDescriptor an = methodAnnotations.elementAt(i);
  90             if (an.getMarker().equals(LATTICE)) {
  91               MethodLattice<String> locOrder =
  92                   new MethodLattice<String>(SSJavaLattice.TOP, SSJavaLattice.BOTTOM);
  93               md2lattice.put(md, locOrder);
  94               parseMethodLatticeDefinition(cd, an.getValue(), locOrder);
  95             }
  96           }
  97         }
  98
  99       }
 100
 101     }
 102   }
 103
 104   private void parseMethodLatticeDefinition(ClassDescriptor cd, String value,
 105       MethodLattice<String> locOrder) {
 106
 107     value = value.replaceAll(" ", ""); // remove all blank spaces
 108
 109     StringTokenizer tokenizer = new StringTokenizer(value, ",");
 110
 111     while (tokenizer.hasMoreTokens()) {
 112       String orderElement = tokenizer.nextToken();
 113       int idx = orderElement.indexOf("<");
 114       if (idx > 0) {// relative order element
 115         String lowerLoc = orderElement.substring(0, idx);
 116         String higherLoc = orderElement.substring(idx + 1);
 117         locOrder.put(higherLoc, lowerLoc);
 118         if (locOrder.isIntroducingCycle(higherLoc)) {
 119           throw new Error("Error: the order relation " + lowerLoc + " < " + higherLoc
 120               + " introduces a cycle.");
 121         }
 122       } else if (orderElement.startsWith(THISLOC + "=")) {
 123         String thisLoc = orderElement.substring(8);
 124         locOrder.setThisLoc(thisLoc);
 125       } else if (orderElement.startsWith(GLOBALLOC + "=")) {
 126         String globalLoc = orderElement.substring(10);
 127         locOrder.setGlobalLoc(globalLoc);
 128       } else if (orderElement.contains("*")) {
 129         // spin loc definition
 130         locOrder.addSpinLoc(orderElement.substring(0,orderElement.length()-1));
 131       } else {
 132         // single element
 133         locOrder.put(orderElement);
 134       }
 135     }
 136
 137     // sanity checks
 138     if (locOrder.getThisLoc() != null && !locOrder.containsKey(locOrder.getThisLoc())) {
 139       throw new Error("Variable 'this' location '" + locOrder.getThisLoc()
 140           + "' is not defined in the default local variable lattice at " + cd.getSourceFileName());
 141     }
 142
 143     if (locOrder.getGlobalLoc() != null && !locOrder.containsKey(locOrder.getGlobalLoc())) {
 144       throw new Error("Variable global location '" + locOrder.getGlobalLoc()
 145           + "' is not defined in the default local variable lattice at " + cd.getSourceFileName());
 146     }
 147   }
 148
 149   private void parseClassLatticeDefinition(ClassDescriptor cd, String value,
 150       SSJavaLattice<String> locOrder) {
 151
 152     value = value.replaceAll(" ", ""); // remove all blank spaces
 153
 154     StringTokenizer tokenizer = new StringTokenizer(value, ",");
 155
 156     while (tokenizer.hasMoreTokens()) {
 157       String orderElement = tokenizer.nextToken();
 158       int idx = orderElement.indexOf("<");
 159
 160       if (idx > 0) {// relative order element
 161         String lowerLoc = orderElement.substring(0, idx);
 162         String higherLoc = orderElement.substring(idx + 1);
 163         locOrder.put(higherLoc, lowerLoc);
 164         if (locOrder.isIntroducingCycle(higherLoc)) {
 165           throw new Error("Error: the order relation " + lowerLoc + " < " + higherLoc
 166               + " introduces a cycle.");
 167         }
 168       } else if (orderElement.contains("*")) {
 169         // spin loc definition
 170         locOrder.addSpinLoc(orderElement.substring(0,orderElement.length()-1));
 171       } else {
 172         // single element
 173         locOrder.put(orderElement);
 174       }
 175     }
 176
 177     // sanity check
 178     Set<String> spinLocSet = locOrder.getSpinLocSet();
 179     for (Iterator iterator = spinLocSet.iterator(); iterator.hasNext();) {
 180       String spinLoc = (String) iterator.next();
 181       if (!locOrder.containsKey(spinLoc)) {
 182         throw new Error("Spin location '" + spinLoc
 183             + "' is not defined in the default local variable lattice at " + cd.getSourceFileName());
 184       }
 185     }
 186   }
 187
 188   public Hashtable<ClassDescriptor, SSJavaLattice<String>> getCd2lattice() {
 189     return cd2lattice;
 190   }
 191
 192   public Hashtable<ClassDescriptor, MethodLattice<String>> getCd2methodDefault() {
 193     return cd2methodDefault;
 194   }
 195
 196   public Hashtable<MethodDescriptor, MethodLattice<String>> getMd2lattice() {
 197     return md2lattice;
 198   }
 199
 200   public SSJavaLattice<String> getClassLattice(ClassDescriptor cd) {
 201     return cd2lattice.get(cd);
 202   }
 203
 204   public MethodLattice<String> getMethodLattice(MethodDescriptor md) {
 205     if (md2lattice.containsKey(md)) {
 206       return md2lattice.get(md);
 207     } else {
 208       return cd2methodDefault.get(md.getClassDesc());
 209     }
 210   }
 211
 212 }