C#: Teach guards library about custom null guards

This commit is contained in:
Tom Hvitved
2018-11-06 09:52:58 +01:00
parent a5dfc10197
commit e4aa196c37
5 changed files with 172 additions and 34 deletions

View File

@@ -2473,7 +2473,7 @@ module ControlFlow {
not startsBB(succ)
}
predicate bbIndex(ControlFlowElement bbStart, ControlFlowElement cfe, int i) =
private predicate bbIndex(ControlFlowElement bbStart, ControlFlowElement cfe, int i) =
shortestDistances(startsBB/1, intraBBSucc/2)(bbStart, cfe, i)
private predicate succBB(PreBasicBlock pred, PreBasicBlock succ) {
@@ -2488,13 +2488,9 @@ module ControlFlow {
idominance(entryBB/1, succBB/2)(_, dom, bb)
class PreBasicBlock extends ControlFlowElement {
PreBasicBlock() {
startsBB(this)
}
PreBasicBlock() { startsBB(this) }
PreBasicBlock getASuccessor() {
result = succ(this.getLastElement(), _)
}
PreBasicBlock getASuccessor() { result = succ(this.getLastElement(), _) }
PreBasicBlock getAPredecessor() {
result.getASuccessor() = this
@@ -2548,6 +2544,22 @@ module ControlFlow {
exists(succExit(this.getLastElement(), c))
) > 1
}
private predicate isCandidateSuccessor(PreBasicBlock succ, ConditionalCompletion c) {
succ = succ(this.getLastElement(), c) and
forall(PreBasicBlock pred |
pred = succ.getAPredecessor() and pred != this |
succ.dominates(pred)
)
}
predicate controls(PreBasicBlock controlled, ConditionalSuccessor s) {
exists(PreBasicBlock succ, ConditionalCompletion c |
isCandidateSuccessor(succ, c) |
succ.dominates(controlled) and
s.matchesCompletion(c)
)
}
}
}
@@ -2729,29 +2741,21 @@ module ControlFlow {
ssaRefRank(bb2, i2, v, _) = 1
}
private cached module PreSsaCached {
cached
predicate firstReadSameVar(Definition def, LocalScopeVariableRead read) {
exists(SimpleLocalScopeVariable v, PreBasicBlock b1, int i1, PreBasicBlock b2, int i2 |
adjacentVarRefs(v, b1, i1, b2, i2) and
defAt(b1, i1, def, v) and
readAt(b2, i2, read, v)
)
}
cached
predicate adjacentReadPairSameVar(LocalScopeVariableRead read1, LocalScopeVariableRead read2) {
exists(SimpleLocalScopeVariable v, PreBasicBlock bb1, int i1, PreBasicBlock bb2, int i2 |
adjacentVarRefs(v, bb1, i1, bb2, i2) and
readAt(bb1, i1, read1, v) and
readAt(bb2, i2, read2, v)
)
}
cached
predicate forceCachingInSameStage() { any() }
predicate firstReadSameVar(Definition def, LocalScopeVariableRead read) {
exists(SimpleLocalScopeVariable v, PreBasicBlock b1, int i1, PreBasicBlock b2, int i2 |
adjacentVarRefs(v, b1, i1, b2, i2) and
defAt(b1, i1, def, v) and
readAt(b2, i2, read, v)
)
}
predicate adjacentReadPairSameVar(LocalScopeVariableRead read1, LocalScopeVariableRead read2) {
exists(SimpleLocalScopeVariable v, PreBasicBlock bb1, int i1, PreBasicBlock bb2, int i2 |
adjacentVarRefs(v, bb1, i1, bb2, i2) and
readAt(bb1, i1, read1, v) and
readAt(bb2, i2, read2, v)
)
}
import PreSsaCached
}
/**
@@ -3837,10 +3841,12 @@ module ControlFlow {
}
private cached module Cached {
private import semmle.code.csharp.controlflow.Guards as Guards
cached
newtype TPreSsaDef =
TExplicitPreSsaDef(PreBasicBlocks::PreBasicBlock bb, int i, AssignableDefinition def, LocalScopeVariable v) {
PreSsa::forceCachingInSameStage() and
Guards::Internal::CachedWithCFG::forceCachingInSameStage() and
PreSsa::assignableDefAt(bb, i, def, v)
}
or

View File

@@ -162,9 +162,11 @@ class DereferenceableExpr extends Expr {
if ck.isInequality() then branch = false else branch = true
)
or
// Call to `string.IsNullOrEmpty()`
result = any(MethodCall mc |
mc.getTarget() = any(SystemStringClass c).getIsNullOrEmptyMethod() and
// Call to `string.IsNullOrEmpty()` or `string.IsNullOrWhiteSpace()`
exists(MethodCall mc, string name |
result = mc |
mc.getTarget() = any(SystemStringClass c).getAMethod(name) and
name.regexpMatch("IsNullOr(Empty|WhiteSpace)") and
mc.getArgument(0) = this and
branch = false and
isNull = false
@@ -179,6 +181,8 @@ class DereferenceableExpr extends Expr {
// E.g. `x is string` or `x is ""`
(branch = true and isNull = false)
)
or
isCustomNullCheck(result, this, v, isNull)
)
}
@@ -491,6 +495,15 @@ module Internal {
)
}
/** Holds if pre basic block `bb` only is reached when `e` has abstract value `v`. */
private predicate preControls(PreBasicBlocks::PreBasicBlock bb, Expr e, AbstractValue v) {
exists(PreBasicBlocks::ConditionBlock cb, ConditionalSuccessor s, AbstractValue v0, Expr cond |
cb.controls(bb, s) |
v0.branchImplies(cb.getLastElement(), s, cond) and
impliesSteps(cond, v0, e, v)
)
}
/**
* Holds if assertion `a` directly asserts that expression `e` evaluates to
* value `v`.
@@ -521,6 +534,86 @@ module Internal {
)
}
private Expr stripConditionalExpr(Expr e) {
e = any(ConditionalExpr ce |
result = stripConditionalExpr(ce.getThen())
or
result = stripConditionalExpr(ce.getElse())
)
or
not e instanceof ConditionalExpr and
result = e
}
private predicate canReturn(Callable c, Expr ret) {
exists(Expr e | c.canReturn(e) | ret = stripConditionalExpr(e))
}
private class PreSsaImplicitParameterDefinition extends PreSsa::Definition {
private Parameter p;
PreSsaImplicitParameterDefinition() {
p = this.getDefinition().(AssignableDefinitions::ImplicitParameterDefinition).getParameter()
}
Parameter getParameter() { result = p }
/**
* Holds if the callable that this parameter belongs to can return `ret`, but
* only if this parameter is `null` or non-`null`, as specified by `isNull`.
*/
predicate nullGuardedReturn(Expr ret, boolean isNull) {
canReturn(p.getCallable(), ret) and
exists(PreBasicBlocks::PreBasicBlock bb, NullValue nv |
preControls(bb, this.getARead(), nv) |
ret = bb.getAnElement() and
if nv.isNull() then isNull = true else isNull = false
)
}
}
/**
* Holds if `ret` is an expression returned by the callable to which parameter
* `p` belongs, and `ret` having Boolean value `retVal` allows the conclusion
* that the parameter `p` either is `null` or non-`null`, as specified by `isNull`.
*/
private predicate validReturnInCustomNullCheck(Expr ret, Parameter p, BooleanValue retVal, boolean isNull) {
exists(Callable c |
canReturn(c, ret) |
p.getCallable() = c and
c.getReturnType() instanceof BoolType
) and
exists(PreSsaImplicitParameterDefinition def |
p = def.getParameter() |
def.nullGuardedReturn(ret, isNull)
or
exists(NullValue nv |
impliesSteps(ret, retVal, def.getARead(), nv) |
if nv.isNull() then isNull = true else isNull = false
)
)
}
/**
* Gets a non-overridable callable with a Boolean return value that performs a
* `null`-check on parameter `p`. A return value having Boolean value `retVal`
* allows us to conclude that the argument either is `null` or non-`null`, as
* specified by `isNull`.
*/
private Callable customNullCheck(Parameter p, BooleanValue retVal, boolean isNull) {
result.getReturnType() instanceof BoolType and
not result.(Virtualizable).isOverridableOrImplementable() and
p.getCallable() = result and
not p.isParams() and
p.getType() = any(Type t | t instanceof RefType or t instanceof NullableType) and
forex(Expr ret |
canReturn(result, ret) and
not ret.(BoolLiteral).getBoolValue() = retVal.getValue().booleanNot()
|
validReturnInCustomNullCheck(ret, p, retVal, isNull)
)
}
private cached module Cached {
pragma[noinline]
private predicate isGuardedBy0(AccessOrCallExpr guarded, Expr e, AccessOrCallExpr sub, AbstractValue v) {
@@ -541,6 +634,21 @@ module Internal {
guarded.getSsaQualifier() = sub.getSsaQualifier()
)
}
}
import Cached
// The predicates in this module should be cached in the same stage as the cache stage
// in ControlFlowGraph.qll. This is to avoid recomputation of pre-basic-blocks and
// pre-SSA predicates
cached module CachedWithCFG {
cached
predicate isCustomNullCheck(Call call, Expr arg, BooleanValue v, boolean isNull) {
exists(Callable callable, Parameter p |
arg = call.getArgumentForParameter(any(Parameter p0 | p0.getSourceDeclaration() = p)) and
call.getTarget().getSourceDeclaration() = callable and
callable = customNullCheck(p, v, isNull)
)
}
/**
* Holds if `e1` having abstract value `v1` implies that `e2` has abstract
@@ -659,8 +767,11 @@ module Internal {
v1 instanceof NullValue and
v1 = v2
}
cached
predicate forceCachingInSameStage() { any() }
}
import Cached
import CachedWithCFG
/**
* Holds if `e1` having some abstract value, `v`, implies that `e2` has the same

View File

@@ -150,12 +150,17 @@
| Guards.cs:162:24:162:24 | access to parameter o | Guards.cs:151:17:151:17 | access to parameter o | Guards.cs:151:17:151:17 | access to parameter o | non-null |
| Guards.cs:169:31:169:31 | access to parameter x | Guards.cs:168:13:168:41 | !... | Guards.cs:168:40:168:40 | access to parameter x | true |
| Guards.cs:169:31:169:31 | access to parameter x | Guards.cs:168:14:168:41 | call to method IsNullOrWhiteSpace | Guards.cs:168:40:168:40 | access to parameter x | false |
| Guards.cs:169:31:169:31 | access to parameter x | Guards.cs:168:40:168:40 | access to parameter x | Guards.cs:168:40:168:40 | access to parameter x | non-null |
| Guards.cs:190:31:190:31 | access to parameter s | Guards.cs:189:13:189:25 | !... | Guards.cs:189:24:189:24 | access to parameter s | true |
| Guards.cs:190:31:190:31 | access to parameter s | Guards.cs:189:14:189:25 | call to method NullTest1 | Guards.cs:189:24:189:24 | access to parameter s | false |
| Guards.cs:190:31:190:31 | access to parameter s | Guards.cs:189:24:189:24 | access to parameter s | Guards.cs:189:24:189:24 | access to parameter s | non-null |
| Guards.cs:192:31:192:31 | access to parameter s | Guards.cs:191:13:191:25 | !... | Guards.cs:191:24:191:24 | access to parameter s | true |
| Guards.cs:192:31:192:31 | access to parameter s | Guards.cs:191:14:191:25 | call to method NullTest2 | Guards.cs:191:24:191:24 | access to parameter s | false |
| Guards.cs:192:31:192:31 | access to parameter s | Guards.cs:191:24:191:24 | access to parameter s | Guards.cs:191:24:191:24 | access to parameter s | non-null |
| Guards.cs:194:31:194:31 | access to parameter s | Guards.cs:193:13:193:25 | !... | Guards.cs:193:24:193:24 | access to parameter s | true |
| Guards.cs:194:31:194:31 | access to parameter s | Guards.cs:193:14:193:25 | call to method NullTest3 | Guards.cs:193:24:193:24 | access to parameter s | false |
| Guards.cs:194:31:194:31 | access to parameter s | Guards.cs:193:24:193:24 | access to parameter s | Guards.cs:193:24:193:24 | access to parameter s | non-null |
| Guards.cs:196:31:196:31 | access to parameter s | Guards.cs:195:13:195:27 | call to method NotNullTest4 | Guards.cs:195:26:195:26 | access to parameter s | true |
| Guards.cs:196:31:196:31 | access to parameter s | Guards.cs:195:26:195:26 | access to parameter s | Guards.cs:195:26:195:26 | access to parameter s | non-null |
| Guards.cs:198:31:198:31 | access to parameter s | Guards.cs:197:13:197:29 | !... | Guards.cs:197:28:197:28 | access to parameter s | true |
| Guards.cs:198:31:198:31 | access to parameter s | Guards.cs:197:14:197:29 | call to method NullTestWrong | Guards.cs:197:28:197:28 | access to parameter s | false |

View File

@@ -151,6 +151,7 @@ impliesStep
| Guards.cs:168:13:168:41 | !... | false | Guards.cs:168:14:168:41 | call to method IsNullOrWhiteSpace | true |
| Guards.cs:168:13:168:41 | !... | true | Guards.cs:168:14:168:41 | call to method IsNullOrWhiteSpace | false |
| Guards.cs:168:14:168:41 | call to method IsNullOrWhiteSpace | false | Guards.cs:168:13:168:41 | !... | true |
| Guards.cs:168:14:168:41 | call to method IsNullOrWhiteSpace | false | Guards.cs:168:40:168:40 | access to parameter x | non-null |
| Guards.cs:168:14:168:41 | call to method IsNullOrWhiteSpace | true | Guards.cs:168:13:168:41 | !... | false |
| Guards.cs:172:33:172:41 | ... == ... | false | Guards.cs:172:33:172:33 | access to parameter o | non-null |
| Guards.cs:172:33:172:41 | ... == ... | true | Guards.cs:172:33:172:33 | access to parameter o | null |
@@ -167,7 +168,9 @@ impliesStep
| Guards.cs:183:36:183:48 | !... | false | Guards.cs:183:37:183:48 | call to method NullTest3 | true |
| Guards.cs:183:36:183:48 | !... | true | Guards.cs:183:37:183:48 | call to method NullTest3 | false |
| Guards.cs:183:37:183:48 | call to method NullTest3 | false | Guards.cs:183:36:183:48 | !... | true |
| Guards.cs:183:37:183:48 | call to method NullTest3 | false | Guards.cs:183:47:183:47 | access to parameter o | non-null |
| Guards.cs:183:37:183:48 | call to method NullTest3 | true | Guards.cs:183:36:183:48 | !... | false |
| Guards.cs:183:37:183:48 | call to method NullTest3 | true | Guards.cs:183:47:183:47 | access to parameter o | null |
| Guards.cs:185:37:185:45 | ... == ... | false | Guards.cs:185:37:185:37 | access to parameter o | non-null |
| Guards.cs:185:37:185:45 | ... == ... | false | Guards.cs:185:37:185:59 | ... ? ... : ... | true |
| Guards.cs:185:37:185:45 | ... == ... | true | Guards.cs:185:37:185:37 | access to parameter o | null |
@@ -179,15 +182,23 @@ impliesStep
| Guards.cs:189:13:189:25 | !... | false | Guards.cs:189:14:189:25 | call to method NullTest1 | true |
| Guards.cs:189:13:189:25 | !... | true | Guards.cs:189:14:189:25 | call to method NullTest1 | false |
| Guards.cs:189:14:189:25 | call to method NullTest1 | false | Guards.cs:189:13:189:25 | !... | true |
| Guards.cs:189:14:189:25 | call to method NullTest1 | false | Guards.cs:189:24:189:24 | access to parameter s | non-null |
| Guards.cs:189:14:189:25 | call to method NullTest1 | true | Guards.cs:189:13:189:25 | !... | false |
| Guards.cs:189:14:189:25 | call to method NullTest1 | true | Guards.cs:189:24:189:24 | access to parameter s | null |
| Guards.cs:191:13:191:25 | !... | false | Guards.cs:191:14:191:25 | call to method NullTest2 | true |
| Guards.cs:191:13:191:25 | !... | true | Guards.cs:191:14:191:25 | call to method NullTest2 | false |
| Guards.cs:191:14:191:25 | call to method NullTest2 | false | Guards.cs:191:13:191:25 | !... | true |
| Guards.cs:191:14:191:25 | call to method NullTest2 | false | Guards.cs:191:24:191:24 | access to parameter s | non-null |
| Guards.cs:191:14:191:25 | call to method NullTest2 | true | Guards.cs:191:13:191:25 | !... | false |
| Guards.cs:191:14:191:25 | call to method NullTest2 | true | Guards.cs:191:24:191:24 | access to parameter s | null |
| Guards.cs:193:13:193:25 | !... | false | Guards.cs:193:14:193:25 | call to method NullTest3 | true |
| Guards.cs:193:13:193:25 | !... | true | Guards.cs:193:14:193:25 | call to method NullTest3 | false |
| Guards.cs:193:14:193:25 | call to method NullTest3 | false | Guards.cs:193:13:193:25 | !... | true |
| Guards.cs:193:14:193:25 | call to method NullTest3 | false | Guards.cs:193:24:193:24 | access to parameter s | non-null |
| Guards.cs:193:14:193:25 | call to method NullTest3 | true | Guards.cs:193:13:193:25 | !... | false |
| Guards.cs:193:14:193:25 | call to method NullTest3 | true | Guards.cs:193:24:193:24 | access to parameter s | null |
| Guards.cs:195:13:195:27 | call to method NotNullTest4 | false | Guards.cs:195:26:195:26 | access to parameter s | null |
| Guards.cs:195:13:195:27 | call to method NotNullTest4 | true | Guards.cs:195:26:195:26 | access to parameter s | non-null |
| Guards.cs:197:13:197:29 | !... | false | Guards.cs:197:14:197:29 | call to method NullTestWrong | true |
| Guards.cs:197:13:197:29 | !... | true | Guards.cs:197:14:197:29 | call to method NullTestWrong | false |
| Guards.cs:197:14:197:29 | call to method NullTestWrong | false | Guards.cs:197:13:197:29 | !... | true |

View File

@@ -34,3 +34,8 @@
| Guards.cs:154:24:154:24 | access to parameter o |
| Guards.cs:158:24:158:24 | access to parameter o |
| Guards.cs:162:24:162:24 | access to parameter o |
| Guards.cs:169:31:169:31 | access to parameter x |
| Guards.cs:190:31:190:31 | access to parameter s |
| Guards.cs:192:31:192:31 | access to parameter s |
| Guards.cs:194:31:194:31 | access to parameter s |
| Guards.cs:196:31:196:31 | access to parameter s |