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}