src/tests/gov/nasa/jpf/test/mc/data/PerturbatorTest.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.data;
  20
  21 import gov.nasa.jpf.util.test.TestJPF;
  22 import gov.nasa.jpf.vm.Verify;
  23
  24 import org.junit.Test;
  25
  26 /**
  27  * regression test for Perturbator listener
  28  */
  29 public class PerturbatorTest extends TestJPF {
  30
  31   int data = 42;
  32
  33   public static void main(String[] args) {
  34     runTestsOfThisClass(args);
  35   }
  36
  37   @Test
  38   public void testIntFieldPerturbation() {
  39
  40     if (!isJPFRun()){
  41       Verify.resetCounter(0);
  42     }
  43
  44     if (verifyNoPropertyViolation("+listener=.listener.Perturbator",
  45                                   "+perturb.fields=data",
  46                                   "+perturb.data.class=.perturb.IntOverUnder",
  47                                   "+perturb.data.field=gov.nasa.jpf.test.mc.data.PerturbatorTest.data",
  48                                   "+perturb.data.delta=1")){
  49       System.out.println("instance field perturbation test");
  50       int d = data;
  51       System.out.print("d = ");
  52       System.out.println(d);
  53
  54       Verify.incrementCounter(0);
  55       switch (Verify.getCounter(0)){
  56         case 1: assert d == 43; break;
  57         case 2: assert d == 42; break;
  58         case 3: assert d == 41; break;
  59         default:
  60           assert false : "wrong counter value: " + Verify.getCounter(0);
  61       }
  62
  63     } else {
  64       assert Verify.getCounter(0) == 3;
  65     }
  66   }
  67
  68   @Test
  69   public void testFieldPerturbationLocation() {
  70
  71     if (!isJPFRun()){
  72       Verify.resetCounter(0);
  73     }
  74
  75     if (verifyNoPropertyViolation("+listener=.listener.Perturbator",
  76                                   "+perturb.fields=data",
  77                                   "+perturb.data.class=.perturb.IntOverUnder",
  78                                   "+perturb.data.field=gov.nasa.jpf.test.mc.data.PerturbatorTest.data",
  79                                   "+perturb.data.location=PerturbatorTest.java:87",
  80                                   "+perturb.data.delta=1")){
  81       System.out.println("instance field location perturbation test");
  82
  83       int x = data; // this should not be perturbed
  84       System.out.print("x = ");
  85       System.out.println(x);
  86
  87       int d = data; // this should be
  88       System.out.print("d = ");
  89       System.out.println(d);
  90
  91       Verify.incrementCounter(0);
  92
  93     } else {
  94       assert Verify.getCounter(0) == 3;
  95     }
  96   }
  97
  98   int foo (int i) {
  99     return i;
 100   }
 101
 102   int bar (int i, boolean b) {
 103         return i-1;
 104   }
 105
 106   int bar (int i){
 107     return i-1;
 108   }
 109
 110   @Test
 111   public void testIntReturnPerturbation() {
 112     if (!isJPFRun()){
 113       Verify.resetCounter(0);
 114       Verify.resetCounter(1);
 115     }
 116
 117     if (verifyNoPropertyViolation("+listener=.listener.Perturbator",
 118                                   "+perturb.returns=foo,bar",
 119
 120                                   "+perturb.foo.class=.perturb.IntOverUnder",
 121                                   "+perturb.foo.method=gov.nasa.jpf.test.mc.data.PerturbatorTest.foo(int)",
 122                                   "+perturb.foo.location=PerturbatorTest.java:136",
 123                                   "+perturb.foo.delta=1",
 124
 125                                   "+perturb.bar.class=.perturb.IntOverUnder",
 126                                   "+perturb.bar.method=gov.nasa.jpf.test.mc.data.PerturbatorTest.bar(int,boolean)",
 127                                   "+perturb.bar.delta=5")){
 128       int x, y;
 129
 130       System.out.println("int return perturbation test");
 131
 132       x = foo(-1); // this should not be perturbed ('foo' has a location spec)
 133       System.out.print("foo() = ");
 134       System.out.println(x);
 135
 136       x = foo(42); // line 136 => this should be
 137       System.out.print("foo() = ");
 138       System.out.println(x);
 139
 140       Verify.incrementCounter(0);
 141       switch (Verify.getCounter(0)){
 142         // foo() preturbations
 143         case 1: assert x == 43; break;
 144         case 2: assert x == 42; break;
 145         case 3: assert x == 41; break;
 146         default:
 147           assert false : "wrong counter 0 (foo() perturbation) value: " + Verify.getCounter(0);
 148       }
 149
 150       if (x == 41){
 151         y = bar(40, false); // this too (no location spec for 'bar')
 152         System.out.print("bar() = ");
 153         System.out.println(y);
 154
 155         Verify.incrementCounter(1);
 156         switch (Verify.getCounter(1)){
 157           // bar() perturbations
 158           case 1: assert y == 44; break;
 159           case 2: assert y == 39; break;
 160           case 3: assert y == 34; break;
 161           default:
 162             assert false : "wrong counter 1 (bar() perturbation) value: " + Verify.getCounter(1);
 163         }
 164       }
 165
 166     } else {
 167       assert Verify.getCounter(0) == 3;
 168       assert Verify.getCounter(1) == 3;
 169     }
 170   }
 171
 172   static void printParams(int i, boolean b) {
 173         System.out.println("(" + i + ", " + b + ")");
 174   }
 175
 176   static int zoo(int i, boolean b) {
 177         printParams(i, b);
 178         if (b)
 179                 return -1 * i;
 180         else
 181                 return i;
 182   }
 183
 184   void printParam(long i, double d) {
 185         System.out.println("(" + i + ", " + d + ")");
 186   }
 187
 188   double foobar(long i, double d) {
 189         printParam(i, d);
 190         long j = i;
 191         return d + (j % 10);
 192   }
 193
 194   @Test
 195   public void testParamPerturbation() {
 196
 197     if (!isJPFRun()){
 198       Verify.resetCounter(0);
 199       Verify.resetCounter(1);
 200     }
 201
 202     if (verifyNoPropertyViolation("+listener=.listener.Perturbator",
 203                                   "+perturb.params=foo,zoo",
 204                                   "+perturb.foo.class=.perturb.GenericDataAbstractor",
 205                                   "+perturb.foo.method=gov.nasa.jpf.test.mc.data.PerturbatorTest.foobar(long,double)",
 206                                   "+perturb.foo.location=PerturbatorTest.java:233",        // <<<<<<<<< update if file is changed!
 207                                   "+perturb.zoo.class=.perturb.GenericDataAbstractor",
 208                                   "+perturb.zoo.method=gov.nasa.jpf.test.mc.data.PerturbatorTest.zoo(int,boolean)"
 209     )) {
 210       System.out.println("parameters perturbation test");
 211
 212       int e = zoo(42, false);
 213       System.out.print("zoo = ");
 214       System.out.println(e);
 215
 216       Verify.incrementCounter(0);
 217       switch (Verify.getCounter(0)){
 218         case 1: assert e == 21; break;
 219         case 2: assert e == -21; break;
 220         case 3: assert e == 0; break;
 221         case 4: assert e == 0; break;
 222         case 5: assert e == -84; break;
 223         case 6: assert e == 84; break;
 224         default:
 225           assert false : "wrong counter value: " + Verify.getCounter(0);
 226       }
 227
 228       if (e == 84) {
 229         double d = foobar(42, 0.0); // no perturbation
 230         System.out.print("foobar = ");
 231         System.out.println(d);
 232
 233         d = foobar(42, 0.0); // <<<< yes perturbation, line 233
 234         System.out.print("foobar = ");
 235         System.out.println(d);
 236
 237         Verify.incrementCounter(1);
 238         switch (Verify.getCounter(1)){
 239         case 1: assert Math.abs(d - 0.586) < 0.0001; break;
 240         case 2: assert d == 2; break;
 241         case 3: assert d == 5.141; break;
 242         case 4: assert d == -1.414; break;
 243         case 5: assert d == 0; break;
 244         case 6: assert d == 3.141; break;
 245         case 7: assert d == -1.414; break;
 246         case 8: assert d == 0; break;
 247         case 9: assert d == 3.141; break;
 248         default:
 249                 assert false : "wrong counter value: " + Verify.getCounter(1);
 250         }
 251       }
 252     } else {
 253       assert Verify.getCounter(0) == 6;
 254       assert Verify.getCounter(1) == 9;
 255     }
 256   }
 257 }