comparison src/tests/gov/nasa/jpf/test/mc/basic/SkipInstructionTest.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 package gov.nasa.jpf.test.mc.basic;
19
20 import gov.nasa.jpf.ListenerAdapter;
21 import gov.nasa.jpf.jvm.bytecode.GETFIELD;
22 import gov.nasa.jpf.jvm.bytecode.IRETURN;
23 import gov.nasa.jpf.jvm.bytecode.JVMInvokeInstruction;
24 import gov.nasa.jpf.util.test.TestJPF;
25 import gov.nasa.jpf.vm.ClassInfo;
26 import gov.nasa.jpf.vm.Instruction;
27 import gov.nasa.jpf.vm.VM;
28 import gov.nasa.jpf.vm.MethodInfo;
29 import gov.nasa.jpf.vm.StackFrame;
30 import gov.nasa.jpf.vm.ThreadInfo;
31 import gov.nasa.jpf.vm.choice.IntChoiceFromList;
32
33 import org.junit.Test;
34
35 public class SkipInstructionTest extends TestJPF {
36
37 //--- replacing field access
38
39 int answer = 0;
40
41 public static class GetFieldListener extends ListenerAdapter {
42
43 @Override
44 public void executeInstruction(VM vm, ThreadInfo ti, Instruction insnToExecute) {
45 Instruction pc = ti.getPC();
46
47 if (pc instanceof GETFIELD) {
48 GETFIELD gf = (GETFIELD) pc;
49 if (gf.getVariableId().equals(SkipInstructionTest.class.getName() + ".answer")) {
50 System.out.println("now intercepting: " + pc);
51
52 // simulate the operand stack behavior of the skipped insn
53 StackFrame frame = ti.getModifiableTopFrame();
54
55 frame.pop();
56 frame.push(42);
57
58 ti.skipInstruction(pc.getNext());
59 }
60 }
61 }
62 }
63
64 @Test
65 public void testGETFIELD () {
66
67 if (verifyNoPropertyViolation("+listener=gov.nasa.jpf.test.mc.basic.SkipInstructionTest$GetFieldListener")){
68 int i = answer; // to be intercepted by listener
69
70 System.out.println(i);
71 assert (i == 42) : "get_field not intercepted: " + i;
72 }
73 }
74
75 //--- replacing method execution
76 // this is not using skipInstruction but is setting the next one to enter, which
77 // means it can skip over a whole bunch of things. The use that comes to mind is to
78 // skip over method bodies, but still preserve the invoke processing so that we
79 // preserve the locking/sync (which we otherwise would have to do explicitly from
80 // a pre-exec listener
81
82 // the intercepted method
83 int foo (int a, int b) {
84 int result = a + b;
85 if (result > 10) {
86 return 10;
87 } else {
88 return result;
89 }
90 }
91
92 // the listener that does the interception
93 public static class InvokeListener extends ListenerAdapter {
94 MethodInfo interceptedMethod;
95
96 @Override
97 public void classLoaded (VM vm, ClassInfo ci) {
98 if (ci.getName().equals("gov.nasa.jpf.test.mc.basic.SkipInstructionTest")) {
99 interceptedMethod = ci.getMethod("foo(II)I", false);
100 assert interceptedMethod != null : "foo(II)I not found";
101 System.out.println("method to intercept: " + interceptedMethod);
102 }
103 }
104
105 @Override
106 public void instructionExecuted (VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
107 MethodInfo mi = ti.getTopFrameMethodInfo();
108 if (mi == interceptedMethod) {
109 System.out.println("in " + mi);
110
111 if (!ti.isFirstStepInsn()) {
112 System.out.println("in top half: " + executedInsn);
113 if (executedInsn instanceof JVMInvokeInstruction) { // we just entered the interceptedMethod
114 IntChoiceFromList cg = new IntChoiceFromList("Test", 42, 43);
115 if (vm.setNextChoiceGenerator(cg)) {
116 return; // we are done here, next insn in this method will skip to return
117 }
118 }
119 } else {
120 // note - this is the first insn WITHIN the interceptedMethod
121 System.out.println("in bottom half: " + executedInsn);
122 IntChoiceFromList cg = vm.getCurrentChoiceGenerator("Test", IntChoiceFromList.class);
123 if (cg != null) {
124 int choice = cg.getNextChoice();
125 Instruction lastInsn = mi.getLastInsn();
126 assert lastInsn instanceof IRETURN : "last instruction not an IRETURN ";
127 StackFrame frame = ti.getModifiableTopFrame(); // we are modifying it
128 System.out.println("listener is skipping method body of " + mi + " returning " + choice);
129 frame.push(choice);
130 ti.setNextPC(lastInsn);
131 } else {
132 System.out.println("unexpected CG: " + cg);
133 }
134 }
135 }
136 }
137 }
138
139 @Test
140 public void testSkipMethodBody() {
141 if (verifyNoPropertyViolation("+listener=gov.nasa.jpf.test.mc.basic.SkipInstructionTest$InvokeListener")){
142 int ret = foo( 3, 4);
143 System.out.println(ret);
144 //assertTrue( ret == 42);
145 }
146 }
147 }