Skip to content

Commit 5efd675

Browse files
committed
Sync Bound between C# and Java
1 parent 1ac0412 commit 5efd675

File tree

11 files changed

+234
-159
lines changed

11 files changed

+234
-159
lines changed

config/identical-files.json

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -62,6 +62,10 @@
6262
"java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisCommon.qll",
6363
"csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SignAnalysisCommon.qll"
6464
],
65+
"Bound Java/C#": [
66+
"java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/BoundCommon.qll",
67+
"csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/BoundCommon.qll"
68+
],
6569
"C++ SubBasicBlocks": [
6670
"cpp/ql/src/semmle/code/cpp/controlflow/SubBasicBlocks.qll",
6771
"cpp/ql/src/semmle/code/cpp/dataflow/internal/SubBasicBlocks.qll"
Lines changed: 2 additions & 55 deletions
Original file line numberDiff line numberDiff line change
@@ -1,58 +1,5 @@
1-
private import csharp
2-
private import Ssa
3-
private import semmle.code.csharp.dataflow.internal.rangeanalysis.ConstantUtils
4-
5-
private newtype TBound =
6-
TBoundZero() or
7-
TBoundSsa(Definition v) { v.getSourceVariable().getType() instanceof IntegralType }
8-
9-
/**
10-
* A bound that may be inferred for an expression plus/minus an integer delta.
11-
*/
12-
abstract class Bound extends TBound {
13-
/** Gets a textual representation of this bound. */
14-
abstract string toString();
15-
16-
/** Gets an expression that equals this bound plus `delta`. */
17-
abstract Expr getExpr(int delta);
18-
19-
/** Gets an expression that equals this bound. */
20-
Expr getExpr() { result = getExpr(0) }
21-
22-
/**
23-
* Holds if this element is at the specified location.
24-
* The location spans column `sc` of line `sl` to
25-
* column `ec` of line `el` in file `path`.
26-
* For more information, see
27-
* [Locations](https://help.semmle.com/QL/learn-ql/ql/locations.html).
28-
*/
29-
predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
30-
path = "" and sl = 0 and sc = 0 and el = 0 and ec = 0
31-
}
32-
}
33-
341
/**
35-
* The bound that corresponds to the integer 0. This is used to represent all
36-
* integer bounds as bounds are always accompanied by an added integer delta.
2+
* Provides classes for representing abstract bounds for use in, for example, range analysis.
373
*/
38-
class ZeroBound extends Bound, TBoundZero {
39-
override string toString() { result = "0" }
40-
41-
override Expr getExpr(int delta) { result.(ConstantIntegerExpr).getIntValue() = delta }
42-
}
43-
44-
/**
45-
* A bound corresponding to the value of an SSA variable.
46-
*/
47-
class DefinitionBound extends Bound, TBoundSsa {
48-
/** Gets the SSA variable that equals this bound. */
49-
Definition getDefinition() { this = TBoundSsa(result) }
50-
51-
override string toString() { result = getDefinition().toString() }
52-
53-
override Expr getExpr(int delta) { result = getDefinition().getARead() and delta = 0 }
544

55-
override predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
56-
getDefinition().getLocation().hasLocationInfo(path, sl, sc, el, ec)
57-
}
58-
}
5+
import semmle.code.csharp.dataflow.internal.rangeanalysis.BoundCommon

