mirror of
https://github.com/github/codeql.git
synced 2025-12-20 10:46:30 +01:00
C#: Use CFG nodes instead of AST nodes in sign/modulus analysis
This commit is contained in:
Tom Hvitved
@@ -310,6 +310,22 @@ module ControlFlow {
|
||||
Split getASplit() { result = splits.getASplit() }
|
||||
}
|
||||
|
||||
/** A control-flow node for an expression. */
|
||||
class ExprNode extends ElementNode {
|
||||
Expr e;
|
||||
|
||||
ExprNode() { e = unique(Expr e_ | e_ = this.getElement() | e_) }
|
||||
|
||||
/** Gets the expression that this control-flow node belongs to. */
|
||||
Expr getExpr() { result = e }
|
||||
|
||||
/** Gets the value of this expression node, if any. */
|
||||
string getValue() { result = e.getValue() }
|
||||
|
||||
/** Gets the type of this expression node. */
|
||||
Type getType() { result = e.getType() }
|
||||
}
|
||||
|
||||
class Split = SplitImpl;
|
||||
|
||||
class FinallySplit = FinallySplitting::FinallySplitImpl;
|
||||
|
||||
@@ -111,18 +111,6 @@ private predicate evenlyDivisibleExpr(Expr e, int factor) {
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
|
||||
* in an arbitrary 1-based numbering of the input edges to `phi`.
|
||||
*/
|
||||
private predicate rankedPhiInput(
|
||||
SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, int r
|
||||
) {
|
||||
edge.phiInput(phi, inp) and
|
||||
edge =
|
||||
rank[r](SsaReadPositionPhiInputEdge e | e.phiInput(phi, _) | e order by getId(e.getOrigBlock()))
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `rix` is the number of input edges to `phi`.
|
||||
*/
|
||||
|
||||
@@ -6,4 +6,41 @@
|
||||
* three-valued domain `{negative, zero, positive}`.
|
||||
*/
|
||||
|
||||
import semmle.code.csharp.dataflow.internal.rangeanalysis.SignAnalysisCommon
|
||||
import csharp
|
||||
private import semmle.code.csharp.dataflow.internal.rangeanalysis.SignAnalysisCommon as Common
|
||||
|
||||
/** Holds if `e` can be positive and cannot be negative. */
|
||||
predicate positiveExpr(Expr e) {
|
||||
forex(ControlFlow::Node cfn | cfn = e.getAControlFlowNode() |
|
||||
positive(cfn) or strictlyPositive(cfn)
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if `e` can be negative and cannot be positive. */
|
||||
predicate negativeExpr(Expr e) {
|
||||
forex(ControlFlow::Node cfn | cfn = e.getAControlFlowNode() |
|
||||
negative(cfn) or strictlyNegative(cfn)
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if `e` is strictly positive. */
|
||||
predicate strictlyPositiveExpr(Expr e) {
|
||||
forex(ControlFlow::Node cfn | cfn = e.getAControlFlowNode() | strictlyPositive(cfn))
|
||||
}
|
||||
|
||||
/** Holds if `e` is strictly negative. */
|
||||
predicate strictlyNegativeExpr(Expr e) {
|
||||
forex(ControlFlow::Node cfn | cfn = e.getAControlFlowNode() | strictlyNegative(cfn))
|
||||
}
|
||||
|
||||
/** Holds if `e` can be positive and cannot be negative. */
|
||||
predicate positive(ControlFlow::Nodes::ExprNode e) { Common::positive(e) }
|
||||
|
||||
/** Holds if `e` can be negative and cannot be positive. */
|
||||
predicate negative(ControlFlow::Nodes::ExprNode e) { Common::negative(e) }
|
||||
|
||||
/** Holds if `e` is strictly positive. */
|
||||
predicate strictlyPositive(ControlFlow::Nodes::ExprNode e) { Common::strictlyPositive(e) }
|
||||
|
||||
/** Holds if `e` is strictly negative. */
|
||||
predicate strictlyNegative(ControlFlow::Nodes::ExprNode e) { Common::strictlyNegative(e) }
|
||||
|
||||
@@ -5,17 +5,16 @@
|
||||
private import csharp as CS
|
||||
private import semmle.code.csharp.dataflow.SSA::Ssa as Ssa
|
||||
private import semmle.code.csharp.dataflow.internal.rangeanalysis.ConstantUtils as CU
|
||||
private import semmle.code.csharp.dataflow.internal.rangeanalysis.RangeUtils as RU
|
||||
private import semmle.code.csharp.dataflow.internal.rangeanalysis.SsaUtils as SU
|
||||
|
||||
class SsaVariable extends Ssa::Definition {
|
||||
/** Gets a read of the source variable underlying this SSA definition. */
|
||||
Expr getAUse() { result = getARead() }
|
||||
}
|
||||
class SsaVariable = SU::SsaVariable;
|
||||
|
||||
class Expr = CS::Expr;
|
||||
class Expr = CS::ControlFlow::Nodes::ExprNode;
|
||||
|
||||
class IntegralType = CS::IntegralType;
|
||||
|
||||
class ConstantIntegerExpr = CU::ConstantIntegerExpr;
|
||||
|
||||
/** Holds if `e` is a bound expression and it is not an SSA variable read. */
|
||||
predicate interestingExprBound(Expr e) { CU::systemArrayLengthAccess(e.(CS::PropertyRead)) }
|
||||
predicate interestingExprBound(Expr e) { CU::systemArrayLengthAccess(e.getExpr()) }
|
||||
|
||||
@@ -4,18 +4,10 @@
|
||||
|
||||
private import csharp
|
||||
private import Ssa
|
||||
private import SsaUtils
|
||||
private import RangeUtils
|
||||
|
||||
/**
|
||||
* 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)
|
||||
)
|
||||
}
|
||||
private class ExprNode = ControlFlow::Nodes::ExprNode;
|
||||
|
||||
/**
|
||||
* Holds if `pa` is an access to the `Length` property of an array.
|
||||
@@ -30,40 +22,42 @@ predicate systemArrayLengthAccess(PropertyAccess pa) {
|
||||
* - 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) {
|
||||
private predicate constantIntegerExpr(ExprNode e, int val) {
|
||||
e.getValue().toInt() = val
|
||||
or
|
||||
exists(ExplicitDefinition v, Expr src |
|
||||
e = v.getARead() and
|
||||
src = v.getADefinition().getSource() and
|
||||
exists(ExprNode src |
|
||||
e = getAnExplicitDefinitionRead(src) and
|
||||
constantIntegerExpr(src, val)
|
||||
)
|
||||
or
|
||||
isArrayLengthAccess(e, val)
|
||||
}
|
||||
|
||||
private int getArrayLength(ArrayCreation arrCreation, int index) {
|
||||
constantIntegerExpr(arrCreation.getLengthArgument(index), result)
|
||||
private int getArrayLength(ExprNode e, int index) {
|
||||
exists(ArrayCreation arrCreation, ExprNode length |
|
||||
hasChild(arrCreation, arrCreation.getLengthArgument(index), e, length) and
|
||||
constantIntegerExpr(length, result)
|
||||
)
|
||||
}
|
||||
|
||||
private int getArrayLengthRec(ArrayCreation arrCreation, int index) {
|
||||
private int getArrayLengthRec(ExprNode 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) {
|
||||
systemArrayLengthAccess(pa) and
|
||||
exists(ExplicitDefinition arr, ArrayCreation arrCreation |
|
||||
getArrayLengthRec(arrCreation, arrCreation.getNumberOfLengthArguments() - 1) = length and
|
||||
arrCreation = arr.getADefinition().getSource() and
|
||||
pa.getQualifier() = arr.getARead()
|
||||
private predicate isArrayLengthAccess(ExprNode e, int length) {
|
||||
exists(PropertyAccess pa, ExprNode arrCreation |
|
||||
systemArrayLengthAccess(pa) and
|
||||
getArrayLengthRec(arrCreation,
|
||||
arrCreation.getExpr().(ArrayCreation).getNumberOfLengthArguments() - 1) = length and
|
||||
hasChild(pa, pa.getQualifier(), e, getAnExplicitDefinitionRead(arrCreation))
|
||||
)
|
||||
}
|
||||
|
||||
/** An expression that always has the same integer value. */
|
||||
class ConstantIntegerExpr extends Expr {
|
||||
class ConstantIntegerExpr extends ExprNode {
|
||||
ConstantIntegerExpr() { constantIntegerExpr(this, _) }
|
||||
|
||||
/** Gets the integer value of this expression. */
|
||||
|
||||
@@ -1,98 +1,39 @@
|
||||
module Private {
|
||||
private import csharp as CS
|
||||
private import ConstantUtils as CU
|
||||
private import semmle.code.csharp.controlflow.Guards as G
|
||||
private import semmle.code.csharp.dataflow.internal.rangeanalysis.RangeUtils as RU
|
||||
private import SsaUtils as SU
|
||||
private import SignAnalysisSpecific::Private as SA
|
||||
private import SsaReadPositionCommon
|
||||
|
||||
class BasicBlock = CS::Ssa::BasicBlock;
|
||||
|
||||
class SsaVariable extends CS::Ssa::Definition {
|
||||
CS::AssignableRead getAUse() { result = this.getARead() }
|
||||
}
|
||||
class SsaVariable = SU::SsaVariable;
|
||||
|
||||
class SsaPhiNode = CS::Ssa::PhiNode;
|
||||
|
||||
class Expr = CS::Expr;
|
||||
class Expr = CS::ControlFlow::Nodes::ExprNode;
|
||||
|
||||
class Guard = G::Guard;
|
||||
class Guard = RU::Guard;
|
||||
|
||||
class ConstantIntegerExpr = CU::ConstantIntegerExpr;
|
||||
|
||||
class ConditionalExpr extends CS::ConditionalExpr {
|
||||
/** Gets the "then" expression of this conditional expression. */
|
||||
Expr getTrueExpr() { result = this.getThen() }
|
||||
class ConditionalExpr = RU::ExprNode::ConditionalExpr;
|
||||
|
||||
/** Gets the "else" expression of this conditional expression. */
|
||||
Expr getFalseExpr() { result = this.getElse() }
|
||||
}
|
||||
class AddExpr = RU::ExprNode::AddExpr;
|
||||
|
||||
/** Represent an addition expression. */
|
||||
class AddExpr extends CS::AddExpr {
|
||||
/** Gets the LHS operand of this add expression. */
|
||||
Expr getLhs() { result = this.getLeftOperand() }
|
||||
class SubExpr = RU::ExprNode::SubExpr;
|
||||
|
||||
/** Gets the RHS operand of this add expression. */
|
||||
Expr getRhs() { result = this.getRightOperand() }
|
||||
}
|
||||
class RemExpr = RU::ExprNode::RemExpr;
|
||||
|
||||
/** Represent a subtraction expression. */
|
||||
class SubExpr extends CS::SubExpr {
|
||||
/** Gets the LHS operand of this subtraction expression. */
|
||||
Expr getLhs() { result = this.getLeftOperand() }
|
||||
class BitwiseAndExpr = RU::ExprNode::BitwiseAndExpr;
|
||||
|
||||
/** Gets the RHS operand of this subtraction expression. */
|
||||
Expr getRhs() { result = this.getRightOperand() }
|
||||
}
|
||||
class MulExpr = RU::ExprNode::MulExpr;
|
||||
|
||||
class RemExpr = CS::RemExpr;
|
||||
class LShiftExpr = RU::ExprNode::LShiftExpr;
|
||||
|
||||
/** Represent a bitwise and or an assign-and expression. */
|
||||
class BitwiseAndExpr extends CS::Expr {
|
||||
BitwiseAndExpr() { this instanceof CS::BitwiseAndExpr or this instanceof CS::AssignAndExpr }
|
||||
predicate guardDirectlyControlsSsaRead = RU::guardControlsSsaRead/3;
|
||||
|
||||
/** Gets an operand of this bitwise and operation. */
|
||||
Expr getAnOperand() {
|
||||
result = this.(CS::BitwiseAndExpr).getAnOperand() or
|
||||
result = this.(CS::AssignAndExpr).getRValue() or
|
||||
result = this.(CS::AssignAndExpr).getLValue()
|
||||
}
|
||||
|
||||
/** Holds if this expression has operands `e1` and `e2`. */
|
||||
predicate hasOperands(Expr e1, Expr e2) {
|
||||
this.getAnOperand() = e1 and
|
||||
this.getAnOperand() = e2 and
|
||||
e1 != e2
|
||||
}
|
||||
}
|
||||
|
||||
/** Represent a multiplication or an assign-mul expression. */
|
||||
class MulExpr extends CS::Expr {
|
||||
MulExpr() { this instanceof CS::MulExpr or this instanceof CS::AssignMulExpr }
|
||||
|
||||
/** Gets an operand of this multiplication. */
|
||||
Expr getAnOperand() {
|
||||
result = this.(CS::MulExpr).getAnOperand() or
|
||||
result = this.(CS::AssignMulExpr).getRValue() or
|
||||
result = this.(CS::AssignMulExpr).getLValue()
|
||||
}
|
||||
}
|
||||
|
||||
/** Represent a left shift or an assign-lshift expression. */
|
||||
class LShiftExpr extends CS::Expr {
|
||||
LShiftExpr() { this instanceof CS::LShiftExpr or this instanceof CS::AssignLShiftExpr }
|
||||
|
||||
/** Gets the RHS operand of this shift. */
|
||||
Expr getRhs() {
|
||||
result = this.(CS::LShiftExpr).getRightOperand() or
|
||||
result = this.(CS::AssignLShiftExpr).getRValue()
|
||||
}
|
||||
}
|
||||
|
||||
predicate guardDirectlyControlsSsaRead = SA::guardControlsSsaRead/3;
|
||||
|
||||
predicate guardControlsSsaRead = SA::guardControlsSsaRead/3;
|
||||
predicate guardControlsSsaRead = RU::guardControlsSsaRead/3;
|
||||
|
||||
predicate valueFlowStep = RU::valueFlowStep/3;
|
||||
|
||||
@@ -100,11 +41,44 @@ module Private {
|
||||
|
||||
predicate ssaUpdateStep = RU::ssaUpdateStep/3;
|
||||
|
||||
Expr getABasicBlockExpr(BasicBlock bb) { result = bb.getANode().getElement() }
|
||||
Expr getABasicBlockExpr(BasicBlock bb) { result = bb.getANode() }
|
||||
|
||||
private predicate id(CS::ControlFlowElement x, CS::ControlFlowElement y) { x = y }
|
||||
private class CallableOrCFE extends CS::Element {
|
||||
CallableOrCFE() { this instanceof CS::Callable or this instanceof CS::ControlFlowElement }
|
||||
}
|
||||
|
||||
private predicate idOf(CS::ControlFlowElement x, int y) = equivalenceRelation(id/2)(x, y)
|
||||
private predicate id(CallableOrCFE x, CallableOrCFE y) { x = y }
|
||||
|
||||
int getId(BasicBlock bb) { idOf(bb.getFirstNode().getElement(), result) }
|
||||
private predicate idOf(CallableOrCFE x, int y) = equivalenceRelation(id/2)(x, y)
|
||||
|
||||
private class PhiInputEdgeBlock extends BasicBlock {
|
||||
PhiInputEdgeBlock() { this = any(SsaReadPositionPhiInputEdge edge).getOrigBlock() }
|
||||
}
|
||||
|
||||
int getId(PhiInputEdgeBlock bb) {
|
||||
idOf(bb.getFirstNode().getElement(), result)
|
||||
or
|
||||
idOf(bb.(CS::ControlFlow::BasicBlocks::EntryBlock).getCallable(), result)
|
||||
}
|
||||
|
||||
private string getSplitString(PhiInputEdgeBlock bb) {
|
||||
result = bb.getFirstNode().(CS::ControlFlow::Nodes::ElementNode).getSplitsString()
|
||||
or
|
||||
not exists(bb.getFirstNode().(CS::ControlFlow::Nodes::ElementNode).getSplitsString()) and
|
||||
result = ""
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
|
||||
* in an arbitrary 1-based numbering of the input edges to `phi`.
|
||||
*/
|
||||
predicate rankedPhiInput(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, int r) {
|
||||
edge.phiInput(phi, inp) and
|
||||
edge =
|
||||
rank[r](SsaReadPositionPhiInputEdge e |
|
||||
e.phiInput(phi, _)
|
||||
|
|
||||
e order by getId(e.getOrigBlock()), getSplitString(e.getOrigBlock())
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
@@ -1,98 +1,406 @@
|
||||
/**
|
||||
* Provides predicates for range and modulus analysis.
|
||||
*/
|
||||
private module Impl {
|
||||
private import csharp
|
||||
private import Ssa
|
||||
private import SsaUtils
|
||||
private import ConstantUtils
|
||||
private import SsaReadPositionCommon
|
||||
private import semmle.code.csharp.controlflow.Guards as G
|
||||
private import ControlFlowReachability
|
||||
|
||||
private import csharp
|
||||
private import Ssa
|
||||
private import SsaUtils
|
||||
private import ConstantUtils
|
||||
private import SsaReadPositionCommon
|
||||
private import semmle.code.csharp.controlflow.Guards as G
|
||||
private class BooleanValue = G::AbstractValues::BooleanValue;
|
||||
|
||||
private class BooleanValue = G::AbstractValues::BooleanValue;
|
||||
private class ExprNode = ControlFlow::Nodes::ExprNode;
|
||||
|
||||
/**
|
||||
* Holds if `v` is an `ExplicitDefinition` that equals `e + delta`.
|
||||
*/
|
||||
predicate ssaUpdateStep(ExplicitDefinition v, Expr e, int delta) {
|
||||
v.getADefinition().getExpr().(Assignment).getRValue() = e and delta = 0
|
||||
or
|
||||
v.getADefinition().getExpr().(PostIncrExpr).getOperand() = e and delta = 1
|
||||
or
|
||||
v.getADefinition().getExpr().(PreIncrExpr).getOperand() = e and delta = 1
|
||||
or
|
||||
v.getADefinition().getExpr().(PostDecrExpr).getOperand() = e and delta = -1
|
||||
or
|
||||
v.getADefinition().getExpr().(PreDecrExpr).getOperand() = e and delta = -1
|
||||
}
|
||||
private class ExprChildReachability extends ControlFlowReachabilityConfiguration {
|
||||
ExprChildReachability() { this = "ExprChildReachability" }
|
||||
|
||||
private G::Guard eqFlowCondAbs(Definition def, Expr e, int delta, boolean isEq, G::AbstractValue v) {
|
||||
exists(boolean eqpolarity |
|
||||
result.isEquality(ssaRead(def, delta), e, eqpolarity) and
|
||||
eqpolarity.booleanXor(v.(BooleanValue).getValue()).booleanNot() = isEq
|
||||
)
|
||||
or
|
||||
exists(G::AbstractValue v0 |
|
||||
G::Internal::impliesSteps(result, v, eqFlowCondAbs(def, e, delta, isEq, v0), v0)
|
||||
)
|
||||
}
|
||||
override predicate candidate(
|
||||
Expr e1, Expr e2, ControlFlowElement scope, boolean exactScope, boolean isSuccessor
|
||||
) {
|
||||
e2 = e1.getAChild() and
|
||||
scope = e1 and
|
||||
exactScope = false and
|
||||
isSuccessor in [false, true]
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets a condition that tests whether `def` equals `e + delta`.
|
||||
*
|
||||
* If the condition evaluates to `testIsTrue`:
|
||||
* - `isEq = true` : `def == e + delta`
|
||||
* - `isEq = false` : `def != e + delta`
|
||||
*/
|
||||
G::Guard eqFlowCond(Definition def, Expr e, int delta, boolean isEq, boolean testIsTrue) {
|
||||
exists(BooleanValue v |
|
||||
result = eqFlowCondAbs(def, e, delta, isEq, v) and
|
||||
testIsTrue = v.getValue()
|
||||
)
|
||||
}
|
||||
/** Holds if `parent` having child `child` implies `parentNode` having child `childNode`. */
|
||||
predicate hasChild(Expr parent, Expr child, ExprNode parentNode, ExprNode childNode) {
|
||||
any(ExprChildReachability x).hasExprPath(parent, parentNode, child, childNode)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `e1 + delta` equals `e2`.
|
||||
*/
|
||||
predicate valueFlowStep(Expr e2, Expr e1, int delta) {
|
||||
valueFlowStep(e2.(AssignOperation).getExpandedAssignment(), e1, delta)
|
||||
or
|
||||
e2.(AssignExpr).getRValue() = e1 and delta = 0
|
||||
or
|
||||
e2.(UnaryPlusExpr).getOperand() = e1 and delta = 0
|
||||
or
|
||||
e2.(PostIncrExpr).getOperand() = e1 and delta = 0
|
||||
or
|
||||
e2.(PostDecrExpr).getOperand() = e1 and delta = 0
|
||||
or
|
||||
e2.(PreIncrExpr).getOperand() = e1 and delta = 1
|
||||
or
|
||||
e2.(PreDecrExpr).getOperand() = e1 and delta = -1
|
||||
or
|
||||
exists(ConstantIntegerExpr x |
|
||||
e2.(AddExpr).getAnOperand() = e1 and
|
||||
e2.(AddExpr).getAnOperand() = x and
|
||||
not e1 = x
|
||||
|
|
||||
x.getIntValue() = delta
|
||||
)
|
||||
or
|
||||
exists(ConstantIntegerExpr x |
|
||||
exists(SubExpr sub |
|
||||
e2 = sub and
|
||||
sub.getLeftOperand() = e1 and
|
||||
sub.getRightOperand() = x
|
||||
/** Holds if SSA definition `def` equals `e + delta`. */
|
||||
predicate ssaUpdateStep(ExplicitDefinition def, ExprNode e, int delta) {
|
||||
exists(ControlFlow::Node cfn | cfn = def.getControlFlowNode() |
|
||||
e = cfn.(ExprNode::Assignment).getRValue() and delta = 0
|
||||
or
|
||||
e = cfn.(ExprNode::PostIncrExpr).getOperand() and delta = 1
|
||||
or
|
||||
e = cfn.(ExprNode::PreIncrExpr).getOperand() and delta = 1
|
||||
or
|
||||
e = cfn.(ExprNode::PostDecrExpr).getOperand() and delta = -1
|
||||
or
|
||||
e = cfn.(ExprNode::PreDecrExpr).getOperand() and delta = -1
|
||||
)
|
||||
|
|
||||
x.getIntValue() = -delta
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if `e1 + delta` equals `e2`. */
|
||||
predicate valueFlowStep(ExprNode e2, ExprNode e1, int delta) {
|
||||
e2.(ExprNode::AssignExpr).getRValue() = e1 and delta = 0
|
||||
or
|
||||
e2.(ExprNode::UnaryPlusExpr).getOperand() = e1 and delta = 0
|
||||
or
|
||||
e2.(ExprNode::PostIncrExpr).getOperand() = e1 and delta = 0
|
||||
or
|
||||
e2.(ExprNode::PostDecrExpr).getOperand() = e1 and delta = 0
|
||||
or
|
||||
e2.(ExprNode::PreIncrExpr).getOperand() = e1 and delta = 1
|
||||
or
|
||||
e2.(ExprNode::PreDecrExpr).getOperand() = e1 and delta = -1
|
||||
or
|
||||
exists(ConstantIntegerExpr x |
|
||||
e2.(ExprNode::AddExpr).getAnOperand() = e1 and
|
||||
e2.(ExprNode::AddExpr).getAnOperand() = x and
|
||||
e1 != x and
|
||||
x.getIntValue() = delta
|
||||
)
|
||||
or
|
||||
exists(ConstantIntegerExpr x |
|
||||
e2.(ExprNode::SubExpr).getLeftOperand() = e1 and
|
||||
e2.(ExprNode::SubExpr).getRightOperand() = x and
|
||||
x.getIntValue() = -delta
|
||||
)
|
||||
}
|
||||
|
||||
/** An expression whose value may control the execution of another element. */
|
||||
class Guard extends Expr {
|
||||
Guard() { this instanceof G::Guard }
|
||||
|
||||
/**
|
||||
* Holds if basic block `bb` is guarded by this guard having value `v`.
|
||||
*/
|
||||
predicate controlsBasicBlock(BasicBlock bb, G::AbstractValue v) {
|
||||
this.(G::Guard).controlsBasicBlock(bb, v)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if this 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(ExprNode e1, ExprNode e2, boolean polarity) {
|
||||
exists(Expr e1_, Expr e2_ |
|
||||
e1 = unique(ExprNode cfn | hasChild(this, e1_, _, cfn) | cfn) and
|
||||
e2 = unique(ExprNode cfn | hasChild(this, e2_, _, cfn) | cfn) and
|
||||
this.(G::Guard).isEquality(e1_, e2_, polarity)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
private Guard eqFlowCondAbs(
|
||||
Definition def, ExprNode e, int delta, boolean isEq, G::AbstractValue v
|
||||
) {
|
||||
exists(boolean eqpolarity |
|
||||
result.isEquality(ssaRead(def, delta), e, eqpolarity) and
|
||||
eqpolarity.booleanXor(v.(BooleanValue).getValue()).booleanNot() = isEq
|
||||
)
|
||||
or
|
||||
exists(G::AbstractValue v0 |
|
||||
G::Internal::impliesSteps(result, v, eqFlowCondAbs(def, e, delta, isEq, v0), v0)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets a condition that tests whether `def` equals `e + delta`.
|
||||
*
|
||||
* If the condition evaluates to `testIsTrue`:
|
||||
* - `isEq = true` : `def == e + delta`
|
||||
* - `isEq = false` : `def != e + delta`
|
||||
*/
|
||||
Guard eqFlowCond(Definition def, ExprNode e, int delta, boolean isEq, boolean testIsTrue) {
|
||||
exists(BooleanValue v |
|
||||
result = eqFlowCondAbs(def, e, delta, isEq, v) and
|
||||
testIsTrue = v.getValue()
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* 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.controlsBasicBlock(controlled.(SsaReadPositionBlock).getBlock(), b)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* 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)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
import Impl
|
||||
|
||||
/**
|
||||
* Holds if `guard` controls the position `controlled` with the value `testIsTrue`.
|
||||
* Provides classes for mapping CFG nodes to AST nodes, in a way that respects
|
||||
* control-flow splitting. For example, in
|
||||
*
|
||||
* ```csharp
|
||||
* int M(bool b)
|
||||
* {
|
||||
* var i = b ? 1 : -1;
|
||||
* i = i - 1;
|
||||
* if (b)
|
||||
* return 0;
|
||||
* return i;
|
||||
* }
|
||||
* ```
|
||||
* the subtraction `i - 1` exists in two copies in the CFG. The class `SubExpr`
|
||||
* contains each copy, with split-respecting `getLeft/RightOperand()` predicates.
|
||||
*/
|
||||
predicate guardControlsSsaRead(G::Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
|
||||
exists(BooleanValue b | b.getValue() = testIsTrue |
|
||||
guard.controlsBasicBlock(controlled.(SsaReadPositionBlock).getBlock(), b)
|
||||
)
|
||||
module ExprNode {
|
||||
private import csharp as CS
|
||||
|
||||
private class ExprNode = CS::ControlFlow::Nodes::ExprNode;
|
||||
|
||||
private import Sign
|
||||
|
||||
/** An assignable access. */
|
||||
class AssignableAccess extends ExprNode {
|
||||
override CS::AssignableAccess e;
|
||||
}
|
||||
|
||||
/** A field access. */
|
||||
class FieldAccess extends ExprNode {
|
||||
override CS::FieldAccess e;
|
||||
}
|
||||
|
||||
/** A character literal. */
|
||||
class CharLiteral extends ExprNode {
|
||||
override CS::CharLiteral e;
|
||||
}
|
||||
|
||||
/** An integer literal. */
|
||||
class IntegerLiteral extends ExprNode {
|
||||
override CS::IntegerLiteral e;
|
||||
}
|
||||
|
||||
/** A long literal. */
|
||||
class LongLiteral extends ExprNode {
|
||||
override CS::LongLiteral e;
|
||||
}
|
||||
|
||||
/** A cast. */
|
||||
class CastExpr extends ExprNode {
|
||||
override CS::CastExpr e;
|
||||
|
||||
/** Gets the source type of this cast. */
|
||||
CS::Type getSourceType() { result = e.getSourceType() }
|
||||
}
|
||||
|
||||
/** A floating point literal. */
|
||||
class RealLiteral extends ExprNode {
|
||||
override CS::RealLiteral e;
|
||||
}
|
||||
|
||||
/** An assignment. */
|
||||
class Assignment extends ExprNode {
|
||||
override CS::Assignment e;
|
||||
|
||||
/** Gets the left operand of this assignment. */
|
||||
ExprNode getLValue() {
|
||||
result = unique(ExprNode res | hasChild(e, e.getLValue(), this, res) | res)
|
||||
}
|
||||
|
||||
/** Gets the right operand of this assignment. */
|
||||
ExprNode getRValue() {
|
||||
result = unique(ExprNode res | hasChild(e, e.getRValue(), this, res) | res)
|
||||
}
|
||||
}
|
||||
|
||||
/** A simple assignment. */
|
||||
class AssignExpr extends Assignment {
|
||||
override CS::AssignExpr e;
|
||||
}
|
||||
|
||||
/** A unary operation. */
|
||||
class UnaryOperation extends ExprNode {
|
||||
override CS::UnaryOperation e;
|
||||
|
||||
/** Returns the operand of this unary operation. */
|
||||
ExprNode getOperand() {
|
||||
result = unique(ExprNode res | hasChild(e, e.getOperand(), this, res) | res)
|
||||
}
|
||||
|
||||
/** Returns the operation representing this unary operation. */
|
||||
TUnarySignOperation getOp() { none() }
|
||||
}
|
||||
|
||||
/** A prefix increment operation. */
|
||||
class PreIncrExpr extends UnaryOperation {
|
||||
override CS::PreIncrExpr e;
|
||||
|
||||
override TIncOp getOp() { any() }
|
||||
}
|
||||
|
||||
/** A postfix increment operation. */
|
||||
class PostIncrExpr extends UnaryOperation {
|
||||
override CS::PostIncrExpr e;
|
||||
}
|
||||
|
||||
/** A prefix decrement operation. */
|
||||
class PreDecrExpr extends UnaryOperation {
|
||||
override CS::PreDecrExpr e;
|
||||
|
||||
override TDecOp getOp() { any() }
|
||||
}
|
||||
|
||||
/** A postfix decrement operation. */
|
||||
class PostDecrExpr extends UnaryOperation {
|
||||
override CS::PostDecrExpr e;
|
||||
}
|
||||
|
||||
/** A unary plus operation. */
|
||||
class UnaryPlusExpr extends UnaryOperation {
|
||||
override CS::UnaryPlusExpr e;
|
||||
}
|
||||
|
||||
/** A unary minus operation. */
|
||||
class UnaryMinusExpr extends UnaryOperation {
|
||||
override CS::UnaryMinusExpr e;
|
||||
|
||||
override TNegOp getOp() { any() }
|
||||
}
|
||||
|
||||
/** A bitwise complement operation. */
|
||||
class ComplementExpr extends UnaryOperation {
|
||||
override CS::ComplementExpr e;
|
||||
|
||||
override TBitNotOp getOp() { any() }
|
||||
}
|
||||
|
||||
/** A binary operation. */
|
||||
class BinaryOperation extends ExprNode {
|
||||
override CS::BinaryOperation e;
|
||||
|
||||
/** Returns the operation representing this binary operation. */
|
||||
TBinarySignOperation getOp() { none() }
|
||||
|
||||
/** Gets the left operand of this binary operation. */
|
||||
ExprNode getLeftOperand() {
|
||||
result = unique(ExprNode res | hasChild(e, e.getLeftOperand(), this, res) | res)
|
||||
}
|
||||
|
||||
/** Gets the right operand of this binary operation. */
|
||||
ExprNode getRightOperand() {
|
||||
result = unique(ExprNode res | hasChild(e, e.getRightOperand(), this, res) | res)
|
||||
}
|
||||
|
||||
/** Gets the left operand of this binary operation. */
|
||||
ExprNode getLhs() { result = this.getLeftOperand() }
|
||||
|
||||
/** Gets the right operand of this binary operation. */
|
||||
ExprNode getRhs() { result = this.getRightOperand() }
|
||||
|
||||
/** Gets an operand of this binary operation. */
|
||||
ExprNode getAnOperand() { hasChild(e, e.getAnOperand(), this, result) }
|
||||
|
||||
/** Holds if this binary operation has operands `e1` and `e2`. */
|
||||
predicate hasOperands(ExprNode e1, ExprNode e2) {
|
||||
this.getAnOperand() = e1 and
|
||||
this.getAnOperand() = e2 and
|
||||
e1 != e2
|
||||
}
|
||||
}
|
||||
|
||||
/** An addition operation. */
|
||||
class AddExpr extends BinaryOperation {
|
||||
override CS::AddExpr e;
|
||||
|
||||
override TAddOp getOp() { any() }
|
||||
}
|
||||
|
||||
/** A subtraction operation. */
|
||||
class SubExpr extends BinaryOperation {
|
||||
override CS::SubExpr e;
|
||||
|
||||
override TSubOp getOp() { any() }
|
||||
}
|
||||
|
||||
/** A multiplication operation. */
|
||||
class MulExpr extends BinaryOperation {
|
||||
override CS::MulExpr e;
|
||||
|
||||
override TMulOp getOp() { any() }
|
||||
}
|
||||
|
||||
/** A division operation. */
|
||||
class DivExpr extends BinaryOperation {
|
||||
override CS::DivExpr e;
|
||||
|
||||
override TDivOp getOp() { any() }
|
||||
}
|
||||
|
||||
/** A remainder operation. */
|
||||
class RemExpr extends BinaryOperation {
|
||||
override CS::RemExpr e;
|
||||
|
||||
override TRemOp getOp() { any() }
|
||||
}
|
||||
|
||||
/** A bitwise-and operation. */
|
||||
class BitwiseAndExpr extends BinaryOperation {
|
||||
override CS::BitwiseAndExpr e;
|
||||
|
||||
override TBitAndOp getOp() { any() }
|
||||
}
|
||||
|
||||
/** A bitwise-or operation. */
|
||||
class BitwiseOrExpr extends BinaryOperation {
|
||||
override CS::BitwiseOrExpr e;
|
||||
|
||||
override TBitOrOp getOp() { any() }
|
||||
}
|
||||
|
||||
/** A bitwise-xor operation. */
|
||||
class BitwiseXorExpr extends BinaryOperation {
|
||||
override CS::BitwiseXorExpr e;
|
||||
|
||||
override TBitXorOp getOp() { any() }
|
||||
}
|
||||
|
||||
/** A left-shift operation. */
|
||||
class LShiftExpr extends BinaryOperation {
|
||||
override CS::LShiftExpr e;
|
||||
|
||||
override TLShiftOp getOp() { any() }
|
||||
}
|
||||
|
||||
/** A right-shift operation. */
|
||||
class RShiftExpr extends BinaryOperation {
|
||||
override CS::RShiftExpr e;
|
||||
|
||||
override TRShiftOp getOp() { any() }
|
||||
}
|
||||
|
||||
/** A conditional expression. */
|
||||
class ConditionalExpr extends ExprNode {
|
||||
override CS::ConditionalExpr e;
|
||||
|
||||
/** Gets the "then" expression of this conditional expression. */
|
||||
ExprNode getTrueExpr() { hasChild(e, e.getThen(), this, result) }
|
||||
|
||||
/** Gets the "else" expression of this conditional expression. */
|
||||
ExprNode getFalseExpr() { hasChild(e, e.getElse(), this, result) }
|
||||
}
|
||||
}
|
||||
|
||||
@@ -51,7 +51,7 @@ private predicate unknownSign(Expr e) {
|
||||
or
|
||||
exists(CastExpr cast, Type fromtyp |
|
||||
cast = e and
|
||||
fromtyp = cast.getExpr().getType() and
|
||||
fromtyp = cast.getSourceType() and
|
||||
not fromtyp instanceof NumericOrCharType
|
||||
)
|
||||
or
|
||||
|
||||
@@ -6,11 +6,10 @@ module Private {
|
||||
private import SsaUtils as SU
|
||||
private import ConstantUtils as CU
|
||||
private import RangeUtils as RU
|
||||
private import semmle.code.csharp.controlflow.Guards as G
|
||||
private import Sign
|
||||
import Impl
|
||||
|
||||
class Guard = G::Guard;
|
||||
class Guard = RU::Guard;
|
||||
|
||||
class ConstantIntegerExpr = CU::ConstantIntegerExpr;
|
||||
|
||||
@@ -18,97 +17,33 @@ module Private {
|
||||
|
||||
class SsaPhiNode = CS::Ssa::PhiNode;
|
||||
|
||||
class VarAccess = CS::AssignableAccess;
|
||||
class VarAccess = RU::ExprNode::AssignableAccess;
|
||||
|
||||
class FieldAccess = CS::FieldAccess;
|
||||
class FieldAccess = RU::ExprNode::FieldAccess;
|
||||
|
||||
class CharacterLiteral = CS::CharLiteral;
|
||||
class CharacterLiteral = RU::ExprNode::CharLiteral;
|
||||
|
||||
class IntegerLiteral = CS::IntegerLiteral;
|
||||
class IntegerLiteral = RU::ExprNode::IntegerLiteral;
|
||||
|
||||
class LongLiteral = CS::LongLiteral;
|
||||
class LongLiteral = RU::ExprNode::LongLiteral;
|
||||
|
||||
class CastExpr = CS::CastExpr;
|
||||
class CastExpr = RU::ExprNode::CastExpr;
|
||||
|
||||
class Type = CS::Type;
|
||||
|
||||
class Expr = CS::Expr;
|
||||
class Expr = CS::ControlFlow::Nodes::ExprNode;
|
||||
|
||||
class VariableUpdate = CS::AssignableDefinition;
|
||||
class VariableUpdate = CS::Ssa::ExplicitDefinition;
|
||||
|
||||
class Field = CS::Field;
|
||||
|
||||
class RealLiteral = CS::RealLiteral;
|
||||
class RealLiteral = RU::ExprNode::RealLiteral;
|
||||
|
||||
class DivExpr = CS::DivExpr;
|
||||
class DivExpr = RU::ExprNode::DivExpr;
|
||||
|
||||
/** Class to represent unary operation. */
|
||||
class UnaryOperation extends Expr {
|
||||
UnaryOperation() {
|
||||
this instanceof CS::PreIncrExpr or
|
||||
this instanceof CS::PreDecrExpr or
|
||||
this instanceof CS::UnaryMinusExpr or
|
||||
this instanceof CS::ComplementExpr
|
||||
}
|
||||
class UnaryOperation = RU::ExprNode::UnaryOperation;
|
||||
|
||||
/** Returns the operand of this expression. */
|
||||
Expr getOperand() {
|
||||
result = this.(CS::PreIncrExpr).getOperand() or
|
||||
result = this.(CS::PreDecrExpr).getOperand() or
|
||||
result = this.(CS::UnaryMinusExpr).getOperand() or
|
||||
result = this.(CS::ComplementExpr).getOperand()
|
||||
}
|
||||
|
||||
/** Returns the operation representing this expression. */
|
||||
TUnarySignOperation getOp() {
|
||||
this instanceof CS::PreIncrExpr and result = TIncOp()
|
||||
or
|
||||
this instanceof CS::PreDecrExpr and result = TDecOp()
|
||||
or
|
||||
this instanceof CS::UnaryMinusExpr and result = TNegOp()
|
||||
or
|
||||
this instanceof CS::ComplementExpr and result = TBitNotOp()
|
||||
}
|
||||
}
|
||||
|
||||
/** Class to represent binary operation. */
|
||||
class BinaryOperation extends CS::BinaryOperation {
|
||||
BinaryOperation() {
|
||||
this instanceof CS::AddExpr or
|
||||
this instanceof CS::SubExpr or
|
||||
this instanceof CS::MulExpr or
|
||||
this instanceof CS::DivExpr or
|
||||
this instanceof CS::RemExpr or
|
||||
this instanceof CS::BitwiseAndExpr or
|
||||
this instanceof CS::BitwiseOrExpr or
|
||||
this instanceof CS::BitwiseXorExpr or
|
||||
this instanceof CS::LShiftExpr or
|
||||
this instanceof CS::RShiftExpr
|
||||
}
|
||||
|
||||
/** Returns the operation representing this expression. */
|
||||
TBinarySignOperation getOp() {
|
||||
this instanceof CS::AddExpr and result = TAddOp()
|
||||
or
|
||||
this instanceof CS::SubExpr and result = TSubOp()
|
||||
or
|
||||
this instanceof CS::MulExpr and result = TMulOp()
|
||||
or
|
||||
this instanceof CS::DivExpr and result = TDivOp()
|
||||
or
|
||||
this instanceof CS::RemExpr and result = TRemOp()
|
||||
or
|
||||
this instanceof CS::BitwiseAndExpr and result = TBitAndOp()
|
||||
or
|
||||
this instanceof CS::BitwiseOrExpr and result = TBitOrOp()
|
||||
or
|
||||
this instanceof CS::BitwiseXorExpr and result = TBitXorOp()
|
||||
or
|
||||
this instanceof CS::LShiftExpr and result = TLShiftOp()
|
||||
or
|
||||
this instanceof CS::RShiftExpr and result = TRShiftOp()
|
||||
}
|
||||
}
|
||||
class BinaryOperation = RU::ExprNode::BinaryOperation;
|
||||
|
||||
predicate ssaRead = SU::ssaRead/2;
|
||||
|
||||
@@ -118,21 +53,21 @@ module Private {
|
||||
private module Impl {
|
||||
private import csharp
|
||||
private import SsaUtils
|
||||
private import RangeUtils
|
||||
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;
|
||||
private class ExprNode = ControlFlow::Nodes::ExprNode;
|
||||
|
||||
/** Gets the character value of expression `e`. */
|
||||
string getCharValue(Expr e) { result = e.getValue() and e.getType() instanceof CharType }
|
||||
string getCharValue(ExprNode e) { result = e.getValue() and e.getType() instanceof CharType }
|
||||
|
||||
/** Gets the constant `float` value of non-`ConstantIntegerExpr` expressions. */
|
||||
float getNonIntegerValue(Expr e) {
|
||||
float getNonIntegerValue(ExprNode e) {
|
||||
exists(string s |
|
||||
s = e.getValue() and
|
||||
result = s.toFloat() and
|
||||
@@ -144,19 +79,19 @@ private module Impl {
|
||||
* Holds if `e` is an access to the size of a container (`string`, `Array`,
|
||||
* `IEnumerable`, or `ICollection`).
|
||||
*/
|
||||
predicate containerSizeAccess(Expr e) {
|
||||
exists(Property p | p = e.(PropertyAccess).getTarget() |
|
||||
predicate containerSizeAccess(ExprNode e) {
|
||||
exists(Property p | p = e.getExpr().(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
|
||||
e.getExpr() instanceof CountCall
|
||||
}
|
||||
|
||||
/** Holds if `e` is by definition strictly positive. */
|
||||
predicate positiveExpression(Expr e) { e instanceof SizeofExpr }
|
||||
predicate positiveExpression(ExprNode e) { e.getExpr() instanceof SizeofExpr }
|
||||
|
||||
abstract class NumericOrCharType extends Type { }
|
||||
|
||||
@@ -185,43 +120,48 @@ private module Impl {
|
||||
}
|
||||
|
||||
/** Returns the underlying variable update of the explicit SSA variable `v`. */
|
||||
AssignableDefinition getExplicitSsaAssignment(Ssa::ExplicitDefinition v) {
|
||||
result = v.getADefinition()
|
||||
}
|
||||
Ssa::ExplicitDefinition getExplicitSsaAssignment(Ssa::ExplicitDefinition v) { result = v }
|
||||
|
||||
/** Returns the assignment of the variable update `def`. */
|
||||
Expr getExprFromSsaAssignment(AssignableDefinition def) { result = def.getSource() }
|
||||
ExprNode getExprFromSsaAssignment(Ssa::ExplicitDefinition def) {
|
||||
exists(AssignableDefinition adef |
|
||||
adef = def.getADefinition() and
|
||||
hasChild(adef.getExpr(), adef.getSource(), def.getControlFlowNode(), result)
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if `def` can have any sign. */
|
||||
predicate explicitSsaDefWithAnySign(AssignableDefinition def) {
|
||||
not exists(def.getSource()) and
|
||||
predicate explicitSsaDefWithAnySign(Ssa::ExplicitDefinition def) {
|
||||
not exists(def.getADefinition().getSource()) and
|
||||
not def.getElement() instanceof MutatorOperation
|
||||
}
|
||||
|
||||
/** Returns the operand of the operation if `def` is a decrement. */
|
||||
Expr getDecrementOperand(AssignableDefinition def) {
|
||||
result = def.getElement().(DecrementOperation).getOperand()
|
||||
ExprNode getDecrementOperand(Ssa::ExplicitDefinition def) {
|
||||
hasChild(def.getElement(), def.getElement().(DecrementOperation).getOperand(),
|
||||
def.getControlFlowNode(), result)
|
||||
}
|
||||
|
||||
/** Returns the operand of the operation if `def` is an increment. */
|
||||
Expr getIncrementOperand(AssignableDefinition def) {
|
||||
result = def.getElement().(IncrementOperation).getOperand()
|
||||
ExprNode getIncrementOperand(Ssa::ExplicitDefinition def) {
|
||||
hasChild(def.getElement(), def.getElement().(IncrementOperation).getOperand(),
|
||||
def.getControlFlowNode(), result)
|
||||
}
|
||||
|
||||
/** Gets the variable underlying the implicit SSA variable `v`. */
|
||||
Declaration getImplicitSsaDeclaration(Ssa::ImplicitDefinition v) {
|
||||
result = v.getSourceVariable().getAssignable()
|
||||
/** Gets the variable underlying the implicit SSA variable `def`. */
|
||||
Declaration getImplicitSsaDeclaration(Ssa::ImplicitDefinition def) {
|
||||
result = def.getSourceVariable().getAssignable()
|
||||
}
|
||||
|
||||
/** Holds if the variable underlying the implicit SSA variable `v` is not a field. */
|
||||
predicate nonFieldImplicitSsaDefinition(Ssa::ImplicitDefinition v) {
|
||||
not getImplicitSsaDeclaration(v) instanceof Field
|
||||
/** Holds if the variable underlying the implicit SSA variable `def` is not a field. */
|
||||
predicate nonFieldImplicitSsaDefinition(Ssa::ImplicitDefinition def) {
|
||||
not getImplicitSsaDeclaration(def) instanceof Field
|
||||
}
|
||||
|
||||
/** Returned an expression that is assigned to `f`. */
|
||||
Expr getAssignedValueToField(Field f) {
|
||||
result = f.getAnAssignedValue() or
|
||||
result = any(AssignOperation a | a.getLValue() = f.getAnAccess())
|
||||
ExprNode getAssignedValueToField(Field f) {
|
||||
result.getExpr() in [f.getAnAssignedValue(),
|
||||
any(AssignOperation a | a.getLValue() = f.getAnAccess())]
|
||||
}
|
||||
|
||||
/** Holds if `f` can have any sign. */
|
||||
@@ -244,71 +184,78 @@ private module Impl {
|
||||
/**
|
||||
* Holds if `e` has type `NumericOrCharType`, but the sign of `e` is unknown.
|
||||
*/
|
||||
predicate numericExprWithUnknownSign(Expr e) {
|
||||
predicate numericExprWithUnknownSign(ExprNode e) {
|
||||
e.getType() instanceof NumericOrCharType and
|
||||
not e = getARead(_) and
|
||||
not e instanceof FieldAccess and
|
||||
not e instanceof TypeAccess and
|
||||
not e.getExpr() instanceof FieldAccess and
|
||||
not e.getExpr() instanceof TypeAccess 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
|
||||
not e.getExpr() instanceof AssignExpr and
|
||||
not e.getExpr() instanceof AssignOperation and
|
||||
not e.getExpr() instanceof UnaryPlusExpr and
|
||||
not e.getExpr() instanceof PostIncrExpr and
|
||||
not e.getExpr() instanceof PostDecrExpr and
|
||||
not e.getExpr() instanceof PreIncrExpr and
|
||||
not e.getExpr() instanceof PreDecrExpr and
|
||||
not e.getExpr() instanceof UnaryMinusExpr and
|
||||
not e.getExpr() instanceof ComplementExpr and
|
||||
not e.getExpr() instanceof AddExpr and
|
||||
not e.getExpr() instanceof SubExpr and
|
||||
not e.getExpr() instanceof MulExpr and
|
||||
not e.getExpr() instanceof DivExpr and
|
||||
not e.getExpr() instanceof RemExpr and
|
||||
not e.getExpr() instanceof BitwiseAndExpr and
|
||||
not e.getExpr() instanceof BitwiseOrExpr and
|
||||
not e.getExpr() instanceof BitwiseXorExpr and
|
||||
not e.getExpr() instanceof LShiftExpr and
|
||||
not e.getExpr() instanceof RShiftExpr and
|
||||
not e.getExpr() instanceof ConditionalExpr and
|
||||
not e.getExpr() instanceof RefExpr and
|
||||
not e.getExpr() instanceof LocalVariableDeclAndInitExpr and
|
||||
not e.getExpr() instanceof SwitchCaseExpr and
|
||||
not e.getExpr() instanceof CastExpr and
|
||||
not e.getExpr() instanceof SwitchExpr and
|
||||
not e.getExpr() instanceof NullCoalescingExpr
|
||||
}
|
||||
|
||||
/** Returns a sub expression of `e` for expression types where the sign depends on the child. */
|
||||
Expr getASubExprWithSameSign(Expr e) {
|
||||
result = e.(AssignExpr).getRValue() or
|
||||
result = e.(AssignOperation).getExpandedAssignment() or
|
||||
result = e.(UnaryPlusExpr).getOperand() or
|
||||
result = e.(PostIncrExpr).getOperand() or
|
||||
result = e.(PostDecrExpr).getOperand() or
|
||||
result = e.(ConditionalExpr).getAChild() or
|
||||
result = e.(NullCoalescingExpr).getAChild() or
|
||||
result = e.(SwitchExpr).getACase().getBody() or
|
||||
result = e.(SwitchCaseExpr).getBody() or
|
||||
result = e.(LocalVariableDeclAndInitExpr).getInitializer() or
|
||||
result = e.(RefExpr).getExpr() or
|
||||
result = e.(CastExpr).getExpr()
|
||||
ExprNode getASubExprWithSameSign(ExprNode e) {
|
||||
exists(Expr e_, Expr child | hasChild(e_, child, e, result) |
|
||||
child = e_.(AssignExpr).getRValue() or
|
||||
child = e_.(UnaryPlusExpr).getOperand() or
|
||||
child = e_.(PostIncrExpr).getOperand() or
|
||||
child = e_.(PostDecrExpr).getOperand() or
|
||||
child = e_.(ConditionalExpr).getAChild() or
|
||||
child = e_.(NullCoalescingExpr).getAChild() or
|
||||
child = e_.(SwitchExpr).getACase() or
|
||||
child = e_.(SwitchCaseExpr).getBody() or
|
||||
child = e_.(LocalVariableDeclAndInitExpr).getInitializer() or
|
||||
child = e_.(RefExpr).getExpr() or
|
||||
child = e_.(CastExpr).getExpr()
|
||||
)
|
||||
}
|
||||
|
||||
Expr getARead(Ssa::Definition v) { result = v.getARead() }
|
||||
ExprNode getARead(Ssa::Definition v) { exists(v.getAReadAtNode(result)) }
|
||||
|
||||
Field getField(FieldAccess fa) { result = fa.getTarget() }
|
||||
Field getField(ExprNode fa) { result = fa.getExpr().(FieldAccess).getTarget() }
|
||||
|
||||
Expr getAnExpression(SsaReadPositionBlock bb) { result = bb.getBlock().getANode().getElement() }
|
||||
ExprNode getAnExpression(SsaReadPositionBlock bb) { result = bb.getBlock().getANode() }
|
||||
|
||||
Guard getComparisonGuard(ComparisonExpr ce) { result = ce.getExpr() }
|
||||
|
||||
private newtype TComparisonExpr =
|
||||
MkComparisonExpr(ComparisonTest ct, ExprNode e) { e = ct.getExpr().getAControlFlowNode() }
|
||||
|
||||
/** A relational comparison */
|
||||
class ComparisonExpr extends ComparisonTest {
|
||||
class ComparisonExpr extends MkComparisonExpr {
|
||||
private ComparisonTest ct;
|
||||
private ExprNode e;
|
||||
private boolean strict;
|
||||
|
||||
ComparisonExpr() {
|
||||
this.getComparisonKind() =
|
||||
this = MkComparisonExpr(ct, e) and
|
||||
ct.getComparisonKind() =
|
||||
any(ComparisonKind ck |
|
||||
ck.isLessThan() and strict = true
|
||||
or
|
||||
@@ -317,13 +264,22 @@ private module Impl {
|
||||
)
|
||||
}
|
||||
|
||||
/** Gets the underlying expression. */
|
||||
Expr getExpr() { result = ct.getExpr() }
|
||||
|
||||
/** Gets a textual representation of this comparison test. */
|
||||
string toString() { result = ct.toString() }
|
||||
|
||||
/** Gets the location of this comparison test. */
|
||||
Location getLocation() { result = ct.getLocation() }
|
||||
|
||||
/**
|
||||
* 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() }
|
||||
ExprNode getGreaterOperand() { hasChild(ct.getExpr(), ct.getSecondArgument(), e, result) }
|
||||
|
||||
/**
|
||||
* Gets the operand on the "lesser" (or "lesser-or-equal") side
|
||||
@@ -331,7 +287,7 @@ private module Impl {
|
||||
* 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() }
|
||||
ExprNode getLesserOperand() { hasChild(ct.getExpr(), ct.getFirstArgument(), e, result) }
|
||||
|
||||
/** Holds if this comparison is strict, i.e. `<` or `>`. */
|
||||
predicate isStrict() { strict = true }
|
||||
|
||||
@@ -4,15 +4,32 @@
|
||||
|
||||
private import csharp
|
||||
private import Ssa
|
||||
private import RangeUtils
|
||||
private import ConstantUtils
|
||||
|
||||
private class ExprNode = ControlFlow::Nodes::ExprNode;
|
||||
|
||||
/** An SSA variable. */
|
||||
class SsaVariable extends Definition {
|
||||
/** Gets a read of this SSA variable. */
|
||||
ExprNode getAUse() { exists(this.getAReadAtNode(result)) }
|
||||
}
|
||||
|
||||
/** Gets a node that reads `src` via an SSA explicit definition. */
|
||||
ExprNode getAnExplicitDefinitionRead(ExprNode src) {
|
||||
exists(ExplicitDefinition def |
|
||||
exists(def.getAReadAtNode(result)) and
|
||||
hasChild(def.getElement(), def.getADefinition().getSource(), def.getControlFlowNode(), src)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets an expression that equals `v - delta`.
|
||||
*/
|
||||
Expr ssaRead(Definition v, int delta) {
|
||||
result = v.getARead() and delta = 0
|
||||
ExprNode ssaRead(Definition v, int delta) {
|
||||
exists(v.getAReadAtNode(result)) and delta = 0
|
||||
or
|
||||
exists(AddExpr add, int d1, ConstantIntegerExpr c |
|
||||
exists(ExprNode::AddExpr add, int d1, ConstantIntegerExpr c |
|
||||
result = add and
|
||||
delta = d1 - c.getIntValue()
|
||||
|
|
||||
@@ -21,22 +38,22 @@ Expr ssaRead(Definition v, int delta) {
|
||||
add.getRightOperand() = ssaRead(v, d1) and add.getLeftOperand() = c
|
||||
)
|
||||
or
|
||||
exists(SubExpr sub, int d1, ConstantIntegerExpr c |
|
||||
exists(ExprNode::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
|
||||
v.(ExplicitDefinition).getControlFlowNode().(ExprNode::PreIncrExpr) = result and delta = 0
|
||||
or
|
||||
v.(ExplicitDefinition).getADefinition().getExpr().(PreDecrExpr) = result and delta = 0
|
||||
v.(ExplicitDefinition).getControlFlowNode().(ExprNode::PreDecrExpr) = result and delta = 0
|
||||
or
|
||||
v.(ExplicitDefinition).getADefinition().getExpr().(PostIncrExpr) = result and delta = 1 // x++ === ++x - 1
|
||||
v.(ExplicitDefinition).getControlFlowNode().(ExprNode::PostIncrExpr) = result and delta = 1 // x++ === ++x - 1
|
||||
or
|
||||
v.(ExplicitDefinition).getADefinition().getExpr().(PostDecrExpr) = result and delta = -1 // x-- === --x + 1
|
||||
v.(ExplicitDefinition).getControlFlowNode().(ExprNode::PostDecrExpr) = result and delta = -1 // x-- === --x + 1
|
||||
or
|
||||
v.(ExplicitDefinition).getADefinition().getExpr().(Assignment) = result and delta = 0
|
||||
v.(ExplicitDefinition).getControlFlowNode().(ExprNode::Assignment) = result and delta = 0
|
||||
or
|
||||
result.(AssignExpr).getRValue() = ssaRead(v, delta)
|
||||
result.(ExprNode::AssignExpr).getRValue() = ssaRead(v, delta)
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user