Robust/src/Tests/OwnershipAnalysisTest/test01/test01.java

   1
   2 public class Parameter {
   3   flag w;
   4   int a;
   5   int b;
   6   //Parameter f;
   7   //Parameter g;
   8   //Penguin p;
   9   //Foo h;
  10
  11   public Parameter() {} // a = 0; b = 0; f = null; g = null; }
  12
  13   //public void bar() { foo(); }
  14   //public void foo() { bar(); }
  15
  16   static public void proof( Fooz p0, Fooz p1 ) {
  17     Fooz c = new Fooz();
  18     Fooz d = new Fooz();
  19
  20     c.x  = d;
  21     p0.x = c;
  22     p1.x = d;
  23   }
  24 }
  25
  26 public class Fooz {
  27   public Fooz() {}
  28   public Fooz x;
  29 }
  30
  31 /*
  32 public class Penguin {
  33   int x;
  34   int y;
  35   Foo h;
  36
  37   public Penguin() { x = 0; y = 0; }
  38
  39   public void bar() { x = 1; }
  40 }
  41
  42 public class Voo {
  43   flag f; int x; Baw b; Baw bb;
  44
  45   public Voo() {}
  46
  47   static Voo getAVoo( Voo bogus ) {
  48     while( false ) {
  49       if( false ) {
  50         return new Voo();
  51       } else {
  52         return new Voo();
  53       }
  54     }
  55     return new Voo();
  56   }
  57 }
  58
  59 public class Baw {
  60   int y;
  61   Foo f;
  62   String s;
  63
  64   public Baw() {}
  65
  66   public void doTheBaw( Voo v ) { v = new Voo(); }
  67 }
  68
  69
  70 public class Foo {
  71   flag f;
  72
  73   public Foo() {}
  74
  75   public Foo x;
  76   public Foo y;
  77   public Foo z;
  78   public Baw b;
  79
  80   public Foo getAFoo() {
  81     return new Foo();
  82   }
  83
  84   public Foo newFooChain( Foo a ) {
  85     Foo b = new Foo();
  86     b.x = a;
  87     return b;
  88   }
  89
  90   public void ruinSomeFoos( Foo a, Foo b ) {
  91     a.x = b.x;
  92   }
  93
  94   static public void aStaticMethod( Foo p0, Foo p1 ) {
  95     Foo f0 = new Foo();
  96     Foo f1 = new Foo();
  97     Foo f2 = new Foo();
  98
  99     f0.x = f1;
 100     p0.x = f0;
 101     p1.x = f1;
 102     p1.x = f2;
 103   }
 104
 105   static public void m1_( Foo p0 ) {
 106     Foo g0 = new Foo();
 107     Foo g1 = new Foo();
 108
 109     g0.x = p0;
 110     p0.x = g1;
 111   }
 112
 113   static public void m2_( Foo p0 ) {
 114     Foo g0 = new Foo();
 115
 116     g0.x = p0;
 117     g0.y = p0;
 118   }
 119
 120   static public void m3_( Foo p0 ) {
 121     Foo g0 = new Foo();
 122
 123     p0.x = g0;
 124     p0.y = g0;
 125   }
 126
 127   static public void m4_( Foo p0 ) {
 128     p0.x = p0;
 129   }
 130
 131   static public void m5_( Foo p0 ) {
 132     Foo g0 = new Foo();
 133     p0.x = g0;
 134     g0.x = p0;
 135   }
 136
 137   static public void m6_( Foo p0, Foo p1 ) {
 138     Foo g0 = new Foo();
 139     Foo g1 = new Foo();
 140     Foo g2 = new Foo();
 141     Foo g3 = new Foo();
 142
 143     g0.x = p0;
 144     p0.x = g1;
 145
 146     g2.x = p1;
 147     p1.x = g3;
 148
 149     p0.y = p1;
 150   }
 151
 152   static public void m7_( Foo p0, Foo p1 ) {
 153     Foo g0 = new Foo();
 154     Foo g1 = new Foo();
 155     Foo g2 = new Foo();
 156     Foo g3 = new Foo();
 157
 158     g0.x = p0;
 159     p0.x = g1;
 160
 161     g2.x = p1;
 162     p1.x = g3;
 163
 164     p0.y = p1;
 165     p0.z = p1;
 166   }
 167
 168   static public void m8_( Foo p0, Foo p1 ) {
 169     Foo g0 = new Foo();
 170     Foo g1 = new Foo();
 171     Foo g2 = new Foo();
 172     Foo g3 = new Foo();
 173
 174     g0.x = p0;
 175     p0.x = g1;
 176
 177     g2.x = p1;
 178     p1.x = g3;
 179
 180     p0.y = p1;
 181     p1.y = p0;
 182   }
 183 }
 184 */
 185
 186
 187 // this empty task should still create a non-empty
 188 // ownership graph showing parameter allocation
 189 // look for the parameter s as a label referencing
 190 // a heap region that is multi-object, flagged, not summary
 191 task Startup( StartupObject s{ initialstate } ) {
 192
 193   //Parameter p0 = new Parameter();
 194
 195   //int a, b, c;
 196
 197   Parameter.proof( null, null );
 198
 199   /*
 200   int a = 1;
 201   int b = 2;
 202   int c = 3;
 203
 204   b = c;
 205   a = b;
 206   */
 207
 208   taskexit( s{ !initialstate } );
 209 }
 210
 211
 212 /*
 213 task NewObjectA( Foo a{ f }, Foo b{ f } ) {
 214
 215     Foo c = new Foo();
 216     Foo d = new Foo();
 217
 218     c.x = d;
 219     a.x = c;
 220
 221     taskexit( a{ !f }, b{ !f } );
 222 }
 223
 224
 225 task NewObjectB( Foo a{ f }, Foo b{ f } ) {
 226
 227     Foo c = new Foo();
 228     Foo d = new Foo();
 229
 230     a.x = c;
 231     c.x = d;
 232
 233     taskexit( a{ !f }, b{ !f } );
 234 }
 235
 236
 237 task NewObjectC( Foo a{ f }, Foo b{ f } ) {
 238
 239     Foo z = new Foo();
 240     a.x = z;
 241     a.y = z;
 242
 243     Foo c;
 244
 245     while( false ) {
 246         c     = new Foo();
 247         Foo f = new Foo();
 248         c.x   = f;
 249         c.y   = f;
 250     }
 251
 252     taskexit( a{ !f }, b{ !f } );
 253 }
 254
 255
 256 task forMethod( Foo p0{ f } ) {
 257
 258     Foo a0;
 259     Foo a1;
 260
 261     while( false ) {
 262         a1 = a0;
 263         if( false ) {
 264             a0 = new Foo();
 265         }
 266     }
 267
 268     Foo z = new Foo();
 269     a1.x = z;
 270     z.x  = a1;
 271
 272
 273     taskexit( p0{ !f } );
 274 }
 275
 276
 277 // this task allocates a new object, so there should
 278 // be a heap region for the parameter, and several
 279 // heap regions for the allocation site, but the label
 280 // merely points to the newest region
 281 task NewObjectInMethod( Voo v{ f } ) {
 282     Voo w = new Voo();
 283     Baw b = new Baw();
 284     b.doTheBaw( w );
 285
 286     taskexit( v{ !f } );
 287 }
 288
 289
 290 task ClobberInitParamReflex( Voo v{ f }, Voo w{ f } ) {
 291     v.b = v.bb;
 292
 293     taskexit( v{ !f }, w{ !f } );
 294 }
 295
 296
 297 task BackToItself( Parameter p0{ w } ) {
 298
 299     Penguin p = new Penguin();
 300     p0.p = p;
 301     p.h = p0.h;
 302
 303     while( false ) {
 304         Parameter p1   = new Parameter();
 305                   p1.h = new Foo();
 306         Penguin   q    = new Penguin();
 307         p1.p = q;
 308         q.h  = p1.h;
 309     }
 310
 311     taskexit( p0{ !w } );
 312 }
 313
 314
 315 task SummaryNodeTokens( Foo p0{ f } ) {
 316
 317     while( false ) {
 318         Foo a = new Foo();
 319         a.x   = new Foo();
 320         a.x.x = new Foo();
 321     }
 322
 323     Foo b;
 324     while( false ) {
 325         Foo c = new Foo();
 326         c.x = b;
 327         b = c;
 328     }
 329
 330     taskexit( p0{ !f } );
 331 }
 332
 333
 334 task strongUpdates( Foo p0{ f } ) {
 335
 336     Foo b = new Foo();
 337
 338     Foo a = new Foo();
 339     if( false ) {
 340         a.x = new Foo();
 341         a.y = new Foo();
 342     } else if( false ) {
 343         a.x = new Foo();
 344         a.y = new Foo();
 345     }
 346
 347     // this should effect a strong update
 348     a.x = b;
 349
 350
 351     if( false ) {
 352         p0.x = new Foo();
 353         p0.y = new Foo();
 354     } else if( false ) {
 355         p0.x = new Foo();
 356         p0.y = new Foo();
 357     }
 358
 359     // p0 points to a multiple-object heap region
 360     // so this should not make a strong update
 361     p0.x = b;
 362
 363     taskexit( p0{ !f } );
 364 }
 365
 366
 367 task ObjectChainByMethodCalls( Foo a{ f } ) {
 368
 369   Foo f = a.getAFoo();
 370   Foo g = a.newFooChain( f );
 371   // g -> f
 372
 373   taskexit( a{ !f } );
 374 }
 375
 376
 377 task arrayAssignments( Foo a{ f } ) {
 378
 379   Foo f[] = new Foo[3];
 380
 381   Foo g = new Foo();
 382   Foo h = new Foo();
 383
 384   f[1] = g;
 385   f[2] = h;
 386
 387   Foo i = f[0];
 388
 389   taskexit( a{ !f } );
 390 }
 391
 392
 393 public class Zool {
 394   public Zool() {}
 395
 396   public static void FooToBaw( Baw x, Foo y ) {
 397     x.f.b = y.b;
 398   }
 399 }
 400
 401 task showPrunedEdgesInMethodCall( Foo a{ f } ) {
 402
 403   Foo b = new Foo();
 404   b.x   = a;
 405   b.y   = new Foo();
 406   b.b   = new Baw();
 407
 408   Baw c = new Baw();
 409   c.f   = new Foo();
 410   c.f.b = new Baw();
 411
 412   Zool.FooToBaw( c, b );
 413
 414   taskexit( a{ !f } );
 415 }
 416
 417 task showStringIsImmutable( Foo a{ f } ) {
 418
 419   Baw x = new Baw();
 420   Baw y = new Baw();
 421
 422   Foo f = new Foo();
 423   String s = new String();
 424
 425   x.f = f;
 426   y.f = f;
 427
 428   x.s = s;
 429   y.s = s;
 430
 431   taskexit( a{ !f } );
 432 }
 433
 434
 435 task methodTest( Foo p0{ f } ) {
 436
 437     Foo up0 = new Foo();
 438     Foo up1 = new Foo();
 439     Foo up2 = new Foo();
 440
 441     Foo a0;
 442     Foo a1;
 443
 444     if( false ) {
 445         a0    = new Foo();
 446         up0.x = a0;
 447         a0.x  = new Foo();
 448         //Foo temp = new Foo();
 449     }
 450
 451     if( false ) {
 452         a0    = new Foo();
 453         a0.x  = new Foo();
 454         a1    = a0;
 455         up1.x = a0;
 456     }
 457
 458     if( false ) {
 459         a1    = new Foo();
 460         up2.x = a1;
 461     }
 462
 463     // Foo.test( a0, a1 );
 464
 465     taskexit( p0{ !f } );
 466 }
 467
 468
 469 task getNewFromMethod( Foo p0{ f } ) {
 470   Voo g = Voo.getAVoo( null );
 471
 472   taskexit( p0{ !f } );
 473 }
 474 */
 475
 476 /*
 477 task methodTest01_( Foo p0{ f }, Foo p1{ f } ) {
 478
 479   Foo a0before = new Foo();
 480   if( false ) {
 481     a0before.x = new Foo();
 482   } else {
 483     a0before.x = new Foo();
 484   }
 485
 486   Foo a0after = new Foo();
 487   if( false ) {
 488     a0after.x = new Foo();
 489   } else {
 490     a0after.x = new Foo();
 491   }
 492
 493   Foo.m1_( a0after );
 494
 495
 496   taskexit( p0{ !f }, p1{ !f } );
 497 }
 498 */
 499
 500 /*
 501 task methodTest02_( Foo p0{ f }, Foo p1{ f } ) {
 502
 503   Foo a0before = new Foo();
 504   if( false ) {
 505     a0before.x = new Foo();
 506   } else {
 507     a0before.x = new Foo();
 508   }
 509
 510   Foo a0after = new Foo();
 511   if( false ) {
 512     a0after.x = new Foo();
 513   } else {
 514     a0after.x = new Foo();
 515   }
 516
 517   Foo.m2_( a0after );
 518
 519
 520   taskexit( p0{ !f }, p1{ !f } );
 521 }
 522
 523
 524 task methodTest03_( Foo p0{ f }, Foo p1{ f } ) {
 525
 526   Foo a0before = new Foo();
 527   if( false ) {
 528     a0before.x = new Foo();
 529   } else {
 530     a0before.x = new Foo();
 531   }
 532
 533   Foo a0after = new Foo();
 534   if( false ) {
 535     a0after.x = new Foo();
 536   } else {
 537     a0after.x = new Foo();
 538   }
 539
 540   Foo.m3_( a0after );
 541
 542
 543   taskexit( p0{ !f }, p1{ !f } );
 544 }
 545
 546
 547 task methodTest04_( Foo p0{ f }, Foo p1{ f } ) {
 548
 549   Foo a0before = new Foo();
 550   if( false ) {
 551     a0before.x = new Foo();
 552   } else {
 553     a0before.x = new Foo();
 554   }
 555
 556   Foo a0after = new Foo();
 557   if( false ) {
 558     a0after.x = new Foo();
 559   } else {
 560     a0after.x = new Foo();
 561   }
 562
 563   Foo.m4_( a0after );
 564
 565
 566   taskexit( p0{ !f }, p1{ !f } );
 567 }
 568
 569
 570 task methodTest05_( Foo p0{ f }, Foo p1{ f } ) {
 571
 572   Foo a0before = new Foo();
 573   if( false ) {
 574     a0before.x = new Foo();
 575   } else {
 576     a0before.x = new Foo();
 577   }
 578
 579   Foo a0after = new Foo();
 580   if( false ) {
 581     a0after.x = new Foo();
 582   } else {
 583     a0after.x = new Foo();
 584   }
 585
 586   Foo.m5_( a0after );
 587
 588
 589   taskexit( p0{ !f }, p1{ !f } );
 590 }
 591
 592
 593 task methodTest06_( Foo p0{ f }, Foo p1{ f } ) {
 594
 595   Foo a0before = new Foo();
 596   if( false ) {
 597     a0before.x = new Foo();
 598   } else {
 599     a0before.x = new Foo();
 600   }
 601
 602   Foo a0after = new Foo();
 603   if( false ) {
 604     a0after.x = new Foo();
 605   } else {
 606     a0after.x = new Foo();
 607   }
 608
 609   Foo a1before = new Foo();
 610   if( false ) {
 611     a1before.x = new Foo();
 612   } else {
 613     a1before.x = new Foo();
 614   }
 615
 616   Foo a1after = new Foo();
 617   if( false ) {
 618     a1after.x = new Foo();
 619   } else {
 620     a1after.x = new Foo();
 621   }
 622
 623   Foo.m6_( a0after, a1after );
 624
 625
 626   taskexit( p0{ !f }, p1{ !f } );
 627 }
 628
 629
 630 task methodTest07_( Foo p0{ f }, Foo p1{ f } ) {
 631
 632   Foo a0before = new Foo();
 633   if( false ) {
 634     a0before.x = new Foo();
 635   } else {
 636     a0before.x = new Foo();
 637   }
 638
 639   Foo a0after = new Foo();
 640   if( false ) {
 641     a0after.x = new Foo();
 642   } else {
 643     a0after.x = new Foo();
 644   }
 645
 646   Foo a1before = new Foo();
 647   if( false ) {
 648     a1before.x = new Foo();
 649   } else {
 650     a1before.x = new Foo();
 651   }
 652
 653   Foo a1after = new Foo();
 654   if( false ) {
 655     a1after.x = new Foo();
 656   } else {
 657     a1after.x = new Foo();
 658   }
 659
 660   Foo.m7_( a0after, a1after );
 661
 662
 663   taskexit( p0{ !f }, p1{ !f } );
 664 }
 665
 666
 667 task methodTest08_( Foo p0{ f }, Foo p1{ f } ) {
 668
 669   Foo a0before = new Foo();
 670   if( false ) {
 671     a0before.x = new Foo();
 672   } else {
 673     a0before.x = new Foo();
 674   }
 675
 676   Foo a0after = new Foo();
 677   if( false ) {
 678     a0after.x = new Foo();
 679   } else {
 680     a0after.x = new Foo();
 681   }
 682
 683   Foo a1before = new Foo();
 684   if( false ) {
 685     a1before.x = new Foo();
 686   } else {
 687     a1before.x = new Foo();
 688   }
 689
 690   Foo a1after = new Foo();
 691   if( false ) {
 692     a1after.x = new Foo();
 693   } else {
 694     a1after.x = new Foo();
 695   }
 696
 697   Foo.m8_( a0after, a1after );
 698
 699
 700   taskexit( p0{ !f }, p1{ !f } );
 701 }
 702 */