src/tests/gov/nasa/jpf/test/mc/basic/BreakTest.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 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 }