From daffae020b7c4fbd7dc24f15cb58c847bc3bc80e Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Thu, 9 Nov 2023 15:36:46 +0100 Subject: [PATCH] Java/C++: Share eqFlowCond. --- .../internal/semantic/analysis/RangeUtils.qll | 50 ------------------- .../code/java/dataflow/RangeAnalysis.qll | 6 --- .../semmle/code/java/dataflow/RangeUtils.qll | 21 +------- .../codeql/rangeanalysis/ModulusAnalysis.qll | 2 +- .../codeql/rangeanalysis/RangeAnalysis.qll | 12 ++--- .../rangeanalysis/internal/RangeUtils.qll | 20 ++++++++ 6 files changed, 27 insertions(+), 84 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 7276f066220..11624d5397f 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 @@ -9,56 +9,6 @@ private import RangeAnalysisImpl private import ConstantAnalysis module RangeUtil Lang> implements UtilSig { - /** - * Gets an expression that equals `v - d`. - */ - 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) - or - exists(D::Delta d1, SemConstantIntegerExpr c | - result.(SemAddExpr).hasOperands(semSsaRead(v, d1), c) and - delta = D::fromFloat(D::toFloat(d1) - c.getIntValue()) - ) - or - exists(SemSubExpr sub, D::Delta d1, SemConstantIntegerExpr c | - result = sub and - sub.getLeftOperand() = semSsaRead(v, d1) and - sub.getRightOperand() = c and - delta = D::fromFloat(D::toFloat(d1) + c.getIntValue()) - ) - or - result = v.(SemSsaExplicitUpdate).getSourceExpr() and - delta = D::fromFloat(0) - or - result.(SemCopyValueExpr).getOperand() = semSsaRead(v, delta) - or - result.(SemStoreExpr).getOperand() = semSsaRead(v, delta) - } - - /** - * Gets a condition that tests whether `v` equals `e + delta`. - * - * If the condition evaluates to `testIsTrue`: - * - `isEq = true` : `v == e + delta` - * - `isEq = false` : `v != e + delta` - */ - pragma[nomagic] - SemGuard semEqFlowCond( - SemSsaVariable v, SemExpr e, D::Delta delta, boolean isEq, boolean testIsTrue - ) { - exists(boolean eqpolarity | - result.isEquality(semSsaRead(v, delta), e, eqpolarity) and - (testIsTrue = true or testIsTrue = false) and - eqpolarity.booleanXor(testIsTrue).booleanNot() = isEq - ) - or - exists(boolean testIsTrue0 | - semImplies_v2(result, testIsTrue, semEqFlowCond(v, e, delta, isEq, testIsTrue0), testIsTrue0) - ) - } - /** * Holds if `v` is an `SsaExplicitUpdate` that equals `e + delta`. */ diff --git a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll index 64d17202d67..bd7ab9411d3 100644 --- a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll +++ b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll @@ -372,12 +372,6 @@ module JavaLangImpl implements LangSig { module Utils implements UtilSig { private import RangeUtils as RU - Sem::Guard semEqFlowCond( - Sem::SsaVariable v, Sem::Expr e, int delta, boolean isEq, boolean testIsTrue - ) { - result = RU::eqFlowCond(v, e, delta, isEq, testIsTrue) - } - predicate semSsaUpdateStep(Sem::SsaExplicitUpdate v, Sem::Expr e, int delta) { RU::ssaUpdateStep(v, e, delta) } diff --git a/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll b/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll index f01d5cc8d54..c9a7412011f 100644 --- a/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll +++ b/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll @@ -19,6 +19,8 @@ predicate guardDirectlyControlsSsaRead = U::guardDirectlyControlsSsaRead/3; predicate guardControlsSsaRead = U::guardControlsSsaRead/3; +predicate eqFlowCond = U::eqFlowCond/5; + /** * Holds if `v` is an input to `phi` that is not along a back edge, and the * only other input to `phi` is a `null` value. @@ -156,25 +158,6 @@ class ConstantStringExpr extends Expr { string getStringValue() { constantStringExpr(this, result) } } -/** - * Gets a condition that tests whether `v` equals `e + delta`. - * - * If the condition evaluates to `testIsTrue`: - * - `isEq = true` : `v == e + delta` - * - `isEq = false` : `v != e + delta` - */ -Guard eqFlowCond(SsaVariable v, Expr e, int delta, boolean isEq, boolean testIsTrue) { - exists(boolean eqpolarity | - result.isEquality(ssaRead(v, delta), e, eqpolarity) and - (testIsTrue = true or testIsTrue = false) and - eqpolarity.booleanXor(testIsTrue).booleanNot() = isEq - ) - or - exists(boolean testIsTrue0 | - implies_v2(result, testIsTrue, eqFlowCond(v, e, delta, isEq, testIsTrue0), testIsTrue0) - ) -} - /** * Holds if `v` is an `SsaExplicitUpdate` that equals `e + delta`. */ diff --git a/shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll b/shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll index 16d63b8ca00..66652b930ac 100644 --- a/shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll +++ b/shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll @@ -34,7 +34,7 @@ module ModulusAnalysis< or exists(Sem::Guard guard, boolean testIsTrue | hasReadOfVarInlineLate(pos, v) and - guard = U::semEqFlowCond(v, e, D::fromInt(delta), true, testIsTrue) and + guard = eqFlowCond(v, e, D::fromInt(delta), true, testIsTrue) and guardDirectlyControlsSsaRead(guard, pos, testIsTrue) ) } diff --git a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll index 3bb399dcebc..302f322dd63 100644 --- a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll +++ b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll @@ -304,10 +304,6 @@ signature module LangSig { } signature module UtilSig { - Sem::Guard semEqFlowCond( - Sem::SsaVariable v, Sem::Expr e, DeltaParam::Delta delta, boolean isEq, boolean testIsTrue - ); - predicate semSsaUpdateStep(Sem::SsaExplicitUpdate v, Sem::Expr e, DeltaParam::Delta delta); predicate semValueFlowStep(Sem::Expr e2, Sem::Expr e1, DeltaParam::Delta delta); @@ -447,7 +443,7 @@ module RangeStage< */ cached predicate possibleReason(Sem::Guard guard) { - guard = boundFlowCond(_, _, _, _, _) or guard = semEqFlowCond(_, _, _, _, _) + guard = boundFlowCond(_, _, _, _, _) or guard = eqFlowCond(_, _, _, _, _) } } @@ -609,7 +605,7 @@ module RangeStage< testIsTrue0) ) or - result = semEqFlowCond(v, e, delta, true, testIsTrue) and + result = eqFlowCond(v, e, delta, true, testIsTrue) and (upper = true or upper = false) or // guard that tests whether `v2` is bounded by `e + delta + d1 - d2` and @@ -630,7 +626,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, ssaRead(v2, d1), d2, true, eqIsTrue) and + guardEq = eqFlowCond(v1, ssaRead(v2, d1), d2, true, eqIsTrue) and delta = D::toFloat(d2) - D::toFloat(d1) and guardEq.directlyControls(result, eqIsTrue) ) @@ -695,7 +691,7 @@ module RangeStage< getTrackedTypeForSsaVariable(v) instanceof Sem::IntegerType and exists(Sem::Guard guard, boolean testIsTrue | pos.hasReadOfVar(v) and - guard = semEqFlowCond(v, e, delta, false, testIsTrue) and + guard = eqFlowCond(v, e, delta, false, testIsTrue) and guardDirectlyControlsSsaRead(guard, pos, testIsTrue) and reason = TSemCondReason(guard) ) diff --git a/shared/rangeanalysis/codeql/rangeanalysis/internal/RangeUtils.qll b/shared/rangeanalysis/codeql/rangeanalysis/internal/RangeUtils.qll index 27205896014..80423c5ce51 100644 --- a/shared/rangeanalysis/codeql/rangeanalysis/internal/RangeUtils.qll +++ b/shared/rangeanalysis/codeql/rangeanalysis/internal/RangeUtils.qll @@ -37,6 +37,26 @@ module MakeUtils { result.(CopyValueExpr).getOperand() = ssaRead(v, delta) } + /** + * Gets a condition that tests whether `v` equals `e + delta`. + * + * If the condition evaluates to `testIsTrue`: + * - `isEq = true` : `v == e + delta` + * - `isEq = false` : `v != e + delta` + */ + pragma[nomagic] + Guard eqFlowCond(SsaVariable v, Expr e, D::Delta delta, boolean isEq, boolean testIsTrue) { + exists(boolean eqpolarity | + result.isEquality(ssaRead(v, delta), e, eqpolarity) and + (testIsTrue = true or testIsTrue = false) and + eqpolarity.booleanXor(testIsTrue).booleanNot() = isEq + ) + or + exists(boolean testIsTrue0 | + implies_v2(result, testIsTrue, eqFlowCond(v, e, delta, isEq, testIsTrue0), testIsTrue0) + ) + } + private newtype TSsaReadPosition = TSsaReadPositionBlock(BasicBlock bb) { exists(SsaVariable v | v.getAUse().getBasicBlock() = bb)