Robust/src/Analysis/Disjoint/DefiniteReachState.java

   1 package Analysis.Disjoint;
   2
   3 import java.io.*;
   4 import java.util.*;
   5
   6 import IR.*;
   7 import IR.Flat.*;
   8 import Util.*;
   9
  10
  11 public class DefiniteReachState {
  12
  13   // R
  14   //
  15   // Maps two variables to an edge (x, y, e) to an unused value when the
  16   // object of x is already reachable from the object of y, and the
  17   // set of edges conservatively gives the path.
  18   // NOTE: Use EdgeKey instead of edges because this analysis's
  19   // scope is beyond the scope of a single reach graph.
  20   private static MultiViewMapBuilder<Object> RBuilder;
  21   private static BitSet viewRfull;
  22   private static BitSet viewR0;
  23   private static BitSet viewR1;
  24   private static BitSet viewR2;
  25   private static BitSet viewR01;
  26   private MultiViewMap<Object> R;
  27
  28
  29   // Rs
  30   //
  31   // Tracks whether the analysis must know the definite reachability
  32   // information of a given variable.
  33   private enum DefReachKnown {
  34     UNKNOWN,
  35     KNOWN,
  36   }
  37   private Map<TempDescriptor, DefReachKnown> Rs;
  38
  39
  40   // Fu (field upstream)
  41   //
  42   // Maps a variable that points to object o0 to the
  43   // set of variables that point to objects o1...oN
  44   // that have a reference to o0.
  45   private class FuSource {
  46     DefReachKnown  isKnown;
  47     TempDescriptor knownSrc;
  48     public FuSource() {
  49       this.isKnown  = DefReachKnown.UNKNOWN;
  50       this.knownSrc = null;
  51     }
  52     public FuSource( TempDescriptor src ) {
  53       assert( src != null );
  54       this.isKnown  = DefReachKnown.KNOWN;
  55       this.knownSrc = src;
  56     }
  57     public boolean equals( Object o ) {
  58       if( !(o instanceof FuSource) ) {
  59         return false;
  60       }
  61       FuSource fus = (FuSource)o;
  62       return
  63         this.isKnown  == fus.isKnown  &&
  64         this.knownSrc == fus.knownSrc;
  65     }
  66     public int hashCode() {
  67       int hash = 0;
  68       if( isKnown == DefReachKnown.KNOWN ) {
  69         hash = 123451;
  70       }
  71       if( knownSrc != null ) {
  72         hash ^= knownSrc.hashCode();
  73       }
  74       return hash;
  75     }
  76     public String toString() {
  77       if( isKnown == DefReachKnown.UNKNOWN ) {
  78         return "unknown";
  79       }
  80       return knownSrc.toString();
  81     }
  82   }
  83   private static MultiViewMapBuilder<Object> FuBuilder;
  84   private static BitSet viewFufull;
  85   private static BitSet viewFu0;
  86   private static BitSet viewFu1;
  87   private MultiViewMap<Object> Fu;
  88
  89
  90   // Fd (field downstream)
  91   //
  92   // Entries <x, f, y> mean x.f points directly at what
  93   // y points at.
  94   public class FdEntry {
  95     TempDescriptor  y;
  96     FieldDescriptor f0;
  97     TempDescriptor  z;
  98     public FdEntry( TempDescriptor  y,
  99                     FieldDescriptor f0,
 100                     TempDescriptor  z ) {
 101       this.y  = y;
 102       this.f0 = f0;
 103       this.z  = z;
 104     }
 105   }
 106   private static MultiViewMapBuilder<Object> FdBuilder;
 107   private static BitSet viewFd0;
 108   private static BitSet viewFd2;
 109   private MultiViewMap<Object> Fd;
 110
 111
 112
 113
 114
 115   // call before instantiating this class
 116   static public void initBuilders() {
 117
 118     RBuilder =
 119       new MultiViewMapBuilder<Object>( new Class[] {
 120                                          TempDescriptor.class,
 121                                          TempDescriptor.class,
 122                                          EdgeKey.class },
 123                                        new JoinOpNop() );
 124     viewRfull = RBuilder.getFullView();
 125     viewR0    = RBuilder.addPartialView( 0 );
 126     viewR1    = RBuilder.addPartialView( 1 );
 127     viewR2    = RBuilder.addPartialView( 2 );
 128     viewR01   = RBuilder.addPartialView( 0, 1 );
 129     RBuilder.setCheckTypes( true );
 130     RBuilder.setCheckConsistency( true );
 131
 132
 133     FuBuilder =
 134       new MultiViewMapBuilder<Object>( new Class[] {
 135                                          TempDescriptor.class,
 136                                          FuSource.class},
 137                                        new JoinOpNop() );
 138     viewFufull = FuBuilder.getFullView();
 139     viewFu0    = FuBuilder.addPartialView( 0 );
 140     viewFu1    = FuBuilder.addPartialView( 1 );
 141     FuBuilder.setCheckTypes( true );
 142     FuBuilder.setCheckConsistency( true );
 143
 144
 145     FdBuilder =
 146       new MultiViewMapBuilder<Object>( new Class[] {
 147                                          TempDescriptor.class,
 148                                          FieldDescriptor.class,
 149                                          TempDescriptor.class},
 150                                        new JoinOpNop() );
 151     viewFd0 = FdBuilder.addPartialView( 0 );
 152     viewFd2 = FdBuilder.addPartialView( 2 );
 153     FdBuilder.setCheckTypes( true );
 154     FdBuilder.setCheckConsistency( true );
 155   }
 156
 157
 158
 159   public DefiniteReachState( DefiniteReachState toCopy ) {
 160     this.R  = toCopy.R.clone( RBuilder );
 161     this.Rs = new HashMap<TempDescriptor, DefReachKnown>( toCopy.Rs );
 162     this.Fu = toCopy.Fu.clone( FuBuilder );
 163     this.Fd = toCopy.Fd.clone( FdBuilder );
 164   }
 165
 166
 167   public DefiniteReachState() {
 168     R  = RBuilder.build();
 169     Rs = new HashMap<TempDescriptor, DefReachKnown>();
 170     Fu = FuBuilder.build();
 171     Fd = FdBuilder.build();
 172   }
 173
 174
 175
 176
 177   public boolean isAlreadyReachable( TempDescriptor a,
 178                                      TempDescriptor b ) {
 179
 180     boolean case1 = !R.get( viewR01, MultiKey.factory( a, b ) ).isEmpty();
 181
 182     boolean case3 = false;
 183     if( Rs.get( b ) != null &&
 184         Rs.get( b ) == DefReachKnown.KNOWN &&
 185         Fu.get( viewFufull, MultiKey.factory( b, new FuSource() ) ).isEmpty()
 186         ) {
 187       boolean allEntriesOk = true;
 188       for( MultiKey fullKeyB : Fu.get( viewFu0,
 189                                        MultiKey.factory( b ) ).keySet()
 190            ) {
 191         if( R.get( viewR01,
 192                    MultiKey.factory( a,
 193                                      ((FuSource)fullKeyB.get( 1 )).knownSrc
 194                                      ) ).isEmpty()
 195             ) {
 196           allEntriesOk = false;
 197           break;
 198         }
 199       }
 200       case3 = allEntriesOk;
 201     }
 202
 203     return case1 || case3;
 204   }
 205
 206
 207
 208   public Set<FdEntry> edgesToElidePropagation( TempDescriptor x,
 209                                                TempDescriptor y ) {
 210     // return the set of edges that definite reach analysis tells
 211     // us we can elide propagating reach info across during the
 212     // store: x.f = y
 213
 214     Set<FdEntry> out = new HashSet<FdEntry>();
 215
 216     // we have to know something about y
 217     DefReachKnown known = Rs.get( y );
 218     if( known == null || known == DefReachKnown.UNKNOWN ) {
 219       return out;
 220     }
 221
 222     // find all 'y points at' entries in Fd
 223     MultiKey keyY = MultiKey.factory( y );
 224     Map<MultiKey, Object> mapY0 = Fd.get( viewFd0, keyY );
 225
 226     for( MultiKey fullKeyY : mapY0.keySet() ) {
 227       // if y.f0 points at z, and z is already reachable from x,
 228       // include the edge y.f0->z
 229       FieldDescriptor f0 = (FieldDescriptor) fullKeyY.get( 1 );
 230       TempDescriptor  z  = (TempDescriptor)  fullKeyY.get( 2 );
 231
 232       if( isAlreadyReachable( z, x ) ) {
 233         out.add( new FdEntry( y, f0, z ) );
 234       }
 235     }
 236
 237     return out;
 238   }
 239
 240
 241
 242
 243   public void methodEntry( Set<TempDescriptor> parameters ) {
 244     methodEntryR ( parameters );
 245     methodEntryRs( parameters );
 246     methodEntryFu( parameters );
 247     methodEntryFd( parameters );
 248   }
 249
 250   public void copy( TempDescriptor x,
 251                     TempDescriptor y ) {
 252     copyR ( x, y );
 253     copyRs( x, y );
 254     copyFu( x, y );
 255     copyFd( x, y );
 256   }
 257
 258   public void load( TempDescriptor x,
 259                     TempDescriptor y,
 260                     FieldDescriptor f,
 261                     Set<EdgeKey> edgeKeysForLoad ) {
 262
 263     loadR ( x, y, f, edgeKeysForLoad );
 264     loadRs( x, y, f, edgeKeysForLoad );
 265     loadFu( x, y, f, edgeKeysForLoad );
 266     loadFd( x, y, f, edgeKeysForLoad );
 267   }
 268
 269   public void store( TempDescriptor x,
 270                      FieldDescriptor f,
 271                      TempDescriptor y,
 272                      Set<EdgeKey> edgeKeysRemoved,
 273                      Set<EdgeKey> edgeKeysAdded ) {
 274
 275     storeR ( x, f, y, edgeKeysRemoved, edgeKeysAdded );
 276     storeRs( x, f, y, edgeKeysRemoved, edgeKeysAdded );
 277     storeFu( x, f, y, edgeKeysRemoved, edgeKeysAdded );
 278     storeFd( x, f, y, edgeKeysRemoved, edgeKeysAdded );
 279   }
 280
 281   public void newObject( TempDescriptor x ) {
 282     newObjectR ( x );
 283     newObjectRs( x );
 284     newObjectFu( x );
 285     newObjectFd( x );
 286   }
 287
 288   public void methodCall( TempDescriptor retVal ) {
 289     methodCallR ( retVal );
 290     methodCallRs( retVal );
 291     methodCallFu( retVal );
 292     methodCallFd( retVal );
 293   }
 294
 295   public void merge( DefiniteReachState that ) {
 296     mergeR ( that );
 297     mergeRs( that );
 298     mergeFu( that );
 299     mergeFd( that );
 300   }
 301
 302
 303
 304
 305
 306
 307   public void methodEntryR( Set<TempDescriptor> parameters ) {
 308     R.clear();
 309   }
 310
 311   public void copyR( TempDescriptor x,
 312                      TempDescriptor y ) {
 313     // consider that x and y can be the same, so do the
 314     // parts of the update in the right order:
 315
 316     // first get all info for update
 317     MultiKey keyY = MultiKey.factory( y );
 318     Map<MultiKey, Object> mapY0 = R.get( viewR0, keyY );
 319     Map<MultiKey, Object> mapY1 = R.get( viewR1, keyY );
 320
 321     // then remove anything
 322     MultiKey keyX = MultiKey.factory( x );
 323     R.remove( viewR0, keyX );
 324     R.remove( viewR1, keyX );
 325
 326     // then insert new stuff
 327     for( MultiKey fullKeyY : mapY0.keySet() ) {
 328       MultiKey fullKeyX = MultiKey.factory( x,
 329                                             fullKeyY.get( 1 ),
 330                                             fullKeyY.get( 2 ) );
 331       R.put( fullKeyX, MultiViewMap.dummyValue );
 332     }
 333     for( MultiKey fullKeyY : mapY1.keySet() ) {
 334       MultiKey fullKeyX = MultiKey.factory( fullKeyY.get( 0 ),
 335                                             x,
 336                                             fullKeyY.get( 2 ) );
 337       R.put( fullKeyX, MultiViewMap.dummyValue );
 338     }
 339   }
 340
 341   public void loadR( TempDescriptor x,
 342                      TempDescriptor y,
 343                      FieldDescriptor f,
 344                      Set<EdgeKey> edgeKeysForLoad ) {
 345     // consider that x and y can be the same, so do the
 346     // parts of the update in the right order:
 347
 348     // first get all info for update
 349     MultiKey keyY = MultiKey.factory( y );
 350     Map<MultiKey, Object> mapY0 = R.get( viewR0, keyY );
 351
 352     // then remove anything
 353     MultiKey keyX = MultiKey.factory( x );
 354     R.remove( viewR0, keyX );
 355     R.remove( viewR1, keyX );
 356
 357     // then insert new stuff
 358     for( EdgeKey e : edgeKeysForLoad ) {
 359       R.put( MultiKey.factory( x, y, e ), MultiViewMap.dummyValue );
 360
 361       for( MultiKey fullKeyY : mapY0.keySet() ) {
 362         R.put( MultiKey.factory( x,
 363                                  fullKeyY.get( 1 ),
 364                                  e ),
 365                MultiViewMap.dummyValue );
 366
 367         R.put( MultiKey.factory( x,
 368                                  fullKeyY.get( 1 ),
 369                                  fullKeyY.get( 2 ) ),
 370                MultiViewMap.dummyValue );
 371       }
 372     }
 373   }
 374
 375   public void storeR( TempDescriptor x,
 376                       FieldDescriptor f,
 377                       TempDescriptor y,
 378                       Set<EdgeKey> edgeKeysRemoved,
 379                       Set<EdgeKey> edgeKeysAdded ) {
 380
 381     for( EdgeKey edgeKeyWZ : edgeKeysRemoved ) {
 382       R.remove( viewR2, MultiKey.factory( edgeKeyWZ ) );
 383     }
 384
 385     for( EdgeKey edgeKeyXY : edgeKeysAdded ) {
 386       R.put( MultiKey.factory( y, x, edgeKeyXY ), MultiViewMap.dummyValue );
 387     }
 388   }
 389
 390   public void newObjectR( TempDescriptor x ) {
 391     MultiKey keyX = MultiKey.factory( x );
 392     R.remove( viewR0, keyX );
 393     R.remove( viewR1, keyX );
 394   }
 395
 396   public void methodCallR( TempDescriptor retVal ) {
 397     MultiKey keyRetVal = MultiKey.factory( retVal );
 398     R.remove( viewR0, keyRetVal );
 399     R.remove( viewR1, keyRetVal );
 400   }
 401
 402   public void mergeR( DefiniteReachState that ) {
 403     for( MultiKey key : this.R.get().keySet() ) {
 404       if( that.R.get( viewRfull, key ).isEmpty() ) {
 405         this.R.remove( viewRfull, key );
 406       }
 407     }
 408   }
 409
 410
 411
 412
 413
 414
 415
 416
 417   public void methodEntryRs( Set<TempDescriptor> parameters ) {
 418     Rs.clear();
 419     for( TempDescriptor p : parameters ) {
 420       Rs.put( p, DefReachKnown.UNKNOWN );
 421     }
 422   }
 423
 424   public void copyRs( TempDescriptor x,
 425                       TempDescriptor y ) {
 426     DefReachKnown valRs = Rs.get( y );
 427     if( valRs != null ) {
 428       Rs.put( x, valRs );
 429     }
 430   }
 431
 432   public void loadRs( TempDescriptor x,
 433                       TempDescriptor y,
 434                       FieldDescriptor f,
 435                       Set<EdgeKey> edgeKeysForLoad ) {
 436     Rs.put( x, DefReachKnown.UNKNOWN );
 437   }
 438
 439   public void storeRs( TempDescriptor x,
 440                        FieldDescriptor f,
 441                        TempDescriptor y,
 442                        Set<EdgeKey> edgeKeysRemoved,
 443                        Set<EdgeKey> edgeKeysAdded ) {
 444   }
 445
 446   public void newObjectRs( TempDescriptor x ) {
 447     Rs.put( x, DefReachKnown.KNOWN );
 448   }
 449
 450   public void methodCallRs( TempDescriptor retVal ) {
 451     Rs.put( retVal, DefReachKnown.UNKNOWN );
 452   }
 453
 454   private void mergeRs( DefiniteReachState that ) {
 455     Set<TempDescriptor> allVars = new HashSet<TempDescriptor>();
 456     allVars.addAll( this.Rs.keySet() );
 457     allVars.addAll( that.Rs.keySet() );
 458     for( TempDescriptor x : allVars ) {
 459       DefReachKnown vThis = this.Rs.get( x );
 460       DefReachKnown vThat = that.Rs.get( x );
 461       if( vThis != null && vThis.equals( DefReachKnown.KNOWN ) &&
 462           vThat != null && vThat.equals( DefReachKnown.KNOWN ) ) {
 463         this.Rs.put( x, DefReachKnown.KNOWN );
 464       } else {
 465         this.Rs.put( x, DefReachKnown.UNKNOWN );
 466       }
 467     }
 468   }
 469
 470
 471
 472
 473
 474
 475
 476
 477   public void methodEntryFu( Set<TempDescriptor> parameters ) {
 478     Fu.clear();
 479   }
 480
 481   public void copyFu( TempDescriptor x,
 482                       TempDescriptor y ) {
 483     // consider that x and y can be the same, so do the
 484     // parts of the update in the right order:
 485
 486     // first get all info for update
 487     MultiKey keyY    = MultiKey.factory( y );
 488     MultiKey keyYsrc = MultiKey.factory( new FuSource( y ) );
 489     Map<MultiKey, Object> mapY0 = Fu.get( viewFu0, keyY );
 490     Map<MultiKey, Object> mapY1 = Fu.get( viewFu1, keyYsrc );
 491
 492     MultiKey keyXsrc = MultiKey.factory( new FuSource( x ) );
 493     Map<MultiKey, Object> mapX1 = Fu.get( viewFu1, keyXsrc );
 494
 495     // then remove anything
 496     MultiKey keyX = MultiKey.factory( x );
 497     Fu.remove( viewFu0, keyX );
 498     Fu.remove( viewFu1, keyXsrc );
 499
 500     // then insert new stuff
 501     for( MultiKey fullKeyY : mapY0.keySet() ) {
 502       MultiKey fullKeyX = MultiKey.factory( x,
 503                                             fullKeyY.get( 1 ) );
 504       Fu.put( fullKeyX, MultiViewMap.dummyValue );
 505     }
 506     for( MultiKey fullKeyY : mapY1.keySet() ) {
 507       MultiKey fullKeyX = MultiKey.factory( fullKeyY.get( 0 ),
 508                                             new FuSource( x ) );
 509       Fu.put( fullKeyX, MultiViewMap.dummyValue );
 510     }
 511     for( MultiKey fullKeyXsrc : mapX1.keySet() ) {
 512       Fu.put( MultiKey.factory( fullKeyXsrc.get( 0 ),
 513                                 new FuSource() ),
 514               MultiViewMap.dummyValue );
 515     }
 516   }
 517
 518   public void loadFu( TempDescriptor x,
 519                       TempDescriptor y,
 520                       FieldDescriptor f,
 521                       Set<EdgeKey> edgeKeysForLoad ) {
 522
 523     // first get all info for update
 524     MultiKey keyXsrc = MultiKey.factory( new FuSource( x ) );
 525     Map<MultiKey, Object> mapX1 = Fu.get( viewFu1, keyXsrc );
 526
 527     MultiKey keyX = MultiKey.factory( x );
 528     // then remove anything
 529     Fu.remove( viewFu0, keyX );
 530     Fu.remove( viewFu1, keyXsrc );
 531
 532     // then insert new stuff
 533     for( MultiKey fullKeyXsrc : mapX1.keySet() ) {
 534       Fu.put( MultiKey.factory( fullKeyXsrc.get( 0 ),
 535                                 new FuSource() ),
 536               MultiViewMap.dummyValue );
 537     }
 538   }
 539
 540   public void storeFu( TempDescriptor x,
 541                        FieldDescriptor f,
 542                        TempDescriptor y,
 543                        Set<EdgeKey> edgeKeysRemoved,
 544                        Set<EdgeKey> edgeKeysAdded ) {
 545
 546     Fu.put( MultiKey.factory( y, new FuSource( x ) ),
 547             MultiViewMap.dummyValue );
 548   }
 549
 550   public void newObjectFu( TempDescriptor x ) {
 551     MultiKey keyXsrc = MultiKey.factory( new FuSource( x ) );
 552     Map<MultiKey, Object> mapX1 = Fu.get( viewFu1, keyXsrc );
 553
 554     MultiKey keyX = MultiKey.factory( x );
 555     Fu.remove( viewFu0, keyX );
 556     Fu.remove( viewFu1, keyXsrc );
 557
 558     for( MultiKey fullKeyXsrc : mapX1.keySet() ) {
 559       Fu.put( MultiKey.factory( fullKeyXsrc.get( 0 ),
 560                                 new FuSource() ),
 561               MultiViewMap.dummyValue );
 562     }
 563   }
 564
 565   public void methodCallFu( TempDescriptor retVal ) {
 566     MultiKey keyRetValsrc = MultiKey.factory( new FuSource( retVal ) );
 567     Map<MultiKey, Object> mapRetVal1 = Fu.get( viewFu1, keyRetValsrc );
 568
 569     MultiKey keyRetVal = MultiKey.factory( retVal );
 570     Fu.remove( viewFu0, keyRetVal );
 571     Fu.remove( viewFu1, keyRetValsrc );
 572
 573     for( MultiKey fullKeyRetValsrc : mapRetVal1.keySet() ) {
 574       Fu.put( MultiKey.factory( fullKeyRetValsrc.get( 0 ),
 575                                 new FuSource() ),
 576               MultiViewMap.dummyValue );
 577     }
 578   }
 579
 580   public void mergeFu( DefiniteReachState that ) {
 581     this.Fu.merge( that.Fu );
 582   }
 583
 584
 585
 586
 587
 588
 589   public void methodEntryFd( Set<TempDescriptor> parameters ) {
 590     Fd.clear();
 591   }
 592
 593   public void copyFd( TempDescriptor x,
 594                      TempDescriptor y ) {
 595     // consider that x and y can be the same, so do the
 596     // parts of the update in the right order:
 597
 598     // first get all info for update
 599     MultiKey keyY = MultiKey.factory( y );
 600     Map<MultiKey, Object> mapY0 = Fd.get( viewFd0, keyY );
 601     Map<MultiKey, Object> mapY2 = Fd.get( viewFd2, keyY );
 602
 603     // then remove anything
 604     MultiKey keyX = MultiKey.factory( x );
 605     Fd.remove( viewFd0, keyX );
 606     Fd.remove( viewFd2, keyX );
 607
 608     // then insert new stuff
 609     for( MultiKey fullKeyY : mapY0.keySet() ) {
 610       MultiKey fullKeyX = MultiKey.factory( x,
 611                                             fullKeyY.get( 1 ),
 612                                             fullKeyY.get( 2 ) );
 613       Fd.put( fullKeyX, MultiViewMap.dummyValue );
 614     }
 615     for( MultiKey fullKeyY : mapY2.keySet() ) {
 616       MultiKey fullKeyX = MultiKey.factory( fullKeyY.get( 0 ),
 617                                             fullKeyY.get( 1 ),
 618                                             x );
 619       Fd.put( fullKeyX, MultiViewMap.dummyValue );
 620     }
 621   }
 622
 623   public void loadFd( TempDescriptor x,
 624                      TempDescriptor y,
 625                      FieldDescriptor f,
 626                      Set<EdgeKey> edgeKeysForLoad ) {
 627
 628     MultiKey keyX = MultiKey.factory( x );
 629     Fd.remove( viewFd0, keyX );
 630     Fd.remove( viewFd2, keyX );
 631   }
 632
 633   public void storeFd( TempDescriptor x,
 634                       FieldDescriptor f,
 635                       TempDescriptor y,
 636                       Set<EdgeKey> edgeKeysFdemoved,
 637                       Set<EdgeKey> edgeKeysAdded ) {
 638     Fd.put( MultiKey.factory( x, f, y ),
 639             MultiViewMap.dummyValue );
 640   }
 641
 642   public void newObjectFd( TempDescriptor x ) {
 643     MultiKey keyX = MultiKey.factory( x );
 644     Fd.remove( viewFd0, keyX );
 645     Fd.remove( viewFd2, keyX );
 646   }
 647
 648   public void methodCallFd( TempDescriptor retVal ) {
 649     MultiKey keyRetVal = MultiKey.factory( retVal );
 650     Fd.remove( viewFd0, keyRetVal );
 651     Fd.remove( viewFd2, keyRetVal );
 652   }
 653
 654   public void mergeFd( DefiniteReachState that ) {
 655     this.Fd.merge( that.Fd );
 656   }
 657
 658
 659
 660
 661
 662
 663
 664
 665
 666
 667
 668
 669   public boolean equals( Object o ) {
 670     if( this == o ) {
 671       return true;
 672     }
 673     if( o == null ) {
 674       return false;
 675     }
 676     if( !(o instanceof DefiniteReachState) ) {
 677       return false;
 678     }
 679     DefiniteReachState that = (DefiniteReachState) o;
 680
 681     assert( false );
 682     return false;
 683   }
 684
 685
 686   public int hashCode() {
 687     assert( false );
 688     return 0;
 689   }
 690
 691
 692   public void writeState( String outputName ) {
 693     try {
 694       BufferedWriter bw = new BufferedWriter( new FileWriter( "defReach-"+outputName+".txt" ) );
 695       bw.write( this.toString() );
 696       bw.close();
 697     } catch( IOException e ) {
 698       System.out.println( "ERROR writing definite reachability state:\n  "+e );
 699     }
 700   }
 701
 702
 703   public String toString() {
 704     StringBuilder s = new StringBuilder();
 705
 706     s.append( "R = {\n" );
 707     s.append( R.toString( 2 ) );
 708     s.append( "}\n" );
 709
 710     s.append( "Rs = {\n" );
 711     for( TempDescriptor x : Rs.keySet() ) {
 712       s.append( "  "+x+"->"+Rs.get( x )+"\n" );
 713     }
 714     s.append( "}\n" );
 715
 716     s.append( "Fu = {\n" );
 717     s.append( Fu.toString( 2 ) );
 718     s.append( "}\n" );
 719
 720     s.append( "Fd = {\n" );
 721     s.append( Fd.toString( 2 ) );
 722     s.append( "}\n" );
 723
 724     return s.toString();
 725   }
 726 }