Skip to content

Commit b0f8037

Browse files
MathiasVPMathiasVP
authored
Merge pull request #11928 from rdmarsh2/rdmarsh2/stageify-range-analysis
2 parents dce81cf + 1e8404c commit b0f8037

7 files changed

Lines changed: 171 additions & 26 deletions

File tree

‎cpp/ql/lib/experimental/semmle/code/cpp/semantic/SemanticBound.qll‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@
55
private import SemanticExpr
66
private import SemanticExprSpecific::SemanticExprConfig as Specific
77
private import SemanticSSA
8+
private import SemanticLocation
89

910
/**
1011
* A valid base for an expression bound.
@@ -14,6 +15,8 @@ private import SemanticSSA
1415
class SemBound instanceof Specific::Bound {
1516
final string toString() { result = super.toString() }
1617

18+
final SemLocation getLocation() { result = super.getLocation() }
19+
1720
final SemExpr getExpr(int delta) { result = Specific::getBoundExpr(this, delta) }
1821
}
1922

‎cpp/ql/lib/experimental/semmle/code/cpp/semantic/SemanticLocation.qll‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
private import semmle.code.cpp.Location
2+
3+
class SemLocation instanceof Location {
4+
/**
5+
* Gets a textual representation of this element.
6+
*
7+
* The format is "file://filePath:startLine:startColumn:endLine:endColumn".
8+
*/
9+
string toString() { result = super.toString() }
10+
11+
/**
12+
* Holds if this element is at the specified location.
13+
* The location spans column `startcolumn` of line `startline` to
14+
* column `endcolumn` of line `endline` in file `filepath`.
15+
* For more information, see
16+
* [Locations](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/).
17+
*/
18+
predicate hasLocationInfo(
19+
string filepath, int startline, int startcolumn, int endline, int endcolumn
20+
) {
21+
super.hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
22+
}
23+
}

‎cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/IntDelta.qll‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
private import RangeAnalysisStage
2+
3+
module IntDelta implements DeltaSig {
4+
class Delta = int;
5+
6+
bindingset[d]
7+
bindingset[result]
8+
float toFloat(Delta d) { result = d }
9+
10+
bindingset[d]
11+
bindingset[result]
12+
int toInt(Delta d) { result = d }
13+
14+
bindingset[n]
15+
bindingset[result]
16+
Delta fromInt(int n) { result = n }
17+
18+
bindingset[f]
19+
Delta fromFloat(float f) {
20+
result =
21+
min(float diff, float res |
22+
diff = (res - f) and res = f.ceil()
23+
or
24+
diff = (f - res) and res = f.floor()
25+
|
26+
res order by diff
27+
)
28+
}
29+
}

‎cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysis.qll‎

Lines changed: 2 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -1,24 +1,2 @@
1-
private import RangeAnalysisStage
2-
private import RangeAnalysisSpecific
3-
private import experimental.semmle.code.cpp.semantic.analysis.FloatDelta
4-
private import RangeUtils
5-
private import experimental.semmle.code.cpp.semantic.SemanticBound as SemanticBound
6-
7-
module Bounds implements BoundSig<FloatDelta> {
8-
class SemBound instanceof SemanticBound::SemBound {
9-
string toString() { result = super.toString() }
10-
11-
SemExpr getExpr(float delta) { result = super.getExpr(delta) }
12-
}
13-
14-
class SemZeroBound extends SemBound instanceof SemanticBound::SemZeroBound { }
15-
16-
class SemSsaBound extends SemBound instanceof SemanticBound::SemSsaBound {
17-
SemSsaVariable getAVariable() { result = this.(SemanticBound::SemSsaBound).getAVariable() }
18-
}
19-
}
20-
21-
private module CppRangeAnalysis =
22-
RangeStage<FloatDelta, Bounds, CppLangImpl, RangeUtil<FloatDelta, CppLangImpl>>;
23-
24-
import CppRangeAnalysis
1+
import RangeAnalysisImpl
2+
import experimental.semmle.code.cpp.semantic.SemanticBound

‎cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysisImpl.qll‎

