comparison src/main/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_vm_Verify.java @ 1:f6886b2bda4a

first set of post v7 patches general part of extendTransition optimization, which skips transition breaks (and hence state matching) if vm.extend_transitions is set, and the next CG has only a single choice that does not require a break (e.g. context switch). This is mainly meant to be a state space optimization, and complements the null return on the CG creator side, which is extension/domain specific and also cuts into observability from listeners (no CG - no CG notifications). Note this is only the first part of the patch and probably too general in most cases. The second part extends this with an interface that can control breaks dynamically (e.g. from listeners). Added a ChoiceGenerator.setCurrent() (empty by default) that can be used as a CG type specific hook to expand/modify choices once the CG becomes active Added the first part of the patch that allows SUT context expansion of EventChoiceGenerators, which is required to make the new event system work in situations that need to add additional events based on the current SUT state (e.g. statemachines with timeout events). Fix for INVOKEDYNAMIC causing a NPE for recycled/restored function objects (Nastaran's patch)
author Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date Fri, 23 Jan 2015 11:08:46 -0800
parents 61d41facf527
children caa0924e093d
comparison
equal deleted inserted replaced
0:61d41facf527 1:f6886b2bda4a
293 @MJI 293 @MJI
294 public static void breakTransition__Ljava_lang_String_2__V (MJIEnv env, int clsObjRef, int reasonRef){ 294 public static void breakTransition__Ljava_lang_String_2__V (MJIEnv env, int clsObjRef, int reasonRef){
295 ThreadInfo ti = env.getThreadInfo(); 295 ThreadInfo ti = env.getThreadInfo();
296 String reason = env.getStringObject(reasonRef); 296 String reason = env.getStringObject(reasonRef);
297 ti.breakTransition(reason); 297 ti.breakTransition(reason);
298 }
299
300 /**
301 * mostly for debugging purposes - this does not optimize away single choice CGs
302 */
303 @MJI
304 public int breakTransition__Ljava_lang_String_2II__I (MJIEnv env, int clsObjRef, int reasonRef, int min, int max) {
305 ThreadInfo ti = env.getThreadInfo();
306 SystemState ss = env.getSystemState();
307 String reason = env.getStringObject(reasonRef);
308
309 if (!ti.isFirstStepInsn()) { // first time around
310 IntChoiceGenerator cg = new IntIntervalGenerator( reason, min,max);
311 if (ss.setNextChoiceGenerator(cg)){
312 env.repeatInvocation();
313 }
314 return -1;
315
316 } else {
317 return getNextChoice(ss, reason, IntChoiceGenerator.class, Integer.class);
318 }
298 } 319 }
299 320
300 @MJI 321 @MJI
301 public static boolean isCalledFromClass__Ljava_lang_String_2__Z (MJIEnv env, int clsObjRef, 322 public static boolean isCalledFromClass__Ljava_lang_String_2__Z (MJIEnv env, int clsObjRef,
302 int clsNameRef) { 323 int clsNameRef) {