KickJava   Java API By Example, From Geeks To Geeks.

Java > Open Source Codes > gov > nasa > jpf > jvm > MJIEnv


1 //
2
// Copyright (C) 2005 United States Government as represented by the
3
// Administrator of the National Aeronautics and Space Administration
4
// (NASA). All Rights Reserved.
5
//
6
// This software is distributed under the NASA Open Source Agreement
7
// (NOSA), version 1.3. The NOSA has been approved by the Open Source
8
// Initiative. See the file NOSA-1.3-JPF at the top of the distribution
9
// directory tree for the complete NOSA document.
10
//
11
// THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
12
// KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
13
// LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
14
// SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
15
// A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
16
// THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
17
// DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
18
//
19
package gov.nasa.jpf.jvm;
20
21 import gov.nasa.jpf.JPFException;
22
23
24 /**
25  * MJIEnv is the call environment for "native" methods, i.e. code that
26  * is executed by the JVM, not by JPF.
27  *
28  * Since library abstractions are supposed to be "user code", we provide
29  * this class as a (little bit of) insulation towards the inner JPF workings.
30  *
31  * There are two APIs exported by this class. The public methods (like
32  * getStringObject) don't expose JPF internals, and can be used from non
33  * gov.nasa.jpf.jvm NativePeer classes). The rest is package-default
34  * and can be used to fiddle around as much as you like to (if you are in
35  * the ..jvm package)
36  *
37  * Note that MJIEnv objects are now per-ThreadInfo (i.e. the variable
38  * call envionment only includes MethodInfo and ClassInfo), which means
39  * MJIEnv can be used in non-native methods (but only carefully, if you
40  * don't need mi or ci)
41  */

