hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2026-04-28 02:05:14 +02:00
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #2009 from AndreiDiaconu1/ircsharp-rangeanalysis

Browse Source 
C# IR: Add range analysis library
This commit is contained in:
Calum Grant
2019-09-27 14:27:41 +01:00
committed by GitHub
parent 18b28b1b57 a7a5eaa23f
commit 09f441a27e
13 changed files with 2364 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

667
csharp/ql/src/semmle/code/csharp/ir/internal/IRGuards.qll Normal file
View File

@@ -0,0 +1,667 @@
import csharp
import semmle.code.csharp.controlflow.BasicBlocks
import semmle.code.csharp.ir.IR
/**
* Holds if `block` consists of an `UnreachedInstruction`.
*
* We avoiding reporting an unreached block as being controlled by a guard. The unreached block
* has the AST for the `Function` itself, which tends to confuse mapping between the AST `BasicBlock`
* and the `IRBlock`.
*/
private predicate isUnreachedBlock(IRBlock block) {
block.getFirstInstruction() instanceof UnreachedInstruction
}
/**
* A Boolean condition in the AST that guards one or more basic blocks. This includes
* operands of logical operators but not switch statements.
*/
cached
class GuardCondition extends Expr {
cached
GuardCondition() {
exists(IRGuardCondition ir | this = ir.getUnconvertedResultExpression())
or
// no binary operators in the IR
exists(GuardCondition gc | this.(BinaryLogicalOperation).getAnOperand() = gc)
or
// the IR short-circuits if(!x)
// don't produce a guard condition for `y = !x` and other non-short-circuited cases
not exists(Instruction inst | this = inst.getAST()) and
exists(IRGuardCondition ir | this.(LogicalNotExpr).getOperand() = ir.getAST())
}
/**
* Holds if this condition controls `block`, meaning that `block` is only
* entered if the value of this condition is `testIsTrue`.
*
* Illustration:
*
* ```
* [ (testIsTrue) ]
* [ this ----------------succ ---- controlled ]
* [ | | ]
* [ (testIsFalse) | ------ ... ]
* [ other ]
* ```
*
* The predicate holds if all paths to `controlled` go via the `testIsTrue`
* edge of the control-flow graph. In other words, the `testIsTrue` edge
* must dominate `controlled`. This means that `controlled` must be
* dominated by both `this` and `succ` (the target of the `testIsTrue`
* edge). It also means that any other edge into `succ` must be a back-edge
* from a node which is dominated by `succ`.
*
* The short-circuit boolean operations have slightly surprising behavior
* here: because the operation itself only dominates one branch (due to
* being short-circuited) then it will only control blocks dominated by the
* true (for `&&`) or false (for `||`) branch.
*/
cached
predicate controls(BasicBlock controlled, boolean testIsTrue) { none() }
/** Holds if (determined by this guard) `left < right + k` evaluates to `isLessThan` if this expression evaluates to `testIsTrue`. */
cached
predicate comparesLt(Expr left, Expr right, int k, boolean isLessThan, boolean testIsTrue) {
none()
}
/**
* Holds if (determined by this guard) `left < right + k` must be `isLessThan` in `block`.
* If `isLessThan = false` then this implies `left >= right + k`.
*/
cached
predicate ensuresLt(Expr left, Expr right, int k, BasicBlock block, boolean isLessThan) { none() }
/** Holds if (determined by this guard) `left == right + k` evaluates to `areEqual` if this expression evaluates to `testIsTrue`. */
cached
predicate comparesEq(Expr left, Expr right, int k, boolean areEqual, boolean testIsTrue) {
none()
}
/**
* Holds if (determined by this guard) `left == right + k` must be `areEqual` in `block`.
* If `areEqual = false` then this implies `left != right + k`.
*/
cached
predicate ensuresEq(Expr left, Expr right, int k, BasicBlock block, boolean areEqual) { none() }
}
/**
* Holds if the truth of the binary logical expression `blo` having value `wholeIsTrue`
* implies that the truth of the child expression `part` has truth value `partIsTrue`.
*
* For example if the binary operation:
* ```
* x && y
* ```
* is true, `x` and `y` must also be true, so `impliesValue(x, true, true)` and
* `impliesValue(y, true, true)` hold.
*/
private predicate impliesValue(
BinaryLogicalOperation blo, Expr part, boolean partIsTrue, boolean wholeIsTrue
) {
blo instanceof LogicalAndExpr and
(
wholeIsTrue = true and partIsTrue = true and part = blo.getAnOperand()
or
wholeIsTrue = true and
impliesValue(blo.getAnOperand().(BinaryLogicalOperation), part, partIsTrue, true)
)
or
blo instanceof LogicalOrExpr and
(
wholeIsTrue = false and partIsTrue = false and part = blo.getAnOperand()
or
wholeIsTrue = false and
impliesValue(blo.getAnOperand().(BinaryLogicalOperation), part, partIsTrue, false)
)
}
/**
* A binary logical operator in the AST that guards one or more basic blocks.
*/
private class GuardConditionFromBinaryLogicalOperator extends GuardCondition {
GuardConditionFromBinaryLogicalOperator() {
exists(GuardCondition gc | this.(BinaryLogicalOperation).getAnOperand() = gc)
}
override predicate controls(BasicBlock controlled, boolean testIsTrue) {
exists(BinaryLogicalOperation binop, GuardCondition lhs, GuardCondition rhs |
this = binop and
lhs = binop.getLeftOperand() and
rhs = binop.getRightOperand() and
lhs.controls(controlled, testIsTrue) and
rhs.controls(controlled, testIsTrue)
)
}
override predicate comparesLt(Expr left, Expr right, int k, boolean isLessThan, boolean testIsTrue) {
exists(boolean partIsTrue, GuardCondition part |
impliesValue(this.(BinaryLogicalOperation), part, partIsTrue, testIsTrue)
|
part.comparesLt(left, right, k, isLessThan, partIsTrue)
)
}
override predicate ensuresLt(Expr left, Expr right, int k, BasicBlock block, boolean isLessThan) {
exists(boolean testIsTrue |
comparesLt(left, right, k, isLessThan, testIsTrue) and this.controls(block, testIsTrue)
)
}
override predicate comparesEq(Expr left, Expr right, int k, boolean isLessThan, boolean testIsTrue) {
exists(boolean partIsTrue, GuardCondition part |
impliesValue(this.(BinaryLogicalOperation), part, partIsTrue, testIsTrue)
|
part.comparesEq(left, right, k, isLessThan, partIsTrue)
)
}
override predicate ensuresEq(Expr left, Expr right, int k, BasicBlock block, boolean isLessThan) {
exists(boolean testIsTrue |
comparesEq(left, right, k, isLessThan, testIsTrue) and this.controls(block, testIsTrue)
)
}
}
/**
* A `!` operator in the AST that guards one or more basic blocks, and does not have a corresponding
* IR instruction.
*/
private class GuardConditionFromShortCircuitNot extends GuardCondition, LogicalNotExpr {
GuardConditionFromShortCircuitNot() {
not exists(Instruction inst | this = inst.getAST()) and
exists(IRGuardCondition ir | getOperand() = ir.getAST())
}
override predicate controls(BasicBlock controlled, boolean testIsTrue) {
getOperand().(GuardCondition).controls(controlled, testIsTrue.booleanNot())
}
override predicate comparesLt(Expr left, Expr right, int k, boolean areEqual, boolean testIsTrue) {
getOperand().(GuardCondition).comparesLt(left, right, k, areEqual, testIsTrue.booleanNot())
}
override predicate ensuresLt(Expr left, Expr right, int k, BasicBlock block, boolean testIsTrue) {
getOperand().(GuardCondition).ensuresLt(left, right, k, block, testIsTrue.booleanNot())
}
override predicate comparesEq(Expr left, Expr right, int k, boolean areEqual, boolean testIsTrue) {
getOperand().(GuardCondition).comparesEq(left, right, k, areEqual, testIsTrue.booleanNot())
}
override predicate ensuresEq(Expr left, Expr right, int k, BasicBlock block, boolean testIsTrue) {
getOperand().(GuardCondition).ensuresEq(left, right, k, block, testIsTrue.booleanNot())
}
}
/**
* A Boolean condition in the AST that guards one or more basic blocks and has a corresponding IR
* instruction.
*/
private class GuardConditionFromIR extends GuardCondition {
IRGuardCondition ir;
GuardConditionFromIR() { this = ir.getUnconvertedResultExpression() }
override predicate controls(BasicBlock controlled, boolean testIsTrue) {
// This condition must determine the flow of control; that is, this
// node must be a top-level condition.
this.controlsBlock1(controlled, testIsTrue)
}
/** Holds if (determined by this guard) `left < right + k` evaluates to `isLessThan` if this expression evaluates to `testIsTrue`. */
override predicate comparesLt(Expr left, Expr right, int k, boolean isLessThan, boolean testIsTrue) {
exists(Instruction li, Instruction ri |
li.getUnconvertedResultExpression() = left and
ri.getUnconvertedResultExpression() = right and
ir.comparesLt(li.getAUse(), ri.getAUse(), k, isLessThan, testIsTrue)
)
}
/**
* Holds if (determined by this guard) `left < right + k` must be `isLessThan` in `block`.
* If `isLessThan = false` then this implies `left >= right + k`.
*/
override predicate ensuresLt(Expr left, Expr right, int k, BasicBlock block, boolean isLessThan) {
exists(Instruction li, Instruction ri, boolean testIsTrue |
li.getUnconvertedResultExpression() = left and
ri.getUnconvertedResultExpression() = right and
ir.comparesLt(li.getAUse(), ri.getAUse(), k, isLessThan, testIsTrue) and
this.controls(block, testIsTrue)
)
}
/** Holds if (determined by this guard) `left == right + k` evaluates to `areEqual` if this expression evaluates to `testIsTrue`. */
override predicate comparesEq(Expr left, Expr right, int k, boolean areEqual, boolean testIsTrue) {
exists(Instruction li, Instruction ri |
li.getUnconvertedResultExpression() = left and
ri.getUnconvertedResultExpression() = right and
ir.comparesEq(li.getAUse(), ri.getAUse(), k, areEqual, testIsTrue)
)
}
/**
* Holds if (determined by this guard) `left == right + k` must be `areEqual` in `block`.
* If `areEqual = false` then this implies `left != right + k`.
*/
override predicate ensuresEq(Expr left, Expr right, int k, BasicBlock block, boolean areEqual) {
exists(Instruction li, Instruction ri, boolean testIsTrue |
li.getUnconvertedResultExpression() = left and
ri.getUnconvertedResultExpression() = right and
ir.comparesEq(li.getAUse(), ri.getAUse(), k, areEqual, testIsTrue) and
this.controls(block, testIsTrue)
)
}
/**
* Holds if this condition controls `block`, meaning that `block` is only
* entered if the value of this condition is `testIsTrue`. This helper
* predicate does not necessarily hold for binary logical operations like
* `&&` and `||`. See the detailed explanation on predicate `controls`.
*/
private predicate controlsBlock1(BasicBlock controlled, boolean testIsTrue) {
exists(IRBlock irb |
forex(IRGuardCondition inst | inst = ir | inst.controls(irb, testIsTrue)) and
irb.getAnInstruction().getAST().(ControlFlowElement).getAControlFlowNode().getBasicBlock() = controlled and
not isUnreachedBlock(irb)
)
}
}
/**
* A Boolean condition in the IR that guards one or more basic blocks. This includes
* operands of logical operators but not switch statements. Note that `&&` and `||`
* don't have an explicit representation in the IR, and therefore will not appear as
* IRGuardConditions.
*/
cached
class IRGuardCondition extends Instruction {
ConditionalBranchInstruction branch;
cached
IRGuardCondition() { branch = get_branch_for_condition(this) }
/**
* Holds if this condition controls `block`, meaning that `block` is only
* entered if the value of this condition is `testIsTrue`.
*
* Illustration:
*
* ```
* [ (testIsTrue) ]
* [ this ----------------succ ---- controlled ]
* [ | | ]
* [ (testIsFalse) | ------ ... ]
* [ other ]
* ```
*
* The predicate holds if all paths to `controlled` go via the `testIsTrue`
* edge of the control-flow graph. In other words, the `testIsTrue` edge
* must dominate `controlled`. This means that `controlled` must be
* dominated by both `this` and `succ` (the target of the `testIsTrue`
* edge). It also means that any other edge into `succ` must be a back-edge
* from a node which is dominated by `succ`.
*
* The short-circuit boolean operations have slightly surprising behavior
* here: because the operation itself only dominates one branch (due to
* being short-circuited) then it will only control blocks dominated by the
* true (for `&&`) or false (for `||`) branch.
*/
cached
predicate controls(IRBlock controlled, boolean testIsTrue) {
// This condition must determine the flow of control; that is, this
// node must be a top-level condition.
this.controlsBlock(controlled, testIsTrue)
or
exists(IRGuardCondition ne |
this = ne.(LogicalNotInstruction).getUnary() and
ne.controls(controlled, testIsTrue.booleanNot())
)
}
cached
predicate controlsEdge(IRBlock pred, IRBlock succ, boolean testIsTrue) {
pred.getASuccessor() = succ and
controls(pred, testIsTrue)
or
hasBranchEdge(succ, testIsTrue) and
branch.getCondition() = this and
branch.getBlock() = pred
}
/**
* Holds if `branch` jumps directly to `succ` when this condition is `testIsTrue`.
*
* This predicate is intended to help with situations in which an inference can only be made
* based on an edge between a block with multiple successors and a block with multiple
* predecessors. For example, in the following situation, an inference can be made about the
* value of `x` at the end of the `if` statement, but there is no block which is controlled by
* the `if` statement when `x >= y`.
* ```
* if (x < y) {
* x = y;
* }
* return x;
* ```
*/
private predicate hasBranchEdge(IRBlock succ, boolean testIsTrue) {
branch.getCondition() = this and
(
testIsTrue = true and
succ.getFirstInstruction() = branch.getTrueSuccessor()
or
testIsTrue = false and
succ.getFirstInstruction() = branch.getFalseSuccessor()
)
}
/** Holds if (determined by this guard) `left < right + k` evaluates to `isLessThan` if this expression evaluates to `testIsTrue`. */
cached
predicate comparesLt(Operand left, Operand right, int k, boolean isLessThan, boolean testIsTrue) {
compares_lt(this, left, right, k, isLessThan, testIsTrue)
}
/**
* Holds if (determined by this guard) `left < right + k` must be `isLessThan` in `block`.
* If `isLessThan = false` then this implies `left >= right + k`.
*/
cached
predicate ensuresLt(Operand left, Operand right, int k, IRBlock block, boolean isLessThan) {
exists(boolean testIsTrue |
compares_lt(this, left, right, k, isLessThan, testIsTrue) and this.controls(block, testIsTrue)
)
}
/**
* Holds if (determined by this guard) `left < right + k` must be `isLessThan` on the edge from
* `pred` to `succ`. If `isLessThan = false` then this implies `left >= right + k`.
*/
cached
predicate ensuresLtEdge(
Operand left, Operand right, int k, IRBlock pred, IRBlock succ, boolean isLessThan
) {
exists(boolean testIsTrue |
compares_lt(this, left, right, k, isLessThan, testIsTrue) and
this.controlsEdge(pred, succ, testIsTrue)
)
}
/** Holds if (determined by this guard) `left == right + k` evaluates to `areEqual` if this expression evaluates to `testIsTrue`. */
cached
predicate comparesEq(Operand left, Operand right, int k, boolean areEqual, boolean testIsTrue) {
compares_eq(this, left, right, k, areEqual, testIsTrue)
}
/**
* Holds if (determined by this guard) `left == right + k` must be `areEqual` in `block`.
* If `areEqual = false` then this implies `left != right + k`.
*/
cached
predicate ensuresEq(Operand left, Operand right, int k, IRBlock block, boolean areEqual) {
exists(boolean testIsTrue |
compares_eq(this, left, right, k, areEqual, testIsTrue) and this.controls(block, testIsTrue)
)
}
/**
* Holds if (determined by this guard) `left == right + k` must be `areEqual` on the edge from
* `pred` to `succ`. If `areEqual = false` then this implies `left != right + k`.
*/
cached
predicate ensuresEqEdge(
Operand left, Operand right, int k, IRBlock pred, IRBlock succ, boolean areEqual
) {
exists(boolean testIsTrue |
compares_eq(this, left, right, k, areEqual, testIsTrue) and
this.controlsEdge(pred, succ, testIsTrue)
)
}
/**
* Holds if this condition controls `block`, meaning that `block` is only
* entered if the value of this condition is `testIsTrue`. This helper
* predicate does not necessarily hold for binary logical operations like
* `&&` and `||`. See the detailed explanation on predicate `controls`.
*/
private predicate controlsBlock(IRBlock controlled, boolean testIsTrue) {
not isUnreachedBlock(controlled) and
exists(IRBlock branchBlock | branchBlock.getAnInstruction() = branch |
exists(IRBlock succ |
testIsTrue = true and succ.getFirstInstruction() = branch.getTrueSuccessor()
or
testIsTrue = false and succ.getFirstInstruction() = branch.getFalseSuccessor()
|
branch.getCondition() = this and
succ.dominates(controlled) and
forall(IRBlock pred | pred.getASuccessor() = succ |
pred = branchBlock or succ.dominates(pred) or not pred.isReachableFromFunctionEntry()
)
)
)
}
}
private ConditionalBranchInstruction get_branch_for_condition(Instruction guard) {
result.getCondition() = guard
or
exists(LogicalNotInstruction cond |
result = get_branch_for_condition(cond) and cond.getUnary() = guard
)
}
/**
* Holds if `left == right + k` is `areEqual` given that test is `testIsTrue`.
*
* Beware making mistaken logical implications here relating `areEqual` and `testIsTrue`.
*/
private predicate compares_eq(
Instruction test, Operand left, Operand right, int k, boolean areEqual, boolean testIsTrue
) {
/* The simple case where the test *is* the comparison so areEqual = testIsTrue xor eq. */
exists(boolean eq | simple_comparison_eq(test, left, right, k, eq) |
areEqual = true and testIsTrue = eq
or
areEqual = false and testIsTrue = eq.booleanNot()
)
or
// I think this is handled by forwarding in controlsBlock.
//or
//logical_comparison_eq(test, left, right, k, areEqual, testIsTrue)
/* a == b + k => b == a - k */
exists(int mk | k = -mk | compares_eq(test, right, left, mk, areEqual, testIsTrue))
or
complex_eq(test, left, right, k, areEqual, testIsTrue)
or
/* (x is true => (left == right + k)) => (!x is false => (left == right + k)) */
exists(boolean isFalse | testIsTrue = isFalse.booleanNot() |
compares_eq(test.(LogicalNotInstruction).getUnary(), left, right, k, areEqual, isFalse)
)
}
/** Rearrange various simple comparisons into `left == right + k` form. */
private predicate simple_comparison_eq(
CompareInstruction cmp, Operand left, Operand right, int k, boolean areEqual
) {
left = cmp.getLeftOperand() and
cmp instanceof CompareEQInstruction and
right = cmp.getRightOperand() and
k = 0 and
areEqual = true
or
left = cmp.getLeftOperand() and
cmp instanceof CompareNEInstruction and
right = cmp.getRightOperand() and
k = 0 and
areEqual = false
}
private predicate complex_eq(
CompareInstruction cmp, Operand left, Operand right, int k, boolean areEqual, boolean testIsTrue
) {
sub_eq(cmp, left, right, k, areEqual, testIsTrue)
or
add_eq(cmp, left, right, k, areEqual, testIsTrue)
}
/*
* Simplification of inequality expressions
* Simplify conditions in the source to the canonical form l < r + k.
*/
/** Holds if `left < right + k` evaluates to `isLt` given that test is `testIsTrue`. */
private predicate compares_lt(
Instruction test, Operand left, Operand right, int k, boolean isLt, boolean testIsTrue
) {
/* In the simple case, the test is the comparison, so isLt = testIsTrue */
simple_comparison_lt(test, left, right, k) and isLt = true and testIsTrue = true
or
simple_comparison_lt(test, left, right, k) and isLt = false and testIsTrue = false
or
complex_lt(test, left, right, k, isLt, testIsTrue)
or
/* (not (left < right + k)) => (left >= right + k) */
exists(boolean isGe | isLt = isGe.booleanNot() |
compares_ge(test, left, right, k, isGe, testIsTrue)
)
or
/* (x is true => (left < right + k)) => (!x is false => (left < right + k)) */
exists(boolean isFalse | testIsTrue = isFalse.booleanNot() |
compares_lt(test.(LogicalNotInstruction).getUnary(), left, right, k, isLt, isFalse)
)
}
/** `(a < b + k) => (b > a - k) => (b >= a + (1-k))` */
private predicate compares_ge(
Instruction test, Operand left, Operand right, int k, boolean isGe, boolean testIsTrue
) {
exists(int onemk | k = 1 - onemk | compares_lt(test, right, left, onemk, isGe, testIsTrue))
}
/** Rearrange various simple comparisons into `left < right + k` form. */
private predicate simple_comparison_lt(CompareInstruction cmp, Operand left, Operand right, int k) {
left = cmp.getLeftOperand() and
cmp instanceof CompareLTInstruction and
right = cmp.getRightOperand() and
k = 0
or
left = cmp.getLeftOperand() and
cmp instanceof CompareLEInstruction and
right = cmp.getRightOperand() and
k = 1
or
right = cmp.getLeftOperand() and
cmp instanceof CompareGTInstruction and
left = cmp.getRightOperand() and
k = 0
or
right = cmp.getLeftOperand() and
cmp instanceof CompareGEInstruction and
left = cmp.getRightOperand() and
k = 1
}
private predicate complex_lt(
CompareInstruction cmp, Operand left, Operand right, int k, boolean isLt, boolean testIsTrue
) {
sub_lt(cmp, left, right, k, isLt, testIsTrue)
or
add_lt(cmp, left, right, k, isLt, testIsTrue)
}
// left - x < right + c => left < right + (c+x)
// left < (right - x) + c => left < right + (c-x)
private predicate sub_lt(
CompareInstruction cmp, Operand left, Operand right, int k, boolean isLt, boolean testIsTrue
) {
exists(SubInstruction lhs, int c, int x |
compares_lt(cmp, lhs.getAUse(), right, c, isLt, testIsTrue) and
left = lhs.getLeftOperand() and
x = int_value(lhs.getRight()) and
k = c + x
)
or
exists(SubInstruction rhs, int c, int x |
compares_lt(cmp, left, rhs.getAUse(), c, isLt, testIsTrue) and
right = rhs.getLeftOperand() and
x = int_value(rhs.getRight()) and
k = c - x
)
}
// left + x < right + c => left < right + (c-x)
// left < (right + x) + c => left < right + (c+x)
private predicate add_lt(
CompareInstruction cmp, Operand left, Operand right, int k, boolean isLt, boolean testIsTrue
) {
exists(AddInstruction lhs, int c, int x |
compares_lt(cmp, lhs.getAUse(), right, c, isLt, testIsTrue) and
(
left = lhs.getLeftOperand() and x = int_value(lhs.getRight())
or
left = lhs.getRightOperand() and x = int_value(lhs.getLeft())
) and
k = c - x
)
or
exists(AddInstruction rhs, int c, int x |
compares_lt(cmp, left, rhs.getAUse(), c, isLt, testIsTrue) and
(
right = rhs.getLeftOperand() and x = int_value(rhs.getRight())
or
right = rhs.getRightOperand() and x = int_value(rhs.getLeft())
) and
k = c + x
)
}
// left - x == right + c => left == right + (c+x)
// left == (right - x) + c => left == right + (c-x)
private predicate sub_eq(
CompareInstruction cmp, Operand left, Operand right, int k, boolean areEqual, boolean testIsTrue
) {
exists(SubInstruction lhs, int c, int x |
compares_eq(cmp, lhs.getAUse(), right, c, areEqual, testIsTrue) and
left = lhs.getLeftOperand() and
x = int_value(lhs.getRight()) and
k = c + x
)
or
exists(SubInstruction rhs, int c, int x |
compares_eq(cmp, left, rhs.getAUse(), c, areEqual, testIsTrue) and
right = rhs.getLeftOperand() and
x = int_value(rhs.getRight()) and
k = c - x
)
}
// left + x == right + c => left == right + (c-x)
// left == (right + x) + c => left == right + (c+x)
private predicate add_eq(
CompareInstruction cmp, Operand left, Operand right, int k, boolean areEqual, boolean testIsTrue
) {
exists(AddInstruction lhs, int c, int x |
compares_eq(cmp, lhs.getAUse(), right, c, areEqual, testIsTrue) and
(
left = lhs.getLeftOperand() and x = int_value(lhs.getRight())
or
left = lhs.getRightOperand() and x = int_value(lhs.getLeft())
) and
k = c - x
)
or
exists(AddInstruction rhs, int c, int x |
compares_eq(cmp, left, rhs.getAUse(), c, areEqual, testIsTrue) and
(
right = rhs.getLeftOperand() and x = int_value(rhs.getRight())
or
right = rhs.getRightOperand() and x = int_value(rhs.getLeft())
) and
k = c + x
)
}
/** The int value of integer constant expression. */
private int int_value(Instruction i) { result = i.(IntegerConstantInstruction).getValue().toInt() }

