55private import codeql.util.Location
66
77signature module BoundDefinitions< LocationSig Location> {
8- class Type ;
9- class IntegralType extends Type ;
8+ class Type ;
109
11- class ConstantIntegerExpr extends Expr {
12- int getIntValue ( ) ;
13- }
10+ class IntegralType extends Type ;
1411
15- class SsaSourceVariable {
16- Type getType ( ) ;
17- }
12+ class ConstantIntegerExpr extends Expr {
13+ int getIntValue ( ) ;
14+ }
1815
19- class SsaVariable {
20- SsaSourceVariable getSourceVariable ( ) ;
21- string toString ( ) ;
22- Location getLocation ( ) ;
23- Expr getAUse ( ) ;
24- }
16+ class SsaSourceVariable {
17+ Type getType ( ) ;
18+ }
2519
26- class Expr {
27- string toString ( ) ;
28- Location getLocation ( ) ;
29- }
20+ class SsaVariable {
21+ SsaSourceVariable getSourceVariable ( ) ;
22+
23+ string toString ( ) ;
24+
25+ Location getLocation ( ) ;
26+
27+ Expr getAUse ( ) ;
28+ }
3029
31- predicate interestingExprBound ( Expr e ) ;
30+ class Expr {
31+ string toString ( ) ;
32+
33+ Location getLocation ( ) ;
34+ }
35+
36+ predicate interestingExprBound ( Expr e ) ;
3237}
3338
3439overlay [ local?]
3540module Bound< LocationSig Location, BoundDefinitions< Location > Defs> {
36- private import Defs
41+ private import Defs
3742
38- private newtype TBound =
43+ private newtype TBound =
3944 TBoundZero ( ) or
4045 TBoundSsa ( SsaVariable v ) { v .getSourceVariable ( ) .getType ( ) instanceof IntegralType } or
4146 TBoundExpr ( Expr e ) {
42- interestingExprBound ( e ) and
43- not exists ( SsaVariable v | e = v .getAUse ( ) )
47+ interestingExprBound ( e ) and
48+ not exists ( SsaVariable v | e = v .getAUse ( ) )
4449 }
4550
46- /**
47- * A bound that may be inferred for an expression plus/minus an integer delta.
48- */
49- abstract class Bound extends TBound {
51+ /**
52+ * A bound that may be inferred for an expression plus/minus an integer delta.
53+ */
54+ abstract class Bound extends TBound {
5055 /** Gets a textual representation of this bound. */
5156 abstract string toString ( ) ;
5257
@@ -58,24 +63,24 @@ module Bound<LocationSig Location, BoundDefinitions<Location> Defs> {
5863
5964 /** Gets the location of this bound. */
6065 abstract Location getLocation ( ) ;
61- }
66+ }
6267
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+ /**
69+ * The bound that corresponds to the integer 0. This is used to represent all
70+ * integer bounds as bounds are always accompanied by an added integer delta.
71+ */
72+ class ZeroBound extends Bound , TBoundZero {
6873 override string toString ( ) { result = "0" }
6974
7075 override Expr getExpr ( int delta ) { result .( ConstantIntegerExpr ) .getIntValue ( ) = delta }
7176
7277 override Location getLocation ( ) { result .hasLocationInfo ( "" , 0 , 0 , 0 , 0 ) }
73- }
78+ }
7479
75- /**
76- * A bound corresponding to the value of an SSA variable.
77- */
78- class SsaBound extends Bound , TBoundSsa {
80+ /**
81+ * A bound corresponding to the value of an SSA variable.
82+ */
83+ class SsaBound extends Bound , TBoundSsa {
7984 /** Gets the SSA variable that equals this bound. */
8085 SsaVariable getSsa ( ) { this = TBoundSsa ( result ) }
8186
@@ -84,17 +89,17 @@ module Bound<LocationSig Location, BoundDefinitions<Location> Defs> {
8489 override Expr getExpr ( int delta ) { result = this .getSsa ( ) .getAUse ( ) and delta = 0 }
8590
8691 override Location getLocation ( ) { result = this .getSsa ( ) .getLocation ( ) }
87- }
92+ }
8893
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+ /**
95+ * A bound that corresponds to the value of a specific expression that might be
96+ * interesting, but isn't otherwise represented by the value of an SSA variable.
97+ */
98+ class ExprBound extends Bound , TBoundExpr {
9499 override string toString ( ) { result = this .getExpr ( ) .toString ( ) }
95100
96101 override Expr getExpr ( int delta ) { this = TBoundExpr ( result ) and delta = 0 }
97102
98103 override Location getLocation ( ) { result = this .getExpr ( ) .getLocation ( ) }
99- }
104+ }
100105}
0 commit comments