src/tests/gov/nasa/jpf/test/mc/data/DynamicAbstractionTest.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.data;
  19
  20 import gov.nasa.jpf.util.test.TestJPF;
  21 import gov.nasa.jpf.vm.Verify;
  22 import gov.nasa.jpf.vm.serialize.AbstractionAdapter;
  23
  24 import org.junit.Test;
  25
  26 /**
  27  * regression test for field value abstractions
  28  */
  29 public class DynamicAbstractionTest extends TestJPF {
  30
  31   static final String SERIALIZER_ARG = "+vm.serializer.class=.vm.serialize.DynamicAbstractionSerializer";
  32
  33   static class MyClass {
  34     int data;
  35     double notAbstracted;
  36   }
  37
  38   public static class MyClassDataAbstraction extends AbstractionAdapter {
  39
  40     @Override
  41     public int getAbstractValue (int data){
  42       int cat = 1;
  43       if (data > 5) cat = 2;
  44       if (data > 10) cat = 3;
  45
  46       System.out.println("abstracted value for " + data + " = " + cat);
  47       return cat;
  48     }
  49   }
  50
  51   //---------------------------------------------------------------------------
  52
  53   @Test
  54   public void testMyClass() {
  55     if (!isJPFRun()){
  56       Verify.resetCounter(0);
  57     }
  58
  59     if (verifyNoPropertyViolation(SERIALIZER_ARG,
  60                                   "+das.classes.include=*$MyClass",
  61                                   "+das.fields=data",
  62                                   "+das.data.field=*$MyClass.data",
  63                                   "+das.data.abstraction=gov.nasa.jpf.test.mc.data.DynamicAbstractionTest$MyClassDataAbstraction")){
  64       MyClass matchedObject = new MyClass();
  65       matchedObject.data = Verify.getInt(0, 20);
  66
  67       Verify.breakTransition("testDataAbstraction");
  68       System.out.println("new state for myClass.data = " + matchedObject.data);
  69       Verify.incrementCounter(0);
  70     }
  71
  72     if (!isJPFRun()){
  73       assertTrue( Verify.getCounter(0) == 3);
  74     }
  75   }
  76
  77
  78   //---------------------------------------------------------------------------
  79
  80   @Test
  81   public void testMixedFields(){
  82     if (!isJPFRun()){
  83       Verify.resetCounter(0);
  84     }
  85
  86     if (verifyNoPropertyViolation(SERIALIZER_ARG,
  87                                   "+das.classes.include=*$MyClass",
  88                                   "+das.fields=data",
  89                                   "+das.data.field=*$MyClass.data",
  90                                   "+das.data.abstraction=gov.nasa.jpf.test.mc.data.DynamicAbstractionTest$MyClassDataAbstraction")){
  91       MyClass matchedObject = new MyClass();
  92       matchedObject.data = Verify.getInt(0, 20);
  93
  94       if (matchedObject.data % 4 == 0){
  95         System.out.println("  notAbstracted=1");
  96         matchedObject.notAbstracted = 1;
  97       }
  98
  99       Verify.breakTransition("testDataAbstraction"); // matching point
 100       System.out.println("new state for myClass.data = " + matchedObject.data + ", " + matchedObject.notAbstracted);
 101       Verify.incrementCounter(0);
 102     }
 103
 104     if (!isJPFRun()){
 105       assertTrue( Verify.getCounter(0) == 6);
 106     }
 107   }
 108
 109
 110   //---------------------------------------------------------------------------
 111
 112   static class SomeIgnoredClass {
 113     int data;  // note that it is not @FilterField annotated
 114   }
 115
 116   @Test
 117   public void testClassFilter() {
 118     if (!isJPFRun()){
 119       Verify.resetCounter(0);
 120     }
 121
 122     if (verifyNoPropertyViolation(SERIALIZER_ARG,
 123                                   "+das.classes.include=*$MyClass", // only consider MyClass instance and static data
 124                                   "+das.methods.exclude=*",  // make sure we don't match this stackframe ('i' changes)
 125                                   "+vm.max_transition_length=MAX")){
 126       MyClass matchedObject = new MyClass();
 127       SomeIgnoredClass ignoredObject = new SomeIgnoredClass();
 128
 129       matchedObject.data = Verify.getInt(0, 2); // (1) 1st CG
 130       System.out.print(" matchedObject.data=");
 131       System.out.println( matchedObject.data);
 132
 133       for (int i=0; i<2; i++){
 134         ignoredObject.data = i;
 135         System.out.print("    ignoredObject.data=");
 136         System.out.println( ignoredObject.data);
 137
 138         Verify.breakTransition("testDataAbstraction"); // (2) matching point for someObject
 139
 140         // if we get here we had a new state (i.e. wasn't matched)
 141         // NOTE we don't get here for matchedObject.data=0 because that would match with the state before (1)
 142         System.out.printf("         new state for matched=%d, ignored=%d\n", matchedObject.data, ignoredObject.data);
 143         Verify.incrementCounter(0); // should be only reached once for matchedObject.data={1,2}
 144       }
 145     }
 146
 147     if (!isJPFRun()){
 148       assertTrue( Verify.getCounter(0) == 2);
 149     }
 150   }
 151
 152
 153   //---------------------------------------------------------------------------
 154
 155   void matchThis() {
 156     for (int i=0; i<2; i++){
 157       System.out.printf("  matchThis() i=%d\n", i);
 158
 159       Verify.breakTransition("testDataAbstraction"); // 'i' has changed
 160       System.out.println("    new state");
 161       Verify.incrementCounter(0);
 162     }
 163   }
 164
 165   @Test
 166   public void testStackFrameFilter() {
 167     if (!isJPFRun()){
 168       Verify.resetCounter(0);
 169     }
 170
 171     if (verifyNoPropertyViolation(SERIALIZER_ARG,
 172                                   "+das.methods.include=*DynamicAbstractionTest.matchThis(*)V")){
 173       for (int i=0; i<10; i++){ // 'i' changes this frame..
 174         System.out.printf("loop cycle %d\n", i);
 175         matchThis(); // ..but not this one
 176       }
 177     }
 178
 179     if (!isJPFRun()){
 180       assertTrue( Verify.getCounter(0) == 2);
 181     }
 182   }
 183 }