1 package Analysis.SSJava;
3 import java.util.Hashtable;
4 import java.util.Iterator;
6 import java.util.StringTokenizer;
7 import java.util.Vector;
9 import IR.AnnotationDescriptor;
10 import IR.ClassDescriptor;
11 import IR.MethodDescriptor;
14 public class SSJavaAnalysis {
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";
23 FlowDownCheck flowDownChecker;
25 // class -> field lattice
26 Hashtable<ClassDescriptor, SSJavaLattice<String>> cd2lattice;
28 // class -> default local variable lattice
29 Hashtable<ClassDescriptor, MethodLattice<String>> cd2methodDefault;
31 // method -> local variable lattice
32 Hashtable<MethodDescriptor, MethodLattice<String>> md2lattice;
34 public SSJavaAnalysis(State state) {
36 cd2lattice = new Hashtable<ClassDescriptor, SSJavaLattice<String>>();
37 cd2methodDefault = new Hashtable<ClassDescriptor, MethodLattice<String>>();
38 md2lattice = new Hashtable<MethodDescriptor, MethodLattice<String>>();
41 public void doCheck() {
42 parseLocationAnnotation();
47 public void doFlowDownCheck() {
48 flowDownChecker = new FlowDownCheck(this, state);
49 flowDownChecker.flowDownCheck();
52 public void doLoopCheck() {
53 DefinitelyWrittenCheck checker = new DefinitelyWrittenCheck(state);
54 checker.definitelyWrittenCheck();
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);
76 if (!cd2lattice.containsKey(cd)) {
77 throw new Error("Class " + cd.getSymbol()
78 + " doesn't have any location hierarchy declaration at " + cd.getSourceFileName());
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);
98 private void parseMethodLatticeDefinition(ClassDescriptor cd, String value,
99 MethodLattice<String> locOrder) {
101 value = value.replaceAll(" ", ""); // remove all blank spaces
103 StringTokenizer tokenizer = new StringTokenizer(value, ",");
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.");
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);
127 locOrder.put(orderElement);
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());
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());
143 private void parseClassLatticeDefinition(ClassDescriptor cd, String value,
144 SSJavaLattice<String> locOrder) {
146 value = value.replaceAll(" ", ""); // remove all blank spaces
148 StringTokenizer tokenizer = new StringTokenizer(value, ",");
150 while (tokenizer.hasMoreTokens()) {
151 String orderElement = tokenizer.nextToken();
152 int idx = orderElement.indexOf("<");
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.");
162 } else if (orderElement.contains("*")) {
163 // spin loc definition
164 locOrder.addSpinLoc(orderElement);
167 locOrder.put(orderElement);
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());
182 public Hashtable<ClassDescriptor, SSJavaLattice<String>> getCd2lattice() {
186 public Hashtable<ClassDescriptor, MethodLattice<String>> getCd2methodDefault() {
187 return cd2methodDefault;
190 public Hashtable<MethodDescriptor, MethodLattice<String>> getMd2lattice() {
194 public SSJavaLattice<String> getClassLattice(ClassDescriptor cd) {
195 return cd2lattice.get(cd);