Mercurial > hg > Members > kono > jpf-core
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 |
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 } |