Robust/src/Analysis/SSJava/SSJavaAnalysis.java

   1 package Analysis.SSJava;
   2
   3 import java.io.BufferedWriter;
   4 import java.io.FileWriter;
   5 import java.io.IOException;
   6 import java.util.HashSet;
   7 import java.util.Hashtable;
   8 import java.util.Iterator;
   9 import java.util.Set;
  10 import java.util.StringTokenizer;
  11 import java.util.Vector;
  12
  13 import Analysis.CallGraph.CallGraph;
  14 import Analysis.Loops.LoopOptimize;
  15 import Analysis.Loops.LoopTerminate;
  16 import IR.AnnotationDescriptor;
  17 import IR.ClassDescriptor;
  18 import IR.Descriptor;
  19 import IR.MethodDescriptor;
  20 import IR.State;
  21 import IR.TypeUtil;
  22 import IR.Flat.BuildFlat;
  23 import IR.Flat.FlatMethod;
  24 import IR.Flat.TempDescriptor;
  25 import Util.Pair;
  26
  27 public class SSJavaAnalysis {
  28
  29   public static final String SSJAVA = "SSJAVA";
  30   public static final String LATTICE = "LATTICE";
  31   public static final String METHODDEFAULT = "METHODDEFAULT";
  32   public static final String THISLOC = "THISLOC";
  33   public static final String GLOBALLOC = "GLOBALLOC";
  34   public static final String RETURNLOC = "RETURNLOC";
  35   public static final String LOC = "LOC";
  36   public static final String DELTA = "DELTA";
  37   public static final String TERMINATE = "TERMINATE";
  38   public static final String DELEGATE = "DELEGATE";
  39
  40   State state;
  41   TypeUtil tu;
  42   FlowDownCheck flowDownChecker;
  43   MethodAnnotationCheck methodAnnotationChecker;
  44
  45   // set containing method requires to be annoated
  46   Set<MethodDescriptor> annotationRequireSet;
  47
  48   // class -> field lattice
  49   Hashtable<ClassDescriptor, SSJavaLattice<String>> cd2lattice;
  50
  51   // class -> default local variable lattice
  52   Hashtable<ClassDescriptor, MethodLattice<String>> cd2methodDefault;
  53
  54   // method -> local variable lattice
  55   Hashtable<MethodDescriptor, MethodLattice<String>> md2lattice;
  56
  57   // method set that does not want to have loop termination analysis
  58   Hashtable<MethodDescriptor, Integer> skipLoopTerminate;
  59
  60   // map shared location to its descriptors
  61   Hashtable<Location, Set<Descriptor>> mapSharedLocation2DescriptorSet;
  62
  63   // set containing a class that has at least one annoated method
  64   Set<ClassDescriptor> annotationRequireClassSet;
  65
  66   CallGraph callgraph;
  67
  68   public SSJavaAnalysis(State state, TypeUtil tu, CallGraph callgraph) {
  69     this.state = state;
  70     this.tu = tu;
  71     this.callgraph = callgraph;
  72     this.cd2lattice = new Hashtable<ClassDescriptor, SSJavaLattice<String>>();
  73     this.cd2methodDefault = new Hashtable<ClassDescriptor, MethodLattice<String>>();
  74     this.md2lattice = new Hashtable<MethodDescriptor, MethodLattice<String>>();
  75     this.annotationRequireSet = new HashSet<MethodDescriptor>();
  76     this.annotationRequireClassSet = new HashSet<ClassDescriptor>();
  77     this.skipLoopTerminate = new Hashtable<MethodDescriptor, Integer>();
  78     this.mapSharedLocation2DescriptorSet = new Hashtable<Location, Set<Descriptor>>();
  79   }
  80
  81   public void doCheck() {
  82     doLinearTypeCheck();
  83     doMethodAnnotationCheck();
  84     if (state.SSJAVADEBUG) {
  85       debugPrint();
  86     }
  87     parseLocationAnnotation();
  88     doFlowDownCheck();
  89     doDefinitelyWrittenCheck();
  90   }
  91
  92   private void doLinearTypeCheck() {
  93     LinearTypeCheck checker = new LinearTypeCheck(this, state);
  94     checker.linearTypeCheck();
  95   }
  96
  97   public void debugPrint() {
  98     System.out.println("SSJAVA: SSJava is checking the following methods:");
  99     for (Iterator<MethodDescriptor> iterator = annotationRequireSet.iterator(); iterator.hasNext();) {
 100       MethodDescriptor md = iterator.next();
 101       System.out.print(" " + md);
 102     }
 103     System.out.println();
 104   }
 105
 106   private void doMethodAnnotationCheck() {
 107     methodAnnotationChecker = new MethodAnnotationCheck(this, state, tu);
 108     methodAnnotationChecker.methodAnnoatationCheck();
 109     methodAnnotationChecker.methodAnnoataionInheritanceCheck();
 110   }
 111
 112   public void doFlowDownCheck() {
 113     flowDownChecker = new FlowDownCheck(this, state);
 114     flowDownChecker.flowDownCheck();
 115   }
 116
 117   public void doDefinitelyWrittenCheck() {
 118     DefinitelyWrittenCheck checker = new DefinitelyWrittenCheck(this, state);
 119     checker.definitelyWrittenCheck();
 120   }
 121
 122   private void parseLocationAnnotation() {
 123     Iterator it = state.getClassSymbolTable().getDescriptorsIterator();
 124     while (it.hasNext()) {
 125       ClassDescriptor cd = (ClassDescriptor) it.next();
 126       // parsing location hierarchy declaration for the class
 127       Vector<AnnotationDescriptor> classAnnotations = cd.getModifier().getAnnotations();
 128       for (int i = 0; i < classAnnotations.size(); i++) {
 129         AnnotationDescriptor an = classAnnotations.elementAt(i);
 130         String marker = an.getMarker();
 131         if (marker.equals(LATTICE)) {
 132           SSJavaLattice<String> locOrder =
 133               new SSJavaLattice<String>(SSJavaLattice.TOP, SSJavaLattice.BOTTOM);
 134           cd2lattice.put(cd, locOrder);
 135           parseClassLatticeDefinition(cd, an.getValue(), locOrder);
 136
 137           if (state.SSJAVADEBUG) {
 138             // generate lattice dot file
 139             writeLatticeDotFile(cd, locOrder);
 140           }
 141
 142         } else if (marker.equals(METHODDEFAULT)) {
 143           MethodLattice<String> locOrder =
 144               new MethodLattice<String>(SSJavaLattice.TOP, SSJavaLattice.BOTTOM);
 145           cd2methodDefault.put(cd, locOrder);
 146           parseMethodDefaultLatticeDefinition(cd, an.getValue(), locOrder);
 147         }
 148       }
 149
 150       for (Iterator method_it = cd.getMethods(); method_it.hasNext();) {
 151         MethodDescriptor md = (MethodDescriptor) method_it.next();
 152         // parsing location hierarchy declaration for the method
 153
 154         if (needTobeAnnotated(md)) {
 155           Vector<AnnotationDescriptor> methodAnnotations = md.getModifiers().getAnnotations();
 156           if (methodAnnotations != null) {
 157             for (int i = 0; i < methodAnnotations.size(); i++) {
 158               AnnotationDescriptor an = methodAnnotations.elementAt(i);
 159               if (an.getMarker().equals(LATTICE)) {
 160                 // developer explicitly defines method lattice
 161                 MethodLattice<String> locOrder =
 162                     new MethodLattice<String>(SSJavaLattice.TOP, SSJavaLattice.BOTTOM);
 163                 md2lattice.put(md, locOrder);
 164                 parseMethodDefaultLatticeDefinition(cd, an.getValue(), locOrder);
 165               } else if (an.getMarker().equals(TERMINATE)) {
 166                 // developer explicitly wants to skip loop termination analysis
 167                 String value = an.getValue();
 168                 int maxIteration = 0;
 169                 if (value != null) {
 170                   maxIteration = Integer.parseInt(value);
 171                 }
 172                 System.out.println("###md=" + md);
 173                 skipLoopTerminate.put(md, new Integer(maxIteration));
 174               }
 175             }
 176           }
 177         }
 178
 179       }
 180
 181     }
 182   }
 183
 184   private void writeLatticeDotFile(ClassDescriptor cd, SSJavaLattice<String> locOrder) {
 185
 186     String className = cd.getSymbol().replaceAll("[\\W_]", "");
 187
 188     Set<Pair<String, String>> pairSet = locOrder.getOrderingPairSet();
 189
 190     try {
 191       BufferedWriter bw = new BufferedWriter(new FileWriter(className + ".dot"));
 192
 193       bw.write("digraph " + className + " {\n");
 194
 195       for (Iterator iterator = pairSet.iterator(); iterator.hasNext();) {
 196         // pair is in the form of <higher, lower>
 197         Pair<String, String> pair = (Pair<String, String>) iterator.next();
 198
 199         String highLocId = pair.getFirst();
 200         if (locOrder.isSharedLoc(highLocId)) {
 201           highLocId = "\"" + highLocId + "*\"";
 202         }
 203         String lowLocId = pair.getSecond();
 204         if (locOrder.isSharedLoc(lowLocId)) {
 205           lowLocId = "\"" + lowLocId + "*\"";
 206         }
 207         bw.write(highLocId + " -> " + lowLocId + ";\n");
 208       }
 209       bw.write("}\n");
 210       bw.close();
 211
 212     } catch (IOException e) {
 213       e.printStackTrace();
 214     }
 215
 216   }
 217
 218   private void parseMethodDefaultLatticeDefinition(ClassDescriptor cd, String value,
 219       MethodLattice<String> locOrder) {
 220
 221     value = value.replaceAll(" ", ""); // remove all blank spaces
 222
 223     StringTokenizer tokenizer = new StringTokenizer(value, ",");
 224
 225     while (tokenizer.hasMoreTokens()) {
 226       String orderElement = tokenizer.nextToken();
 227       int idx = orderElement.indexOf("<");
 228       if (idx > 0) {// relative order element
 229         String lowerLoc = orderElement.substring(0, idx);
 230         String higherLoc = orderElement.substring(idx + 1);
 231         locOrder.put(higherLoc, lowerLoc);
 232         if (locOrder.isIntroducingCycle(higherLoc)) {
 233           throw new Error("Error: the order relation " + lowerLoc + " < " + higherLoc
 234               + " introduces a cycle.");
 235         }
 236       } else if (orderElement.startsWith(THISLOC + "=")) {
 237         String thisLoc = orderElement.substring(8);
 238         locOrder.setThisLoc(thisLoc);
 239       } else if (orderElement.startsWith(GLOBALLOC + "=")) {
 240         String globalLoc = orderElement.substring(10);
 241         locOrder.setGlobalLoc(globalLoc);
 242       } else if (orderElement.startsWith(RETURNLOC + "=")) {
 243         String returnLoc = orderElement.substring(10);
 244         locOrder.setReturnLoc(returnLoc);
 245       } else if (orderElement.endsWith("*")) {
 246         // spin loc definition
 247         locOrder.addSharedLoc(orderElement.substring(0, orderElement.length() - 1));
 248       } else {
 249         // single element
 250         locOrder.put(orderElement);
 251       }
 252     }
 253
 254     // sanity checks
 255     if (locOrder.getThisLoc() != null && !locOrder.containsKey(locOrder.getThisLoc())) {
 256       throw new Error("Variable 'this' location '" + locOrder.getThisLoc()
 257           + "' is not defined in the default local variable lattice at " + cd.getSourceFileName());
 258     }
 259
 260     if (locOrder.getGlobalLoc() != null && !locOrder.containsKey(locOrder.getGlobalLoc())) {
 261       throw new Error("Variable global location '" + locOrder.getGlobalLoc()
 262           + "' is not defined in the default local variable lattice at " + cd.getSourceFileName());
 263     }
 264   }
 265
 266   private void parseClassLatticeDefinition(ClassDescriptor cd, String value,
 267       SSJavaLattice<String> locOrder) {
 268
 269     value = value.replaceAll(" ", ""); // remove all blank spaces
 270
 271     StringTokenizer tokenizer = new StringTokenizer(value, ",");
 272
 273     while (tokenizer.hasMoreTokens()) {
 274       String orderElement = tokenizer.nextToken();
 275       int idx = orderElement.indexOf("<");
 276
 277       if (idx > 0) {// relative order element
 278         String lowerLoc = orderElement.substring(0, idx);
 279         String higherLoc = orderElement.substring(idx + 1);
 280         locOrder.put(higherLoc, lowerLoc);
 281         if (locOrder.isIntroducingCycle(higherLoc)) {
 282           throw new Error("Error: the order relation " + lowerLoc + " < " + higherLoc
 283               + " introduces a cycle.");
 284         }
 285       } else if (orderElement.contains("*")) {
 286         // spin loc definition
 287         locOrder.addSharedLoc(orderElement.substring(0, orderElement.length() - 1));
 288       } else {
 289         // single element
 290         locOrder.put(orderElement);
 291       }
 292     }
 293
 294     // sanity check
 295     Set<String> spinLocSet = locOrder.getSharedLocSet();
 296     for (Iterator iterator = spinLocSet.iterator(); iterator.hasNext();) {
 297       String spinLoc = (String) iterator.next();
 298       if (!locOrder.containsKey(spinLoc)) {
 299         throw new Error("Spin location '" + spinLoc
 300             + "' is not defined in the default local variable lattice at " + cd.getSourceFileName());
 301       }
 302     }
 303   }
 304
 305   public Hashtable<ClassDescriptor, SSJavaLattice<String>> getCd2lattice() {
 306     return cd2lattice;
 307   }
 308
 309   public Hashtable<ClassDescriptor, MethodLattice<String>> getCd2methodDefault() {
 310     return cd2methodDefault;
 311   }
 312
 313   public Hashtable<MethodDescriptor, MethodLattice<String>> getMd2lattice() {
 314     return md2lattice;
 315   }
 316
 317   public SSJavaLattice<String> getClassLattice(ClassDescriptor cd) {
 318     return cd2lattice.get(cd);
 319   }
 320
 321   public MethodLattice<String> getMethodDefaultLattice(ClassDescriptor cd) {
 322     return cd2methodDefault.get(cd);
 323   }
 324
 325   public MethodLattice<String> getMethodLattice(MethodDescriptor md) {
 326     if (md2lattice.containsKey(md)) {
 327       return md2lattice.get(md);
 328     } else {
 329       return cd2methodDefault.get(md.getClassDesc());
 330     }
 331   }
 332
 333   public boolean needTobeAnnotated(MethodDescriptor md) {
 334     return annotationRequireSet.contains(md);
 335   }
 336
 337   public boolean needToBeAnnoated(ClassDescriptor cd) {
 338     return annotationRequireClassSet.contains(cd);
 339   }
 340
 341   public void addAnnotationRequire(ClassDescriptor cd) {
 342     annotationRequireClassSet.add(cd);
 343   }
 344
 345   public void addAnnotationRequire(MethodDescriptor md) {
 346
 347     ClassDescriptor cd = md.getClassDesc();
 348     // if a method requires to be annotated, class containg that method also
 349     // requires to be annotated
 350     annotationRequireClassSet.add(cd);
 351     annotationRequireSet.add(md);
 352   }
 353
 354   public Set<MethodDescriptor> getAnnotationRequireSet() {
 355     return annotationRequireSet;
 356   }
 357
 358   public void doLoopTerminationCheck(LoopOptimize lo, FlatMethod fm) {
 359     LoopTerminate lt = new LoopTerminate();
 360     if (needTobeAnnotated(fm.getMethod())) {
 361       lt.terminateAnalysis(fm, lo.getLoopInvariant(fm));
 362     }
 363   }
 364
 365   public void doLoopTerminationCheck(LoopOptimize lo) {
 366     LoopTerminate lt = new LoopTerminate();
 367     for (Iterator iterator = annotationRequireSet.iterator(); iterator.hasNext();) {
 368       MethodDescriptor md = (MethodDescriptor) iterator.next();
 369       if (!skipLoopTerminate.containsKey(md)) {
 370         FlatMethod fm = state.getMethodFlat(md);
 371         lt.terminateAnalysis(fm, lo.getLoopInvariant(fm));
 372       }
 373     }
 374
 375   }
 376
 377   public CallGraph getCallGraph() {
 378     return callgraph;
 379   }
 380
 381   public SSJavaLattice<String> getLattice(Descriptor d) {
 382
 383     if (d instanceof MethodDescriptor) {
 384       return getMethodLattice((MethodDescriptor) d);
 385     } else {
 386       return getClassLattice((ClassDescriptor) d);
 387     }
 388
 389   }
 390
 391   public boolean isSharedLocation(Location loc) {
 392     SSJavaLattice<String> lattice = getLattice(loc.getDescriptor());
 393     return lattice.getSharedLocSet().contains(loc.getLocIdentifier());
 394   }
 395
 396   public void mapSharedLocation2Descriptor(Location loc, Descriptor d) {
 397     Set<Descriptor> set = mapSharedLocation2DescriptorSet.get(loc);
 398     if (set == null) {
 399       set = new HashSet<Descriptor>();
 400       mapSharedLocation2DescriptorSet.put(loc, set);
 401     }
 402     set.add(d);
 403   }
 404
 405 }