79
csharp/ql/src/semmle/code/csharp/ir/rangeanalysis/Bound.qll Normal file
View File

@@ -0,0 +1,79 @@
import csharp
private import semmle.code.csharp.ir.IR
private import semmle.code.csharp.ir.ValueNumbering
private newtype TBound =
TBoundZero() or
TBoundValueNumber(ValueNumber vn) {
exists(Instruction i |
vn.getAnInstruction() = i and
(
i.getResultType() instanceof IntegralType or
i.getResultType() instanceof PointerType
) and
not vn.getAnInstruction() instanceof ConstantInstruction
|
i instanceof PhiInstruction
or
i instanceof InitializeParameterInstruction
or
i instanceof CallInstruction
or
i instanceof VariableAddressInstruction
or
i instanceof FieldAddressInstruction
or
i.(LoadInstruction).getSourceAddress() instanceof VariableAddressInstruction
or
i.(LoadInstruction).getSourceAddress() instanceof FieldAddressInstruction
or
i.getAUse() instanceof ArgumentOperand
)
}
/**
* A bound that may be inferred for an expression plus/minus an integer delta.
*/
abstract class Bound extends TBound {
abstract string toString();
/** Gets an expression that equals this bound plus `delta`. */
abstract Instruction getInstruction(int delta);
/** Gets an expression that equals this bound. */
Instruction getInstruction() { result = getInstruction(0) }
abstract Location getLocation();
}
/**
* The bound that corresponds to the integer 0. This is used to represent all
* integer bounds as bounds are always accompanied by an added integer delta.
*/
class ZeroBound extends Bound, TBoundZero {
override string toString() { result = "0" }
override Instruction getInstruction(int delta) {
result.(ConstantValueInstruction).getValue().toInt() = delta
}
override Location getLocation() { result instanceof EmptyLocation }
}
/**
* A bound corresponding to the value of an `Instruction`.
*/
class ValueNumberBound extends Bound, TBoundValueNumber {
ValueNumber vn;
ValueNumberBound() { this = TBoundValueNumber(vn) }
/** Gets the SSA variable that equals this bound. */
override Instruction getInstruction(int delta) {
this = TBoundValueNumber(valueNumber(result)) and delta = 0
}
override string toString() { result = vn.getExampleInstruction().toString() }
override Location getLocation() { result = vn.getLocation() }
}

