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 java.util.Date;
  21 import java.util.Locale;
  22 import java.util.Optional;
  23
  24 import gov.nasa.jpf.Config;
  25 import gov.nasa.jpf.JPF;
  26 import gov.nasa.jpf.JPFException;
  27 import gov.nasa.jpf.JPFListener;
  28 import gov.nasa.jpf.vm.AnnotationInfo.EnumValue;
  29 import gov.nasa.jpf.vm.serialize.UnknownJPFClass;
  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.Character")) {
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     return String.format(format,arg);
1157   }
1158
1159   public String format (Locale l,int fmtRef, int argRef){
1160             String format = getStringObject(fmtRef);
1161             int len = getArrayLength(argRef);
1162             Object[] arg = new Object[len];
1163
1164             for (int i=0; i<len; i++){
1165               int ref = getReferenceArrayElement(argRef,i);
1166               if (ref != NULL) {
1167                 String clsName = getClassName(ref);
1168                 if (clsName.equals("java.lang.String")) {
1169                   arg[i] = getStringObject(ref);
1170                 } else if (clsName.equals("java.lang.Byte")) {
1171                   arg[i] = getByteObject(ref);
1172                 } else if (clsName.equals("java.lang.Character")) {
1173                   arg[i] = getCharObject(ref);
1174                 } else if (clsName.equals("java.lang.Short")) {
1175                   arg[i] = getShortObject(ref);
1176                 } else if (clsName.equals("java.lang.Integer")) {
1177                   arg[i] = getIntegerObject(ref);
1178                 } else if (clsName.equals("java.lang.Long")) {
1179                   arg[i] = getLongObject(ref);
1180                 } else if (clsName.equals("java.lang.Float")) {
1181                   arg[i] = getFloatObject(ref);
1182                 } else if (clsName.equals("java.lang.Double")) {
1183                   arg[i] = getDoubleObject(ref);
1184                 } else {
1185                   // need a toString() here
1186                   arg[i] = "??";
1187                 }
1188               }
1189             }
1190
1191             return String.format(l,format,arg);
1192           }
1193
1194
1195   public int newBoolean (boolean b){
1196     return getStaticReferenceField("java.lang.Boolean", b ? "TRUE" : "FALSE");
1197   }
1198
1199   public int newInteger (int n){
1200     ElementInfo ei = heap.newObject(ClassLoaderInfo.getSystemResolvedClassInfo("java.lang.Integer"), ti);
1201     ei.setIntField("value",n);
1202     return ei.getObjectRef();
1203   }
1204
1205   public int newLong (long l){
1206     ElementInfo ei = heap.newObject(ClassLoaderInfo.getSystemResolvedClassInfo("java.lang.Long"), ti);
1207     ei.setLongField("value",l);
1208     return ei.getObjectRef();
1209   }
1210
1211   public int newDouble (double d){
1212     ElementInfo ei = heap.newObject(ClassLoaderInfo.getSystemResolvedClassInfo("java.lang.Double"), ti);
1213     ei.setDoubleField("value",d);
1214     return ei.getObjectRef();
1215   }
1216
1217   public int newFloat (float f){
1218     ElementInfo ei = heap.newObject(ClassLoaderInfo.getSystemResolvedClassInfo("java.lang.Float"), ti);
1219     ei.setFloatField("value",f);
1220     return ei.getObjectRef();
1221   }
1222
1223   public int newByte (byte b){
1224     ElementInfo ei = heap.newObject(ClassLoaderInfo.getSystemResolvedClassInfo("java.lang.Byte"), ti);
1225     ei.setByteField("value",b);
1226     return ei.getObjectRef();
1227   }
1228
1229   public int newShort (short s){
1230     ElementInfo ei = heap.newObject(ClassLoaderInfo.getSystemResolvedClassInfo("java.lang.Short"), ti);
1231     ei.setShortField("value",s);
1232     return ei.getObjectRef();
1233   }
1234
1235   public int newCharacter (char c){
1236     ElementInfo ei =  heap.newObject(ClassLoaderInfo.getSystemResolvedClassInfo("java.lang.Character"), ti);
1237     ei.setCharField("value",c);
1238     return ei.getObjectRef();
1239   }
1240
1241
1242   public boolean notify (int objref) {
1243     // objref can't be NULL since the corresponding INVOKE would have failed
1244     ElementInfo ei = getModifiableElementInfo(objref);
1245     return notify(ei);
1246   }
1247
1248   public boolean notify (ElementInfo ei) {
1249     if (!ei.isLockedBy(ti)){
1250       throwException("java.lang.IllegalMonitorStateException",
1251                                  "un-synchronized notify");
1252       return false;
1253     }
1254
1255     return ei.notifies(getSystemState(), ti);
1256   }
1257
1258   public boolean notifyAll (int objref) {
1259     // objref can't be NULL since the corresponding INVOKE would have failed
1260     ElementInfo ei = getElementInfo(objref);
1261     return notifyAll(ei);
1262   }
1263
1264   public boolean notifyAll (ElementInfo ei) {
1265     if (!ei.isLockedBy(ti)){
1266       throwException("java.lang.IllegalMonitorStateException",
1267                                  "un-synchronized notifyAll");
1268       return false;
1269     }
1270
1271     return ei.notifiesAll();
1272   }
1273
1274   public void registerPinDown(int objref){
1275     heap.registerPinDown(objref);
1276   }
1277   public void registerPinDown (ElementInfo ei){
1278     registerPinDown(ei.getObjectRef());
1279   }
1280
1281   public void releasePinDown(int objref){
1282     heap.releasePinDown(objref);
1283   }
1284   public void releasePinDown (ElementInfo ei){
1285     releasePinDown(ei.getObjectRef());
1286   }
1287
1288   /**
1289    *  use this whenever a peer performs an operation on a class that might not be initialized yet
1290    *  Do a repeatInvocation() in this case
1291    */
1292   public boolean requiresClinitExecution(ClassInfo ci) {
1293     return ci.initializeClass(ti);
1294   }
1295
1296   /**
1297    * repeat execution of the instruction that caused a native method call
1298    * NOTE - this does NOT mean it's the NEXT executed insn, since the native method
1299    * might have pushed direct call frames on the stack before asking us to repeat it.
1300    */
1301   public void repeatInvocation () {
1302     repeat = true;
1303   }
1304
1305   public boolean isInvocationRepeated() {
1306     return repeat;
1307   }
1308
1309
1310   public boolean setNextChoiceGenerator (ChoiceGenerator<?> cg){
1311     return vm.getSystemState().setNextChoiceGenerator(cg);
1312   }
1313
1314   public void setMandatoryNextChoiceGenerator(ChoiceGenerator<?> cg, String failMsg){
1315     vm.getSystemState().setMandatoryNextChoiceGenerator(cg, failMsg);
1316   }
1317
1318   public ChoiceGenerator<?> getChoiceGenerator () {
1319     return vm.getSystemState().getChoiceGenerator();
1320   }
1321
1322   // note this only makes sense if we actually do return something
1323   public void setReturnAttribute (Object attr) {
1324     returnAttr = attr;
1325   }
1326
1327   /**
1328    * return attr list of all arguments. Use ObjectList to retrieve values
1329    * from this list
1330    *
1331    * NOTE - this can only be called from a native method context, since
1332    * otherwise the top frame is the callee
1333    */
1334   public Object[] getArgAttributes () {
1335     StackFrame caller = getCallerStackFrame();
1336     return caller.getArgumentAttrs(mi);
1337   }
1338
1339   public Object getReturnAttribute() {
1340     return returnAttr;
1341   }
1342
1343   // if any of the next methods is called from the bottom
1344   // half of a CG method, you might want to check if another thread
1345   // or a listener has already set an exception you don't want to override
1346   // (this is for instance used in Thread.stop())
1347
1348   public void throwException (int xRef){
1349     assert isInstanceOf(xRef, "java.lang.Throwable");
1350     exceptionRef = xRef;
1351   }
1352
1353   public void throwException (String clsName) {
1354     ClassInfo ciX = ClassInfo.getInitializedClassInfo(clsName, ti);
1355     assert ciX.isInstanceOf("java.lang.Throwable") : ciX;
1356     exceptionRef = ti.createException(ciX, null, NULL);
1357   }
1358
1359   public void throwException (String clsName, String details) {
1360     ClassInfo ciX = ClassInfo.getInitializedClassInfo(clsName, ti);
1361     assert ciX.isInstanceOf("java.lang.Throwable");
1362     exceptionRef = ti.createException(ciX, details, NULL);
1363   }
1364
1365   public void throwAssertion (String details) {
1366     throwException("java.lang.AssertionError", details);
1367   }
1368
1369   public void throwInterrupt(){
1370     throwException("java.lang.InterruptedException");
1371   }
1372
1373   public void stopThread(){
1374     stopThreadWithException(MJIEnv.NULL);
1375   }
1376
1377   public void stopThreadWithException (int xRef){
1378     // this will call throwException(xRef) with the proper Throwable
1379     ti.setStopped(xRef);
1380   }
1381
1382   void setCallEnvironment (MethodInfo mi) {
1383     this.mi = mi;
1384
1385     if (mi != null){
1386       ciMth = mi.getClassInfo();
1387     } else {
1388       //ciMth = null;
1389       //mi = null;
1390     }
1391
1392     repeat = false;
1393     returnAttr = null;
1394
1395     // we should NOT reset exceptionRef here because it might have been set
1396     // at the beginning of the transition. It gets reset upon return from the
1397     // native method
1398     //exceptionRef = NULL;
1399   }
1400
1401   void clearCallEnvironment () {
1402     setCallEnvironment(null);
1403   }
1404
1405   ElementInfo getStaticElementInfo (int clsObjRef) {
1406     ClassInfo ci = getReferredClassInfo( clsObjRef);
1407     if (ci != null) {
1408       return ci.getStaticElementInfo();
1409     }
1410
1411     return null;
1412   }
1413
1414   ElementInfo getModifiableStaticElementInfo (int clsObjRef) {
1415     ClassInfo ci = getReferredClassInfo( clsObjRef);
1416     if (ci != null) {
1417       return ci.getModifiableStaticElementInfo();
1418     }
1419
1420     return null;
1421   }
1422
1423
1424   ClassInfo getClassInfo () {
1425     return ciMth;
1426   }
1427
1428   public ClassInfo getReferredClassInfo (int clsObjRef) {
1429     ElementInfo ei = getElementInfo(clsObjRef);
1430     if (ei.getClassInfo().getName().equals("java.lang.Class")) {
1431       int ciId = ei.getIntField( ClassInfo.ID_FIELD);
1432       int clref = ei.getReferenceField("classLoader");
1433
1434       ElementInfo eiCl = getElementInfo(clref);
1435       int cliId = eiCl.getIntField(ClassLoaderInfo.ID_FIELD);
1436
1437       ClassLoaderInfo cli = getVM().getClassLoader(cliId);
1438       ClassInfo referredCi = cli.getClassInfo(ciId);
1439
1440       return referredCi;
1441
1442     } else {
1443       throw new JPFException("not a java.lang.Class object: " + ei);
1444     }
1445   }
1446
1447   public ClassInfo getClassInfo (int objref) {
1448     ElementInfo ei = getElementInfo(objref);
1449     if (ei != null){
1450       return ei.getClassInfo();
1451     } else {
1452       return null;
1453     }
1454   }
1455
1456   public String getClassName (int objref) {
1457     return getClassInfo(objref).getName();
1458   }
1459
1460   public Heap getHeap () {
1461     return vm.getHeap();
1462   }
1463
1464   public ElementInfo getElementInfo (int objref) {
1465     return heap.get(objref);
1466   }
1467
1468   public ElementInfo getModifiableElementInfo (int objref) {
1469     return heap.getModifiable(objref);
1470   }
1471
1472
1473   public int getStateId () {
1474     return VM.getVM().getStateId();
1475   }
1476
1477   void clearException(){
1478     exceptionRef = MJIEnv.NULL;
1479   }
1480
1481   public int peekException () {
1482     return exceptionRef;
1483   }
1484
1485   public int popException () {
1486     int ret = exceptionRef;
1487     exceptionRef = NULL;
1488     return ret;
1489   }
1490
1491   public boolean hasException(){
1492     return (exceptionRef != NULL);
1493   }
1494
1495   public boolean hasPendingInterrupt(){
1496     return (exceptionRef != NULL && isInstanceOf(exceptionRef, "java.lang.InterruptedException"));
1497   }
1498
1499   //-- time is managed by the VM
1500   public long currentTimeMillis(){
1501     return vm.currentTimeMillis();
1502   }
1503
1504   public long nanoTime(){
1505     return vm.nanoTime();
1506   }
1507
1508   //--- those are not public since they refer to JPF internals
1509   public KernelState getKernelState () {
1510     return VM.getVM().getKernelState();
1511   }
1512
1513   public MethodInfo getMethodInfo () {
1514     return mi;
1515   }
1516
1517   public Instruction getInstruction () {
1518     return ti.getPC();
1519   }
1520
1521   /**
1522    * It returns the ClassLoaderInfo corresponding to the given classloader object
1523    * reference
1524    */
1525   public ClassLoaderInfo getClassLoaderInfo(int clObjRef) {
1526     if(clObjRef == MJIEnv.NULL) {
1527       return null;
1528     }
1529
1530     int cliId = heap.get(clObjRef).getIntField(ClassLoaderInfo.ID_FIELD);
1531     return getVM().getClassLoader(cliId);
1532   }
1533
1534   // <2do> that's not correct - it should return the current SystemClassLoader, NOT the startup SystemClassLoader
1535   // (we can instantiate them explicitly)
1536   public ClassLoaderInfo getSystemClassLoaderInfo() {
1537     return ti.getSystemClassLoaderInfo();
1538   }
1539
1540   public SystemState getSystemState () {
1541     return ti.getVM().getSystemState();
1542   }
1543
1544   public ApplicationContext getApplicationContext (){
1545     return ti.getApplicationContext();
1546   }
1547
1548   public ThreadInfo getThreadInfo () {
1549     return ti;
1550   }
1551
1552   /**
1553    * NOTE - callers have to be prepared this might return null in case
1554    * the thread got already terminated
1555    */
1556   public ThreadInfo getThreadInfoForId (int id){
1557     return vm.getThreadList().getThreadInfoForId(id);
1558   }
1559
1560   public ThreadInfo getLiveThreadInfoForId (int id){
1561     ThreadInfo ti = vm.getThreadList().getThreadInfoForId(id);
1562     if (ti != null && ti.isAlive()){
1563       return ti;
1564     }
1565
1566     return null;
1567   }
1568
1569   /**
1570    * NOTE - callers have to be prepared this might return null in case
1571    * the thread got already terminated
1572    */
1573   public ThreadInfo getThreadInfoForObjRef (int id){
1574     return vm.getThreadList().getThreadInfoForObjRef(id);
1575   }
1576
1577   public ThreadInfo getLiveThreadInfoForObjRef (int id){
1578     ThreadInfo ti = vm.getThreadList().getThreadInfoForObjRef(id);
1579     if (ti != null && ti.isAlive()){
1580       return ti;
1581     }
1582
1583     return null;
1584   }
1585
1586
1587
1588   public ThreadInfo[] getLiveThreads(){
1589     return getVM().getLiveThreads();
1590   }
1591
1592   // <2do> - naming? not very intuitive
1593   void lockNotified (int objref) {
1594     ElementInfo ei = getModifiableElementInfo(objref);
1595     ei.lockNotified(ti);
1596   }
1597
1598   public int liftNativeAnnotationValue(String ftype, Object v) {
1599     if (v instanceof String){
1600       return newString((String)v);
1601     } else if (v instanceof Boolean){
1602       return valueOfBoolean((Boolean)v);
1603     } else if (v instanceof Integer) {
1604       return valueOfInteger((Integer)v);
1605     } else if (v instanceof Long){
1606       return valueOfLong((Long)v);
1607     } else if (v instanceof Float){
1608       return newFloat((Float) v);
1609     } else if (v instanceof Short){
1610       return valueOfShort((Short)v);
1611     } else if (v instanceof Character){
1612       return valueOfCharacter((Character)v);
1613     } else if (v instanceof Byte){
1614       return valueOfByte((Byte)v);
1615     } else if (v instanceof Double){
1616       return newDouble((Double)v);
1617     } else {
1618       Optional<Integer> ref = liftAnnotationReferenceValue(v, ftype);
1619       if(ref.isPresent()) {
1620         return ref.get();
1621       } else {
1622         throwException("java.lang.InternalError", "AnnotationElement type not supported: " + ftype);
1623         return -1;
1624       }
1625     }
1626   }
1627
1628   Optional<Integer> liftAnnotationReferenceValue(Object v, String ftype) {
1629     if (v instanceof AnnotationInfo.EnumValue){ // an enum constant
1630       int eref = makeAnnotationEnumRef((EnumValue) v);
1631       return Optional.of(eref);
1632
1633     } else if (v instanceof AnnotationInfo.ClassValue){ // a class
1634       String clsName = v.toString();
1635       ClassInfo cci = ClassLoaderInfo.getCurrentResolvedClassInfo(clsName);
1636       // <2do> should throw ClassNotFoundError here if cci is null
1637
1638       if (!cci.isInitialized()){
1639         throw new ClinitRequired(cci);
1640       }
1641
1642       int cref = cci.getClassObjectRef();
1643       return Optional.of(cref);
1644
1645     } else if (v.getClass().isArray()){ // ..or arrays thereof
1646       Object[] a = (Object[])v;
1647       int aref = NULL;
1648
1649       if (ftype.equals("java.lang.String[]")){
1650         aref = newObjectArray("Ljava/lang/String;", a.length);
1651         for (int i=0; i<a.length; i++){
1652           setReferenceArrayElement(aref,i,newString(a[i].toString()));
1653         }
1654       } else if (ftype.equals("int[]")){
1655         aref = newIntArray(a.length);
1656         for (int i=0; i<a.length; i++){
1657           setIntArrayElement(aref,i,((Number)a[i]).intValue());
1658         }
1659       } else if (ftype.equals("boolean[]")){
1660         aref = newBooleanArray(a.length);
1661         for (int i=0; i<a.length; i++){
1662           setBooleanArrayElement(aref,i,((Boolean)a[i]).booleanValue());
1663         }
1664       } else if (ftype.equals("long[]")){
1665         aref = newLongArray(a.length);
1666         for (int i=0; i<a.length; i++){
1667           setLongArrayElement(aref,i,((Number)a[i]).longValue());
1668         }
1669       } else if (ftype.equals("double[]")){
1670         aref = newDoubleArray(a.length);
1671         for (int i=0; i<a.length; i++){
1672           setDoubleArrayElement(aref,i,((Number)a[i]).doubleValue());
1673         }
1674       } else if(ftype.equals("char[]")) {
1675         aref = newCharArray(a.length);
1676         for (int i=0; i<a.length; i++){
1677           setCharArrayElement(aref,i,((Character)a[i]).charValue());
1678         }
1679       } else if(ftype.equals("short[]")) {
1680         aref = newShortArray(a.length);
1681         for (int i=0; i<a.length; i++){
1682           setShortArrayElement(aref,i,((Number)a[i]).shortValue());
1683         }
1684       } else if(ftype.equals("byte[]")) {
1685         aref = newByteArray(a.length);
1686         for (int i=0; i<a.length; i++){
1687           setByteArrayElement(aref,i,((Number)a[i]).byteValue());
1688         }
1689       } else if(ftype.equals("float[]")) {
1690         aref = newFloatArray(a.length);
1691         for (int i=0; i<a.length; i++){
1692           setFloatArrayElement(aref,i,((Number)a[i]).floatValue());
1693         }
1694       } else if (ftype.equals("java.lang.Class[]")){
1695         aref = newObjectArray("java.lang.Class", a.length);
1696         for (int i=0; i<a.length; i++){
1697           String clsName = ((AnnotationInfo.ClassValue)a[i]).getName();
1698           ClassInfo cci = ClassLoaderInfo.getCurrentResolvedClassInfo(clsName);
1699           if (!cci.isInitialized()){
1700             throw new ClinitRequired(cci);
1701           }
1702           int cref = cci.getClassObjectRef();
1703           setReferenceArrayElement(aref,i,cref);
1704         }
1705       } else {
1706         String typeName = ftype.substring(0, ftype.length() - 2);
1707         ClassInfo elemType = ClassLoaderInfo.getCurrentResolvedClassInfo(typeName);
1708         aref = newObjectArray(typeName, a.length);
1709         if(elemType.isEnum()) {
1710           for(int i = 0; i < a.length; i++) {
1711             setReferenceArrayElement(aref, i, makeAnnotationEnumRef((EnumValue) a[i]));
1712           }
1713
1714         } else {
1715           for(int i = 0; i < a.length; i++) {
1716             setReferenceArrayElement(aref, i, makeAnnotationProxy((AnnotationInfo) a[i]));
1717           }
1718         }
1719       }
1720
1721       if (aref != NULL){
1722         return Optional.of(aref);
1723       } else {
1724         return Optional.empty();
1725       }
1726
1727     } else if(v instanceof AnnotationInfo) {
1728       return Optional.of(makeAnnotationProxy((AnnotationInfo) v));
1729     } else {
1730       return Optional.empty();
1731     }
1732   }
1733
1734   void initAnnotationProxyField (int proxyRef, FieldInfo fi, Object v) throws ClinitRequired {
1735     String fname = fi.getName();
1736     String ftype = fi.getType();
1737
1738     if (v instanceof String){
1739       setReferenceField(proxyRef, fname, newString((String)v));
1740     } else if (v instanceof Boolean){
1741       setBooleanField(proxyRef, fname, ((Boolean)v).booleanValue());
1742     } else if (v instanceof Integer){
1743       setIntField(proxyRef, fname, ((Integer)v).intValue());
1744     } else if (v instanceof Long){
1745       setLongField(proxyRef, fname, ((Long)v).longValue());
1746     } else if (v instanceof Float){
1747       setFloatField(proxyRef, fname, ((Float)v).floatValue());
1748     } else if (v instanceof Short){
1749       setShortField(proxyRef, fname, ((Short)v).shortValue());
1750     } else if (v instanceof Character){
1751       setCharField(proxyRef, fname, ((Character)v).charValue());
1752     } else if (v instanceof Byte){
1753       setByteField(proxyRef, fname, ((Byte)v).byteValue());
1754     } else if (v instanceof Double){
1755       setDoubleField(proxyRef, fname, ((Double)v).doubleValue());
1756     } else {
1757       Optional<Integer> ref = liftAnnotationReferenceValue(v, ftype);
1758       if(ref.isPresent()) {
1759         setReferenceField(proxyRef, fname, ref.get());
1760       } else {
1761         throwException("java.lang.InternalError", "AnnotationElement type not supported: " + ftype);
1762       }
1763     }
1764   }
1765
1766   private int makeAnnotationEnumRef(AnnotationInfo.EnumValue v) {
1767     AnnotationInfo.EnumValue ev = (AnnotationInfo.EnumValue)v;
1768     String eCls = ev.getEnumClassName();
1769     String eConst = ev.getEnumConstName();
1770
1771     ClassInfo eci = ClassLoaderInfo.getCurrentResolvedClassInfo(eCls);
1772     if (!eci.isInitialized()){
1773       throw new ClinitRequired(eci);
1774     }
1775
1776     StaticElementInfo sei = eci.getStaticElementInfo();
1777     int eref = sei.getReferenceField(eConst);
1778     return eref;
1779   }
1780
1781   int newAnnotationProxy (ClassInfo aciProxy, AnnotationInfo ai) throws ClinitRequired {
1782
1783     int proxyRef = newObject(aciProxy);
1784
1785     // init fields of the new object from the AnnotationInfo
1786     for (AnnotationInfo.Entry e : ai.getEntries()){
1787       Object v = e.getValue();
1788       String fname = e.getKey();
1789       FieldInfo fi = aciProxy.getInstanceField(fname);
1790       initAnnotationProxyField(proxyRef, fi, v);
1791     }
1792
1793     return proxyRef;
1794   }
1795
1796   int newAnnotationProxies (AnnotationInfo[] ai) throws ClinitRequired {
1797
1798     if ((ai != null) && (ai.length > 0)){
1799       int aref = newObjectArray("Ljava/lang/annotation/Annotation;", ai.length);
1800       for (int i=0; i<ai.length; i++){
1801         int ar = makeAnnotationProxy(ai[i]);
1802         setReferenceArrayElement(aref, i, ar);
1803       }
1804       return aref;
1805
1806     } else {
1807       // on demand init (not too many programs use annotation reflection)
1808       int aref = getStaticReferenceField("java.lang.Class", "emptyAnnotations");
1809       if (aref == NULL) {
1810         aref = newObjectArray("Ljava/lang/annotation/Annotation;", 0);
1811         setStaticReferenceField("java.lang.Class", "emptyAnnotations", aref);
1812       }
1813       return aref;
1814     }
1815   }
1816
1817   private int makeAnnotationProxy(AnnotationInfo annotationInfo) {
1818     ClassInfo aci = ClassLoaderInfo.getCurrentResolvedClassInfo(annotationInfo.getName());
1819     ClassInfo aciProxy = aci.getAnnotationProxy();
1820
1821     int ar = newAnnotationProxy(aciProxy, annotationInfo);
1822     return ar;
1823   }
1824
1825   public void handleClinitRequest (ClassInfo ci) {
1826     ThreadInfo ti = getThreadInfo();
1827
1828     // NOTE: we have to repeat no matter what, since this is called from
1829     // a handler context (if we only had to create a class object w/o
1830     // calling clinit, we can't just go on)
1831     ci.initializeClass(ti);
1832     repeatInvocation();
1833   }
1834
1835   public StackFrame getCallerStackFrame() {
1836     // since native methods are now executed within their own stack frames
1837     // we provide a little helper to get the caller
1838     return ti.getLastNonSyntheticStackFrame();
1839   }
1840
1841   public StackFrame getModifiableCallerStackFrame() {
1842     // since native methods are now executed within their own stack frames
1843     // we provide a little helper to get the caller
1844     return ti.getModifiableLastNonSyntheticStackFrame();
1845   }
1846
1847
1848   public int valueOfBoolean(boolean b) {
1849     return BoxObjectCacheManager.valueOfBoolean(ti, b);
1850   }
1851
1852   public int valueOfByte(byte b) {
1853     return BoxObjectCacheManager.valueOfByte(ti, b);
1854   }
1855
1856   public int valueOfCharacter(char c) {
1857     return BoxObjectCacheManager.valueOfCharacter(ti, c);
1858   }
1859
1860   public int valueOfShort(short s) {
1861     return BoxObjectCacheManager.valueOfShort(ti, s);
1862   }
1863
1864   public int valueOfInteger(int i) {
1865     return BoxObjectCacheManager.valueOfInteger(ti, i);
1866   }
1867
1868   public int valueOfLong(long l) {
1869     return BoxObjectCacheManager.valueOfLong(ti, l);
1870   }
1871 }