From a39a94ca8ebe7076edb394cba92bd462b7385309 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 31 Oct 2023 15:23:05 +0100 Subject: [PATCH] Rangeanalysis: Switch to shared ssaRead predicate. --- .../internal/semantic/analysis/RangeUtils.qll | 2 +- .../semantic/analysis/SignAnalysisCommon.qll | 12 +++++++----- .../semmle/code/java/dataflow/RangeAnalysis.qll | 2 -- .../codeql/rangeanalysis/RangeAnalysis.qll | 17 ++++++++--------- 4 files changed, 16 insertions(+), 17 deletions(-) diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeUtils.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeUtils.qll index e3798600f85..6b6af10c45f 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeUtils.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeUtils.qll @@ -12,7 +12,7 @@ module RangeUtil Lang> implements UtilSig { /** * Gets an expression that equals `v - d`. */ - SemExpr semSsaRead(SemSsaVariable v, D::Delta delta) { + private SemExpr semSsaRead(SemSsaVariable v, D::Delta delta) { // There are various language-specific extension points that can be removed once we no longer // expect to match the original Java implementation's results exactly. result = v.getAUse() and delta = D::fromInt(0) diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/SignAnalysisCommon.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/SignAnalysisCommon.qll index 20ada012c2a..fff53b99cf6 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/SignAnalysisCommon.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/SignAnalysisCommon.qll @@ -15,6 +15,8 @@ private import RangeUtils private import Sign module SignAnalysis Utils> { + private import codeql.rangeanalysis.internal.RangeUtils::MakeUtils + /** * An SSA definition for which the analysis can compute the sign. * @@ -297,12 +299,12 @@ module SignAnalysis Utils> { | testIsTrue = true and comp.getLesserOperand() = lowerbound and - comp.getGreaterOperand() = Utils::semSsaRead(v, D::fromInt(0)) and + comp.getGreaterOperand() = ssaRead(v, D::fromInt(0)) and (if comp.isStrict() then isStrict = true else isStrict = false) or testIsTrue = false and comp.getGreaterOperand() = lowerbound and - comp.getLesserOperand() = Utils::semSsaRead(v, D::fromInt(0)) and + comp.getLesserOperand() = ssaRead(v, D::fromInt(0)) and (if comp.isStrict() then isStrict = false else isStrict = true) ) } @@ -321,12 +323,12 @@ module SignAnalysis Utils> { | testIsTrue = true and comp.getGreaterOperand() = upperbound and - comp.getLesserOperand() = Utils::semSsaRead(v, D::fromInt(0)) and + comp.getLesserOperand() = ssaRead(v, D::fromInt(0)) and (if comp.isStrict() then isStrict = true else isStrict = false) or testIsTrue = false and comp.getLesserOperand() = upperbound and - comp.getGreaterOperand() = Utils::semSsaRead(v, D::fromInt(0)) and + comp.getGreaterOperand() = ssaRead(v, D::fromInt(0)) and (if comp.isStrict() then isStrict = false else isStrict = true) ) } @@ -342,7 +344,7 @@ module SignAnalysis Utils> { exists(SemGuard guard, boolean testIsTrue, boolean polarity, SemExpr e | pos.hasReadOfVar(pragma[only_bind_into](v)) and semGuardControlsSsaRead(guard, pragma[only_bind_into](pos), testIsTrue) and - e = Utils::semSsaRead(pragma[only_bind_into](v), D::fromInt(0)) and + e = ssaRead(pragma[only_bind_into](v), D::fromInt(0)) and guard.isEquality(eqbound, e, polarity) and isEq = polarity.booleanXor(testIsTrue).booleanNot() and not unknownSign(eqbound) diff --git a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll index e521d8632e5..16480187482 100644 --- a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll +++ b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll @@ -396,8 +396,6 @@ module Utils implements UtilSig { private import RangeUtils as RU private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon as SsaReadPos - Sem::Expr semSsaRead(Sem::SsaVariable v, int delta) { result = RU::ssaRead(v, delta) } - Sem::Guard semEqFlowCond( Sem::SsaVariable v, Sem::Expr e, int delta, boolean isEq, boolean testIsTrue ) { diff --git a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll index d750ac4f945..83bcddd80a4 100644 --- a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll +++ b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll @@ -337,8 +337,6 @@ signature module LangSig { } signature module UtilSig { - Sem::Expr semSsaRead(Sem::SsaVariable v, DeltaParam::Delta delta); - Sem::Guard semEqFlowCond( Sem::SsaVariable v, Sem::Expr e, DeltaParam::Delta delta, boolean isEq, boolean testIsTrue ); @@ -409,6 +407,7 @@ module RangeStage< private import OverflowParam private import SignAnalysis private import ModulusAnalysis + private import internal.RangeUtils::MakeUtils /** * An expression that does conversion, boxing, or unboxing @@ -522,11 +521,11 @@ module RangeStage< private predicate boundCondition( Sem::RelationalExpr comp, Sem::SsaVariable v, Sem::Expr e, D::Delta delta, boolean upper ) { - comp.getLesserOperand() = semSsaRead(v, delta) and + comp.getLesserOperand() = ssaRead(v, delta) and e = comp.getGreaterOperand() and upper = true or - comp.getGreaterOperand() = semSsaRead(v, delta) and + comp.getGreaterOperand() = ssaRead(v, delta) and e = comp.getLesserOperand() and upper = false or @@ -534,7 +533,7 @@ module RangeStage< // (v - d) - e < c comp.getLesserOperand() = sub and comp.getGreaterOperand() = c and - sub.getLeftOperand() = semSsaRead(v, d) and + sub.getLeftOperand() = ssaRead(v, d) and sub.getRightOperand() = e and upper = true and delta = D::fromFloat(D::toFloat(d) + c.getIntValue()) @@ -542,7 +541,7 @@ module RangeStage< // (v - d) - e > c comp.getGreaterOperand() = sub and comp.getLesserOperand() = c and - sub.getLeftOperand() = semSsaRead(v, d) and + sub.getLeftOperand() = ssaRead(v, d) and sub.getRightOperand() = e and upper = false and delta = D::fromFloat(D::toFloat(d) + c.getIntValue()) @@ -551,7 +550,7 @@ module RangeStage< comp.getLesserOperand() = sub and comp.getGreaterOperand() = c and sub.getLeftOperand() = e and - sub.getRightOperand() = semSsaRead(v, d) and + sub.getRightOperand() = ssaRead(v, d) and upper = false and delta = D::fromFloat(D::toFloat(d) - c.getIntValue()) or @@ -559,7 +558,7 @@ module RangeStage< comp.getGreaterOperand() = sub and comp.getLesserOperand() = c and sub.getLeftOperand() = e and - sub.getRightOperand() = semSsaRead(v, d) and + sub.getRightOperand() = ssaRead(v, d) and upper = true and delta = D::fromFloat(D::toFloat(d) - c.getIntValue()) ) @@ -677,7 +676,7 @@ module RangeStage< Sem::SsaVariable v1, Sem::SsaVariable v2, float delta ) { exists(Sem::Guard guardEq, D::Delta d1, D::Delta d2, boolean eqIsTrue | - guardEq = semEqFlowCond(v1, semSsaRead(v2, d1), d2, true, eqIsTrue) and + guardEq = semEqFlowCond(v1, ssaRead(v2, d1), d2, true, eqIsTrue) and delta = D::toFloat(d2) - D::toFloat(d1) and guardEq.directlyControls(result, eqIsTrue) )