src/tests/gov/nasa/jpf/test/mc/basic/CascadedCGTest.java

   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 }