Skip to content

Commit 6b178fb

Browse files
committed
Rangeanalysis: Preparatory refactor for bounds sharing.
1 parent d8f53e5 commit 6b178fb

File tree

4 files changed

+25
-4
lines changed

4 files changed

+25
-4
lines changed

cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisConstantSpecific.qll

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,4 +25,8 @@ module CppLangImplConstant implements LangSig<Sem, FloatDelta> {
2525
* Holds if `e2 >= e1 + delta` (if `upper = false`) or `e2 <= e1 + delta` (if `upper = true`).
2626
*/
2727
predicate additionalBoundFlowStep(SemExpr e2, SemExpr e1, float delta, boolean upper) { none() }
28+
29+
predicate includeConstantBounds() { any() }
30+
31+
predicate includeRelativeBounds() { none() }
2832
}

cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -173,11 +173,11 @@ private module ModulusAnalysisInstantiated implements ModulusAnalysisSig<Sem> {
173173
}
174174

175175
module ConstantStage =
176-
RangeStage<SemLocation, Sem, FloatDelta, ConstantBounds, FloatOverflow, CppLangImplConstant,
176+
RangeStage<SemLocation, Sem, FloatDelta, AllBounds, FloatOverflow, CppLangImplConstant,
177177
SignAnalysis, ModulusAnalysisInstantiated>;
178178

179179
module RelativeStage =
180-
RangeStage<SemLocation, Sem, FloatDelta, RelativeBounds, FloatOverflow, CppLangImplRelative,
180+
RangeStage<SemLocation, Sem, FloatDelta, AllBounds, FloatOverflow, CppLangImplRelative,
181181
SignAnalysis, ModulusAnalysisInstantiated>;
182182

183183
private newtype TSemReason =

cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisRelativeSpecific.qll

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -57,4 +57,8 @@ module CppLangImplRelative implements LangSig<Sem, FloatDelta> {
5757
* Holds if `e2 >= e1 + delta` (if `upper = false`) or `e2 <= e1 + delta` (if `upper = true`).
5858
*/
5959
predicate additionalBoundFlowStep(SemExpr e2, SemExpr e1, float delta, boolean upper) { none() }
60+
61+
predicate includeConstantBounds() { none() }
62+
63+
predicate includeRelativeBounds() { any() }
6064
}

shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll

Lines changed: 15 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -289,6 +289,10 @@ signature module LangSig<Semantic Sem, DeltaSig D> {
289289
predicate ignoreExprBound(Sem::Expr e);
290290

291291
default predicate javaCompatibility() { none() }
292+
293+
default predicate includeConstantBounds() { any() }
294+
295+
default predicate includeRelativeBounds() { any() }
292296
}
293297

294298
signature module BoundSig<LocationSig Location, Semantic Sem, DeltaSig D> {
@@ -983,6 +987,13 @@ module RangeStage<
983987
)
984988
}
985989

990+
private predicate includeBound(SemBound b) {
991+
// always include phi bounds
992+
b.(SemSsaBound).getVariable() instanceof Sem::SsaPhiNode
993+
or
994+
if b instanceof SemZeroBound then includeConstantBounds() else includeRelativeBounds()
995+
}
996+
986997
/**
987998
* Holds if `e` has an upper (for `upper = true`) or lower
988999
* (for `upper = false`) bound of `b`.
@@ -1122,13 +1133,15 @@ module RangeStage<
11221133
(upper = true or upper = false) and
11231134
fromBackEdge = false and
11241135
origdelta = delta and
1125-
reason = TSemNoReason()
1136+
reason = TSemNoReason() and
1137+
includeBound(b)
11261138
or
11271139
baseBound(e, delta, upper) and
11281140
b instanceof SemZeroBound and
11291141
fromBackEdge = false and
11301142
origdelta = delta and
1131-
reason = TSemNoReason()
1143+
reason = TSemNoReason() and
1144+
includeBound(b)
11321145
or
11331146
exists(Sem::SsaVariable v, SsaReadPositionBlock bb |
11341147
boundedSsa(v, b, delta, bb, upper, fromBackEdge, origdelta, reason) and

0 commit comments

Comments
 (0)