csharp/ql/src/semmle/code/csharp/dataflow/RangeAnalysis.qll

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -567,7 +567,7 @@ private predicate boundedPhiInp(
567567
or
568568
boundedPhi(inp, b, d, upper, fromBackEdge0, origdelta)
569569
or
570-
b.(DefinitionBound).getDefinition() = inp and
570+
b.(SsaBound).getSsa() = inp and
571571
d = 0 and
572572
(upper = true or upper = false) and
573573
fromBackEdge0 = false and
@@ -651,8 +651,8 @@ private predicate bbSucc(BasicBlock pre, BasicBlock post) { post = pre.getASucce
651651
private predicate selfBoundedPhiInp(
652652
PhiNode phi, Definition inp, SsaReadPositionPhiInputEdge edge, boolean upper
653653
) {
654-
exists(int d, DefinitionBound phibound |
655-
phibound.getDefinition() = phi and
654+
exists(int d, SsaBound phibound |
655+
phibound.getSsa() = phi and
656656
boundedPhiInp(phi, inp, edge, phibound, d, upper, _, _) and
657657
(
658658
upper = true and d <= 0
Lines changed: 75 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,75 @@
1+
/**
2+
* Provides classes for representing abstract bounds for use in, for example, range analysis.
3+
*/
4+
5+
private import BoundSpecific
6+
7+
private newtype TBound =
8+
TBoundZero() or
9+
TBoundSsa(SsaVariable v) { v.getSourceVariable().getType() instanceof IntegralType } or
10+
TBoundExpr(Expr e) { nonSsaVariableBoundedExpr(e) }
11+
12+
/**
13+
* A bound that may be inferred for an expression plus/minus an integer delta.
14+
*/
15+
abstract class Bound extends TBound {
16+
/** Gets a textual representation of this bound. */
17+
abstract string toString();
18+
19+
/** Gets an expression that equals this bound plus `delta`. */
20+
abstract Expr getExpr(int delta);
21+
22+
/** Gets an expression that equals this bound. */
23+
Expr getExpr() { result = getExpr(0) }
24+
25+
/**
26+
* Holds if this element is at the specified location.
27+
* The location spans column `sc` of line `sl` to
28+
* column `ec` of line `el` in file `path`.
29+
* For more information, see
30+
* [Locations](https://help.semmle.com/QL/learn-ql/ql/locations.html).
31+
*/
32+
predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
33+
path = "" and sl = 0 and sc = 0 and el = 0 and ec = 0
34+
}
35+
}
36+
37+
/**
38+
* The bound that corresponds to the integer 0. This is used to represent all
39+
* integer bounds as bounds are always accompanied by an added integer delta.
40+
*/
41+
class ZeroBound extends Bound, TBoundZero {
42+
override string toString() { result = "0" }
43+
44+
override Expr getExpr(int delta) { result.(ConstantIntegerExpr).getIntValue() = delta }
45+
}
46+
47+
/**
48+
* A bound corresponding to the value of an SSA variable.
49+
*/
50+
class SsaBound extends Bound, TBoundSsa {
51+
/** Gets the SSA variable that equals this bound. */
52+
SsaVariable getSsa() { this = TBoundSsa(result) }
53+
54+
override string toString() { result = getSsa().toString() }
55+
56+
override Expr getExpr(int delta) { result = getSsa().getAUse() and delta = 0 }
57+
58+
override predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
59+
getSsa().getLocation().hasLocationInfo(path, sl, sc, el, ec)
60+
}
61+
}
62+
63+
/**
64+
* A bound that corresponds to the value of a specific expression that might be
65+
* interesting, but isn't otherwise represented by the value of an SSA variable.
66+
*/
67+
class ExprBound extends Bound, TBoundExpr {
68+
override string toString() { result = getExpr().toString() }
69+
70+
override Expr getExpr(int delta) { this = TBoundExpr(result) and delta = 0 }
71+
72+
override predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
73+
getExpr().getLocation().hasLocationInfo(path, sl, sc, el, ec)
74+
}
75+
}
Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
/**
2+
* Provides C#-specific definitions for bounds.
3+
*/
4+
5+
private import csharp as CS
6+
private import semmle.code.csharp.dataflow.SSA::Ssa as Ssa
7+
private import semmle.code.csharp.dataflow.internal.rangeanalysis.ConstantUtils as CU
8+
9+
class SsaVariable extends Ssa::Definition {
10+
/** Gets a read of the source variable underlying this SSA definition. */
11+
Expr getAUse() { result = getARead() }
12+
}
13+
14+
class Expr = CS::Expr;
15+
16+
class IntegralType = CS::IntegralType;
17+
18+
class ConstantIntegerExpr = CU::ConstantIntegerExpr;
19+
20+
/** Holds if `e` is a bound expression and it is not an SSA variable read. */
21+
predicate nonSsaVariableBoundedExpr(Expr e) { CU::systemArrayLengthAccess(e.(CS::PropertyRead)) }

csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/ConstantUtils.qll

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,13 @@ predicate propertyOverrides(Property p, string baseClass, string property) {
1717
)
1818
}
1919

20+
/**
21+
* Holds if `pa` is an access to the `Length` property of an array.
22+
*/
23+
predicate systemArrayLengthAccess(PropertyAccess pa) {
24+
propertyOverrides(pa.getTarget(), "System.Array", "Length")
25+
}
26+
2027
/**
2128
* Holds if expression `e` is either
2229
* - a compile time constant with integer value `val`, or
@@ -47,7 +54,7 @@ private int getArrayLengthRec(ArrayCreation arrCreation, int index) {
4754
}
4855

4956
private predicate isArrayLengthAccess(PropertyAccess pa, int length) {
50-
propertyOverrides(pa.getTarget(), "System.Array", "Length") and
57+
systemArrayLengthAccess(pa) and
5158
exists(ExplicitDefinition arr, ArrayCreation arrCreation |
5259
getArrayLengthRec(arrCreation, arrCreation.getNumberOfLengthArguments() - 1) = length and
5360
arrCreation = arr.getADefinition().getSource() and

csharp/ql/test/library-tests/dataflow/rangeanalysis/RangeAnalysis.expected

Lines changed: 21 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -1,41 +1,41 @@
1-
| RangeAnalysis.cs:7:9:7:9 | access to parameter x | DefinitionBound | 0 | lower |
2-
| RangeAnalysis.cs:7:9:7:9 | access to parameter x | DefinitionBound | 0 | upper |
1+
| RangeAnalysis.cs:7:9:7:9 | access to parameter x | SsaBound | 0 | lower |
2+
| RangeAnalysis.cs:7:9:7:9 | access to parameter x | SsaBound | 0 | upper |
33
| RangeAnalysis.cs:7:13:7:15 | 500 | ZeroBound | 500 | lower |
44
| RangeAnalysis.cs:7:13:7:15 | 500 | ZeroBound | 500 | upper |
5-
| RangeAnalysis.cs:9:11:9:11 | access to parameter x | DefinitionBound | 0 | lower |
6-
| RangeAnalysis.cs:9:11:9:11 | access to parameter x | DefinitionBound | 0 | upper |
5+
| RangeAnalysis.cs:9:11:9:11 | access to parameter x | SsaBound | 0 | lower |
6+
| RangeAnalysis.cs:9:11:9:11 | access to parameter x | SsaBound | 0 | upper |
77
| RangeAnalysis.cs:9:11:9:11 | access to parameter x | ZeroBound | 499 | upper |
88
| RangeAnalysis.cs:9:15:9:17 | 400 | ZeroBound | 400 | lower |
99
| RangeAnalysis.cs:9:15:9:17 | 400 | ZeroBound | 400 | upper |
10-
| RangeAnalysis.cs:11:16:11:16 | access to parameter x | DefinitionBound | 0 | lower |
11-
| RangeAnalysis.cs:11:16:11:16 | access to parameter x | DefinitionBound | 0 | upper |
10+
| RangeAnalysis.cs:11:16:11:16 | access to parameter x | SsaBound | 0 | lower |
11+
| RangeAnalysis.cs:11:16:11:16 | access to parameter x | SsaBound | 0 | upper |
1212
| RangeAnalysis.cs:11:16:11:16 | access to parameter x | ZeroBound | 401 | lower |
1313
| RangeAnalysis.cs:11:16:11:16 | access to parameter x | ZeroBound | 499 | upper |
14-
| RangeAnalysis.cs:14:11:14:11 | access to parameter y | DefinitionBound | 0 | lower |
15-
| RangeAnalysis.cs:14:11:14:11 | access to parameter y | DefinitionBound | 0 | upper |
16-
| RangeAnalysis.cs:14:16:14:16 | access to parameter x | DefinitionBound | 0 | lower |
17-
| RangeAnalysis.cs:14:16:14:16 | access to parameter x | DefinitionBound | 0 | upper |
14+
| RangeAnalysis.cs:14:11:14:11 | access to parameter y | SsaBound | 0 | lower |
15+
| RangeAnalysis.cs:14:11:14:11 | access to parameter y | SsaBound | 0 | upper |
16+
| RangeAnalysis.cs:14:16:14:16 | access to parameter x | SsaBound | 0 | lower |
17+
| RangeAnalysis.cs:14:16:14:16 | access to parameter x | SsaBound | 0 | upper |
1818
| RangeAnalysis.cs:14:16:14:16 | access to parameter x | ZeroBound | 400 | upper |
19-
| RangeAnalysis.cs:14:21:14:21 | access to parameter y | DefinitionBound | 0 | lower |
20-
| RangeAnalysis.cs:14:21:14:21 | access to parameter y | DefinitionBound | 0 | upper |
19+
| RangeAnalysis.cs:14:21:14:21 | access to parameter y | SsaBound | 0 | lower |
20+
| RangeAnalysis.cs:14:21:14:21 | access to parameter y | SsaBound | 0 | upper |
2121
| RangeAnalysis.cs:14:21:14:21 | access to parameter y | ZeroBound | 400 | upper |
2222
| RangeAnalysis.cs:14:25:14:27 | 300 | ZeroBound | 300 | lower |
2323
| RangeAnalysis.cs:14:25:14:27 | 300 | ZeroBound | 300 | upper |
24-
| RangeAnalysis.cs:16:16:16:16 | access to parameter x | DefinitionBound | 0 | lower |
25-
| RangeAnalysis.cs:16:16:16:16 | access to parameter x | DefinitionBound | 0 | upper |
24+
| RangeAnalysis.cs:16:16:16:16 | access to parameter x | SsaBound | 0 | lower |
25+
| RangeAnalysis.cs:16:16:16:16 | access to parameter x | SsaBound | 0 | upper |
2626
| RangeAnalysis.cs:16:16:16:16 | access to parameter x | ZeroBound | 400 | upper |
27-
| RangeAnalysis.cs:16:16:16:20 | ... + ... | DefinitionBound | 1 | lower |
28-
| RangeAnalysis.cs:16:20:16:20 | access to parameter y | DefinitionBound | 0 | lower |
29-
| RangeAnalysis.cs:16:20:16:20 | access to parameter y | DefinitionBound | 0 | upper |
27+
| RangeAnalysis.cs:16:16:16:20 | ... + ... | SsaBound | 1 | lower |
28+
| RangeAnalysis.cs:16:20:16:20 | access to parameter y | SsaBound | 0 | lower |
29+
| RangeAnalysis.cs:16:20:16:20 | access to parameter y | SsaBound | 0 | upper |
3030
| RangeAnalysis.cs:16:20:16:20 | access to parameter y | ZeroBound | 301 | lower |
3131
| RangeAnalysis.cs:16:20:16:20 | access to parameter y | ZeroBound | 400 | upper |
32-
| RangeAnalysis.cs:19:11:19:11 | access to parameter x | DefinitionBound | 0 | lower |
33-
| RangeAnalysis.cs:19:11:19:11 | access to parameter x | DefinitionBound | 0 | upper |
32+
| RangeAnalysis.cs:19:11:19:11 | access to parameter x | SsaBound | 0 | lower |
33+
| RangeAnalysis.cs:19:11:19:11 | access to parameter x | SsaBound | 0 | upper |
3434
| RangeAnalysis.cs:19:11:19:11 | access to parameter x | ZeroBound | 400 | upper |
3535
| RangeAnalysis.cs:19:15:19:17 | 500 | ZeroBound | 500 | lower |
3636
| RangeAnalysis.cs:19:15:19:17 | 500 | ZeroBound | 500 | upper |
37-
| RangeAnalysis.cs:21:16:21:16 | access to parameter x | DefinitionBound | 0 | lower |
38-
| RangeAnalysis.cs:21:16:21:16 | access to parameter x | DefinitionBound | 0 | upper |
37+
| RangeAnalysis.cs:21:16:21:16 | access to parameter x | SsaBound | 0 | lower |
38+
| RangeAnalysis.cs:21:16:21:16 | access to parameter x | SsaBound | 0 | upper |
3939
| RangeAnalysis.cs:21:16:21:16 | access to parameter x | ZeroBound | 400 | upper |
4040
| RangeAnalysis.cs:21:16:21:16 | access to parameter x | ZeroBound | 501 | lower |
4141
| RangeAnalysis.cs:25:12:25:12 | 0 | ZeroBound | 0 | lower |

java/ql/src/semmle/code/java/dataflow/Bound.qll

Lines changed: 1 addition & 76 deletions
Original file line numberDiff line numberDiff line change
@@ -2,79 +2,4 @@
22
* Provides classes for representing abstract bounds for use in, for example, range analysis.
33
*/
44

5-
import java
6-
private import SSA
7-
private import RangeUtils
8-
9-
private newtype TBound =
10-
TBoundZero() or
11-
TBoundSsa(SsaVariable v) { v.getSourceVariable().getType() instanceof IntegralType } or
12-
TBoundExpr(Expr e) {
13-
e.(FieldRead).getField() instanceof ArrayLengthField and
14-
not exists(SsaVariable v | e = v.getAUse())
15-
}
16-
17-
/**
18-
* A bound that may be inferred for an expression plus/minus an integer delta.
19-
*/
20-
abstract class Bound extends TBound {
21-
/** Gets a textual representation of this bound. */
22-
abstract string toString();
23-
24-
/** Gets an expression that equals this bound plus `delta`. */
25-
abstract Expr getExpr(int delta);
26-
27-
/** Gets an expression that equals this bound. */
28-
Expr getExpr() { result = getExpr(0) }
29-
30-
/**
31-
* Holds if this element is at the specified location.
32-
* The location spans column `sc` of line `sl` to
33-
* column `ec` of line `el` in file `path`.
34-
* For more information, see
35-
* [Locations](https://help.semmle.com/QL/learn-ql/ql/locations.html).
36-
*/
37-
predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
38-
path = "" and sl = 0 and sc = 0 and el = 0 and ec = 0
39-
}
40-
}
41-
42-
/**
43-
* The bound that corresponds to the integer 0. This is used to represent all
44-
* integer bounds as bounds are always accompanied by an added integer delta.
45-
*/
46-
class ZeroBound extends Bound, TBoundZero {
47-
override string toString() { result = "0" }
48-
49-
override Expr getExpr(int delta) { result.(ConstantIntegerExpr).getIntValue() = delta }
50-
}
51-
52-
/**
53-
* A bound corresponding to the value of an SSA variable.
54-
*/
55-
class SsaBound extends Bound, TBoundSsa {
56-
/** Gets the SSA variable that equals this bound. */
57-
SsaVariable getSsa() { this = TBoundSsa(result) }
58-
59-
override string toString() { result = getSsa().toString() }
60-
61-
override Expr getExpr(int delta) { result = getSsa().getAUse() and delta = 0 }
62-
63-
override predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
64-
getSsa().getLocation().hasLocationInfo(path, sl, sc, el, ec)
65-
}
66-
}
67-
68-
/**
69-
* A bound that corresponds to the value of a specific expression that might be
70-
* interesting, but isn't otherwise represented by the value of an SSA variable.
71-
*/
72-
class ExprBound extends Bound, TBoundExpr {
73-
override string toString() { result = getExpr().toString() }
74-
75-
override Expr getExpr(int delta) { this = TBoundExpr(result) and delta = 0 }
76-
77-
override predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
78-
getExpr().hasLocationInfo(path, sl, sc, el, ec)
79-
}
80-
}
5+
import semmle.code.java.dataflow.internal.rangeanalysis.BoundCommon

