001: //
002: // Copyright (C) 2005 United States Government as represented by the
003: // Administrator of the National Aeronautics and Space Administration
004: // (NASA). All Rights Reserved.
005: //
006: // This software is distributed under the NASA Open Source Agreement
007: // (NOSA), version 1.3. The NOSA has been approved by the Open Source
008: // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
009: // directory tree for the complete NOSA document.
010: //
011: // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
012: // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
013: // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
014: // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
015: // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
016: // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
017: // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
018: //
019: package gov.nasa.jpf.jvm;
020:
021: import org.apache.bcel.classfile.JavaClass;
022: import org.apache.bcel.classfile.Method;
023: import org.apache.bcel.classfile.Field;
024:
025: /**
026: * default Attributor implementation to set method and fiel attributes
027: * at class load time. Note this is critical functionality, esp.
028: * with respect to threading
029: */
030: public class DefaultAttributor implements Attributor {
031:
032: // <2do> we should turn atomicity and scheduling relevance into general
033: // MethodInfo attributes, to keep it consistent with object and field attrs
034:
035: public boolean isMethodAtomic(JavaClass jc, Method mth,
036: String uniqueName) {
037:
038: // per default, we set all standard library methods atomic
039: // (aren't we nicely optimistic, are we?)
040: if (jc.getPackageName().startsWith("java.")) {
041: String clsName = jc.getClassName();
042:
043: // except of the signal methods, of course
044: if (clsName.equals("java.lang.Object")) {
045: if (uniqueName.startsWith("wait(")
046: || uniqueName.equals("notify()")) {
047: return false;
048: }
049: } else if (clsName.equals("java.lang.Thread")) {
050: if (uniqueName.equals("join()")) {
051: return false;
052: }
053: }
054:
055: return true;
056: }
057:
058: return false;
059: }
060:
061: /**
062: * is calling a certain method in the context of multiple runnable threads
063: * scheduling relevant (i.e. has to be considered as a step boundary
064: */
065: public int getSchedulingRelevance(JavaClass jc, Method mth,
066: String uniqueName) {
067: String cls = jc.getClassName();
068:
069: if (cls.equals("java.lang.Thread")) {
070: if (uniqueName.equals("start()")) {
071: // <2do> - this is not required if we re-compute reachability after
072: // a thread becomes runnable, so that subsequent field/lock accesses
073: // depending on the number of runnables will break correctly. Check
074: // what other insns (beyond ref-field assignment) might be in the same
075: // category (on-the-fly remark w/o saving the state)
076:
077: //return MethodInfo.SR_ALWAYS;
078: } else if (uniqueName.equals("yield()")
079: || uniqueName.equals("sleep(J)")
080: || uniqueName.equals("join()")) {
081: return MethodInfo.SR_RUNNABLES;
082: }
083: } else if (cls.equals("java.lang.Object")) {
084: if ( /*uniqueName.equals("wait()") || */
085: uniqueName.equals("wait(J)")
086: || uniqueName.equals("notify()")) {
087: return MethodInfo.SR_RUNNABLES;
088: }
089: } else if (cls.equals("gov.nasa.jpf.jvm.Verify")) {
090: // note that the Verify.randoms do not fall into this category,
091: // since they are always step boundaries
092: if (uniqueName.equals("beginAtomic()")
093: || uniqueName.equals("endAtomic()")) {
094: //return MethodInfo.SR_ALWAYS;
095: }
096: }
097:
098: if (mth.isSynchronized()) {
099: return MethodInfo.SR_SYNC;
100: }
101:
102: return MethodInfo.SR_NEVER;
103: }
104:
105: /**
106: * answer the type based object attributes for this class. See
107: * ElementInfo for valid choices
108: */
109: public int getObjectAttributes(JavaClass jc) {
110: String clsName = jc.getClassName();
111:
112: // very very simplistic for now
113: if (clsName.equals("java.lang.String")
114: || clsName.equals("java.lang.Integer")
115: || clsName.equals("java.lang.Long")
116: || clsName.equals("java.lang.Class")
117: /* ..and a lot more.. */
118: ) {
119: return ElementInfo.ATTR_IMMUTABLE;
120: } else {
121: return 0;
122: }
123: }
124:
125: public int getFieldAttributes(JavaClass jc, Field f) {
126: String clsName = jc.getClassName();
127: String fName = f.getName();
128:
129: if (clsName.equals("java.lang.ThreadGroup")) {
130: if (fName.equals("threads")) {
131: return ElementInfo.ATTR_PROP_MASK
132: & ~ElementInfo.ATTR_TSHARED;
133: }
134: }
135:
136: return ElementInfo.ATTR_PROP_MASK;
137: }
138: }
|