annotate src/tests/gov/nasa/jpf/test/mc/basic/ExtendTransitionTest.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
children b920e6b1be83
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
1
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
1 /*
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
2 * Copyright (C) 2014, United States Government, as represented by the
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
3 * Administrator of the National Aeronautics and Space Administration.
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
4 * All rights reserved.
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
5 *
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
6 * The Java Pathfinder core (jpf-core) platform is licensed under the
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
7 * Apache License, Version 2.0 (the "License"); you may not use this file except
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
8 * in compliance with the License. You may obtain a copy of the License at
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
9 *
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
10 * http://www.apache.org/licenses/LICENSE-2.0.
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
11 *
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
12 * Unless required by applicable law or agreed to in writing, software
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
13 * distributed under the License is distributed on an "AS IS" BASIS,
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
14 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
15 * See the License for the specific language governing permissions and
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
16 * limitations under the License.
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
17 */
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
18
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
19 package gov.nasa.jpf.test.mc.basic;
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
20
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
21 import gov.nasa.jpf.ListenerAdapter;
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
22 import gov.nasa.jpf.util.test.TestJPF;
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
23 import gov.nasa.jpf.vm.ChoiceGenerator;
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
24 import gov.nasa.jpf.vm.Instruction;
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
25 import gov.nasa.jpf.vm.ThreadInfo;
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
26 import gov.nasa.jpf.vm.VM;
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
27 import gov.nasa.jpf.vm.Verify;
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
28 import org.junit.Test;
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
29
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
30 /**
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
31 * regression test for extended transitions
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
32 */
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
33 public class ExtendTransitionTest extends TestJPF {
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
34
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
35 public static class CGListener extends ListenerAdapter {
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
36 @Override
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
37 public void choiceGeneratorRegistered (VM vm, ChoiceGenerator<?> nextCG, ThreadInfo currentThread, Instruction executedInstruction) {
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
38 System.out.println("CG registered: " + nextCG);
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
39 }
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
40
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
41 @Override
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
42 public void choiceGeneratorSet (VM vm, ChoiceGenerator<?> newCG) {
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
43 System.out.println("\nCG set: " + newCG + " by: " + newCG.getInsn());
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
44 }
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
45
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
46 @Override
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
47 public void choiceGeneratorAdvanced (VM vm, ChoiceGenerator<?> currentCG) {
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
48 System.out.println("CG advanced: " + currentCG);
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
49 }
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
50
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
51 @Override
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
52 public void choiceGeneratorProcessed (VM vm, ChoiceGenerator<?> processedCG) {
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
53 System.out.println("CG processed: " + processedCG);
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
54 }
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
55 }
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
56
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
57 @Test
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
58 public void testExtendedStateTransitions(){
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
59 if (verifyNoPropertyViolation("+vm.extend_transitions=true", "+cg.break_single_choice=false",
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
60 "+listener=" + getClass().getName() + "$CGListener")){
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
61 Verify.print("-- start\n");
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
62 for (int i=0; i<5; i++){
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
63 int n = Verify.breakTransition( "loop cycle", i, i);
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
64 Verify.print("i=", i);
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
65 Verify.print(", n=", n);
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
66 Verify.println();
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
67 }
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
68 }
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
69
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
70 if (!isJPFRun()){
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
71 int nStates = VM.getVM().getStateCount();
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
72 System.out.println("nStates=" + nStates);
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
73 }
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
74 }
f6886b2bda4a first set of post v7 patches
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
75 }