From 8bf4a4209c9026c3b87a59a24df26c8c093c4552 Mon Sep 17 00:00:00 2001 From: Tamas Vajk Date: Wed, 2 Sep 2020 16:52:17 +0200 Subject: [PATCH] C#: Sign analysis Synced between Java and C# through `identical-files.json`. --- config/identical-files.json | 20 +- csharp/ql/src/Linq/Helpers.qll | 11 + .../code/csharp/commons/ComparisonTest.qll | 2 +- .../semmle/code/csharp/controlflow/Guards.qll | 27 + .../semmle/code/csharp/dataflow/Nullness.qll | 2 - .../src/semmle/code/csharp/dataflow/SSA.qll | 7 + .../code/csharp/dataflow/SignAnalysis.qll | 9 + .../internal/rangeanalysis/ConstantUtils.qll | 64 ++ .../dataflow/internal/rangeanalysis/Sign.qll | 219 +++++++ .../rangeanalysis/SignAnalysisCommon.qll | 293 +++++++++ .../rangeanalysis/SignAnalysisSpecific.qll | 283 +++++++++ .../rangeanalysis/SsaReadPositionCommon.qll | 57 ++ .../rangeanalysis/SsaReadPositionSpecific.qll | 16 + .../internal/rangeanalysis/SsaUtils.qll | 42 ++ .../code/csharp/exprs/ComparisonOperation.qll | 3 + .../signanalysis/MissingSign.expected | 4 + .../dataflow/signanalysis/MissingSign.ql | 15 + .../dataflow/signanalysis/SignAnalysis.cs | 455 ++++++++++++++ .../signanalysis/SignAnalysis.expected | 217 +++++++ .../dataflow/signanalysis/SignAnalysis.ql | 21 + .../code/java/dataflow/ModulusAnalysis.qll | 1 + .../code/java/dataflow/RangeAnalysis.qll | 1 + .../semmle/code/java/dataflow/RangeUtils.qll | 58 +- .../code/java/dataflow/SignAnalysis.qll | 594 +----------------- .../dataflow/internal/rangeanalysis/Sign.qll | 219 +++++++ .../rangeanalysis/SignAnalysisCommon.qll | 293 +++++++++ .../rangeanalysis/SignAnalysisSpecific.qll | 235 +++++++ .../rangeanalysis/SsaReadPositionCommon.qll | 57 ++ .../rangeanalysis/SsaReadPositionSpecific.qll | 15 + .../sign-analysis/SignAnalysis.expected | 4 +- .../dataflow/sign-analysis/SignAnalysis.ql | 12 +- 31 files changed, 2592 insertions(+), 664 deletions(-) create mode 100644 csharp/ql/src/semmle/code/csharp/dataflow/SignAnalysis.qll create mode 100644 csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/ConstantUtils.qll create mode 100644 csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/Sign.qll create mode 100644 csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SignAnalysisCommon.qll create mode 100644 csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll create mode 100644 csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaReadPositionCommon.qll create mode 100644 csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaReadPositionSpecific.qll create mode 100644 csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaUtils.qll create mode 100644 csharp/ql/test/library-tests/dataflow/signanalysis/MissingSign.expected create mode 100644 csharp/ql/test/library-tests/dataflow/signanalysis/MissingSign.ql create mode 100644 csharp/ql/test/library-tests/dataflow/signanalysis/SignAnalysis.cs create mode 100644 csharp/ql/test/library-tests/dataflow/signanalysis/SignAnalysis.expected create mode 100644 csharp/ql/test/library-tests/dataflow/signanalysis/SignAnalysis.ql create mode 100644 java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/Sign.qll create mode 100644 java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisCommon.qll create mode 100644 java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll create mode 100644 java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SsaReadPositionCommon.qll create mode 100644 java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SsaReadPositionSpecific.qll diff --git a/config/identical-files.json b/config/identical-files.json index 7e62497c9bf..e0a4e8dabf4 100644 --- a/config/identical-files.json +++ b/config/identical-files.json @@ -50,6 +50,18 @@ "csharp/ql/src/semmle/code/csharp/dataflow/internal/DataFlowImplConsistency.qll", "python/ql/src/experimental/dataflow/internal/DataFlowImplConsistency.qll" ], + "SsaReadPosition Java/C#": [ + "java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SsaReadPositionCommon.qll", + "csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaReadPositionCommon.qll" + ], + "Sign Java/C#": [ + "java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/Sign.qll", + "csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/Sign.qll" + ], + "SignAnalysis Java/C#": [ + "java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisCommon.qll", + "csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SignAnalysisCommon.qll" + ], "C++ SubBasicBlocks": [ "cpp/ql/src/semmle/code/cpp/controlflow/SubBasicBlocks.qll", "cpp/ql/src/semmle/code/cpp/dataflow/internal/SubBasicBlocks.qll" @@ -87,7 +99,7 @@ "cpp/ql/src/semmle/code/cpp/ir/implementation/unaliased_ssa/Operand.qll", "cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/Operand.qll", "csharp/ql/src/experimental/ir/implementation/raw/Operand.qll", - "csharp/ql/src/experimental/ir/implementation/unaliased_ssa/Operand.qll" + "csharp/ql/src/experimental/ir/implementation/unaliased_ssa/Operand.qll" ], "IR IRType": [ "cpp/ql/src/semmle/code/cpp/ir/implementation/IRType.qll", @@ -109,11 +121,11 @@ "cpp/ql/src/semmle/code/cpp/ir/implementation/internal/OperandTag.qll", "csharp/ql/src/experimental/ir/implementation/internal/OperandTag.qll" ], - "IR TInstruction":[ + "IR TInstruction": [ "cpp/ql/src/semmle/code/cpp/ir/implementation/internal/TInstruction.qll", "csharp/ql/src/experimental/ir/implementation/internal/TInstruction.qll" ], - "IR TIRVariable":[ + "IR TIRVariable": [ "cpp/ql/src/semmle/code/cpp/ir/implementation/internal/TIRVariable.qll", "csharp/ql/src/experimental/ir/implementation/internal/TIRVariable.qll" ], @@ -381,4 +393,4 @@ "javascript/ql/src/Comments/CommentedOutCodeReferences.qhelp", "python/ql/src/Lexical/CommentedOutCodeReferences.qhelp" ] -} +} \ No newline at end of file diff --git a/csharp/ql/src/Linq/Helpers.qll b/csharp/ql/src/Linq/Helpers.qll index 41d1e305ca6..e1b1beb1222 100644 --- a/csharp/ql/src/Linq/Helpers.qll +++ b/csharp/ql/src/Linq/Helpers.qll @@ -132,6 +132,17 @@ class AnyCall extends MethodCall { } } +/** A LINQ Count(...) call. */ +class CountCall extends MethodCall { + CountCall() { + exists(Method m | + m = getTarget() and + isEnumerableType(m.getDeclaringType()) and + m.hasName("Count") + ) + } +} + /** A variable of type IEnumerable<T>, for some T. */ class IEnumerableSequence extends Variable { IEnumerableSequence() { isIEnumerableType(getType()) } diff --git a/csharp/ql/src/semmle/code/csharp/commons/ComparisonTest.qll b/csharp/ql/src/semmle/code/csharp/commons/ComparisonTest.qll index 5d083679f9d..ea7d250abb0 100644 --- a/csharp/ql/src/semmle/code/csharp/commons/ComparisonTest.qll +++ b/csharp/ql/src/semmle/code/csharp/commons/ComparisonTest.qll @@ -2,7 +2,7 @@ * Provides classes for capturing various ways of performing comparison tests. */ -import csharp +private import csharp private import semmle.code.csharp.frameworks.System private import semmle.code.csharp.frameworks.system.Collections private import semmle.code.csharp.frameworks.system.collections.Generic diff --git a/csharp/ql/src/semmle/code/csharp/controlflow/Guards.qll b/csharp/ql/src/semmle/code/csharp/controlflow/Guards.qll index 89042f7de07..f81b3b09212 100644 --- a/csharp/ql/src/semmle/code/csharp/controlflow/Guards.qll +++ b/csharp/ql/src/semmle/code/csharp/controlflow/Guards.qll @@ -31,6 +31,33 @@ class Guard extends Expr { predicate controlsNode(ControlFlow::Nodes::ElementNode cfn, AccessOrCallExpr sub, AbstractValue v) { isGuardedByNode(cfn, this, sub, v) } + + /** + * Holds if guard is an equality test between `e1` and `e2`. If the test is + * negated, that is `!=`, then `polarity` is false, otherwise `polarity` is + * true. + */ + predicate isEquality(Expr e1, Expr e2, boolean polarity) { + exists(Expr exp1, Expr exp2 | equalityGuard(exp1, exp2, polarity) | + e1 = exp1 and e2 = exp2 + or + e2 = exp1 and e1 = exp2 + ) + } + + private predicate equalityGuard(Expr e1, Expr e2, boolean polarity) { + exists(ComparisonTest eqtest | + eqtest.getExpr() = this and + eqtest.getAnArgument() = e1 and + eqtest.getAnArgument() = e2 and + not e1 = e2 and + ( + polarity = true and eqtest.getComparisonKind().isEquality() + or + polarity = false and eqtest.getComparisonKind().isInequality() + ) + ) + } } /** An abstract value. */ diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/Nullness.qll b/csharp/ql/src/semmle/code/csharp/dataflow/Nullness.qll index a537d08aabc..ed10e700966 100644 --- a/csharp/ql/src/semmle/code/csharp/dataflow/Nullness.qll +++ b/csharp/ql/src/semmle/code/csharp/dataflow/Nullness.qll @@ -21,10 +21,8 @@ import csharp private import ControlFlow private import internal.CallableReturns private import semmle.code.csharp.commons.Assertions -private import semmle.code.csharp.commons.ComparisonTest private import semmle.code.csharp.controlflow.Guards as G private import semmle.code.csharp.controlflow.Guards::AbstractValues -private import semmle.code.csharp.dataflow.SSA private import semmle.code.csharp.frameworks.System private import semmle.code.csharp.frameworks.Test diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/SSA.qll b/csharp/ql/src/semmle/code/csharp/dataflow/SSA.qll index adcfdfaaca7..50a69857d0c 100644 --- a/csharp/ql/src/semmle/code/csharp/dataflow/SSA.qll +++ b/csharp/ql/src/semmle/code/csharp/dataflow/SSA.qll @@ -2537,6 +2537,13 @@ module Ssa { ) } + /** Holds if `inp` is an input to the phi node along the edge originating in `bb`. */ + predicate hasInputFromBlock(Definition inp, BasicBlock bb) { + this.getAnInput() = inp and + this.getBasicBlock().getAPredecessor() = bb and + inp.isLiveAtEndOfBlock(bb) + } + override string toString() { result = getToStringPrefix(this) + "SSA phi(" + getSourceVariable() + ")" } diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/SignAnalysis.qll b/csharp/ql/src/semmle/code/csharp/dataflow/SignAnalysis.qll new file mode 100644 index 00000000000..3742f87de25 --- /dev/null +++ b/csharp/ql/src/semmle/code/csharp/dataflow/SignAnalysis.qll @@ -0,0 +1,9 @@ +/** + * Provides sign analysis to determine whether expression are always positive + * or negative. + * + * The analysis is implemented as an abstract interpretation over the + * three-valued domain `{negative, zero, positive}`. + */ + +import semmle.code.csharp.dataflow.internal.rangeanalysis.SignAnalysisCommon diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/ConstantUtils.qll b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/ConstantUtils.qll new file mode 100644 index 00000000000..e283909155c --- /dev/null +++ b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/ConstantUtils.qll @@ -0,0 +1,64 @@ +/** + * Provides classes and predicates to represent constant integer expressions. + */ + +private import csharp +private import Ssa + +/** + * Holds if property `p` matches `property` in `baseClass` or any overrides. + */ +predicate propertyOverrides(Property p, string baseClass, string property) { + exists(Property p2 | + p2.getSourceDeclaration().getDeclaringType().hasQualifiedName(baseClass) and + p2.hasName(property) + | + p.overridesOrImplementsOrEquals(p2) + ) +} + +/** + * Holds if expression `e` is either + * - a compile time constant with integer value `val`, or + * - a read of a compile time constant with integer value `val`, or + * - a read of the `Length` of an array with `val` lengths. + */ +private predicate constantIntegerExpr(Expr e, int val) { + e.getValue().toInt() = val + or + exists(ExplicitDefinition v, Expr src | + e = v.getARead() and + src = v.getADefinition().getSource() and + constantIntegerExpr(src, val) + ) + or + isArrayLengthAccess(e, val) +} + +private int getArrayLength(ArrayCreation arrCreation, int index) { + constantIntegerExpr(arrCreation.getLengthArgument(index), result) +} + +private int getArrayLengthRec(ArrayCreation arrCreation, int index) { + index = 0 and result = getArrayLength(arrCreation, 0) + or + index > 0 and + result = getArrayLength(arrCreation, index) * getArrayLengthRec(arrCreation, index - 1) +} + +private predicate isArrayLengthAccess(PropertyAccess pa, int length) { + propertyOverrides(pa.getTarget(), "System.Array", "Length") and + exists(ExplicitDefinition arr, ArrayCreation arrCreation | + getArrayLengthRec(arrCreation, arrCreation.getNumberOfLengthArguments() - 1) = length and + arrCreation = arr.getADefinition().getSource() and + pa.getQualifier() = arr.getARead() + ) +} + +/** An expression that always has the same integer value. */ +class ConstantIntegerExpr extends Expr { + ConstantIntegerExpr() { constantIntegerExpr(this, _) } + + /** Gets the integer value of this expression. */ + int getIntValue() { constantIntegerExpr(this, result) } +} diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/Sign.qll b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/Sign.qll new file mode 100644 index 00000000000..10ca946a044 --- /dev/null +++ b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/Sign.qll @@ -0,0 +1,219 @@ +newtype TSign = + TNeg() or + TZero() or + TPos() + +/** Class representing expression signs (+, -, 0). */ +class Sign extends TSign { + /** Gets the string representation of this sign. */ + string toString() { + result = "-" and this = TNeg() + or + result = "0" and this = TZero() + or + result = "+" and this = TPos() + } + + /** Gets a possible sign after incrementing an expression that has this sign. */ + Sign inc() { + this = TNeg() and result = TNeg() + or + this = TNeg() and result = TZero() + or + this = TZero() and result = TPos() + or + this = TPos() and result = TPos() + } + + /** Gets a possible sign after decrementing an expression that has this sign. */ + Sign dec() { result.inc() = this } + + /** Gets a possible sign after negating an expression that has this sign. */ + Sign neg() { + this = TNeg() and result = TPos() + or + this = TZero() and result = TZero() + or + this = TPos() and result = TNeg() + } + + /** + * Gets a possible sign after bitwise complementing an expression that has this + * sign. + */ + Sign bitnot() { + this = TNeg() and result = TPos() + or + this = TNeg() and result = TZero() + or + this = TZero() and result = TNeg() + or + this = TPos() and result = TNeg() + } + + /** + * Gets a possible sign after adding an expression with sign `s` to an expression + * that has this sign. + */ + Sign add(Sign s) { + this = TZero() and result = s + or + s = TZero() and result = this + or + this = s and this = result + or + this = TPos() and s = TNeg() + or + this = TNeg() and s = TPos() + } + + /** + * Gets a possible sign after multiplying an expression with sign `s` to an expression + * that has this sign. + */ + Sign mul(Sign s) { + result = TZero() and this = TZero() + or + result = TZero() and s = TZero() + or + result = TNeg() and this = TPos() and s = TNeg() + or + result = TNeg() and this = TNeg() and s = TPos() + or + result = TPos() and this = TPos() and s = TPos() + or + result = TPos() and this = TNeg() and s = TNeg() + } + + /** + * Gets a possible sign after integer dividing an expression that has this sign + * by an expression with sign `s`. + */ + Sign div(Sign s) { + result = TZero() and s = TNeg() // ex: 3 / -5 = 0 + or + result = TZero() and s = TPos() // ex: 3 / 5 = 0 + or + result = TNeg() and this = TPos() and s = TNeg() + or + result = TNeg() and this = TNeg() and s = TPos() + or + result = TPos() and this = TPos() and s = TPos() + or + result = TPos() and this = TNeg() and s = TNeg() + } + + /** + * Gets a possible sign after modulo dividing an expression that has this sign + * by an expression with sign `s`. + */ + Sign rem(Sign s) { + result = TZero() and s = TNeg() + or + result = TZero() and s = TPos() + or + result = this and s = TNeg() + or + result = this and s = TPos() + } + + /** + * Gets a possible sign after bitwise `and` of an expression that has this sign + * and an expression with sign `s`. + */ + Sign bitand(Sign s) { + result = TZero() and this = TZero() + or + result = TZero() and s = TZero() + or + result = TZero() and this = TPos() + or + result = TZero() and s = TPos() + or + result = TNeg() and this = TNeg() and s = TNeg() + or + result = TPos() and this = TNeg() and s = TPos() + or + result = TPos() and this = TPos() and s = TNeg() + or + result = TPos() and this = TPos() and s = TPos() + } + + /** + * Gets a possible sign after bitwise `or` of an expression that has this sign + * and an expression with sign `s`. + */ + Sign bitor(Sign s) { + result = TZero() and this = TZero() and s = TZero() + or + result = TNeg() and this = TNeg() + or + result = TNeg() and s = TNeg() + or + result = TPos() and this = TPos() and s = TZero() + or + result = TPos() and this = TZero() and s = TPos() + or + result = TPos() and this = TPos() and s = TPos() + } + + /** + * Gets a possible sign after bitwise `xor` of an expression that has this sign + * and an expression with sign `s`. + */ + Sign bitxor(Sign s) { + result = TZero() and this = s + or + result = this and s = TZero() + or + result = s and this = TZero() + or + result = TPos() and this = TPos() and s = TPos() + or + result = TNeg() and this = TNeg() and s = TPos() + or + result = TNeg() and this = TPos() and s = TNeg() + or + result = TPos() and this = TNeg() and s = TNeg() + } + + /** + * Gets a possible sign after left shift of an expression that has this sign + * by an expression with sign `s`. + */ + Sign lshift(Sign s) { + result = TZero() and this = TZero() + or + result = this and s = TZero() + or + this != TZero() and s != TZero() + } + + /** + * Gets a possible sign after right shift of an expression that has this sign + * by an expression with sign `s`. + */ + Sign rshift(Sign s) { + result = TZero() and this = TZero() + or + result = this and s = TZero() + or + result = TNeg() and this = TNeg() + or + result != TNeg() and this = TPos() and s != TZero() + } + + /** + * Gets a possible sign after unsigned right shift of an expression that has + * this sign by an expression with sign `s`. + */ + Sign urshift(Sign s) { + result = TZero() and this = TZero() + or + result = this and s = TZero() + or + result != TZero() and this = TNeg() and s != TZero() + or + result != TNeg() and this = TPos() and s != TZero() + } +} diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SignAnalysisCommon.qll b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SignAnalysisCommon.qll new file mode 100644 index 00000000000..66b38433eef --- /dev/null +++ b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SignAnalysisCommon.qll @@ -0,0 +1,293 @@ +/** + * Provides sign analysis to determine whether expression are always positive + * or negative. + * + * The analysis is implemented as an abstract interpretation over the + * three-valued domain `{negative, zero, positive}`. + */ + +private import SignAnalysisSpecific::Private +private import SsaReadPositionCommon +private import Sign + +/** Gets the sign of `e` if this can be directly determined. */ +Sign certainExprSign(Expr e) { + exists(int i | e.(ConstantIntegerExpr).getIntValue() = i | + i < 0 and result = TNeg() + or + i = 0 and result = TZero() + or + i > 0 and result = TPos() + ) + or + not exists(e.(ConstantIntegerExpr).getIntValue()) and + ( + exists(float f | f = getNonIntegerValue(e) | + f < 0 and result = TNeg() + or + f = 0 and result = TZero() + or + f > 0 and result = TPos() + ) + or + exists(string charlit | charlit = getCharValue(e) | + if charlit.regexpMatch("\\u0000") then result = TZero() else result = TPos() + ) + or + containerSizeAccess(e) and + (result = TPos() or result = TZero()) + or + positiveExpression(e) and result = TPos() + ) +} + +/** Holds if the sign of `e` is too complicated to determine. */ +predicate unknownSign(Expr e) { + not exists(certainExprSign(e)) and + ( + exists(IntegerLiteral lit | lit = e and not exists(lit.getValue().toInt())) + or + exists(LongLiteral lit | lit = e and not exists(lit.getValue().toFloat())) + or + exists(CastExpr cast, Type fromtyp | + cast = e and + fromtyp = cast.getExpr().getType() and + not fromtyp instanceof NumericOrCharType + ) + or + unknownIntegerAccess(e) + ) +} + +/** + * Holds if `lowerbound` is a lower bound for `v` at `pos`. This is restricted + * to only include bounds for which we might determine a sign. + */ +private predicate lowerBound(Expr lowerbound, SsaVariable v, SsaReadPosition pos, boolean isStrict) { + exists(boolean testIsTrue, ComparisonExpr comp | + pos.hasReadOfVar(v) and + guardControlsSsaRead(getComparisonGuard(comp), pos, testIsTrue) and + not unknownSign(lowerbound) + | + testIsTrue = true and + comp.getLesserOperand() = lowerbound and + comp.getGreaterOperand() = ssaRead(v, 0) and + (if comp.isStrict() then isStrict = true else isStrict = false) + or + testIsTrue = false and + comp.getGreaterOperand() = lowerbound and + comp.getLesserOperand() = ssaRead(v, 0) and + (if comp.isStrict() then isStrict = false else isStrict = true) + ) +} + +/** + * Holds if `upperbound` is an upper bound for `v` at `pos`. This is restricted + * to only include bounds for which we might determine a sign. + */ +private predicate upperBound(Expr upperbound, SsaVariable v, SsaReadPosition pos, boolean isStrict) { + exists(boolean testIsTrue, ComparisonExpr comp | + pos.hasReadOfVar(v) and + guardControlsSsaRead(getComparisonGuard(comp), pos, testIsTrue) and + not unknownSign(upperbound) + | + testIsTrue = true and + comp.getGreaterOperand() = upperbound and + comp.getLesserOperand() = ssaRead(v, 0) and + (if comp.isStrict() then isStrict = true else isStrict = false) + or + testIsTrue = false and + comp.getLesserOperand() = upperbound and + comp.getGreaterOperand() = ssaRead(v, 0) and + (if comp.isStrict() then isStrict = false else isStrict = true) + ) +} + +/** + * Holds if `eqbound` is an equality/inequality for `v` at `pos`. This is + * restricted to only include bounds for which we might determine a sign. The + * boolean `isEq` gives the polarity: + * - `isEq = true` : `v = eqbound` + * - `isEq = false` : `v != eqbound` + */ +private predicate eqBound(Expr eqbound, SsaVariable v, SsaReadPosition pos, boolean isEq) { + exists(Guard guard, boolean testIsTrue, boolean polarity | + pos.hasReadOfVar(v) and + guardControlsSsaRead(guard, pos, testIsTrue) and + guard.isEquality(eqbound, ssaRead(v, 0), polarity) and + isEq = polarity.booleanXor(testIsTrue).booleanNot() and + not unknownSign(eqbound) + ) +} + +/** + * Holds if `bound` is a bound for `v` at `pos` that needs to be positive in + * order for `v` to be positive. + */ +private predicate posBound(Expr bound, SsaVariable v, SsaReadPosition pos) { + upperBound(bound, v, pos, _) or + eqBound(bound, v, pos, true) +} + +/** + * Holds if `bound` is a bound for `v` at `pos` that needs to be negative in + * order for `v` to be negative. + */ +private predicate negBound(Expr bound, SsaVariable v, SsaReadPosition pos) { + lowerBound(bound, v, pos, _) or + eqBound(bound, v, pos, true) +} + +/** + * Holds if `bound` is a bound for `v` at `pos` that can restrict whether `v` + * can be zero. + */ +private predicate zeroBound(Expr bound, SsaVariable v, SsaReadPosition pos) { + lowerBound(bound, v, pos, _) or + upperBound(bound, v, pos, _) or + eqBound(bound, v, pos, _) +} + +/** Holds if `bound` allows `v` to be positive at `pos`. */ +private predicate posBoundOk(Expr bound, SsaVariable v, SsaReadPosition pos) { + posBound(bound, v, pos) and TPos() = exprSign(bound) +} + +/** Holds if `bound` allows `v` to be negative at `pos`. */ +private predicate negBoundOk(Expr bound, SsaVariable v, SsaReadPosition pos) { + negBound(bound, v, pos) and TNeg() = exprSign(bound) +} + +/** Holds if `bound` allows `v` to be zero at `pos`. */ +private predicate zeroBoundOk(Expr bound, SsaVariable v, SsaReadPosition pos) { + lowerBound(bound, v, pos, _) and TNeg() = exprSign(bound) + or + lowerBound(bound, v, pos, false) and TZero() = exprSign(bound) + or + upperBound(bound, v, pos, _) and TPos() = exprSign(bound) + or + upperBound(bound, v, pos, false) and TZero() = exprSign(bound) + or + eqBound(bound, v, pos, true) and TZero() = exprSign(bound) + or + eqBound(bound, v, pos, false) and TZero() != exprSign(bound) +} + +/** + * Holds if there is a bound that might restrict whether `v` has the sign `s` + * at `pos`. + */ +private predicate hasGuard(SsaVariable v, SsaReadPosition pos, Sign s) { + s = TPos() and posBound(_, v, pos) + or + s = TNeg() and negBound(_, v, pos) + or + s = TZero() and zeroBound(_, v, pos) +} + +pragma[noinline] +private Sign guardedSsaSign(SsaVariable v, SsaReadPosition pos) { + // SSA variable can have sign `result` + result = ssaDefSign(v) and + pos.hasReadOfVar(v) and + // there are guards at this position on `v` that might restrict it to be sign `result`. + // (So we need to check if they are satisfied) + hasGuard(v, pos, result) +} + +pragma[noinline] +private Sign unguardedSsaSign(SsaVariable v, SsaReadPosition pos) { + // SSA variable can have sign `result` + result = ssaDefSign(v) and + pos.hasReadOfVar(v) and + // there's no guard at this position on `v` that might restrict it to be sign `result`. + not hasGuard(v, pos, result) +} + +/** + * Gets the sign of `v` at read position `pos`, when there's at least one guard + * on `v` at position `pos`. Each bound corresponding to a given sign must be met + * in order for `v` to be of that sign. + */ +private Sign guardedSsaSignOk(SsaVariable v, SsaReadPosition pos) { + result = TPos() and + forex(Expr bound | posBound(bound, v, pos) | posBoundOk(bound, v, pos)) + or + result = TNeg() and + forex(Expr bound | negBound(bound, v, pos) | negBoundOk(bound, v, pos)) + or + result = TZero() and + forex(Expr bound | zeroBound(bound, v, pos) | zeroBoundOk(bound, v, pos)) +} + +/** Gets a possible sign for `v` at `pos`. */ +Sign ssaSign(SsaVariable v, SsaReadPosition pos) { + result = unguardedSsaSign(v, pos) + or + result = guardedSsaSign(v, pos) and + result = guardedSsaSignOk(v, pos) +} + +/** Gets a possible sign for `v`. */ +pragma[nomagic] +Sign ssaDefSign(SsaVariable v) { + result = explicitSsaDefSign(v) + or + result = implicitSsaDefSign(v) + or + exists(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge | + v = phi and + edge.phiInput(phi, inp) and + result = ssaSign(inp, edge) + ) +} + +/** Gets a possible sign for `e`. */ +cached +Sign exprSign(Expr e) { + result = certainExprSign(e) + or + not exists(certainExprSign(e)) and + ( + unknownSign(e) + or + exists(SsaVariable v | getARead(v) = e | result = ssaVariableSign(v, e)) + or + e = + any(VarAccess access | + not exists(SsaVariable v | getARead(v) = access) and + ( + result = fieldSign(getField(access.(FieldAccess))) or + not access instanceof FieldAccess + ) + ) + or + result = specificSubExprSign(e) + ) +} + +/** Holds if `e` can be positive and cannot be negative. */ +predicate positive(Expr e) { + exprSign(e) = TPos() and + not exprSign(e) = TNeg() +} + +/** Holds if `e` can be negative and cannot be positive. */ +predicate negative(Expr e) { + exprSign(e) = TNeg() and + not exprSign(e) = TPos() +} + +/** Holds if `e` is strictly positive. */ +predicate strictlyPositive(Expr e) { + exprSign(e) = TPos() and + not exprSign(e) = TNeg() and + not exprSign(e) = TZero() +} + +/** Holds if `e` is strictly negative. */ +predicate strictlyNegative(Expr e) { + exprSign(e) = TNeg() and + not exprSign(e) = TPos() and + not exprSign(e) = TZero() +} diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll new file mode 100644 index 00000000000..75adec96909 --- /dev/null +++ b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll @@ -0,0 +1,283 @@ +/** + * Provides C#-specific definitions for use in sign analysis. + */ +module Private { + private import SsaUtils as SU + private import csharp as CS + private import ConstantUtils as CU + private import semmle.code.csharp.controlflow.Guards as G + import Impl + + class Guard = G::Guard; + + class ConstantIntegerExpr = CU::ConstantIntegerExpr; + + class SsaVariable = CS::Ssa::Definition; + + class SsaPhiNode = CS::Ssa::PhiNode; + + class VarAccess = CS::AssignableAccess; + + class FieldAccess = CS::FieldAccess; + + class CharacterLiteral = CS::CharLiteral; + + class IntegerLiteral = CS::IntegerLiteral; + + class LongLiteral = CS::LongLiteral; + + class CastExpr = CS::CastExpr; + + class Type = CS::Type; + + class Expr = CS::Expr; + + predicate ssaRead = SU::ssaRead/2; +} + +private module Impl { + private import csharp + private import SsaUtils + private import ConstantUtils + private import semmle.code.csharp.controlflow.Guards + private import Linq.Helpers + private import Sign + private import SignAnalysisCommon + private import SsaReadPositionCommon + private import semmle.code.csharp.commons.ComparisonTest + + private class BooleanValue = AbstractValues::BooleanValue; + + float getNonIntegerValue(Expr e) { + exists(string s | + s = e.getValue() and + result = s.toFloat() and + not exists(s.toInt()) + ) + } + + string getCharValue(Expr e) { result = e.getValue() and e.getType() instanceof CharType } + + predicate containerSizeAccess(Expr e) { + exists(Property p | p = e.(PropertyAccess).getTarget() | + propertyOverrides(p, "System.Collections.Generic.IEnumerable<>", "Count") or + propertyOverrides(p, "System.Collections.ICollection", "Count") or + propertyOverrides(p, "System.String", "Length") or + propertyOverrides(p, "System.Array", "Length") + ) + or + e instanceof CountCall + } + + predicate positiveExpression(Expr e) { e instanceof SizeofExpr } + + class NumericOrCharType extends Type { + NumericOrCharType() { + this instanceof CharType or + this instanceof IntegralType or + this instanceof FloatingPointType or + this instanceof DecimalType or + this instanceof Enum or + this instanceof PointerType // should be similar to unsigned integers + } + } + + Sign explicitSsaDefSign(Ssa::ExplicitDefinition v) { + exists(AssignableDefinition def | def = v.getADefinition() | + result = exprSign(def.getSource()) + or + not exists(def.getSource()) and + not def.getElement() instanceof MutatorOperation + or + result = exprSign(def.getElement().(IncrementOperation).getOperand()).inc() + or + result = exprSign(def.getElement().(DecrementOperation).getOperand()).dec() + ) + } + + Sign implicitSsaDefSign(Ssa::ImplicitDefinition v) { + result = fieldSign(v.getSourceVariable().getAssignable()) or + not v.getSourceVariable().getAssignable() instanceof Field + } + + pragma[inline] + Sign ssaVariableSign(Ssa::Definition v, Expr e) { + result = ssaSign(v, any(SsaReadPositionBlock bb | getAnExpression(bb) = e)) + } + + /** Gets a possible sign for `f`. */ + Sign fieldSign(Field f) { + if f.fromSource() and f.isEffectivelyPrivate() + then + result = exprSign(f.getAnAssignedValue()) + or + any(IncrementOperation inc).getOperand() = f.getAnAccess() and result = fieldSign(f).inc() + or + any(DecrementOperation dec).getOperand() = f.getAnAccess() and result = fieldSign(f).dec() + or + exists(AssignOperation a | a.getLValue() = f.getAnAccess() | result = exprSign(a)) + or + not exists(f.getInitializer()) and result = TZero() + else any() + } + + predicate unknownIntegerAccess(Expr e) { + e.getType() instanceof NumericOrCharType and + not e = getARead(_) and + not e instanceof FieldAccess and + // The expression types that are listed here are the ones handled in `specificSubExprSign`. + // Keep them in sync. + not e instanceof AssignExpr and + not e instanceof AssignOperation and + not e instanceof UnaryPlusExpr and + not e instanceof PostIncrExpr and + not e instanceof PostDecrExpr and + not e instanceof PreIncrExpr and + not e instanceof PreDecrExpr and + not e instanceof UnaryMinusExpr and + not e instanceof ComplementExpr and + not e instanceof AddExpr and + not e instanceof SubExpr and + not e instanceof MulExpr and + not e instanceof DivExpr and + not e instanceof RemExpr and + not e instanceof BitwiseAndExpr and + not e instanceof BitwiseOrExpr and + not e instanceof BitwiseXorExpr and + not e instanceof LShiftExpr and + not e instanceof RShiftExpr and + not e instanceof ConditionalExpr and + not e instanceof RefExpr and + not e instanceof LocalVariableDeclAndInitExpr and + not e instanceof SwitchCaseExpr and + not e instanceof CastExpr and + not e instanceof SwitchExpr and + not e instanceof NullCoalescingExpr + } + + Sign specificSubExprSign(Expr e) { + // The expression types that are handled here should be excluded in `unknownIntegerAccess`. + // Keep them in sync. + result = exprSign(e.(AssignExpr).getRValue()) + or + result = exprSign(e.(AssignOperation).getExpandedAssignment()) + or + result = exprSign(e.(UnaryPlusExpr).getOperand()) + or + result = exprSign(e.(PostIncrExpr).getOperand()) + or + result = exprSign(e.(PostDecrExpr).getOperand()) + or + result = exprSign(e.(PreIncrExpr).getOperand()).inc() + or + result = exprSign(e.(PreDecrExpr).getOperand()).dec() + or + result = exprSign(e.(UnaryMinusExpr).getOperand()).neg() + or + result = exprSign(e.(ComplementExpr).getOperand()).bitnot() + or + e = + any(DivExpr div | + result = exprSign(div.getLeftOperand()) and + result != TZero() and + div.getRightOperand().(RealLiteral).getValue().toFloat() = 0 + ) + or + exists(Sign s1, Sign s2 | binaryOpSigns(e, s1, s2) | + e instanceof AddExpr and result = s1.add(s2) + or + e instanceof SubExpr and result = s1.add(s2.neg()) + or + e instanceof MulExpr and result = s1.mul(s2) + or + e instanceof DivExpr and result = s1.div(s2) + or + e instanceof RemExpr and result = s1.rem(s2) + or + e instanceof BitwiseAndExpr and result = s1.bitand(s2) + or + e instanceof BitwiseOrExpr and result = s1.bitor(s2) + or + e instanceof BitwiseXorExpr and result = s1.bitxor(s2) + or + e instanceof LShiftExpr and result = s1.lshift(s2) + or + e instanceof RShiftExpr and result = s1.rshift(s2) + ) + or + result = exprSign(e.(ConditionalExpr).getAChild()) + or + result = exprSign(e.(NullCoalescingExpr).getAChild()) + or + result = exprSign(e.(SwitchExpr).getACase().getBody()) + or + result = exprSign(e.(CastExpr).getExpr()) + or + result = exprSign(e.(SwitchCaseExpr).getBody()) + or + result = exprSign(e.(LocalVariableDeclAndInitExpr).getInitializer()) + or + result = exprSign(e.(RefExpr).getExpr()) + } + + private Sign binaryOpLhsSign(BinaryOperation e) { result = exprSign(e.getLeftOperand()) } + + private Sign binaryOpRhsSign(BinaryOperation e) { result = exprSign(e.getRightOperand()) } + + pragma[noinline] + private predicate binaryOpSigns(Expr e, Sign lhs, Sign rhs) { + lhs = binaryOpLhsSign(e) and + rhs = binaryOpRhsSign(e) + } + + Expr getARead(Ssa::Definition v) { result = v.getARead() } + + Field getField(FieldAccess fa) { result = fa.getTarget() } + + Expr getAnExpression(SsaReadPositionBlock bb) { result = bb.getBlock().getANode().getElement() } + + Guard getComparisonGuard(ComparisonExpr ce) { result = ce.getExpr() } + + /** + * Holds if `guard` controls the position `controlled` with the value `testIsTrue`. + */ + predicate guardControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) { + exists(BooleanValue b | b.getValue() = testIsTrue | + guard.controlsNode(controlled.(SsaReadPositionBlock).getBlock().getANode(), _, b) + ) + } + + /** A relational comparison */ + class ComparisonExpr extends ComparisonTest { + private boolean strict; + + ComparisonExpr() { + this.getComparisonKind() = + any(ComparisonKind ck | + ck.isLessThan() and strict = true + or + ck.isLessThanEquals() and + strict = false + ) + } + + /** + * Gets the operand on the "greater" (or "greater-or-equal") side + * of this relational expression, that is, the side that is larger + * if the overall expression evaluates to `true`; for example on + * `x <= 20` this is the `20`, and on `y > 0` it is `y`. + */ + Expr getGreaterOperand() { result = this.getSecondArgument() } + + /** + * Gets the operand on the "lesser" (or "lesser-or-equal") side + * of this relational expression, that is, the side that is smaller + * if the overall expression evaluates to `true`; for example on + * `x <= 20` this is `x`, and on `y > 0` it is the `0`. + */ + Expr getLesserOperand() { result = this.getFirstArgument() } + + /** Holds if this comparison is strict, i.e. `<` or `>`. */ + predicate isStrict() { strict = true } + } +} diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaReadPositionCommon.qll b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaReadPositionCommon.qll new file mode 100644 index 00000000000..558ecd1b88b --- /dev/null +++ b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaReadPositionCommon.qll @@ -0,0 +1,57 @@ +/** + * Provides classes for representing a position at which an SSA variable is read. + */ + +private import SsaReadPositionSpecific + +private newtype TSsaReadPosition = + TSsaReadPositionBlock(BasicBlock bb) { bb = getAReadBasicBlock(_) } or + TSsaReadPositionPhiInputEdge(BasicBlock bbOrig, BasicBlock bbPhi) { + exists(SsaPhiNode phi | phi.hasInputFromBlock(_, bbOrig) and bbPhi = phi.getBasicBlock()) + } + +/** + * A position at which an SSA variable is read. This includes both ordinary + * reads occurring in basic blocks and input to phi nodes occurring along an + * edge between two basic blocks. + */ +class SsaReadPosition extends TSsaReadPosition { + /** Holds if `v` is read at this position. */ + abstract predicate hasReadOfVar(SsaVariable v); + + /** Gets a textual representation of this SSA read position. */ + abstract string toString(); +} + +/** A basic block in which an SSA variable is read. */ +class SsaReadPositionBlock extends SsaReadPosition, TSsaReadPositionBlock { + /** Gets the basic block corresponding to this position. */ + BasicBlock getBlock() { this = TSsaReadPositionBlock(result) } + + override predicate hasReadOfVar(SsaVariable v) { getBlock() = getAReadBasicBlock(v) } + + override string toString() { result = "block" } +} + +/** + * An edge between two basic blocks where the latter block has an SSA phi + * definition. The edge therefore has a read of an SSA variable serving as the + * input to the phi node. + */ +class SsaReadPositionPhiInputEdge extends SsaReadPosition, TSsaReadPositionPhiInputEdge { + /** Gets the source of the edge. */ + BasicBlock getOrigBlock() { this = TSsaReadPositionPhiInputEdge(result, _) } + + /** Gets the target of the edge. */ + BasicBlock getPhiBlock() { this = TSsaReadPositionPhiInputEdge(_, result) } + + override predicate hasReadOfVar(SsaVariable v) { this.phiInput(_, v) } + + /** Holds if `inp` is an input to `phi` along this edge. */ + predicate phiInput(SsaPhiNode phi, SsaVariable inp) { + phi.hasInputFromBlock(inp, getOrigBlock()) and + getPhiBlock() = phi.getBasicBlock() + } + + override string toString() { result = "edge" } +} diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaReadPositionSpecific.qll b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaReadPositionSpecific.qll new file mode 100644 index 00000000000..d7df9781b2a --- /dev/null +++ b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaReadPositionSpecific.qll @@ -0,0 +1,16 @@ +/** + * Provides C#-specific definitions for use in the `SsaReadPosition`. + */ + +private import csharp + +class SsaVariable = Ssa::Definition; + +class SsaPhiNode = Ssa::PhiNode; + +class BasicBlock = Ssa::BasicBlock; + +/** Gets a basic block in which SSA variable `v` is read. */ +BasicBlock getAReadBasicBlock(SsaVariable v) { + result = v.getARead().getAControlFlowNode().getBasicBlock() +} diff --git a/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaUtils.qll b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaUtils.qll new file mode 100644 index 00000000000..7f1811c1f37 --- /dev/null +++ b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaUtils.qll @@ -0,0 +1,42 @@ +/** + * Provides utility predicates to extend the core SSA functionality. + */ + +private import csharp +private import Ssa +private import ConstantUtils + +/** + * Gets an expression that equals `v - delta`. + */ +Expr ssaRead(Definition v, int delta) { + result = v.getARead() and delta = 0 + or + exists(AddExpr add, int d1, ConstantIntegerExpr c | + result = add and + delta = d1 - c.getIntValue() + | + add.getLeftOperand() = ssaRead(v, d1) and add.getRightOperand() = c + or + add.getRightOperand() = ssaRead(v, d1) and add.getLeftOperand() = c + ) + or + exists(SubExpr sub, int d1, ConstantIntegerExpr c | + result = sub and + sub.getLeftOperand() = ssaRead(v, d1) and + sub.getRightOperand() = c and + delta = d1 + c.getIntValue() + ) + or + v.(ExplicitDefinition).getADefinition().getExpr().(PreIncrExpr) = result and delta = 0 + or + v.(ExplicitDefinition).getADefinition().getExpr().(PreDecrExpr) = result and delta = 0 + or + v.(ExplicitDefinition).getADefinition().getExpr().(PostIncrExpr) = result and delta = 1 // x++ === ++x - 1 + or + v.(ExplicitDefinition).getADefinition().getExpr().(PostDecrExpr) = result and delta = -1 // x-- === --x + 1 + or + v.(ExplicitDefinition).getADefinition().getExpr().(Assignment) = result and delta = 0 + or + result.(AssignExpr).getRValue() = ssaRead(v, delta) +} diff --git a/csharp/ql/src/semmle/code/csharp/exprs/ComparisonOperation.qll b/csharp/ql/src/semmle/code/csharp/exprs/ComparisonOperation.qll index e48aabd76a7..8b94ef5b4d7 100644 --- a/csharp/ql/src/semmle/code/csharp/exprs/ComparisonOperation.qll +++ b/csharp/ql/src/semmle/code/csharp/exprs/ComparisonOperation.qll @@ -57,6 +57,9 @@ class RelationalOperation extends ComparisonOperation, @rel_op_expr { * `x <= 20` this is `x`, and on `y > 0` it is the `0`. */ Expr getLesserOperand() { none() } + + /** Holds if this comparison is strict, i.e. `<` or `>`. */ + predicate isStrict() { this instanceof LTExpr or this instanceof GTExpr } } /** diff --git a/csharp/ql/test/library-tests/dataflow/signanalysis/MissingSign.expected b/csharp/ql/test/library-tests/dataflow/signanalysis/MissingSign.expected new file mode 100644 index 00000000000..72f1bdadeda --- /dev/null +++ b/csharp/ql/test/library-tests/dataflow/signanalysis/MissingSign.expected @@ -0,0 +1,4 @@ +| SignAnalysis.cs:428:23:428:24 | access to constant A | +| SignAnalysis.cs:448:22:448:29 | Byte* to = ... | +| SignAnalysis.cs:450:38:450:44 | (...) ... | +| SignAnalysis.cs:450:43:450:44 | access to local variable to | diff --git a/csharp/ql/test/library-tests/dataflow/signanalysis/MissingSign.ql b/csharp/ql/test/library-tests/dataflow/signanalysis/MissingSign.ql new file mode 100644 index 00000000000..b769f3eff6e --- /dev/null +++ b/csharp/ql/test/library-tests/dataflow/signanalysis/MissingSign.ql @@ -0,0 +1,15 @@ +import csharp +import semmle.code.csharp.dataflow.SignAnalysis + +from Expr e +where + not exists(exprSign(e)) and + ( + e.getType() instanceof CharType or + e.getType() instanceof IntegralType or + e.getType() instanceof FloatingPointType or + e.getType() instanceof DecimalType or + e.getType() instanceof Enum or + e.getType() instanceof PointerType + ) +select e diff --git a/csharp/ql/test/library-tests/dataflow/signanalysis/SignAnalysis.cs b/csharp/ql/test/library-tests/dataflow/signanalysis/SignAnalysis.cs new file mode 100644 index 00000000000..13a94a18aae --- /dev/null +++ b/csharp/ql/test/library-tests/dataflow/signanalysis/SignAnalysis.cs @@ -0,0 +1,455 @@ +using System; +using System.Linq; +using System.Diagnostics; + +class SignAnalysis +{ + static int GetRandomValue() { return (new System.Random()).Next(0, 1000) - 500; } + + int RandomValue { get => GetRandomValue(); } + + int random = GetRandomValue(); + + int SsaSources(int p, int[] values) + { + var v = GetRandomValue(); + if (v < 0) + { + return v; + } + + v = RandomValue; + if (v < 0) + { + return v; + } + + v = p; + if (v < 0) + { + return v; + } + + v = random; + if (v < 0) + { + return v; + } + + v = values[0]; + if (v < 0) + { + return v; + } + + int x = values[1]; + v = x; + if (v < 0) + { + return v; + } + + return 0; + } + + void Operations(int i, int j, bool b) + { + if (i < 0 && j < 0) + { + var x = i + j; + System.Console.WriteLine(x); // strictly neg + x = i * j; + System.Console.WriteLine(x); // strictly pos + x = i / j; + System.Console.WriteLine(x); // pos + x = i - j; + System.Console.WriteLine(x); // no clue + x = i % j; + System.Console.WriteLine(x); // neg + x = i++; + System.Console.WriteLine(x); // strictly neg + x = i--; + System.Console.WriteLine(x); // neg + x = -i; + System.Console.WriteLine(x); // strictly pos + x = +i; + System.Console.WriteLine(x); // strictly neg + var l = (long)i; + System.Console.WriteLine(l); // strictly neg + + x = i; + x += i; + System.Console.WriteLine(x); // strictly neg + } + + if (i < 0 && j > 0) + { + var x = i + j; + System.Console.WriteLine(x); + x = i * j; + System.Console.WriteLine(x); // strictly neg + x = i / j; + System.Console.WriteLine(x); // neg + x = i - j; + System.Console.WriteLine(x); // strictly neg + x = i % j; + System.Console.WriteLine(x); // neg + x = b ? i : j; + System.Console.WriteLine(x); // any (except 0) + } + } + + void NumericalTypes() + { + var f = 4.2f; + System.Console.WriteLine(f); + var d = 4.2; + System.Console.WriteLine(d); + var de = 4.2m; + System.Console.WriteLine(de); + var c = 'a'; + System.Console.WriteLine(c); + } + + int f0; + + int f1; + + void Field0() + { + f0++; + System.Console.WriteLine(f0); // strictly positive + f0 = 0; + } + + void Field1() + { + f1++; + System.Console.WriteLine(f1); // no clue + f1 = -10; + } + + void Field2() + { + System.Console.WriteLine(f1); // no clue + } + + void Ctor() + { + var i = new Int32(); // const 0 value + i++; + System.Console.WriteLine(i); // strictly pos + } + + int Guards(int x, int y) + { + if (x < 0) + { + return x; // strictly negative + } + + if (y == 1) + { + return y; // strictly positive + } + + if (y is -1) + { + return y; // strictly negative [MISSING] + } + + if (x < y) + { + return y; // strictly positive + } + + var b = y == 1; + if (b) + { + return y; // strictly positive + } + + return 0; + } + + void Inconsistent() + { + var i = 1; + if (i < 0) + { + System.Console.WriteLine(i); // reported as strictly pos, although unreachable + } + } + + void SpecialValues(int[] ints) + { + System.Console.WriteLine(ints.Length); // positive + ints = new int[] { 1, 2, 3 }; + System.Console.WriteLine(ints.Length); // 3, so strictly positive + System.Console.WriteLine(ints.Count()); // positive + System.Console.WriteLine(ints.Count(i => i > 1)); // positive + + var s = "abc"; + System.Console.WriteLine(s.Length); // positive, could be strictly positive + + var enumerable = Enumerable.Empty(); + System.Console.WriteLine(enumerable.Count()); // positive + + var i = new int[,] { { 1, 1 }, { 1, 2 }, { 1, 3 } }; + System.Console.WriteLine(i.Length); // 6, so strictly positive + } + + void Phi1(int i) + { + if (i > 0) + { + System.Console.WriteLine(i); // strictly positive + } + else + { + System.Console.WriteLine(i); // negative + } + System.Console.WriteLine(i); // any + } + + void Phi2(int i) + { + if (i > 0) + { + System.Console.WriteLine(i); // strictly positive + } + else + { + if (i < 0) // negative + { + System.Console.WriteLine(i); // strictly negative + return; + } + } + System.Console.WriteLine(i); // positive, not found + } + + void Phi3(int i) + { + if (i > 0) + { + System.Console.WriteLine(i); // strictly positive + } + else + { + if (i < 0) // negative + { + System.Console.WriteLine(i); // strictly negative + } + else + { + System.Console.WriteLine(i); // zero, nothing is reported + } + } + } + + void Loop(int i, int j, int k) + { + if (i > 0) + { + while (i >= 0) // any + { + i--; // positive + System.Console.WriteLine(i); // any + } + System.Console.WriteLine(i); // strictly neg + } + + if (j > 0) + { + while (j > 0) + { + j--; // strictly pos + System.Console.WriteLine(j); // positive + } + System.Console.WriteLine(j); // reported negative, can only be 0 + } + + if (k > 0) + { + while (k > 0) + { + k--; // strictly pos + System.Console.WriteLine(k); // positive + + if (k == 5) // positive + { + break; + } + } + System.Console.WriteLine(k); // any + } + } + + void Assert(int i, bool b) + { + Debug.Assert(i > 0); + System.Console.WriteLine(i); // strictly positive + + if (b) + System.Console.WriteLine(i); // strictly positive + } + + void CheckedUnchecked(int i) + { + var x = unchecked(-1 * i * i); + if (x < 0) + { + System.Console.WriteLine(x); // strictly negative + } + + x = checked(-1 * i * i); + if (x < 0) + { + System.Console.WriteLine(x); // strictly negative + } + } + + void CharMinMax() + { + var min = char.MinValue; + var max = char.MaxValue; + var c = min + 1; + System.Console.WriteLine(c); // strictly positive + c = min - 1; + System.Console.WriteLine(c); // strictly negative + c = max + 1; + System.Console.WriteLine(c); // strictly positive + } + + void NullCoalesce(int? v) + { + if (v > 0) + { + var x = v ?? 1; + System.Console.WriteLine(x); // strictly positive + } + + if (v == null) + { + var x = v ?? 1; + System.Console.WriteLine(x); // strictly positive + } + + if (v < 0) + { + var x = v ?? 0; + System.Console.WriteLine(x); // negative + } + } + + async System.Threading.Tasks.Task Await() + { + var i = await System.Threading.Tasks.Task.FromResult(5); + if (i < 0) + { + System.Console.WriteLine(i); // strictly negative + } + } + + void Unsigned(uint i) + { + if (i != 0) // positive + { + System.Console.WriteLine(i); // strictly positive + } + } + + public int MyField = 0; + + void FieldAccess() + { + var x = new SignAnalysis(); + var y = x.MyField; + if (y < 0) + { + System.Console.WriteLine(y); // strictly negative + } + } + + private static unsafe void Pointer(float d) + { + float* dp = &d; + var x = *dp; + if (x < 0) + { + System.Console.WriteLine(x); // strictly negative + } + } + + [System.Runtime.InteropServices.StructLayout(System.Runtime.InteropServices.LayoutKind.Explicit, Size = 15)] + struct MyStruct { } + + unsafe void Sizeof() + { + var x = sizeof(MyStruct); + System.Console.WriteLine(x); // strictly positive + } + + void SwitchCase(string s) + { + var x = s switch + { + "x" => 0, + _ => 2 + }; + System.Console.WriteLine(x); // positive + } + + void Capture() + { + var i = 1; + void Capture() + { + if (i > 0) + Console.WriteLine(i); // strictly positive + } + Capture(); + + if (i > 0) + Console.WriteLine(i); // strictly positive + } + + public struct MyStruct2 { public int F; } + void RefExpression(MyStruct2 s) + { + ref var x = ref s.F; + if (x < 0) + { + Console.WriteLine(x); // strictly negative + } + } + + enum MyEnum { A = 12, B, C } + void EnumOp(MyEnum x, MyEnum y) + { + var i = x - y; + if (i < 0) + { + System.Console.WriteLine(i); // strictly negative + } + } + + unsafe void PointerCast(byte* src, byte* dst) + { + var x = (int)(src-dst); + if (x < 0) + { + System.Console.WriteLine(x); // strictly negative + } + + byte[] buf = new byte[10]; + + fixed (byte* to = buf) + { + System.Console.WriteLine((int)to); + } + } +} + +// semmle-extractor-options: /r:System.Linq.dll \ No newline at end of file diff --git a/csharp/ql/test/library-tests/dataflow/signanalysis/SignAnalysis.expected b/csharp/ql/test/library-tests/dataflow/signanalysis/SignAnalysis.expected new file mode 100644 index 00000000000..91d429a45ef --- /dev/null +++ b/csharp/ql/test/library-tests/dataflow/signanalysis/SignAnalysis.expected @@ -0,0 +1,217 @@ +| SignAnalysis.cs:7:72:7:75 | 1000 | strictlyPositive | +| SignAnalysis.cs:7:80:7:82 | 500 | strictlyPositive | +| SignAnalysis.cs:18:20:18:20 | access to local variable v | strictlyNegative | +| SignAnalysis.cs:24:20:24:20 | access to local variable v | strictlyNegative | +| SignAnalysis.cs:30:20:30:20 | access to local variable v | strictlyNegative | +| SignAnalysis.cs:36:20:36:20 | access to local variable v | strictlyNegative | +| SignAnalysis.cs:42:20:42:20 | access to local variable v | strictlyNegative | +| SignAnalysis.cs:45:24:45:24 | 1 | strictlyPositive | +| SignAnalysis.cs:49:20:49:20 | access to local variable v | strictlyNegative | +| SignAnalysis.cs:59:17:59:25 | Int32 x = ... | strictlyNegative | +| SignAnalysis.cs:59:21:59:21 | access to parameter i | strictlyNegative | +| SignAnalysis.cs:59:21:59:25 | ... + ... | strictlyNegative | +| SignAnalysis.cs:59:25:59:25 | access to parameter j | strictlyNegative | +| SignAnalysis.cs:60:38:60:38 | access to local variable x | strictlyNegative | +| SignAnalysis.cs:61:13:61:21 | ... = ... | strictlyPositive | +| SignAnalysis.cs:61:17:61:17 | access to parameter i | strictlyNegative | +| SignAnalysis.cs:61:17:61:21 | ... * ... | strictlyPositive | +| SignAnalysis.cs:61:21:61:21 | access to parameter j | strictlyNegative | +| SignAnalysis.cs:62:38:62:38 | access to local variable x | strictlyPositive | +| SignAnalysis.cs:63:13:63:21 | ... = ... | positive | +| SignAnalysis.cs:63:17:63:17 | access to parameter i | strictlyNegative | +| SignAnalysis.cs:63:17:63:21 | ... / ... | positive | +| SignAnalysis.cs:63:21:63:21 | access to parameter j | strictlyNegative | +| SignAnalysis.cs:64:38:64:38 | access to local variable x | positive | +| SignAnalysis.cs:65:17:65:17 | access to parameter i | strictlyNegative | +| SignAnalysis.cs:65:21:65:21 | access to parameter j | strictlyNegative | +| SignAnalysis.cs:67:13:67:21 | ... = ... | negative | +| SignAnalysis.cs:67:17:67:17 | access to parameter i | strictlyNegative | +| SignAnalysis.cs:67:17:67:21 | ... % ... | negative | +| SignAnalysis.cs:67:21:67:21 | access to parameter j | strictlyNegative | +| SignAnalysis.cs:68:38:68:38 | access to local variable x | negative | +| SignAnalysis.cs:69:13:69:19 | ... = ... | strictlyNegative | +| SignAnalysis.cs:69:17:69:17 | access to parameter i | strictlyNegative | +| SignAnalysis.cs:69:17:69:19 | ...++ | strictlyNegative | +| SignAnalysis.cs:70:38:70:38 | access to local variable x | strictlyNegative | +| SignAnalysis.cs:71:13:71:19 | ... = ... | negative | +| SignAnalysis.cs:71:17:71:17 | access to parameter i | negative | +| SignAnalysis.cs:71:17:71:19 | ...-- | negative | +| SignAnalysis.cs:72:38:72:38 | access to local variable x | negative | +| SignAnalysis.cs:73:13:73:18 | ... = ... | strictlyPositive | +| SignAnalysis.cs:73:17:73:18 | -... | strictlyPositive | +| SignAnalysis.cs:73:18:73:18 | access to parameter i | strictlyNegative | +| SignAnalysis.cs:74:38:74:38 | access to local variable x | strictlyPositive | +| SignAnalysis.cs:75:13:75:18 | ... = ... | strictlyNegative | +| SignAnalysis.cs:75:17:75:18 | +... | strictlyNegative | +| SignAnalysis.cs:75:18:75:18 | access to parameter i | strictlyNegative | +| SignAnalysis.cs:76:38:76:38 | access to local variable x | strictlyNegative | +| SignAnalysis.cs:77:17:77:27 | Int64 l = ... | strictlyNegative | +| SignAnalysis.cs:77:21:77:27 | (...) ... | strictlyNegative | +| SignAnalysis.cs:77:27:77:27 | access to parameter i | strictlyNegative | +| SignAnalysis.cs:78:38:78:38 | access to local variable l | strictlyNegative | +| SignAnalysis.cs:80:13:80:17 | ... = ... | strictlyNegative | +| SignAnalysis.cs:80:17:80:17 | access to parameter i | strictlyNegative | +| SignAnalysis.cs:81:13:81:13 | access to local variable x | strictlyNegative | +| SignAnalysis.cs:81:13:81:18 | ... + ... | strictlyNegative | +| SignAnalysis.cs:81:13:81:18 | ... += ... | strictlyNegative | +| SignAnalysis.cs:81:13:81:18 | ... = ... | strictlyNegative | +| SignAnalysis.cs:81:18:81:18 | access to parameter i | strictlyNegative | +| SignAnalysis.cs:82:38:82:38 | access to local variable x | strictlyNegative | +| SignAnalysis.cs:87:21:87:21 | access to parameter i | strictlyNegative | +| SignAnalysis.cs:87:25:87:25 | access to parameter j | strictlyPositive | +| SignAnalysis.cs:89:13:89:21 | ... = ... | strictlyNegative | +| SignAnalysis.cs:89:17:89:17 | access to parameter i | strictlyNegative | +| SignAnalysis.cs:89:17:89:21 | ... * ... | strictlyNegative | +| SignAnalysis.cs:89:21:89:21 | access to parameter j | strictlyPositive | +| SignAnalysis.cs:90:38:90:38 | access to local variable x | strictlyNegative | +| SignAnalysis.cs:91:13:91:21 | ... = ... | negative | +| SignAnalysis.cs:91:17:91:17 | access to parameter i | strictlyNegative | +| SignAnalysis.cs:91:17:91:21 | ... / ... | negative | +| SignAnalysis.cs:91:21:91:21 | access to parameter j | strictlyPositive | +| SignAnalysis.cs:92:38:92:38 | access to local variable x | negative | +| SignAnalysis.cs:93:13:93:21 | ... = ... | strictlyNegative | +| SignAnalysis.cs:93:17:93:17 | access to parameter i | strictlyNegative | +| SignAnalysis.cs:93:17:93:21 | ... - ... | strictlyNegative | +| SignAnalysis.cs:93:21:93:21 | access to parameter j | strictlyPositive | +| SignAnalysis.cs:94:38:94:38 | access to local variable x | strictlyNegative | +| SignAnalysis.cs:95:13:95:21 | ... = ... | negative | +| SignAnalysis.cs:95:17:95:17 | access to parameter i | strictlyNegative | +| SignAnalysis.cs:95:17:95:21 | ... % ... | negative | +| SignAnalysis.cs:95:21:95:21 | access to parameter j | strictlyPositive | +| SignAnalysis.cs:96:38:96:38 | access to local variable x | negative | +| SignAnalysis.cs:97:21:97:21 | access to parameter i | strictlyNegative | +| SignAnalysis.cs:97:25:97:25 | access to parameter j | strictlyPositive | +| SignAnalysis.cs:104:13:104:20 | Single f = ... | strictlyPositive | +| SignAnalysis.cs:104:17:104:20 | 4.2 | strictlyPositive | +| SignAnalysis.cs:105:34:105:34 | access to local variable f | strictlyPositive | +| SignAnalysis.cs:106:13:106:19 | Double d = ... | strictlyPositive | +| SignAnalysis.cs:106:17:106:19 | 4.2 | strictlyPositive | +| SignAnalysis.cs:107:34:107:34 | access to local variable d | strictlyPositive | +| SignAnalysis.cs:108:13:108:21 | Decimal de = ... | strictlyPositive | +| SignAnalysis.cs:108:18:108:21 | 4.2 | strictlyPositive | +| SignAnalysis.cs:109:34:109:35 | access to local variable de | strictlyPositive | +| SignAnalysis.cs:110:13:110:19 | Char c = ... | strictlyPositive | +| SignAnalysis.cs:110:17:110:19 | a | strictlyPositive | +| SignAnalysis.cs:111:34:111:34 | access to local variable c | strictlyPositive | +| SignAnalysis.cs:120:9:120:10 | access to field f0 | positive | +| SignAnalysis.cs:120:9:120:12 | ...++ | positive | +| SignAnalysis.cs:121:34:121:35 | access to field f0 | strictlyPositive | +| SignAnalysis.cs:122:9:122:10 | access to field f0 | positive | +| SignAnalysis.cs:129:9:129:16 | ... = ... | strictlyNegative | +| SignAnalysis.cs:129:14:129:16 | -... | strictlyNegative | +| SignAnalysis.cs:129:15:129:16 | 10 | strictlyPositive | +| SignAnalysis.cs:141:34:141:34 | access to local variable i | strictlyPositive | +| SignAnalysis.cs:148:20:148:20 | access to parameter x | strictlyNegative | +| SignAnalysis.cs:151:18:151:18 | 1 | strictlyPositive | +| SignAnalysis.cs:153:20:153:20 | access to parameter y | strictlyPositive | +| SignAnalysis.cs:156:18:156:19 | -... | strictlyNegative | +| SignAnalysis.cs:156:19:156:19 | 1 | strictlyPositive | +| SignAnalysis.cs:161:13:161:13 | access to parameter x | positive | +| SignAnalysis.cs:163:20:163:20 | access to parameter y | strictlyPositive | +| SignAnalysis.cs:166:22:166:22 | 1 | strictlyPositive | +| SignAnalysis.cs:169:20:169:20 | access to parameter y | strictlyPositive | +| SignAnalysis.cs:177:13:177:17 | Int32 i = ... | strictlyPositive | +| SignAnalysis.cs:177:17:177:17 | 1 | strictlyPositive | +| SignAnalysis.cs:178:13:178:13 | access to local variable i | strictlyPositive | +| SignAnalysis.cs:180:38:180:38 | access to local variable i | strictlyPositive | +| SignAnalysis.cs:186:34:186:44 | access to property Length | positive | +| SignAnalysis.cs:187:16:187:36 | 3 | strictlyPositive | +| SignAnalysis.cs:187:28:187:28 | 1 | strictlyPositive | +| SignAnalysis.cs:187:31:187:31 | 2 | strictlyPositive | +| SignAnalysis.cs:187:34:187:34 | 3 | strictlyPositive | +| SignAnalysis.cs:188:34:188:44 | access to property Length | strictlyPositive | +| SignAnalysis.cs:189:34:189:45 | call to method Count | positive | +| SignAnalysis.cs:190:34:190:55 | call to method Count | positive | +| SignAnalysis.cs:190:54:190:54 | 1 | strictlyPositive | +| SignAnalysis.cs:193:34:193:41 | access to property Length | positive | +| SignAnalysis.cs:196:34:196:51 | call to method Count | positive | +| SignAnalysis.cs:198:17:198:59 | 2 | strictlyPositive | +| SignAnalysis.cs:198:17:198:59 | 3 | strictlyPositive | +| SignAnalysis.cs:198:32:198:32 | 1 | strictlyPositive | +| SignAnalysis.cs:198:35:198:35 | 1 | strictlyPositive | +| SignAnalysis.cs:198:42:198:42 | 1 | strictlyPositive | +| SignAnalysis.cs:198:45:198:45 | 2 | strictlyPositive | +| SignAnalysis.cs:198:52:198:52 | 1 | strictlyPositive | +| SignAnalysis.cs:198:55:198:55 | 3 | strictlyPositive | +| SignAnalysis.cs:199:34:199:41 | access to property Length | strictlyPositive | +| SignAnalysis.cs:206:38:206:38 | access to parameter i | strictlyPositive | +| SignAnalysis.cs:210:38:210:38 | access to parameter i | negative | +| SignAnalysis.cs:219:38:219:38 | access to parameter i | strictlyPositive | +| SignAnalysis.cs:223:17:223:17 | access to parameter i | negative | +| SignAnalysis.cs:225:42:225:42 | access to parameter i | strictlyNegative | +| SignAnalysis.cs:236:38:236:38 | access to parameter i | strictlyPositive | +| SignAnalysis.cs:240:17:240:17 | access to parameter i | negative | +| SignAnalysis.cs:242:42:242:42 | access to parameter i | strictlyNegative | +| SignAnalysis.cs:257:17:257:17 | access to parameter i | positive | +| SignAnalysis.cs:257:17:257:19 | ...-- | positive | +| SignAnalysis.cs:260:38:260:38 | access to parameter i | strictlyNegative | +| SignAnalysis.cs:267:17:267:17 | access to parameter j | strictlyPositive | +| SignAnalysis.cs:267:17:267:19 | ...-- | strictlyPositive | +| SignAnalysis.cs:268:42:268:42 | access to parameter j | positive | +| SignAnalysis.cs:270:38:270:38 | access to parameter j | negative | +| SignAnalysis.cs:277:17:277:17 | access to parameter k | strictlyPositive | +| SignAnalysis.cs:277:17:277:19 | ...-- | strictlyPositive | +| SignAnalysis.cs:278:42:278:42 | access to parameter k | positive | +| SignAnalysis.cs:280:21:280:21 | access to parameter k | positive | +| SignAnalysis.cs:280:26:280:26 | 5 | strictlyPositive | +| SignAnalysis.cs:291:22:291:22 | access to parameter i | strictlyPositive | +| SignAnalysis.cs:292:34:292:34 | access to parameter i | strictlyPositive | +| SignAnalysis.cs:295:38:295:38 | access to parameter i | strictlyPositive | +| SignAnalysis.cs:300:27:300:28 | -... | strictlyNegative | +| SignAnalysis.cs:300:28:300:28 | 1 | strictlyPositive | +| SignAnalysis.cs:303:38:303:38 | access to local variable x | strictlyNegative | +| SignAnalysis.cs:306:21:306:22 | -... | strictlyNegative | +| SignAnalysis.cs:306:22:306:22 | 1 | strictlyPositive | +| SignAnalysis.cs:309:38:309:38 | access to local variable x | strictlyNegative | +| SignAnalysis.cs:316:13:316:31 | Char max = ... | strictlyPositive | +| SignAnalysis.cs:316:19:316:31 | access to constant MaxValue | strictlyPositive | +| SignAnalysis.cs:317:13:317:23 | Int32 c = ... | strictlyPositive | +| SignAnalysis.cs:317:17:317:23 | ... + ... | strictlyPositive | +| SignAnalysis.cs:317:23:317:23 | 1 | strictlyPositive | +| SignAnalysis.cs:318:34:318:34 | access to local variable c | strictlyPositive | +| SignAnalysis.cs:319:9:319:19 | ... = ... | strictlyNegative | +| SignAnalysis.cs:319:13:319:19 | ... - ... | strictlyNegative | +| SignAnalysis.cs:319:19:319:19 | 1 | strictlyPositive | +| SignAnalysis.cs:320:34:320:34 | access to local variable c | strictlyNegative | +| SignAnalysis.cs:321:9:321:19 | ... = ... | strictlyPositive | +| SignAnalysis.cs:321:13:321:15 | (...) ... | strictlyPositive | +| SignAnalysis.cs:321:13:321:15 | access to local variable max | strictlyPositive | +| SignAnalysis.cs:321:13:321:19 | ... + ... | strictlyPositive | +| SignAnalysis.cs:321:19:321:19 | 1 | strictlyPositive | +| SignAnalysis.cs:322:34:322:34 | access to local variable c | strictlyPositive | +| SignAnalysis.cs:329:17:329:26 | Int32 x = ... | strictlyPositive | +| SignAnalysis.cs:329:21:329:21 | access to parameter v | strictlyPositive | +| SignAnalysis.cs:329:21:329:26 | ... ?? ... | strictlyPositive | +| SignAnalysis.cs:329:26:329:26 | 1 | strictlyPositive | +| SignAnalysis.cs:330:38:330:38 | access to local variable x | strictlyPositive | +| SignAnalysis.cs:335:17:335:26 | Int32 x = ... | strictlyPositive | +| SignAnalysis.cs:335:21:335:26 | ... ?? ... | strictlyPositive | +| SignAnalysis.cs:335:26:335:26 | 1 | strictlyPositive | +| SignAnalysis.cs:336:38:336:38 | access to local variable x | strictlyPositive | +| SignAnalysis.cs:341:17:341:26 | Int32 x = ... | negative | +| SignAnalysis.cs:341:21:341:21 | access to parameter v | strictlyNegative | +| SignAnalysis.cs:341:21:341:26 | ... ?? ... | negative | +| SignAnalysis.cs:342:38:342:38 | access to local variable x | negative | +| SignAnalysis.cs:348:62:348:62 | 5 | strictlyPositive | +| SignAnalysis.cs:351:38:351:38 | access to local variable i | strictlyNegative | +| SignAnalysis.cs:371:38:371:38 | access to local variable y | strictlyNegative | +| SignAnalysis.cs:381:38:381:38 | access to local variable x | strictlyNegative | +| SignAnalysis.cs:385:50:385:99 | access to constant Explicit | strictlyPositive | +| SignAnalysis.cs:385:109:385:110 | 15 | strictlyPositive | +| SignAnalysis.cs:390:13:390:32 | Int32 x = ... | strictlyPositive | +| SignAnalysis.cs:390:17:390:32 | sizeof(..) | strictlyPositive | +| SignAnalysis.cs:391:34:391:34 | access to local variable x | strictlyPositive | +| SignAnalysis.cs:396:13:400:9 | Int32 x = ... | positive | +| SignAnalysis.cs:396:17:400:9 | ... switch { ... } | positive | +| SignAnalysis.cs:399:13:399:18 | ... => ... | strictlyPositive | +| SignAnalysis.cs:399:18:399:18 | 2 | strictlyPositive | +| SignAnalysis.cs:401:34:401:34 | access to local variable x | positive | +| SignAnalysis.cs:406:13:406:17 | Int32 i = ... | strictlyPositive | +| SignAnalysis.cs:406:17:406:17 | 1 | strictlyPositive | +| SignAnalysis.cs:410:35:410:35 | access to local variable i | strictlyPositive | +| SignAnalysis.cs:414:13:414:13 | access to local variable i | strictlyPositive | +| SignAnalysis.cs:415:31:415:31 | access to local variable i | strictlyPositive | +| SignAnalysis.cs:424:31:424:31 | access to local variable x | strictlyNegative | +| SignAnalysis.cs:434:38:434:38 | access to local variable i | strictlyNegative | +| SignAnalysis.cs:443:38:443:38 | access to local variable x | strictlyNegative | +| SignAnalysis.cs:446:31:446:32 | 10 | strictlyPositive | diff --git a/csharp/ql/test/library-tests/dataflow/signanalysis/SignAnalysis.ql b/csharp/ql/test/library-tests/dataflow/signanalysis/SignAnalysis.ql new file mode 100644 index 00000000000..4350e8f1742 --- /dev/null +++ b/csharp/ql/test/library-tests/dataflow/signanalysis/SignAnalysis.ql @@ -0,0 +1,21 @@ +import csharp +import semmle.code.csharp.dataflow.SignAnalysis + +string getASignString(Expr e) { + positive(e) and + not strictlyPositive(e) and + result = "positive" + or + negative(e) and + not strictlyNegative(e) and + result = "negative" + or + strictlyPositive(e) and + result = "strictlyPositive" + or + strictlyNegative(e) and + result = "strictlyNegative" +} + +from Expr e +select e, strictconcat(string s | s = getASignString(e) | s, " ") diff --git a/java/ql/src/semmle/code/java/dataflow/ModulusAnalysis.qll b/java/ql/src/semmle/code/java/dataflow/ModulusAnalysis.qll index 1fb3eb201a8..b153e9fbd04 100644 --- a/java/ql/src/semmle/code/java/dataflow/ModulusAnalysis.qll +++ b/java/ql/src/semmle/code/java/dataflow/ModulusAnalysis.qll @@ -6,6 +6,7 @@ import java private import SSA +private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon private import RangeUtils private import semmle.code.java.controlflow.Guards import Bound diff --git a/java/ql/src/semmle/code/java/dataflow/RangeAnalysis.qll b/java/ql/src/semmle/code/java/dataflow/RangeAnalysis.qll index cbd59f8302a..07860c76ee4 100644 --- a/java/ql/src/semmle/code/java/dataflow/RangeAnalysis.qll +++ b/java/ql/src/semmle/code/java/dataflow/RangeAnalysis.qll @@ -66,6 +66,7 @@ import java private import SSA private import RangeUtils +private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon private import semmle.code.java.controlflow.internal.GuardsLogic private import SignAnalysis private import ModulusAnalysis diff --git a/java/ql/src/semmle/code/java/dataflow/RangeUtils.qll b/java/ql/src/semmle/code/java/dataflow/RangeUtils.qll index e7da9891b47..631145a2aa2 100644 --- a/java/ql/src/semmle/code/java/dataflow/RangeUtils.qll +++ b/java/ql/src/semmle/code/java/dataflow/RangeUtils.qll @@ -5,6 +5,7 @@ import java private import SSA private import semmle.code.java.controlflow.internal.GuardsLogic +private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon /** * Holds if `v` is an input to `phi` that is not along a back edge, and the @@ -127,63 +128,6 @@ Expr ssaRead(SsaVariable v, int delta) { result.(AssignExpr).getSource() = ssaRead(v, delta) } -private newtype TSsaReadPosition = - TSsaReadPositionBlock(BasicBlock bb) { exists(SsaVariable v | bb = v.getAUse().getBasicBlock()) } or - TSsaReadPositionPhiInputEdge(BasicBlock bbOrig, BasicBlock bbPhi) { - exists(SsaPhiNode phi | phi.hasInputFromBlock(_, bbOrig) and bbPhi = phi.getBasicBlock()) - } - -/** - * A position at which an SSA variable is read. This includes both ordinary - * reads occurring in basic blocks and input to phi nodes occurring along an - * edge between two basic blocks. - */ -class SsaReadPosition extends TSsaReadPosition { - /** Holds if `v` is read at this position. */ - abstract predicate hasReadOfVar(SsaVariable v); - - /** Gets a textual representation of this SSA read position. */ - abstract string toString(); -} - -/** A basic block in which an SSA variable is read. */ -class SsaReadPositionBlock extends SsaReadPosition, TSsaReadPositionBlock { - /** Gets the basic block corresponding to this position. */ - BasicBlock getBlock() { this = TSsaReadPositionBlock(result) } - - override predicate hasReadOfVar(SsaVariable v) { getBlock() = v.getAUse().getBasicBlock() } - - override string toString() { result = "block" } -} - -/** - * An edge between two basic blocks where the latter block has an SSA phi - * definition. The edge therefore has a read of an SSA variable serving as the - * input to the phi node. - */ -class SsaReadPositionPhiInputEdge extends SsaReadPosition, TSsaReadPositionPhiInputEdge { - /** Gets the head of the edge. */ - BasicBlock getOrigBlock() { this = TSsaReadPositionPhiInputEdge(result, _) } - - /** Gets the tail of the edge. */ - BasicBlock getPhiBlock() { this = TSsaReadPositionPhiInputEdge(_, result) } - - override predicate hasReadOfVar(SsaVariable v) { - exists(SsaPhiNode phi | - phi.hasInputFromBlock(v, getOrigBlock()) and - getPhiBlock() = phi.getBasicBlock() - ) - } - - /** Holds if `inp` is an input to `phi` along this edge. */ - predicate phiInput(SsaPhiNode phi, SsaVariable inp) { - phi.hasInputFromBlock(inp, getOrigBlock()) and - getPhiBlock() = phi.getBasicBlock() - } - - override string toString() { result = "edge" } -} - /** * Holds if `inp` is an input to `phi` along a back edge. */ diff --git a/java/ql/src/semmle/code/java/dataflow/SignAnalysis.qll b/java/ql/src/semmle/code/java/dataflow/SignAnalysis.qll index 595f9c623f2..9cd629f4ef9 100644 --- a/java/ql/src/semmle/code/java/dataflow/SignAnalysis.qll +++ b/java/ql/src/semmle/code/java/dataflow/SignAnalysis.qll @@ -6,596 +6,4 @@ * three-valued domain `{negative, zero, positive}`. */ -import java -private import SSA -private import RangeUtils -private import semmle.code.java.controlflow.Guards -private import semmle.code.java.Reflection -private import semmle.code.java.Collections -private import semmle.code.java.Maps - -private newtype TSign = - TNeg() or - TZero() or - TPos() - -private class Sign extends TSign { - string toString() { - result = "-" and this = TNeg() - or - result = "0" and this = TZero() - or - result = "+" and this = TPos() - } - - Sign inc() { - this = TNeg() and result = TNeg() - or - this = TNeg() and result = TZero() - or - this = TZero() and result = TPos() - or - this = TPos() and result = TPos() - } - - Sign dec() { result.inc() = this } - - Sign neg() { - this = TNeg() and result = TPos() - or - this = TZero() and result = TZero() - or - this = TPos() and result = TNeg() - } - - Sign bitnot() { - this = TNeg() and result = TPos() - or - this = TNeg() and result = TZero() - or - this = TZero() and result = TNeg() - or - this = TPos() and result = TNeg() - } - - Sign add(Sign s) { - this = TZero() and result = s - or - s = TZero() and result = this - or - this = s and this = result - or - this = TPos() and s = TNeg() - or - this = TNeg() and s = TPos() - } - - Sign mul(Sign s) { - result = TZero() and this = TZero() - or - result = TZero() and s = TZero() - or - result = TNeg() and this = TPos() and s = TNeg() - or - result = TNeg() and this = TNeg() and s = TPos() - or - result = TPos() and this = TPos() and s = TPos() - or - result = TPos() and this = TNeg() and s = TNeg() - } - - Sign div(Sign s) { - result = TZero() and s = TNeg() - or - result = TZero() and s = TPos() - or - result = TNeg() and this = TPos() and s = TNeg() - or - result = TNeg() and this = TNeg() and s = TPos() - or - result = TPos() and this = TPos() and s = TPos() - or - result = TPos() and this = TNeg() and s = TNeg() - } - - Sign rem(Sign s) { - result = TZero() and s = TNeg() - or - result = TZero() and s = TPos() - or - result = this and s = TNeg() - or - result = this and s = TPos() - } - - Sign bitand(Sign s) { - result = TZero() and this = TZero() - or - result = TZero() and s = TZero() - or - result = TZero() and this = TPos() - or - result = TZero() and s = TPos() - or - result = TNeg() and this = TNeg() and s = TNeg() - or - result = TPos() and this = TNeg() and s = TPos() - or - result = TPos() and this = TPos() and s = TNeg() - or - result = TPos() and this = TPos() and s = TPos() - } - - Sign bitor(Sign s) { - result = TZero() and this = TZero() and s = TZero() - or - result = TNeg() and this = TNeg() - or - result = TNeg() and s = TNeg() - or - result = TPos() and this = TPos() and s = TZero() - or - result = TPos() and this = TZero() and s = TPos() - or - result = TPos() and this = TPos() and s = TPos() - } - - Sign bitxor(Sign s) { - result = TZero() and this = s - or - result = this and s = TZero() - or - result = s and this = TZero() - or - result = TPos() and this = TPos() and s = TPos() - or - result = TNeg() and this = TNeg() and s = TPos() - or - result = TNeg() and this = TPos() and s = TNeg() - or - result = TPos() and this = TNeg() and s = TNeg() - } - - Sign lshift(Sign s) { - result = TZero() and this = TZero() - or - result = this and s = TZero() - or - this != TZero() and s != TZero() - } - - Sign rshift(Sign s) { - result = TZero() and this = TZero() - or - result = this and s = TZero() - or - result = TNeg() and this = TNeg() - or - result != TNeg() and this = TPos() and s != TZero() - } - - Sign urshift(Sign s) { - result = TZero() and this = TZero() - or - result = this and s = TZero() - or - result != TZero() and this = TNeg() and s != TZero() - or - result != TNeg() and this = TPos() and s != TZero() - } -} - -/** Gets the sign of `e` if this can be directly determined. */ -private Sign certainExprSign(Expr e) { - exists(int i | e.(ConstantIntegerExpr).getIntValue() = i | - i < 0 and result = TNeg() - or - i = 0 and result = TZero() - or - i > 0 and result = TPos() - ) - or - not exists(e.(ConstantIntegerExpr).getIntValue()) and - ( - exists(float f | - f = e.(LongLiteral).getValue().toFloat() or - f = e.(FloatingPointLiteral).getValue().toFloat() or - f = e.(DoubleLiteral).getValue().toFloat() - | - f < 0 and result = TNeg() - or - f = 0 and result = TZero() - or - f > 0 and result = TPos() - ) - or - exists(string charlit | charlit = e.(CharacterLiteral).getValue() | - if charlit = "\\0" or charlit = "\\u0000" then result = TZero() else result = TPos() - ) - or - e.(MethodAccess).getMethod() instanceof StringLengthMethod and - (result = TPos() or result = TZero()) - or - e.(MethodAccess).getMethod() instanceof CollectionSizeMethod and - (result = TPos() or result = TZero()) - or - e.(MethodAccess).getMethod() instanceof MapSizeMethod and - (result = TPos() or result = TZero()) - ) -} - -/** Holds if the sign of `e` is too complicated to determine. */ -private predicate unknownSign(Expr e) { - not exists(e.(ConstantIntegerExpr).getIntValue()) and - ( - exists(IntegerLiteral lit | lit = e and not exists(lit.getValue().toInt())) - or - exists(LongLiteral lit | lit = e and not exists(lit.getValue().toFloat())) - or - exists(CastExpr cast, Type fromtyp | - cast = e and - fromtyp = cast.getExpr().getType() and - not fromtyp instanceof NumericOrCharType - ) - or - e instanceof ArrayAccess and e.getType() instanceof NumericOrCharType - or - e instanceof MethodAccess and e.getType() instanceof NumericOrCharType - or - e instanceof ClassInstanceExpr and e.getType() instanceof NumericOrCharType - ) -} - -/** - * Holds if `lowerbound` is a lower bound for `v` at `pos`. This is restricted - * to only include bounds for which we might determine a sign. - */ -private predicate lowerBound(Expr lowerbound, SsaVariable v, SsaReadPosition pos, boolean isStrict) { - exists(boolean testIsTrue, ComparisonExpr comp | - pos.hasReadOfVar(v) and - guardControlsSsaRead(comp, pos, testIsTrue) and - not unknownSign(lowerbound) - | - testIsTrue = true and - comp.getLesserOperand() = lowerbound and - comp.getGreaterOperand() = ssaRead(v, 0) and - (if comp.isStrict() then isStrict = true else isStrict = false) - or - testIsTrue = false and - comp.getGreaterOperand() = lowerbound and - comp.getLesserOperand() = ssaRead(v, 0) and - (if comp.isStrict() then isStrict = false else isStrict = true) - ) -} - -/** - * Holds if `upperbound` is an upper bound for `v` at `pos`. This is restricted - * to only include bounds for which we might determine a sign. - */ -private predicate upperBound(Expr upperbound, SsaVariable v, SsaReadPosition pos, boolean isStrict) { - exists(boolean testIsTrue, ComparisonExpr comp | - pos.hasReadOfVar(v) and - guardControlsSsaRead(comp, pos, testIsTrue) and - not unknownSign(upperbound) - | - testIsTrue = true and - comp.getGreaterOperand() = upperbound and - comp.getLesserOperand() = ssaRead(v, 0) and - (if comp.isStrict() then isStrict = true else isStrict = false) - or - testIsTrue = false and - comp.getLesserOperand() = upperbound and - comp.getGreaterOperand() = ssaRead(v, 0) and - (if comp.isStrict() then isStrict = false else isStrict = true) - ) -} - -/** - * Holds if `eqbound` is an equality/inequality for `v` at `pos`. This is - * restricted to only include bounds for which we might determine a sign. The - * boolean `isEq` gives the polarity: - * - `isEq = true` : `v = eqbound` - * - `isEq = false` : `v != eqbound` - */ -private predicate eqBound(Expr eqbound, SsaVariable v, SsaReadPosition pos, boolean isEq) { - exists(Guard guard, boolean testIsTrue, boolean polarity | - pos.hasReadOfVar(v) and - guardControlsSsaRead(guard, pos, testIsTrue) and - guard.isEquality(eqbound, ssaRead(v, 0), polarity) and - isEq = polarity.booleanXor(testIsTrue).booleanNot() and - not unknownSign(eqbound) - ) -} - -/** - * Holds if `bound` is a bound for `v` at `pos` that needs to be positive in - * order for `v` to be positive. - */ -private predicate posBound(Expr bound, SsaVariable v, SsaReadPosition pos) { - upperBound(bound, v, pos, _) or - eqBound(bound, v, pos, true) -} - -/** - * Holds if `bound` is a bound for `v` at `pos` that needs to be negative in - * order for `v` to be negative. - */ -private predicate negBound(Expr bound, SsaVariable v, SsaReadPosition pos) { - lowerBound(bound, v, pos, _) or - eqBound(bound, v, pos, true) -} - -/** - * Holds if `bound` is a bound for `v` at `pos` that can restrict whether `v` - * can be zero. - */ -private predicate zeroBound(Expr bound, SsaVariable v, SsaReadPosition pos) { - lowerBound(bound, v, pos, _) or - upperBound(bound, v, pos, _) or - eqBound(bound, v, pos, _) -} - -/** Holds if `bound` allows `v` to be positive at `pos`. */ -private predicate posBoundOk(Expr bound, SsaVariable v, SsaReadPosition pos) { - posBound(bound, v, pos) and TPos() = exprSign(bound) -} - -/** Holds if `bound` allows `v` to be negative at `pos`. */ -private predicate negBoundOk(Expr bound, SsaVariable v, SsaReadPosition pos) { - negBound(bound, v, pos) and TNeg() = exprSign(bound) -} - -/** Holds if `bound` allows `v` to be zero at `pos`. */ -private predicate zeroBoundOk(Expr bound, SsaVariable v, SsaReadPosition pos) { - lowerBound(bound, v, pos, _) and TNeg() = exprSign(bound) - or - lowerBound(bound, v, pos, false) and TZero() = exprSign(bound) - or - upperBound(bound, v, pos, _) and TPos() = exprSign(bound) - or - upperBound(bound, v, pos, false) and TZero() = exprSign(bound) - or - eqBound(bound, v, pos, true) and TZero() = exprSign(bound) - or - eqBound(bound, v, pos, false) and TZero() != exprSign(bound) -} - -/** - * Holds if there is a bound that might restrict whether `v` has the sign `s` - * at `pos`. - */ -private predicate hasGuard(SsaVariable v, SsaReadPosition pos, Sign s) { - s = TPos() and posBound(_, v, pos) - or - s = TNeg() and negBound(_, v, pos) - or - s = TZero() and zeroBound(_, v, pos) -} - -pragma[noinline] -private Sign guardedSsaSign(SsaVariable v, SsaReadPosition pos) { - result = ssaDefSign(v) and - pos.hasReadOfVar(v) and - hasGuard(v, pos, result) -} - -pragma[noinline] -private Sign unguardedSsaSign(SsaVariable v, SsaReadPosition pos) { - result = ssaDefSign(v) and - pos.hasReadOfVar(v) and - not hasGuard(v, pos, result) -} - -private Sign guardedSsaSignOk(SsaVariable v, SsaReadPosition pos) { - result = TPos() and - forex(Expr bound | posBound(bound, v, pos) | posBoundOk(bound, v, pos)) - or - result = TNeg() and - forex(Expr bound | negBound(bound, v, pos) | negBoundOk(bound, v, pos)) - or - result = TZero() and - forex(Expr bound | zeroBound(bound, v, pos) | zeroBoundOk(bound, v, pos)) -} - -/** Gets a possible sign for `v` at `pos`. */ -private Sign ssaSign(SsaVariable v, SsaReadPosition pos) { - result = unguardedSsaSign(v, pos) - or - result = guardedSsaSign(v, pos) and - result = guardedSsaSignOk(v, pos) -} - -/** Gets a possible sign for `v`. */ -pragma[nomagic] -private Sign ssaDefSign(SsaVariable v) { - exists(VariableUpdate def | def = v.(SsaExplicitUpdate).getDefiningExpr() | - result = exprSign(def.(VariableAssign).getSource()) - or - exists(EnhancedForStmt for | def = for.getVariable()) - or - result = exprSign(def.(PostIncExpr).getExpr()).inc() - or - result = exprSign(def.(PreIncExpr).getExpr()).inc() - or - result = exprSign(def.(PostDecExpr).getExpr()).dec() - or - result = exprSign(def.(PreDecExpr).getExpr()).dec() - or - exists(AssignOp a | a = def and result = exprSign(a)) - ) - or - result = fieldSign(v.(SsaImplicitUpdate).getSourceVariable().getVariable()) - or - result = fieldSign(v.(SsaImplicitInit).getSourceVariable().getVariable()) - or - exists(Parameter p | v.(SsaImplicitInit).isParameterDefinition(p)) - or - exists(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge | - v = phi and - edge.phiInput(phi, inp) and - result = ssaSign(inp, edge) - ) -} - -/** Gets a possible sign for `f`. */ -private Sign fieldSign(Field f) { - result = exprSign(f.getAnAssignedValue()) - or - exists(PostIncExpr inc | inc.getExpr() = f.getAnAccess() and result = fieldSign(f).inc()) - or - exists(PreIncExpr inc | inc.getExpr() = f.getAnAccess() and result = fieldSign(f).inc()) - or - exists(PostDecExpr inc | inc.getExpr() = f.getAnAccess() and result = fieldSign(f).dec()) - or - exists(PreDecExpr inc | inc.getExpr() = f.getAnAccess() and result = fieldSign(f).dec()) - or - exists(AssignOp a | a.getDest() = f.getAnAccess() | result = exprSign(a)) - or - exists(ReflectiveFieldAccess rfa | rfa.inferAccessedField() = f) - or - if f.fromSource() - then not exists(f.getInitializer()) and result = TZero() - else - if f instanceof ArrayLengthField - then result != TNeg() - else - if f.hasName("MAX_VALUE") - then result = TPos() - else - if f.hasName("MIN_VALUE") - then result = TNeg() - else any() -} - -/** Gets a possible sign for `e`. */ -cached -private Sign exprSign(Expr e) { - result = certainExprSign(e) - or - not exists(certainExprSign(e)) and - ( - unknownSign(e) - or - exists(SsaVariable v | v.getAUse() = e | - result = ssaSign(v, any(SsaReadPositionBlock bb | bb.getBlock() = e.getBasicBlock())) - or - not exists(e.getBasicBlock()) and result = ssaDefSign(v) - ) - or - exists(FieldAccess fa | fa = e | - not exists(SsaVariable v | v.getAUse() = fa) and - result = fieldSign(fa.getField()) - ) - or - exists(VarAccess va | va = e | - not exists(SsaVariable v | v.getAUse() = va) and - not va instanceof FieldAccess - ) - or - result = exprSign(e.(AssignExpr).getSource()) - or - result = exprSign(e.(PlusExpr).getExpr()) - or - result = exprSign(e.(PostIncExpr).getExpr()) - or - result = exprSign(e.(PostDecExpr).getExpr()) - or - result = exprSign(e.(PreIncExpr).getExpr()).inc() - or - result = exprSign(e.(PreDecExpr).getExpr()).dec() - or - result = exprSign(e.(MinusExpr).getExpr()).neg() - or - result = exprSign(e.(BitNotExpr).getExpr()).bitnot() - or - exists(DivExpr div | - div = e and - result = exprSign(div.getLeftOperand()) and - result != TZero() - | - div.getRightOperand().(FloatingPointLiteral).getValue().toFloat() = 0 or - div.getRightOperand().(DoubleLiteral).getValue().toFloat() = 0 - ) - or - exists(Sign s1, Sign s2 | binaryOpSigns(e, s1, s2) | - (e instanceof AssignAddExpr or e instanceof AddExpr) and - result = s1.add(s2) - or - (e instanceof AssignSubExpr or e instanceof SubExpr) and - result = s1.add(s2.neg()) - or - (e instanceof AssignMulExpr or e instanceof MulExpr) and - result = s1.mul(s2) - or - (e instanceof AssignDivExpr or e instanceof DivExpr) and - result = s1.div(s2) - or - (e instanceof AssignRemExpr or e instanceof RemExpr) and - result = s1.rem(s2) - or - (e instanceof AssignAndExpr or e instanceof AndBitwiseExpr) and - result = s1.bitand(s2) - or - (e instanceof AssignOrExpr or e instanceof OrBitwiseExpr) and - result = s1.bitor(s2) - or - (e instanceof AssignXorExpr or e instanceof XorBitwiseExpr) and - result = s1.bitxor(s2) - or - (e instanceof AssignLShiftExpr or e instanceof LShiftExpr) and - result = s1.lshift(s2) - or - (e instanceof AssignRShiftExpr or e instanceof RShiftExpr) and - result = s1.rshift(s2) - or - (e instanceof AssignURShiftExpr or e instanceof URShiftExpr) and - result = s1.urshift(s2) - ) - or - result = exprSign(e.(ChooseExpr).getAResultExpr()) - or - result = exprSign(e.(CastExpr).getExpr()) - ) -} - -private Sign binaryOpLhsSign(Expr e) { - result = exprSign(e.(BinaryExpr).getLeftOperand()) or - result = exprSign(e.(AssignOp).getDest()) -} - -private Sign binaryOpRhsSign(Expr e) { - result = exprSign(e.(BinaryExpr).getRightOperand()) or - result = exprSign(e.(AssignOp).getRhs()) -} - -pragma[noinline] -private predicate binaryOpSigns(Expr e, Sign lhs, Sign rhs) { - lhs = binaryOpLhsSign(e) and - rhs = binaryOpRhsSign(e) -} - -/** Holds if `e` can be positive and cannot be negative. */ -predicate positive(Expr e) { - exprSign(e) = TPos() and - not exprSign(e) = TNeg() -} - -/** Holds if `e` can be negative and cannot be positive. */ -predicate negative(Expr e) { - exprSign(e) = TNeg() and - not exprSign(e) = TPos() -} - -/** Holds if `e` is strictly positive. */ -predicate strictlyPositive(Expr e) { - exprSign(e) = TPos() and - not exprSign(e) = TNeg() and - not exprSign(e) = TZero() -} - -/** Holds if `e` is strictly negative. */ -predicate strictlyNegative(Expr e) { - exprSign(e) = TNeg() and - not exprSign(e) = TPos() and - not exprSign(e) = TZero() -} +import semmle.code.java.dataflow.internal.rangeanalysis.SignAnalysisCommon diff --git a/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/Sign.qll b/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/Sign.qll new file mode 100644 index 00000000000..10ca946a044 --- /dev/null +++ b/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/Sign.qll @@ -0,0 +1,219 @@ +newtype TSign = + TNeg() or + TZero() or + TPos() + +/** Class representing expression signs (+, -, 0). */ +class Sign extends TSign { + /** Gets the string representation of this sign. */ + string toString() { + result = "-" and this = TNeg() + or + result = "0" and this = TZero() + or + result = "+" and this = TPos() + } + + /** Gets a possible sign after incrementing an expression that has this sign. */ + Sign inc() { + this = TNeg() and result = TNeg() + or + this = TNeg() and result = TZero() + or + this = TZero() and result = TPos() + or + this = TPos() and result = TPos() + } + + /** Gets a possible sign after decrementing an expression that has this sign. */ + Sign dec() { result.inc() = this } + + /** Gets a possible sign after negating an expression that has this sign. */ + Sign neg() { + this = TNeg() and result = TPos() + or + this = TZero() and result = TZero() + or + this = TPos() and result = TNeg() + } + + /** + * Gets a possible sign after bitwise complementing an expression that has this + * sign. + */ + Sign bitnot() { + this = TNeg() and result = TPos() + or + this = TNeg() and result = TZero() + or + this = TZero() and result = TNeg() + or + this = TPos() and result = TNeg() + } + + /** + * Gets a possible sign after adding an expression with sign `s` to an expression + * that has this sign. + */ + Sign add(Sign s) { + this = TZero() and result = s + or + s = TZero() and result = this + or + this = s and this = result + or + this = TPos() and s = TNeg() + or + this = TNeg() and s = TPos() + } + + /** + * Gets a possible sign after multiplying an expression with sign `s` to an expression + * that has this sign. + */ + Sign mul(Sign s) { + result = TZero() and this = TZero() + or + result = TZero() and s = TZero() + or + result = TNeg() and this = TPos() and s = TNeg() + or + result = TNeg() and this = TNeg() and s = TPos() + or + result = TPos() and this = TPos() and s = TPos() + or + result = TPos() and this = TNeg() and s = TNeg() + } + + /** + * Gets a possible sign after integer dividing an expression that has this sign + * by an expression with sign `s`. + */ + Sign div(Sign s) { + result = TZero() and s = TNeg() // ex: 3 / -5 = 0 + or + result = TZero() and s = TPos() // ex: 3 / 5 = 0 + or + result = TNeg() and this = TPos() and s = TNeg() + or + result = TNeg() and this = TNeg() and s = TPos() + or + result = TPos() and this = TPos() and s = TPos() + or + result = TPos() and this = TNeg() and s = TNeg() + } + + /** + * Gets a possible sign after modulo dividing an expression that has this sign + * by an expression with sign `s`. + */ + Sign rem(Sign s) { + result = TZero() and s = TNeg() + or + result = TZero() and s = TPos() + or + result = this and s = TNeg() + or + result = this and s = TPos() + } + + /** + * Gets a possible sign after bitwise `and` of an expression that has this sign + * and an expression with sign `s`. + */ + Sign bitand(Sign s) { + result = TZero() and this = TZero() + or + result = TZero() and s = TZero() + or + result = TZero() and this = TPos() + or + result = TZero() and s = TPos() + or + result = TNeg() and this = TNeg() and s = TNeg() + or + result = TPos() and this = TNeg() and s = TPos() + or + result = TPos() and this = TPos() and s = TNeg() + or + result = TPos() and this = TPos() and s = TPos() + } + + /** + * Gets a possible sign after bitwise `or` of an expression that has this sign + * and an expression with sign `s`. + */ + Sign bitor(Sign s) { + result = TZero() and this = TZero() and s = TZero() + or + result = TNeg() and this = TNeg() + or + result = TNeg() and s = TNeg() + or + result = TPos() and this = TPos() and s = TZero() + or + result = TPos() and this = TZero() and s = TPos() + or + result = TPos() and this = TPos() and s = TPos() + } + + /** + * Gets a possible sign after bitwise `xor` of an expression that has this sign + * and an expression with sign `s`. + */ + Sign bitxor(Sign s) { + result = TZero() and this = s + or + result = this and s = TZero() + or + result = s and this = TZero() + or + result = TPos() and this = TPos() and s = TPos() + or + result = TNeg() and this = TNeg() and s = TPos() + or + result = TNeg() and this = TPos() and s = TNeg() + or + result = TPos() and this = TNeg() and s = TNeg() + } + + /** + * Gets a possible sign after left shift of an expression that has this sign + * by an expression with sign `s`. + */ + Sign lshift(Sign s) { + result = TZero() and this = TZero() + or + result = this and s = TZero() + or + this != TZero() and s != TZero() + } + + /** + * Gets a possible sign after right shift of an expression that has this sign + * by an expression with sign `s`. + */ + Sign rshift(Sign s) { + result = TZero() and this = TZero() + or + result = this and s = TZero() + or + result = TNeg() and this = TNeg() + or + result != TNeg() and this = TPos() and s != TZero() + } + + /** + * Gets a possible sign after unsigned right shift of an expression that has + * this sign by an expression with sign `s`. + */ + Sign urshift(Sign s) { + result = TZero() and this = TZero() + or + result = this and s = TZero() + or + result != TZero() and this = TNeg() and s != TZero() + or + result != TNeg() and this = TPos() and s != TZero() + } +} diff --git a/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisCommon.qll b/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisCommon.qll new file mode 100644 index 00000000000..66b38433eef --- /dev/null +++ b/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisCommon.qll @@ -0,0 +1,293 @@ +/** + * Provides sign analysis to determine whether expression are always positive + * or negative. + * + * The analysis is implemented as an abstract interpretation over the + * three-valued domain `{negative, zero, positive}`. + */ + +private import SignAnalysisSpecific::Private +private import SsaReadPositionCommon +private import Sign + +/** Gets the sign of `e` if this can be directly determined. */ +Sign certainExprSign(Expr e) { + exists(int i | e.(ConstantIntegerExpr).getIntValue() = i | + i < 0 and result = TNeg() + or + i = 0 and result = TZero() + or + i > 0 and result = TPos() + ) + or + not exists(e.(ConstantIntegerExpr).getIntValue()) and + ( + exists(float f | f = getNonIntegerValue(e) | + f < 0 and result = TNeg() + or + f = 0 and result = TZero() + or + f > 0 and result = TPos() + ) + or + exists(string charlit | charlit = getCharValue(e) | + if charlit.regexpMatch("\\u0000") then result = TZero() else result = TPos() + ) + or + containerSizeAccess(e) and + (result = TPos() or result = TZero()) + or + positiveExpression(e) and result = TPos() + ) +} + +/** Holds if the sign of `e` is too complicated to determine. */ +predicate unknownSign(Expr e) { + not exists(certainExprSign(e)) and + ( + exists(IntegerLiteral lit | lit = e and not exists(lit.getValue().toInt())) + or + exists(LongLiteral lit | lit = e and not exists(lit.getValue().toFloat())) + or + exists(CastExpr cast, Type fromtyp | + cast = e and + fromtyp = cast.getExpr().getType() and + not fromtyp instanceof NumericOrCharType + ) + or + unknownIntegerAccess(e) + ) +} + +/** + * Holds if `lowerbound` is a lower bound for `v` at `pos`. This is restricted + * to only include bounds for which we might determine a sign. + */ +private predicate lowerBound(Expr lowerbound, SsaVariable v, SsaReadPosition pos, boolean isStrict) { + exists(boolean testIsTrue, ComparisonExpr comp | + pos.hasReadOfVar(v) and + guardControlsSsaRead(getComparisonGuard(comp), pos, testIsTrue) and + not unknownSign(lowerbound) + | + testIsTrue = true and + comp.getLesserOperand() = lowerbound and + comp.getGreaterOperand() = ssaRead(v, 0) and + (if comp.isStrict() then isStrict = true else isStrict = false) + or + testIsTrue = false and + comp.getGreaterOperand() = lowerbound and + comp.getLesserOperand() = ssaRead(v, 0) and + (if comp.isStrict() then isStrict = false else isStrict = true) + ) +} + +/** + * Holds if `upperbound` is an upper bound for `v` at `pos`. This is restricted + * to only include bounds for which we might determine a sign. + */ +private predicate upperBound(Expr upperbound, SsaVariable v, SsaReadPosition pos, boolean isStrict) { + exists(boolean testIsTrue, ComparisonExpr comp | + pos.hasReadOfVar(v) and + guardControlsSsaRead(getComparisonGuard(comp), pos, testIsTrue) and + not unknownSign(upperbound) + | + testIsTrue = true and + comp.getGreaterOperand() = upperbound and + comp.getLesserOperand() = ssaRead(v, 0) and + (if comp.isStrict() then isStrict = true else isStrict = false) + or + testIsTrue = false and + comp.getLesserOperand() = upperbound and + comp.getGreaterOperand() = ssaRead(v, 0) and + (if comp.isStrict() then isStrict = false else isStrict = true) + ) +} + +/** + * Holds if `eqbound` is an equality/inequality for `v` at `pos`. This is + * restricted to only include bounds for which we might determine a sign. The + * boolean `isEq` gives the polarity: + * - `isEq = true` : `v = eqbound` + * - `isEq = false` : `v != eqbound` + */ +private predicate eqBound(Expr eqbound, SsaVariable v, SsaReadPosition pos, boolean isEq) { + exists(Guard guard, boolean testIsTrue, boolean polarity | + pos.hasReadOfVar(v) and + guardControlsSsaRead(guard, pos, testIsTrue) and + guard.isEquality(eqbound, ssaRead(v, 0), polarity) and + isEq = polarity.booleanXor(testIsTrue).booleanNot() and + not unknownSign(eqbound) + ) +} + +/** + * Holds if `bound` is a bound for `v` at `pos` that needs to be positive in + * order for `v` to be positive. + */ +private predicate posBound(Expr bound, SsaVariable v, SsaReadPosition pos) { + upperBound(bound, v, pos, _) or + eqBound(bound, v, pos, true) +} + +/** + * Holds if `bound` is a bound for `v` at `pos` that needs to be negative in + * order for `v` to be negative. + */ +private predicate negBound(Expr bound, SsaVariable v, SsaReadPosition pos) { + lowerBound(bound, v, pos, _) or + eqBound(bound, v, pos, true) +} + +/** + * Holds if `bound` is a bound for `v` at `pos` that can restrict whether `v` + * can be zero. + */ +private predicate zeroBound(Expr bound, SsaVariable v, SsaReadPosition pos) { + lowerBound(bound, v, pos, _) or + upperBound(bound, v, pos, _) or + eqBound(bound, v, pos, _) +} + +/** Holds if `bound` allows `v` to be positive at `pos`. */ +private predicate posBoundOk(Expr bound, SsaVariable v, SsaReadPosition pos) { + posBound(bound, v, pos) and TPos() = exprSign(bound) +} + +/** Holds if `bound` allows `v` to be negative at `pos`. */ +private predicate negBoundOk(Expr bound, SsaVariable v, SsaReadPosition pos) { + negBound(bound, v, pos) and TNeg() = exprSign(bound) +} + +/** Holds if `bound` allows `v` to be zero at `pos`. */ +private predicate zeroBoundOk(Expr bound, SsaVariable v, SsaReadPosition pos) { + lowerBound(bound, v, pos, _) and TNeg() = exprSign(bound) + or + lowerBound(bound, v, pos, false) and TZero() = exprSign(bound) + or + upperBound(bound, v, pos, _) and TPos() = exprSign(bound) + or + upperBound(bound, v, pos, false) and TZero() = exprSign(bound) + or + eqBound(bound, v, pos, true) and TZero() = exprSign(bound) + or + eqBound(bound, v, pos, false) and TZero() != exprSign(bound) +} + +/** + * Holds if there is a bound that might restrict whether `v` has the sign `s` + * at `pos`. + */ +private predicate hasGuard(SsaVariable v, SsaReadPosition pos, Sign s) { + s = TPos() and posBound(_, v, pos) + or + s = TNeg() and negBound(_, v, pos) + or + s = TZero() and zeroBound(_, v, pos) +} + +pragma[noinline] +private Sign guardedSsaSign(SsaVariable v, SsaReadPosition pos) { + // SSA variable can have sign `result` + result = ssaDefSign(v) and + pos.hasReadOfVar(v) and + // there are guards at this position on `v` that might restrict it to be sign `result`. + // (So we need to check if they are satisfied) + hasGuard(v, pos, result) +} + +pragma[noinline] +private Sign unguardedSsaSign(SsaVariable v, SsaReadPosition pos) { + // SSA variable can have sign `result` + result = ssaDefSign(v) and + pos.hasReadOfVar(v) and + // there's no guard at this position on `v` that might restrict it to be sign `result`. + not hasGuard(v, pos, result) +} + +/** + * Gets the sign of `v` at read position `pos`, when there's at least one guard + * on `v` at position `pos`. Each bound corresponding to a given sign must be met + * in order for `v` to be of that sign. + */ +private Sign guardedSsaSignOk(SsaVariable v, SsaReadPosition pos) { + result = TPos() and + forex(Expr bound | posBound(bound, v, pos) | posBoundOk(bound, v, pos)) + or + result = TNeg() and + forex(Expr bound | negBound(bound, v, pos) | negBoundOk(bound, v, pos)) + or + result = TZero() and + forex(Expr bound | zeroBound(bound, v, pos) | zeroBoundOk(bound, v, pos)) +} + +/** Gets a possible sign for `v` at `pos`. */ +Sign ssaSign(SsaVariable v, SsaReadPosition pos) { + result = unguardedSsaSign(v, pos) + or + result = guardedSsaSign(v, pos) and + result = guardedSsaSignOk(v, pos) +} + +/** Gets a possible sign for `v`. */ +pragma[nomagic] +Sign ssaDefSign(SsaVariable v) { + result = explicitSsaDefSign(v) + or + result = implicitSsaDefSign(v) + or + exists(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge | + v = phi and + edge.phiInput(phi, inp) and + result = ssaSign(inp, edge) + ) +} + +/** Gets a possible sign for `e`. */ +cached +Sign exprSign(Expr e) { + result = certainExprSign(e) + or + not exists(certainExprSign(e)) and + ( + unknownSign(e) + or + exists(SsaVariable v | getARead(v) = e | result = ssaVariableSign(v, e)) + or + e = + any(VarAccess access | + not exists(SsaVariable v | getARead(v) = access) and + ( + result = fieldSign(getField(access.(FieldAccess))) or + not access instanceof FieldAccess + ) + ) + or + result = specificSubExprSign(e) + ) +} + +/** Holds if `e` can be positive and cannot be negative. */ +predicate positive(Expr e) { + exprSign(e) = TPos() and + not exprSign(e) = TNeg() +} + +/** Holds if `e` can be negative and cannot be positive. */ +predicate negative(Expr e) { + exprSign(e) = TNeg() and + not exprSign(e) = TPos() +} + +/** Holds if `e` is strictly positive. */ +predicate strictlyPositive(Expr e) { + exprSign(e) = TPos() and + not exprSign(e) = TNeg() and + not exprSign(e) = TZero() +} + +/** Holds if `e` is strictly negative. */ +predicate strictlyNegative(Expr e) { + exprSign(e) = TNeg() and + not exprSign(e) = TPos() and + not exprSign(e) = TZero() +} diff --git a/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll b/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll new file mode 100644 index 00000000000..16784ccf0ec --- /dev/null +++ b/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll @@ -0,0 +1,235 @@ +/** + * Provides Java-specific definitions for use in sign analysis. + */ +module Private { + import semmle.code.java.dataflow.RangeUtils as RU + private import semmle.code.java.dataflow.SSA as Ssa + private import semmle.code.java.controlflow.Guards as G + private import java as J + import Impl + + class ConstantIntegerExpr = RU::ConstantIntegerExpr; + + class Guard = G::Guard; + + class SsaVariable = Ssa::SsaVariable; + + class SsaPhiNode = Ssa::SsaPhiNode; + + class VarAccess = J::VarAccess; + + class FieldAccess = J::FieldAccess; + + class CharacterLiteral = J::CharacterLiteral; + + class IntegerLiteral = J::IntegerLiteral; + + class LongLiteral = J::LongLiteral; + + class CastExpr = J::CastExpr; + + class Type = J::Type; + + class Expr = J::Expr; + + class ComparisonExpr = J::ComparisonExpr; + + class NumericOrCharType = J::NumericOrCharType; + + predicate ssaRead = RU::ssaRead/2; + + predicate guardControlsSsaRead = RU::guardControlsSsaRead/3; +} + +private module Impl { + private import java + private import semmle.code.java.dataflow.RangeUtils + private import semmle.code.java.dataflow.SSA + private import semmle.code.java.controlflow.Guards + private import semmle.code.java.Reflection + private import semmle.code.java.Collections + private import semmle.code.java.Maps + private import Sign + private import SignAnalysisCommon + private import SsaReadPositionCommon + + float getNonIntegerValue(Expr e) { + result = e.(LongLiteral).getValue().toFloat() or + result = e.(FloatingPointLiteral).getValue().toFloat() or + result = e.(DoubleLiteral).getValue().toFloat() + } + + string getCharValue(Expr e) { result = e.(CharacterLiteral).getValue() } + + predicate containerSizeAccess(Expr e) { + e.(MethodAccess).getMethod() instanceof StringLengthMethod + or + e.(MethodAccess).getMethod() instanceof CollectionSizeMethod + or + e.(MethodAccess).getMethod() instanceof MapSizeMethod + } + + predicate positiveExpression(Expr e) { none() } + + predicate unknownIntegerAccess(Expr e) { + e instanceof ArrayAccess and e.getType() instanceof NumericOrCharType + or + e instanceof MethodAccess and e.getType() instanceof NumericOrCharType + or + e instanceof ClassInstanceExpr and e.getType() instanceof NumericOrCharType + } + + Sign explicitSsaDefSign(SsaVariable v) { + exists(VariableUpdate def | def = v.(SsaExplicitUpdate).getDefiningExpr() | + result = exprSign(def.(VariableAssign).getSource()) + or + exists(EnhancedForStmt for | def = for.getVariable()) + or + result = exprSign(def.(PostIncExpr).getExpr()).inc() + or + result = exprSign(def.(PreIncExpr).getExpr()).inc() + or + result = exprSign(def.(PostDecExpr).getExpr()).dec() + or + result = exprSign(def.(PreDecExpr).getExpr()).dec() + or + exists(AssignOp a | a = def and result = exprSign(a)) + ) + } + + Sign implicitSsaDefSign(SsaVariable v) { + result = fieldSign(v.(SsaImplicitUpdate).getSourceVariable().getVariable()) + or + result = fieldSign(v.(SsaImplicitInit).getSourceVariable().getVariable()) + or + exists(Parameter p | v.(SsaImplicitInit).isParameterDefinition(p)) + } + + pragma[inline] + Sign ssaVariableSign(SsaVariable v, Expr e) { + result = ssaSign(v, any(SsaReadPositionBlock bb | getAnExpression(bb) = e)) + or + not exists(SsaReadPositionBlock bb | getAnExpression(bb) = e) and + result = ssaDefSign(v) + } + + /** Gets a possible sign for `f`. */ + Sign fieldSign(Field f) { + result = exprSign(f.getAnAssignedValue()) + or + exists(PostIncExpr inc | inc.getExpr() = f.getAnAccess() and result = fieldSign(f).inc()) + or + exists(PreIncExpr inc | inc.getExpr() = f.getAnAccess() and result = fieldSign(f).inc()) + or + exists(PostDecExpr inc | inc.getExpr() = f.getAnAccess() and result = fieldSign(f).dec()) + or + exists(PreDecExpr inc | inc.getExpr() = f.getAnAccess() and result = fieldSign(f).dec()) + or + exists(AssignOp a | a.getDest() = f.getAnAccess() | result = exprSign(a)) + or + exists(ReflectiveFieldAccess rfa | rfa.inferAccessedField() = f) + or + if f.fromSource() + then not exists(f.getInitializer()) and result = TZero() + else + if f instanceof ArrayLengthField + then result != TNeg() + else + if f.hasName("MAX_VALUE") + then result = TPos() + else + if f.hasName("MIN_VALUE") + then result = TNeg() + else any() + } + + Sign specificSubExprSign(Expr e) { + result = exprSign(e.(AssignExpr).getSource()) + or + result = exprSign(e.(PlusExpr).getExpr()) + or + result = exprSign(e.(PostIncExpr).getExpr()) + or + result = exprSign(e.(PostDecExpr).getExpr()) + or + result = exprSign(e.(PreIncExpr).getExpr()).inc() + or + result = exprSign(e.(PreDecExpr).getExpr()).dec() + or + result = exprSign(e.(MinusExpr).getExpr()).neg() + or + result = exprSign(e.(BitNotExpr).getExpr()).bitnot() + or + exists(DivExpr div | + div = e and + result = exprSign(div.getLeftOperand()) and + result != TZero() + | + div.getRightOperand().(FloatingPointLiteral).getValue().toFloat() = 0 or + div.getRightOperand().(DoubleLiteral).getValue().toFloat() = 0 + ) + or + exists(Sign s1, Sign s2 | binaryOpSigns(e, s1, s2) | + (e instanceof AssignAddExpr or e instanceof AddExpr) and + result = s1.add(s2) + or + (e instanceof AssignSubExpr or e instanceof SubExpr) and + result = s1.add(s2.neg()) + or + (e instanceof AssignMulExpr or e instanceof MulExpr) and + result = s1.mul(s2) + or + (e instanceof AssignDivExpr or e instanceof DivExpr) and + result = s1.div(s2) + or + (e instanceof AssignRemExpr or e instanceof RemExpr) and + result = s1.rem(s2) + or + (e instanceof AssignAndExpr or e instanceof AndBitwiseExpr) and + result = s1.bitand(s2) + or + (e instanceof AssignOrExpr or e instanceof OrBitwiseExpr) and + result = s1.bitor(s2) + or + (e instanceof AssignXorExpr or e instanceof XorBitwiseExpr) and + result = s1.bitxor(s2) + or + (e instanceof AssignLShiftExpr or e instanceof LShiftExpr) and + result = s1.lshift(s2) + or + (e instanceof AssignRShiftExpr or e instanceof RShiftExpr) and + result = s1.rshift(s2) + or + (e instanceof AssignURShiftExpr or e instanceof URShiftExpr) and + result = s1.urshift(s2) + ) + or + result = exprSign(e.(ChooseExpr).getAResultExpr()) + or + result = exprSign(e.(CastExpr).getExpr()) + } + + private Sign binaryOpLhsSign(Expr e) { + result = exprSign(e.(BinaryExpr).getLeftOperand()) or + result = exprSign(e.(AssignOp).getDest()) + } + + private Sign binaryOpRhsSign(Expr e) { + result = exprSign(e.(BinaryExpr).getRightOperand()) or + result = exprSign(e.(AssignOp).getRhs()) + } + + pragma[noinline] + private predicate binaryOpSigns(Expr e, Sign lhs, Sign rhs) { + lhs = binaryOpLhsSign(e) and + rhs = binaryOpRhsSign(e) + } + + Expr getARead(SsaVariable v) { result = v.getAUse() } + + Field getField(FieldAccess fa) { result = fa.getField() } + + Expr getAnExpression(SsaReadPositionBlock bb) { result = bb.getBlock().getANode() } + + Guard getComparisonGuard(ComparisonExpr ce) { result = ce } +} diff --git a/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SsaReadPositionCommon.qll b/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SsaReadPositionCommon.qll new file mode 100644 index 00000000000..558ecd1b88b --- /dev/null +++ b/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SsaReadPositionCommon.qll @@ -0,0 +1,57 @@ +/** + * Provides classes for representing a position at which an SSA variable is read. + */ + +private import SsaReadPositionSpecific + +private newtype TSsaReadPosition = + TSsaReadPositionBlock(BasicBlock bb) { bb = getAReadBasicBlock(_) } or + TSsaReadPositionPhiInputEdge(BasicBlock bbOrig, BasicBlock bbPhi) { + exists(SsaPhiNode phi | phi.hasInputFromBlock(_, bbOrig) and bbPhi = phi.getBasicBlock()) + } + +/** + * A position at which an SSA variable is read. This includes both ordinary + * reads occurring in basic blocks and input to phi nodes occurring along an + * edge between two basic blocks. + */ +class SsaReadPosition extends TSsaReadPosition { + /** Holds if `v` is read at this position. */ + abstract predicate hasReadOfVar(SsaVariable v); + + /** Gets a textual representation of this SSA read position. */ + abstract string toString(); +} + +/** A basic block in which an SSA variable is read. */ +class SsaReadPositionBlock extends SsaReadPosition, TSsaReadPositionBlock { + /** Gets the basic block corresponding to this position. */ + BasicBlock getBlock() { this = TSsaReadPositionBlock(result) } + + override predicate hasReadOfVar(SsaVariable v) { getBlock() = getAReadBasicBlock(v) } + + override string toString() { result = "block" } +} + +/** + * An edge between two basic blocks where the latter block has an SSA phi + * definition. The edge therefore has a read of an SSA variable serving as the + * input to the phi node. + */ +class SsaReadPositionPhiInputEdge extends SsaReadPosition, TSsaReadPositionPhiInputEdge { + /** Gets the source of the edge. */ + BasicBlock getOrigBlock() { this = TSsaReadPositionPhiInputEdge(result, _) } + + /** Gets the target of the edge. */ + BasicBlock getPhiBlock() { this = TSsaReadPositionPhiInputEdge(_, result) } + + override predicate hasReadOfVar(SsaVariable v) { this.phiInput(_, v) } + + /** Holds if `inp` is an input to `phi` along this edge. */ + predicate phiInput(SsaPhiNode phi, SsaVariable inp) { + phi.hasInputFromBlock(inp, getOrigBlock()) and + getPhiBlock() = phi.getBasicBlock() + } + + override string toString() { result = "edge" } +} diff --git a/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SsaReadPositionSpecific.qll b/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SsaReadPositionSpecific.qll new file mode 100644 index 00000000000..dcfc3d69e32 --- /dev/null +++ b/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SsaReadPositionSpecific.qll @@ -0,0 +1,15 @@ +/** + * Provides Java-specific definitions for use in the `SsaReadPosition`. + */ + +private import semmle.code.java.dataflow.SSA as Ssa +private import semmle.code.java.controlflow.BasicBlocks as BB + +class SsaVariable = Ssa::SsaVariable; + +class SsaPhiNode = Ssa::SsaPhiNode; + +class BasicBlock = BB::BasicBlock; + +/** Gets a basic block in which SSA variable `v` is read. */ +BasicBlock getAReadBasicBlock(SsaVariable v) { result = v.getAUse().getBasicBlock() } diff --git a/java/ql/test/library-tests/dataflow/sign-analysis/SignAnalysis.expected b/java/ql/test/library-tests/dataflow/sign-analysis/SignAnalysis.expected index 1e3fe9acf27..a1dedfa95b1 100644 --- a/java/ql/test/library-tests/dataflow/sign-analysis/SignAnalysis.expected +++ b/java/ql/test/library-tests/dataflow/sign-analysis/SignAnalysis.expected @@ -1,3 +1,3 @@ -| A.java:4:14:4:14 | x | negative strictlyNegative | +| A.java:4:14:4:14 | x | strictlyNegative | | A.java:6:9:6:9 | x | positive | -| A.java:7:14:7:14 | y | positive strictlyPositive | +| A.java:7:14:7:14 | y | strictlyPositive | diff --git a/java/ql/test/library-tests/dataflow/sign-analysis/SignAnalysis.ql b/java/ql/test/library-tests/dataflow/sign-analysis/SignAnalysis.ql index 7dd564dd77d..bc4fed33dc8 100644 --- a/java/ql/test/library-tests/dataflow/sign-analysis/SignAnalysis.ql +++ b/java/ql/test/library-tests/dataflow/sign-analysis/SignAnalysis.ql @@ -1,17 +1,19 @@ import java import semmle.code.java.dataflow.SignAnalysis -string getASignString(Expr i) { - positive(i) and +string getASignString(Expr e) { + positive(e) and + not strictlyPositive(e) and result = "positive" or - negative(i) and + negative(e) and + not strictlyNegative(e) and result = "negative" or - strictlyPositive(i) and + strictlyPositive(e) and result = "strictlyPositive" or - strictlyNegative(i) and + strictlyNegative(e) and result = "strictlyNegative" }