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

Merge pull request #901 from hvitved/csharp/conditional-assign-join-order

Browse Source 
C#: Improve join order in `conditionalAssign()`
This commit is contained in:
Calum Grant
2019-02-12 10:39:49 +00:00
committed by GitHub
parent b557b7b438 23e63e983c
commit e10ea73a07
1 changed files with 49 additions and 10 deletions
Download Patch File Download Diff File Expand all files Collapse all files

59
csharp/ql/src/semmle/code/csharp/controlflow/Guards.qll
View File

@@ -896,6 +896,48 @@ module Internal {
)
}
pragma[noinline]
private predicate conditionalAssign0(
Guard guard, AbstractValue vGuard, PreSsa::Definition def, Expr e, PreSsa::Definition upd,
PreBasicBlocks::PreBasicBlock bbGuard
) {
e = upd.getDefinition().getSource() and
upd = def.getAPhiInput() and
guard.preControlsDirect(upd.getBasicBlock(), vGuard) and
bbGuard.getAnElement() = guard and
bbGuard.strictlyDominates(def.getBasicBlock()) and
not guard.preControlsDirect(def.getBasicBlock(), vGuard)
}
pragma[noinline]
private predicate conditionalAssign1(
Guard guard, AbstractValue vGuard, PreSsa::Definition def, Expr e, PreSsa::Definition upd,
PreBasicBlocks::PreBasicBlock bbGuard, PreSsa::Definition other
) {
conditionalAssign0(guard, vGuard, def, e, upd, bbGuard) and
other != upd and
other = def.getAPhiInput()
}
pragma[noinline]
private predicate conditionalAssign2(
Guard guard, AbstractValue vGuard, PreSsa::Definition def, Expr e, PreSsa::Definition upd,
PreBasicBlocks::PreBasicBlock bbGuard, PreSsa::Definition other
) {
conditionalAssign1(guard, vGuard, def, e, upd, bbGuard, other) and
guard.preControlsDirect(other.getBasicBlock(), vGuard.getDualValue())
}
pragma[noinline]
private predicate conditionalAssign3(
Guard guard, AbstractValue vGuard, PreSsa::Definition def, Expr e, PreSsa::Definition upd,
PreBasicBlocks::PreBasicBlock bbGuard, PreSsa::Definition other
) {
conditionalAssign1(guard, vGuard, def, e, upd, bbGuard, other) and
other.getBasicBlock().dominates(bbGuard) and
not PreSsa::ssaDefReachesEndOfBlock(guard.getConditionalSuccessor(vGuard), other, _)
}
/**
* Holds if the evaluation of `guard` to `vGuard` implies that `def` is assigned
* expression `e`.
@@ -917,28 +959,25 @@ module Internal {
)
or
exists(PreSsa::Definition upd, PreBasicBlocks::PreBasicBlock bbGuard |
e = upd.getDefinition().getSource() and
upd = def.getAPhiInput() and
guard.preControlsDirect(upd.getBasicBlock(), vGuard) and
bbGuard.getAnElement() = guard and
bbGuard.strictlyDominates(def.getBasicBlock()) and
not guard.preControlsDirect(def.getBasicBlock(), vGuard) and
forall(PreSsa::Definition other | other != upd and other = def.getAPhiInput() |
conditionalAssign0(guard, vGuard, def, e, upd, bbGuard)
|
forall(PreSsa::Definition other |
conditionalAssign1(guard, vGuard, def, e, upd, bbGuard, other)
|
// For example:
// if (guard)
// upd = a;
// else
// other = b;
// def = phi(upd, other)
guard.preControlsDirect(other.getBasicBlock(), vGuard.getDualValue())
conditionalAssign2(guard, vGuard, def, e, upd, bbGuard, other)
or
// For example:
// other = a;
// if (guard)
// upd = b;
// def = phi(other, upd)
other.getBasicBlock().dominates(bbGuard) and
not PreSsa::ssaDefReachesEndOfBlock(guard.getConditionalSuccessor(vGuard), other, _)
conditionalAssign3(guard, vGuard, def, e, upd, bbGuard, other)
)
)
}