42 public class MJIEnv {
43   public static final int NULL = -1;
44   
45   JVM vm;
46   ClassInfo ci;
47   MethodInfo mi;
48   ThreadInfo ti;
49   DynamicArea da;
50   StaticArea sa;
51   boolean repeat;
52   String JavaDoc exception;
53   String JavaDoc exceptionDetails;
54
55   MJIEnv (ThreadInfo ti) {
56     this.ti = ti;
57     
58     // set those here so that we don't have an inconsistent state between
59
// creation of an MJI object and the first native method call in
60
// this thread (where any access to the da or sa would bomb)
61
vm = ti.getVM();
62     da = vm.getDynamicArea();
63     sa = vm.getStaticArea();
64   }
65
66   public JVM getVM () {
67     return vm;
68   }
69   
70   public boolean isArray (int objref) {
71     return da.get(objref).isArray();
72   }
73
74   public int getArrayLength (int objref) {
75     if (isArray(objref)) {
76       return da.get(objref).arrayLength();
77     } else {
78       throwException("java.lang.IllegalArgumentException");
79
80       return 0;
81     }
82   }
83
84   public String JavaDoc getArrayType (int objref) {
85     return da.get(objref).getArrayType();
86   }
87
88   public int getArrayTypeSize (int objref) {
89     return Types.getTypeSize(getArrayType(objref));
90   }
91
92   // the instance field setters
93
public void setBooleanField (int objref, String JavaDoc fname, boolean val) {
94     setIntField(objref, null, fname, Types.booleanToInt(val));
95   }
96
97   public boolean getBooleanField (int objref, String JavaDoc fname) {
98     return Types.intToBoolean(getIntField(objref, null, fname));
99   }
100
101   public void setByteField (int objref, String JavaDoc fname, byte val) {
102     setIntField(objref, null, fname, (int) val);
103   }
104
105   public byte getByteField (int objref, String JavaDoc fname) {
106     return (byte) getIntField(objref, null, fname);
107   }
108
109   public void setCharField (int objref, String JavaDoc fname, char val) {
110     setIntField(objref, null, fname, (int) val);
111   }
112
113   public char getCharField (int objref, String JavaDoc fname) {
114     return (char) getIntField(objref, null, fname);
115   }
116
117   public void setDoubleField (int objref, String JavaDoc fname, double val) {
118     setLongField(objref, null, fname, Types.doubleToLong(val));
119   }
120
121   public double getDoubleField (int objref, String JavaDoc fname) {
122     return Types.longToDouble(getLongField(objref, null, fname));
123   }
124
125   public void setFloatField (int objref, String JavaDoc fname, float val) {
126     setIntField(objref, null, fname, Types.floatToInt(val));
127   }
128
129   public float getFloatField (int objref, String JavaDoc fname) {
130     return Types.intToFloat(getIntField(objref, null, fname));
131   }
132
133   public void setByteArrayElement (int objref, int index, byte value) {
134     da.get(objref).setElement(index, value);
135   }
136
137   public void setCharArrayElement (int objref, int index, char value) {
138     da.get(objref).setElement(index, value);
139   }
140   
141   public void setIntArrayElement (int objref, int index, int value) {
142     da.get(objref).setElement(index, value);
143   }
144
145   public int getIntArrayElement (int objref, int index) {
146     return da.get(objref).getElement(index);
147   }
148
149   public char getCharArrayElement (int objref, int index) {
150     return (char) da.get(objref).getElement(index);
151   }
152   
153   public void setIntField (int objref, String JavaDoc fname, int val) {
154     setIntField(objref, null, fname, val);
155   }
156
157   // these two are the workhorses
158
public void setIntField (int objref, String JavaDoc refType, String JavaDoc fname, int val) {
159     ElementInfo ei = da.get(objref);
160     ei.setIntField(fname, refType, val);
161   }
162
163   public int getIntField (int objref, String JavaDoc fname) {
164     return getIntField(objref, null, fname);
165   }
166
167   public int getIntField (int objref, String JavaDoc refType, String JavaDoc 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 JavaDoc refType, String JavaDoc fname, int val) {
175     ElementInfo ei = da.get(objref);
176     ei.setReferenceField(fname, refType, val);
177   }
178   
179   public void setReferenceField (int objref, String JavaDoc fname, int ref) {
180     setReferenceField(objref, null, fname, ref);
181   }
182
183   public int getReferenceField (int objref, String JavaDoc fname) {
184     return getIntField(objref, null, fname);
185   }
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   
222   public void setLongArrayElement (int objref, int index, long value) {
223     da.get(objref).setLongElement(index, value);
224   }
225
226   public long getLongArrayElement (int objref, int index) {
227     return da.get(objref).getLongElement(index);
228   }
229
230   public void setLongField (int objref, String JavaDoc fname, long val) {
231     setLongField(objref, null, fname, val);
232   }
233
234   public void setLongField (int objref, String JavaDoc refType, String JavaDoc fname, long val) {
235     ElementInfo ei = da.get(objref);
236     ei.setLongField(fname, refType, val);
237   }
238
239   public long getLongField (int objref, String JavaDoc fname) {
240     return getLongField(objref, null, fname);
241   }
242
243   public long getLongField (int objref, String JavaDoc refType, String JavaDoc 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 JavaDoc fname, short val) {
258     setIntField(objref, null, fname, (int) val);
259   }
260
261   public short getShortField (int objref, String JavaDoc fname) {
262     return (short) getIntField(objref, null, fname);
263   }
264
265   public String JavaDoc getTypeName (int objref) {
266     return da.get(objref).getType();
267   }
268   
269   public boolean isInstanceOf (int objref, String JavaDoc clsName) {
270     ClassInfo ci = getClassInfo(objref);
271     return ci.instanceOf(clsName);
272   }
273   
274   // the static field setters
275
public void setStaticBooleanField (String JavaDoc clsName, String JavaDoc fname,
276                                      boolean value) {
277     setStaticIntField(clsName, fname, Types.booleanToInt(value));
278   }
279
280   public boolean getStaticBooleanField (String JavaDoc clsName, String JavaDoc fname) {
281     return Types.intToBoolean(getStaticIntField(clsName, fname));
282   }
283
284   public void setStaticByteField (String JavaDoc clsName, String JavaDoc fname, byte value) {
285     setStaticIntField(clsName, fname, (int) value);
286   }
287
288   public byte getStaticByteField (String JavaDoc clsName, String JavaDoc fname) {
289     return (byte) getStaticIntField(clsName, fname);
290   }
291
292   public void setStaticCharField (String JavaDoc clsName, String JavaDoc fname, char value) {
293     setStaticIntField(clsName, fname, (int) value);
294   }
295
296   public char getStaticCharField (String JavaDoc clsName, String JavaDoc fname) {
297     return (char) getStaticIntField(clsName, fname);
298   }
299
300   public void setStaticDoubleField (String JavaDoc clsName, String JavaDoc fname, double val) {
301     setStaticLongField(clsName, fname, Types.doubleToLong(val));
302   }
303
304   public double getStaticDoubleField (String JavaDoc clsName, String JavaDoc fname) {
305     return Types.longToDouble(getStaticLongField(clsName, fname));
306   }
307
308   public void setStaticFloatField (String JavaDoc clsName, String JavaDoc fname, float value) {
309     setStaticIntField(clsName, fname, Types.floatToInt(value));
310   }
311
312   public float getStaticFloatField (String JavaDoc clsName, String JavaDoc fname) {
313     return Types.intToFloat(getStaticIntField(clsName, fname));
314   }
315
316   public void setStaticIntField (String JavaDoc clsName, String JavaDoc fname, int value) {
317     ClassInfo ci = ClassInfo.getClassInfo(clsName);
318     sa.get(ci.getName()).setIntField(fname, null, value);
319   }
320   
321   public void setStaticIntField (int clsObjRef, String JavaDoc fname, int val) {
322     try {
323       ElementInfo cei = getClassElementInfo(clsObjRef);
324       cei.setIntField(fname, val);
325     } catch (Throwable JavaDoc x) {
326       throw new JPFException("set static field failed: " + x.getMessage());
327     }
328   }
329
330   public int getStaticIntField (String JavaDoc clsName, String JavaDoc fname) {
331     ClassInfo ci = ClassInfo.getClassInfo(clsName);
332     StaticElementInfo ei = sa.get(ci.getName());
333
334     return ei.getIntField(fname, null);
335   }
336
337   public void setStaticLongField (String JavaDoc clsName, String JavaDoc fname, long value) {
338     ClassInfo ci = ClassInfo.getClassInfo(clsName);
339     sa.get(ci.getName()).setLongField(fname, value);
340   }
341
342   public long getStaticLongField (String JavaDoc clsName, String JavaDoc fname) {
343     ClassInfo ci = ClassInfo.getClassInfo(clsName);
344     StaticElementInfo ei = sa.get(ci.getName());
345
346     return ei.getLongField(fname, null);
347   }
348
349   public void setStaticReferenceField (String JavaDoc clsName, String JavaDoc fname, int objref) {
350     ClassInfo ci = ClassInfo.getClassInfo(clsName);
351
352     // <2do> - we should REALLY check for type compatibility here
353
sa.get(ci.getName()).setReferenceField(fname, objref);
354   }
355
356   public int getStaticObjectField (String JavaDoc clsName, String JavaDoc fname) {
357     return getStaticIntField(clsName, fname);
358   }
359
360   public short getStaticShortField (String JavaDoc clsName, String JavaDoc fname) {
361     return (short) getStaticIntField(clsName, fname);
362   }
363
364   /**
365    * turn JPF String object into a JVM String object
366    * (this is a method available for non gov..jvm NativePeer classes)
367    */

368   public String JavaDoc getStringObject (int objref) {
369     if (objref != -1) {
370       ElementInfo ei = getElementInfo(objref);
371       return ei.asString();
372     } else {
373       return null;
374     }
375   }
376
377   public byte[] getByteArrayObject (int objref) {
378     ElementInfo ei = getElementInfo(objref);
379     byte[] a = ei.asByteArray();
380     
381     return a;
382   }
383   
384   public char[] getCharArrayObject (int objref) {
385     ElementInfo ei = getElementInfo(objref);
386     char[] a = ei.asCharArray();
387     
388     return a;
389   }
390   
391   public short[] getShortArrayObject (int objref) {
392     ElementInfo ei = getElementInfo(objref);
393     short[] a = ei.asShortArray();
394     
395     return a;
396   }
397
398   public int[] getIntArrayObject (int objref) {
399     ElementInfo ei = getElementInfo(objref);
400     int[] a = ei.asIntArray();
401     
402     return a;
403   }
404
405   public long[] getLongArrayObject (int objref) {
406     ElementInfo ei = getElementInfo(objref);
407     long[] a = ei.asLongArray();
408     
409     return a;
410   }
411
412   public float[] getFloatArrayObject (int objref) {
413     ElementInfo ei = getElementInfo(objref);
414     float[] a = ei.asFloatArray();
415     
416     return a;
417   }
418
419   public double[] getDoubleArrayObject (int objref) {
420     ElementInfo ei = getElementInfo(objref);
421     double[] a = ei.asDoubleArray();
422     
423     return a;
424   }
425
426   public boolean[] getBooleanArrayObject (int objref) {
427     ElementInfo ei = getElementInfo(objref);
428     boolean[] a = ei.asBooleanArray();
429     
430     return a;
431   }
432
433   
434   public boolean canLock (int objref) {
435     ElementInfo ei = getElementInfo(objref);
436
437     return ei.canLock(ti);
438   }
439
440   public int newBooleanArray (int size) {
441     return da.newArray("Z", size, ti);
442   }
443
444   public int newByteArray (int size) {
445     return da.newArray("B", size, ti);
446   }
447
448   public int newCharArray (int size) {
449     return da.newArray("C", size, ti);
450   }
451
452   public int newDoubleArray (int size) {
453     return da.newArray("D", size, ti);
454   }
455
456   public int newFloatArray (int size) {
457     return da.newArray("F", size, ti);
458   }
459
460   public int newIntArray (int size) {
461     return da.newArray("I", size, ti);
462   }
463
464   public int newLongArray (int size) {
465     return da.newArray("J", size, ti);
466   }
467
468   public int newObject (String JavaDoc clsName) {
469     // watch out - this is not initialized!!
470
ClassInfo ci = ClassInfo.getClassInfo(clsName);
471
472     return da.newObject(ci, ti);
473   }
474
475   public int newObjectArray (String JavaDoc clsName, int size) {
476     return da.newArray(clsName, size, ti);
477   }
478
479   public int newShortArray (int size) {
480     return da.newArray("S", size, ti);
481   }
482
483   public int newString (String JavaDoc s) {
484     return da.newString(s, ti);
485   }
486
487   public int newString (int arrayRef) {
488     int r = NULL;
489     String JavaDoc t = getArrayType(arrayRef);
490     String JavaDoc s = null;
491     
492     if ("C".equals(t)) { // character array
493
char[] ca = getCharArrayObject(arrayRef);
494       s = new String JavaDoc(ca);
495     } else if ("B".equals(t)) { // byte array
496
byte[] ba = getByteArrayObject(arrayRef);
497       s = new String JavaDoc(ba);
498     }
499     
500     if (s == null) {
501       return NULL;
502     }
503     
504     return newString(s);
505   }
506   
507   public void notify (int objref) {
508     ElementInfo ei = getElementInfo(objref);
509     
510     if (!ei.isLockedBy(ti)){
511       throwException("java.lang.IllegalMonitorStateException",
512                                  "un-synchronized notify");
513       return;
514     }
515     
516     ei.notifies();
517   }
518
519   public void notifyAll (int objref) {
520     ElementInfo ei = getElementInfo(objref);
521
522     if (!ei.isLockedBy(ti)){
523       throwException("java.lang.IllegalMonitorStateException",
524                                  "un-synchronized notifyAll");
525       return;
526     }
527
528     ei.notifiesAll();
529   }
530
531   public void repeatInvocation () {
532     repeat = true;
533   }
534
535   public void throwException (String JavaDoc classname) {
536     exception = Types.asTypeName(classname);
537   }
538
539   public void throwException (String JavaDoc classname, String JavaDoc details) {
540     exception = Types.asTypeName(classname);
541     exceptionDetails = details;
542   }
543
544   public void wait (int objref) {
545     ElementInfo ei = getElementInfo(objref);
546     
547     if (!ei.isLockedBy(ti)){
548       throwException("java.lang.IllegalMonitorStateException",
549                                  "un-synchronized wait");
550       return;
551     }
552
553     
554     ei.wait(ti);
555   }
556
557   void setCallEnvironment (MethodInfo mi) {
558     this.mi = mi;
559     
560     if (mi != null){
561       ci = mi.getClassInfo();
562     } else {
563       //ci = null;
564
//mi = null;
565
}
566
567     repeat = false;
568     exception = null;
569     exceptionDetails = null;
570   }
571   
572   void clearCallEnvironment () {
573     setCallEnvironment(null);
574   }
575
576   ElementInfo getClassElementInfo (int clsObjRef) {
577     ElementInfo ei = da.get(clsObjRef);
578     int cref = ei.getIntField("cref", null);
579
580     ElementInfo cei = sa.get(cref);
581
582     return cei;
583   }
584
585   ClassInfo getClassInfo () {
586     return ci;
587   }
588
589   ClassInfo getClassInfo (int objref) {
590     ElementInfo ei = getElementInfo(objref);
591     return ei.getClassInfo();
592   }
593
594   public String JavaDoc getClassName (int objref) {
595     return getClassInfo(objref).getName();
596   }
597   
598   DynamicArea getDynamicArea () {
599     return JVM.getVM().getDynamicArea();
600   }
601
602   ElementInfo getElementInfo (int objref) {
603     return da.get(objref);
604   }
605
606   int getStateId () {
607     return JVM.getVM().getStateId();
608   }
609   
610   String JavaDoc getException () {
611     return exception;
612   }
613
614   String JavaDoc getExceptionDetails () {
615     return exceptionDetails;
616   }
617
618   KernelState getKernelState () {
619     SystemState ss = getSystemState();
620
621     return ss.ks;
622   }
623
624   MethodInfo getMethodInfo () {
625     return mi;
626   }
627
628   boolean getRepeat () {
629     return repeat;
630   }
631
632   StaticArea getStaticArea () {
633     return JVM.getVM().getStaticArea();
634   }
635
636   SystemState getSystemState () {
637     JVM vm = JVM.getVM();
638
639     // <2do> - getSystemState() returns a dreaded interface
640
return vm.ss;
641   }
642
643   ThreadInfo getThreadInfo () {
644     return ti;
645   }
646
647   // <2do> - naming? not very intuitive
648
void lockNotified (int objref) {
649     ElementInfo ei = getElementInfo(objref);
650     ei.lockNotified(ti);
651   }
652 }
653
Popular Tags