1 package gov.nasa.jpf.jvm; 20 21 import gov.nasa.jpf.JPFException; 22 23 24 42 public class MJIEnv { 43 public static final int NULL = -1; 44 45 JVM vm; 46 ClassInfo ci; 47 MethodInfo mi; 48 ThreadInfo ti; 49 DynamicArea da; 50 StaticArea sa; 51 boolean repeat; 52 String exception; 53 String exceptionDetails; 54 55 MJIEnv (ThreadInfo ti) { 56 this.ti = ti; 57 58 vm = ti.getVM(); 62 da = vm.getDynamicArea(); 63 sa = vm.getStaticArea(); 64 } 65 66 public JVM getVM () { 67 return vm; 68 } 69 70 public boolean isArray (int objref) { 71 return da.get(objref).isArray(); 72 } 73 74 public int getArrayLength (int objref) { 75 if (isArray(objref)) { 76 return da.get(objref).arrayLength(); 77 } else { 78 throwException("java.lang.IllegalArgumentException"); 79 80 return 0; 81 } 82 } 83 84 public String getArrayType (int objref) { 85 return da.get(objref).getArrayType(); 86 } 87 88 public int getArrayTypeSize (int objref) { 89 return Types.getTypeSize(getArrayType(objref)); 90 } 91 92 public void setBooleanField (int objref, String fname, boolean val) { 94 setIntField(objref, null, fname, Types.booleanToInt(val)); 95 } 96 97 public boolean getBooleanField (int objref, String fname) { 98 return Types.intToBoolean(getIntField(objref, null, fname)); 99 } 100 101 public void setByteField (int objref, String fname, byte val) { 102 setIntField(objref, null, fname, (int) val); 103 } 104 105 public byte getByteField (int objref, String fname) { 106 return (byte) getIntField(objref, null, fname); 107 } 108 109 public void setCharField (int objref, String fname, char val) { 110 setIntField(objref, null, fname, (int) val); 111 } 112 113 public char getCharField (int objref, String fname) { 114 return (char) getIntField(objref, null, fname); 115 } 116 117 public void setDoubleField (int objref, String fname, double val) { 118 setLongField(objref, null, fname, Types.doubleToLong(val)); 119 } 120 121 public double getDoubleField (int objref, String fname) { 122 return Types.longToDouble(getLongField(objref, null, fname)); 123 } 124 125 public void setFloatField (int objref, String fname, float val) { 126 setIntField(objref, null, fname, Types.floatToInt(val)); 127 } 128 129 public float getFloatField (int objref, String fname) { 130 return Types.intToFloat(getIntField(objref, null, fname)); 131 } 132 133 public void setByteArrayElement (int objref, int index, byte value) { 134 da.get(objref).setElement(index, value); 135 } 136 137 public void setCharArrayElement (int objref, int index, char value) { 138 da.get(objref).setElement(index, value); 139 } 140 141 public void setIntArrayElement (int objref, int index, int value) { 142 da.get(objref).setElement(index, value); 143 } 144 145 public int getIntArrayElement (int objref, int index) { 146 return da.get(objref).getElement(index); 147 } 148 149 public char getCharArrayElement (int objref, int index) { 150 return (char) da.get(objref).getElement(index); 151 } 152 153 public void setIntField (int objref, String fname, int val) { 154 setIntField(objref, null, fname, val); 155 } 156 157 public void setIntField (int objref, String refType, String fname, int val) { 159 ElementInfo ei = da.get(objref); 160 ei.setIntField(fname, refType, val); 161 } 162 163 public int getIntField (int objref, String fname) { 164 return getIntField(objref, null, fname); 165 } 166 167 public int getIntField (int objref, String refType, String fname) { 168 ElementInfo ei = da.get(objref); 169 170 return ei.getIntField(fname, refType); 171 } 172 173 public void setReferenceField (int objref, String refType, String fname, int val) { 175 ElementInfo ei = da.get(objref); 176 ei.setReferenceField(fname, refType, val); 177 } 178 179 public void setReferenceField (int objref, String fname, int ref) { 180 setReferenceField(objref, null, fname, ref); 181 } 182 183 public int getReferenceField (int objref, String fname) { 184 return getIntField(objref, null, fname); 185 } 186 187 188 public boolean getBooleanValue (int objref) { 190 return getBooleanField(objref, "value"); 191 } 192 193 public byte getByteValue (int objref) { 194 return getByteField(objref, "value"); 195 } 196 197 public char getCharValue (int objref) { 198 return getCharField(objref, "value"); 199 } 200 201 public short getShortValue (int objref) { 202 return getShortField(objref, "value"); 203 } 204 205 public int getIntValue (int objref) { 206 return getIntField(objref, "value"); 207 } 208 209 public long getLongValue (int objref) { 210 return getLongField(objref, "value"); 211 } 212 213 public float getFloatValue (int objref) { 214 return getFloatField(objref, "value"); 215 } 216 217 public double getDoubleValue (int objref) { 218 return getDoubleField(objref, "value"); 219 } 220 221 222 public void setLongArrayElement (int objref, int index, long value) { 223 da.get(objref).setLongElement(index, value); 224 } 225 226 public long getLongArrayElement (int objref, int index) { 227 return da.get(objref).getLongElement(index); 228 } 229 230 public void setLongField (int objref, String fname, long val) { 231 setLongField(objref, null, fname, val); 232 } 233 234 public void setLongField (int objref, String refType, String fname, long val) { 235 ElementInfo ei = da.get(objref); 236 ei.setLongField(fname, refType, val); 237 } 238 239 public long getLongField (int objref, String fname) { 240 return getLongField(objref, null, fname); 241 } 242 243 public long getLongField (int objref, String refType, String fname) { 244 ElementInfo ei = da.get(objref); 245 246 return ei.getLongField(fname, refType); 247 } 248 249 public void setReferenceArrayElement (int objref, int index, int eRef) { 250 da.get(objref).setElement(index, eRef); 251 } 252 253 public int getReferenceArrayElement (int objref, int index) { 254 return da.get(objref).getElement(index); 255 } 256 257 public void setShortField (int objref, String fname, short val) { 258 setIntField(objref, null, fname, (int) val); 259 } 260 261 public short getShortField (int objref, String fname) { 262 return (short) getIntField(objref, null, fname); 263 } 264 265 public String getTypeName (int objref) { 266 return da.get(objref).getType(); 267 } 268 269 public boolean isInstanceOf (int objref, String clsName) { 270 ClassInfo ci = getClassInfo(objref); 271 return ci.instanceOf(clsName); 272 } 273 274 public void setStaticBooleanField (String clsName, String fname, 276 boolean value) { 277 setStaticIntField(clsName, fname, Types.booleanToInt(value)); 278 } 279 280 public boolean getStaticBooleanField (String clsName, String fname) { 281 return Types.intToBoolean(getStaticIntField(clsName, fname)); 282 } 283 284 public void setStaticByteField (String clsName, String fname, byte value) { 285 setStaticIntField(clsName, fname, (int) value); 286 } 287 288 public byte getStaticByteField (String clsName, String fname) { 289 return (byte) getStaticIntField(clsName, fname); 290 } 291 292 public void setStaticCharField (String clsName, String fname, char value) { 293 setStaticIntField(clsName, fname, (int) value); 294 } 295 296 public char getStaticCharField (String clsName, String fname) { 297 return (char) getStaticIntField(clsName, fname); 298 } 299 300 public void setStaticDoubleField (String clsName, String fname, double val) { 301 setStaticLongField(clsName, fname, Types.doubleToLong(val)); 302 } 303 304 public double getStaticDoubleField (String clsName, String fname) { 305 return Types.longToDouble(getStaticLongField(clsName, fname)); 306 } 307 308 public void setStaticFloatField (String clsName, String fname, float value) { 309 setStaticIntField(clsName, fname, Types.floatToInt(value)); 310 } 311 312 public float getStaticFloatField (String clsName, String fname) { 313 return Types.intToFloat(getStaticIntField(clsName, fname)); 314 } 315 316 public void setStaticIntField (String clsName, String fname, int value) { 317 ClassInfo ci = ClassInfo.getClassInfo(clsName); 318 sa.get(ci.getName()).setIntField(fname, null, value); 319 } 320 321 public void setStaticIntField (int clsObjRef, String fname, int val) { 322 try { 323 ElementInfo cei = getClassElementInfo(clsObjRef); 324 cei.setIntField(fname, val); 325 } catch (Throwable x) { 326 throw new JPFException("set static field failed: " + x.getMessage()); 327 } 328 } 329 330 public int getStaticIntField (String clsName, String fname) { 331 ClassInfo ci = ClassInfo.getClassInfo(clsName); 332 StaticElementInfo ei = sa.get(ci.getName()); 333 334 return ei.getIntField(fname, null); 335 } 336 337 public void setStaticLongField (String clsName, String fname, long value) { 338 ClassInfo ci = ClassInfo.getClassInfo(clsName); 339 sa.get(ci.getName()).setLongField(fname, value); 340 } 341 342 public long getStaticLongField (String clsName, String fname) { 343 ClassInfo ci = ClassInfo.getClassInfo(clsName); 344 StaticElementInfo ei = sa.get(ci.getName()); 345 346 return ei.getLongField(fname, null); 347 } 348 349 public void setStaticReferenceField (String clsName, String fname, int objref) { 350 ClassInfo ci = ClassInfo.getClassInfo(clsName); 351 352 sa.get(ci.getName()).setReferenceField(fname, objref); 354 } 355 356 public int getStaticObjectField (String clsName, String fname) { 357 return getStaticIntField(clsName, fname); 358 } 359 360 public short getStaticShortField (String clsName, String fname) { 361 return (short) getStaticIntField(clsName, fname); 362 } 363 364 368 public String getStringObject (int objref) { 369 if (objref != -1) { 370 ElementInfo ei = getElementInfo(objref); 371 return ei.asString(); 372 } else { 373 return null; 374 } 375 } 376 377 public byte[] getByteArrayObject (int objref) { 378 ElementInfo ei = getElementInfo(objref); 379 byte[] a = ei.asByteArray(); 380 381 return a; 382 } 383 384 public char[] getCharArrayObject (int objref) { 385 ElementInfo ei = getElementInfo(objref); 386 char[] a = ei.asCharArray(); 387 388 return a; 389 } 390 391 public short[] getShortArrayObject (int objref) { 392 ElementInfo ei = getElementInfo(objref); 393 short[] a = ei.asShortArray(); 394 395 return a; 396 } 397 398 public int[] getIntArrayObject (int objref) { 399 ElementInfo ei = getElementInfo(objref); 400 int[] a = ei.asIntArray(); 401 402 return a; 403 } 404 405 public long[] getLongArrayObject (int objref) { 406 ElementInfo ei = getElementInfo(objref); 407 long[] a = ei.asLongArray(); 408 409 return a; 410 } 411 412 public float[] getFloatArrayObject (int objref) { 413 ElementInfo ei = getElementInfo(objref); 414 float[] a = ei.asFloatArray(); 415 416 return a; 417 } 418 419 public double[] getDoubleArrayObject (int objref) { 420 ElementInfo ei = getElementInfo(objref); 421 double[] a = ei.asDoubleArray(); 422 423 return a; 424 } 425 426 public boolean[] getBooleanArrayObject (int objref) { 427 ElementInfo ei = getElementInfo(objref); 428 boolean[] a = ei.asBooleanArray(); 429 430 return a; 431 } 432 433 434 public boolean canLock (int objref) { 435 ElementInfo ei = getElementInfo(objref); 436 437 return ei.canLock(ti); 438 } 439 440 public int newBooleanArray (int size) { 441 return da.newArray("Z", size, ti); 442 } 443 444 public int newByteArray (int size) { 445 return da.newArray("B", size, ti); 446 } 447 448 public int newCharArray (int size) { 449 return da.newArray("C", size, ti); 450 } 451 452 public int newDoubleArray (int size) { 453 return da.newArray("D", size, ti); 454 } 455 456 public int newFloatArray (int size) { 457 return da.newArray("F", size, ti); 458 } 459 460 public int newIntArray (int size) { 461 return da.newArray("I", size, ti); 462 } 463 464 public int newLongArray (int size) { 465 return da.newArray("J", size, ti); 466 } 467 468 public int newObject (String clsName) { 469 ClassInfo ci = ClassInfo.getClassInfo(clsName); 471 472 return da.newObject(ci, ti); 473 } 474 475 public int newObjectArray (String clsName, int size) { 476 return da.newArray(clsName, size, ti); 477 } 478 479 public int newShortArray (int size) { 480 return da.newArray("S", size, ti); 481 } 482 483 public int newString (String s) { 484 return da.newString(s, ti); 485 } 486 487 public int newString (int arrayRef) { 488 int r = NULL; 489 String t = getArrayType(arrayRef); 490 String s = null; 491 492 if ("C".equals(t)) { char[] ca = getCharArrayObject(arrayRef); 494 s = new String (ca); 495 } else if ("B".equals(t)) { byte[] ba = getByteArrayObject(arrayRef); 497 s = new String (ba); 498 } 499 500 if (s == null) { 501 return NULL; 502 } 503 504 return newString(s); 505 } 506 507 public void notify (int objref) { 508 ElementInfo ei = getElementInfo(objref); 509 510 if (!ei.isLockedBy(ti)){ 511 throwException("java.lang.IllegalMonitorStateException", 512 "un-synchronized notify"); 513 return; 514 } 515 516 ei.notifies(); 517 } 518 519 public void notifyAll (int objref) { 520 ElementInfo ei = getElementInfo(objref); 521 522 if (!ei.isLockedBy(ti)){ 523 throwException("java.lang.IllegalMonitorStateException", 524 "un-synchronized notifyAll"); 525 return; 526 } 527 528 ei.notifiesAll(); 529 } 530 531 public void repeatInvocation () { 532 repeat = true; 533 } 534 535 public void throwException (String classname) { 536 exception = Types.asTypeName(classname); 537 } 538 539 public void throwException (String classname, String details) { 540 exception = Types.asTypeName(classname); 541 exceptionDetails = details; 542 } 543 544 public void wait (int objref) { 545 ElementInfo ei = getElementInfo(objref); 546 547 if (!ei.isLockedBy(ti)){ 548 throwException("java.lang.IllegalMonitorStateException", 549 "un-synchronized wait"); 550 return; 551 } 552 553 554 ei.wait(ti); 555 } 556 557 void setCallEnvironment (MethodInfo mi) { 558 this.mi = mi; 559 560 if (mi != null){ 561 ci = mi.getClassInfo(); 562 } else { 563 } 566 567 repeat = false; 568 exception = null; 569 exceptionDetails = null; 570 } 571 572 void clearCallEnvironment () { 573 setCallEnvironment(null); 574 } 575 576 ElementInfo getClassElementInfo (int clsObjRef) { 577 ElementInfo ei = da.get(clsObjRef); 578 int cref = ei.getIntField("cref", null); 579 580 ElementInfo cei = sa.get(cref); 581 582 return cei; 583 } 584 585 ClassInfo getClassInfo () { 586 return ci; 587 } 588 589 ClassInfo getClassInfo (int objref) { 590 ElementInfo ei = getElementInfo(objref); 591 return ei.getClassInfo(); 592 } 593 594 public String getClassName (int objref) { 595 return getClassInfo(objref).getName(); 596 } 597 598 DynamicArea getDynamicArea () { 599 return JVM.getVM().getDynamicArea(); 600 } 601 602 ElementInfo getElementInfo (int objref) { 603 return da.get(objref); 604 } 605 606 int getStateId () { 607 return JVM.getVM().getStateId(); 608 } 609 610 String getException () { 611 return exception; 612 } 613 614 String getExceptionDetails () { 615 return exceptionDetails; 616 } 617 618 KernelState getKernelState () { 619 SystemState ss = getSystemState(); 620 621 return ss.ks; 622 } 623 624 MethodInfo getMethodInfo () { 625 return mi; 626 } 627 628 boolean getRepeat () { 629 return repeat; 630 } 631 632 StaticArea getStaticArea () { 633 return JVM.getVM().getStaticArea(); 634 } 635 636 SystemState getSystemState () { 637 JVM vm = JVM.getVM(); 638 639 return vm.ss; 641 } 642 643 ThreadInfo getThreadInfo () { 644 return ti; 645 } 646 647 void lockNotified (int objref) { 649 ElementInfo ei = getElementInfo(objref); 650 ei.lockNotified(ti); 651 } 652 } 653 | Popular Tags |