635
csharp/ql/src/semmle/code/csharp/ir/rangeanalysis/RangeAnalysis.qll Normal file
View File

@@ -0,0 +1,635 @@
/**
* Provides classes and predicates for range analysis.
*
* An inferred bound can either be a specific integer or a `ValueNumber`
* representing the abstract value of a set of `Instruction`s.
*
* If an inferred bound relies directly on a condition, then this condition is
* reported as the reason for the bound.
*/
/*
* This library tackles range analysis as a flow problem. Consider e.g.:
* ```
* len = arr.length;
* if (x < len) { ... y = x-1; ... y ... }
* ```
* In this case we would like to infer `y <= arr.length - 2`, and this is
* accomplished by tracking the bound through a sequence of steps:
* ```
* arr.length --> len = .. --> x < len --> x-1 --> y = .. --> y
* ```
*
* In its simplest form the step relation `I1 --> I2` relates two `Instruction`s
* such that `I1 <= B` implies `I2 <= B` for any `B` (with a second separate
* step relation handling lower bounds). Examples of such steps include
* assignments `I2 = I1` and conditions `x <= I1` where `I2` is a use of `x`
* guarded by the condition.
*
* In order to handle subtractions and additions with constants, and strict
* comparisons, the step relation is augmented with an integer delta. With this
* generalization `I1 --(delta)--> I2` relates two `Instruction`s and an integer
* such that `I1 <= B` implies `I2 <= B + delta` for any `B`. This corresponds
* to the predicate `boundFlowStep`.
*
* The complete range analysis is then implemented as the transitive closure of
* the step relation summing the deltas along the way. If `I1` transitively
* steps to `I2`, `delta` is the sum of deltas along the path, and `B` is an
* interesting bound equal to the value of `I1` then `I2 <= B + delta`. This
* corresponds to the predicate `boundedInstruction`.
*
* Bounds come in two forms: either they are relative to zero (and thus provide
* a constant bound), or they are relative to some program value. This value is
* represented by the `ValueNumber` class, each instance of which represents a
* set of `Instructions` that must have the same value.
*
* Phi nodes need a little bit of extra handling. Consider `x0 = phi(x1, x2)`.
* There are essentially two cases:
* - If `x1 <= B + d1` and `x2 <= B + d2` then `x0 <= B + max(d1,d2)`.
* - If `x1 <= B + d1` and `x2 <= x0 + d2` with `d2 <= 0` then `x0 <= B + d1`.
* The first case is for whenever a bound can be proven without taking looping
* into account. The second case is relevant when `x2` comes from a back-edge
* where we can prove that the variable has been non-increasing through the
* loop-iteration as this means that any upper bound that holds prior to the
* loop also holds for the variable during the loop.
* This generalizes to a phi node with `n` inputs, so if
* `x0 = phi(x1, ..., xn)` and `xi <= B + delta` for one of the inputs, then we
* also have `x0 <= B + delta` if we can prove either:
* - `xj <= B + d` with `d <= delta` or
* - `xj <= x0 + d` with `d <= 0`
* for each input `xj`.
*
* As all inferred bounds can be related directly to a path in the source code
* the only source of non-termination is if successive redundant (and thereby
* increasingly worse) bounds are calculated along a loop in the source code.
* We prevent this by weakening the bound to a small finite set of bounds when
* a path follows a second back-edge (we postpone weakening till the second
* back-edge as a precise bound might require traversing a loop once).
*/
import csharp
private import semmle.code.csharp.ir.IR
private import semmle.code.csharp.ir.internal.IRGuards
private import semmle.code.csharp.ir.ValueNumbering
private import RangeUtils
private import SignAnalysis
import Bound
cached
private module RangeAnalysisCache {
cached
module RangeAnalysisPublic {
/**
* Holds if `b + delta` is a valid bound for `i`.
* - `upper = true` : `i <= b + delta`
* - `upper = false` : `i >= b + delta`
*
* The reason for the bound is given by `reason` and may be either a condition
* or `NoReason` if the bound was proven directly without the use of a bounding
* condition.
*/
cached
predicate boundedInstruction(Instruction i, Bound b, int delta, boolean upper, Reason reason) {
boundedInstruction(i, b, delta, upper, _, _, reason)
}
/**
* Holds if `b + delta` is a valid bound for `op`.
* - `upper = true` : `op <= b + delta`
* - `upper = false` : `op >= b + delta`
*
* The reason for the bound is given by `reason` and may be either a condition
* or `NoReason` if the bound was proven directly without the use of a bounding
* condition.
*/
cached
predicate boundedOperand(Operand op, Bound b, int delta, boolean upper, Reason reason) {
boundedNonPhiOperand(op, b, delta, upper, _, _, reason)
or
boundedPhiOperand(op, b, delta, upper, _, _, reason)
}
}
/**
* Holds if `guard = boundFlowCond(_, _, _, _, _) or guard = eqFlowCond(_, _, _, _, _)`.
*/
cached
predicate possibleReason(IRGuardCondition guard) {
guard = boundFlowCond(_, _, _, _, _)
or
guard = eqFlowCond(_, _, _, _, _)
}
}
private import RangeAnalysisCache
import RangeAnalysisPublic
/**
* Gets a condition that tests whether `vn` equals `bound + delta`.
*
* If the condition evaluates to `testIsTrue`:
* - `isEq = true` : `vn == bound + delta`
* - `isEq = false` : `vn != bound + delta`
*/
private IRGuardCondition eqFlowCond(
ValueNumber vn, Operand bound, int delta, boolean isEq, boolean testIsTrue
) {
result.comparesEq(vn.getAUse(), bound, delta, isEq, testIsTrue)
}
/**
* Holds if `op1 + delta` is a valid bound for `op2`.
* - `upper = true` : `op2 <= op1 + delta`
* - `upper = false` : `op2 >= op1 + delta`
*/
private predicate boundFlowStepSsa(
NonPhiOperand op2, Operand op1, int delta, boolean upper, Reason reason
) {
exists(IRGuardCondition guard, boolean testIsTrue |
guard = boundFlowCond(valueNumberOfOperand(op2), op1, delta, upper, testIsTrue) and
guard.controls(op2.getUse().getBlock(), testIsTrue) and
reason = TCondReason(guard)
)
}
/**
* Gets a condition that tests whether `vn` is bounded by `bound + delta`.
*
* If the condition evaluates to `testIsTrue`:
* - `upper = true` : `vn <= bound + delta`
* - `upper = false` : `vn >= bound + delta`
*/
private IRGuardCondition boundFlowCond(
ValueNumber vn, NonPhiOperand bound, int delta, boolean upper, boolean testIsTrue
) {
exists(int d |
result.comparesLt(vn.getAUse(), bound, d, upper, testIsTrue) and
// `comparesLt` provides bounds of the form `x < y + k` or `x >= y + k`, but we need
// `x <= y + k` so we strengthen here. `testIsTrue` has the same semantics in `comparesLt` as
// it does here, so we don't need to account for it.
if upper = true then delta = d - 1 else delta = d
)
or
result = eqFlowCond(vn, bound, delta, true, testIsTrue) and
(upper = true or upper = false)
}
private newtype TReason =
TNoReason() or
TCondReason(IRGuardCondition guard) { possibleReason(guard) }
/**
* A reason for an inferred bound. This can either be `CondReason` if the bound
* is due to a specific condition, or `NoReason` if the bound is inferred
* without going through a bounding condition.
*/
abstract class Reason extends TReason {
abstract string toString();
}
class NoReason extends Reason, TNoReason {
override string toString() { result = "NoReason" }
}
class CondReason extends Reason, TCondReason {
IRGuardCondition getCond() { this = TCondReason(result) }
override string toString() { result = getCond().toString() }
}
/**
* Holds if a cast from `fromtyp` to `totyp` can be ignored for the purpose of
* range analysis.
*/
pragma[inline]
private predicate safeCast(IntegralType fromtyp, IntegralType totyp) {
fromtyp.getSize() < totyp.getSize() and
(
fromtyp instanceof UnsignedIntegralType
or
totyp instanceof SignedIntegralType
)
or
fromtyp.getSize() <= totyp.getSize() and
(
fromtyp instanceof SignedIntegralType and
totyp instanceof SignedIntegralType
or
fromtyp instanceof UnsignedIntegralType and
totyp instanceof UnsignedIntegralType
)
}
private class SafeCastInstruction extends ConvertInstruction {
SafeCastInstruction() {
safeCast(getResultType(), getUnary().getResultType())
or
getResultType() instanceof PointerType and
getUnary().getResultType() instanceof PointerType
}
}
/**
* Holds if `typ` is a small integral type with the given lower and upper bounds.
*/
private predicate typeBound(IntegralType typ, int lowerbound, int upperbound) {
typ instanceof SignedIntegralType and
typ.getSize() = 1 and
lowerbound = typ.minValue() and
upperbound = typ.maxValue()
or
typ instanceof UnsignedIntegralType and
typ.getSize() = 1 and
lowerbound = typ.minValue() and
upperbound = typ.maxValue()
or
typ instanceof SignedIntegralType and
typ.getSize() = 2 and
lowerbound = typ.minValue() and
upperbound = typ.maxValue()
or
typ instanceof UnsignedIntegralType and
typ.getSize() = 2 and
lowerbound = typ.minValue() and
upperbound = typ.maxValue()
}
/**
* A cast to a small integral type that may overflow or underflow.
*/
private class NarrowingCastInstruction extends ConvertInstruction {
NarrowingCastInstruction() {
not this instanceof SafeCastInstruction and
typeBound(getResultType(), _, _)
}
/** Gets the lower bound of the resulting type. */
int getLowerBound() { typeBound(getResultType(), result, _) }
/** Gets the upper bound of the resulting type. */
int getUpperBound() { typeBound(getResultType(), _, result) }
}
/**
* Holds if `op + delta` is a valid bound for `i`.
* - `upper = true` : `i <= op + delta`
* - `upper = false` : `i >= op + delta`
*/
private predicate boundFlowStep(Instruction i, NonPhiOperand op, int delta, boolean upper) {
valueFlowStep(i, op, delta) and
(upper = true or upper = false)
or
i.(SafeCastInstruction).getAnOperand() = op and
delta = 0 and
(upper = true or upper = false)
or
exists(Operand x |
i.(AddInstruction).getAnOperand() = op and
i.(AddInstruction).getAnOperand() = x and
op != x
|
not exists(getValue(getConstantValue(op.getUse()))) and
not exists(getValue(getConstantValue(x.getUse()))) and
if strictlyPositive(x)
then upper = false and delta = 1
else
if positive(x)
then upper = false and delta = 0
else
if strictlyNegative(x)
then upper = true and delta = -1
else
if negative(x)
then upper = true and delta = 0
else none()
)
or
exists(Operand x |
exists(SubInstruction sub |
i = sub and
sub.getLeftOperand() = op and
sub.getRightOperand() = x
)
|
// `x` with constant value is covered by valueFlowStep
not exists(getValue(getConstantValue(x.getUse()))) and
if strictlyPositive(x)
then upper = true and delta = -1
else
if positive(x)
then upper = true and delta = 0
else
if strictlyNegative(x)
then upper = false and delta = 1
else
if negative(x)
then upper = false and delta = 0
else none()
)
or
i.(RemInstruction).getRightOperand() = op and positive(op) and delta = -1 and upper = true
or
i.(RemInstruction).getLeftOperand() = op and positive(op) and delta = 0 and upper = true
or
i.(BitAndInstruction).getAnOperand() = op and positive(op) and delta = 0 and upper = true
or
i.(BitOrInstruction).getAnOperand() = op and
positiveInstruction(i) and
delta = 0 and
upper = false
// TODO: min, max, rand
}
private predicate boundFlowStepMul(Instruction i1, Operand op, int factor) {
exists(Instruction c, int k | k = getValue(getConstantValue(c)) and k > 0 |
i1.(MulInstruction).hasOperands(op, c.getAUse()) and factor = k
or
exists(ShiftLeftInstruction i |
i = i1 and i.getLeftOperand() = op and i.getRightOperand() = c.getAUse() and factor = 2.pow(k)
)
)
}
private predicate boundFlowStepDiv(Instruction i1, Operand op, int factor) {
exists(Instruction c, int k | k = getValue(getConstantValue(c)) and k > 0 |
exists(DivInstruction i |
i = i1 and i.getLeftOperand() = op and i.getRight() = c and factor = k
)
or
exists(ShiftRightInstruction i |
i = i1 and i.getLeftOperand() = op and i.getRight() = c and factor = 2.pow(k)
)
)
}
/**
* Holds if `b` is a valid bound for `op`
*/
pragma[noinline]
private predicate boundedNonPhiOperand(
NonPhiOperand op, Bound b, int delta, boolean upper, boolean fromBackEdge, int origdelta,
Reason reason
) {
exists(NonPhiOperand op2, int d1, int d2 |
boundFlowStepSsa(op, op2, d1, upper, reason) and
boundedNonPhiOperand(op2, b, d2, upper, fromBackEdge, origdelta, _) and
delta = d1 + d2
)
or
boundedInstruction(op.getDef(), b, delta, upper, fromBackEdge, origdelta, reason)
or
exists(int d, Reason r1, Reason r2 |
boundedNonPhiOperand(op, b, d, upper, fromBackEdge, origdelta, r2)
|
unequalOperand(op, b, d, r1) and
(
upper = true and delta = d - 1
or
upper = false and delta = d + 1
) and
(
reason = r1
or
reason = r2 and not r2 instanceof NoReason
)
)
}
/**
* Holds if `op1 + delta` is a valid bound for `op2`.
* - `upper = true` : `op2 <= op1 + delta`
* - `upper = false` : `op2 >= op1 + delta`
*/
private predicate boundFlowStepPhi(
PhiInputOperand op2, Operand op1, int delta, boolean upper, Reason reason
) {
op2.getDef().(CopyInstruction).getSourceValueOperand() = op1 and
(upper = true or upper = false) and
reason = TNoReason() and
delta = 0
or
exists(IRGuardCondition guard, boolean testIsTrue |
guard = boundFlowCond(valueNumberOfOperand(op2), op1, delta, upper, testIsTrue) and
guard.controlsEdge(op2.getPredecessorBlock(), op2.getUse().getBlock(), testIsTrue) and
reason = TCondReason(guard)
)
}
private predicate boundedPhiOperand(
PhiInputOperand op, Bound b, int delta, boolean upper, boolean fromBackEdge, int origdelta,
Reason reason
) {
exists(NonPhiOperand op2, int d1, int d2, Reason r1, Reason r2 |
boundFlowStepPhi(op, op2, d1, upper, r1) and
boundedNonPhiOperand(op2, b, d2, upper, fromBackEdge, origdelta, r2) and
delta = d1 + d2 and
(if r1 instanceof NoReason then reason = r2 else reason = r1)
)
or
boundedInstruction(op.getDef(), b, delta, upper, fromBackEdge, origdelta, reason)
or
exists(int d, Reason r1, Reason r2 |
boundedInstruction(op.getDef(), b, d, upper, fromBackEdge, origdelta, r2)
|
unequalOperand(op, b, d, r1) and
(
upper = true and delta = d - 1
or
upper = false and delta = d + 1
) and
(
reason = r1
or
reason = r2 and not r2 instanceof NoReason
)
)
}
/** Holds if `op2 != op1 + delta` at `pos`. */
private predicate unequalFlowStep(Operand op2, Operand op1, int delta, Reason reason) {
exists(IRGuardCondition guard, boolean testIsTrue |
guard = eqFlowCond(valueNumberOfOperand(op2), op1, delta, false, testIsTrue) and
guard.controls(op2.getUse().getBlock(), testIsTrue) and
reason = TCondReason(guard)
)
}
/**
* Holds if `op != b + delta` at `pos`.
*/
private predicate unequalOperand(Operand op, Bound b, int delta, Reason reason) {
exists(Operand op2, int d1, int d2 |
unequalFlowStep(op, op2, d1, reason) and
boundedNonPhiOperand(op2, b, d2, true, _, _, _) and
boundedNonPhiOperand(op2, b, d2, false, _, _, _) and
delta = d1 + d2
)
}
private predicate boundedPhiCandValidForEdge(
PhiInstruction phi, Bound b, int delta, boolean upper, boolean fromBackEdge, int origdelta,
Reason reason, PhiInputOperand op
) {
boundedPhiCand(phi, upper, b, delta, fromBackEdge, origdelta, reason) and
(
exists(int d | boundedPhiInp1(phi, op, b, d, upper) | upper = true and d <= delta)
or
exists(int d | boundedPhiInp1(phi, op, b, d, upper) | upper = false and d >= delta)
or
selfBoundedPhiInp(phi, op, upper)
)
}
/** Weakens a delta to lie in the range `[-1..1]`. */
bindingset[delta, upper]
private int weakenDelta(boolean upper, int delta) {
delta in [-1 .. 1] and result = delta
or
upper = true and result = -1 and delta < -1
or
upper = false and result = 1 and delta > 1
}
private predicate boundedPhiInp(
PhiInstruction phi, PhiInputOperand op, Bound b, int delta, boolean upper, boolean fromBackEdge,
int origdelta, Reason reason
) {
phi.getAnOperand() = op and
exists(int d, boolean fromBackEdge0 |
boundedPhiOperand(op, b, d, upper, fromBackEdge0, origdelta, reason)
or
b.(ValueNumberBound).getInstruction() = op.getDef() and
d = 0 and
(upper = true or upper = false) and
fromBackEdge0 = false and
origdelta = 0 and
reason = TNoReason()
|
if backEdge(phi, op)
then
fromBackEdge = true and
(
fromBackEdge0 = true and delta = weakenDelta(upper, d - origdelta) + origdelta
or
fromBackEdge0 = false and delta = d
)
else (
delta = d and fromBackEdge = fromBackEdge0
)
)
}
pragma[noinline]
private predicate boundedPhiInp1(
PhiInstruction phi, PhiInputOperand op, Bound b, int delta, boolean upper
) {
boundedPhiInp(phi, op, b, delta, upper, _, _, _)
}
private predicate selfBoundedPhiInp(PhiInstruction phi, PhiInputOperand op, boolean upper) {
exists(int d, ValueNumberBound phibound |
phibound.getInstruction() = phi and
boundedPhiInp(phi, op, phibound, d, upper, _, _, _) and
(
upper = true and d <= 0
or
upper = false and d >= 0
)
)
}
pragma[noinline]
private predicate boundedPhiCand(
PhiInstruction phi, boolean upper, Bound b, int delta, boolean fromBackEdge, int origdelta,
Reason reason
) {
exists(PhiInputOperand op |
boundedPhiInp(phi, op, b, delta, upper, fromBackEdge, origdelta, reason)
)
}
/**
* Holds if the value being cast has an upper (for `upper = true`) or lower
* (for `upper = false`) bound within the bounds of the resulting type.
* For `upper = true` this means that the cast will not overflow and for
* `upper = false` this means that the cast will not underflow.
*/
private predicate safeNarrowingCast(NarrowingCastInstruction cast, boolean upper) {
exists(int bound |
boundedNonPhiOperand(cast.getAnOperand(), any(ZeroBound zb), bound, upper, _, _, _)
|
upper = true and bound <= cast.getUpperBound()
or
upper = false and bound >= cast.getLowerBound()
)
}
pragma[noinline]
private predicate boundedCastExpr(
NarrowingCastInstruction cast, Bound b, int delta, boolean upper, boolean fromBackEdge,
int origdelta, Reason reason
) {
boundedNonPhiOperand(cast.getAnOperand(), b, delta, upper, fromBackEdge, origdelta, reason)
}
/**
* Holds if `b + delta` is a valid bound for `i`.
* - `upper = true` : `i <= b + delta`
* - `upper = false` : `i >= b + delta`
*/
private predicate boundedInstruction(
Instruction i, Bound b, int delta, boolean upper, boolean fromBackEdge, int origdelta,
Reason reason
) {
i instanceof PhiInstruction and
forex(PhiInputOperand op | op = i.getAnOperand() |
boundedPhiCandValidForEdge(i, b, delta, upper, fromBackEdge, origdelta, reason, op)
)
or
i = b.getInstruction(delta) and
(upper = true or upper = false) and
fromBackEdge = false and
origdelta = delta and
reason = TNoReason()
or
exists(Operand mid, int d1, int d2 |
boundFlowStep(i, mid, d1, upper) and
boundedNonPhiOperand(mid, b, d2, upper, fromBackEdge, origdelta, reason) and
delta = d1 + d2 and
not exists(getValue(getConstantValue(i)))
)
or
exists(Operand mid, int factor, int d |
boundFlowStepMul(i, mid, factor) and
boundedNonPhiOperand(mid, b, d, upper, fromBackEdge, origdelta, reason) and
b instanceof ZeroBound and
delta = d * factor and
not exists(getValue(getConstantValue(i)))
)
or
exists(Operand mid, int factor, int d |
boundFlowStepDiv(i, mid, factor) and
boundedNonPhiOperand(mid, b, d, upper, fromBackEdge, origdelta, reason) and
d >= 0 and
b instanceof ZeroBound and
delta = d / factor and
not exists(getValue(getConstantValue(i)))
)
or
exists(NarrowingCastInstruction cast |
cast = i and
safeNarrowingCast(cast, upper.booleanNot()) and
boundedCastExpr(cast, b, delta, upper, fromBackEdge, origdelta, reason)
)
or
exists(PropertyAccess pa |
i.(CallInstruction).getAST() = pa and
pa.getProperty().getName() = "Length" and
b instanceof ZeroBound and
delta = origdelta and
(upper = true or upper = false) and
fromBackEdge = false and
delta = getArrayDim(pa.getQualifier().(VariableAccess).getTarget()) and
reason = TNoReason()
)
}

