Mercurial > hg > Members > kono > jpf-core
diff 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 |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/tests/gov/nasa/jpf/test/mc/basic/CascadedCGTest.java Fri Jan 23 10:14:01 2015 -0800 @@ -0,0 +1,216 @@ +/* + * Copyright (C) 2014, United States Government, as represented by the + * Administrator of the National Aeronautics and Space Administration. + * All rights reserved. + * + * The Java Pathfinder core (jpf-core) platform is licensed under the + * Apache License, Version 2.0 (the "License"); you may not use this file except + * in compliance with the License. You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0. + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package gov.nasa.jpf.test.mc.basic; + + +import gov.nasa.jpf.ListenerAdapter; +import gov.nasa.jpf.jvm.bytecode.EXECUTENATIVE; +import gov.nasa.jpf.jvm.bytecode.GETFIELD; +import gov.nasa.jpf.search.Search; +import gov.nasa.jpf.util.test.TestJPF; +import gov.nasa.jpf.vm.ChoiceGenerator; +import gov.nasa.jpf.vm.FieldInfo; +import gov.nasa.jpf.vm.Instruction; +import gov.nasa.jpf.vm.VM; +import gov.nasa.jpf.vm.StackFrame; +import gov.nasa.jpf.vm.SystemState; +import gov.nasa.jpf.vm.ThreadInfo; +import gov.nasa.jpf.vm.Verify; +import gov.nasa.jpf.vm.choice.IntChoiceFromSet; +import gov.nasa.jpf.vm.choice.IntIntervalGenerator; + +import org.junit.Test; + +/** + * regression test for cascaded ChoiceGenerators + */ +public class CascadedCGTest extends TestJPF { + + public static class IntChoiceCascader extends ListenerAdapter { + static int result; + + @Override + public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) { + SystemState ss = vm.getSystemState(); + + if (executedInsn instanceof EXECUTENATIVE) { // break on native method exec + EXECUTENATIVE exec = (EXECUTENATIVE) executedInsn; + + if (exec.getExecutedMethodName().equals("getInt")){// this insn did create a CG + if (!ti.isFirstStepInsn()){ + result = 0; + + IntIntervalGenerator cg = new IntIntervalGenerator("listenerCG", 3,4); + ss.setNextChoiceGenerator(cg); + System.out.println("# listener registered " + cg); + + } else { // reexecution + + ChoiceGenerator<?>[] curCGs = ss.getCurrentChoiceGenerators(); + assert curCGs.length == 2; + + IntIntervalGenerator cg = ss.getCurrentChoiceGenerator("listenerCG", IntIntervalGenerator.class); + assert cg != null : "no 'listenerCG' IntIntervalGenerator found"; + int i = cg.getNextChoice(); + System.out.println("# current listener CG choice: " + i); + + cg = ss.getCurrentChoiceGenerator("verifyGetInt(II)", IntIntervalGenerator.class); + assert cg != null : "no 'verifyGetInt(II)' IntIntervalGenerator found"; + int j = cg.getNextChoice(); + System.out.println("# current insn CG choice: " + j); + + result += i * j; + } + } + } + } + } + + @Test + public void testCascadedIntIntervals () { + if (verifyNoPropertyViolation("+listener=.test.mc.basic.CascadedCGTest$IntChoiceCascader")){ + int i = Verify.getInt( 1, 2); + System.out.print("i="); + System.out.println(i); + } else { + assert IntChoiceCascader.result == 21; + } + } + + + //--- mixed data and thread CG + + // this listener replaces all GETFIELD "mySharedField" results with configured + // choice values (i.e. it is a simplified field Perturbator). + // The demo point is that it is not aware of that such GETFIELDs might also be + // scheduling points because of shared object field access, and it should work + // the same no matter if there also was a ThreadChoice/context switch or not + + // NOTE: while the cascaded CG interface is easy to use (almost the same as the + // single CG interface), the context can be quite tricky because the cascaded + // CG (the scheduling point in this case) means the corresponding instruction + // is already rescheduled and might have been cut short in insn specific ways + // (in this case before pushing the field value on the operand stack). For this + // reason a simple ti.isFirstStepInsn() check is not sufficient. There might not + // have been a reschedule if there was only one thread, or even if this is the + // first step insn, the corresponding CG might have been not related to the + // getfield but some action in the preceeding thread (e.g. a terminate). + // In this case, the simple solution is based on that we want the data CG + // unconditionally, so we check if there is a corresponding current CG + // (which means this is not the first step insn) + + public static class FieldAccessCascader extends ListenerAdapter { + + @Override + public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) { + SystemState ss = vm.getSystemState(); + + if (executedInsn instanceof GETFIELD){ + GETFIELD getInsn = (GETFIELD) executedInsn; + FieldInfo fi = getInsn.getFieldInfo(); + if (fi.getName().equals("mySharedField")){ + + IntChoiceFromSet cg = ss.getCurrentChoiceGenerator("fieldReplace", IntChoiceFromSet.class); + if (cg == null){ + + // we might get here after a preceding rescheduling exec, i.e. + // partial execution (with successive re-execution), or after + // non-rescheduling exec has been completed (only one runnable thread). + // In the first case we have to restore the operand stack so that + // we can reexecute + if (!ti.willReExecuteInstruction()){ + // restore old operand stack contents + StackFrame frame = ti.getModifiableTopFrame(); + + frame.pop(); + frame.pushRef( getInsn.getLastThis()); + } + + cg = new IntChoiceFromSet("fieldReplace", 42, 43); + ss.setNextChoiceGenerator(cg); + ti.reExecuteInstruction(); + + System.out.println("# listener registered CG: " + cg); + + } else { + StackFrame frame = ti.getModifiableTopFrame(); + + int v = cg.getNextChoice(); + int n = frame.pop(); + frame.push(v); + + System.out.println("# listener replacing " + n + " with " + v); + } + } + } + } + + //--- those are just for debugging purposes + @Override + public void stateBacktracked(Search search) { + System.out.println("#------ [" + search.getDepth() + "] backtrack: " + search.getStateId()); + } + + @Override + public void stateAdvanced(Search search){ + System.out.println("#------ " + search.getStateId() + " isNew: " + search.isNewState() + ", isEnd: " + search.isEndState()); + } + + @Override + public void threadScheduled(VM vm, ThreadInfo ti){ + System.out.println("# running thread: " + ti); + } + + @Override + public void threadTerminated(VM vm, ThreadInfo ti){ + System.out.println("# terminated thread: " + ti); + } + + @Override + public void threadStarted(VM vm, ThreadInfo ti){ + System.out.println("# started thread: " + ti); + } + + @Override + public void choiceGeneratorAdvanced (VM vm, ChoiceGenerator<?> currentCG) { + System.out.println("# choice: " + currentCG); + } + } + + int mySharedField = -1; + + @Test + public void testMixedThreadDataCGs () { + if (verifyNoPropertyViolation("+listener=.test.mc.basic.CascadedCGTest$FieldAccessCascader")){ + Thread t = new Thread(){ + @Override + public void run() { + int n = mySharedField; + System.out.print("<thread> mySharedField read: "); + System.out.println( n); + assert n == 42 || n == 43; // regardless of main thread exec state + } + }; + t.start(); + + mySharedField = 7; + System.out.println("<main> mySharedField write: 7"); + } + } +}