2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
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
10 * http://www.apache.org/licenses/LICENSE-2.0.
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.
18 package gov.nasa.jpf.vm;
20 import gov.nasa.jpf.Config;
21 import gov.nasa.jpf.JPF;
22 import gov.nasa.jpf.JPFException;
23 import gov.nasa.jpf.annotation.MJI;
24 import gov.nasa.jpf.util.IntTable;
25 import gov.nasa.jpf.util.JPFLogger;
26 import gov.nasa.jpf.util.ObjectConverter;
27 import gov.nasa.jpf.util.ObjectList;
28 import gov.nasa.jpf.util.RunListener;
29 import gov.nasa.jpf.util.RunRegistry;
30 import gov.nasa.jpf.util.json.CGCall;
31 import gov.nasa.jpf.util.json.JSONLexer;
32 import gov.nasa.jpf.util.json.JSONObject;
33 import gov.nasa.jpf.util.json.JSONParser;
34 import gov.nasa.jpf.vm.choice.DoubleChoiceFromList;
35 import gov.nasa.jpf.vm.choice.FloatChoiceFromList;
36 import gov.nasa.jpf.vm.choice.IntChoiceFromSet;
37 import gov.nasa.jpf.vm.choice.IntIntervalGenerator;
38 import gov.nasa.jpf.vm.choice.LongChoiceFromList;
40 import java.io.FileInputStream;
41 import java.io.FileNotFoundException;
42 import java.io.IOException;
43 import java.io.ObjectInputStream;
44 import java.io.PrintStream;
45 import java.util.BitSet;
46 import java.util.List;
49 * native peer class for programmatic JPF interface (that can be used inside
50 * of apps to verify - if you are aware of the danger that comes with it)
52 * this peer is a bit different in that it only uses static fields and methods because
53 * its use is supposed to be JPF global (without classloader namespaces)
55 public class JPF_gov_nasa_jpf_vm_Verify extends NativePeer {
56 static final int MAX_COUNTERS = 127;
58 static boolean isInitialized;
60 // those are used to store search global int values (e.g. from TestJPF derived classes)
62 static IntTable<String> map;
64 public static int heuristicSearchValue;
66 static boolean supportIgnorePath;
67 static boolean breakSingleChoice;
68 static boolean enableAtomic;
70 static Config config; // we need to keep this around for CG creation
72 // our const ChoiceGenerator ctor argtypes
73 static Class[] cgArgTypes = { Config.class, String.class };
74 // this is our cache for ChoiceGenerator ctor parameters
75 static Object[] cgArgs = { null, null };
77 static BitSet[] bitSets;
78 static int nextBitSet;
80 static PrintStream out;
82 public static boolean init (Config conf) {
85 supportIgnorePath = conf.getBoolean("vm.verify.ignore_path");
86 breakSingleChoice = conf.getBoolean("cg.break_single_choice");
87 enableAtomic = conf.getBoolean("cg.enable_atomic", true);
89 heuristicSearchValue = conf.getInt("search.heuristic.default_value");
96 String outFile = conf.getString("vm.verify.output_file");
99 out = new PrintStream(outFile);
100 } catch (FileNotFoundException fnx){
101 System.err.println("error: could not open verify output file " + outFile + ", using System.out");
108 Verify.setPeerClass( JPF_gov_nasa_jpf_vm_Verify.class);
110 RunRegistry.getDefaultRegistry().addListener( new RunListener() {
112 public void reset (RunRegistry reg){
113 isInitialized = false;
121 public static final int NO_VALUE = -1;
124 public static int getValue__Ljava_lang_String_2__I (MJIEnv env, int clsObjRef, int keyRef) {
128 String key = env.getStringObject(keyRef);
129 IntTable.Entry<String> e = map.get(key);
139 public static void putValue__Ljava_lang_String_2I__V (MJIEnv env, int clsObjRef, int keyRef, int val) {
141 map = new IntTable<String>();
144 String key = env.getStringObject(keyRef);
149 public static int getCounter__I__I (MJIEnv env, int clsObjRef, int counterId) {
150 if ((counter == null) || (counterId < 0) || (counterId >= counter.length)) {
154 return counter[counterId];
157 private static void ensureCounterCapacity (int counterId){
158 if (counter == null) {
159 counter = new int[(counterId >= MAX_COUNTERS) ? counterId+1 : MAX_COUNTERS];
160 } else if (counterId >= counter.length) {
161 int[] newCounter = new int[counterId+1];
162 System.arraycopy(counter, 0, newCounter, 0, counter.length);
163 counter = newCounter;
168 public static void resetCounter__I__V (MJIEnv env, int clsObjRef, int counterId) {
169 if ((counter == null) || (counterId < 0) || (counterId >= counter.length)) {
172 counter[counterId] = 0;
176 public static void setCounter__II__V (MJIEnv env, int clsObjRef, int counterId, int val) {
181 ensureCounterCapacity(counterId);
182 counter[counterId] = val;
186 public static int incrementCounter__I__I (MJIEnv env, int clsObjRef, int counterId) {
191 ensureCounterCapacity(counterId);
192 return ++counter[counterId];
195 private static void checkBitSetId(int id) {
196 if (bitSets == null) {
197 bitSets = new BitSet[id + 1];
198 } else if (id >= bitSets.length) {
199 BitSet[] newBitSets = new BitSet[id + 1];
200 System.arraycopy(bitSets, 0, newBitSets, 0, bitSets.length);
201 bitSets = newBitSets;
204 if (bitSets[id] == null) {
205 bitSets[id] = new BitSet();
210 public static void setBitInBitSet__IIZ__V(MJIEnv env, int clsObjRef, int id, int bitNum, boolean value) {
212 bitSets[id].set(bitNum, value);
216 public static boolean getBitInBitSet__II__Z(MJIEnv env, int clsObjRef, int id, int bitNum) {
218 return bitSets[id].get(bitNum);
222 public static long currentTimeMillis____J (MJIEnv env, int clsObjRef) {
223 return System.currentTimeMillis();
227 public static String getType (int objRef, MJIEnv env) {
228 return Types.getTypeName(env.getElementInfo(objRef).getType());
232 public static void addComment__Ljava_lang_String_2__V (MJIEnv env, int clsObjRef, int stringRef) {
233 SystemState ss = env.getSystemState();
234 String cmt = env.getStringObject(stringRef);
235 ss.getTrail().setAnnotation(cmt);
239 public static void assertTrue__Z__V (MJIEnv env, int clsObjRef, boolean b) {
241 env.throwException("java.lang.AssertionError", "assertTrue failed");
245 // those are evil - use with extreme care. If something blocks inside of
246 // an atomic section we have to raise an exception
249 public static void beginAtomic____V (MJIEnv env, int clsObjRef) {
251 ThreadInfo tiAtomic = env.getThreadInfo();
253 if (tiAtomic.getScheduler().setsBeginAtomicCG(tiAtomic)){
254 env.repeatInvocation();
258 env.getSystemState().incAtomic();
263 public static void endAtomic____V (MJIEnv env, int clsObjRef) {
265 ThreadInfo tiAtomic = env.getThreadInfo();
267 if (!tiAtomic.isFirstStepInsn()){
268 env.getSystemState().decAtomic();
271 if (tiAtomic.getScheduler().setsEndAtomicCG(tiAtomic)){
272 env.repeatInvocation();
279 public static void busyWait__J__V (MJIEnv env, int clsObjRef, long duration) {
280 // nothing required here (we systematically explore scheduling
281 // sequences anyway), but we need to intercept the call
285 public static void ignoreIf__Z__V (MJIEnv env, int clsObjRef, boolean cond) {
286 if (supportIgnorePath) {
287 env.getSystemState().setIgnored(cond);
292 public static void interesting__Z__V (MJIEnv env, int clsObjRef, boolean cond) {
293 env.getSystemState().setInteresting(cond);
297 public static void breakTransition__Ljava_lang_String_2__V (MJIEnv env, int clsObjRef, int reasonRef){
298 ThreadInfo ti = env.getThreadInfo();
299 String reason = env.getStringObject(reasonRef);
300 ti.breakTransition(reason);
304 * mostly for debugging purposes - this does not optimize away single choice CGs
307 public int breakTransition__Ljava_lang_String_2II__I (MJIEnv env, int clsObjRef, int reasonRef, int min, int max) {
308 ThreadInfo ti = env.getThreadInfo();
309 SystemState ss = env.getSystemState();
310 String reason = env.getStringObject(reasonRef);
312 if (!ti.isFirstStepInsn()) { // first time around
313 IntChoiceGenerator cg = new IntIntervalGenerator( reason, min,max);
314 if (ss.setNextChoiceGenerator(cg)){
315 env.repeatInvocation();
320 return getNextChoice(ss, reason, IntChoiceGenerator.class, Integer.class);
325 public static boolean isCalledFromClass__Ljava_lang_String_2__Z (MJIEnv env, int clsObjRef,
327 String refClassName = env.getStringObject(clsNameRef);
328 ThreadInfo ti = env.getThreadInfo();
330 StackFrame caller = ti.getLastInvokedStackFrame();
332 ClassInfo ci = caller.getClassInfo();
333 return ci.isInstanceOf(refClassName);
340 static <T extends ChoiceGenerator<?>> T createChoiceGenerator (Class<T> cgClass, SystemState ss, String id) {
344 cgArgs[1] = id; // good thing we are not multithreaded (other fields are const)
346 String key = id + ".class";
347 gen = config.getEssentialInstance(key, cgClass, cgArgTypes, cgArgs);
351 static <T> T registerChoiceGenerator (MJIEnv env, SystemState ss, ThreadInfo ti, ChoiceGenerator<T> cg, T dummyVal){
353 int n = cg.getTotalNumberOfChoices();
355 // nothing, just return the default value
357 } else if (n == 1 && !breakSingleChoice) {
358 // no choice -> no CG optimization
360 return cg.getNextChoice();
363 if (ss.setNextChoiceGenerator(cg)){
364 env.repeatInvocation();
371 static <T,C extends ChoiceGenerator<T>> T getNextChoice (SystemState ss, String id, Class<C> cgClass, Class<T> choiceClass){
372 ChoiceGenerator<?> cg = ss.getCurrentChoiceGenerator(id, cgClass);
374 assert (cg != null) : "no ChoiceGenerator of type " + cgClass.getName();
375 return ((ChoiceGenerator<T>)cg).getNextChoice();
379 public static boolean getBoolean____Z (MJIEnv env, int clsObjRef) {
380 ThreadInfo ti = env.getThreadInfo();
381 SystemState ss = env.getSystemState();
382 ChoiceGenerator<?> cg;
384 if (!ti.isFirstStepInsn()) { // first time around
385 cg = new BooleanChoiceGenerator(config, "verifyGetBoolean");
386 if (ss.setNextChoiceGenerator(cg)){
387 env.repeatInvocation();
389 return true; // not used if we repeat
391 } else { // this is what really returns results
392 return getNextChoice(ss,"verifyGetBoolean", BooleanChoiceGenerator.class,Boolean.class);
397 public static boolean getBoolean__Z__Z (MJIEnv env, int clsObjRef, boolean falseFirst) {
398 ThreadInfo ti = env.getThreadInfo();
399 SystemState ss = env.getSystemState();
400 ChoiceGenerator<?> cg;
402 if (!ti.isFirstStepInsn()) { // first time around
403 cg = new BooleanChoiceGenerator( "verifyGetBoolean(Z)", falseFirst );
404 if (ss.setNextChoiceGenerator(cg)){
405 env.repeatInvocation();
407 return true; // not used if we repeat
409 } else { // this is what really returns results
410 return getNextChoice(ss,"verifyGetBoolean(Z)", BooleanChoiceGenerator.class, Boolean.class);
415 public static int getInt__II__I (MJIEnv env, int clsObjRef, int min, int max) {
416 ThreadInfo ti = env.getThreadInfo();
417 SystemState ss = env.getSystemState();
419 if (!ti.isFirstStepInsn()) { // first time around
427 IntChoiceGenerator cg = new IntIntervalGenerator( "verifyGetInt(II)", min,max);
428 return registerChoiceGenerator(env,ss,ti,cg,0);
431 return getNextChoice(ss, "verifyGetInt(II)", IntChoiceGenerator.class, Integer.class);
435 static int getIntFromList (MJIEnv env, int[] values){
436 ThreadInfo ti = env.getThreadInfo();
437 SystemState ss = env.getSystemState();
439 if (!ti.isFirstStepInsn()) { // first time around
440 ChoiceGenerator<Integer> cg = new IntChoiceFromSet( "verifyGetIntSet([I)", values);
441 return registerChoiceGenerator(env,ss,ti,cg,0);
444 return getNextChoice(ss, "verifyGetIntSet([I)", IntChoiceGenerator.class, Integer.class);
449 public static int getIntFromList___3I__I (MJIEnv env, int clsObjRef, int valArrayRef){
450 int[] values = env.getIntArrayObject(valArrayRef);
451 return getIntFromList( env, values);
455 public static int getInt__Ljava_lang_String_2__I (MJIEnv env, int clsObjRef, int idRef) {
456 ThreadInfo ti = env.getThreadInfo();
457 SystemState ss = env.getSystemState();
460 if (!ti.isFirstStepInsn()) { // first time around
461 String id = env.getStringObject(idRef);
462 IntChoiceGenerator cg = createChoiceGenerator( IntChoiceGenerator.class, ss, id);
463 return registerChoiceGenerator(env,ss,ti,cg, 0);
466 String id = env.getStringObject(idRef);
467 return getNextChoice(ss, id, IntChoiceGenerator.class,Integer.class);
471 static long getLongFromList (MJIEnv env, long[] values){
472 ThreadInfo ti = env.getThreadInfo();
473 SystemState ss = env.getSystemState();
475 if (!ti.isFirstStepInsn()) { // first time around
476 ChoiceGenerator<Long> cg = new LongChoiceFromList( "verifyLongList([J)", values);
477 return registerChoiceGenerator(env,ss,ti,cg,0L);
480 return getNextChoice(ss, "verifyLongList([J)", LongChoiceGenerator.class, Long.class);
485 public static long getLongFromList___3J__J (MJIEnv env, int clsObjRef, int valArrayRef){
486 long[] values = env.getLongArrayObject(valArrayRef);
487 return getLongFromList( env, values);
491 public static int getObject__Ljava_lang_String_2__Ljava_lang_Object_2 (MJIEnv env, int clsObjRef, int idRef) {
492 ThreadInfo ti = env.getThreadInfo();
493 SystemState ss = env.getSystemState();
495 if (!ti.isFirstStepInsn()) { // first time around
496 String id = env.getStringObject(idRef);
497 ReferenceChoiceGenerator cg = createChoiceGenerator( ReferenceChoiceGenerator.class, ss, id);
498 return registerChoiceGenerator(env,ss,ti,cg, MJIEnv.NULL);
501 String id = env.getStringObject(idRef);
502 return getNextChoice(ss, id, ReferenceChoiceGenerator.class,Integer.class);
507 public static double getDouble__Ljava_lang_String_2__D (MJIEnv env, int clsObjRef, int idRef) {
508 ThreadInfo ti = env.getThreadInfo();
509 SystemState ss = env.getSystemState();
511 if (!ti.isFirstStepInsn()) { // first time around
512 String id = env.getStringObject(idRef);
513 DoubleChoiceGenerator cg = createChoiceGenerator( DoubleChoiceGenerator.class, ss, id);
514 return registerChoiceGenerator(env,ss,ti,cg, 0.0);
517 String id = env.getStringObject(idRef);
518 return getNextChoice(ss, id, DoubleChoiceGenerator.class,Double.class);
523 public static double getDoubleFromList (MJIEnv env, double[] values){
524 ThreadInfo ti = env.getThreadInfo();
525 SystemState ss = env.getSystemState();
527 if (!ti.isFirstStepInsn()) { // first time around
528 ChoiceGenerator<Double> cg = new DoubleChoiceFromList("verifyDoubleList([D)", values);
529 return registerChoiceGenerator(env,ss,ti,cg, 0.0);
532 return getNextChoice(ss, "verifyDoubleList([D)", DoubleChoiceFromList.class,Double.class);
537 public static double getDoubleFromList___3D__D (MJIEnv env, int clsObjRef, int valArrayRef){
538 double[] values = env.getDoubleArrayObject(valArrayRef);
539 return getDoubleFromList( env, values);
543 public static float getFloatFromList (MJIEnv env, float[] values){
544 ThreadInfo ti = env.getThreadInfo();
545 SystemState ss = env.getSystemState();
547 if (!ti.isFirstStepInsn()) { // first time around
548 ChoiceGenerator<Float> cg = new FloatChoiceFromList("verifyFloatList([F)", values);
549 return registerChoiceGenerator(env,ss,ti,cg, 0.0f);
552 return getNextChoice(ss, "verifyFloatList([F)", FloatChoiceFromList.class, Float.class);
557 public static float getFloatFromList___3F__F (MJIEnv env, int clsObjRef, int valArrayRef){
558 float[] values = env.getFloatArrayObject(valArrayRef);
559 return getFloatFromList( env, values);
563 public static void threadPrint__Ljava_lang_String_2__V (MJIEnv env, int clsRef, int sRef){
564 String s = env.getStringObject(sRef);
565 ThreadInfo ti = env.getThreadInfo();
566 System.out.print(ti.getName());
571 public static void print__Ljava_lang_String_2I__V (MJIEnv env, int clsRef, int sRef, int val){
572 String s = env.getStringObject(sRef);
573 System.out.print(s + " : " + val);
577 public static void print__Ljava_lang_String_2Z__V (MJIEnv env, int clsRef, int sRef, boolean val){
578 String s = env.getStringObject(sRef);
579 System.out.print(s + " : " + val);
583 public static void print___3Ljava_lang_String_2__V (MJIEnv env, int clsRef, int argsRef){
584 int n = env.getArrayLength(argsRef);
585 for (int i=0; i<n; i++){
586 int aref = env.getReferenceArrayElement(argsRef, i);
587 String s = env.getStringObject(aref);
593 public static void print__Ljava_lang_String_2__V (MJIEnv env, int clsRef, int sRef){
594 String s = env.getStringObject(sRef);
599 public static void println__Ljava_lang_String_2__V (MJIEnv env, int clsRef, int sRef){
600 String s = env.getStringObject(sRef);
601 System.out.println(s);
605 public static void threadPrintln__Ljava_lang_String_2__V (MJIEnv env, int clsRef, int sRef){
606 threadPrint__Ljava_lang_String_2__V(env, clsRef, sRef);
607 System.out.println();
612 public static void println____V (MJIEnv env, int clsRef){
613 System.out.println();
616 //--- various attribute test methods
618 private static int getAttribute (MJIEnv env, Object a){
620 if (a instanceof Integer) {
621 return ((Integer) a).intValue();
623 env.throwException("java.lang.RuntimeException", "element attribute not an Integer: " + a);
630 private static int getAttributeList (MJIEnv env, Object a){
632 int l = ObjectList.size(a);
633 int[] attrs = new int[l];
635 for (Integer v : ObjectList.typedIterator(a, Integer.class)) {
639 env.throwException("java.lang.RuntimeException", "found non-Integer attributes");
643 return env.newIntArray(attrs);
651 public static void setObjectAttribute__Ljava_lang_Object_2I__V (MJIEnv env, int clsRef, int oRef, int attr){
652 if (oRef != MJIEnv.NULL){
653 ElementInfo ei = env.getElementInfo(oRef);
654 ei.setObjectAttr(Integer.valueOf(attr));
659 public static int getObjectAttribute__Ljava_lang_Object_2__I (MJIEnv env, int clsRef, int oRef){
660 if (oRef != MJIEnv.NULL){
661 ElementInfo ei = env.getElementInfo(oRef);
662 return getAttribute( env, ei.getObjectAttr());
669 public static void addObjectAttribute__Ljava_lang_Object_2I__V (MJIEnv env, int clsRef, int oRef, int attr){
670 if (oRef != MJIEnv.NULL){
671 ElementInfo ei = env.getElementInfo(oRef);
672 ei.addObjectAttr(Integer.valueOf(attr));
677 public static int getObjectAttributes__Ljava_lang_Object_2___3I (MJIEnv env, int clsRef, int oRef){
678 if (oRef != MJIEnv.NULL){
679 ElementInfo ei = env.getElementInfo(oRef);
680 return getAttributeList( env, ei.getObjectAttr());
687 public static void setFieldAttribute__Ljava_lang_Object_2Ljava_lang_String_2I__V (MJIEnv env, int clsRef,
688 int oRef, int fnRef, int attr){
689 if (oRef != MJIEnv.NULL){
690 ElementInfo ei = env.getElementInfo(oRef);
692 String fname = env.getStringObject(fnRef);
693 FieldInfo fi = ei.getFieldInfo(fname);
696 ei.setFieldAttr(fi, Integer.valueOf(attr));
698 env.throwException("java.lang.NoSuchFieldException",
699 ei.getClassInfo().getName() + '.' + fname);
702 env.throwException("java.lang.RuntimeException", "illegal reference value: " + oRef);
708 public static int getFieldAttribute__Ljava_lang_Object_2Ljava_lang_String_2__I (MJIEnv env, int clsRef,
709 int oRef, int fnRef){
710 if (oRef != MJIEnv.NULL){
711 ElementInfo ei = env.getElementInfo(oRef);
713 String fname = env.getStringObject(fnRef);
714 FieldInfo fi = ei.getFieldInfo(fname);
717 return getAttribute( env, ei.getFieldAttr(fi));
719 env.throwException("java.lang.NoSuchFieldException",
720 ei.toString() + '.' + fname);
723 env.throwException("java.lang.RuntimeException", "illegal reference value: " + oRef);
731 public static void addFieldAttribute__Ljava_lang_Object_2Ljava_lang_String_2I__V (MJIEnv env, int clsRef,
732 int oRef, int fnRef, int attr){
733 if (oRef != MJIEnv.NULL){
734 ElementInfo ei = env.getElementInfo(oRef);
736 String fname = env.getStringObject(fnRef);
737 FieldInfo fi = ei.getFieldInfo(fname);
740 ei.addFieldAttr(fi, Integer.valueOf(attr));
742 env.throwException("java.lang.NoSuchFieldException",
743 ei.getClassInfo().getName() + '.' + fname);
746 env.throwException("java.lang.RuntimeException", "illegal reference value: " + oRef);
752 public static int getFieldAttributes__Ljava_lang_Object_2Ljava_lang_String_2___3I (MJIEnv env, int clsRef,
753 int oRef, int fnRef){
754 if (oRef != MJIEnv.NULL){
755 ElementInfo ei = env.getElementInfo(oRef);
757 String fname = env.getStringObject(fnRef);
758 FieldInfo fi = ei.getFieldInfo(fname);
761 return getAttributeList( env, ei.getFieldAttr(fi));
763 env.throwException("java.lang.NoSuchFieldException",
764 ei.toString() + '.' + fname);
767 env.throwException("java.lang.RuntimeException", "illegal reference value: " + oRef);
775 public static void setLocalAttribute__Ljava_lang_String_2I__V (MJIEnv env, int clsRef, int varRef, int attr) {
776 String slotName = env.getStringObject(varRef);
777 StackFrame frame = env.getModifiableCallerStackFrame(); // we are executing in a NativeStackFrame
779 if (!frame.getMethodInfo().isStatic() && slotName.equals("this")) {
780 frame.setLocalAttr(0, Integer.valueOf(attr)); // only for instance methods of course
783 int slotIdx = frame.getLocalVariableSlotIndex(slotName);
785 frame.setLocalAttr(slotIdx, Integer.valueOf(attr));
787 env.throwException("java.lang.RuntimeException", "local variable not found: " + slotName);
793 public static int getLocalAttribute__Ljava_lang_String_2__I (MJIEnv env, int clsRef, int varRef) {
794 String slotName = env.getStringObject(varRef);
795 ThreadInfo ti = env.getThreadInfo();
796 StackFrame frame = env.getCallerStackFrame();
798 int slotIdx = frame.getLocalVariableSlotIndex(slotName);
800 return getAttribute( env, frame.getLocalAttr(slotIdx));
802 env.throwException("java.lang.RuntimeException", "local variable not found: " + slotName);
808 public static void addLocalAttribute__Ljava_lang_String_2I__V (MJIEnv env, int clsRef, int varRef, int attr) {
809 String slotName = env.getStringObject(varRef);
810 StackFrame frame = env.getModifiableCallerStackFrame(); // we are executing in a NativeStackFrame
812 if (!frame.getMethodInfo().isStatic() && slotName.equals("this")) {
813 frame.addLocalAttr(0, Integer.valueOf(attr)); // only for instance methods of course
816 int slotIdx = frame.getLocalVariableSlotIndex(slotName);
818 frame.addLocalAttr(slotIdx, Integer.valueOf(attr));
820 env.throwException("java.lang.RuntimeException", "local variable not found: " + slotName);
826 public static int getLocalAttributes__Ljava_lang_String_2___3I (MJIEnv env, int clsRef, int varRef) {
827 String slotName = env.getStringObject(varRef);
828 ThreadInfo ti = env.getThreadInfo();
829 StackFrame frame = env.getCallerStackFrame();
831 int slotIdx = frame.getLocalVariableSlotIndex(slotName);
833 return getAttributeList( env, frame.getLocalAttr(slotIdx));
835 env.throwException("java.lang.RuntimeException", "local variable not found: " + slotName);
842 public static void setElementAttribute__Ljava_lang_Object_2II__V (MJIEnv env, int clsRef,
843 int oRef, int idx, int attr){
844 if (oRef != MJIEnv.NULL){
845 ElementInfo ei = env.getElementInfo(oRef);
849 if (idx < ei.arrayLength()) {
850 ei.setElementAttr(idx, Integer.valueOf(attr));
852 env.throwException("java.lang.ArrayIndexOutOfBoundsException",
853 Integer.toString(idx));
856 env.throwException("java.lang.RuntimeException",
857 "not an array: " + ei);
860 env.throwException("java.lang.RuntimeException", "illegal reference value: " + oRef);
866 public static int getElementAttribute__Ljava_lang_Object_2I__I (MJIEnv env, int clsRef,
868 if (oRef != MJIEnv.NULL){
869 ElementInfo ei = env.getElementInfo(oRef);
873 if (idx < ei.arrayLength()) {
874 return getAttribute( env, ei.getElementAttr( idx));
876 env.throwException("java.lang.ArrayIndexOutOfBoundsException",
877 Integer.toString(idx));
880 env.throwException("java.lang.RuntimeException",
881 "not an array: " + ei);
884 env.throwException("java.lang.RuntimeException", "illegal reference value: " + oRef);
892 public static void addElementAttribute__Ljava_lang_Object_2II__V (MJIEnv env, int clsRef,
893 int oRef, int idx, int attr){
894 if (oRef != MJIEnv.NULL){
895 ElementInfo ei = env.getElementInfo(oRef);
899 if (idx < ei.arrayLength()) {
900 ei.addElementAttr(idx, Integer.valueOf(attr));
902 env.throwException("java.lang.ArrayIndexOutOfBoundsException",
903 Integer.toString(idx));
906 env.throwException("java.lang.RuntimeException",
907 "not an array: " + ei);
910 env.throwException("java.lang.RuntimeException", "illegal reference value: " + oRef);
916 public static int getElementAttributes__Ljava_lang_Object_2I___3I (MJIEnv env, int clsRef,
918 if (oRef != MJIEnv.NULL){
919 ElementInfo ei = env.getElementInfo(oRef);
922 if (idx < ei.arrayLength()) {
923 return getAttributeList( env, ei.getElementAttr( idx));
925 env.throwException("java.lang.ArrayIndexOutOfBoundsException",
926 Integer.toString(idx));
929 env.throwException("java.lang.RuntimeException",
930 "not an array: " + ei);
933 env.throwException("java.lang.RuntimeException", "illegal reference value: " + oRef);
942 * deprecated, use getBoolean()
945 public static boolean randomBool (MJIEnv env, int clsObjRef) {
946 //SystemState ss = env.getSystemState();
947 //return (ss.random(2) != 0);
949 return getBoolean____Z(env, clsObjRef);
955 * deprecated, use getInt
958 public static int random__I__I (MJIEnv env, int clsObjRef, int x) {
959 return getInt__II__I(env, clsObjRef, 0, x);
962 static void boring__Z__V (MJIEnv env, int clsObjRef, boolean b) {
963 env.getSystemState().setBoring(b);
967 public static boolean isRunningInJPF____Z(MJIEnv env, int clsObjRef) {
972 public static boolean vmIsMatchingStates____Z(MJIEnv env, int clsObjRef) {
973 return env.getVM().getStateSet() != null;
977 public static void storeTrace__Ljava_lang_String_2Ljava_lang_String_2__V (MJIEnv env, int clsObjRef,
978 int filenameRef, int commentRef) {
979 String fileName = env.getStringObject(filenameRef);
980 String comment = env.getStringObject(commentRef);
981 env.getVM().storeTrace(fileName, comment, config.getBoolean("trace.verbose", false));
985 public static void terminateSearch____V (MJIEnv env, int clsObjRef) {
986 JPF jpf = env.getVM().getJPF();
987 jpf.getSearch().terminate();
990 @MJI public static void setHeuristicSearchValue__I__V (MJIEnv env, int clsObjRef, int val){
991 heuristicSearchValue = val;
994 @MJI public static int getHeuristicSearchValue____I (MJIEnv env, int clsObjRef){
995 return heuristicSearchValue;
998 @MJI public static void resetHeuristicSearchValue____V (MJIEnv env, int clsObjRef){
999 heuristicSearchValue = config.getInt("search.heuristic.default_value");
1005 public static boolean isTraceReplay____Z (MJIEnv env, int clsObjRef) {
1006 return env.getVM().isTraceReplay();
1010 public static boolean isShared__Ljava_lang_Object_2__Z (MJIEnv env, int clsObjRef, int objRef){
1011 if (objRef != MJIEnv.NULL){
1012 ElementInfo ei = env.getElementInfo(objRef);
1014 return ei.isShared();
1022 public static void setShared__Ljava_lang_Object_2Z__V (MJIEnv env, int clsObjRef, int objRef, boolean isShared) {
1023 if (objRef != MJIEnv.NULL){
1024 ElementInfo ei = env.getElementInfo(objRef);
1026 if (ei.getClassInfo() == ClassLoaderInfo.getCurrentSystemClassLoader().getClassClassInfo()) {
1027 // it's a class object, set static fields shared
1028 ei = env.getStaticElementInfo(objRef);
1031 if (ei.isShared() != isShared) {
1032 ei = ei.getModifiableInstance();
1033 ei.setShared( env.getThreadInfo(), isShared);
1040 public static void freezeSharedness__Ljava_lang_Object_2Z__V (MJIEnv env, int clsObjRef, int objRef, boolean freeze) {
1041 if (objRef != MJIEnv.NULL){
1042 ElementInfo ei = env.getElementInfo(objRef);
1044 if (ei.getClassInfo() == ClassLoaderInfo.getCurrentSystemClassLoader().getClassClassInfo()) {
1045 // it's a class object, freeze sharedness of static fields
1046 ei = env.getStaticElementInfo(objRef);
1049 if (ei.isSharednessFrozen() != freeze) {
1050 ei = ei.getModifiableInstance();
1051 ei.freezeSharedness(freeze);
1058 public static void setProperties___3Ljava_lang_String_2__V (MJIEnv env, int clsObjRef, int argRef) {
1059 if (argRef != MJIEnv.NULL) {
1060 Config conf = env.getConfig();
1062 int n = env.getArrayLength(argRef);
1063 for (int i=0; i<n; i++) {
1064 int pRef = env.getReferenceArrayElement(argRef, i);
1065 if (pRef != MJIEnv.NULL) {
1066 String p = env.getStringObject(pRef);
1074 public static int getProperty__Ljava_lang_String_2__Ljava_lang_String_2 (MJIEnv env, int clsObjRef, int keyRef) {
1075 if (keyRef != MJIEnv.NULL){
1076 Config conf = env.getConfig();
1078 String key = env.getStringObject(keyRef);
1079 String val = config.getString(key);
1082 return env.newString(val);
1093 public static void printPathOutput__ZLjava_lang_String_2__V (MJIEnv env, int clsObjRef, boolean cond, int msgRef){
1095 printPathOutput__Ljava_lang_String_2__V(env,clsObjRef,msgRef);
1100 public static void printPathOutput__Ljava_lang_String_2__V (MJIEnv env, int clsObjRef, int msgRef){
1101 VM vm = env.getVM();
1103 System.out.println();
1104 if (msgRef != MJIEnv.NULL){
1105 String msg = env.getStringObject(msgRef);
1106 System.out.println("~~~~~~~~~~~~~~~~~~~~~~~ begin program output at: " + msg);
1108 System.out.println("~~~~~~~~~~~~~~~~~~~~~~~ begin path output");
1111 for (Transition t : vm.getPath()) {
1112 String s = t.getOutput();
1114 System.out.print(s);
1118 // we might be in the middle of a transition that isn't stored yet in the path
1119 String s = vm.getPendingOutput();
1121 System.out.print(s);
1124 System.out.println("~~~~~~~~~~~~~~~~~~~~~~~ end path output");
1128 // the JSON object initialization
1130 public static int createFromJSON__Ljava_lang_Class_2Ljava_lang_String_2__Ljava_lang_Object_2(
1131 MJIEnv env, int clsObjRef, int newObjClsRef, int jsonStringRef) {
1132 ThreadInfo ti = env.getThreadInfo();
1133 SystemState ss = env.getSystemState();
1135 String jsonString = env.getStringObject(jsonStringRef);
1136 JSONLexer lexer = new JSONLexer(jsonString);
1137 JSONParser parser = new JSONParser(lexer);
1138 JSONObject jsonObject = parser.parse();
1140 if (jsonObject != null) {
1141 ClassInfo ci = env.getReferredClassInfo( newObjClsRef);
1143 // check if we need any class init (and hence reexecution) before creating any CGs
1144 if (jsonObject.requiresClinitExecution(ci,ti)){
1145 env.repeatInvocation();
1149 if (!ti.isFirstStepInsn()) {
1150 // Top half - get and register CGs we need to set to fill object from JSON
1151 List<ChoiceGenerator<?>> cgList = CGCall.createCGList(jsonObject);
1152 if (cgList.isEmpty()){
1153 return jsonObject.fillObject(env, ci, null, "");
1156 for (ChoiceGenerator<?> cg : cgList) {
1157 ss.setNextChoiceGenerator(cg);
1160 env.repeatInvocation();
1165 // Bottom half - fill object with JSON and current values of CGs
1166 ChoiceGenerator<?>[] cgs = ss.getChoiceGenerators();
1168 return jsonObject.fillObject(env, ci, cgs, "");
1177 public static int readObjectFromFile__Ljava_lang_Class_2Ljava_lang_String_2__Ljava_lang_Object_2(
1178 MJIEnv env, int clsObjRef, int newObjClsRef, int fileNameRef) {
1179 int typeNameRef = env.getReferenceField(newObjClsRef, "name");
1180 String typeName = env.getStringObject(typeNameRef);
1181 String fileName = env.getStringObject(fileNameRef);
1185 FileInputStream fis = new FileInputStream(fileName);
1186 ObjectInputStream ois = new ObjectInputStream(fis);
1187 Object javaObject = ois.readObject();
1188 String readObjectTypeName = javaObject.getClass().getCanonicalName();
1190 int readObjRef = ObjectConverter.JPFObjectFromJavaObject(env, javaObject);
1194 } catch (ClinitRequired clix){
1195 env.repeatInvocation();
1198 } catch (IOException iox){
1199 throw new JPFException("failure reading object from file: " + fileName, iox);
1200 } catch (ClassNotFoundException cnfx){
1201 throw new JPFException("failure reading object from file: " + fileName, cnfx);
1205 //--- those need to be kept in sync with the model side
1206 public static final int SEVERE = 1;
1207 public static final int WARNING = 2;
1208 public static final int INFO = 3;
1209 public static final int FINE = 4;
1210 public static final int FINER = 5;
1211 public static final int FINEST = 6;
1214 private static void log (JPFLogger logger, int logLevel, String msg){
1217 logger.severe( msg);
1220 logger.warning( msg);
1232 logger.finest( msg);
1235 throw new JPFException("unknown log level " + logLevel + " for logger " + logger.getName());
1240 public static void log__Ljava_lang_String_2ILjava_lang_String_2__V (MJIEnv env, int clsObjRef,
1241 int loggerIdRef, int logLevel, int msgRef){
1242 String loggerId = env.getStringObject(loggerIdRef);
1243 String msg = env.getStringObject(msgRef);
1244 JPFLogger logger = JPF.getLogger(loggerId);
1246 log( logger, logLevel, msg);
1250 public static void log__Ljava_lang_String_2ILjava_lang_String_2Ljava_lang_String_2__V (MJIEnv env, int clsObjRef,
1251 int loggerIdRef, int logLevel, int arg1Ref, int arg2Ref){
1252 String loggerId = env.getStringObject(loggerIdRef);
1253 String msg = env.getStringObject(arg1Ref) + env.getStringObject(arg2Ref);
1254 JPFLogger logger = JPF.getLogger(loggerId);
1256 log( logger, logLevel, msg);
1260 public static void log__Ljava_lang_String_2ILjava_lang_String_2_3Ljava_lang_Object_2__V (MJIEnv env, int clsObjRef,
1261 int loggerIdRef, int logLevel, int fmtRef, int argsRef){
1262 String loggerId = env.getStringObject(loggerIdRef);
1263 String fmt = env.getStringObject(fmtRef);
1264 JPFLogger logger = JPF.getLogger(loggerId);
1266 int[] argRefs = env.getReferenceArrayObject( argsRef);
1267 Object[] args = new Object[argRefs.length];
1268 for (int i=0; i<args.length; i++){
1269 ElementInfo eiArg = env.getElementInfo(argRefs[i]);
1270 if (eiArg.isStringObject()){
1271 args[i] = env.getStringObject(argRefs[i]);
1272 } else if (eiArg.isBoxObject()){
1273 args[i] = eiArg.asBoxObject();
1275 args[i] = eiArg.toString();
1279 String msg = String.format(fmt, args);
1281 log( logger, logLevel, msg);