Mercurial > hg > Members > kono > jpf-core

comparison src/tests/gov/nasa/jpf/test/mc/basic/BreakTest.java @ 0:61d41facf527

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 package gov.nasa.jpf.test.mc.basic;
19
20 import gov.nasa.jpf.ListenerAdapter;
21 import gov.nasa.jpf.jvm.bytecode.JVMInvokeInstruction;
22 import gov.nasa.jpf.jvm.bytecode.PUTFIELD;
23 import gov.nasa.jpf.util.test.TestJPF;
24 import gov.nasa.jpf.vm.ChoiceGenerator;
25 import gov.nasa.jpf.vm.FieldInfo;
26 import gov.nasa.jpf.vm.Instruction;
27 import gov.nasa.jpf.vm.VM;
28 import gov.nasa.jpf.vm.SystemState;
29 import gov.nasa.jpf.vm.ThreadInfo;
30 import gov.nasa.jpf.vm.Verify;
31
32 import org.junit.Test;
33
34
35 /**
36 * simple test application to break transitions from listeners
37 */
38 public class BreakTest extends TestJPF {
39
40 static final String LISTENER = "+listener=.test.mc.basic.BreakTestListener";
41
42 static class BreakListener extends ListenerAdapter {
43 public static int nCG; // braindead, just to check from outside
44
45 public BreakListener() {
46 nCG = 0;
47 }
48
49 @Override
50 public void choiceGeneratorSet (VM vm, ChoiceGenerator<?> newCG) {
51 System.out.println("CG set: " + newCG);
52 nCG++;
53 }
54
55 @Override
56 public void choiceGeneratorAdvanced (VM vm, ChoiceGenerator<?> currentCG) {
57 System.out.println("CG advanced: " + currentCG);
58 }
59 }
60
61
62 int data;
63
64 //--- test setIgnored
65
66 public static class FieldIgnorer extends BreakListener {
67 @Override
68 public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
69 SystemState ss = vm.getSystemState();
70
71 if (executedInsn instanceof PUTFIELD) { // break on field access
72 FieldInfo fi = ((PUTFIELD) executedInsn).getFieldInfo();
73 if (fi.getClassInfo().getName().endsWith(".BreakTest")) {
74 System.out.println("# ignoring after: " + executedInsn);
75 ss.setIgnored(true);
76 }
77 }
78 }
79 }
80
81 @Test
82 public void testSimpleIgnore () {
83 if (verifyNoPropertyViolation("+listener=.test.mc.basic.BreakTest$FieldIgnorer",
84 "+vm.max_transition_length=1000000")) {
85 int i = 42;
86 data = i; // we ignore here
87 fail("should never get here");
88
89 } else {
90 if (BreakListener.nCG != 1) { // that's really simplistic
91 fail("wrong number of CGs: " + BreakListener.nCG);
92 }
93 }
94 }
95
96
97 //--- testSimpleBreak
98
99 public static class FieldBreaker extends BreakListener {
100 @Override
101 public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
102 SystemState ss = vm.getSystemState();
103
104 if (executedInsn instanceof PUTFIELD) { // break on field access
105 FieldInfo fi = ((PUTFIELD) executedInsn).getFieldInfo();
106 if (fi.getClassInfo().getName().endsWith(".BreakTest")) {
107 System.out.println("# breaking after: " + executedInsn);
108 ti.breakTransition("breakTest");
109 }
110 }
111 }
112 }
113
114 @Test
115 public void testSimpleBreak () {
116 if (verifyNoPropertyViolation("+listener=.test.mc.basic.BreakTest$FieldBreaker",
117 "+vm.max_transition_length=1000000")) {
118 int i = 42;
119 data = i; // we break after that
120 i = 0;
121
122 } else {
123 if (BreakListener.nCG != 2) { // that's really simplistic
124 fail("wrong number of CGs: " + BreakListener.nCG);
125 }
126 }
127 }
128
129
130 //--- test CG chain break
131
132 public static class FooCallBreaker extends BreakListener {
133 @Override
134 public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
135 SystemState ss = vm.getSystemState();
136
137 if (executedInsn instanceof JVMInvokeInstruction) { // break on method call
138 JVMInvokeInstruction call = (JVMInvokeInstruction) executedInsn;
139
140 if ("foo()V".equals(call.getInvokedMethodName())) {
141 System.out.println("# breaking & pruning after: " + executedInsn);
142 System.out.println("# registered (ignored) CG: " + ss.getNextChoiceGenerator());
143 ti.breakTransition("breakTest"); // not required since we ignore
144 ss.setIgnored(true);
145 }
146 }
147 }
148 }
149
150 void foo () {
151 System.out.println("foo");
152 }
153
154 void bar () {
155 System.out.println("bar");
156 }
157
158 @Test
159 public void testDeepCGBreak () {
160 if (!isJPFRun()){
161 Verify.resetCounter(0);
162 }
163
164 if (verifyNoPropertyViolation("+listener=.test.mc.basic.BreakTest$FooCallBreaker")) {
165 if (Verify.getBoolean(false)) {
166 System.out.println("foo,bar branch");
167 foo(); // listener sets it ignored -> break
168 bar();
169 fail("should not get here");
170
171 } else {
172 Verify.incrementCounter(0);
173
174 System.out.println("bar,foo branch");
175 bar();
176 foo(); // listener sets it ignored -> break
177 fail("should not get here");
178 }
179 }
180
181 if (!isJPFRun()){
182 assert Verify.getCounter(0) == 1;
183 }
184 }
185
186
187 //--- test ignore after setting nextCG
188
189 public static class VerifyNextIntBreaker extends BreakListener {
190 @Override
191 public void choiceGeneratorRegistered(VM vm, ChoiceGenerator<?> nextCG, ThreadInfo ti, Instruction executedInsn) {
192 SystemState ss = vm.getSystemState();
193
194 ChoiceGenerator<?> cg = ss.getNextChoiceGenerator();
195 if (cg.getId().equals("verifyGetInt(II)")) {
196 System.out.println("# breaking & pruning after: " + ti.getPC());
197 System.out.println("# registered (ignored) CG: " + cg);
198
199 ss.setIgnored(true); // should reset the IntIntervalCG registered by the native getInt()
200 ti.breakTransition("breakTest"); // should have no effect
201 }
202 }
203 }
204
205 @Test
206 public void testIgnoreAfterCG () {
207 if (!isJPFRun()){
208 Verify.resetCounter(0);
209 }
210
211 if (verifyNoPropertyViolation("+listener=.test.mc.basic.BreakTest$VerifyNextIntBreaker")) {
212 if (Verify.getBoolean(false)){
213 System.out.println("true branch (should be first)");
214
215 int i = Verify.getInt(1, 2); // listener breaks & ignores post exec
216 fail("should never get here");
217
218 } else {
219 Verify.incrementCounter(0);
220
221 System.out.println("false branch");
222 }
223 }
224
225 if (!isJPFRun()){
226 assert Verify.getCounter(0) == 1;
227 }
228 }
229
230 }