97
csharp/ql/src/semmle/code/csharp/ir/rangeanalysis/RangeUtils.qll Normal file
View File

@@ -0,0 +1,97 @@
import csharp
private import semmle.code.csharp.ir.IR
// TODO: move this dependency
import semmle.code.csharp.ir.internal.IntegerConstant
// TODO: move this out of test code
language[monotonicAggregates]
IntValue getConstantValue(Instruction instr) {
result = instr.(IntegerConstantInstruction).getValue().toInt()
or
exists(BinaryInstruction binInstr, IntValue left, IntValue right |
binInstr = instr and
left = getConstantValue(binInstr.getLeft()) and
right = getConstantValue(binInstr.getRight()) and
(
binInstr instanceof AddInstruction and result = add(left, right)
or
binInstr instanceof SubInstruction and result = sub(left, right)
or
binInstr instanceof MulInstruction and result = mul(left, right)
or
binInstr instanceof DivInstruction and result = div(left, right)
)
)
or
result = getConstantValue(instr.(CopyInstruction).getSourceValue())
or
exists(PhiInstruction phi |
phi = instr and
result = max(PhiInputOperand operand |
operand = phi.getAnOperand()
|
getConstantValue(operand.getDef())
) and
result = min(PhiInputOperand operand |
operand = phi.getAnOperand()
|
getConstantValue(operand.getDef())
)
)
}
/**
* Gets the dimension of the array (either the declared size, or the
* size of the initializer); if no size is declared and no initializer used,
* the predicate does not hold.
*/
IntValue getArrayDim(Variable arr) {
exists(ArrayCreation ac |
arr.getInitializer() = ac and
if exists(ac.getLengthArgument(0))
then result = ac.getLengthArgument(0).getValue().toInt()
else
if exists(ac.getInitializer())
then result = ac.getInitializer().getNumberOfElements()
else none()
)
}
predicate valueFlowStep(Instruction i, Operand op, int delta) {
i.(CopyInstruction).getSourceValueOperand() = op and delta = 0
or
exists(Operand x |
i.(AddInstruction).getAnOperand() = op and
i.(AddInstruction).getAnOperand() = x and
op != x
|
delta = getValue(getConstantValue(x.getDef()))
)
or
exists(Operand x |
i.(SubInstruction).getLeftOperand() = op and
i.(SubInstruction).getRightOperand() = x
|
delta = -getValue(getConstantValue(x.getDef()))
)
or
exists(Operand x |
i.(PointerAddInstruction).getAnOperand() = op and
i.(PointerAddInstruction).getAnOperand() = x and
op != x
|
delta = i.(PointerAddInstruction).getElementSize() * getValue(getConstantValue(x.getDef()))
)
or
exists(Operand x |
i.(PointerSubInstruction).getLeftOperand() = op and
i.(PointerSubInstruction).getRightOperand() = x
|
delta = i.(PointerSubInstruction).getElementSize() * -getValue(getConstantValue(x.getDef()))
)
}
predicate backEdge(PhiInstruction phi, PhiInputOperand op) {
phi.getAnOperand() = op and
phi.getBlock() = op.getPredecessorBlock().getBackEdgeSuccessor(_)
}