java/ql/src/semmle/code/java/dataflow/ModulusAnalysis.qll

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -68,11 +68,11 @@ private Expr modExpr(Expr arg, int mod) {
6868
exists(RemExpr rem |
6969
result = rem and
7070
arg = rem.getLeftOperand() and
71-
rem.getRightOperand().(CompileTimeConstantExpr).getIntValue() = mod and
71+
rem.getRightOperand().(ConstantIntegerExpr).getIntValue() = mod and
7272
mod >= 2
7373
)
7474
or
75-
exists(CompileTimeConstantExpr c |
75+
exists(ConstantIntegerExpr c |
7676
mod = 2.pow([1 .. 30]) and
7777
c.getIntValue() = mod - 1 and
7878
result.(AndBitwiseExpr).hasOperands(arg, c)
@@ -84,7 +84,7 @@ private Expr modExpr(Expr arg, int mod) {
8484
* its `testIsTrue` branch.
8585
*/
8686
private Guard moduloCheck(SsaVariable v, int val, int mod, boolean testIsTrue) {
87-
exists(Expr rem, CompileTimeConstantExpr c, int r, boolean polarity |
87+
exists(Expr rem, ConstantIntegerExpr c, int r, boolean polarity |
8888
result.isEquality(rem, c, polarity) and
8989
c.getIntValue() = r and
9090
rem = modExpr(v.getAUse(), mod) and

0 commit comments

Comments
 (0)