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