585
csharp/ql/src/semmle/code/csharp/ir/rangeanalysis/SignAnalysis.qll Normal file
View File

@@ -0,0 +1,585 @@
/**
* 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 csharp
private import semmle.code.csharp.ir.IR
private import semmle.code.csharp.ir.internal.IRGuards
private import semmle.code.csharp.ir.ValueNumbering
private import SignAnalysisCached
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()
}
}
private Sign certainInstructionSign(Instruction inst) {
exists(int i | inst.(IntegerConstantInstruction).getValue().toInt() = i |
i < 0 and result = TNeg()
or
i = 0 and result = TZero()
or
i > 0 and result = TPos()
)
or
exists(float f | f = inst.(FloatConstantInstruction).getValue().toFloat() |
f < 0 and result = TNeg()
or
f = 0 and result = TZero()
or
f > 0 and result = TPos()
)
}
private newtype CastKind =
TWiden() or
TSame() or
TNarrow()
private CastKind getCastKind(ConvertInstruction ci) {
exists(int fromSize, int toSize |
toSize = ci.getResultSize() and
fromSize = ci.getUnary().getResultSize()
|
fromSize < toSize and
result = TWiden()
or
fromSize = toSize and
result = TSame()
or
fromSize > toSize and
result = TNarrow()
)
}
private predicate bindBool(boolean bool) {
bool = true or
bool = false
}
private Sign castSign(Sign s, boolean fromSigned, boolean toSigned, CastKind ck) {
result = TZero() and
(
bindBool(fromSigned) and
bindBool(toSigned) and
s = TZero()
or
bindBool(fromSigned) and
bindBool(toSigned) and
ck = TNarrow()
)
or
result = TPos() and
(
bindBool(fromSigned) and
bindBool(toSigned) and
s = TPos()
or
bindBool(fromSigned) and
bindBool(toSigned) and
s = TNeg() and
ck = TNarrow()
or
fromSigned = true and
toSigned = false and
s = TNeg()
)
or
result = TNeg() and
(
fromSigned = true and
toSigned = true and
s = TNeg()
or
fromSigned = false and
toSigned = true and
s = TPos() and
ck != TWiden()
)
}
/** Holds if the sign of `e` is too complicated to determine. */
private predicate unknownSign(Instruction i) {
// REVIEW: This should probably be a list of the instructions that we _do_ understand, rather than
// the ones we don't understand. Currently, if we try to compute the sign of an instruction that
// we don't understand, and it isn't on this list, we incorrectly compute the sign as "none"
// instead of "+,0,-".
// Even better, we could track the state of each instruction as a power set of {non-negative,
// non-positive, non-zero}, which would mean that the representation of the sign of an unknown
// value would be the empty set.
(
i instanceof UnmodeledDefinitionInstruction
or
i instanceof UninitializedInstruction
or
i instanceof InitializeParameterInstruction
or
i instanceof BuiltInOperationInstruction
or
i instanceof CallInstruction
or
i instanceof ChiInstruction
)
}
/**
* Holds if `lowerbound` is a lower bound for `bounded`. This is restricted
* to only include bounds for which we might determine a sign.
*/
private predicate lowerBound(
IRGuardCondition comp, Operand lowerbound, Operand bounded, boolean isStrict
) {
exists(int adjustment, Operand compared |
valueNumberOfOperand(bounded) = valueNumberOfOperand(compared) and
(
isStrict = true and
adjustment = 0
or
isStrict = false and
adjustment = 1
) and
comp.ensuresLt(lowerbound, compared, adjustment, bounded.getUse().getBlock(), true)
)
}
/**
* Holds if `upperbound` is an upper bound for `bounded` at `pos`. This is restricted
* to only include bounds for which we might determine a sign.
*/
private predicate upperBound(
IRGuardCondition comp, Operand upperbound, Operand bounded, boolean isStrict
) {
exists(int adjustment, Operand compared |
valueNumberOfOperand(bounded) = valueNumberOfOperand(compared) and
(
isStrict = true and
adjustment = 0
or
isStrict = false and
adjustment = 1
) and
comp.ensuresLt(compared, upperbound, adjustment, bounded.getUse().getBlock(), true)
)
}
/**
* Holds if `eqbound` is an equality/inequality for `bounded` at `pos`. This is
* restricted to only include bounds for which we might determine a sign. The
* boolean `isEq` gives the polarity:
* - `isEq = true` : `bounded = eqbound`
* - `isEq = false` : `bounded != eqbound`
*/
private predicate eqBound(IRGuardCondition guard, Operand eqbound, Operand bounded, boolean isEq) {
exists(Operand compared |
valueNumberOfOperand(bounded) = valueNumberOfOperand(compared) and
guard.ensuresEq(compared, eqbound, 0, bounded.getUse().getBlock(), isEq)
)
}
/**
* 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(IRGuardCondition comp, Operand bound, Operand op) {
upperBound(comp, bound, op, _) or
eqBound(comp, bound, op, 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(IRGuardCondition comp, Operand bound, Operand op) {
lowerBound(comp, bound, op, _) or
eqBound(comp, bound, op, true)
}
/**
* Holds if `bound` is a bound for `v` at `pos` that can restrict whether `v`
* can be zero.
*/
private predicate zeroBound(IRGuardCondition comp, Operand bound, Operand op) {
lowerBound(comp, bound, op, _) or
upperBound(comp, bound, op, _) or
eqBound(comp, bound, op, _)
}
/** Holds if `bound` allows `v` to be positive at `pos`. */
private predicate posBoundOk(IRGuardCondition comp, Operand bound, Operand op) {
posBound(comp, bound, op) and TPos() = operandSign(bound)
}
/** Holds if `bound` allows `v` to be negative at `pos`. */
private predicate negBoundOk(IRGuardCondition comp, Operand bound, Operand op) {
negBound(comp, bound, op) and TNeg() = operandSign(bound)
}
/** Holds if `bound` allows `v` to be zero at `pos`. */
private predicate zeroBoundOk(IRGuardCondition comp, Operand bound, Operand op) {
lowerBound(comp, bound, op, _) and TNeg() = operandSign(bound)
or
lowerBound(comp, bound, op, false) and TZero() = operandSign(bound)
or
upperBound(comp, bound, op, _) and TPos() = operandSign(bound)
or
upperBound(comp, bound, op, false) and TZero() = operandSign(bound)
or
eqBound(comp, bound, op, true) and TZero() = operandSign(bound)
or
eqBound(comp, bound, op, false) and TZero() != operandSign(bound)
}
private Sign binaryOpLhsSign(BinaryInstruction i) { result = operandSign(i.getLeftOperand()) }
private Sign binaryOpRhsSign(BinaryInstruction i) { result = operandSign(i.getRightOperand()) }
pragma[noinline]
private predicate binaryOpSigns(BinaryInstruction i, Sign lhs, Sign rhs) {
lhs = binaryOpLhsSign(i) and
rhs = binaryOpRhsSign(i)
}
private Sign unguardedOperandSign(Operand operand) {
result = instructionSign(operand.getDef()) and
not hasGuard(operand, result)
}
private Sign guardedOperandSign(Operand operand) {
result = instructionSign(operand.getDef()) and
hasGuard(operand, result)
}
private Sign guardedOperandSignOk(Operand operand) {
result = TPos() and
forex(IRGuardCondition guard, Operand bound | posBound(guard, bound, operand) |
posBoundOk(guard, bound, operand)
)
or
result = TNeg() and
forex(IRGuardCondition guard, Operand bound | negBound(guard, bound, operand) |
negBoundOk(guard, bound, operand)
)
or
result = TZero() and
forex(IRGuardCondition guard, Operand bound | zeroBound(guard, bound, operand) |
zeroBoundOk(guard, bound, operand)
)
}
/**
* Holds if there is a bound that might restrict whether `v` has the sign `s`
* at `pos`.
*/
private predicate hasGuard(Operand op, Sign s) {
s = TPos() and posBound(_, _, op)
or
s = TNeg() and negBound(_, _, op)
or
s = TZero() and zeroBound(_, _, op)
}
cached
module SignAnalysisCached {
/**
* Gets a sign that `operand` may have at `pos`, taking guards into account.
*/
cached
Sign operandSign(Operand operand) {
result = unguardedOperandSign(operand)
or
result = guardedOperandSign(operand) and
result = guardedOperandSignOk(operand)
or
// `result` is unconstrained if the definition is inexact. Then any sign is possible.
operand.isDefinitionInexact()
}
cached
Sign instructionSign(Instruction i) {
result = certainInstructionSign(i)
or
not exists(certainInstructionSign(i)) and
not (
result = TNeg() and
i.getResultType() instanceof UnsignedIntegralType
) and
(
unknownSign(i)
or
exists(ConvertInstruction ci, Instruction prior, boolean fromSigned, boolean toSigned |
i = ci and
prior = ci.getUnary() and
(
if ci.getResultType() instanceof SignedIntegralType
then toSigned = true
else toSigned = false
) and
(
if prior.getResultType() instanceof SignedIntegralType
then fromSigned = true
else fromSigned = false
) and
result = castSign(operandSign(ci.getAnOperand()), fromSigned, toSigned, getCastKind(ci))
)
or
result = operandSign(i.(CopyInstruction).getSourceValueOperand())
or
result = operandSign(i.(BitComplementInstruction).getAnOperand()).bitnot()
or
result = operandSign(i.(NegateInstruction).getAnOperand()).neg()
or
exists(Sign s1, Sign s2 | binaryOpSigns(i, s1, s2) |
i instanceof AddInstruction and result = s1.add(s2)
or
i instanceof SubInstruction and result = s1.add(s2.neg())
or
i instanceof MulInstruction and result = s1.mul(s2)
or
i instanceof DivInstruction and result = s1.div(s2)
or
i instanceof RemInstruction and result = s1.rem(s2)
or
i instanceof BitAndInstruction and result = s1.bitand(s2)
or
i instanceof BitOrInstruction and result = s1.bitor(s2)
or
i instanceof BitXorInstruction and result = s1.bitxor(s2)
or
i instanceof ShiftLeftInstruction and result = s1.lshift(s2)
or
i instanceof ShiftRightInstruction and
i.getResultType().(IntegralType) instanceof SignedIntegralType and
result = s1.rshift(s2)
or
i instanceof ShiftRightInstruction and
not i.getResultType().(IntegralType) instanceof SignedIntegralType and
result = s1.urshift(s2)
)
or
// use hasGuard here?
result = operandSign(i.(PhiInstruction).getAnOperand())
)
}
}
/** Holds if `i` can be positive and cannot be negative. */
predicate positiveInstruction(Instruction i) {
instructionSign(i) = TPos() and
not instructionSign(i) = TNeg()
}
/** Holds if `i` at `pos` can be positive at and cannot be negative. */
predicate positive(Operand op) {
operandSign(op) = TPos() and
not operandSign(op) = TNeg()
}
/** Holds if `i` can be negative and cannot be positive. */
predicate negativeInstruction(Instruction i) {
instructionSign(i) = TNeg() and
not instructionSign(i) = TPos()
}
/** Holds if `i` at `pos` can be negative and cannot be positive. */
predicate negative(Operand op) {
operandSign(op) = TNeg() and
not operandSign(op) = TPos()
}
/** Holds if `i` is strictly positive. */
predicate strictlyPositiveInstruction(Instruction i) {
instructionSign(i) = TPos() and
not instructionSign(i) = TNeg() and
not instructionSign(i) = TZero()
}
/** Holds if `i` is strictly positive at `pos`. */
predicate strictlyPositive(Operand op) {
operandSign(op) = TPos() and
not operandSign(op) = TNeg() and
not operandSign(op) = TZero()
}
/** Holds if `i` is strictly negative. */
predicate strictlyNegativeInstruction(Instruction i) {
instructionSign(i) = TNeg() and
not instructionSign(i) = TPos() and
not instructionSign(i) = TZero()
}
/** Holds if `i` is strictly negative at `pos`. */
predicate strictlyNegative(Operand op) {
operandSign(op) = TNeg() and
not operandSign(op) = TPos() and
not operandSign(op) = TZero()
}

