diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticSSA.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticSSA.qll index 9bc55e4fa80..677bfd22abc 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticSSA.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticSSA.qll @@ -23,6 +23,8 @@ class SemSsaExplicitUpdate extends SemSsaVariable { SemSsaExplicitUpdate() { Specific::explicitUpdate(this, sourceExpr) } final SemExpr getSourceExpr() { result = sourceExpr } + + final SemExpr getDefiningExpr() { result = sourceExpr } } class SemSsaPhiNode extends SemSsaVariable { diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/ModulusAnalysis.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/ModulusAnalysis.qll index c53b0b85eb2..3ef885f8f9e 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/ModulusAnalysis.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/ModulusAnalysis.qll @@ -151,7 +151,7 @@ module ModulusAnalysis Bounds, UtilSig ) { exists(Bounds::SemSsaBound phibound, int v, int m | edge.phiInput(phi, inp) and - phibound.getAVariable() = phi and + phibound.getVariable() = phi and ssaModulus(inp, edge, phibound, v, m) and mod = m.gcd(v) and mod != 1 @@ -233,7 +233,7 @@ module ModulusAnalysis Bounds, UtilSig ) { phiModulus(v, b, val, mod) and pos.hasReadOfVar(v) or - b.(Bounds::SemSsaBound).getAVariable() = v and pos.hasReadOfVar(v) and val = 0 and mod = 0 + b.(Bounds::SemSsaBound).getVariable() = v and pos.hasReadOfVar(v) and val = 0 and mod = 0 or exists(SemExpr e, int val0, int delta | semExprModulus(e, b, val0, mod) and diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisConstantSpecific.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisConstantSpecific.qll index fc729766d2d..d4883b02530 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisConstantSpecific.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisConstantSpecific.qll @@ -8,14 +8,6 @@ private import RangeAnalysisImpl private import codeql.rangeanalysis.RangeAnalysis module CppLangImplConstant implements LangSig { - /** - * Holds if the specified expression should be excluded from the result of `ssaRead()`. - * - * This predicate is to keep the results identical to the original Java implementation. It should be - * removed once we have the new implementation matching the old results exactly. - */ - predicate ignoreSsaReadCopy(SemExpr e) { none() } - /** * Ignore the bound on this expression. * @@ -24,40 +16,6 @@ module CppLangImplConstant implements LangSig { */ predicate ignoreExprBound(SemExpr e) { none() } - /** - * Ignore any inferred zero lower bound on this expression. - * - * This predicate is to keep the results identical to the original Java implementation. It should be - * removed once we have the new implementation matching the old results exactly. - */ - predicate ignoreZeroLowerBound(SemExpr e) { none() } - - /** - * Holds if the specified expression should be excluded from the result of `ssaRead()`. - * - * This predicate is to keep the results identical to the original Java implementation. It should be - * removed once we have the new implementation matching the old results exactly. - */ - predicate ignoreSsaReadArithmeticExpr(SemExpr e) { none() } - - /** - * Holds if the specified variable should be excluded from the result of `ssaRead()`. - * - * This predicate is to keep the results identical to the original Java implementation. It should be - * removed once we have the new implementation matching the old results exactly. - */ - predicate ignoreSsaReadAssignment(SemSsaVariable v) { none() } - - /** - * Adds additional results to `ssaRead()` that are specific to Java. - * - * This predicate handles propagation of offsets for post-increment and post-decrement expressions - * in exactly the same way as the old Java implementation. Once the new implementation matches the - * old one, we should remove this predicate and propagate deltas for all similar patterns, whether - * or not they come from a post-increment/decrement expression. - */ - SemExpr specificSsaRead(SemSsaVariable v, float delta) { none() } - /** * Holds if `e >= bound` (if `upper = false`) or `e <= bound` (if `upper = true`). */ diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll index cbbd5d092bb..3e336a3d514 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll @@ -52,9 +52,21 @@ module Sem implements Semantic { class NegateExpr = SemNegateExpr; - class AddOneExpr = SemAddOneExpr; + class PreIncExpr = SemAddOneExpr; - class SubOneExpr = SemSubOneExpr; + class PreDecExpr = SemSubOneExpr; + + class PostIncExpr extends SemUnaryExpr { + PostIncExpr() { none() } + } + + class PostDecExpr extends SemUnaryExpr { + PostDecExpr() { none() } + } + + class CopyValueExpr extends SemUnaryExpr { + CopyValueExpr() { this instanceof SemCopyValueExpr or this instanceof SemStoreExpr } + } class ConditionalExpr = SemConditionalExpr; @@ -116,7 +128,7 @@ module ConstantBounds implements BoundSig { class SemZeroBound extends SemBound instanceof SemanticBound::SemZeroBound { } class SemSsaBound extends SemBound instanceof SemanticBound::SemSsaBound { - SemSsaVariable getAVariable() { result = this.(SemanticBound::SemSsaBound).getAVariable() } + SemSsaVariable getVariable() { result = this.(SemanticBound::SemSsaBound).getAVariable() } } } @@ -134,7 +146,7 @@ module RelativeBounds implements BoundSig { class SemZeroBound extends SemBound instanceof SemanticBound::SemZeroBound { } class SemSsaBound extends SemBound instanceof SemanticBound::SemSsaBound { - SemSsaVariable getAVariable() { result = this.(SemanticBound::SemSsaBound).getAVariable() } + SemSsaVariable getVariable() { result = this.(SemanticBound::SemSsaBound).getAVariable() } } } @@ -150,7 +162,7 @@ module AllBounds implements BoundSig { class SemZeroBound extends SemBound instanceof SemanticBound::SemZeroBound { } class SemSsaBound extends SemBound instanceof SemanticBound::SemSsaBound { - SemSsaVariable getAVariable() { result = this.(SemanticBound::SemSsaBound).getAVariable() } + SemSsaVariable getVariable() { result = this.(SemanticBound::SemSsaBound).getAVariable() } } } diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisRelativeSpecific.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisRelativeSpecific.qll index 11421978386..29cef82579c 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisRelativeSpecific.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisRelativeSpecific.qll @@ -9,14 +9,6 @@ private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils private import codeql.rangeanalysis.RangeAnalysis module CppLangImplRelative implements LangSig { - /** - * Holds if the specified expression should be excluded from the result of `ssaRead()`. - * - * This predicate is to keep the results identical to the original Java implementation. It should be - * removed once we have the new implementation matching the old results exactly. - */ - predicate ignoreSsaReadCopy(SemExpr e) { none() } - /** * Ignore the bound on this expression. * @@ -56,40 +48,6 @@ module CppLangImplRelative implements LangSig { t instanceof SemFloatingPointType and lb = -(1.0 / 0.0) and ub = 1.0 / 0.0 } - /** - * Ignore any inferred zero lower bound on this expression. - * - * This predicate is to keep the results identical to the original Java implementation. It should be - * removed once we have the new implementation matching the old results exactly. - */ - predicate ignoreZeroLowerBound(SemExpr e) { none() } - - /** - * Holds if the specified expression should be excluded from the result of `ssaRead()`. - * - * This predicate is to keep the results identical to the original Java implementation. It should be - * removed once we have the new implementation matching the old results exactly. - */ - predicate ignoreSsaReadArithmeticExpr(SemExpr e) { none() } - - /** - * Holds if the specified variable should be excluded from the result of `ssaRead()`. - * - * This predicate is to keep the results identical to the original Java implementation. It should be - * removed once we have the new implementation matching the old results exactly. - */ - predicate ignoreSsaReadAssignment(SemSsaVariable v) { none() } - - /** - * Adds additional results to `ssaRead()` that are specific to Java. - * - * This predicate handles propagation of offsets for post-increment and post-decrement expressions - * in exactly the same way as the old Java implementation. Once the new implementation matches the - * old one, we should remove this predicate and propagate deltas for all similar patterns, whether - * or not they come from a post-increment/decrement expression. - */ - SemExpr specificSsaRead(SemSsaVariable v, float delta) { none() } - /** * Holds if `e >= bound` (if `upper = false`) or `e <= bound` (if `upper = true`). */ 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..c61bf4817c2 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,33 +12,27 @@ 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) or exists(D::Delta d1, SemConstantIntegerExpr c | result.(SemAddExpr).hasOperands(semSsaRead(v, d1), c) and - delta = D::fromFloat(D::toFloat(d1) - c.getIntValue()) and - not Lang::ignoreSsaReadArithmeticExpr(result) + 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()) and - not Lang::ignoreSsaReadArithmeticExpr(result) + delta = D::fromFloat(D::toFloat(d1) + c.getIntValue()) ) or result = v.(SemSsaExplicitUpdate).getSourceExpr() and - delta = D::fromFloat(0) and - not Lang::ignoreSsaReadAssignment(v) + delta = D::fromFloat(0) or - result = Lang::specificSsaRead(v, delta) - or - result.(SemCopyValueExpr).getOperand() = semSsaRead(v, delta) and - not Lang::ignoreSsaReadCopy(result) + result.(SemCopyValueExpr).getOperand() = semSsaRead(v, delta) or result.(SemStoreExpr).getOperand() = semSsaRead(v, delta) } 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 2b2b539d548..f4f7adaa330 100644 --- a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll +++ b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll @@ -150,6 +150,8 @@ module Sem implements Semantic { } } + predicate isAssignOp(BinaryExpr bin) { bin instanceof AssignOp } + class RelationalExpr = J::ComparisonExpr; abstract class UnaryExpr extends Expr { @@ -176,18 +178,34 @@ module Sem implements Semantic { override Expr getOperand() { result = super.getExpr() } } - // TODO: Implement once utils are properly shared - class AddOneExpr extends UnaryExpr { - AddOneExpr() { none() } - - override Expr getOperand() { none() } + class PreIncExpr extends UnaryExpr instanceof J::PreIncExpr { + override Expr getOperand() { result = super.getExpr() } } - // TODO: Implement once utils are properly shared - class SubOneExpr extends UnaryExpr { - SubOneExpr() { none() } + class PreDecExpr extends UnaryExpr instanceof J::PreDecExpr { + override Expr getOperand() { result = super.getExpr() } + } - override Expr getOperand() { none() } + class PostIncExpr extends UnaryExpr instanceof J::PostIncExpr { + override Expr getOperand() { result = super.getExpr() } + } + + class PostDecExpr extends UnaryExpr instanceof J::PostDecExpr { + override Expr getOperand() { result = super.getExpr() } + } + + class CopyValueExpr extends UnaryExpr { + CopyValueExpr() { + this instanceof J::PlusExpr or + this instanceof J::AssignExpr or + this instanceof LocalVariableDeclExpr + } + + override Expr getOperand() { + result = this.(J::PlusExpr).getExpr() or + result = this.(J::AssignExpr).getSource() or + result = this.(J::LocalVariableDeclExpr).getInit() + } } class ConditionalExpr = J::ConditionalExpr; @@ -228,7 +246,9 @@ module Sem implements Semantic { class SsaPhiNode extends SsaVariable instanceof SSA::SsaPhiNode { } - class SsaExplicitUpdate extends SsaVariable instanceof SSA::SsaExplicitUpdate { } + class SsaExplicitUpdate extends SsaVariable instanceof SSA::SsaExplicitUpdate { + Expr getDefiningExpr() { result = super.getDefiningExpr() } + } final private class FinalSsaReadPosition = SsaReadPos::SsaReadPosition; @@ -295,8 +315,6 @@ module IntDelta implements DeltaSig { } module JavaLangImpl implements LangSig { - predicate ignoreSsaReadCopy(Sem::Expr e) { none() } - /** * Holds if `e >= bound` (if `upper = false`) or `e <= bound` (if `upper = true`). */ @@ -355,14 +373,6 @@ module JavaLangImpl implements LangSig { predicate ignoreExprBound(Sem::Expr e) { none() } - predicate ignoreZeroLowerBound(Sem::Expr e) { none() } - - predicate ignoreSsaReadArithmeticExpr(Sem::Expr e) { none() } - - predicate ignoreSsaReadAssignment(Sem::SsaVariable v) { none() } - - Sem::Expr specificSsaRead(Sem::SsaVariable v, int delta) { none() } - predicate additionalValueFlowStep(Sem::Expr dest, Sem::Expr src, int delta) { none() } Sem::Type getAlternateType(Sem::Expr e) { none() } @@ -376,8 +386,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 ) { @@ -411,7 +419,7 @@ module Bounds implements BoundSig { class SemZeroBound = ZeroBound; class SemSsaBound extends SsaBound { - Sem::SsaVariable getAVariable() { result = super.getSsa() } + Sem::SsaVariable getVariable() { result = super.getSsa() } } } diff --git a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll index 50c0130ffcd..b94d6ab9115 100644 --- a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll +++ b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll @@ -106,6 +106,8 @@ signature module Semantic { class ShiftRightUnsignedExpr extends BinaryExpr; + default predicate isAssignOp(BinaryExpr bin) { none() } + class RelationalExpr extends Expr { Expr getLesserOperand(); @@ -126,9 +128,15 @@ signature module Semantic { class NegateExpr extends UnaryExpr; - class AddOneExpr extends UnaryExpr; + class PreIncExpr extends UnaryExpr; - class SubOneExpr extends UnaryExpr; + class PreDecExpr extends UnaryExpr; + + class PostIncExpr extends UnaryExpr; + + class PostDecExpr extends UnaryExpr; + + class CopyValueExpr extends UnaryExpr; class ConditionalExpr extends Expr { Expr getBranchExpr(boolean branch); @@ -168,7 +176,9 @@ signature module Semantic { class SsaPhiNode extends SsaVariable; - class SsaExplicitUpdate extends SsaVariable; + class SsaExplicitUpdate extends SsaVariable { + Expr getDefiningExpr(); + } class SsaReadPosition { predicate hasReadOfVar(SsaVariable v); @@ -240,14 +250,6 @@ signature module DeltaSig { } signature module LangSig { - /** - * Holds if the specified expression should be excluded from the result of `ssaRead()`. - * - * This predicate is to keep the results identical to the original Java implementation. It should be - * removed once we have the new implementation matching the old results exactly. - */ - predicate ignoreSsaReadCopy(Sem::Expr e); - /** * Holds if `e >= bound` (if `upper = false`) or `e <= bound` (if `upper = true`). */ @@ -266,40 +268,6 @@ signature module LangSig { */ predicate ignoreExprBound(Sem::Expr e); - /** - * Ignore any inferred zero lower bound on this expression. - * - * This predicate is to keep the results identical to the original Java implementation. It should be - * removed once we have the new implementation matching the old results exactly. - */ - predicate ignoreZeroLowerBound(Sem::Expr e); - - /** - * Holds if the specified expression should be excluded from the result of `ssaRead()`. - * - * This predicate is to keep the results identical to the original Java implementation. It should be - * removed once we have the new implementation matching the old results exactly. - */ - predicate ignoreSsaReadArithmeticExpr(Sem::Expr e); - - /** - * Holds if the specified variable should be excluded from the result of `ssaRead()`. - * - * This predicate is to keep the results identical to the original Java implementation. It should be - * removed once we have the new implementation matching the old results exactly. - */ - predicate ignoreSsaReadAssignment(Sem::SsaVariable v); - - /** - * Adds additional results to `ssaRead()` that are specific to Java. - * - * This predicate handles propagation of offsets for post-increment and post-decrement expressions - * in exactly the same way as the old Java implementation. Once the new implementation matches the - * old one, we should remove this predicate and propagate deltas for all similar patterns, whether - * or not they come from a post-increment/decrement expression. - */ - Sem::Expr specificSsaRead(Sem::SsaVariable v, D::Delta delta); - /** * Holds if the value of `dest` is known to be `src + delta`. */ @@ -327,8 +295,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 ); @@ -379,7 +345,7 @@ signature module BoundSig { class SemZeroBound extends SemBound; class SemSsaBound extends SemBound { - Sem::SsaVariable getAVariable(); + Sem::SsaVariable getVariable(); } } @@ -399,6 +365,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 @@ -512,11 +479,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 @@ -524,7 +491,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()) @@ -532,7 +499,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()) @@ -541,7 +508,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 @@ -549,7 +516,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()) ) @@ -667,7 +634,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) ) @@ -950,7 +917,7 @@ module RangeStage< or boundedPhi(inp, b, d, upper, fromBackEdge0, origdelta, reason) or - b.(SemSsaBound).getAVariable() = inp and + b.(SemSsaBound).getVariable() = inp and d = D::fromFloat(0) and (upper = true or upper = false) and fromBackEdge0 = false and @@ -1000,7 +967,7 @@ module RangeStage< Sem::SsaPhiNode phi, Sem::SsaVariable inp, Sem::SsaReadPositionPhiInputEdge edge, boolean upper ) { exists(D::Delta d, SemSsaBound phibound | - phibound.getAVariable() = phi and + phibound.getVariable() = phi and boundedPhiInp(phi, inp, edge, phibound, d, upper, _, _, _) and ( upper = true and D::toFloat(d) <= 0 @@ -1091,9 +1058,7 @@ module RangeStage< or upper = false and b = D::fromInt(0) and - semPositive(e.(Sem::BitAndExpr).getAnOperand()) and - // REVIEW: We let the language opt out here to preserve original results. - not ignoreZeroLowerBound(e) + semPositive(e.(Sem::BitAndExpr).getAnOperand()) } /** @@ -1188,12 +1153,12 @@ module RangeStage< positively = false and ( expr instanceof Sem::NegateExpr or - expr instanceof Sem::SubOneExpr or + expr instanceof Sem::PreDecExpr or getTrackedType(expr.(Sem::DivExpr)) instanceof Sem::FloatingPointType ) or positively = true and - expr instanceof Sem::AddOneExpr + expr instanceof Sem::PreIncExpr } /** diff --git a/shared/rangeanalysis/codeql/rangeanalysis/internal/RangeUtils.qll b/shared/rangeanalysis/codeql/rangeanalysis/internal/RangeUtils.qll new file mode 100644 index 00000000000..3a471aa2c38 --- /dev/null +++ b/shared/rangeanalysis/codeql/rangeanalysis/internal/RangeUtils.qll @@ -0,0 +1,37 @@ +private import codeql.rangeanalysis.RangeAnalysis + +module MakeUtils { + /** + * Gets an expression that equals `v - d`. + */ + Lang::Expr ssaRead(Lang::SsaVariable v, D::Delta delta) { + result = v.getAUse() and delta = D::fromInt(0) + or + exists(D::Delta d1, Lang::ConstantIntegerExpr c | + result.(Lang::AddExpr).hasOperands(ssaRead(v, d1), c) and + delta = D::fromFloat(D::toFloat(d1) - c.getIntValue()) and + // In the scope of `x += ..`, which is SSA translated as `x2 = x1 + ..`, + // the variable `x1` is shadowed by `x2`, so there's no need to view this + // as a read of `x1`. + not Lang::isAssignOp(result) + ) + or + exists(Lang::SubExpr sub, D::Delta d1, Lang::ConstantIntegerExpr c | + result = sub and + sub.getLeftOperand() = ssaRead(v, d1) and + sub.getRightOperand() = c and + delta = D::fromFloat(D::toFloat(d1) + c.getIntValue()) and + not Lang::isAssignOp(result) + ) + or + result = v.(Lang::SsaExplicitUpdate).getDefiningExpr() and + if result instanceof Lang::PostIncExpr + then delta = D::fromFloat(1) // x++ === ++x - 1 + else + if result instanceof Lang::PostDecExpr + then delta = D::fromFloat(-1) // x-- === --x + 1 + else delta = D::fromFloat(0) + or + result.(Lang::CopyValueExpr).getOperand() = ssaRead(v, delta) + } +}