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: * MJI NativePeer class for java.lang.Object library abstraction
025: */
026: public class JPF_java_lang_Object {
027: public static int getClass(MJIEnv env, int objref) {
028: ClassInfo oci = env.getClassInfo(objref);
029:
030: return oci.getClassObjectRef();
031: }
032:
033: public static boolean $isDeterministic_wait__J(MJIEnv env,
034: int objref, long length) {
035: return (length == 0);
036: }
037:
038: public static boolean $isExecutable_wait__J(MJIEnv env, int objref,
039: long length) {
040: ThreadInfo ti = env.getThreadInfo();
041:
042: if (length != 0) {
043: if (env.getSystemState().random(2) == 0) {
044: return true;
045: }
046: }
047:
048: switch (ti.getStatus()) {
049: case ThreadInfo.RUNNING:
050: case ThreadInfo.SYNC_RUNNING:
051: return true;
052:
053: case ThreadInfo.NOTIFIED:
054: return env.canLock(objref);
055:
056: case ThreadInfo.INTERRUPTED:
057: return env.canLock(objref);
058:
059: default:
060:
061: return false;
062: }
063: }
064:
065: public static int clone(MJIEnv env, int objref) {
066: // <2do>
067: return -1;
068: }
069:
070: public static int hashCode(MJIEnv env, int objref) {
071: return (objref ^ 0xABCD);
072: }
073:
074: public static void notifyAll(MJIEnv env, int objref) {
075: env.notifyAll(objref);
076: }
077:
078: public static void registerNatives(MJIEnv env, int clsObjRef) {
079: // let go un-noticed
080: }
081:
082: public static void wait__J(MJIEnv env, int objref, long length) {
083: ThreadInfo ti = env.getThreadInfo();
084:
085: if (length != 0) {
086: if (env.getSystemState().random(2) == 0) {
087: return;
088: }
089: }
090:
091: switch (ti.getStatus()) {
092: case ThreadInfo.RUNNING:
093: case ThreadInfo.SYNC_RUNNING:
094:
095: env.wait(objref);
096: env.repeatInvocation();
097:
098: break;
099:
100: case ThreadInfo.NOTIFIED:
101: env.lockNotified(objref);
102:
103: break;
104:
105: case ThreadInfo.INTERRUPTED:
106: env.lockNotified(objref);
107: env.throwException("java.lang.InterruptedException");
108:
109: break;
110:
111: default:
112:
113: // <2do> - need to make this consistent
114: throw new JPFException("invalid thread state");
115: }
116: }
117:
118: public static final void notify(MJIEnv env, int objref) {
119: env.notify(objref);
120: }
121: }
|