5
csharp/ql/test/library-tests/ir/offbyone/OffByOneRA.expected Normal file
View File

@@ -0,0 +1,5 @@
| test.cs:21:17:21:21 | Test2 | test.cs:34:41:34:51 | access to array element | This array access might be out of bounds, as the index might be equal to the array length |
| test.cs:56:17:56:21 | Test4 | test.cs:67:41:67:51 | access to array element | This array access might be out of bounds, as the index might be equal to the array length |
| test.cs:71:17:71:21 | Test5 | test.cs:77:22:77:27 | access to indexer | This array access might be out of bounds, as the index might be equal to the array length |
| test.cs:81:17:81:21 | Test6 | test.cs:90:41:90:55 | access to array element | This array access might be out of bounds, as the index might be equal to the array length |
| test.cs:94:17:94:21 | Test7 | test.cs:104:41:104:50 | access to array element | This array access might be out of bounds, as the index might be equal to the array length + 1 |

51
csharp/ql/test/library-tests/ir/offbyone/OffByOneRA.ql Normal file
View File

@@ -0,0 +1,51 @@
import csharp
import semmle.code.csharp.ir.IR
import semmle.code.csharp.ir.rangeanalysis.RangeAnalysis
import semmle.code.csharp.ir.rangeanalysis.RangeUtils
/**
* Holds if the index expression of `aa` is less than or equal to the array length plus `k`.
*/
predicate boundedArrayAccess(ElementAccess aa, int k) {
exists(Instruction index, Instruction usage, Bound b, int delta |
(
// indexer access
usage.(CallInstruction).getAST() = aa
or
// array access
usage.(PointerAddInstruction).getAST() = aa
) and
usage.getAnOperand().getDef() = index and
boundedInstruction(index, b, delta, true, _)
|
exists(PropertyAccess pa |
k = delta and
b.getInstruction().getAST() = pa and
pa.getProperty().getName() = "Length" and
pa.(QualifiableExpr).getQualifier().(VariableAccess).getTarget() = aa
.getQualifier()
.(VariableAccess)
.getTarget()
)
or
b instanceof ZeroBound and
k = delta - getArrayDim(aa.getQualifier().(VariableAccess).getTarget())
)
}
/**
* Holds if the index expression is less than or equal to the array length plus `k`,
* but not necessarily less than or equal to the array length plus `k-1`.
*/
predicate bestArrayAccessBound(ElementAccess aa, int k) {
k = min(int k0 | boundedArrayAccess(aa, k0))
}
from ElementAccess aa, int k, string msg, string add
where
bestArrayAccessBound(aa, k) and
k >= 0 and
(if k = 0 then add = "" else add = " + " + k) and
msg = "This array access might be out of bounds, as the index might be equal to the array length" +
add
select aa.getEnclosingCallable(), aa, msg