Lines changed: 107 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,107 @@
1+
private import RangeAnalysisStage
2+
private import RangeAnalysisSpecific
3+
private import experimental.semmle.code.cpp.semantic.analysis.FloatDelta
4+
private import RangeUtils
5+
private import experimental.semmle.code.cpp.semantic.SemanticBound as SemanticBound
6+
private import experimental.semmle.code.cpp.semantic.SemanticLocation
7+
private import experimental.semmle.code.cpp.semantic.SemanticSSA
8+
9+
module ConstantBounds implements BoundSig<FloatDelta> {
10+
class SemBound instanceof SemanticBound::SemBound {
11+
SemBound() {
12+
this instanceof SemanticBound::SemZeroBound
13+
or
14+
this.(SemanticBound::SemSsaBound).getAVariable() instanceof SemSsaPhiNode
15+
}
16+
17+
string toString() { result = super.toString() }
18+
19+
SemLocation getLocation() { result = super.getLocation() }
20+
21+
SemExpr getExpr(float delta) { result = super.getExpr(delta) }
22+
}
23+
24+
class SemZeroBound extends SemBound instanceof SemanticBound::SemZeroBound { }
25+
26+
class SemSsaBound extends SemBound instanceof SemanticBound::SemSsaBound {
27+
SemSsaVariable getAVariable() { result = this.(SemanticBound::SemSsaBound).getAVariable() }
28+
}
29+
}
30+
31+
private module RelativeBounds implements BoundSig<FloatDelta> {
32+
class SemBound instanceof SemanticBound::SemBound {
33+
SemBound() { not this instanceof SemanticBound::SemZeroBound }
34+
35+
string toString() { result = super.toString() }
36+
37+
SemLocation getLocation() { result = super.getLocation() }
38+
39+
SemExpr getExpr(float delta) { result = super.getExpr(delta) }
40+
}
41+
42+
class SemZeroBound extends SemBound instanceof SemanticBound::SemZeroBound { }
43+
44+
class SemSsaBound extends SemBound instanceof SemanticBound::SemSsaBound {
45+
SemSsaVariable getAVariable() { result = this.(SemanticBound::SemSsaBound).getAVariable() }
46+
}
47+
}
48+
49+
private module ConstantStage =
50+
RangeStage<FloatDelta, ConstantBounds, CppLangImpl, RangeUtil<FloatDelta, CppLangImpl>>;
51+
52+
private module RelativeStage =
53+
RangeStage<FloatDelta, RelativeBounds, CppLangImpl, RangeUtil<FloatDelta, CppLangImpl>>;
54+
55+
private newtype TSemReason =
56+
TSemNoReason() or
57+
TSemCondReason(SemGuard guard) {
58+
guard = any(ConstantStage::SemCondReason reason).getCond()
59+
or
60+
guard = any(RelativeStage::SemCondReason reason).getCond()
61+
}
62+
63+
/**
64+
* A reason for an inferred bound. This can either be `CondReason` if the bound
65+
* is due to a specific condition, or `NoReason` if the bound is inferred
66+
* without going through a bounding condition.
67+
*/
68+
abstract class SemReason extends TSemReason {
69+
/** Gets a textual representation of this reason. */
70+
abstract string toString();
71+
}
72+
73+
/**
74+
* A reason for an inferred bound that indicates that the bound is inferred
75+
* without going through a bounding condition.
76+
*/
77+
class SemNoReason extends SemReason, TSemNoReason {
78+
override string toString() { result = "NoReason" }
79+
}
80+
81+
/** A reason for an inferred bound pointing to a condition. */
82+
class SemCondReason extends SemReason, TSemCondReason {
83+
/** Gets the condition that is the reason for the bound. */
84+
SemGuard getCond() { this = TSemCondReason(result) }
85+
86+
override string toString() { result = getCond().toString() }
87+
}
88+
89+
private ConstantStage::SemReason constantReason(SemReason reason) {
90+
result instanceof ConstantStage::SemNoReason and reason instanceof SemNoReason
91+
or
92+
result.(ConstantStage::SemCondReason).getCond() = reason.(SemCondReason).getCond()
93+
}
94+
95+
private RelativeStage::SemReason relativeReason(SemReason reason) {
96+
result instanceof RelativeStage::SemNoReason and reason instanceof SemNoReason
97+
or
98+
result.(RelativeStage::SemCondReason).getCond() = reason.(SemCondReason).getCond()
99+
}
100+
101+
predicate semBounded(
102+
SemExpr e, SemanticBound::SemBound b, float delta, boolean upper, SemReason reason
103+
) {
104+
ConstantStage::semBounded(e, b, delta, upper, constantReason(reason))
105+
or
106+
RelativeStage::semBounded(e, b, delta, upper, relativeReason(reason))
107+
}

‎cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysisStage.qll‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -73,6 +73,7 @@ import experimental.semmle.code.cpp.semantic.SemanticCFG
7373
import experimental.semmle.code.cpp.semantic.SemanticType
7474
import experimental.semmle.code.cpp.semantic.SemanticOpcode
7575
private import ConstantAnalysis
76+
import experimental.semmle.code.cpp.semantic.SemanticLocation
7677

7778
/**
7879
* Holds if `typ` is a small integral type with the given lower and upper bounds.
@@ -228,6 +229,10 @@ signature module UtilSig<DeltaSig DeltaParam> {
228229

229230
signature module BoundSig<DeltaSig D> {
230231
class SemBound {
232+
string toString();
233+
234+
SemLocation getLocation();
235+
231236
SemExpr getExpr(D::Delta delta);
232237
}
233238

‎cpp/ql/test/library-tests/ir/modulus-analysis/ModulusAnalysis.ql‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,12 +4,12 @@ import experimental.semmle.code.cpp.semantic.Semantic
44
import experimental.semmle.code.cpp.semantic.analysis.RangeUtils
55
import experimental.semmle.code.cpp.semantic.analysis.FloatDelta
66
import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysisSpecific
7-
import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysis
7+
import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysisImpl
88
import semmle.code.cpp.ir.IR as IR
99
import TestUtilities.InlineExpectationsTest
1010

1111
module ModulusAnalysisInstantiated =
12-
ModulusAnalysis<FloatDelta, Bounds, RangeUtil<FloatDelta, CppLangImpl>>;
12+
ModulusAnalysis<FloatDelta, ConstantBounds, RangeUtil<FloatDelta, CppLangImpl>>;
1313

1414
class ModulusAnalysisTest extends InlineExpectationsTest {
1515
ModulusAnalysisTest() { this = "ModulusAnalysisTest" }

0 commit comments

Comments
 (0)