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 gov.nasa.jpf.JPFException;
022:
023: /**
024: * MJIEnv is the call environment for "native" methods, i.e. code that
025: * is executed by the JVM, not by JPF.
026: *
027: * Since library abstractions are supposed to be "user code", we provide
028: * this class as a (little bit of) insulation towards the inner JPF workings.
029: *
030: * There are two APIs exported by this class. The public methods (like
031: * getStringObject) don't expose JPF internals, and can be used from non
032: * gov.nasa.jpf.jvm NativePeer classes). The rest is package-default
033: * and can be used to fiddle around as much as you like to (if you are in
034: * the ..jvm package)
035: *
036: * Note that MJIEnv objects are now per-ThreadInfo (i.e. the variable
037: * call envionment only includes MethodInfo and ClassInfo), which means
038: * MJIEnv can be used in non-native methods (but only carefully, if you
039: * don't need mi or ci)
040: */
041: public class MJIEnv {
042: public static final int NULL = -1;
043:
044: JVM vm;
045: ClassInfo ci;
046: MethodInfo mi;
047: ThreadInfo ti;
048: DynamicArea da;
049: StaticArea sa;
050: boolean repeat;
051: String exception;
052: String exceptionDetails;
053:
054: MJIEnv(ThreadInfo ti) {
055: this .ti = ti;
056:
057: // set those here so that we don't have an inconsistent state between
058: // creation of an MJI object and the first native method call in
059: // this thread (where any access to the da or sa would bomb)
060: vm = ti.getVM();
061: da = vm.getDynamicArea();
062: sa = vm.getStaticArea();
063: }
064:
065: public JVM getVM() {
066: return vm;
067: }
068:
069: public boolean isArray(int objref) {
070: return da.get(objref).isArray();
071: }
072:
073: public int getArrayLength(int objref) {
074: if (isArray(objref)) {
075: return da.get(objref).arrayLength();
076: } else {
077: throwException("java.lang.IllegalArgumentException");
078:
079: return 0;
080: }
081: }
082:
083: public String getArrayType(int objref) {
084: return da.get(objref).getArrayType();
085: }
086:
087: public int getArrayTypeSize(int objref) {
088: return Types.getTypeSize(getArrayType(objref));
089: }
090:
091: // the instance field setters
092: public void setBooleanField(int objref, String fname, boolean val) {
093: setIntField(objref, null, fname, Types.booleanToInt(val));
094: }
095:
096: public boolean getBooleanField(int objref, String fname) {
097: return Types.intToBoolean(getIntField(objref, null, fname));
098: }
099:
100: public void setByteField(int objref, String fname, byte val) {
101: setIntField(objref, null, fname, (int) val);
102: }
103:
104: public byte getByteField(int objref, String fname) {
105: return (byte) getIntField(objref, null, fname);
106: }
107:
108: public void setCharField(int objref, String fname, char val) {
109: setIntField(objref, null, fname, (int) val);
110: }
111:
112: public char getCharField(int objref, String fname) {
113: return (char) getIntField(objref, null, fname);
114: }
115:
116: public void setDoubleField(int objref, String fname, double val) {
117: setLongField(objref, null, fname, Types.doubleToLong(val));
118: }
119:
120: public double getDoubleField(int objref, String fname) {
121: return Types.longToDouble(getLongField(objref, null, fname));
122: }
123:
124: public void setFloatField(int objref, String fname, float val) {
125: setIntField(objref, null, fname, Types.floatToInt(val));
126: }
127:
128: public float getFloatField(int objref, String fname) {
129: return Types.intToFloat(getIntField(objref, null, fname));
130: }
131:
132: public void setByteArrayElement(int objref, int index, byte value) {
133: da.get(objref).setElement(index, value);
134: }
135:
136: public void setCharArrayElement(int objref, int index, char value) {
137: da.get(objref).setElement(index, value);
138: }
139:
140: public void setIntArrayElement(int objref, int index, int value) {
141: da.get(objref).setElement(index, value);
142: }
143:
144: public int getIntArrayElement(int objref, int index) {
145: return da.get(objref).getElement(index);
146: }
147:
148: public char getCharArrayElement(int objref, int index) {
149: return (char) da.get(objref).getElement(index);
150: }
151:
152: public void setIntField(int objref, String fname, int val) {
153: setIntField(objref, null, fname, val);
154: }
155:
156: // these two are the workhorses
157: public void setIntField(int objref, String refType, String fname,
158: int val) {
159: ElementInfo ei = da.get(objref);
160: ei.setIntField(fname, refType, val);
161: }
162:
163: public int getIntField(int objref, String fname) {
164: return getIntField(objref, null, fname);
165: }
166:
167: public int getIntField(int objref, String refType, String fname) {
168: ElementInfo ei = da.get(objref);
169:
170: return ei.getIntField(fname, refType);
171: }
172:
173: // these two are the workhorses
174: public void setReferenceField(int objref, String refType,
175: String fname, int val) {
176: ElementInfo ei = da.get(objref);
177: ei.setReferenceField(fname, refType, val);
178: }
179:
180: public void setReferenceField(int objref, String fname, int ref) {
181: setReferenceField(objref, null, fname, ref);
182: }
183:
184: public int getReferenceField(int objref, String fname) {
185: return getIntField(objref, null, fname);
186: }
187:
188: // the box object accessors (should probably test for the appropriate class)
189: public boolean getBooleanValue(int objref) {
190: return getBooleanField(objref, "value");
191: }
192:
193: public byte getByteValue(int objref) {
194: return getByteField(objref, "value");
195: }
196:
197: public char getCharValue(int objref) {
198: return getCharField(objref, "value");
199: }
200:
201: public short getShortValue(int objref) {
202: return getShortField(objref, "value");
203: }
204:
205: public int getIntValue(int objref) {
206: return getIntField(objref, "value");
207: }
208:
209: public long getLongValue(int objref) {
210: return getLongField(objref, "value");
211: }
212:
213: public float getFloatValue(int objref) {
214: return getFloatField(objref, "value");
215: }
216:
217: public double getDoubleValue(int objref) {
218: return getDoubleField(objref, "value");
219: }
220:
221: public void setLongArrayElement(int objref, int index, long value) {
222: da.get(objref).setLongElement(index, value);
223: }
224:
225: public long getLongArrayElement(int objref, int index) {
226: return da.get(objref).getLongElement(index);
227: }
228:
229: public void setLongField(int objref, String fname, long val) {
230: setLongField(objref, null, fname, val);
231: }
232:
233: public void setLongField(int objref, String refType, String fname,
234: long val) {
235: ElementInfo ei = da.get(objref);
236: ei.setLongField(fname, refType, val);
237: }
238:
239: public long getLongField(int objref, String fname) {
240: return getLongField(objref, null, fname);
241: }
242:
243: public long getLongField(int objref, String refType, String fname) {
244: ElementInfo ei = da.get(objref);
245:
246: return ei.getLongField(fname, refType);
247: }
248:
249: public void setReferenceArrayElement(int objref, int index, int eRef) {
250: da.get(objref).setElement(index, eRef);
251: }
252:
253: public int getReferenceArrayElement(int objref, int index) {
254: return da.get(objref).getElement(index);
255: }
256:
257: public void setShortField(int objref, String fname, short val) {
258: setIntField(objref, null, fname, (int) val);
259: }
260:
261: public short getShortField(int objref, String fname) {
262: return (short) getIntField(objref, null, fname);
263: }
264:
265: public String getTypeName(int objref) {
266: return da.get(objref).getType();
267: }
268:
269: public boolean isInstanceOf(int objref, String clsName) {
270: ClassInfo ci = getClassInfo(objref);
271: return ci.instanceOf(clsName);
272: }
273:
274: // the static field setters
275: public void setStaticBooleanField(String clsName, String fname,
276: boolean value) {
277: setStaticIntField(clsName, fname, Types.booleanToInt(value));
278: }
279:
280: public boolean getStaticBooleanField(String clsName, String fname) {
281: return Types.intToBoolean(getStaticIntField(clsName, fname));
282: }
283:
284: public void setStaticByteField(String clsName, String fname,
285: byte value) {
286: setStaticIntField(clsName, fname, (int) value);
287: }
288:
289: public byte getStaticByteField(String clsName, String fname) {
290: return (byte) getStaticIntField(clsName, fname);
291: }
292:
293: public void setStaticCharField(String clsName, String fname,
294: char value) {
295: setStaticIntField(clsName, fname, (int) value);
296: }
297:
298: public char getStaticCharField(String clsName, String fname) {
299: return (char) getStaticIntField(clsName, fname);
300: }
301:
302: public void setStaticDoubleField(String clsName, String fname,
303: double val) {
304: setStaticLongField(clsName, fname, Types.doubleToLong(val));
305: }
306:
307: public double getStaticDoubleField(String clsName, String fname) {
308: return Types.longToDouble(getStaticLongField(clsName, fname));
309: }
310:
311: public void setStaticFloatField(String clsName, String fname,
312: float value) {
313: setStaticIntField(clsName, fname, Types.floatToInt(value));
314: }
315:
316: public float getStaticFloatField(String clsName, String fname) {
317: return Types.intToFloat(getStaticIntField(clsName, fname));
318: }
319:
320: public void setStaticIntField(String clsName, String fname,
321: int value) {
322: ClassInfo ci = ClassInfo.getClassInfo(clsName);
323: sa.get(ci.getName()).setIntField(fname, null, value);
324: }
325:
326: public void setStaticIntField(int clsObjRef, String fname, int val) {
327: try {
328: ElementInfo cei = getClassElementInfo(clsObjRef);
329: cei.setIntField(fname, val);
330: } catch (Throwable x) {
331: throw new JPFException("set static field failed: "
332: + x.getMessage());
333: }
334: }
335:
336: public int getStaticIntField(String clsName, String fname) {
337: ClassInfo ci = ClassInfo.getClassInfo(clsName);
338: StaticElementInfo ei = sa.get(ci.getName());
339:
340: return ei.getIntField(fname, null);
341: }
342:
343: public void setStaticLongField(String clsName, String fname,
344: long value) {
345: ClassInfo ci = ClassInfo.getClassInfo(clsName);
346: sa.get(ci.getName()).setLongField(fname, value);
347: }
348:
349: public long getStaticLongField(String clsName, String fname) {
350: ClassInfo ci = ClassInfo.getClassInfo(clsName);
351: StaticElementInfo ei = sa.get(ci.getName());
352:
353: return ei.getLongField(fname, null);
354: }
355:
356: public void setStaticReferenceField(String clsName, String fname,
357: int objref) {
358: ClassInfo ci = ClassInfo.getClassInfo(clsName);
359:
360: // <2do> - we should REALLY check for type compatibility here
361: sa.get(ci.getName()).setReferenceField(fname, objref);
362: }
363:
364: public int getStaticObjectField(String clsName, String fname) {
365: return getStaticIntField(clsName, fname);
366: }
367:
368: public short getStaticShortField(String clsName, String fname) {
369: return (short) getStaticIntField(clsName, fname);
370: }
371:
372: /**
373: * turn JPF String object into a JVM String object
374: * (this is a method available for non gov..jvm NativePeer classes)
375: */
376: public String getStringObject(int objref) {
377: if (objref != -1) {
378: ElementInfo ei = getElementInfo(objref);
379: return ei.asString();
380: } else {
381: return null;
382: }
383: }
384:
385: public byte[] getByteArrayObject(int objref) {
386: ElementInfo ei = getElementInfo(objref);
387: byte[] a = ei.asByteArray();
388:
389: return a;
390: }
391:
392: public char[] getCharArrayObject(int objref) {
393: ElementInfo ei = getElementInfo(objref);
394: char[] a = ei.asCharArray();
395:
396: return a;
397: }
398:
399: public short[] getShortArrayObject(int objref) {
400: ElementInfo ei = getElementInfo(objref);
401: short[] a = ei.asShortArray();
402:
403: return a;
404: }
405:
406: public int[] getIntArrayObject(int objref) {
407: ElementInfo ei = getElementInfo(objref);
408: int[] a = ei.asIntArray();
409:
410: return a;
411: }
412:
413: public long[] getLongArrayObject(int objref) {
414: ElementInfo ei = getElementInfo(objref);
415: long[] a = ei.asLongArray();
416:
417: return a;
418: }
419:
420: public float[] getFloatArrayObject(int objref) {
421: ElementInfo ei = getElementInfo(objref);
422: float[] a = ei.asFloatArray();
423:
424: return a;
425: }
426:
427: public double[] getDoubleArrayObject(int objref) {
428: ElementInfo ei = getElementInfo(objref);
429: double[] a = ei.asDoubleArray();
430:
431: return a;
432: }
433:
434: public boolean[] getBooleanArrayObject(int objref) {
435: ElementInfo ei = getElementInfo(objref);
436: boolean[] a = ei.asBooleanArray();
437:
438: return a;
439: }
440:
441: public boolean canLock(int objref) {
442: ElementInfo ei = getElementInfo(objref);
443:
444: return ei.canLock(ti);
445: }
446:
447: public int newBooleanArray(int size) {
448: return da.newArray("Z", size, ti);
449: }
450:
451: public int newByteArray(int size) {
452: return da.newArray("B", size, ti);
453: }
454:
455: public int newCharArray(int size) {
456: return da.newArray("C", size, ti);
457: }
458:
459: public int newDoubleArray(int size) {
460: return da.newArray("D", size, ti);
461: }
462:
463: public int newFloatArray(int size) {
464: return da.newArray("F", size, ti);
465: }
466:
467: public int newIntArray(int size) {
468: return da.newArray("I", size, ti);
469: }
470:
471: public int newLongArray(int size) {
472: return da.newArray("J", size, ti);
473: }
474:
475: public int newObject(String clsName) {
476: // watch out - this is not initialized!!
477: ClassInfo ci = ClassInfo.getClassInfo(clsName);
478:
479: return da.newObject(ci, ti);
480: }
481:
482: public int newObjectArray(String clsName, int size) {
483: return da.newArray(clsName, size, ti);
484: }
485:
486: public int newShortArray(int size) {
487: return da.newArray("S", size, ti);
488: }
489:
490: public int newString(String s) {
491: return da.newString(s, ti);
492: }
493:
494: public int newString(int arrayRef) {
495: int r = NULL;
496: String t = getArrayType(arrayRef);
497: String s = null;
498:
499: if ("C".equals(t)) { // character array
500: char[] ca = getCharArrayObject(arrayRef);
501: s = new String(ca);
502: } else if ("B".equals(t)) { // byte array
503: byte[] ba = getByteArrayObject(arrayRef);
504: s = new String(ba);
505: }
506:
507: if (s == null) {
508: return NULL;
509: }
510:
511: return newString(s);
512: }
513:
514: public void notify(int objref) {
515: ElementInfo ei = getElementInfo(objref);
516:
517: if (!ei.isLockedBy(ti)) {
518: throwException("java.lang.IllegalMonitorStateException",
519: "un-synchronized notify");
520: return;
521: }
522:
523: ei.notifies();
524: }
525:
526: public void notifyAll(int objref) {
527: ElementInfo ei = getElementInfo(objref);
528:
529: if (!ei.isLockedBy(ti)) {
530: throwException("java.lang.IllegalMonitorStateException",
531: "un-synchronized notifyAll");
532: return;
533: }
534:
535: ei.notifiesAll();
536: }
537:
538: public void repeatInvocation() {
539: repeat = true;
540: }
541:
542: public void throwException(String classname) {
543: exception = Types.asTypeName(classname);
544: }
545:
546: public void throwException(String classname, String details) {
547: exception = Types.asTypeName(classname);
548: exceptionDetails = details;
549: }
550:
551: public void wait(int objref) {
552: ElementInfo ei = getElementInfo(objref);
553:
554: if (!ei.isLockedBy(ti)) {
555: throwException("java.lang.IllegalMonitorStateException",
556: "un-synchronized wait");
557: return;
558: }
559:
560: ei.wait(ti);
561: }
562:
563: void setCallEnvironment(MethodInfo mi) {
564: this .mi = mi;
565:
566: if (mi != null) {
567: ci = mi.getClassInfo();
568: } else {
569: //ci = null;
570: //mi = null;
571: }
572:
573: repeat = false;
574: exception = null;
575: exceptionDetails = null;
576: }
577:
578: void clearCallEnvironment() {
579: setCallEnvironment(null);
580: }
581:
582: ElementInfo getClassElementInfo(int clsObjRef) {
583: ElementInfo ei = da.get(clsObjRef);
584: int cref = ei.getIntField("cref", null);
585:
586: ElementInfo cei = sa.get(cref);
587:
588: return cei;
589: }
590:
591: ClassInfo getClassInfo() {
592: return ci;
593: }
594:
595: ClassInfo getClassInfo(int objref) {
596: ElementInfo ei = getElementInfo(objref);
597: return ei.getClassInfo();
598: }
599:
600: public String getClassName(int objref) {
601: return getClassInfo(objref).getName();
602: }
603:
604: DynamicArea getDynamicArea() {
605: return JVM.getVM().getDynamicArea();
606: }
607:
608: ElementInfo getElementInfo(int objref) {
609: return da.get(objref);
610: }
611:
612: int getStateId() {
613: return JVM.getVM().getStateId();
614: }
615:
616: String getException() {
617: return exception;
618: }
619:
620: String getExceptionDetails() {
621: return exceptionDetails;
622: }
623:
624: KernelState getKernelState() {
625: SystemState ss = getSystemState();
626:
627: return ss.ks;
628: }
629:
630: MethodInfo getMethodInfo() {
631: return mi;
632: }
633:
634: boolean getRepeat() {
635: return repeat;
636: }
637:
638: StaticArea getStaticArea() {
639: return JVM.getVM().getStaticArea();
640: }
641:
642: SystemState getSystemState() {
643: JVM vm = JVM.getVM();
644:
645: // <2do> - getSystemState() returns a dreaded interface
646: return vm.ss;
647: }
648:
649: ThreadInfo getThreadInfo() {
650: return ti;
651: }
652:
653: // <2do> - naming? not very intuitive
654: void lockNotified(int objref) {
655: ElementInfo ei = getElementInfo(objref);
656: ei.lockNotified(ti);
657: }
658: }
|