5
csharp/ql/test/library-tests/ir/offbyone/null.cs Normal file
View File

@@ -0,0 +1,5 @@
class Null {
public static void Main() {
object o = null;
}
}

107
csharp/ql/test/library-tests/ir/offbyone/test.cs Normal file
View File

@@ -0,0 +1,107 @@
class ContainerLengthOffByOne
{
public int[] arr;
public string str;
public static void Fun(int elem)
{
}
public void Test1()
{
int len1 = this.arr.Length;
int len2 = len1 + 1;
// OK
for(int i = 0; i < len2 - 1; i++)
{
ContainerLengthOffByOne.Fun(this.arr[i]);
}
}
public void Test2()
{
int len1 = this.arr.Length;
int len2;
if (len1 % 2 == 0)
len2 = len1 + 1;
else
len2 = len1;
// Not OK, PHI node where the upper bound
// exceeds the size of the array.
for(int i = 0; i < len2; i++)
{
ContainerLengthOffByOne.Fun(this.arr[i]);
}
}
public void Test3()
{
int len1 = this.arr.Length;
int len2 = len1 - 1;
int len3;
if (len2 % 2 == 0)
len3 = len2 + 1;
else
len3 = len2;
// OK, PHI node has bounds that ensure
// we don't get an off by one error.
for(int i = 0; i < len3; i++)
{
ContainerLengthOffByOne.Fun(this.arr[i]);
}
}
public void Test4()
{
int len1 = this.arr.Length;
int len2 = len1 + 1;
int len3 = len2 - 1;
int len4 = len3 + 2;
int len5 = len4 - 1;
// Not OK, len5 is off by one.
for(int i = 0; i < len5; i++)
{
ContainerLengthOffByOne.Fun(this.arr[i]);
}
}
public void Test5()
{
int len = this.str.Length;
// Not OK; test for indexers
for (int i = 0; i <= len; i++)
{
char c = str[i];
}
}
public void Test6()
{
int len = this.arr.Length - 2;
int len1 = len + 3;
int len2 = len1 - 1;
// Not OK, off by one
// The test shows that more complex expressions are treated correctly
for (int i = 0; i < len2; i++)
{
ContainerLengthOffByOne.Fun(this.arr[i + 1]);
}
}
public void Test7()
{
int[] arrInit = { 1, 2, 3 };
int len = (arrInit.Length * 2 + 2) / 2 * 2;
int len1 = len / 2 - 3 + 4;
// Not OK, len1 == this.arrInit + 1
// This test shows that array initializer's length
// are used in bounds
for (int i = 0; i < len1; i++)
{
ContainerLengthOffByOne.Fun(arrInit[i]);
}
}
}

