@@ -10,7 +10,7 @@ private import RangeUtils
10
10
private import RangeAnalysis
11
11
12
12
/** Gets an expression that might have the value `i`. */
13
- private Expr exprWithIntValue ( int i ) {
13
+ deprecated private Expr exprWithIntValue ( int i ) {
14
14
result .( ConstantIntegerExpr ) .getIntValue ( ) = i or
15
15
result .( ChooseExpr ) .getAResultExpr ( ) = exprWithIntValue ( i )
16
16
}
@@ -19,11 +19,11 @@ private Expr exprWithIntValue(int i) {
19
19
* An expression for which the predicate `integerGuard` is relevant.
20
20
* This includes `VarRead` and `MethodCall`.
21
21
*/
22
- class IntComparableExpr extends Expr {
22
+ deprecated class IntComparableExpr extends Expr {
23
23
IntComparableExpr ( ) { this instanceof VarRead or this instanceof MethodCall }
24
24
25
25
/** Gets an integer that is directly assigned to the expression in case of a variable; or zero. */
26
- int relevantInt ( ) {
26
+ deprecated int relevantInt ( ) {
27
27
exists ( SsaExplicitUpdate ssa , SsaSourceVariable v |
28
28
this = v .getAnAccess ( ) and
29
29
ssa .getSourceVariable ( ) = v and
@@ -55,14 +55,18 @@ private predicate comparison(ComparisonExpr comp, boolean branch, Expr e1, Expr
55
55
* Holds if `guard` evaluating to `branch` ensures that:
56
56
* `e <= k` when `upper = true`
57
57
* `e >= k` when `upper = false`
58
+ *
59
+ * Does _not_ include the constant comparison case where the guard directly
60
+ * ensures `e == k`.
58
61
*/
59
62
pragma [ nomagic]
60
63
predicate rangeGuard ( Expr guard , boolean branch , Expr e , int k , boolean upper ) {
61
64
exists ( EqualityTest eqtest , Expr c |
62
65
eqtest = guard and
63
66
eqtest .hasOperands ( e , c ) and
64
67
bounded ( c , any ( ZeroBound zb ) , k , upper , _) and
65
- branch = eqtest .polarity ( )
68
+ branch = eqtest .polarity ( ) and
69
+ not c instanceof ConstantIntegerExpr
66
70
)
67
71
or
68
72
exists ( Expr c , int val , boolean strict , int d |
@@ -87,6 +91,30 @@ predicate rangeGuard(Expr guard, boolean branch, Expr e, int k, boolean upper) {
87
91
}
88
92
89
93
/**
94
+ * Gets an expression that directly tests whether a given expression, `e`, is
95
+ * non-zero.
96
+ */
97
+ Expr nonZeroGuard ( Expr e , boolean branch ) {
98
+ exists ( EqualityTest eqtest , boolean polarity , int k |
99
+ eqtest = result and
100
+ eqtest .hasOperands ( e , any ( ConstantIntegerExpr c | c .getIntValue ( ) = k ) ) and
101
+ polarity = eqtest .polarity ( )
102
+ |
103
+ k = 0 and branch = polarity .booleanNot ( )
104
+ or
105
+ k != 0 and branch = polarity
106
+ )
107
+ or
108
+ exists ( int val , boolean upper | rangeGuard ( result , branch , e , val , upper ) |
109
+ upper = true and val < 0 // e <= val < 0 ==> e != 0
110
+ or
111
+ upper = false and val > 0 // e >= val > 0 ==> e != 0
112
+ )
113
+ }
114
+
115
+ /**
116
+ * DEPRECATED.
117
+ *
90
118
* An expression that directly tests whether a given expression is equal to `k` or not.
91
119
* The set of `k`s is restricted to those that are relevant for the expression or
92
120
* have a direct comparison with the expression.
@@ -95,7 +123,7 @@ predicate rangeGuard(Expr guard, boolean branch, Expr e, int k, boolean upper) {
95
123
* is true, and different from `k` if `is_k` is false.
96
124
*/
97
125
pragma [ nomagic]
98
- Expr integerGuard ( IntComparableExpr e , boolean branch , int k , boolean is_k ) {
126
+ deprecated Expr integerGuard ( IntComparableExpr e , boolean branch , int k , boolean is_k ) {
99
127
exists ( EqualityTest eqtest , boolean polarity |
100
128
eqtest = result and
101
129
eqtest .hasOperands ( e , any ( ConstantIntegerExpr c | c .getIntValue ( ) = k ) ) and
@@ -119,13 +147,15 @@ Expr integerGuard(IntComparableExpr e, boolean branch, int k, boolean is_k) {
119
147
}
120
148
121
149
/**
150
+ * DEPRECATED: Use `rangeGuard` instead.
151
+ *
122
152
* A guard that splits the values of a variable into one range with an upper bound of `k-1`
123
153
* and one with a lower bound of `k`.
124
154
*
125
155
* If `branch_with_lower_bound_k` is true then `result` is equivalent to `k <= x`
126
156
* and if it is false then `result` is equivalent to `k > x`.
127
157
*/
128
- Expr intBoundGuard ( VarRead x , boolean branch_with_lower_bound_k , int k ) {
158
+ deprecated Expr intBoundGuard ( VarRead x , boolean branch_with_lower_bound_k , int k ) {
129
159
exists ( ComparisonExpr comp , ConstantIntegerExpr c , int val |
130
160
comp = result and
131
161
comp .hasOperands ( x , c ) and
0 commit comments