зеркало из https://github.com/github/codeql.git
C#: Sign analysis
Synced between Java and C# through `identical-files.json`.
This commit is contained in:
Tamas Vajk
Родитель
441fbe3215
Коммит
8bf4a4209c
|
|
@ -50,6 +50,18 @@
|
||||||
"csharp/ql/src/semmle/code/csharp/dataflow/internal/DataFlowImplConsistency.qll",
|
"csharp/ql/src/semmle/code/csharp/dataflow/internal/DataFlowImplConsistency.qll",
|
||||||
"python/ql/src/experimental/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": [
|
"C++ SubBasicBlocks": [
|
||||||
"cpp/ql/src/semmle/code/cpp/controlflow/SubBasicBlocks.qll",
|
"cpp/ql/src/semmle/code/cpp/controlflow/SubBasicBlocks.qll",
|
||||||
"cpp/ql/src/semmle/code/cpp/dataflow/internal/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/unaliased_ssa/Operand.qll",
|
||||||
"cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_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/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": [
|
"IR IRType": [
|
||||||
"cpp/ql/src/semmle/code/cpp/ir/implementation/IRType.qll",
|
"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",
|
"cpp/ql/src/semmle/code/cpp/ir/implementation/internal/OperandTag.qll",
|
||||||
"csharp/ql/src/experimental/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",
|
"cpp/ql/src/semmle/code/cpp/ir/implementation/internal/TInstruction.qll",
|
||||||
"csharp/ql/src/experimental/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",
|
"cpp/ql/src/semmle/code/cpp/ir/implementation/internal/TIRVariable.qll",
|
||||||
"csharp/ql/src/experimental/ir/implementation/internal/TIRVariable.qll"
|
"csharp/ql/src/experimental/ir/implementation/internal/TIRVariable.qll"
|
||||||
],
|
],
|
||||||
|
|
@ -381,4 +393,4 @@
|
||||||
"javascript/ql/src/Comments/CommentedOutCodeReferences.qhelp",
|
"javascript/ql/src/Comments/CommentedOutCodeReferences.qhelp",
|
||||||
"python/ql/src/Lexical/CommentedOutCodeReferences.qhelp"
|
"python/ql/src/Lexical/CommentedOutCodeReferences.qhelp"
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
|
|
@ -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. */
|
/** A variable of type IEnumerable<T>, for some T. */
|
||||||
class IEnumerableSequence extends Variable {
|
class IEnumerableSequence extends Variable {
|
||||||
IEnumerableSequence() { isIEnumerableType(getType()) }
|
IEnumerableSequence() { isIEnumerableType(getType()) }
|
||||||
|
|
|
||||||
|
|
@ -2,7 +2,7 @@
|
||||||
* Provides classes for capturing various ways of performing comparison tests.
|
* 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
|
||||||
private import semmle.code.csharp.frameworks.system.Collections
|
private import semmle.code.csharp.frameworks.system.Collections
|
||||||
private import semmle.code.csharp.frameworks.system.collections.Generic
|
private import semmle.code.csharp.frameworks.system.collections.Generic
|
||||||
|
|
|
||||||
|
|
@ -31,6 +31,33 @@ class Guard extends Expr {
|
||||||
predicate controlsNode(ControlFlow::Nodes::ElementNode cfn, AccessOrCallExpr sub, AbstractValue v) {
|
predicate controlsNode(ControlFlow::Nodes::ElementNode cfn, AccessOrCallExpr sub, AbstractValue v) {
|
||||||
isGuardedByNode(cfn, this, sub, 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. */
|
/** An abstract value. */
|
||||||
|
|
|
||||||
|
|
@ -21,10 +21,8 @@ import csharp
|
||||||
private import ControlFlow
|
private import ControlFlow
|
||||||
private import internal.CallableReturns
|
private import internal.CallableReturns
|
||||||
private import semmle.code.csharp.commons.Assertions
|
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 as G
|
||||||
private import semmle.code.csharp.controlflow.Guards::AbstractValues
|
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.System
|
||||||
private import semmle.code.csharp.frameworks.Test
|
private import semmle.code.csharp.frameworks.Test
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -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() {
|
override string toString() {
|
||||||
result = getToStringPrefix(this) + "SSA phi(" + getSourceVariable() + ")"
|
result = getToStringPrefix(this) + "SSA phi(" + getSourceVariable() + ")"
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -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
|
||||||
|
|
@ -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) }
|
||||||
|
}
|
||||||
|
|
@ -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()
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
@ -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()
|
||||||
|
}
|
||||||
|
|
@ -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 }
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
@ -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" }
|
||||||
|
}
|
||||||
|
|
@ -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()
|
||||||
|
}
|
||||||
|
|
@ -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)
|
||||||
|
}
|
||||||
|
|
@ -57,6 +57,9 @@ class RelationalOperation extends ComparisonOperation, @rel_op_expr {
|
||||||
* `x <= 20` this is `x`, and on `y > 0` it is the `0`.
|
* `x <= 20` this is `x`, and on `y > 0` it is the `0`.
|
||||||
*/
|
*/
|
||||||
Expr getLesserOperand() { none() }
|
Expr getLesserOperand() { none() }
|
||||||
|
|
||||||
|
/** Holds if this comparison is strict, i.e. `<` or `>`. */
|
||||||
|
predicate isStrict() { this instanceof LTExpr or this instanceof GTExpr }
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
|
|
|
||||||
|
|
@ -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 |
|
||||||
|
|
@ -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
|
||||||
|
|
@ -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<int>();
|
||||||
|
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
|
||||||
|
|
@ -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 |
|
||||||
|
|
@ -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, " ")
|
||||||
|
|
@ -6,6 +6,7 @@
|
||||||
|
|
||||||
import java
|
import java
|
||||||
private import SSA
|
private import SSA
|
||||||
|
private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon
|
||||||
private import RangeUtils
|
private import RangeUtils
|
||||||
private import semmle.code.java.controlflow.Guards
|
private import semmle.code.java.controlflow.Guards
|
||||||
import Bound
|
import Bound
|
||||||
|
|
|
||||||
|
|
@ -66,6 +66,7 @@
|
||||||
import java
|
import java
|
||||||
private import SSA
|
private import SSA
|
||||||
private import RangeUtils
|
private import RangeUtils
|
||||||
|
private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon
|
||||||
private import semmle.code.java.controlflow.internal.GuardsLogic
|
private import semmle.code.java.controlflow.internal.GuardsLogic
|
||||||
private import SignAnalysis
|
private import SignAnalysis
|
||||||
private import ModulusAnalysis
|
private import ModulusAnalysis
|
||||||
|
|
|
||||||
|
|
@ -5,6 +5,7 @@
|
||||||
import java
|
import java
|
||||||
private import SSA
|
private import SSA
|
||||||
private import semmle.code.java.controlflow.internal.GuardsLogic
|
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
|
* 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)
|
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.
|
* Holds if `inp` is an input to `phi` along a back edge.
|
||||||
*/
|
*/
|
||||||
|
|
|
||||||
|
|
@ -6,596 +6,4 @@
|
||||||
* three-valued domain `{negative, zero, positive}`.
|
* three-valued domain `{negative, zero, positive}`.
|
||||||
*/
|
*/
|
||||||
|
|
||||||
import java
|
import semmle.code.java.dataflow.internal.rangeanalysis.SignAnalysisCommon
|
||||||
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()
|
|
||||||
}
|
|
||||||
|
|
|
||||||
|
|
@ -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()
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
@ -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()
|
||||||
|
}
|
||||||
|
|
@ -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 }
|
||||||
|
}
|
||||||
|
|
@ -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" }
|
||||||
|
}
|
||||||
|
|
@ -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() }
|
||||||
|
|
@ -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:6:9:6:9 | x | positive |
|
||||||
| A.java:7:14:7:14 | y | positive strictlyPositive |
|
| A.java:7:14:7:14 | y | strictlyPositive |
|
||||||
|
|
|
||||||
|
|
@ -1,17 +1,19 @@
|
||||||
import java
|
import java
|
||||||
import semmle.code.java.dataflow.SignAnalysis
|
import semmle.code.java.dataflow.SignAnalysis
|
||||||
|
|
||||||
string getASignString(Expr i) {
|
string getASignString(Expr e) {
|
||||||
positive(i) and
|
positive(e) and
|
||||||
|
not strictlyPositive(e) and
|
||||||
result = "positive"
|
result = "positive"
|
||||||
or
|
or
|
||||||
negative(i) and
|
negative(e) and
|
||||||
|
not strictlyNegative(e) and
|
||||||
result = "negative"
|
result = "negative"
|
||||||
or
|
or
|
||||||
strictlyPositive(i) and
|
strictlyPositive(e) and
|
||||||
result = "strictlyPositive"
|
result = "strictlyPositive"
|
||||||
or
|
or
|
||||||
strictlyNegative(i) and
|
strictlyNegative(e) and
|
||||||
result = "strictlyNegative"
|
result = "strictlyNegative"
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
Загрузка…
Ссылка в новой задаче