Robust/src/Analysis/SSJava/SSJavaAnalysis.java

   1 package Analysis.SSJava;
   2
   3 import java.util.HashSet;
   4 import java.util.Hashtable;
   5 import java.util.Iterator;
   6 import java.util.Set;
   7 import java.util.StringTokenizer;
   8 import java.util.Vector;
   9
  10 import Analysis.CallGraph.CallGraph;
  11 import Analysis.Loops.LoopOptimize;
  12 import Analysis.Loops.LoopTerminate;
  13 import IR.AnnotationDescriptor;
  14 import IR.ClassDescriptor;
  15 import IR.Descriptor;
  16 import IR.MethodDescriptor;
  17 import IR.State;
  18 import IR.TypeUtil;
  19 import IR.Flat.FlatMethod;
  20
  21 public class SSJavaAnalysis {
  22
  23   public static final String SSJAVA = "SSJAVA";
  24   public static final String LATTICE = "LATTICE";
  25   public static final String METHODDEFAULT = "METHODDEFAULT";
  26   public static final String THISLOC = "THISLOC";
  27   public static final String GLOBALLOC = "GLOBALLOC";
  28   public static final String RETURNLOC = "RETURNLOC";
  29   public static final String LOC = "LOC";
  30   public static final String DELTA = "DELTA";
  31   public static final String TERMINATE = "TERMINATE";
  32
  33   State state;
  34   TypeUtil tu;
  35   FlowDownCheck flowDownChecker;
  36   MethodAnnotationCheck methodAnnotationChecker;
  37
  38   // if a method has annotations, the mapping has true
  39   Set<MethodDescriptor> annotationRequireSet;
  40
  41   // class -> field lattice
  42   Hashtable<ClassDescriptor, SSJavaLattice<String>> cd2lattice;
  43
  44   // class -> default local variable lattice
  45   Hashtable<ClassDescriptor, MethodLattice<String>> cd2methodDefault;
  46
  47   // method -> local variable lattice
  48   Hashtable<MethodDescriptor, MethodLattice<String>> md2lattice;
  49
  50   // method set that does not have loop termination analysis
  51   Hashtable<MethodDescriptor, Integer> skipLoopTerminate;
  52
  53   CallGraph callgraph;
  54
  55   public SSJavaAnalysis(State state, TypeUtil tu, CallGraph callgraph) {
  56     this.state = state;
  57     this.tu = tu;
  58     this.callgraph = callgraph;
  59     this.cd2lattice = new Hashtable<ClassDescriptor, SSJavaLattice<String>>();
  60     this.cd2methodDefault = new Hashtable<ClassDescriptor, MethodLattice<String>>();
  61     this.md2lattice = new Hashtable<MethodDescriptor, MethodLattice<String>>();
  62     this.annotationRequireSet = new HashSet<MethodDescriptor>();
  63     this.skipLoopTerminate = new Hashtable<MethodDescriptor, Integer>();
  64   }
  65
  66   public void doCheck() {
  67     doMethodAnnotationCheck();
  68     if (state.SSJAVADEBUG) {
  69       debugPrint();
  70     }
  71     parseLocationAnnotation();
  72     doFlowDownCheck();
  73     doDefinitelyWrittenCheck();
  74     doSingleReferenceCheck();
  75   }
  76
  77   public void debugPrint() {
  78     System.out.println("SSJAVA: SSJava is checking the following methods:");
  79     for (Iterator<MethodDescriptor> iterator = annotationRequireSet.iterator(); iterator.hasNext();) {
  80       MethodDescriptor md = iterator.next();
  81       System.out.println("SSJAVA: " + md);
  82     }
  83   }
  84
  85   private void doMethodAnnotationCheck() {
  86     methodAnnotationChecker = new MethodAnnotationCheck(this, state, tu);
  87     methodAnnotationChecker.methodAnnoatationCheck();
  88     methodAnnotationChecker.methodAnnoataionInheritanceCheck();
  89   }
  90
  91   public void doFlowDownCheck() {
  92     flowDownChecker = new FlowDownCheck(this, state);
  93     flowDownChecker.flowDownCheck();
  94   }
  95
  96   public void doDefinitelyWrittenCheck() {
  97     DefinitelyWrittenCheck checker = new DefinitelyWrittenCheck(this, state);
  98     checker.definitelyWrittenCheck();
  99   }
 100
 101   public void doSingleReferenceCheck() {
 102     SingleReferenceCheck checker = new SingleReferenceCheck(this, state);
 103     checker.singleReferenceCheck();
 104   }
 105
 106   private void parseLocationAnnotation() {
 107     Iterator it = state.getClassSymbolTable().getDescriptorsIterator();
 108     while (it.hasNext()) {
 109       ClassDescriptor cd = (ClassDescriptor) it.next();
 110       // parsing location hierarchy declaration for the class
 111       Vector<AnnotationDescriptor> classAnnotations = cd.getModifier().getAnnotations();
 112       for (int i = 0; i < classAnnotations.size(); i++) {
 113         AnnotationDescriptor an = classAnnotations.elementAt(i);
 114         String marker = an.getMarker();
 115         if (marker.equals(LATTICE)) {
 116           SSJavaLattice<String> locOrder =
 117               new SSJavaLattice<String>(SSJavaLattice.TOP, SSJavaLattice.BOTTOM);
 118           cd2lattice.put(cd, locOrder);
 119           parseClassLatticeDefinition(cd, an.getValue(), locOrder);
 120         } else if (marker.equals(METHODDEFAULT)) {
 121           MethodLattice<String> locOrder =
 122               new MethodLattice<String>(SSJavaLattice.TOP, SSJavaLattice.BOTTOM);
 123           cd2methodDefault.put(cd, locOrder);
 124           parseMethodLatticeDefinition(cd, an.getValue(), locOrder);
 125         }
 126       }
 127
 128       for (Iterator method_it = cd.getMethods(); method_it.hasNext();) {
 129         MethodDescriptor md = (MethodDescriptor) method_it.next();
 130         // parsing location hierarchy declaration for the method
 131
 132         if (needTobeAnnotated(md)) {
 133           Vector<AnnotationDescriptor> methodAnnotations = md.getModifiers().getAnnotations();
 134           if (methodAnnotations != null) {
 135             for (int i = 0; i < methodAnnotations.size(); i++) {
 136               AnnotationDescriptor an = methodAnnotations.elementAt(i);
 137               if (an.getMarker().equals(LATTICE)) {
 138                 // developer explicitly defines method lattice
 139                 MethodLattice<String> locOrder =
 140                     new MethodLattice<String>(SSJavaLattice.TOP, SSJavaLattice.BOTTOM);
 141                 md2lattice.put(md, locOrder);
 142                 parseMethodLatticeDefinition(cd, an.getValue(), locOrder);
 143               } else if (an.getMarker().equals(TERMINATE)) {
 144                 // developer explicitly wants to skip loop termination analysis
 145                 String value = an.getValue();
 146                 int maxIteration = 0;
 147                 if (value != null) {
 148                   maxIteration = Integer.parseInt(value);
 149                 }
 150                 skipLoopTerminate.put(md, new Integer(maxIteration));
 151               }
 152             }
 153           }
 154         }
 155
 156       }
 157
 158     }
 159   }
 160
 161   private void parseMethodLatticeDefinition(ClassDescriptor cd, String value,
 162       MethodLattice<String> locOrder) {
 163
 164     value = value.replaceAll(" ", ""); // remove all blank spaces
 165
 166     StringTokenizer tokenizer = new StringTokenizer(value, ",");
 167
 168     while (tokenizer.hasMoreTokens()) {
 169       String orderElement = tokenizer.nextToken();
 170       int idx = orderElement.indexOf("<");
 171       if (idx > 0) {// relative order element
 172         String lowerLoc = orderElement.substring(0, idx);
 173         String higherLoc = orderElement.substring(idx + 1);
 174         locOrder.put(higherLoc, lowerLoc);
 175         if (locOrder.isIntroducingCycle(higherLoc)) {
 176           throw new Error("Error: the order relation " + lowerLoc + " < " + higherLoc
 177               + " introduces a cycle.");
 178         }
 179       } else if (orderElement.startsWith(THISLOC + "=")) {
 180         String thisLoc = orderElement.substring(8);
 181         locOrder.setThisLoc(thisLoc);
 182       } else if (orderElement.startsWith(GLOBALLOC + "=")) {
 183         String globalLoc = orderElement.substring(10);
 184         locOrder.setGlobalLoc(globalLoc);
 185       } else if (orderElement.contains("*")) {
 186         // spin loc definition
 187         locOrder.addSpinLoc(orderElement.substring(0, orderElement.length() - 1));
 188       } else {
 189         // single element
 190         locOrder.put(orderElement);
 191       }
 192     }
 193
 194     // sanity checks
 195     if (locOrder.getThisLoc() != null && !locOrder.containsKey(locOrder.getThisLoc())) {
 196       throw new Error("Variable 'this' location '" + locOrder.getThisLoc()
 197           + "' is not defined in the default local variable lattice at " + cd.getSourceFileName());
 198     }
 199
 200     if (locOrder.getGlobalLoc() != null && !locOrder.containsKey(locOrder.getGlobalLoc())) {
 201       throw new Error("Variable global location '" + locOrder.getGlobalLoc()
 202           + "' is not defined in the default local variable lattice at " + cd.getSourceFileName());
 203     }
 204   }
 205
 206   private void parseClassLatticeDefinition(ClassDescriptor cd, String value,
 207       SSJavaLattice<String> locOrder) {
 208
 209     value = value.replaceAll(" ", ""); // remove all blank spaces
 210
 211     StringTokenizer tokenizer = new StringTokenizer(value, ",");
 212
 213     while (tokenizer.hasMoreTokens()) {
 214       String orderElement = tokenizer.nextToken();
 215       int idx = orderElement.indexOf("<");
 216
 217       if (idx > 0) {// relative order element
 218         String lowerLoc = orderElement.substring(0, idx);
 219         String higherLoc = orderElement.substring(idx + 1);
 220         locOrder.put(higherLoc, lowerLoc);
 221         if (locOrder.isIntroducingCycle(higherLoc)) {
 222           throw new Error("Error: the order relation " + lowerLoc + " < " + higherLoc
 223               + " introduces a cycle.");
 224         }
 225       } else if (orderElement.contains("*")) {
 226         // spin loc definition
 227         locOrder.addSpinLoc(orderElement.substring(0, orderElement.length() - 1));
 228       } else {
 229         // single element
 230         locOrder.put(orderElement);
 231       }
 232     }
 233
 234     // sanity check
 235     Set<String> spinLocSet = locOrder.getSpinLocSet();
 236     for (Iterator iterator = spinLocSet.iterator(); iterator.hasNext();) {
 237       String spinLoc = (String) iterator.next();
 238       if (!locOrder.containsKey(spinLoc)) {
 239         throw new Error("Spin location '" + spinLoc
 240             + "' is not defined in the default local variable lattice at " + cd.getSourceFileName());
 241       }
 242     }
 243   }
 244
 245   public Hashtable<ClassDescriptor, SSJavaLattice<String>> getCd2lattice() {
 246     return cd2lattice;
 247   }
 248
 249   public Hashtable<ClassDescriptor, MethodLattice<String>> getCd2methodDefault() {
 250     return cd2methodDefault;
 251   }
 252
 253   public Hashtable<MethodDescriptor, MethodLattice<String>> getMd2lattice() {
 254     return md2lattice;
 255   }
 256
 257   public SSJavaLattice<String> getClassLattice(ClassDescriptor cd) {
 258     return cd2lattice.get(cd);
 259   }
 260
 261   public MethodLattice<String> getMethodLattice(MethodDescriptor md) {
 262     if (md2lattice.containsKey(md)) {
 263       return md2lattice.get(md);
 264     } else {
 265       return cd2methodDefault.get(md.getClassDesc());
 266     }
 267   }
 268
 269   public boolean needTobeAnnotated(MethodDescriptor md) {
 270     return annotationRequireSet.contains(md);
 271   }
 272
 273   public void addAnnotationRequire(MethodDescriptor md) {
 274     annotationRequireSet.add(md);
 275   }
 276
 277   public Set<MethodDescriptor> getAnnotationRequireSet() {
 278     return annotationRequireSet;
 279   }
 280
 281   public void doLoopTerminationCheck(LoopOptimize lo, FlatMethod fm) {
 282     LoopTerminate lt = new LoopTerminate();
 283     lt.terminateAnalysis(fm, lo.getLoopInvariant(fm));
 284   }
 285
 286   public void doLoopTerminationCheck(LoopOptimize lo) {
 287     LoopTerminate lt = new LoopTerminate();
 288     for (Iterator iterator = annotationRequireSet.iterator(); iterator.hasNext();) {
 289       MethodDescriptor md = (MethodDescriptor) iterator.next();
 290       if (!skipLoopTerminate.containsKey(md)) {
 291         FlatMethod fm = state.getMethodFlat(md);
 292         lt.terminateAnalysis(fm, lo.getLoopInvariant(fm));
 293       }
 294     }
 295
 296   }
 297
 298   public CallGraph getCallGraph() {
 299     return callgraph;
 300   }
 301
 302   public SSJavaLattice<String> getLattice(Descriptor d) {
 303
 304     if (d instanceof MethodDescriptor) {
 305       return getMethodLattice((MethodDescriptor) d);
 306     } else {
 307       return getClassLattice((ClassDescriptor) d);
 308     }
 309
 310   }
 311
 312   public boolean isSharedLocation(Location loc) {
 313
 314     SSJavaLattice<String> lattice = getLattice(loc.getDescriptor());
 315     return lattice.getSpinLocSet().contains(loc.getLocIdentifier());
 316
 317   }
 318 }