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.bytecode;
020:
021: import gov.nasa.jpf.JPFException;
022: import gov.nasa.jpf.jvm.ClassInfo;
023: import gov.nasa.jpf.jvm.JVM;
024: import gov.nasa.jpf.jvm.KernelState;
025: import gov.nasa.jpf.jvm.MethodInfo;
026: import gov.nasa.jpf.jvm.SystemState;
027: import gov.nasa.jpf.jvm.ThreadInfo;
028: import gov.nasa.jpf.util.Debug;
029:
030: import java.util.ArrayList;
031: import java.util.List;
032:
033: import org.apache.bcel.classfile.ConstantPool;
034: import org.apache.bcel.generic.InstructionHandle;
035:
036: /**
037: * common root of all JPF bytecode instruction classes
038: */
039: public abstract class Instruction {
040: protected static List Unimplemented = new ArrayList();
041: protected int position; // accumulated position (prev pos + prev bc-length)
042: protected int offset; // consecutive index of instruction
043:
044: /**
045: * NOTE - this is the method this instruction belongs to!
046: * <2do> pcm - Seems nobody has noticed this gets shadowed all over the place
047: * by local vars with a different meaning (InvokeInstruction)
048: */
049: protected MethodInfo mi;
050: protected String asString;
051: protected boolean isObservable;
052:
053: abstract public int getByteCode();
054:
055: // to allow a classname and methodname context for each instruction
056: public void setContext(String className, String methodName,
057: int lineNumber, int offset) {
058: }
059:
060: public boolean isFirstInstruction() {
061: return (offset == 0);
062: }
063:
064: /**
065: * answer if this is a potential loop closing jump
066: */
067: public boolean isBackJump() {
068: return false;
069: }
070:
071: public boolean isDeterministic(SystemState ss, KernelState ks,
072: ThreadInfo ti) {
073: return true;
074: }
075:
076: public boolean isExecutable(SystemState ss, KernelState ks,
077: ThreadInfo th) {
078: return true;
079: }
080:
081: public MethodInfo getMethod() {
082: return mi;
083: }
084:
085: public Instruction getNext() {
086: return mi.getInstruction(offset + 1);
087: }
088:
089: public void setObservable() {
090: isObservable = true;
091: }
092:
093: public boolean isObservable() {
094: if (!isObservable) {
095: Instruction prev = getPrev();
096:
097: if (prev != null) {
098: if (prev instanceof INVOKESTATIC) {
099: INVOKESTATIC invoke = (INVOKESTATIC) prev;
100: isObservable |= (invoke.cname
101: .equals("gov.nasa.jpf.jvm.Verify") && invoke.mname
102: .equals("assertTrue(Z)V"));
103: }
104: }
105: }
106:
107: return isObservable;
108: }
109:
110: public int getOffset() {
111: return offset;
112: }
113:
114: public int getPosition() {
115: return position;
116: }
117:
118: public Instruction getPrev() {
119: if (offset > 0) {
120: return mi.getInstruction(offset - 1);
121: } else {
122: return null;
123: }
124: }
125:
126: //SUNYSB
127: public boolean isVisible(SystemState ss, KernelState ks,
128: ThreadInfo th) {
129: return false;
130: }
131:
132: public boolean isSchedulingRelevant(SystemState ss, KernelState ks,
133: ThreadInfo ti) {
134: return false;
135: }
136:
137: public abstract Instruction execute(SystemState ss, KernelState ks,
138: ThreadInfo th);
139:
140: public static Instruction create(InstructionHandle h, int o,
141: MethodInfo m, ConstantPool cp) {
142: Instruction i = null;
143: String name = null;
144:
145: try {
146: name = h.getInstruction().getClass().getName();
147:
148: if (!name.startsWith("org.apache.bcel.generic.")) {
149: throw new JPFException("not a BCEL instruction type: "
150: + name);
151: }
152:
153: name = "gov.nasa.jpf.jvm.bytecode." + name.substring(24);
154: Class clazz = Class.forName(name);
155:
156: i = (gov.nasa.jpf.jvm.bytecode.Instruction) clazz
157: .newInstance();
158: i.init(h, o, m, cp);
159: } catch (ClassNotFoundException e) {
160: if (!Unimplemented.contains(name)) {
161: Unimplemented.add(name);
162: Debug.println(Debug.WARNING,
163: "warning: unimplemented bytecode instruction: "
164: + name.substring(34));
165: }
166: } catch (Exception e) {
167: e.printStackTrace();
168: throw new JPFException("creation of instruction "
169: + name.substring(34) + " failed");
170: }
171:
172: return i;
173: }
174:
175: public boolean Methodexamine(ThreadInfo th) {
176: return false; // default: next ins is not already covered method
177: }
178:
179: public boolean examine(SystemState ss, KernelState ks, ThreadInfo th) {
180: return false;
181: }
182:
183: public boolean examineAbstraction(SystemState ss, KernelState ks,
184: ThreadInfo th) {
185: return false;
186: }
187:
188: public String toString() {
189: return asString;
190: }
191:
192: public String getMnemonic() {
193: String s = getClass().getName();
194: return s.substring(26); // gov.nasa.jpf.jvm.bytecode package
195: }
196:
197: public String getSourceLocation() {
198: ClassInfo ci = mi.getClassInfo();
199: int line = mi.getLineNumber(this );
200: String file = ci.getSourceFileName();
201:
202: String s = ci.getName() + '.' + mi.getFullName() + " at ";
203:
204: if (file != null) {
205: s += file;
206: s += ':';
207: s += line;
208: } else {
209: s += "pc ";
210: s += position;
211: }
212:
213: return s;
214: }
215:
216: //SUNYSB
217: protected abstract void setPeer(
218: org.apache.bcel.generic.Instruction i, ConstantPool cp);
219:
220: protected void init(InstructionHandle h, int o, MethodInfo m,
221: ConstantPool cp) {
222: position = h.getPosition();
223: offset = o;
224: mi = m;
225: asString = h.getInstruction().toString(cp);
226: setPeer(h.getInstruction(), cp);
227: isObservable = JVM.observablePositions.contains(mi
228: .getCompleteName()
229: + ":" + position);
230: }
231:
232: /**
233: * this is returning the next Instruction to execute, to be called after
234: * we executed ourselves.
235: *
236: * Be aware of that we might have had exceptions caused by our execution,
237: * i.e. we can't simply assume it's the next insn following us (we have to
238: * acquire the 'current' insn after our exec from the ThreadInfo).
239: *
240: * To make it even more interesting, the ThreadInfo might return null because
241: * we might have run into a System.exit, which purges all stacks.
242: * It's questionable if it's the right way to handle this by just returning
243: * our own successor, and rely on ThreadInfo.executeXXMethod to catch
244: * this, but it seems to be the smallest change
245: *
246: * <?> pcm - this is hackish control in case of System.exit
247: */
248: Instruction getNext(ThreadInfo th) {
249: Instruction insn = th.getPC();
250:
251: if (insn == null) {
252: // could be all purged (System.exit)
253: insn = this;
254: }
255:
256: return insn.getNext();
257: }
258: }
|