|
| 1 | +/** |
| 2 | + * Provides classes for representing abstract bounds for use in, for example, range analysis. |
| 3 | + */ |
| 4 | + |
| 5 | +private import codeql.util.Location |
| 6 | + |
| 7 | +signature module BoundDefinitions<LocationSig Location> { |
| 8 | + class Type; |
| 9 | + class IntegralType extends Type; |
| 10 | + |
| 11 | + class ConstantIntegerExpr extends Expr { |
| 12 | + int getIntValue(); |
| 13 | + } |
| 14 | + |
| 15 | + class SsaSourceVariable { |
| 16 | + Type getType(); |
| 17 | + } |
| 18 | + |
| 19 | + class SsaVariable { |
| 20 | + SsaSourceVariable getSourceVariable(); |
| 21 | + string toString(); |
| 22 | + Location getLocation(); |
| 23 | + Expr getAUse(); |
| 24 | + } |
| 25 | + |
| 26 | + class Expr { |
| 27 | + string toString(); |
| 28 | + Location getLocation(); |
| 29 | + } |
| 30 | + |
| 31 | + predicate interestingExprBound(Expr e); |
| 32 | +} |
| 33 | + |
| 34 | +overlay[local?] |
| 35 | +module Bound<LocationSig Location, BoundDefinitions<Location> Defs> { |
| 36 | + private import Defs |
| 37 | + |
| 38 | + private newtype TBound = |
| 39 | + TBoundZero() or |
| 40 | + TBoundSsa(SsaVariable v) { v.getSourceVariable().getType() instanceof IntegralType } or |
| 41 | + TBoundExpr(Expr e) { |
| 42 | + interestingExprBound(e) and |
| 43 | + not exists(SsaVariable v | e = v.getAUse()) |
| 44 | + } |
| 45 | + |
| 46 | + /** |
| 47 | + * A bound that may be inferred for an expression plus/minus an integer delta. |
| 48 | + */ |
| 49 | + abstract class Bound extends TBound { |
| 50 | + /** Gets a textual representation of this bound. */ |
| 51 | + abstract string toString(); |
| 52 | + |
| 53 | + /** Gets an expression that equals this bound plus `delta`. */ |
| 54 | + abstract Expr getExpr(int delta); |
| 55 | + |
| 56 | + /** Gets an expression that equals this bound. */ |
| 57 | + Expr getExpr() { result = this.getExpr(0) } |
| 58 | + |
| 59 | + /** Gets the location of this bound. */ |
| 60 | + abstract Location getLocation(); |
| 61 | + } |
| 62 | + |
| 63 | + /** |
| 64 | + * The bound that corresponds to the integer 0. This is used to represent all |
| 65 | + * integer bounds as bounds are always accompanied by an added integer delta. |
| 66 | + */ |
| 67 | + class ZeroBound extends Bound, TBoundZero { |
| 68 | + override string toString() { result = "0" } |
| 69 | + |
| 70 | + override Expr getExpr(int delta) { result.(ConstantIntegerExpr).getIntValue() = delta } |
| 71 | + |
| 72 | + override Location getLocation() { result.hasLocationInfo("", 0, 0, 0, 0) } |
| 73 | + } |
| 74 | + |
| 75 | + /** |
| 76 | + * A bound corresponding to the value of an SSA variable. |
| 77 | + */ |
| 78 | + class SsaBound extends Bound, TBoundSsa { |
| 79 | + /** Gets the SSA variable that equals this bound. */ |
| 80 | + SsaVariable getSsa() { this = TBoundSsa(result) } |
| 81 | + |
| 82 | + override string toString() { result = this.getSsa().toString() } |
| 83 | + |
| 84 | + override Expr getExpr(int delta) { result = this.getSsa().getAUse() and delta = 0 } |
| 85 | + |
| 86 | + override Location getLocation() { result = this.getSsa().getLocation() } |
| 87 | + } |
| 88 | + |
| 89 | + /** |
| 90 | + * A bound that corresponds to the value of a specific expression that might be |
| 91 | + * interesting, but isn't otherwise represented by the value of an SSA variable. |
| 92 | + */ |
| 93 | + class ExprBound extends Bound, TBoundExpr { |
| 94 | + override string toString() { result = this.getExpr().toString() } |
| 95 | + |
| 96 | + override Expr getExpr(int delta) { this = TBoundExpr(result) and delta = 0 } |
| 97 | + |
| 98 | + override Location getLocation() { result = this.getExpr().getLocation() } |
| 99 | + } |
| 100 | +} |
0 commit comments