src/tests/gov/nasa/jpf/test/mc/basic/AttrsTest.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.DSTORE;
  22 import gov.nasa.jpf.jvm.bytecode.INVOKEVIRTUAL;
  23 import gov.nasa.jpf.jvm.bytecode.ISTORE;
  24 import gov.nasa.jpf.jvm.bytecode.JVMInvokeInstruction;
  25 import gov.nasa.jpf.jvm.bytecode.LRETURN;
  26 import gov.nasa.jpf.util.ObjectList;
  27 import gov.nasa.jpf.util.test.TestJPF;
  28 import gov.nasa.jpf.vm.Instruction;
  29 import gov.nasa.jpf.vm.VM;
  30 import gov.nasa.jpf.vm.MethodInfo;
  31 import gov.nasa.jpf.vm.StackFrame;
  32 import gov.nasa.jpf.vm.ThreadInfo;
  33 import gov.nasa.jpf.vm.Verify;
  34
  35 import org.junit.Test;
  36
  37 /**
  38  * raw test for field/operand/local attribute handling
  39  */
  40 public class AttrsTest extends TestJPF {
  41
  42 //------------ this part we only need outside of JPF execution
  43   static class AttrType {
  44     @Override
  45         public String toString() {
  46       return "<an AttrType>";
  47     }
  48   }
  49   static final AttrType ATTR = new AttrType();
  50   static final Class<?> ATTR_CLASS = ATTR.getClass();
  51
  52   public static class IntListener extends ListenerAdapter {
  53
  54     public IntListener () {}
  55
  56     @Override
  57     public void instructionExecuted (VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn){
  58       MethodInfo mi = executedInsn.getMethodInfo();
  59
  60       // not very efficient, but who cares - it's a small test
  61       if (executedInsn instanceof ISTORE){
  62         if (mi.getName().equals("testIntPropagation")){
  63           ISTORE istore = (ISTORE)executedInsn;
  64           String localName = istore.getLocalVariableName();
  65           int localIndex = istore.getLocalVariableIndex();
  66
  67           if (localName.equals("i")){
  68             StackFrame frame = ti.getModifiableTopFrame();
  69             frame.setLocalAttr(localIndex, ATTR);
  70
  71             Object a = frame.getLocalAttr(localIndex, ATTR_CLASS);
  72             System.out.println("'i' attribute set to: " + a);
  73
  74           } else if (localName.equals("j")){
  75             StackFrame frame = ti.getTopFrame();
  76
  77             Object a = frame.getLocalAttr(localIndex, ATTR_CLASS);
  78             System.out.println("'j' AttrType attribute: " + a);
  79           }
  80         }
  81       }
  82     }
  83   }
  84
  85   static int sInt;
  86   int iInt;
  87
  88   static double sDouble;
  89   double iDouble;
  90
  91   int echoInt (int a){
  92     return a;
  93   }
  94
  95   @Test public void testIntPropagation () {
  96     if (verifyNoPropertyViolation("+listener=.test.mc.basic.AttrsTest$IntListener")) {
  97       int i = 42; // this gets attributed
  98       Verify.setLocalAttribute("i", 42); // this overwrites whatever the ISTORE listener did set on 'i'
  99       int attr = Verify.getLocalAttribute("i");
 100       Verify.println("'i' attribute after Verify.setLocalAttribute(\"i\",42): " + attr);
 101       assertTrue( attr == 42);
 102
 103       iInt = echoInt(i); // return val -> instance field
 104       sInt = iInt; // instance field -> static field
 105       int j = sInt; // static field -> local - now j should have the initial i attribute, and value 42
 106
 107       attr = Verify.getLocalAttribute("j");
 108       Verify.println("'j' attribute after assignment: " + attr);
 109       assertTrue( attr == 42);
 110     }
 111   }
 112
 113   //----------------------------------------------------------------------------------------------
 114
 115   public static class DoubleListener extends ListenerAdapter {
 116
 117     public DoubleListener () {}
 118
 119     @Override
 120     public void instructionExecuted (VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn){
 121       MethodInfo mi = executedInsn.getMethodInfo();
 122
 123       if (executedInsn instanceof DSTORE){
 124         if (mi.getName().equals("testDoublePropagation")){
 125           DSTORE dstore = (DSTORE)executedInsn;
 126           String localName = dstore.getLocalVariableName();
 127           int localIndex = dstore.getLocalVariableIndex();
 128
 129           if (localName.equals("d")){
 130             StackFrame frame = ti.getModifiableTopFrame();
 131
 132             System.out.print("listener setting 'd' attr = ");
 133             frame.setLocalAttr(localIndex, ATTR);
 134             Object a = frame.getLocalAttr(localIndex);
 135             System.out.println( a);
 136
 137           } else if (localName.equals("r")){
 138             StackFrame frame = ti.getTopFrame();
 139             Object a = frame.getLocalAttr(localIndex, ATTR_CLASS);
 140             System.out.println("'r' attribute: " + a);
 141
 142             /** get's overwritten in the model class
 143             if (a != ATTR){
 144               throw new JPFException("attribute propagation failed");
 145             }
 146             **/
 147           }
 148         }
 149
 150       }
 151     }
 152   }
 153
 154   @Test public void testDoublePropagation () {
 155     if (verifyNoPropertyViolation("+listener=.test.mc.basic.AttrsTest$DoubleListener")) {
 156       double d = 42.0; // this gets attributed
 157       Verify.setLocalAttribute("d", 42);  // this overwrites whatever the DSTORE listener did set on 'd'
 158       int attr = Verify.getLocalAttribute("d");
 159       assert attr == 42;
 160
 161       // some noise on the stack
 162       iDouble = echoDouble(d);
 163       sDouble = iDouble;
 164
 165       //double r = sDouble; // now r should have the same attribute
 166       double r = echoDouble(d);
 167
 168       attr = Verify.getLocalAttribute("r");
 169       Verify.print("@ 'r' attribute after assignment: " + attr);
 170       Verify.println();
 171
 172       assert attr == 42;
 173     }
 174   }
 175
 176
 177   //-----------------------------------------------------------------------------------------------
 178
 179   public static class InvokeListener extends ListenerAdapter {
 180
 181     @Override
 182     public void instructionExecuted (VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn){
 183       if (executedInsn instanceof JVMInvokeInstruction) {
 184         JVMInvokeInstruction call = (JVMInvokeInstruction)executedInsn;
 185         MethodInfo mi = call.getInvokedMethod();
 186         String mName = mi.getName();
 187         if (mName.equals("goModel") || mName.equals("goNative")) {
 188           Object[] a = call.getArgumentAttrs(ti);
 189           assert a != null & a.length == 3;
 190
 191           System.out.println("listener notified of: " + mName + "(), attributes= "
 192                              + a[0] + ',' + a[1] + ',' + a[2]);
 193
 194           // note - this is only acceptable if we know exactly there are just
 195           // single attrs
 196
 197           assert a[0] instanceof Integer && a[1] instanceof Integer;
 198           assert (((Integer)a[0]).intValue() == 1) &&
 199                  (((Integer)a[1]).intValue() == 2) &&
 200                  (((Integer)a[2]).intValue() == 3);
 201         }
 202       }
 203     }
 204   }
 205
 206   @Test public void testInvokeListener () {
 207     if (verifyNoPropertyViolation("+listener=.test.mc.basic.AttrsTest$InvokeListener")) {
 208       Verify.setLocalAttribute("this", 1);
 209
 210       double d = 42.0;
 211       Verify.setLocalAttribute("d", 2);
 212
 213       int i = 42;
 214       Verify.setLocalAttribute("i", 3);
 215
 216       double result = goNative(d, i); // that's going to be listened on
 217       int attr = Verify.getLocalAttribute("result");
 218
 219       Verify.print("@ 'result' attribute: " + attr);
 220       Verify.println();
 221
 222       assert attr == 6;
 223
 224       int r = goModel(d, i);  // that's listened for, too
 225       assert r == 6;
 226     }
 227   }
 228
 229
 230   native double goNative (double d, int i);
 231
 232   @Test public void testNativeMethod () {
 233     if (verifyNoPropertyViolation()) {
 234       Verify.setLocalAttribute("this", 1);
 235
 236       double d = 42.0;
 237       Verify.setLocalAttribute("d", 2);
 238
 239       int i = 42;
 240       Verify.setLocalAttribute("i", 3);
 241
 242       double result = goNative(d, i);
 243       int attr = Verify.getLocalAttribute("result");
 244
 245       Verify.print("@ 'result' attribute: " + attr);
 246       Verify.println();
 247
 248       assert attr == 6;
 249     }
 250   }
 251
 252
 253   int goModel (double d, int i) {
 254     int a1 = Verify.getLocalAttribute("d");
 255     int a2 = Verify.getLocalAttribute("i");
 256
 257     return a1*a2;
 258   }
 259
 260   double echoDouble (double d){
 261     return d;
 262   }
 263
 264
 265   @Test public void testExplicitRef () {
 266     if (verifyNoPropertyViolation()) {
 267       int attr = Verify.getFieldAttribute(this, "iDouble");
 268       Verify.print("@ 'iDouble' attribute before set: ", Integer.toString(attr));
 269       Verify.println();
 270
 271       Verify.setFieldAttribute(this, "iDouble", 42);
 272
 273       attr = Verify.getFieldAttribute(this, "iDouble");
 274       Verify.print("@ 'iDouble' attribute after set: ", Integer.toString(attr));
 275       Verify.println();
 276
 277       assert attr == 42;
 278     }
 279   }
 280
 281   @Test public void testExplicitArrayRef () {
 282     if (verifyNoPropertyViolation()) {
 283       int attr;
 284       double[] myArray = new double[10];
 285
 286       attr = Verify.getElementAttribute(myArray, 5);
 287       Verify.print("@ 'myArray[5]' attribute before set: ", Integer.toString(attr));
 288       Verify.println();
 289
 290       Verify.setElementAttribute(myArray, 5, 42);
 291
 292       attr = Verify.getElementAttribute(myArray, 5);
 293       Verify.print("@ 'myArray[5]' attribute after set: ", Integer.toString(attr));
 294       Verify.println();
 295
 296       assert attr == 42;
 297     }
 298   }
 299
 300   @Test public void testArraycopy () {
 301     if (verifyNoPropertyViolation()) {
 302       int attr;
 303       double[] a1 = new double[10];
 304       double[] a2 = new double[10];
 305
 306       Verify.setElementAttribute(a1, 3, 42);
 307       System.arraycopy(a1, 1, a2, 0, 3);
 308
 309       attr = Verify.getElementAttribute(a2, 2);
 310       assert attr == 42;
 311     }
 312   }
 313
 314   double ddd;
 315
 316   @Test public void testArrayPropagation() {
 317     if (verifyNoPropertyViolation()) {
 318
 319       int attr;
 320       double[] a1 = new double[10];
 321       double[] a2 = new double[10];
 322
 323       Verify.setElementAttribute(a1, 3, 42);
 324
 325       //attr = Verify.getElementAttribute(a1,3);
 326       //System.out.println(attr);
 327
 328       ddd = a1[3];
 329       //Verify.setFieldAttribute(this,"ddd",42);
 330       //attr = Verify.getFieldAttribute(this,"ddd");
 331       //System.out.println("@ ddd : " + attr);
 332
 333       double d = ddd;
 334       //ccc = d;
 335       //attr = Verify.getFieldAttribute(this,"ccc");
 336       //System.out.println("ccc ; " + attr);
 337
 338       //double d = a1[3]; // now d should have the attr
 339       a2[0] = d;
 340       attr = Verify.getElementAttribute(a2, 0);
 341       System.out.println("@ a2[0] : " + attr);
 342
 343       assert attr == 42;
 344     }
 345   }
 346
 347   @Test public void testBacktrack() {
 348     if (verifyNoPropertyViolation()) {
 349       int v = 42; // need to init or the compiler does not add it to the name table
 350       Verify.setLocalAttribute("v", 42);
 351
 352       boolean b = Verify.getBoolean(); // restore point
 353       System.out.println(b);
 354
 355       int attr = Verify.getLocalAttribute("v");
 356       System.out.println(attr);
 357
 358       Verify.setLocalAttribute("v", -1);
 359       attr = Verify.getLocalAttribute("v");
 360       System.out.println(attr);
 361     }
 362   }
 363
 364   @Test public void testInteger() {
 365     if (verifyNoPropertyViolation()) {
 366       int v = 42;
 367       Verify.setLocalAttribute("v", 4200);
 368
 369       // explicit
 370       Integer o = new Integer(v);
 371       int j = o.intValue();
 372       int attr = Verify.getLocalAttribute("j");
 373       assert attr == 4200;
 374
 375       // semi autoboxed
 376       j = o;
 377       boolean b = Verify.getBoolean(); // just cause some backtracking damage
 378       attr = Verify.getLocalAttribute("j");
 379       assert attr == 4200;
 380
 381     /** this does not work because of cached, preallocated Integer objects)
 382     // fully autoboxed
 383     Integer a = v;
 384     j = a;
 385     attr = Verify.getLocalAttribute("j");
 386     assert attr == 4200;
 387      **/
 388     }
 389   }
 390
 391   @Test public void testObjectAttr(){
 392
 393     if (verifyNoPropertyViolation()){
 394       Integer o = new Integer(41);
 395       Verify.setObjectAttribute(o, 42);
 396
 397       boolean b = Verify.getBoolean();
 398
 399       int attr = Verify.getObjectAttribute(o);
 400       System.out.println("object attr = " + attr);
 401       assert attr == 42;
 402     }
 403   }
 404
 405   //--- the multiple attributes tests
 406
 407   @Test
 408   public void testIntAttrList(){
 409     if (verifyNoPropertyViolation()){
 410       int var = 42;
 411       Verify.addLocalAttribute("var", Integer.valueOf(var));
 412       Verify.addLocalAttribute("var", Integer.valueOf(-var));
 413
 414       int x = var;
 415       int[] attrs = Verify.getLocalAttributes("x");
 416       for (int i=0; i<attrs.length; i++){
 417         System.out.printf("[%d] = %d\n", i, attrs[i]);
 418       }
 419
 420       assertTrue( attrs.length == 2);
 421       assertTrue( attrs[0] == -var); // lifo
 422       assertTrue( attrs[1] == var);
 423     }
 424   }
 425
 426
 427   public static class MixedAttrTypeListener extends ListenerAdapter {
 428
 429     public MixedAttrTypeListener() {}
 430
 431     @Override
 432     public void executeInstruction (VM vm, ThreadInfo ti, Instruction insnToExecute){
 433
 434       if (insnToExecute instanceof INVOKEVIRTUAL){
 435         MethodInfo callee = ((INVOKEVIRTUAL)insnToExecute).getInvokedMethod();
 436         if (callee.getUniqueName().equals("foo(J)J")){
 437           System.out.println("--- pre-exec foo() invoke interception, setting arg attrs");
 438
 439           StackFrame frame = ti.getModifiableTopFrame();
 440
 441           // we are still in the caller stackframe
 442           frame.addLongOperandAttr("foo-arg");
 443
 444           Long v = Long.valueOf( frame.peekLong());
 445           frame.addLongOperandAttr( v);
 446
 447           System.out.println("   operand attrs:");
 448           for (Object a: frame.longOperandAttrIterator()){
 449             System.out.println(a);
 450           }
 451         }
 452
 453       } else if (insnToExecute instanceof LRETURN){
 454         MethodInfo mi = insnToExecute.getMethodInfo();
 455         if (mi.getUniqueName().equals("foo(J)J")){
 456           System.out.println("--- pre-exec foo() return interception");
 457           StackFrame frame = ti.getModifiableTopFrame();
 458           int varIdx = frame.getLocalVariableSlotIndex("x");
 459           Object attr = frame.getLocalAttr(varIdx);
 460
 461           System.out.println("  got 'x' attributes");
 462           for (Object a: frame.localAttrIterator(varIdx)){
 463             System.out.println(a);
 464           }
 465
 466           assertTrue(attr.equals("foo-arg"));
 467
 468           System.out.println("  setting lreturn operand attrs");
 469           frame.addLongOperandAttr("returned");
 470
 471           for (Object a: frame.longOperandAttrIterator()){
 472             System.out.println(a);
 473           }
 474         }
 475       }
 476     }
 477
 478     @Override
 479     public void instructionExecuted (VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn){
 480
 481       if (executedInsn instanceof INVOKEVIRTUAL){
 482         MethodInfo callee = ((INVOKEVIRTUAL)executedInsn).getInvokedMethod();
 483         if (callee.getUniqueName().equals("foo(J)J")){
 484           System.out.println("--- post-exec foo() invoke interception");
 485
 486           StackFrame frame = ti.getModifiableTopFrame(); // we are now in the callee
 487           int varIdx = frame.getLocalVariableSlotIndex("x");
 488
 489           for (Object a: frame.localAttrIterator(varIdx)){
 490             System.out.println(a);
 491           }
 492
 493           Object attrs = frame.getLocalAttr(varIdx);
 494           assertTrue( ObjectList.size(attrs) == 2);
 495
 496           Object sAttr = frame.getLocalAttr(varIdx, String.class);
 497           assertTrue( sAttr != null && sAttr.equals("foo-arg"));
 498           assertTrue( frame.getNextLocalAttr(varIdx, String.class, sAttr) == null);
 499
 500           Object lAttr = frame.getLocalAttr(varIdx, Long.class);
 501           assertTrue( lAttr != null && lAttr.equals( frame.getLongLocalVariable(varIdx)));
 502           assertTrue( frame.getNextLocalAttr(varIdx, Long.class, lAttr) == null);
 503
 504           frame.removeLocalAttr(varIdx, lAttr);
 505           System.out.println("  removing " + lAttr);
 506           for (Object a: frame.localAttrIterator(varIdx)){
 507             System.out.println(a);
 508           }
 509         }
 510
 511       } else if (executedInsn instanceof LRETURN){
 512         MethodInfo mi = executedInsn.getMethodInfo();
 513         if (mi.getUniqueName().equals("foo(J)J")){
 514           StackFrame frame = ti.getTopFrame();
 515
 516           System.out.println("--- post-exec foo() return interception");
 517           for (Object a: frame.longOperandAttrIterator()){
 518             System.out.println(a);
 519           }
 520
 521           String a = frame.getLongOperandAttr(String.class);
 522           assertTrue( a.equals("returned"));
 523
 524           a = frame.getNextLongOperandAttr(String.class, a);
 525           assertTrue( a.equals("foo-arg"));
 526
 527           a = frame.getNextLongOperandAttr(String.class, a);
 528           assertTrue(a == null);
 529         }
 530       }
 531     }
 532   }
 533
 534   long foo (long x){
 535     return x;
 536   }
 537
 538   @Test
 539   public void testListenerMixedLongAttrLists(){
 540     if (verifyNoPropertyViolation("+listener=.test.mc.basic.AttrsTest$MixedAttrTypeListener")){
 541       foo(42);
 542     }
 543   }
 544 }