Robust/src/Analysis/Disjoint/ExistPredEdge.java

   1 package Analysis.Disjoint;
   2
   3 import IR.*;
   4 import IR.Flat.*;
   5 import java.util.*;
   6 import java.io.*;
   7
   8 // A edge existence predicate is satisfied if the elements
   9 // defining an edge are part of the given graph.
  10 // The reach state may be null--if not the predicate is
  11 // satisfied when the edge exists AND it has the state.
  12
  13 public class ExistPredEdge extends Canonical {
  14
  15   // the source of an edge is *either* a variable
  16   // node or a heap region node
  17   protected TempDescriptor tdSrc;
  18   protected Integer        hrnSrcID;
  19
  20   // dst is always a heap region
  21   protected Integer        hrnDstID;
  22
  23   // a reference has a field name and type
  24   protected TypeDescriptor type;
  25   protected String         field;
  26
  27   // state can be null
  28   protected ReachState     state;
  29
  30
  31   public ExistPredEdge( TempDescriptor tdSrc,
  32                         Integer        hrnSrcID,
  33                         Integer        hrnDstID,
  34                         TypeDescriptor type,
  35                         String         field,
  36                         ReachState     state ) {
  37
  38     assert (vnSrc == null) || (hrnSrcID == null);
  39     assert hrnDstID != null;
  40     assert type     != null;
  41     assert field    != null;
  42
  43     this.tdSrc    = tdSrc;
  44     this.hrnSrcID = hrnSrcID;
  45     this.hrnDstID = hrnDstID;
  46     this.type     = type;
  47     this.field    = field;
  48     this.state    = state;
  49   }
  50
  51   public boolean isSatisfiedBy( ReachGraph rg ) {
  52
  53     // first establish whether the source of the
  54     // reference edge exists
  55     VariableNode   vnSrc  = rg.td2vn.get( tdSrc );
  56     HeapRegionNode hrnSrc = rg.id2hrn.get( hrnSrcID );
  57     assert (vnSrc == null) || (hrnSrc == null);
  58
  59     // the source is not present in graph
  60     if( vnSrc == null && hrnSrc == null ) {
  61       return false;
  62     }
  63
  64     RefSrcNode rsn;
  65     if( vnSrc != null ) {
  66       rsn = vnSrc;
  67     } else {
  68       rsn = hrnSrc;
  69     }
  70
  71     // is the destination present?
  72     HeapRegionNode hrnDst = rg.id2hrn.get( hrnDstID );
  73     if( hrnDst == null ) {
  74       return false;
  75     }
  76
  77     // is there an edge between them with the given
  78     // type and field?
  79     // TODO: type OR a subtype?
  80     RefEdge edge = rsn.getReferenceTo( hrnDst, type, field );
  81     if( edge == null ) {
  82       return false;
  83     }
  84
  85     // when state is null it is not part of the predicate
  86     // so we've satisfied the edge existence
  87     if( state == null ) {
  88       return true;
  89     }
  90
  91     // otherwise look for state too
  92     // TODO: contains OR containsSuperSet OR containsWithZeroes??
  93     return hrnDst.getAlpha().contains( state );
  94   }
  95
  96
  97   public boolean equals( Object o ) {
  98     if( o == null ) {
  99       return false;
 100     }
 101
 102     if( !(o instanceof ExistPredEdge) ) {
 103       return false;
 104     }
 105
 106     ExistPredEdge epn = (ExistPredEdge) o;
 107
 108     this.tdSrc    = tdSrc;
 109     this.hrnSrcID = hrnSrcID;
 110     this.hrnDstID = hrnDstID;
 111     this.type     = type;
 112     this.field    = field;
 113     this.state    = state;
 114
 115     if( tdSrc == null && epn.tdSrc != null ) {
 116       return false;
 117     } else if( !tdSrc.equals( epn.tdSrc ) ) {
 118       return false;
 119     }
 120
 121     if( hrnSrcID == null && epn.hrnSrcID != null ) {
 122       return false;
 123     } else if( !hrnSrcID.equals( epn.hrnSrcID ) ) {
 124       return false;
 125     }
 126
 127     if( !hrnDstID.equals( epn.hrnDstID ) ) {
 128       return false;
 129     }
 130
 131     if( !type.equals( epn.type ) ) {
 132       return false;
 133     }
 134
 135     if( !field.equals( epn.field ) ) {
 136       return false;
 137     }
 138
 139     // ReachState objects are cannonical
 140     return state == epn.state;
 141   }
 142
 143   public int hashCode() {
 144     int hash = 0;
 145
 146     hash += type.hashCode()*17;
 147
 148     if( field != null ) {
 149       hash += field.hashCode()*7;
 150     }
 151
 152     if( tdSrc != null ) {
 153       hash += tdSrc.hashCode()*11;
 154     } else {
 155       hash += hrnSrcID.hashCode()*11;
 156     }
 157
 158     hash += hrnDst.hashCode();
 159
 160     if( state != null ) {
 161       hash += state.hashCode();
 162     }
 163
 164     return hash;
 165   }
 166
 167
 168   public String toString() {
 169     String s = "(";
 170
 171     if( tdSrc != null ) {
 172       s += tdSrc.toString();
 173     } else {
 174       s += hrnSrcID.toString();
 175     }
 176
 177     s += "-->"+hrnDstID+")";
 178
 179     if( state != null ) {
 180       s += "w"+state;
 181     }
 182
 183     return s;
 184   }
 185 }