18
csharp/ql/test/library-tests/ir/rangeanalysis/RangeAnalysis.expected Normal file
View File

@@ -0,0 +1,18 @@
| test.cs:22:12:22:12 | Store: access to parameter x | test.cs:16:24:16:24 | InitializeParameter: x | 0 | false | NoReason | file://:0:0:0:0 | :0:0:0:0 |
| test.cs:22:12:22:12 | Store: access to parameter x | test.cs:16:31:16:31 | InitializeParameter: y | 0 | false | CompareLT: ... < ... | test.cs:18:9:18:13 | test.cs:18:9:18:13 |
| test.cs:22:12:22:12 | Store: access to parameter x | test.cs:16:31:16:31 | InitializeParameter: y | 0 | false | NoReason | file://:0:0:0:0 | :0:0:0:0 |
| test.cs:36:12:36:12 | Store: access to parameter x | test.cs:26:24:26:24 | InitializeParameter: x | -2 | false | NoReason | file://:0:0:0:0 | :0:0:0:0 |
| test.cs:36:12:36:12 | Store: access to parameter x | test.cs:26:31:26:31 | InitializeParameter: y | -2 | false | CompareLT: ... < ... | test.cs:28:9:28:13 | test.cs:28:9:28:13 |
| test.cs:45:12:45:12 | Load: access to local variable i | file://:0:0:0:0 | 0 | 0 | false | NoReason | file://:0:0:0:0 | :0:0:0:0 |
| test.cs:45:12:45:12 | Load: access to local variable i | test.cs:40:25:40:25 | InitializeParameter: x | -1 | true | CompareLT: ... < ... | test.cs:43:20:43:24 | test.cs:43:20:43:24 |
| test.cs:49:12:49:12 | Load: access to local variable i | file://:0:0:0:0 | 0 | 1 | false | CompareGT: ... > ... | test.cs:47:20:47:24 | test.cs:47:20:47:24 |
| test.cs:49:12:49:12 | Load: access to local variable i | test.cs:40:25:40:25 | InitializeParameter: x | 0 | true | NoReason | file://:0:0:0:0 | :0:0:0:0 |
| test.cs:49:12:49:12 | Load: access to local variable i | test.cs:43:20:43:20 | Phi: access to local variable i | 0 | true | CompareLT: ... < ... | test.cs:43:20:43:24 | test.cs:43:20:43:24 |
| test.cs:53:12:53:12 | Load: access to local variable i | file://:0:0:0:0 | 0 | 0 | false | NoReason | file://:0:0:0:0 | :0:0:0:0 |
| test.cs:53:12:53:12 | Load: access to local variable i | test.cs:40:25:40:25 | InitializeParameter: x | 1 | true | CompareLT: ... < ... | test.cs:51:20:51:28 | test.cs:51:20:51:28 |
| test.cs:53:12:53:12 | Load: access to local variable i | test.cs:43:20:43:20 | Phi: access to local variable i | 1 | true | CompareLT: ... < ... | test.cs:51:20:51:28 | test.cs:51:20:51:28 |
| test.cs:53:12:53:12 | Load: access to local variable i | test.cs:47:20:47:20 | Phi: access to local variable i | 0 | false | CompareGT: ... > ... | test.cs:47:20:47:24 | test.cs:47:20:47:24 |
| test.cs:62:13:62:17 | Load: access to parameter begin | test.cs:58:33:58:37 | InitializeParameter: begin | 0 | false | NoReason | file://:0:0:0:0 | :0:0:0:0 |
| test.cs:74:14:74:14 | Load: access to parameter x | test.cs:68:32:68:32 | InitializeParameter: y | -1 | true | CompareLT: ... < ... | test.cs:72:11:72:15 | test.cs:72:11:72:15 |
| test.cs:74:14:74:14 | Load: access to parameter x | test.cs:68:39:68:39 | InitializeParameter: z | -2 | true | CompareLT: ... < ... | test.cs:72:11:72:15 | test.cs:72:11:72:15 |
| test.cs:81:14:81:14 | Load: access to parameter x | test.cs:68:32:68:32 | InitializeParameter: y | -1 | true | CompareLT: ... < ... | test.cs:77:9:77:13 | test.cs:77:9:77:13 |

25
csharp/ql/test/library-tests/ir/rangeanalysis/RangeAnalysis.ql Normal file
View File

@@ -0,0 +1,25 @@
import semmle.code.csharp.ir.rangeanalysis.RangeAnalysis
import semmle.code.csharp.ir.IR
import semmle.code.csharp.ir.internal.IRGuards
import semmle.code.csharp.ir.ValueNumbering
query predicate instructionBounds(
Instruction i, Bound b, int delta, boolean upper, Reason reason, Location reasonLoc
) {
(
i.getAUse() instanceof ArgumentOperand
or
exists(ReturnValueInstruction retInstr | retInstr.getReturnValueOperand() = i.getAUse())
) and
(
upper = true and
delta = min(int d | boundedInstruction(i, b, d, upper, reason))
or
upper = false and
delta = max(int d | boundedInstruction(i, b, d, upper, reason))
) and
not valueNumber(b.getInstruction()) = valueNumber(i) and
if reason instanceof CondReason
then reasonLoc = reason.(CondReason).getCond().getLocation()
else reasonLoc instanceof EmptyLocation
}

5
csharp/ql/test/library-tests/ir/rangeanalysis/null.cs Normal file
View File

@@ -0,0 +1,5 @@
class Null {
public static void Main() {
object o = null;
}
}

85
csharp/ql/test/library-tests/ir/rangeanalysis/test.cs Normal file
View File

@@ -0,0 +1,85 @@
class RangeAnalysis {
static void Sink(int val)
{
}
static unsafe void Sinkp(int* p)
{
}
static int Source()
{
return 0;
}
// Guards, inference, critical edges
static int Test1(int x, int y)
{
if (x < y)
{
x = y;
}
return x;
}
// Bounds mergers at phi nodes
static int Test2(int x, int y)
{
if (x < y)
{
x = y;
}
else
{
x = x - 2;
}
return x;
}
// for loops
static void Test3(int x)
{
int y = x;
for(int i = 0; i < x; i++)
{
Sink(i);
}
for(int i = y; i > 0; i--)
{
Sink(i);
}
for(int i = 0; i < y + 2; i++)
{
Sink(i);
}
}
// pointer bounds
unsafe static void Test4(int *begin, int *end)
{
while (begin < end)
{
Sinkp(begin);
begin++;
}
}
// bound propagation through conditionals
static void Test5(int x, int y, int z)
{
if (y < z)
{
if (x < y)
{
Sink(x);
}
}
if (x < y)
{
if (y < z)
{
Sink(x); // x < z is not inferred here
}
}
}
}