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 import IR.TypeUtil;
  14
  15 public class SSJavaAnalysis {
  16
  17   public static final String SSJAVA = "SSJAVA";
  18   public static final String LATTICE = "LATTICE";
  19   public static final String METHODDEFAULT = "METHODDEFAULT";
  20   public static final String THISLOC = "THISLOC";
  21   public static final String GLOBALLOC = "GLOBALLOC";
  22   public static final String RETURNLOC = "RETURNLOC";
  23   public static final String LOC = "LOC";
  24   public static final String DELTA = "DELTA";
  25   State state;
  26   TypeUtil tu;
  27   FlowDownCheck flowDownChecker;
  28   MethodAnnotationCheck methodAnnotationChecker;
  29
  30   // if a method has annotations, the mapping has true
  31   Hashtable<MethodDescriptor, Boolean> md2hasAnnotation;
  32
  33   // class -> field lattice
  34   Hashtable<ClassDescriptor, SSJavaLattice<String>> cd2lattice;
  35
  36   // class -> default local variable lattice
  37   Hashtable<ClassDescriptor, MethodLattice<String>> cd2methodDefault;
  38
  39   // method -> local variable lattice
  40   Hashtable<MethodDescriptor, MethodLattice<String>> md2lattice;
  41
  42   public SSJavaAnalysis(State state, TypeUtil tu) {
  43     this.state = state;
  44     this.tu = tu;
  45     this.cd2lattice = new Hashtable<ClassDescriptor, SSJavaLattice<String>>();
  46     this.cd2methodDefault = new Hashtable<ClassDescriptor, MethodLattice<String>>();
  47     this.md2lattice = new Hashtable<MethodDescriptor, MethodLattice<String>>();
  48     this.md2hasAnnotation = new Hashtable<MethodDescriptor, Boolean>();
  49   }
  50
  51   public void doCheck() {
  52     doMethodAnnotationCheck();
  53     parseLocationAnnotation();
  54     doFlowDownCheck();
  55     doLoopCheck();
  56     doSingleReferenceCheck();
  57   }
  58
  59   private void doMethodAnnotationCheck() {
  60     methodAnnotationChecker = new MethodAnnotationCheck(this, state, tu);
  61     methodAnnotationChecker.methodAnnoatationCheck();
  62     methodAnnotationChecker.methodAnnoataionInheritanceCheck();
  63   }
  64
  65   public void doFlowDownCheck() {
  66     flowDownChecker = new FlowDownCheck(this, state);
  67     flowDownChecker.flowDownCheck();
  68   }
  69
  70   public void doLoopCheck() {
  71     DefinitelyWrittenCheck checker = new DefinitelyWrittenCheck(state);
  72     checker.definitelyWrittenCheck();
  73   }
  74
  75   public void doSingleReferenceCheck() {
  76     SingleReferenceCheck checker = new SingleReferenceCheck(state);
  77     checker.singleReferenceCheck();
  78   }
  79
  80   private void parseLocationAnnotation() {
  81     Iterator it = state.getClassSymbolTable().getDescriptorsIterator();
  82     while (it.hasNext()) {
  83       ClassDescriptor cd = (ClassDescriptor) it.next();
  84       // parsing location hierarchy declaration for the class
  85       Vector<AnnotationDescriptor> classAnnotations = cd.getModifier().getAnnotations();
  86       for (int i = 0; i < classAnnotations.size(); i++) {
  87         AnnotationDescriptor an = classAnnotations.elementAt(i);
  88         String marker = an.getMarker();
  89         if (marker.equals(LATTICE)) {
  90           SSJavaLattice<String> locOrder =
  91               new SSJavaLattice<String>(SSJavaLattice.TOP, SSJavaLattice.BOTTOM);
  92           cd2lattice.put(cd, locOrder);
  93           parseClassLatticeDefinition(cd, an.getValue(), locOrder);
  94         } else if (marker.equals(METHODDEFAULT)) {
  95           MethodLattice<String> locOrder =
  96               new MethodLattice<String>(SSJavaLattice.TOP, SSJavaLattice.BOTTOM);
  97           cd2methodDefault.put(cd, locOrder);
  98           parseMethodLatticeDefinition(cd, an.getValue(), locOrder);
  99         }
 100       }
 101
 102       for (Iterator method_it = cd.getMethods(); method_it.hasNext();) {
 103         MethodDescriptor md = (MethodDescriptor) method_it.next();
 104         // parsing location hierarchy declaration for the method
 105
 106         if (hasAnnotation(md)) {
 107           Vector<AnnotationDescriptor> methodAnnotations = md.getModifiers().getAnnotations();
 108           if (methodAnnotations != null) {
 109             for (int i = 0; i < methodAnnotations.size(); i++) {
 110               AnnotationDescriptor an = methodAnnotations.elementAt(i);
 111               if (an.getMarker().equals(LATTICE)) {
 112                 // developer explicitly defines method lattice
 113                 MethodLattice<String> locOrder =
 114                     new MethodLattice<String>(SSJavaLattice.TOP, SSJavaLattice.BOTTOM);
 115                 md2lattice.put(md, locOrder);
 116                 parseMethodLatticeDefinition(cd, an.getValue(), locOrder);
 117               }
 118             }
 119           }
 120         }
 121
 122       }
 123
 124     }
 125   }
 126
 127   private void parseMethodLatticeDefinition(ClassDescriptor cd, String value,
 128       MethodLattice<String> locOrder) {
 129
 130     value = value.replaceAll(" ", ""); // remove all blank spaces
 131
 132     StringTokenizer tokenizer = new StringTokenizer(value, ",");
 133
 134     while (tokenizer.hasMoreTokens()) {
 135       String orderElement = tokenizer.nextToken();
 136       int idx = orderElement.indexOf("<");
 137       if (idx > 0) {// relative order element
 138         String lowerLoc = orderElement.substring(0, idx);
 139         String higherLoc = orderElement.substring(idx + 1);
 140         locOrder.put(higherLoc, lowerLoc);
 141         if (locOrder.isIntroducingCycle(higherLoc)) {
 142           throw new Error("Error: the order relation " + lowerLoc + " < " + higherLoc
 143               + " introduces a cycle.");
 144         }
 145       } else if (orderElement.startsWith(THISLOC + "=")) {
 146         String thisLoc = orderElement.substring(8);
 147         locOrder.setThisLoc(thisLoc);
 148       } else if (orderElement.startsWith(GLOBALLOC + "=")) {
 149         String globalLoc = orderElement.substring(10);
 150         locOrder.setGlobalLoc(globalLoc);
 151       } else if (orderElement.contains("*")) {
 152         // spin loc definition
 153         locOrder.addSpinLoc(orderElement.substring(0, orderElement.length() - 1));
 154       } else {
 155         // single element
 156         locOrder.put(orderElement);
 157       }
 158     }
 159
 160     // sanity checks
 161     if (locOrder.getThisLoc() != null && !locOrder.containsKey(locOrder.getThisLoc())) {
 162       throw new Error("Variable 'this' location '" + locOrder.getThisLoc()
 163           + "' is not defined in the default local variable lattice at " + cd.getSourceFileName());
 164     }
 165
 166     if (locOrder.getGlobalLoc() != null && !locOrder.containsKey(locOrder.getGlobalLoc())) {
 167       throw new Error("Variable global location '" + locOrder.getGlobalLoc()
 168           + "' is not defined in the default local variable lattice at " + cd.getSourceFileName());
 169     }
 170   }
 171
 172   private void parseClassLatticeDefinition(ClassDescriptor cd, String value,
 173       SSJavaLattice<String> locOrder) {
 174
 175     value = value.replaceAll(" ", ""); // remove all blank spaces
 176
 177     StringTokenizer tokenizer = new StringTokenizer(value, ",");
 178
 179     while (tokenizer.hasMoreTokens()) {
 180       String orderElement = tokenizer.nextToken();
 181       int idx = orderElement.indexOf("<");
 182
 183       if (idx > 0) {// relative order element
 184         String lowerLoc = orderElement.substring(0, idx);
 185         String higherLoc = orderElement.substring(idx + 1);
 186         locOrder.put(higherLoc, lowerLoc);
 187         if (locOrder.isIntroducingCycle(higherLoc)) {
 188           throw new Error("Error: the order relation " + lowerLoc + " < " + higherLoc
 189               + " introduces a cycle.");
 190         }
 191       } else if (orderElement.contains("*")) {
 192         // spin loc definition
 193         locOrder.addSpinLoc(orderElement.substring(0, orderElement.length() - 1));
 194       } else {
 195         // single element
 196         locOrder.put(orderElement);
 197       }
 198     }
 199
 200     // sanity check
 201     Set<String> spinLocSet = locOrder.getSpinLocSet();
 202     for (Iterator iterator = spinLocSet.iterator(); iterator.hasNext();) {
 203       String spinLoc = (String) iterator.next();
 204       if (!locOrder.containsKey(spinLoc)) {
 205         throw new Error("Spin location '" + spinLoc
 206             + "' is not defined in the default local variable lattice at " + cd.getSourceFileName());
 207       }
 208     }
 209   }
 210
 211   public Hashtable<ClassDescriptor, SSJavaLattice<String>> getCd2lattice() {
 212     return cd2lattice;
 213   }
 214
 215   public Hashtable<ClassDescriptor, MethodLattice<String>> getCd2methodDefault() {
 216     return cd2methodDefault;
 217   }
 218
 219   public Hashtable<MethodDescriptor, MethodLattice<String>> getMd2lattice() {
 220     return md2lattice;
 221   }
 222
 223   public SSJavaLattice<String> getClassLattice(ClassDescriptor cd) {
 224     return cd2lattice.get(cd);
 225   }
 226
 227   public MethodLattice<String> getMethodLattice(MethodDescriptor md) {
 228     if (md2lattice.containsKey(md)) {
 229       return md2lattice.get(md);
 230     } else {
 231       return cd2methodDefault.get(md.getClassDesc());
 232     }
 233   }
 234
 235   public boolean hasAnnotation(MethodDescriptor md) {
 236     return md2hasAnnotation.containsKey(md);
 237   }
 238
 239   public void putHasAnnotation(MethodDescriptor md) {
 240     md2hasAnnotation.put(md, new Boolean(true));
 241   }
 242
 243   public Hashtable<MethodDescriptor, Boolean> getMd2hasAnnotation() {
 244     return md2hasAnnotation;
 245   }
 246
 247 }