Skip to content

Commit a39a94c

Browse files
committed
Rangeanalysis: Switch to shared ssaRead predicate.
1 parent 19644a8 commit a39a94c

File tree

4 files changed

+16
-17
lines changed

4 files changed

+16
-17
lines changed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ module RangeUtil<DeltaSig D, LangSig<Sem, D> Lang> implements UtilSig<Sem, D> {
1212
/**
1313
* Gets an expression that equals `v - d`.
1414
*/
15-
SemExpr semSsaRead(SemSsaVariable v, D::Delta delta) {
15+
private SemExpr semSsaRead(SemSsaVariable v, D::Delta delta) {
1616
// There are various language-specific extension points that can be removed once we no longer
1717
// expect to match the original Java implementation's results exactly.
1818
result = v.getAUse() and delta = D::fromInt(0)

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

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,8 @@ private import RangeUtils
1515
private import Sign
1616

1717
module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
18+
private import codeql.rangeanalysis.internal.RangeUtils::MakeUtils<Sem, D>
19+
1820
/**
1921
* An SSA definition for which the analysis can compute the sign.
2022
*
@@ -297,12 +299,12 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
297299
|
298300
testIsTrue = true and
299301
comp.getLesserOperand() = lowerbound and
300-
comp.getGreaterOperand() = Utils::semSsaRead(v, D::fromInt(0)) and
302+
comp.getGreaterOperand() = ssaRead(v, D::fromInt(0)) and
301303
(if comp.isStrict() then isStrict = true else isStrict = false)
302304
or
303305
testIsTrue = false and
304306
comp.getGreaterOperand() = lowerbound and
305-
comp.getLesserOperand() = Utils::semSsaRead(v, D::fromInt(0)) and
307+
comp.getLesserOperand() = ssaRead(v, D::fromInt(0)) and
306308
(if comp.isStrict() then isStrict = false else isStrict = true)
307309
)
308310
}
@@ -321,12 +323,12 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
321323
|
322324
testIsTrue = true and
323325
comp.getGreaterOperand() = upperbound and
324-
comp.getLesserOperand() = Utils::semSsaRead(v, D::fromInt(0)) and
326+
comp.getLesserOperand() = ssaRead(v, D::fromInt(0)) and
325327
(if comp.isStrict() then isStrict = true else isStrict = false)
326328
or
327329
testIsTrue = false and
328330
comp.getLesserOperand() = upperbound and
329-
comp.getGreaterOperand() = Utils::semSsaRead(v, D::fromInt(0)) and
331+
comp.getGreaterOperand() = ssaRead(v, D::fromInt(0)) and
330332
(if comp.isStrict() then isStrict = false else isStrict = true)
331333
)
332334
}
@@ -342,7 +344,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
342344
exists(SemGuard guard, boolean testIsTrue, boolean polarity, SemExpr e |
343345
pos.hasReadOfVar(pragma[only_bind_into](v)) and
344346
semGuardControlsSsaRead(guard, pragma[only_bind_into](pos), testIsTrue) and
345-
e = Utils::semSsaRead(pragma[only_bind_into](v), D::fromInt(0)) and
347+
e = ssaRead(pragma[only_bind_into](v), D::fromInt(0)) and
346348
guard.isEquality(eqbound, e, polarity) and
347349
isEq = polarity.booleanXor(testIsTrue).booleanNot() and
348350
not unknownSign(eqbound)

java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -396,8 +396,6 @@ module Utils implements UtilSig<Sem, IntDelta> {
396396
private import RangeUtils as RU
397397
private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon as SsaReadPos
398398

399-
Sem::Expr semSsaRead(Sem::SsaVariable v, int delta) { result = RU::ssaRead(v, delta) }
400-
401399
Sem::Guard semEqFlowCond(
402400
Sem::SsaVariable v, Sem::Expr e, int delta, boolean isEq, boolean testIsTrue
403401
) {

shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -337,8 +337,6 @@ signature module LangSig<Semantic Sem, DeltaSig D> {
337337
}
338338

339339
signature module UtilSig<Semantic Sem, DeltaSig DeltaParam> {
340-
Sem::Expr semSsaRead(Sem::SsaVariable v, DeltaParam::Delta delta);
341-
342340
Sem::Guard semEqFlowCond(
343341
Sem::SsaVariable v, Sem::Expr e, DeltaParam::Delta delta, boolean isEq, boolean testIsTrue
344342
);
@@ -409,6 +407,7 @@ module RangeStage<
409407
private import OverflowParam
410408
private import SignAnalysis
411409
private import ModulusAnalysis
410+
private import internal.RangeUtils::MakeUtils<Sem, D>
412411

413412
/**
414413
* An expression that does conversion, boxing, or unboxing
@@ -522,27 +521,27 @@ module RangeStage<
522521
private predicate boundCondition(
523522
Sem::RelationalExpr comp, Sem::SsaVariable v, Sem::Expr e, D::Delta delta, boolean upper
524523
) {
525-
comp.getLesserOperand() = semSsaRead(v, delta) and
524+
comp.getLesserOperand() = ssaRead(v, delta) and
526525
e = comp.getGreaterOperand() and
527526
upper = true
528527
or
529-
comp.getGreaterOperand() = semSsaRead(v, delta) and
528+
comp.getGreaterOperand() = ssaRead(v, delta) and
530529
e = comp.getLesserOperand() and
531530
upper = false
532531
or
533532
exists(Sem::SubExpr sub, Sem::ConstantIntegerExpr c, D::Delta d |
534533
// (v - d) - e < c
535534
comp.getLesserOperand() = sub and
536535
comp.getGreaterOperand() = c and
537-
sub.getLeftOperand() = semSsaRead(v, d) and
536+
sub.getLeftOperand() = ssaRead(v, d) and
538537
sub.getRightOperand() = e and
539538
upper = true and
540539
delta = D::fromFloat(D::toFloat(d) + c.getIntValue())
541540
or
542541
// (v - d) - e > c
543542
comp.getGreaterOperand() = sub and
544543
comp.getLesserOperand() = c and
545-
sub.getLeftOperand() = semSsaRead(v, d) and
544+
sub.getLeftOperand() = ssaRead(v, d) and
546545
sub.getRightOperand() = e and
547546
upper = false and
548547
delta = D::fromFloat(D::toFloat(d) + c.getIntValue())
@@ -551,15 +550,15 @@ module RangeStage<
551550
comp.getLesserOperand() = sub and
552551
comp.getGreaterOperand() = c and
553552
sub.getLeftOperand() = e and
554-
sub.getRightOperand() = semSsaRead(v, d) and
553+
sub.getRightOperand() = ssaRead(v, d) and
555554
upper = false and
556555
delta = D::fromFloat(D::toFloat(d) - c.getIntValue())
557556
or
558557
// e - (v - d) > c
559558
comp.getGreaterOperand() = sub and
560559
comp.getLesserOperand() = c and
561560
sub.getLeftOperand() = e and
562-
sub.getRightOperand() = semSsaRead(v, d) and
561+
sub.getRightOperand() = ssaRead(v, d) and
563562
upper = true and
564563
delta = D::fromFloat(D::toFloat(d) - c.getIntValue())
565564
)
@@ -677,7 +676,7 @@ module RangeStage<
677676
Sem::SsaVariable v1, Sem::SsaVariable v2, float delta
678677
) {
679678
exists(Sem::Guard guardEq, D::Delta d1, D::Delta d2, boolean eqIsTrue |
680-
guardEq = semEqFlowCond(v1, semSsaRead(v2, d1), d2, true, eqIsTrue) and
679+
guardEq = semEqFlowCond(v1, ssaRead(v2, d1), d2, true, eqIsTrue) and
681680
delta = D::toFloat(d2) - D::toFloat(d1) and
682681
guardEq.directlyControls(result, eqIsTrue)
683682
)

0 commit comments

Comments
 (0)