Mercurial > hg > Members > kono > jpf-core
comparison src/tests/gov/nasa/jpf/test/mc/basic/CascadedCGTest.java @ 0:61d41facf527
initial v8 import (history reset)
author | Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> |
---|---|
date | Fri, 23 Jan 2015 10:14:01 -0800 |
parents | |
children |
comparison
equal
deleted
inserted
replaced
-1:000000000000 | 0:61d41facf527 |
---|---|
1 /* | |
2 * Copyright (C) 2014, United States Government, as represented by the | |
3 * Administrator of the National Aeronautics and Space Administration. | |
4 * All rights reserved. | |
5 * | |
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 | |
9 * | |
10 * http://www.apache.org/licenses/LICENSE-2.0. | |
11 * | |
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. | |
17 */ | |
18 | |
19 package gov.nasa.jpf.test.mc.basic; | |
20 | |
21 | |
22 import gov.nasa.jpf.ListenerAdapter; | |
23 import gov.nasa.jpf.jvm.bytecode.EXECUTENATIVE; | |
24 import gov.nasa.jpf.jvm.bytecode.GETFIELD; | |
25 import gov.nasa.jpf.search.Search; | |
26 import gov.nasa.jpf.util.test.TestJPF; | |
27 import gov.nasa.jpf.vm.ChoiceGenerator; | |
28 import gov.nasa.jpf.vm.FieldInfo; | |
29 import gov.nasa.jpf.vm.Instruction; | |
30 import gov.nasa.jpf.vm.VM; | |
31 import gov.nasa.jpf.vm.StackFrame; | |
32 import gov.nasa.jpf.vm.SystemState; | |
33 import gov.nasa.jpf.vm.ThreadInfo; | |
34 import gov.nasa.jpf.vm.Verify; | |
35 import gov.nasa.jpf.vm.choice.IntChoiceFromSet; | |
36 import gov.nasa.jpf.vm.choice.IntIntervalGenerator; | |
37 | |
38 import org.junit.Test; | |
39 | |
40 /** | |
41 * regression test for cascaded ChoiceGenerators | |
42 */ | |
43 public class CascadedCGTest extends TestJPF { | |
44 | |
45 public static class IntChoiceCascader extends ListenerAdapter { | |
46 static int result; | |
47 | |
48 @Override | |
49 public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) { | |
50 SystemState ss = vm.getSystemState(); | |
51 | |
52 if (executedInsn instanceof EXECUTENATIVE) { // break on native method exec | |
53 EXECUTENATIVE exec = (EXECUTENATIVE) executedInsn; | |
54 | |
55 if (exec.getExecutedMethodName().equals("getInt")){// this insn did create a CG | |
56 if (!ti.isFirstStepInsn()){ | |
57 result = 0; | |
58 | |
59 IntIntervalGenerator cg = new IntIntervalGenerator("listenerCG", 3,4); | |
60 ss.setNextChoiceGenerator(cg); | |
61 System.out.println("# listener registered " + cg); | |
62 | |
63 } else { // reexecution | |
64 | |
65 ChoiceGenerator<?>[] curCGs = ss.getCurrentChoiceGenerators(); | |
66 assert curCGs.length == 2; | |
67 | |
68 IntIntervalGenerator cg = ss.getCurrentChoiceGenerator("listenerCG", IntIntervalGenerator.class); | |
69 assert cg != null : "no 'listenerCG' IntIntervalGenerator found"; | |
70 int i = cg.getNextChoice(); | |
71 System.out.println("# current listener CG choice: " + i); | |
72 | |
73 cg = ss.getCurrentChoiceGenerator("verifyGetInt(II)", IntIntervalGenerator.class); | |
74 assert cg != null : "no 'verifyGetInt(II)' IntIntervalGenerator found"; | |
75 int j = cg.getNextChoice(); | |
76 System.out.println("# current insn CG choice: " + j); | |
77 | |
78 result += i * j; | |
79 } | |
80 } | |
81 } | |
82 } | |
83 } | |
84 | |
85 @Test | |
86 public void testCascadedIntIntervals () { | |
87 if (verifyNoPropertyViolation("+listener=.test.mc.basic.CascadedCGTest$IntChoiceCascader")){ | |
88 int i = Verify.getInt( 1, 2); | |
89 System.out.print("i="); | |
90 System.out.println(i); | |
91 } else { | |
92 assert IntChoiceCascader.result == 21; | |
93 } | |
94 } | |
95 | |
96 | |
97 //--- mixed data and thread CG | |
98 | |
99 // this listener replaces all GETFIELD "mySharedField" results with configured | |
100 // choice values (i.e. it is a simplified field Perturbator). | |
101 // The demo point is that it is not aware of that such GETFIELDs might also be | |
102 // scheduling points because of shared object field access, and it should work | |
103 // the same no matter if there also was a ThreadChoice/context switch or not | |
104 | |
105 // NOTE: while the cascaded CG interface is easy to use (almost the same as the | |
106 // single CG interface), the context can be quite tricky because the cascaded | |
107 // CG (the scheduling point in this case) means the corresponding instruction | |
108 // is already rescheduled and might have been cut short in insn specific ways | |
109 // (in this case before pushing the field value on the operand stack). For this | |
110 // reason a simple ti.isFirstStepInsn() check is not sufficient. There might not | |
111 // have been a reschedule if there was only one thread, or even if this is the | |
112 // first step insn, the corresponding CG might have been not related to the | |
113 // getfield but some action in the preceeding thread (e.g. a terminate). | |
114 // In this case, the simple solution is based on that we want the data CG | |
115 // unconditionally, so we check if there is a corresponding current CG | |
116 // (which means this is not the first step insn) | |
117 | |
118 public static class FieldAccessCascader extends ListenerAdapter { | |
119 | |
120 @Override | |
121 public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) { | |
122 SystemState ss = vm.getSystemState(); | |
123 | |
124 if (executedInsn instanceof GETFIELD){ | |
125 GETFIELD getInsn = (GETFIELD) executedInsn; | |
126 FieldInfo fi = getInsn.getFieldInfo(); | |
127 if (fi.getName().equals("mySharedField")){ | |
128 | |
129 IntChoiceFromSet cg = ss.getCurrentChoiceGenerator("fieldReplace", IntChoiceFromSet.class); | |
130 if (cg == null){ | |
131 | |
132 // we might get here after a preceding rescheduling exec, i.e. | |
133 // partial execution (with successive re-execution), or after | |
134 // non-rescheduling exec has been completed (only one runnable thread). | |
135 // In the first case we have to restore the operand stack so that | |
136 // we can reexecute | |
137 if (!ti.willReExecuteInstruction()){ | |
138 // restore old operand stack contents | |
139 StackFrame frame = ti.getModifiableTopFrame(); | |
140 | |
141 frame.pop(); | |
142 frame.pushRef( getInsn.getLastThis()); | |
143 } | |
144 | |
145 cg = new IntChoiceFromSet("fieldReplace", 42, 43); | |
146 ss.setNextChoiceGenerator(cg); | |
147 ti.reExecuteInstruction(); | |
148 | |
149 System.out.println("# listener registered CG: " + cg); | |
150 | |
151 } else { | |
152 StackFrame frame = ti.getModifiableTopFrame(); | |
153 | |
154 int v = cg.getNextChoice(); | |
155 int n = frame.pop(); | |
156 frame.push(v); | |
157 | |
158 System.out.println("# listener replacing " + n + " with " + v); | |
159 } | |
160 } | |
161 } | |
162 } | |
163 | |
164 //--- those are just for debugging purposes | |
165 @Override | |
166 public void stateBacktracked(Search search) { | |
167 System.out.println("#------ [" + search.getDepth() + "] backtrack: " + search.getStateId()); | |
168 } | |
169 | |
170 @Override | |
171 public void stateAdvanced(Search search){ | |
172 System.out.println("#------ " + search.getStateId() + " isNew: " + search.isNewState() + ", isEnd: " + search.isEndState()); | |
173 } | |
174 | |
175 @Override | |
176 public void threadScheduled(VM vm, ThreadInfo ti){ | |
177 System.out.println("# running thread: " + ti); | |
178 } | |
179 | |
180 @Override | |
181 public void threadTerminated(VM vm, ThreadInfo ti){ | |
182 System.out.println("# terminated thread: " + ti); | |
183 } | |
184 | |
185 @Override | |
186 public void threadStarted(VM vm, ThreadInfo ti){ | |
187 System.out.println("# started thread: " + ti); | |
188 } | |
189 | |
190 @Override | |
191 public void choiceGeneratorAdvanced (VM vm, ChoiceGenerator<?> currentCG) { | |
192 System.out.println("# choice: " + currentCG); | |
193 } | |
194 } | |
195 | |
196 int mySharedField = -1; | |
197 | |
198 @Test | |
199 public void testMixedThreadDataCGs () { | |
200 if (verifyNoPropertyViolation("+listener=.test.mc.basic.CascadedCGTest$FieldAccessCascader")){ | |
201 Thread t = new Thread(){ | |
202 @Override | |
203 public void run() { | |
204 int n = mySharedField; | |
205 System.out.print("<thread> mySharedField read: "); | |
206 System.out.println( n); | |
207 assert n == 42 || n == 43; // regardless of main thread exec state | |
208 } | |
209 }; | |
210 t.start(); | |
211 | |
212 mySharedField = 7; | |
213 System.out.println("<main> mySharedField write: 7"); | |
214 } | |
215 } | |
216 } |