src/main/gov/nasa/jpf/vm/MJIEnv.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   6  * The Java Pathfinder core (jpf-core) platform is licensed under the
   7  * Apache License, Version 2.0 (the "License"); you may not use this file except
   8  * in compliance with the License. You may obtain a copy of the License at
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  12  * Unless required by applicable law or agreed to in writing, software
  13  * distributed under the License is distributed on an "AS IS" BASIS,
  14  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  15  * See the License for the specific language governing permissions and
  16  * limitations under the License.
  17  */
  18 package gov.nasa.jpf.vm;
  19
  20 import com.sun.org.apache.bcel.internal.generic.InstructionConstants;
  21 import gov.nasa.jpf.Config;
  22 import gov.nasa.jpf.JPF;
  23 import gov.nasa.jpf.JPFException;
  24 import gov.nasa.jpf.JPFListener;
  25 import gov.nasa.jpf.vm.serialize.UnknownJPFClass;
  26
  27 import java.util.Date;
  28 import java.util.Locale;
  29
  30
  31 /**
  32  * MJIEnv is the call environment for "native" methods, i.e. code that
  33  * is executed by the VM, not by JPF.
  34  *
  35  * Since library abstractions are supposed to be "user code", we provide
  36  * this class as a (little bit of) insulation towards the inner JPF workings.
  37  *
  38  * There are two APIs exported by this class. The public methods (like
  39  * getStringObject) don't expose JPF internals, and can be used from non
  40  * gov.nasa.jpf.vm NativePeer classes). The rest is package-default
  41  * and can be used to fiddle around as much as you like to (if you are in
  42  * the ..jvm package)
  43  *
  44  * Note that MJIEnv objects are now per-ThreadInfo (i.e. the variable
  45  * call envionment only includes MethodInfo and ClassInfo), which means
  46  * MJIEnv can be used in non-native methods (but only carefully, if you
  47  * don't need mi or ciMth).
  48  *
  49  * Note also this only works because we are not getting recursive in
  50  * native method calls. In fact, the whole DirectCallStackFrame / repeatTopInstruction
  51  * mechanism is there to turn logial recursion (JPF calling native, calling
  52  * JPF, calling native,..) into iteration. Otherwise we couldn't backtrack
  53  */
  54 public class MJIEnv {
  55   public static final int NULL = 0;
  56
  57   VM                     vm;
  58   ClassInfo               ciMth;  // the ClassInfo of the method this is called from
  59   MethodInfo              mi;
  60   ThreadInfo              ti;
  61   Heap                    heap;
  62
  63   // those are various attributes set by the execution. note that
  64   // NativePeer.invoke never gets recursive in a roundtrip (at least if
  65   // used correctly, so we don't have to be afraid to overwrite any of these
  66   boolean                 repeat;
  67   Object                  returnAttr;
  68
  69   // exception to be thrown upon return from native method
  70   // NOTE: this is only transient - don't expect this to be preserved over
  71   // transition boundaries
  72   int                     exceptionRef;
  73
  74   MJIEnv (ThreadInfo ti) {
  75     this.ti = ti;
  76
  77     // set those here so that we don't have an inconsistent state between
  78     // creation of an MJI object and the first native method call in
  79     // this thread (where any access to the heap or sa would bomb)
  80     vm = ti.getVM();
  81     heap = vm.getHeap();
  82
  83     exceptionRef = NULL;
  84   }
  85
  86   public VM getVM () {
  87     return vm;
  88   }
  89
  90   public JPF getJPF () {
  91     return vm.getJPF();
  92   }
  93
  94   public boolean isBigEndianPlatform(){
  95     return vm.isBigEndianPlatform();
  96   }
  97
  98   public void addListener (JPFListener l){
  99     vm.getJPF().addListener(l);
 100   }
 101
 102   public void removeListener (JPFListener l){
 103     vm.getJPF().removeListener(l);
 104   }
 105
 106   public Config getConfig() {
 107     return vm.getConfig();
 108   }
 109
 110   public void gc() {
 111     heap.gc();
 112   }
 113
 114   public void forceState (){
 115     getSystemState().setForced(true);
 116   }
 117
 118   public void ignoreTransition () {
 119     getSystemState().setIgnored(true);
 120   }
 121
 122   public boolean isArray (int objref) {
 123     return heap.get(objref).isArray();
 124   }
 125
 126   public int getArrayLength (int objref) {
 127     if (isArray(objref)) {
 128       return heap.get(objref).arrayLength();
 129     } else {
 130       throwException("java.lang.IllegalArgumentException");
 131
 132       return 0;
 133     }
 134   }
 135
 136   public String getArrayType (int objref) {
 137     return heap.get(objref).getArrayType();
 138   }
 139
 140   public int getArrayTypeSize (int objref) {
 141     return Types.getTypeSize(getArrayType(objref));
 142   }
 143
 144   //=== various attribute accessors ============================================
 145   // we only support some attribute APIs here, since MJIEnv adds little value
 146   // other than hiding the ElementInfo access. If the client already has
 147   // an ElementInfo reference, it should use that one to retrieve/enumerate/set
 148   // attributes since this avoids repeated Heap.get() calls
 149
 150   //--- object attributes
 151
 152   public boolean hasObjectAttr (int objref){
 153     if (objref != NULL){
 154       ElementInfo ei = heap.get(objref);
 155       return ei.hasObjectAttr();
 156     }
 157
 158     return false;
 159   }
 160
 161   public boolean hasObjectAttr (int objref, Class<?> type){
 162     if (objref != NULL){
 163       ElementInfo ei = heap.get(objref);
 164       return ei.hasObjectAttr(type);
 165     }
 166
 167     return false;
 168   }
 169
 170   /**
 171    * this returns all of them - use either if you know there will be only
 172    * one attribute at a time, or check/process result with ObjectList
 173    */
 174   public Object getObjectAttr (int objref){
 175     if (objref != NULL){
 176       ElementInfo ei = heap.get(objref);
 177       return ei.getObjectAttr();
 178     }
 179     return null;
 180   }
 181
 182   /**
 183    * this replaces all of them - use only if you know
 184    *  - there will be only one attribute at a time
 185    *  - you obtained the value you set by a previous getXAttr()
 186    *  - you constructed a multi value list with ObjectList.createList()
 187    */
 188   public void setObjectAttr (int objref, Object a){
 189     if (objref != NULL){
 190       ElementInfo ei = heap.get(objref);
 191       ei.setObjectAttr(a);
 192     }
 193   }
 194
 195   public void addObjectAttr (int objref, Object a){
 196     if (objref != NULL){
 197       ElementInfo ei = heap.getModifiable(objref);
 198       ei.addObjectAttr(a);
 199     }
 200   }
 201
 202
 203   /**
 204    * this only returns the first attr of this type, there can be more
 205    * if you don't use client private types or the provided type is too general
 206    */
 207   public <T> T getObjectAttr (int objref, Class<T> attrType){
 208     ElementInfo ei = heap.get(objref);
 209     return ei.getObjectAttr(attrType);
 210   }
 211
 212   //--- field attributes
 213
 214   public boolean hasFieldAttr (int objref){
 215     if (objref != NULL){
 216       ElementInfo ei = heap.get(objref);
 217       return ei.hasFieldAttr();
 218     }
 219
 220     return false;
 221   }
 222
 223   public boolean hasFieldAttr (int objref, Class<?> type){
 224     if (objref != NULL){
 225       ElementInfo ei = heap.get(objref);
 226       return ei.hasFieldAttr(type);
 227     }
 228
 229     return false;
 230   }
 231
 232   /**
 233    * this returns all of them - use either if you know there will be only
 234    * one attribute at a time, or check/process result with ObjectList
 235    */
 236   public Object getFieldAttr (int objref, String fname){
 237     ElementInfo ei = heap.get(objref);
 238     FieldInfo fi = ei.getFieldInfo(fname);
 239     if (fi != null){
 240       return ei.getFieldAttr(fi);
 241     } else {
 242       throw new JPFException("no such field: " + fname);
 243     }
 244   }
 245
 246   /**
 247    * this replaces all of them - use only if you know
 248    *  - there will be only one attribute at a time
 249    *  - you obtained the value you set by a previous getXAttr()
 250    *  - you constructed a multi value list with ObjectList.createList()
 251    */
 252   public void setFieldAttr (int objref, String fname, Object a){
 253     if (objref != NULL){
 254       ElementInfo ei = heap.get(objref);
 255       FieldInfo fi = ei.getFieldInfo(fname);
 256       ei.setFieldAttr(fi, a);
 257     }
 258   }
 259
 260   public void addFieldAttr (int objref, String fname, Object a){
 261     if (objref != NULL){
 262       ElementInfo ei = heap.getModifiable(objref);
 263       FieldInfo fi = ei.getFieldInfo(fname);
 264       ei.addFieldAttr(fi, a);
 265     }
 266   }
 267
 268
 269   /**
 270    * this only returns the first attr of this type, there can be more
 271    * if you don't use client private types or the provided type is too general
 272    */
 273   public <T> T getFieldAttr (int objref, String fname, Class<T> attrType){
 274     ElementInfo ei = heap.get(objref);
 275     FieldInfo fi = ei.getFieldInfo(fname);
 276     if (fi != null){
 277       return ei.getFieldAttr(fi, attrType);
 278     } else {
 279       throw new JPFException("no such field: " + fname);
 280     }
 281   }
 282
 283
 284   //--- element attrs
 285
 286   public boolean hasElementdAttr (int objref){
 287     if (objref != NULL){
 288       ElementInfo ei = heap.get(objref);
 289       return ei.hasElementAttr();
 290     }
 291
 292     return false;
 293   }
 294
 295   public boolean hasElementAttr (int objref, Class<?> type){
 296     if (objref != NULL){
 297       ElementInfo ei = heap.get(objref);
 298       return ei.hasElementAttr(type);
 299     }
 300
 301     return false;
 302   }
 303
 304   /**
 305    * this returns all of them - use either if you know there will be only
 306    * one attribute at a time, or check/process result with ObjectList
 307    */
 308   public Object getElementAttr (int objref, int idx){
 309     ElementInfo ei = heap.get(objref);
 310     return ei.getElementAttr(idx);
 311   }
 312
 313   /**
 314    * this replaces all of them - use only if you know
 315    *  - there will be only one attribute at a time
 316    *  - you obtained the value you set by a previous getXAttr()
 317    *  - you constructed a multi value list with ObjectList.createList()
 318    */
 319   public void setElementAttr (int objref, int idx, Object a){
 320     ElementInfo ei = heap.get(objref);
 321     ei.setElementAttr(idx, a);
 322   }
 323
 324   public void addElementAttr (int objref, int idx, Object a){
 325     ElementInfo ei = heap.getModifiable(objref);
 326     ei.addElementAttr(idx, a);
 327   }
 328
 329
 330   /**
 331    * this only returns the first attr of this type, there can be more
 332    * if you don't use client private types or the provided type is too general
 333    */
 334   public <T> T getElementAttr (int objref, int idx, Class<T> attrType){
 335     if (objref != NULL){
 336       ElementInfo ei = heap.get(objref);
 337       return ei.getElementAttr(idx, attrType);
 338     }
 339     return null;
 340   }
 341
 342
 343
 344   // == end attrs ==
 345
 346
 347
 348   // the instance field setters
 349   public void setBooleanField (int objref, String fname, boolean val) {
 350     heap.getModifiable(objref).setBooleanField(fname, val);
 351   }
 352
 353   public boolean getBooleanField (int objref, String fname) {
 354     return heap.get(objref).getBooleanField(fname);
 355   }
 356
 357   public boolean getBooleanArrayElement (int objref, int index) {
 358     return heap.get(objref).getBooleanElement(index);
 359   }
 360
 361   public void setBooleanArrayElement (int objref, int index, boolean value) {
 362     heap.getModifiable(objref).setBooleanElement(index, value);
 363   }
 364
 365
 366   public void setByteField (int objref, String fname, byte val) {
 367     heap.getModifiable(objref).setByteField(fname, val);
 368   }
 369
 370   public byte getByteField (int objref, String fname) {
 371     return heap.get(objref).getByteField(fname);
 372   }
 373
 374   public void setCharField (int objref, String fname, char val) {
 375     heap.getModifiable(objref).setCharField(fname, val);
 376   }
 377
 378   public char getCharField (int objref, String fname) {
 379     return heap.get(objref).getCharField(fname);
 380   }
 381
 382   public void setDoubleField (int objref, String fname, double val) {
 383     heap.getModifiable(objref).setDoubleField(fname, val);
 384   }
 385
 386   public double getDoubleField (int objref, String fname) {
 387     return heap.get(objref).getDoubleField(fname);
 388   }
 389
 390   public void setFloatField (int objref, String fname, float val) {
 391     heap.getModifiable(objref).setFloatField(fname, val);
 392   }
 393
 394   public float getFloatField (int objref, String fname) {
 395     return heap.get(objref).getFloatField(fname);
 396   }
 397
 398
 399   public void setByteArrayElement (int objref, int index, byte value) {
 400     heap.getModifiable(objref).setByteElement(index, value);
 401   }
 402
 403   public byte getByteArrayElement (int objref, int index) {
 404     return heap.get(objref).getByteElement(index);
 405   }
 406
 407   public void setCharArrayElement (int objref, int index, char value) {
 408     heap.getModifiable(objref).setCharElement(index, value);
 409   }
 410
 411   public void setIntArrayElement (int objref, int index, int value) {
 412     heap.getModifiable(objref).setIntElement(index, value);
 413   }
 414
 415   public void setShortArrayElement (int objref, int index, short value) {
 416     heap.getModifiable(objref).setShortElement(index, value);
 417   }
 418
 419   public void setFloatArrayElement (int objref, int index, float value) {
 420     heap.getModifiable(objref).setFloatElement(index, value);
 421   }
 422
 423   public float getFloatArrayElement (int objref, int index) {
 424     return heap.get(objref).getFloatElement(index);
 425   }
 426
 427   public double getDoubleArrayElement (int objref, int index) {
 428     return heap.get(objref).getDoubleElement(index);
 429   }
 430   public void setDoubleArrayElement (int objref, int index, double value) {
 431     heap.getModifiable(objref).setDoubleElement(index, value);
 432   }
 433
 434   public short getShortArrayElement (int objref, int index) {
 435     return heap.get(objref).getShortElement(index);
 436   }
 437
 438   public int getIntArrayElement (int objref, int index) {
 439     return heap.get(objref).getIntElement(index);
 440   }
 441
 442   public char getCharArrayElement (int objref, int index) {
 443     return heap.get(objref).getCharElement(index);
 444   }
 445
 446   public void setIntField (int objref, String fname, int val) {
 447     ElementInfo ei = heap.getModifiable(objref);
 448     ei.setIntField(fname, val);
 449   }
 450
 451   // these two are the workhorses
 452   public void setDeclaredIntField (int objref, String refType, String fname, int val) {
 453     ElementInfo ei = heap.getModifiable(objref);
 454     ei.setDeclaredIntField(fname, refType, val);
 455   }
 456
 457   public int getIntField (int objref, String fname) {
 458     ElementInfo ei = heap.get(objref);
 459     return ei.getIntField(fname);
 460   }
 461
 462   public int getDeclaredIntField (int objref, String refType, String fname) {
 463     ElementInfo ei = heap.get(objref);
 464     return ei.getDeclaredIntField(fname, refType);
 465   }
 466
 467   // these two are the workhorses
 468   public void setDeclaredReferenceField (int objref, String refType, String fname, int val) {
 469     ElementInfo ei = heap.getModifiable(objref);
 470     ei.setDeclaredReferenceField(fname, refType, val);
 471   }
 472
 473   public void setReferenceField (int objref, String fname, int ref) {
 474      ElementInfo ei = heap.getModifiable(objref);
 475      ei.setReferenceField(fname, ref);
 476   }
 477
 478   public int getReferenceField (int objref, String fname) {
 479     ElementInfo ei = heap.get(objref);
 480     return ei.getReferenceField(fname);
 481   }
 482
 483   // we need this in case of a masked field
 484   public int getReferenceField (int objref, FieldInfo fi) {
 485     ElementInfo ei = heap.get(objref);
 486     return ei.getReferenceField(fi);
 487   }
 488
 489   public String getStringField (int objref, String fname){
 490     int ref = getReferenceField(objref, fname);
 491     return getStringObject(ref);
 492   }
 493
 494   // the box object accessors (should probably test for the appropriate class)
 495   public boolean getBooleanValue (int objref) {
 496     return getBooleanField(objref, "value");
 497   }
 498
 499   public byte getByteValue (int objref) {
 500     return getByteField(objref, "value");
 501   }
 502
 503   public char getCharValue (int objref) {
 504     return getCharField(objref, "value");
 505   }
 506
 507   public short getShortValue (int objref) {
 508     return getShortField(objref, "value");
 509   }
 510
 511   public int getIntValue (int objref) {
 512     return getIntField(objref, "value");
 513   }
 514
 515   public long getLongValue (int objref) {
 516     return getLongField(objref, "value");
 517   }
 518
 519   public float getFloatValue (int objref) {
 520     return getFloatField(objref, "value");
 521   }
 522
 523   public double getDoubleValue (int objref) {
 524     return getDoubleField(objref, "value");
 525   }
 526
 527
 528   public void setLongArrayElement (int objref, int index, long value) {
 529     heap.getModifiable(objref).setLongElement(index, value);
 530   }
 531
 532   public long getLongArrayElement (int objref, int index) {
 533     return heap.get(objref).getLongElement(index);
 534   }
 535
 536   public void setLongField (int objref, String fname, long val) {
 537     ElementInfo ei = heap.getModifiable(objref);
 538     ei.setLongField(fname, val);
 539   }
 540
 541 //  public void setLongField (int objref, String refType, String fname, long val) {
 542 //    ElementInfo ei = heap.get(objref);
 543 //    ei.setLongField(fname, refType, val);
 544 //  }
 545
 546   public long getLongField (int objref, String fname) {
 547     ElementInfo ei = heap.get(objref);
 548     return ei.getLongField(fname);
 549   }
 550
 551 //  public long getLongField (int objref, String refType, String fname) {
 552 //    ElementInfo ei = heap.get(objref);
 553 //    return ei.getLongField(fname, refType);
 554 //  }
 555
 556   public void setReferenceArrayElement (int objref, int index, int eRef) {
 557     heap.getModifiable(objref).setReferenceElement(index, eRef);
 558   }
 559
 560   public int getReferenceArrayElement (int objref, int index) {
 561     return heap.get(objref).getReferenceElement(index);
 562   }
 563
 564   public void setShortField (int objref, String fname, short val) {
 565     ElementInfo ei = heap.getModifiable(objref);
 566     ei.setShortField(fname, val);
 567   }
 568
 569   public short getShortField (int objref, String fname) {
 570     ElementInfo ei = heap.get(objref);
 571     return ei.getShortField(fname);
 572   }
 573
 574   /**
 575    * NOTE - this doesn't support element type checks or overlapping in-array copy
 576    */
 577   public void arrayCopy (int srcRef, int srcPos, int dstRef, int dstPos, int len){
 578     ElementInfo eiSrc = heap.get(srcRef);
 579     ElementInfo eiDst = heap.get(dstRef);
 580
 581     eiDst.arrayCopy(eiSrc, srcPos, dstPos, len);
 582   }
 583
 584   public String getTypeName (int objref) {
 585     return heap.get(objref).getType();
 586   }
 587
 588   public boolean isInstanceOf (int objref, String clsName) {
 589     ClassInfo ci = getClassInfo(objref);
 590     return ci.isInstanceOf(clsName);
 591   }
 592
 593   public boolean isInstanceOf (int objref, ClassInfo cls) {
 594     ClassInfo ci = getClassInfo(objref);
 595     return ci.isInstanceOf(cls);
 596   }
 597
 598   //--- the static field accessors
 599   // NOTE - it is the callers responsibility to ensure the class is
 600   // properly initialized, since calling <clinit> requires a roundtrip
 601   // (i.e. cannot be done synchronously from one of the following methods)
 602
 603   // <2do> this uses the current system CL, we should probably use an explicit CL argument
 604
 605   public void setStaticBooleanField (String clsName, String fname,
 606                                      boolean value) {
 607     ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(clsName);
 608     ci.getStaticElementInfo().setBooleanField(fname, value);
 609   }
 610   public void setStaticBooleanField (int clsObjRef, String fname, boolean val) {
 611     ElementInfo cei = getStaticElementInfo(clsObjRef);
 612     cei.setBooleanField(fname, val);
 613   }
 614
 615   public boolean getStaticBooleanField (String clsName, String fname) {
 616     ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(clsName);
 617     return ci.getStaticElementInfo().getBooleanField(fname);
 618   }
 619
 620   public void setStaticByteField (String clsName, String fname, byte value) {
 621     ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(clsName);
 622     ci.getStaticElementInfo().setByteField(fname, value);  }
 623
 624   public byte getStaticByteField (String clsName, String fname) {
 625     ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(clsName);
 626     return ci.getStaticElementInfo().getByteField(fname);
 627   }
 628
 629   public void setStaticCharField (String clsName, String fname, char value) {
 630     ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(clsName);
 631     ci.getStaticElementInfo().setCharField(fname, value);  }
 632
 633   public char getStaticCharField (String clsName, String fname) {
 634     ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(clsName);
 635     return ci.getStaticElementInfo().getCharField(fname);
 636   }
 637
 638   public void setStaticDoubleField (String clsName, String fname, double val) {
 639     ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(clsName);
 640     ci.getStaticElementInfo().setDoubleField(fname, val);
 641   }
 642
 643   public double getStaticDoubleField (String clsName, String fname) {
 644     ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(clsName);
 645     return ci.getStaticElementInfo().getDoubleField(fname);
 646   }
 647
 648   public double getStaticDoubleField (int clsObjRef, String fname) {
 649     ElementInfo cei = getStaticElementInfo(clsObjRef);
 650     return cei.getDoubleField(fname);
 651   }
 652
 653   public double getStaticDoubleField (ClassInfo ci, String fname) {
 654     ElementInfo ei = ci.getStaticElementInfo();
 655     return ei.getDoubleField(fname);
 656   }
 657
 658   public void setStaticFloatField (String clsName, String fname, float val) {
 659     ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(clsName);
 660     ci.getStaticElementInfo().setFloatField(fname, val);
 661   }
 662
 663   public float getStaticFloatField (String clsName, String fname) {
 664     ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(clsName);
 665     return ci.getStaticElementInfo().getFloatField(fname);
 666   }
 667
 668   public void setStaticIntField (String clsName, String fname, int val) {
 669     ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(clsName);
 670     ci.getStaticElementInfo().setIntField(fname, val);
 671   }
 672
 673   public void setStaticIntField (int clsObjRef, String fname, int val) {
 674     ElementInfo cei = getStaticElementInfo(clsObjRef);
 675     cei.setIntField(fname, val);
 676   }
 677
 678   public int getStaticIntField (String clsName, String fname) {
 679     ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(clsName);
 680     return ci.getStaticElementInfo().getIntField(fname);
 681   }
 682
 683   public int getStaticIntField (int clsObjRef, String fname) {
 684     ElementInfo cei = getStaticElementInfo(clsObjRef);
 685     return cei.getIntField(fname);
 686   }
 687
 688   public int getStaticIntField (ClassInfo ci, String fname) {
 689     ElementInfo ei = ci.getStaticElementInfo();
 690     return ei.getIntField(fname);
 691   }
 692
 693   public void setStaticLongField (String clsName, String fname, long value) {
 694     ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(clsName);
 695     ci.getStaticElementInfo().setLongField(fname, value);
 696   }
 697
 698   public void setStaticLongField (int clsObjRef, String fname, long val) {
 699     ElementInfo cei = getModifiableStaticElementInfo(clsObjRef);
 700     cei.setLongField(fname, val);
 701   }
 702
 703   public long getStaticLongField (int clsRef, String fname) {
 704     ClassInfo ci = getReferredClassInfo(clsRef);
 705     return getStaticLongField(ci, fname);
 706   }
 707
 708   public long getStaticLongField (String clsName, String fname) {
 709     ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(clsName);
 710     return getStaticLongField(ci, fname);
 711   }
 712
 713   public long getStaticLongField (ClassInfo ci, String fname){
 714     ElementInfo ei = ci.getStaticElementInfo();
 715     return ei.getLongField(fname);
 716   }
 717
 718   public void setStaticReferenceField (String clsName, String fname, int objref) {
 719     ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(clsName);
 720
 721     // <2do> - we should REALLY check for type compatibility here
 722     ci.getModifiableStaticElementInfo().setReferenceField(fname, objref);
 723   }
 724
 725   public void setStaticReferenceField (int clsObjRef, String fname, int objref) {
 726     ElementInfo cei = getModifiableStaticElementInfo(clsObjRef);
 727
 728     // <2do> - we should REALLY check for type compatibility here
 729     cei.setReferenceField(fname, objref);
 730   }
 731
 732   public int getStaticReferenceField (String clsName, String fname) {
 733     ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(clsName);
 734     return ci.getStaticElementInfo().getReferenceField(fname);
 735   }
 736
 737   public int getStaticReferenceField (int clsObjRef, String fname) {
 738     ElementInfo cei = getStaticElementInfo(clsObjRef);
 739     return cei.getReferenceField(fname);
 740   }
 741
 742   public int getStaticReferenceField (ClassInfo ci, String fname){
 743     return ci.getStaticElementInfo().getReferenceField(fname);
 744   }
 745
 746   public short getStaticShortField (String clsName, String fname) {
 747     ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(clsName);
 748     return ci.getStaticElementInfo().getShortField(fname);
 749   }
 750
 751   public char[] getStringChars (int objRef){
 752     if (objRef != MJIEnv.NULL) {
 753       ElementInfo ei = getElementInfo(objRef);
 754       return ei.getStringChars();
 755
 756     } else {
 757       return null;
 758     }
 759
 760   }
 761
 762   /**
 763    * turn JPF String object into a VM String object
 764    * (this is a method available for non gov..jvm NativePeer classes)
 765    */
 766   public String getStringObject (int objRef) {
 767     if (objRef != MJIEnv.NULL) {
 768       ElementInfo ei = getElementInfo(objRef);
 769       return ei.asString();
 770
 771     } else {
 772       return null;
 773     }
 774   }
 775
 776   public String[] getStringArrayObject (int aRef){
 777     String[] sa = null;
 778
 779     if (aRef == NULL) return sa;
 780
 781     ClassInfo aci = getClassInfo(aRef);
 782     if (aci.isArray()){
 783       ClassInfo eci = aci.getComponentClassInfo();
 784       if (eci.getName().equals("java.lang.String")){
 785         int len = getArrayLength(aRef);
 786         sa = new String[len];
 787
 788         for (int i=0; i<len; i++){
 789           int sRef = getReferenceArrayElement(aRef,i);
 790           sa[i] = getStringObject(sRef);
 791         }
 792
 793         return sa;
 794
 795       } else {
 796         throw new IllegalArgumentException("not a String[] array: " + aci.getName());
 797       }
 798     } else {
 799       throw new IllegalArgumentException("not an array reference: " + aci.getName());
 800     }
 801   }
 802
 803   public Date getDateObject (int objref) {
 804     if (objref != MJIEnv.NULL) {
 805       ElementInfo ei = getElementInfo(objref);
 806       if (ei.getClassInfo().getName().equals("java.util.Date")) {
 807         // <2do> this is not complete yet
 808         long fastTime = ei.getLongField("fastTime");
 809         Date d = new Date(fastTime);
 810         return d;
 811       } else {
 812         throw new JPFException("not a Date object reference: " + ei);
 813       }
 814     } else {
 815       return null;
 816     }
 817
 818   }
 819
 820   public Object[] getArgumentArray (int argRef) {
 821     Object[] args = null;
 822     if (argRef == NULL) return args;
 823
 824     int nArgs = getArrayLength(argRef);
 825     args = new Object[nArgs];
 826
 827     for (int i=0; i<nArgs; i++){
 828       int aref = getReferenceArrayElement(argRef,i);
 829       ClassInfo ci = getClassInfo(aref);
 830       String clsName = ci.getName();
 831       if (clsName.equals("java.lang.Boolean")){
 832         args[i] = Boolean.valueOf(getBooleanField(aref,"value"));
 833       } else if (clsName.equals("java.lang.Integer")){
 834         args[i] = Integer.valueOf(getIntField(aref,"value"));
 835       } else if (clsName.equals("java.lang.Double")){
 836         args[i] = Double.valueOf(getDoubleField(aref,"value"));
 837       } else if (clsName.equals("java.lang.String")){
 838         args[i] = getStringObject(aref);
 839       }
 840     }
 841
 842     return args;
 843   }
 844
 845   public Boolean getBooleanObject (int objref){
 846     return Boolean.valueOf(getBooleanField(objref, "value"));
 847   }
 848
 849   public Byte getByteObject (int objref){
 850     return new Byte(getByteField(objref, "value"));
 851   }
 852
 853   public Character getCharObject (int objref){
 854     return new Character(getCharField(objref, "value"));
 855   }
 856
 857   public Short getShortObject (int objref){
 858     return new Short(getShortField(objref, "value"));
 859   }
 860
 861   public Integer getIntegerObject (int objref){
 862     return new Integer(getIntField(objref, "value"));
 863   }
 864
 865   public Long getLongObject (int objref){
 866     return new Long(getLongField(objref, "value"));
 867   }
 868
 869   public Float getFloatObject (int objref){
 870     return new Float(getFloatField(objref, "value"));
 871   }
 872
 873   public Double getDoubleObject (int objref){
 874     return new Double(getDoubleField(objref, "value"));
 875   }
 876
 877   // danger - the returned arrays could be used to modify contents of stored objects
 878
 879   public byte[] getByteArrayObject (int objref) {
 880     ElementInfo ei = getElementInfo(objref);
 881     byte[] a = ei.asByteArray();
 882
 883     return a;
 884   }
 885
 886   public char[] getCharArrayObject (int objref) {
 887     ElementInfo ei = getElementInfo(objref);
 888     char[] a = ei.asCharArray();
 889
 890     return a;
 891   }
 892
 893   public short[] getShortArrayObject (int objref) {
 894     ElementInfo ei = getElementInfo(objref);
 895     short[] a = ei.asShortArray();
 896
 897     return a;
 898   }
 899
 900   public int[] getIntArrayObject (int objref) {
 901     ElementInfo ei = getElementInfo(objref);
 902     int[] a = ei.asIntArray();
 903
 904     return a;
 905   }
 906
 907   public long[] getLongArrayObject (int objref) {
 908     ElementInfo ei = getElementInfo(objref);
 909     long[] a = ei.asLongArray();
 910
 911     return a;
 912   }
 913
 914   public float[] getFloatArrayObject (int objref) {
 915     ElementInfo ei = getElementInfo(objref);
 916     float[] a = ei.asFloatArray();
 917
 918     return a;
 919   }
 920
 921   public double[] getDoubleArrayObject (int objref) {
 922     ElementInfo ei = getElementInfo(objref);
 923     double[] a = ei.asDoubleArray();
 924
 925     return a;
 926   }
 927
 928   public boolean[] getBooleanArrayObject (int objref) {
 929     ElementInfo ei = getElementInfo(objref);
 930     boolean[] a = ei.asBooleanArray();
 931
 932     return a;
 933   }
 934
 935   public int[] getReferenceArrayObject (int objref){
 936     ElementInfo ei = getElementInfo(objref);
 937     int[] a = ei.asReferenceArray();
 938
 939     return a;
 940   }
 941
 942   public boolean canLock (int objref) {
 943     ElementInfo ei = getElementInfo(objref);
 944
 945     return ei.canLock(ti);
 946   }
 947
 948   public int newBooleanArray (int size) {
 949     return heap.newArray("Z", size, ti).getObjectRef();
 950   }
 951
 952   public int newByteArray (int size) {
 953     return heap.newArray("B", size, ti).getObjectRef();
 954   }
 955
 956   public int newByteArray (byte[] buf){
 957     ElementInfo eiArray = heap.newArray("B", buf.length, ti);
 958     for (int i=0; i<buf.length; i++){
 959       eiArray.setByteElement( i, buf[i]);
 960     }
 961     return eiArray.getObjectRef();
 962   }
 963
 964   public int newCharArray (int size) {
 965     return heap.newArray("C", size, ti).getObjectRef();
 966   }
 967
 968   public int newCharArray (char[] buf){
 969     ElementInfo eiArray = heap.newArray("C", buf.length, ti);
 970     for (int i=0; i<buf.length; i++){
 971       eiArray.setCharElement( i, buf[i]);
 972     }
 973     return eiArray.getObjectRef();
 974   }
 975
 976   public int newShortArray (int size) {
 977     return heap.newArray("S", size, ti).getObjectRef();
 978   }
 979
 980   public int newShortArray (short[] buf){
 981     ElementInfo eiArray = heap.newArray("S", buf.length, ti);
 982     for (int i=0; i<buf.length; i++){
 983       eiArray.setShortElement(i, buf[i]);
 984     }
 985     return eiArray.getObjectRef();
 986   }
 987
 988   public int newDoubleArray (int size) {
 989     return heap.newArray("D", size, ti).getObjectRef();
 990   }
 991
 992   public int newDoubleArray (double[] buf){
 993     ElementInfo eiArray =  heap.newArray("D", buf.length, ti);
 994     for (int i=0; i<buf.length; i++){
 995       eiArray.setDoubleElement(i, buf[i]);
 996     }
 997     return eiArray.getObjectRef();
 998   }
 999
1000   public int newFloatArray (int size) {
1001     return heap.newArray("F", size, ti).getObjectRef();
1002   }
1003
1004   public int newFloatArray (float[] buf){
1005     ElementInfo eiArray =  heap.newArray("F", buf.length, ti);
1006     for (int i=0; i<buf.length; i++){
1007       eiArray.setFloatElement( i, buf[i]);
1008     }
1009     return eiArray.getObjectRef();
1010   }
1011
1012   public int newIntArray (int size) {
1013     return heap.newArray("I", size, ti).getObjectRef();
1014   }
1015
1016   public int newIntArray (int[] buf){
1017     ElementInfo eiArray = heap.newArray("I", buf.length, ti);
1018     for (int i=0; i<buf.length; i++){
1019       eiArray.setIntElement( i, buf[i]);
1020     }
1021     return eiArray.getObjectRef();
1022   }
1023
1024   public int newLongArray (int size) {
1025     return heap.newArray("J", size, ti).getObjectRef();
1026   }
1027
1028   public int newLongArray (long[] buf){
1029     ElementInfo eiArray = heap.newArray("J", buf.length, ti);
1030     for (int i=0; i<buf.length; i++){
1031       eiArray.setLongElement( i, buf[i]);
1032     }
1033     return eiArray.getObjectRef();
1034   }
1035
1036   public int newObjectArray (String elementClsName, int size) {
1037     if (!elementClsName.endsWith(";")) {
1038       elementClsName = Types.getTypeSignature(elementClsName, false);
1039     }
1040
1041     return heap.newArray(elementClsName, size, ti).getObjectRef();
1042   }
1043
1044   public ElementInfo newElementInfo (ClassInfo ci) throws ClinitRequired {
1045     if (ci.initializeClass(ti)){
1046       throw new ClinitRequired(ci);
1047     }
1048
1049     return heap.newObject(ci, ti);
1050   }
1051
1052   /**
1053    * check if the ClassInfo is properly initialized
1054    * if yes, create a new instance of it but don't call any ctor
1055    * if no, throw a ClinitRequired exception
1056    */
1057   public int newObject (ClassInfo ci)  throws ClinitRequired {
1058     ElementInfo ei = newElementInfo(ci);
1059     return ei.getObjectRef();
1060   }
1061
1062   /**
1063    * this creates a new object without checking if the ClassInfo needs
1064    * initialization. This is useful in a context that already
1065    * is aware and handles re-execution
1066    */
1067   public int newObjectOfUncheckedClass (ClassInfo ci){
1068     ElementInfo ei = heap.newObject(ci, ti);
1069     return ei.getObjectRef();
1070   }
1071
1072   public ElementInfo newElementInfo (String clsName)  throws ClinitRequired, UnknownJPFClass {
1073     ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(clsName);
1074     if (ci != null){
1075       return newElementInfo(ci);
1076     } else {
1077       throw new UnknownJPFClass(clsName);
1078     }
1079   }
1080
1081   public int newObject (String clsName)   throws ClinitRequired, UnknownJPFClass {
1082     ElementInfo ei = newElementInfo(clsName);
1083     return (ei != null) ? ei.getObjectRef() : NULL;
1084   }
1085
1086   public int newString (String s) {
1087     if (s == null){
1088       return NULL;
1089     } else {
1090       return heap.newString(s, ti).getObjectRef();
1091     }
1092   }
1093
1094   public int newStringArray (String[] a){
1095     int aref = newObjectArray("Ljava/lang/String;", a.length);
1096
1097     for (int i=0; i<a.length; i++){
1098       setReferenceArrayElement(aref, i, newString(a[i]));
1099     }
1100
1101     return aref;
1102   }
1103
1104   public int newString (int arrayRef) {
1105     String t = getArrayType(arrayRef);
1106     String s = null;
1107
1108     if ("C".equals(t)) {          // character array
1109       char[] ca = getCharArrayObject(arrayRef);
1110       s = new String(ca);
1111     } else if ("B".equals(t)) {   // byte array
1112       byte[] ba = getByteArrayObject(arrayRef);
1113       s = new String(ba);
1114     }
1115
1116     if (s == null) {
1117       return NULL;
1118     }
1119
1120     return newString(s);
1121   }
1122
1123   public String format (int fmtRef, int argRef){
1124     String format = getStringObject(fmtRef);
1125     int len = getArrayLength(argRef);
1126     Object[] arg = new Object[len];
1127
1128     for (int i=0; i<len; i++){
1129       int ref = getReferenceArrayElement(argRef,i);
1130       if (ref != NULL) {
1131         String clsName = getClassName(ref);
1132         if (clsName.equals("java.lang.String")) {
1133           arg[i] = getStringObject(ref);
1134         } else if (clsName.equals("java.lang.Boolean")){
1135           arg[i] = getBooleanObject(ref);
1136         } else if (clsName.equals("java.lang.Byte")) {
1137           arg[i] = getByteObject(ref);
1138         } else if (clsName.equals("java.lang.Char")) {
1139           arg[i] = getCharObject(ref);
1140         } else if (clsName.equals("java.lang.Short")) {
1141           arg[i] = getShortObject(ref);
1142         } else if (clsName.equals("java.lang.Integer")) {
1143           arg[i] = getIntegerObject(ref);
1144         } else if (clsName.equals("java.lang.Long")) {
1145           arg[i] = getLongObject(ref);
1146         } else if (clsName.equals("java.lang.Float")) {
1147           arg[i] = getFloatObject(ref);
1148         } else if (clsName.equals("java.lang.Double")) {
1149           arg[i] = getDoubleObject(ref);
1150         } else {
1151           // need a toString() here
1152           arg[i] = "??";
1153         }
1154       }
1155     }
1156
1157     return String.format(format,arg);
1158   }
1159
1160   public String format (Locale l,int fmtRef, int argRef){
1161             String format = getStringObject(fmtRef);
1162             int len = getArrayLength(argRef);
1163             Object[] arg = new Object[len];
1164
1165             for (int i=0; i<len; i++){
1166               int ref = getReferenceArrayElement(argRef,i);
1167               if (ref != NULL) {
1168                 String clsName = getClassName(ref);
1169                 if (clsName.equals("java.lang.String")) {
1170                   arg[i] = getStringObject(ref);
1171                 } else if (clsName.equals("java.lang.Byte")) {
1172                   arg[i] = getByteObject(ref);
1173                 } else if (clsName.equals("java.lang.Char")) {
1174                   arg[i] = getCharObject(ref);
1175                 } else if (clsName.equals("java.lang.Short")) {
1176                   arg[i] = getShortObject(ref);
1177                 } else if (clsName.equals("java.lang.Integer")) {
1178                   arg[i] = getIntegerObject(ref);
1179                 } else if (clsName.equals("java.lang.Long")) {
1180                   arg[i] = getLongObject(ref);
1181                 } else if (clsName.equals("java.lang.Float")) {
1182                   arg[i] = getFloatObject(ref);
1183                 } else if (clsName.equals("java.lang.Double")) {
1184                   arg[i] = getDoubleObject(ref);
1185                 } else {
1186                   // need a toString() here
1187                   arg[i] = "??";
1188                 }
1189               }
1190             }
1191
1192             return String.format(l,format,arg);
1193           }
1194
1195
1196   public int newBoolean (boolean b){
1197     return getStaticReferenceField("java.lang.Boolean", b ? "TRUE" : "FALSE");
1198   }
1199
1200   public int newInteger (int n){
1201     ElementInfo ei = heap.newObject(ClassLoaderInfo.getSystemResolvedClassInfo("java.lang.Integer"), ti);
1202     ei.setIntField("value",n);
1203     return ei.getObjectRef();
1204   }
1205
1206   public int newLong (long l){
1207     ElementInfo ei = heap.newObject(ClassLoaderInfo.getSystemResolvedClassInfo("java.lang.Long"), ti);
1208     ei.setLongField("value",l);
1209     return ei.getObjectRef();
1210   }
1211
1212   public int newDouble (double d){
1213     ElementInfo ei = heap.newObject(ClassLoaderInfo.getSystemResolvedClassInfo("java.lang.Double"), ti);
1214     ei.setDoubleField("value",d);
1215     return ei.getObjectRef();
1216   }
1217
1218   public int newFloat (float f){
1219     ElementInfo ei = heap.newObject(ClassLoaderInfo.getSystemResolvedClassInfo("java.lang.Float"), ti);
1220     ei.setFloatField("value",f);
1221     return ei.getObjectRef();
1222   }
1223
1224   public int newByte (byte b){
1225     ElementInfo ei = heap.newObject(ClassLoaderInfo.getSystemResolvedClassInfo("java.lang.Byte"), ti);
1226     ei.setByteField("value",b);
1227     return ei.getObjectRef();
1228   }
1229
1230   public int newShort (short s){
1231     ElementInfo ei = heap.newObject(ClassLoaderInfo.getSystemResolvedClassInfo("java.lang.Short"), ti);
1232     ei.setShortField("value",s);
1233     return ei.getObjectRef();
1234   }
1235
1236   public int newCharacter (char c){
1237     ElementInfo ei =  heap.newObject(ClassLoaderInfo.getSystemResolvedClassInfo("java.lang.Character"), ti);
1238     ei.setCharField("value",c);
1239     return ei.getObjectRef();
1240   }
1241
1242
1243   public boolean notify (int objref) {
1244     // objref can't be NULL since the corresponding INVOKE would have failed
1245     ElementInfo ei = getModifiableElementInfo(objref);
1246     return notify(ei);
1247   }
1248
1249   public boolean notify (ElementInfo ei) {
1250     if (!ei.isLockedBy(ti)){
1251       throwException("java.lang.IllegalMonitorStateException",
1252                                  "un-synchronized notify");
1253       return false;
1254     }
1255
1256     return ei.notifies(getSystemState(), ti);
1257   }
1258
1259   public boolean notifyAll (int objref) {
1260     // objref can't be NULL since the corresponding INVOKE would have failed
1261     ElementInfo ei = getElementInfo(objref);
1262     return notifyAll(ei);
1263   }
1264
1265   public boolean notifyAll (ElementInfo ei) {
1266     if (!ei.isLockedBy(ti)){
1267       throwException("java.lang.IllegalMonitorStateException",
1268                                  "un-synchronized notifyAll");
1269       return false;
1270     }
1271
1272     return ei.notifiesAll();
1273   }
1274
1275   public void registerPinDown(int objref){
1276     heap.registerPinDown(objref);
1277   }
1278   public void registerPinDown (ElementInfo ei){
1279     registerPinDown(ei.getObjectRef());
1280   }
1281
1282   public void releasePinDown(int objref){
1283     heap.releasePinDown(objref);
1284   }
1285   public void releasePinDown (ElementInfo ei){
1286     releasePinDown(ei.getObjectRef());
1287   }
1288
1289   /**
1290    *  use this whenever a peer performs an operation on a class that might not be initialized yet
1291    *  Do a repeatInvocation() in this case
1292    */
1293   public boolean requiresClinitExecution(ClassInfo ci) {
1294     return ci.initializeClass(ti);
1295   }
1296
1297   /**
1298    * repeat execution of the instruction that caused a native method call
1299    * NOTE - this does NOT mean it's the NEXT executed insn, since the native method
1300    * might have pushed direct call frames on the stack before asking us to repeat it.
1301    */
1302   public void repeatInvocation () {
1303     repeat = true;
1304   }
1305
1306   public boolean isInvocationRepeated() {
1307     return repeat;
1308   }
1309
1310
1311   public boolean setNextChoiceGenerator (ChoiceGenerator<?> cg){
1312     return vm.getSystemState().setNextChoiceGenerator(cg);
1313   }
1314
1315   public void setMandatoryNextChoiceGenerator(ChoiceGenerator<?> cg, String failMsg){
1316     vm.getSystemState().setMandatoryNextChoiceGenerator(cg, failMsg);
1317   }
1318
1319   public ChoiceGenerator<?> getChoiceGenerator () {
1320     return vm.getSystemState().getChoiceGenerator();
1321   }
1322
1323   // note this only makes sense if we actually do return something
1324   public void setReturnAttribute (Object attr) {
1325     returnAttr = attr;
1326   }
1327
1328   /**
1329    * return attr list of all arguments. Use ObjectList to retrieve values
1330    * from this list
1331    *
1332    * NOTE - this can only be called from a native method context, since
1333    * otherwise the top frame is the callee
1334    */
1335   public Object[] getArgAttributes () {
1336     StackFrame caller = getCallerStackFrame();
1337     return caller.getArgumentAttrs(mi);
1338   }
1339
1340   public Object getReturnAttribute() {
1341     return returnAttr;
1342   }
1343
1344   // if any of the next methods is called from the bottom
1345   // half of a CG method, you might want to check if another thread
1346   // or a listener has already set an exception you don't want to override
1347   // (this is for instance used in Thread.stop())
1348
1349   public void throwException (int xRef){
1350     assert isInstanceOf(xRef, "java.lang.Throwable");
1351     exceptionRef = xRef;
1352   }
1353
1354   public void throwException (String clsName) {
1355     ClassInfo ciX = ClassInfo.getInitializedClassInfo(clsName, ti);
1356     assert ciX.isInstanceOf("java.lang.Throwable");
1357     exceptionRef = ti.createException(ciX, null, NULL);
1358   }
1359
1360   public void throwException (String clsName, String details) {
1361     ClassInfo ciX = ClassInfo.getInitializedClassInfo(clsName, ti);
1362     assert ciX.isInstanceOf("java.lang.Throwable");
1363     exceptionRef = ti.createException(ciX, details, NULL);
1364   }
1365
1366   public void throwAssertion (String details) {
1367     throwException("java.lang.AssertionError", details);
1368   }
1369
1370   public void throwInterrupt(){
1371     throwException("java.lang.InterruptedException");
1372   }
1373
1374   public void stopThread(){
1375     stopThreadWithException(MJIEnv.NULL);
1376   }
1377
1378   public void stopThreadWithException (int xRef){
1379     // this will call throwException(xRef) with the proper Throwable
1380     ti.setStopped(xRef);
1381   }
1382
1383   void setCallEnvironment (MethodInfo mi) {
1384     this.mi = mi;
1385
1386     if (mi != null){
1387       ciMth = mi.getClassInfo();
1388     } else {
1389       //ciMth = null;
1390       //mi = null;
1391     }
1392
1393     repeat = false;
1394     returnAttr = null;
1395
1396     // we should NOT reset exceptionRef here because it might have been set
1397     // at the beginning of the transition. It gets reset upon return from the
1398     // native method
1399     //exceptionRef = NULL;
1400   }
1401
1402   void clearCallEnvironment () {
1403     setCallEnvironment(null);
1404   }
1405
1406   ElementInfo getStaticElementInfo (int clsObjRef) {
1407     ClassInfo ci = getReferredClassInfo( clsObjRef);
1408     if (ci != null) {
1409       return ci.getStaticElementInfo();
1410     }
1411
1412     return null;
1413   }
1414
1415   ElementInfo getModifiableStaticElementInfo (int clsObjRef) {
1416     ClassInfo ci = getReferredClassInfo( clsObjRef);
1417     if (ci != null) {
1418       return ci.getModifiableStaticElementInfo();
1419     }
1420
1421     return null;
1422   }
1423
1424
1425   ClassInfo getClassInfo () {
1426     return ciMth;
1427   }
1428
1429   public ClassInfo getReferredClassInfo (int clsObjRef) {
1430     ElementInfo ei = getElementInfo(clsObjRef);
1431     if (ei.getClassInfo().getName().equals("java.lang.Class")) {
1432       int ciId = ei.getIntField( ClassInfo.ID_FIELD);
1433       int clref = ei.getReferenceField("classLoader");
1434
1435       ElementInfo eiCl = getElementInfo(clref);
1436       int cliId = eiCl.getIntField(ClassLoaderInfo.ID_FIELD);
1437
1438       ClassLoaderInfo cli = getVM().getClassLoader(cliId);
1439       ClassInfo referredCi = cli.getClassInfo(ciId);
1440
1441       return referredCi;
1442
1443     } else {
1444       throw new JPFException("not a java.lang.Class object: " + ei);
1445     }
1446   }
1447
1448   public ClassInfo getClassInfo (int objref) {
1449     ElementInfo ei = getElementInfo(objref);
1450     if (ei != null){
1451       return ei.getClassInfo();
1452     } else {
1453       return null;
1454     }
1455   }
1456
1457   public String getClassName (int objref) {
1458     return getClassInfo(objref).getName();
1459   }
1460
1461   public Heap getHeap () {
1462     return vm.getHeap();
1463   }
1464
1465   public ElementInfo getElementInfo (int objref) {
1466     return heap.get(objref);
1467   }
1468
1469   public ElementInfo getModifiableElementInfo (int objref) {
1470     return heap.getModifiable(objref);
1471   }
1472
1473
1474   public int getStateId () {
1475     return VM.getVM().getStateId();
1476   }
1477
1478   void clearException(){
1479     exceptionRef = MJIEnv.NULL;
1480   }
1481
1482   public int peekException () {
1483     return exceptionRef;
1484   }
1485
1486   public int popException () {
1487     int ret = exceptionRef;
1488     exceptionRef = NULL;
1489     return ret;
1490   }
1491
1492   public boolean hasException(){
1493     return (exceptionRef != NULL);
1494   }
1495
1496   public boolean hasPendingInterrupt(){
1497     return (exceptionRef != NULL && isInstanceOf(exceptionRef, "java.lang.InterruptedException"));
1498   }
1499
1500   //-- time is managed by the VM
1501   public long currentTimeMillis(){
1502     return vm.currentTimeMillis();
1503   }
1504
1505   public long nanoTime(){
1506     return vm.nanoTime();
1507   }
1508
1509   //--- those are not public since they refer to JPF internals
1510   public KernelState getKernelState () {
1511     return VM.getVM().getKernelState();
1512   }
1513
1514   public MethodInfo getMethodInfo () {
1515     return mi;
1516   }
1517
1518   public Instruction getInstruction () {
1519     return ti.getPC();
1520   }
1521
1522   /**
1523    * It returns the ClassLoaderInfo corresponding to the given classloader object
1524    * reference
1525    */
1526   public ClassLoaderInfo getClassLoaderInfo(int clObjRef) {
1527     if(clObjRef == MJIEnv.NULL) {
1528       return null;
1529     }
1530
1531     int cliId = heap.get(clObjRef).getIntField(ClassLoaderInfo.ID_FIELD);
1532     return getVM().getClassLoader(cliId);
1533   }
1534
1535   // <2do> that's not correct - it should return the current SystemClassLoader, NOT the startup SystemClassLoader
1536   // (we can instantiate them explicitly)
1537   public ClassLoaderInfo getSystemClassLoaderInfo() {
1538     return ti.getSystemClassLoaderInfo();
1539   }
1540
1541   public SystemState getSystemState () {
1542     return ti.getVM().getSystemState();
1543   }
1544
1545   public ApplicationContext getApplicationContext (){
1546     return ti.getApplicationContext();
1547   }
1548
1549   public ThreadInfo getThreadInfo () {
1550     return ti;
1551   }
1552
1553   /**
1554    * NOTE - callers have to be prepared this might return null in case
1555    * the thread got already terminated
1556    */
1557   public ThreadInfo getThreadInfoForId (int id){
1558     return vm.getThreadList().getThreadInfoForId(id);
1559   }
1560
1561   public ThreadInfo getLiveThreadInfoForId (int id){
1562     ThreadInfo ti = vm.getThreadList().getThreadInfoForId(id);
1563     if (ti != null && ti.isAlive()){
1564       return ti;
1565     }
1566
1567     return null;
1568   }
1569
1570   /**
1571    * NOTE - callers have to be prepared this might return null in case
1572    * the thread got already terminated
1573    */
1574   public ThreadInfo getThreadInfoForObjRef (int id){
1575     return vm.getThreadList().getThreadInfoForObjRef(id);
1576   }
1577
1578   public ThreadInfo getLiveThreadInfoForObjRef (int id){
1579     ThreadInfo ti = vm.getThreadList().getThreadInfoForObjRef(id);
1580     if (ti != null && ti.isAlive()){
1581       return ti;
1582     }
1583
1584     return null;
1585   }
1586
1587
1588
1589   public ThreadInfo[] getLiveThreads(){
1590     return getVM().getLiveThreads();
1591   }
1592
1593   // <2do> - naming? not very intuitive
1594   void lockNotified (int objref) {
1595     ElementInfo ei = getModifiableElementInfo(objref);
1596     ei.lockNotified(ti);
1597   }
1598
1599   void initAnnotationProxyField (int proxyRef, FieldInfo fi, Object v) throws ClinitRequired {
1600     String fname = fi.getName();
1601     String ftype = fi.getType();
1602
1603     if (v instanceof String){
1604       setReferenceField(proxyRef, fname, newString((String)v));
1605     } else if (v instanceof Boolean){
1606       setBooleanField(proxyRef, fname, ((Boolean)v).booleanValue());
1607     } else if (v instanceof Integer){
1608       setIntField(proxyRef, fname, ((Integer)v).intValue());
1609     } else if (v instanceof Long){
1610       setLongField(proxyRef, fname, ((Long)v).longValue());
1611     } else if (v instanceof Float){
1612       setFloatField(proxyRef, fname, ((Float)v).floatValue());
1613     } else if (v instanceof Short){
1614       setShortField(proxyRef, fname, ((Short)v).shortValue());
1615     } else if (v instanceof Character){
1616       setCharField(proxyRef, fname, ((Character)v).charValue());
1617     } else if (v instanceof Byte){
1618       setByteField(proxyRef, fname, ((Byte)v).byteValue());
1619     } else if (v instanceof Double){
1620       setDoubleField(proxyRef, fname, ((Double)v).doubleValue());
1621
1622     } else if (v instanceof AnnotationInfo.EnumValue){ // an enum constant
1623       AnnotationInfo.EnumValue ev = (AnnotationInfo.EnumValue)v;
1624       String eCls = ev.getEnumClassName();
1625       String eConst = ev.getEnumConstName();
1626
1627       ClassInfo eci = ClassLoaderInfo.getCurrentResolvedClassInfo(eCls);
1628       if (!eci.isInitialized()){
1629         throw new ClinitRequired(eci);
1630       }
1631
1632       StaticElementInfo sei = eci.getStaticElementInfo();
1633       int eref = sei.getReferenceField(eConst);
1634       setReferenceField(proxyRef, fname, eref);
1635
1636     } else if (v instanceof AnnotationInfo.ClassValue){ // a class
1637       String clsName = v.toString();
1638       ClassInfo cci = ClassLoaderInfo.getCurrentResolvedClassInfo(clsName);
1639       // <2do> should throw ClassNotFoundError here if cci is null
1640
1641       if (!cci.isInitialized()){
1642         throw new ClinitRequired(cci);
1643       }
1644
1645       int cref = cci.getClassObjectRef();
1646       setReferenceField(proxyRef, fname, cref);
1647
1648     } else if (v.getClass().isArray()){ // ..or arrays thereof
1649       Object[] a = (Object[])v;
1650       int aref = NULL;
1651
1652       if (ftype.equals("java.lang.String[]")){
1653         aref = newObjectArray("Ljava/lang/String;", a.length);
1654         for (int i=0; i<a.length; i++){
1655           setReferenceArrayElement(aref,i,newString(a[i].toString()));
1656         }
1657       } else if (ftype.equals("int[]")){
1658         aref = newIntArray(a.length);
1659         for (int i=0; i<a.length; i++){
1660           setIntArrayElement(aref,i,((Number)a[i]).intValue());
1661         }
1662       } else if (ftype.equals("boolean[]")){
1663         aref = newBooleanArray(a.length);
1664         for (int i=0; i<a.length; i++){
1665           setBooleanArrayElement(aref,i,((Boolean)a[i]).booleanValue());
1666         }
1667       } else if (ftype.equals("long[]")){
1668         aref = newLongArray(a.length);
1669         for (int i=0; i<a.length; i++){
1670           setLongArrayElement(aref,i,((Number)a[i]).longValue());
1671         }
1672       } else if (ftype.equals("double[]")){
1673         aref = newDoubleArray(a.length);
1674         for (int i=0; i<a.length; i++){
1675           setDoubleArrayElement(aref,i,((Number)a[i]).doubleValue());
1676         }
1677       } else if (ftype.equals("java.lang.Class[]")){
1678         aref = newObjectArray("java.lang.Class", a.length);
1679         for (int i=0; i<a.length; i++){
1680           String clsName = ((AnnotationInfo.ClassValue)a[i]).getName();
1681           ClassInfo cci = ClassLoaderInfo.getCurrentResolvedClassInfo(clsName);
1682           if (!cci.isInitialized()){
1683             throw new ClinitRequired(cci);
1684           }
1685           int cref = cci.getClassObjectRef();
1686           setReferenceArrayElement(aref,i,cref);
1687         }
1688       }
1689
1690       if (aref != NULL){
1691         setReferenceField(proxyRef, fname, aref);
1692       } else {
1693         throwException("AnnotationElement type not supported: " + ftype);
1694       }
1695
1696     } else {
1697       throwException("AnnotationElement type not supported: " + ftype);
1698     }
1699   }
1700
1701   int newAnnotationProxy (ClassInfo aciProxy, AnnotationInfo ai) throws ClinitRequired {
1702
1703     int proxyRef = newObject(aciProxy);
1704
1705     // init fields of the new object from the AnnotationInfo
1706     for (AnnotationInfo.Entry e : ai.getEntries()){
1707       Object v = e.getValue();
1708       String fname = e.getKey();
1709       FieldInfo fi = aciProxy.getInstanceField(fname);
1710
1711       initAnnotationProxyField(proxyRef, fi, v);
1712     }
1713
1714     return proxyRef;
1715   }
1716
1717   int newAnnotationProxies (AnnotationInfo[] ai) throws ClinitRequired {
1718
1719     if ((ai != null) && (ai.length > 0)){
1720       int aref = newObjectArray("Ljava/lang/annotation/Annotation;", ai.length);
1721       for (int i=0; i<ai.length; i++){
1722         ClassInfo aci = ClassLoaderInfo.getCurrentResolvedClassInfo(ai[i].getName());
1723         ClassInfo aciProxy = aci.getAnnotationProxy();
1724
1725         int ar = newAnnotationProxy(aciProxy, ai[i]);
1726         setReferenceArrayElement(aref, i, ar);
1727       }
1728       return aref;
1729
1730     } else {
1731       // on demand init (not too many programs use annotation reflection)
1732       int aref = getStaticReferenceField("java.lang.Class", "emptyAnnotations");
1733       if (aref == NULL) {
1734         aref = newObjectArray("Ljava/lang/annotation/Annotation;", 0);
1735         setStaticReferenceField("java.lang.Class", "emptyAnnotations", aref);
1736       }
1737       return aref;
1738     }
1739   }
1740
1741   public void handleClinitRequest (ClassInfo ci) {
1742     ThreadInfo ti = getThreadInfo();
1743
1744     // NOTE: we have to repeat no matter what, since this is called from
1745     // a handler context (if we only had to create a class object w/o
1746     // calling clinit, we can't just go on)
1747     ci.initializeClass(ti);
1748     repeatInvocation();
1749   }
1750
1751   public StackFrame getCallerStackFrame() {
1752     // since native methods are now executed within their own stack frames
1753     // we provide a little helper to get the caller
1754     return ti.getLastNonSyntheticStackFrame();
1755   }
1756
1757   public StackFrame getModifiableCallerStackFrame() {
1758     // since native methods are now executed within their own stack frames
1759     // we provide a little helper to get the caller
1760     return ti.getModifiableLastNonSyntheticStackFrame();
1761   }
1762
1763
1764   public int valueOfBoolean(boolean b) {
1765     return BoxObjectCacheManager.valueOfBoolean(ti, b);
1766   }
1767
1768   public int valueOfByte(byte b) {
1769     return BoxObjectCacheManager.valueOfByte(ti, b);
1770   }
1771
1772   public int valueOfCharacter(char c) {
1773     return BoxObjectCacheManager.valueOfCharacter(ti, c);
1774   }
1775
1776   public int valueOfShort(short s) {
1777     return BoxObjectCacheManager.valueOfShort(ti, s);
1778   }
1779
1780   public int valueOfInteger(int i) {
1781     return BoxObjectCacheManager.valueOfInteger(ti, i);
1782   }
1783
1784   public int valueOfLong(long l) {
1785     return BoxObjectCacheManager.valueOfLong(ti, l);
1786   }
1787 }