001package daikon.inv.unary.scalar;
002
003import daikon.PptSlice;
004import daikon.ProglangType;
005import daikon.VarInfo;
006import daikon.inv.Invariant;
007import daikon.inv.InvariantStatus;
008import daikon.inv.OutputFormat;
009import daikon.inv.ValueSet;
010import org.checkerframework.checker.lock.qual.GuardSatisfied;
011import org.checkerframework.dataflow.qual.Pure;
012import org.checkerframework.dataflow.qual.SideEffectFree;
013import typequals.prototype.qual.Prototype;
014
015/**
016 * IsPointer is an invariant that heuristically determines whether an integer represents a pointer
017 * (a 32-bit memory address). Since both a 32-bit integer and an address have the same
018 * representation, sometimes a a pointer can be mistaken for an integer. When this happens, several
019 * scalar invariants are computed for integer variables. Most of them would not make any sense for
020 * pointers. Determining whether a 32-bit variable is a pointer can thus spare the computation of
021 * many irrelevant invariants.
022 *
023 * <p>The basic approach is to discard the invariant if any values that are not valid pointers are
024 * encountered. By default values between -100,000 and 100,000 (except 0) are considered to be
025 * invalid pointers. This approach has been experimentally confirmed on Windows x86 executables.
026 */
027public class IsPointer extends SingleScalar {
028
029  private static final long serialVersionUID = 20080221L;
030
031  /** Boolean. True iff IsPointer invariants should be considered. */
032  public static boolean dkconfig_enabled = false;
033
034  // pointers values in ff_prepare.dtrace were starting from 65536,
035  // in other dtrace files, the pointer values were even larger
036  private static long largestNonPointerValue = 100000;
037
038  private static long smallestNonPointerValue = -100000;
039
040  protected IsPointer(PptSlice ppt) {
041    super(ppt);
042  }
043
044  protected @Prototype IsPointer() {
045    super();
046  }
047
048  private static @Prototype IsPointer proto = new @Prototype IsPointer();
049
050  /** Returns the prototype invariant for IsPointer. */
051  public static @Prototype IsPointer get_proto() {
052    return proto;
053  }
054
055  @Override
056  protected IsPointer instantiate_dyn(PptSlice slice) {
057    return new IsPointer(slice);
058  }
059
060  @Override
061  public boolean enabled() {
062    return dkconfig_enabled;
063  }
064
065  @Override
066  public boolean instantiate_ok(VarInfo[] vis) {
067    if (!super.valid_types(vis)) {
068      return false;
069    }
070
071    ProglangType file_rep_type = vis[0].file_rep_type;
072
073    return (file_rep_type == ProglangType.INT);
074  }
075
076  @Override
077  public InvariantStatus add_modified(long value, int count) {
078    return check_modified(value, count);
079  }
080
081  @Override
082  public InvariantStatus check_modified(long v, int count) {
083    if (!isWithinPointerRange(v)) {
084      return InvariantStatus.FALSIFIED;
085    }
086    return InvariantStatus.NO_CHANGE;
087  }
088
089  @Pure
090  private boolean isWithinPointerRange(long value) {
091    if (value == 0) {
092      return true;
093    }
094    return (value >= largestNonPointerValue) || (value <= smallestNonPointerValue);
095  }
096
097  @Override
098  @SideEffectFree
099  public String format_using(@GuardSatisfied IsPointer this, OutputFormat format) {
100    String varname = var().name_using(format);
101    if (format == OutputFormat.SIMPLIFY) {
102      // trivially true
103      return "(AND)";
104    } else if (format == OutputFormat.JAVA) {
105      return "daikon.tools.runtimechecker.Runtime.isWithinPointerRange(" + varname + ")";
106    } else {
107      return varname + " is a pointer";
108    }
109  }
110
111  @Override
112  protected double computeConfidence() {
113    return 1 - computeProbability();
114  }
115
116  // computes the probability that this is the result
117  // of chance
118  protected double computeProbability() {
119    assert !falsified;
120
121    ValueSet.ValueSetScalar vs = (ValueSet.ValueSetScalar) ppt.var_infos[0].get_value_set();
122
123    if (!isWithinPointerRange(vs.max()) || !isWithinPointerRange(vs.min())) {
124      return Invariant.PROBABILITY_UNJUSTIFIED;
125    }
126
127    return Invariant.PROBABILITY_JUSTIFIED;
128  }
129
130  @Pure
131  @Override
132  public boolean isSameFormula(Invariant other) {
133    assert other instanceof IsPointer;
134    return true;
135  }
136}