mirror of
https://github.com/github/codeql.git
synced 2025-12-16 16:53:25 +01:00
Merge pull request #6513 from hvitved/csharp/cfg/shared
C#: Make CFG library shared
This commit is contained in:
Tom Hvitved
@@ -18,7 +18,7 @@ module Stages {
|
||||
|
||||
cached
|
||||
private predicate forceCachingInSameStageRev() {
|
||||
exists(SplitImpl si)
|
||||
exists(Split s)
|
||||
or
|
||||
exists(SuccessorType st)
|
||||
or
|
||||
|
||||
@@ -183,7 +183,7 @@ module ControlFlow {
|
||||
}
|
||||
|
||||
/** Gets a successor node of a given type, if any. */
|
||||
Node getASuccessorByType(SuccessorType t) { result = getASuccessorByType(this, t) }
|
||||
Node getASuccessorByType(SuccessorType t) { result = getASuccessor(this, t) }
|
||||
|
||||
/** Gets an immediate successor, if any. */
|
||||
Node getASuccessor() { result = getASuccessorByType(_) }
|
||||
@@ -255,9 +255,15 @@ module ControlFlow {
|
||||
|
||||
override Callable getEnclosingCallable() { result = this.getCallable() }
|
||||
|
||||
override Location getLocation() { result = getCallable().getLocation() }
|
||||
private Assignable getAssignable() { this = TEntryNode(result) }
|
||||
|
||||
override string toString() { result = "enter " + getCallable().toString() }
|
||||
override Location getLocation() {
|
||||
result in [this.getCallable().getLocation(), this.getAssignable().getLocation()]
|
||||
}
|
||||
|
||||
override string toString() {
|
||||
result = "enter " + [this.getCallable().toString(), this.getAssignable().toString()]
|
||||
}
|
||||
}
|
||||
|
||||
/** A node for a callable exit point, annotated with the type of exit. */
|
||||
@@ -314,7 +320,7 @@ module ControlFlow {
|
||||
* different splits for the element.
|
||||
*/
|
||||
class ElementNode extends Node, TElementNode {
|
||||
private Splitting::Splits splits;
|
||||
private Splits splits;
|
||||
private ControlFlowElement cfe;
|
||||
|
||||
ElementNode() { this = TElementNode(cfe, splits) }
|
||||
|
||||
@@ -43,13 +43,22 @@
|
||||
*/
|
||||
|
||||
import csharp
|
||||
private import semmle.code.csharp.controlflow.ControlFlowGraph::ControlFlow
|
||||
private import Completion
|
||||
private import SuccessorType
|
||||
private import SuccessorTypes
|
||||
private import Splitting
|
||||
private import semmle.code.csharp.ExprOrStmtParent
|
||||
private import semmle.code.csharp.commons.Compilation
|
||||
import ControlFlowGraphImplShared
|
||||
|
||||
/** An element that defines a new CFG scope. */
|
||||
class CfgScope extends Element, @top_level_exprorstmt_parent {
|
||||
CfgScope() {
|
||||
this instanceof Callable
|
||||
or
|
||||
// For now, static initializer values have their own scope. Eventually, they
|
||||
// should be treated like instance initializers.
|
||||
this.(Assignable).(Modifiable).isStatic()
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* A compilation.
|
||||
@@ -71,16 +80,11 @@ CompilationExt getCompilation(SourceFile f) {
|
||||
result = TBuildless()
|
||||
}
|
||||
|
||||
/** An element that defines a new CFG scope. */
|
||||
class CfgScope extends Element, @top_level_exprorstmt_parent {
|
||||
CfgScope() { not this instanceof Attribute }
|
||||
}
|
||||
|
||||
module ControlFlowTree {
|
||||
class Range_ = @callable or @control_flow_element;
|
||||
|
||||
class Range extends Element, Range_ {
|
||||
Range() { this = getAChild*(any(CfgScope scope)) }
|
||||
Range() { this = getAChild*(any(@top_level_exprorstmt_parent p | not p instanceof Attribute)) }
|
||||
}
|
||||
|
||||
Element getAChild(Element p) {
|
||||
@@ -93,61 +97,6 @@ module ControlFlowTree {
|
||||
predicate idOf(Range_ x, int y) = equivalenceRelation(id/2)(x, y)
|
||||
}
|
||||
|
||||
abstract private class ControlFlowTree extends ControlFlowTree::Range {
|
||||
/**
|
||||
* Holds if `first` is the first element executed within this control
|
||||
* flow element.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
abstract predicate first(ControlFlowElement first);
|
||||
|
||||
/**
|
||||
* Holds if `last` with completion `c` is a potential last element executed
|
||||
* within this control flow element.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
abstract predicate last(ControlFlowElement last, Completion c);
|
||||
|
||||
/** Holds if abnormal execution of `child` should propagate upwards. */
|
||||
abstract predicate propagatesAbnormal(ControlFlowElement child);
|
||||
|
||||
/**
|
||||
* Holds if `succ` is a control flow successor for `pred`, given that `pred`
|
||||
* finishes with completion `c`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
abstract predicate succ(ControlFlowElement pred, ControlFlowElement succ, Completion c);
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `first` is the first element executed within control flow
|
||||
* element `cft`.
|
||||
*/
|
||||
predicate first(ControlFlowTree cft, ControlFlowElement first) { cft.first(first) }
|
||||
|
||||
/**
|
||||
* Holds if `last` with completion `c` is a potential last element executed
|
||||
* within control flow element `cft`.
|
||||
*/
|
||||
predicate last(ControlFlowTree cft, ControlFlowElement last, Completion c) {
|
||||
cft.last(last, c)
|
||||
or
|
||||
exists(ControlFlowElement cfe |
|
||||
cft.propagatesAbnormal(cfe) and
|
||||
last(cfe, last, c) and
|
||||
not c instanceof NormalCompletion
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `succ` is a control flow successor for `pred`, given that `pred`
|
||||
* finishes with completion `c`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate succ(ControlFlowElement pred, ControlFlowElement succ, Completion c) {
|
||||
any(ControlFlowTree cft).succ(pred, succ, c)
|
||||
}
|
||||
|
||||
/** Holds if `first` is first executed when entering `scope`. */
|
||||
predicate scopeFirst(CfgScope scope, ControlFlowElement first) {
|
||||
scope =
|
||||
@@ -161,8 +110,7 @@ predicate scopeFirst(CfgScope scope, ControlFlowElement first) {
|
||||
)
|
||||
or
|
||||
expr_parent_top_level_adjusted(any(Expr e | first(e, first)), _, scope) and
|
||||
not scope instanceof Callable and
|
||||
not scope instanceof InitializerSplitting::InitializedInstanceMember
|
||||
not scope instanceof Callable
|
||||
}
|
||||
|
||||
/** Holds if `scope` is exited when `last` finishes with completion `c`. */
|
||||
@@ -204,53 +152,6 @@ private class ConstructorTree extends ControlFlowTree, Constructor {
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* A control flow element where the children are evaluated following a
|
||||
* standard left-to-right evaluation. The actual evaluation order is
|
||||
* determined by the predicate `getChildElement()`.
|
||||
*/
|
||||
abstract private class StandardElement extends ControlFlowTree {
|
||||
/** Gets the `i`th child element, in order of evaluation, starting from 0. */
|
||||
abstract ControlFlowElement getChildElement(int i);
|
||||
|
||||
/** Gets the first child element of this element. */
|
||||
final ControlFlowElement getFirstChild() { result = this.getChildElement(0) }
|
||||
|
||||
/** Holds if this element has no children. */
|
||||
final predicate isLeafElement() { not exists(this.getFirstChild()) }
|
||||
|
||||
/** Gets the last child element of this element. */
|
||||
final ControlFlowTree getLastChild() {
|
||||
exists(int last |
|
||||
result = this.getChildElement(last) and
|
||||
not exists(this.getChildElement(last + 1))
|
||||
)
|
||||
}
|
||||
|
||||
final override predicate propagatesAbnormal(ControlFlowElement child) {
|
||||
child = this.getChildElement(_)
|
||||
}
|
||||
|
||||
override predicate succ(ControlFlowElement pred, ControlFlowElement succ, Completion c) {
|
||||
exists(int i |
|
||||
last(this.getChildElement(i), pred, c) and
|
||||
first(this.getChildElement(i + 1), succ) and
|
||||
c instanceof NormalCompletion
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
abstract private class PreOrderTree extends ControlFlowTree {
|
||||
final override predicate first(ControlFlowElement first) { first = this }
|
||||
}
|
||||
|
||||
abstract private class PostOrderTree extends ControlFlowTree {
|
||||
override predicate last(ControlFlowElement last, Completion c) {
|
||||
last = this and
|
||||
c.isValidFor(last)
|
||||
}
|
||||
}
|
||||
|
||||
abstract private class SwitchTree extends ControlFlowTree, Switch {
|
||||
override predicate propagatesAbnormal(ControlFlowElement child) { child = this.getExpr() }
|
||||
|
||||
@@ -368,7 +269,7 @@ module Expressions {
|
||||
)
|
||||
}
|
||||
|
||||
private class StandardExpr extends StandardElement, PostOrderTree, Expr {
|
||||
private class StandardExpr extends StandardPostOrderTree, Expr {
|
||||
StandardExpr() {
|
||||
// The following expressions need special treatment
|
||||
not this instanceof LogicalNotExpr and
|
||||
@@ -396,21 +297,6 @@ module Expressions {
|
||||
}
|
||||
|
||||
final override ControlFlowElement getChildElement(int i) { result = getExprChild(this, i) }
|
||||
|
||||
final override predicate first(ControlFlowElement first) {
|
||||
first(this.getFirstChild(), first)
|
||||
or
|
||||
not exists(this.getFirstChild()) and
|
||||
first = this
|
||||
}
|
||||
|
||||
final override predicate succ(ControlFlowElement pred, ControlFlowElement succ, Completion c) {
|
||||
StandardElement.super.succ(pred, succ, c)
|
||||
or
|
||||
last(this.getLastChild(), pred, c) and
|
||||
succ = this and
|
||||
c instanceof NormalCompletion
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1095,7 +981,7 @@ private class PropertyPatternExprExprTree extends PostOrderTree, PropertyPattern
|
||||
}
|
||||
|
||||
module Statements {
|
||||
private class StandardStmt extends StandardElement, PreOrderTree, Stmt {
|
||||
private class StandardStmt extends StandardPreOrderTree, Stmt {
|
||||
StandardStmt() {
|
||||
// The following statements need special treatment
|
||||
not this instanceof IfStmt and
|
||||
@@ -1140,22 +1026,6 @@ module Statements {
|
||||
result =
|
||||
rank[i + 1](ControlFlowElement cfe, int j | cfe = this.getChildElement0(j) | cfe order by j)
|
||||
}
|
||||
|
||||
final override predicate last(ControlFlowElement last, Completion c) {
|
||||
last(this.getLastChild(), last, c)
|
||||
or
|
||||
this.isLeafElement() and
|
||||
last = this and
|
||||
c.isValidFor(this)
|
||||
}
|
||||
|
||||
final override predicate succ(ControlFlowElement pred, ControlFlowElement succ, Completion c) {
|
||||
StandardElement.super.succ(pred, succ, c)
|
||||
or
|
||||
pred = this and
|
||||
first(this.getFirstChild(), succ) and
|
||||
c instanceof SimpleCompletion
|
||||
}
|
||||
}
|
||||
|
||||
private class IfStmtTree extends PreOrderTree, IfStmt {
|
||||
@@ -1779,88 +1649,6 @@ module Statements {
|
||||
}
|
||||
}
|
||||
|
||||
cached
|
||||
private module Cached {
|
||||
private import semmle.code.csharp.Caching
|
||||
|
||||
private predicate isAbnormalExitType(SuccessorType t) {
|
||||
t instanceof ExceptionSuccessor or t instanceof ExitSuccessor
|
||||
}
|
||||
|
||||
/**
|
||||
* Internal representation of control flow nodes in the control flow graph.
|
||||
* The control flow graph is pruned for unreachable nodes.
|
||||
*/
|
||||
cached
|
||||
newtype TNode =
|
||||
TEntryNode(Callable c) {
|
||||
Stages::ControlFlowStage::forceCachingInSameStage() and
|
||||
succEntrySplits(c, _, _, _)
|
||||
} or
|
||||
TAnnotatedExitNode(Callable c, boolean normal) {
|
||||
exists(Reachability::SameSplitsBlock b, SuccessorType t | b.isReachable(_) |
|
||||
succExitSplits(b.getAnElement(), _, c, t) and
|
||||
if isAbnormalExitType(t) then normal = false else normal = true
|
||||
)
|
||||
} or
|
||||
TExitNode(Callable c) {
|
||||
exists(Reachability::SameSplitsBlock b | b.isReachable(_) |
|
||||
succExitSplits(b.getAnElement(), _, c, _)
|
||||
)
|
||||
} or
|
||||
TElementNode(ControlFlowElement cfe, Splits splits) {
|
||||
exists(Reachability::SameSplitsBlock b | b.isReachable(splits) | cfe = b.getAnElement())
|
||||
}
|
||||
|
||||
/** Gets a successor node of a given flow type, if any. */
|
||||
cached
|
||||
Node getASuccessorByType(Node pred, SuccessorType t) {
|
||||
// Callable entry node -> callable body
|
||||
exists(ControlFlowElement succElement, Splits succSplits |
|
||||
result = TElementNode(succElement, succSplits)
|
||||
|
|
||||
succEntrySplits(pred.(Nodes::EntryNode).getCallable(), succElement, succSplits, t)
|
||||
)
|
||||
or
|
||||
exists(ControlFlowElement predElement, Splits predSplits |
|
||||
pred = TElementNode(predElement, predSplits)
|
||||
|
|
||||
// Element node -> callable exit (annotated)
|
||||
result =
|
||||
any(Nodes::AnnotatedExitNode exit |
|
||||
succExitSplits(predElement, predSplits, exit.getCallable(), t) and
|
||||
if isAbnormalExitType(t) then not exit.isNormal() else exit.isNormal()
|
||||
)
|
||||
or
|
||||
// Element node -> element node
|
||||
exists(ControlFlowElement succElement, Splits succSplits, Completion c |
|
||||
result = TElementNode(succElement, succSplits)
|
||||
|
|
||||
succSplits(predElement, predSplits, succElement, succSplits, c) and
|
||||
t = c.getAMatchingSuccessorType()
|
||||
)
|
||||
)
|
||||
or
|
||||
// Callable exit (annotated) -> callable exit
|
||||
pred.(Nodes::AnnotatedExitNode).getCallable() = result.(Nodes::ExitNode).getCallable() and
|
||||
t instanceof SuccessorTypes::NormalSuccessor
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets a first control flow element executed within `cfe`.
|
||||
*/
|
||||
cached
|
||||
ControlFlowElement getAControlFlowEntryNode(ControlFlowElement cfe) { first(cfe, result) }
|
||||
|
||||
/**
|
||||
* Gets a potential last control flow element executed within `cfe`.
|
||||
*/
|
||||
cached
|
||||
ControlFlowElement getAControlFlowExitNode(ControlFlowElement cfe) { last(cfe, result, _) }
|
||||
}
|
||||
|
||||
import Cached
|
||||
|
||||
/** A control flow element that is split into multiple control flow nodes. */
|
||||
class SplitControlFlowElement extends ControlFlowElement {
|
||||
SplitControlFlowElement() { strictcount(this.getAControlFlowNode()) > 1 }
|
||||
|
||||
@@ -0,0 +1,945 @@
|
||||
/** Provides language-independent definitions for AST-to-CFG construction. */
|
||||
|
||||
private import ControlFlowGraphImplSpecific
|
||||
|
||||
/** An element with associated control flow. */
|
||||
abstract class ControlFlowTree extends ControlFlowTreeBase {
|
||||
/** Holds if `first` is the first element executed within this element. */
|
||||
pragma[nomagic]
|
||||
abstract predicate first(ControlFlowElement first);
|
||||
|
||||
/**
|
||||
* Holds if `last` with completion `c` is a potential last element executed
|
||||
* within this element.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
abstract predicate last(ControlFlowElement last, Completion c);
|
||||
|
||||
/** Holds if abnormal execution of `child` should propagate upwards. */
|
||||
abstract predicate propagatesAbnormal(ControlFlowElement child);
|
||||
|
||||
/**
|
||||
* Holds if `succ` is a control flow successor for `pred`, given that `pred`
|
||||
* finishes with completion `c`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
abstract predicate succ(ControlFlowElement pred, ControlFlowElement succ, Completion c);
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `first` is the first element executed within control flow
|
||||
* element `cft`.
|
||||
*/
|
||||
predicate first(ControlFlowTree cft, ControlFlowElement first) { cft.first(first) }
|
||||
|
||||
/**
|
||||
* Holds if `last` with completion `c` is a potential last element executed
|
||||
* within control flow element `cft`.
|
||||
*/
|
||||
predicate last(ControlFlowTree cft, ControlFlowElement last, Completion c) {
|
||||
cft.last(last, c)
|
||||
or
|
||||
exists(ControlFlowElement cfe |
|
||||
cft.propagatesAbnormal(cfe) and
|
||||
last(cfe, last, c) and
|
||||
not completionIsNormal(c)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `succ` is a control flow successor for `pred`, given that `pred`
|
||||
* finishes with completion `c`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate succ(ControlFlowElement pred, ControlFlowElement succ, Completion c) {
|
||||
any(ControlFlowTree cft).succ(pred, succ, c)
|
||||
}
|
||||
|
||||
/** An element that is executed in pre-order. */
|
||||
abstract class PreOrderTree extends ControlFlowTree {
|
||||
final override predicate first(ControlFlowElement first) { first = this }
|
||||
}
|
||||
|
||||
/** An element that is executed in post-order. */
|
||||
abstract class PostOrderTree extends ControlFlowTree {
|
||||
override predicate last(ControlFlowElement last, Completion c) {
|
||||
last = this and
|
||||
completionIsValidFor(c, last)
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* An element where the children are evaluated following a standard left-to-right
|
||||
* evaluation. The actual evaluation order is determined by the predicate
|
||||
* `getChildElement()`.
|
||||
*/
|
||||
abstract class StandardTree extends ControlFlowTree {
|
||||
/** Gets the `i`th child element, in order of evaluation. */
|
||||
abstract ControlFlowElement getChildElement(int i);
|
||||
|
||||
private ControlFlowElement getChildElementRanked(int i) {
|
||||
result =
|
||||
rank[i + 1](ControlFlowElement child, int j |
|
||||
child = this.getChildElement(j)
|
||||
|
|
||||
child order by j
|
||||
)
|
||||
}
|
||||
|
||||
/** Gets the first child node of this element. */
|
||||
final ControlFlowElement getFirstChildElement() { result = this.getChildElementRanked(0) }
|
||||
|
||||
/** Gets the last child node of this node. */
|
||||
final ControlFlowElement getLastChildElement() {
|
||||
exists(int last |
|
||||
result = this.getChildElementRanked(last) and
|
||||
not exists(this.getChildElementRanked(last + 1))
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if this element has no children. */
|
||||
predicate isLeafElement() { not exists(this.getFirstChildElement()) }
|
||||
|
||||
override predicate propagatesAbnormal(ControlFlowElement child) {
|
||||
child = this.getChildElement(_)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
override predicate succ(ControlFlowElement pred, ControlFlowElement succ, Completion c) {
|
||||
exists(int i |
|
||||
last(this.getChildElementRanked(i), pred, c) and
|
||||
completionIsNormal(c) and
|
||||
first(this.getChildElementRanked(i + 1), succ)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
/** A standard element that is executed in pre-order. */
|
||||
abstract class StandardPreOrderTree extends StandardTree, PreOrderTree {
|
||||
override predicate last(ControlFlowElement last, Completion c) {
|
||||
last(this.getLastChildElement(), last, c)
|
||||
or
|
||||
this.isLeafElement() and
|
||||
completionIsValidFor(c, this) and
|
||||
last = this
|
||||
}
|
||||
|
||||
override predicate succ(ControlFlowElement pred, ControlFlowElement succ, Completion c) {
|
||||
StandardTree.super.succ(pred, succ, c)
|
||||
or
|
||||
pred = this and
|
||||
first(this.getFirstChildElement(), succ) and
|
||||
completionIsSimple(c)
|
||||
}
|
||||
}
|
||||
|
||||
/** A standard element that is executed in post-order. */
|
||||
abstract class StandardPostOrderTree extends StandardTree, PostOrderTree {
|
||||
override predicate first(ControlFlowElement first) {
|
||||
first(this.getFirstChildElement(), first)
|
||||
or
|
||||
not exists(this.getFirstChildElement()) and
|
||||
first = this
|
||||
}
|
||||
|
||||
override predicate succ(ControlFlowElement pred, ControlFlowElement succ, Completion c) {
|
||||
StandardTree.super.succ(pred, succ, c)
|
||||
or
|
||||
last(this.getLastChildElement(), pred, c) and
|
||||
succ = this and
|
||||
completionIsNormal(c)
|
||||
}
|
||||
}
|
||||
|
||||
/** An element that is a leaf in the control flow graph. */
|
||||
abstract class LeafTree extends PreOrderTree, PostOrderTree {
|
||||
override predicate propagatesAbnormal(ControlFlowElement child) { none() }
|
||||
|
||||
override predicate succ(ControlFlowElement pred, ControlFlowElement succ, Completion c) { none() }
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if split kinds `sk1` and `sk2` may overlap. That is, they may apply
|
||||
* to at least one common AST node inside `scope`.
|
||||
*/
|
||||
private predicate overlapping(CfgScope scope, SplitKind sk1, SplitKind sk2) {
|
||||
exists(ControlFlowElement e |
|
||||
sk1.appliesTo(e) and
|
||||
sk2.appliesTo(e) and
|
||||
scope = getCfgScope(e)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* A split kind. Each control flow node can have at most one split of a
|
||||
* given kind.
|
||||
*/
|
||||
abstract class SplitKind extends SplitKindBase {
|
||||
/** Gets a split of this kind. */
|
||||
SplitImpl getASplit() { result.getKind() = this }
|
||||
|
||||
/** Holds if some split of this kind applies to AST node `n`. */
|
||||
predicate appliesTo(ControlFlowElement n) { this.getASplit().appliesTo(n) }
|
||||
|
||||
/**
|
||||
* Gets a unique integer representing this split kind. The integer is used
|
||||
* to represent sets of splits as ordered lists.
|
||||
*/
|
||||
abstract int getListOrder();
|
||||
|
||||
/** Gets the rank of this split kind among all overlapping kinds for `c`. */
|
||||
private int getRank(CfgScope scope) {
|
||||
this = rank[result](SplitKind sk | overlapping(scope, this, sk) | sk order by sk.getListOrder())
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if this split kind is enabled for AST node `n`. For performance reasons,
|
||||
* the number of splits is restricted by the `maxSplits()` predicate.
|
||||
*/
|
||||
predicate isEnabled(ControlFlowElement n) {
|
||||
this.appliesTo(n) and
|
||||
this.getRank(getCfgScope(n)) <= maxSplits()
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the rank of this split kind among all the split kinds that apply to
|
||||
* AST node `n`. The rank is based on the order defined by `getListOrder()`.
|
||||
*/
|
||||
int getListRank(ControlFlowElement n) {
|
||||
this.isEnabled(n) and
|
||||
this = rank[result](SplitKind sk | sk.appliesTo(n) | sk order by sk.getListOrder())
|
||||
}
|
||||
|
||||
/** Gets a textual representation of this split kind. */
|
||||
abstract string toString();
|
||||
}
|
||||
|
||||
/** Provides the interface for implementing an entity to split on. */
|
||||
abstract class SplitImpl extends Split {
|
||||
/** Gets the kind of this split. */
|
||||
abstract SplitKind getKind();
|
||||
|
||||
/**
|
||||
* Holds if this split is entered when control passes from `pred` to `succ` with
|
||||
* completion `c`.
|
||||
*
|
||||
* Invariant: `hasEntry(pred, succ, c) implies succ(pred, succ, c)`.
|
||||
*/
|
||||
abstract predicate hasEntry(ControlFlowElement pred, ControlFlowElement succ, Completion c);
|
||||
|
||||
/**
|
||||
* Holds if this split is entered when control passes from `scope` to the entry point
|
||||
* `first`.
|
||||
*
|
||||
* Invariant: `hasEntryScope(scope, first) implies scopeFirst(scope, first)`.
|
||||
*/
|
||||
abstract predicate hasEntryScope(CfgScope scope, ControlFlowElement first);
|
||||
|
||||
/**
|
||||
* Holds if this split is left when control passes from `pred` to `succ` with
|
||||
* completion `c`.
|
||||
*
|
||||
* Invariant: `hasExit(pred, succ, c) implies succ(pred, succ, c)`.
|
||||
*/
|
||||
abstract predicate hasExit(ControlFlowElement pred, ControlFlowElement succ, Completion c);
|
||||
|
||||
/**
|
||||
* Holds if this split is left when control passes from `last` out of the enclosing
|
||||
* scope `scope` with completion `c`.
|
||||
*
|
||||
* Invariant: `hasExitScope(scope, last, c) implies scopeLast(scope, last, c)`
|
||||
*/
|
||||
abstract predicate hasExitScope(CfgScope scope, ControlFlowElement last, Completion c);
|
||||
|
||||
/**
|
||||
* Holds if this split is maintained when control passes from `pred` to `succ` with
|
||||
* completion `c`.
|
||||
*
|
||||
* Invariant: `hasSuccessor(pred, succ, c) implies succ(pred, succ, c)`
|
||||
*/
|
||||
abstract predicate hasSuccessor(ControlFlowElement pred, ControlFlowElement succ, Completion c);
|
||||
|
||||
/** Holds if this split applies to control flow element `cfe`. */
|
||||
final predicate appliesTo(ControlFlowElement cfe) {
|
||||
this.hasEntry(_, cfe, _)
|
||||
or
|
||||
this.hasEntryScope(_, cfe)
|
||||
or
|
||||
exists(ControlFlowElement pred | this.appliesTo(pred) | this.hasSuccessor(pred, cfe, _))
|
||||
}
|
||||
|
||||
/** The `succ` relation restricted to predecessors `pred` that this split applies to. */
|
||||
pragma[noinline]
|
||||
final predicate appliesSucc(ControlFlowElement pred, ControlFlowElement succ, Completion c) {
|
||||
this.appliesTo(pred) and
|
||||
succ(pred, succ, c)
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* A set of control flow node splits. The set is represented by a list of splits,
|
||||
* ordered by ascending rank.
|
||||
*/
|
||||
class Splits extends TSplits {
|
||||
/** Gets a textual representation of this set of splits. */
|
||||
string toString() { result = splitsToString(this) }
|
||||
|
||||
/** Gets a split belonging to this set of splits. */
|
||||
SplitImpl getASplit() {
|
||||
exists(SplitImpl head, Splits tail | this = TSplitsCons(head, tail) |
|
||||
result = head
|
||||
or
|
||||
result = tail.getASplit()
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
private predicate succEntrySplitsFromRank(
|
||||
CfgScope pred, ControlFlowElement succ, Splits splits, int rnk
|
||||
) {
|
||||
splits = TSplitsNil() and
|
||||
scopeFirst(pred, succ) and
|
||||
rnk = 0
|
||||
or
|
||||
exists(SplitImpl head, Splits tail | succEntrySplitsCons(pred, succ, head, tail, rnk) |
|
||||
splits = TSplitsCons(head, tail)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate succEntrySplitsCons(
|
||||
CfgScope pred, ControlFlowElement succ, SplitImpl head, Splits tail, int rnk
|
||||
) {
|
||||
succEntrySplitsFromRank(pred, succ, tail, rnk - 1) and
|
||||
head.hasEntryScope(pred, succ) and
|
||||
rnk = head.getKind().getListRank(succ)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `succ` with splits `succSplits` is the first element that is executed
|
||||
* when entering callable `pred`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate succEntrySplits(
|
||||
CfgScope pred, ControlFlowElement succ, Splits succSplits, SuccessorType t
|
||||
) {
|
||||
exists(int rnk |
|
||||
scopeFirst(pred, succ) and
|
||||
successorTypeIsSimple(t) and
|
||||
succEntrySplitsFromRank(pred, succ, succSplits, rnk)
|
||||
|
|
||||
rnk = 0 and
|
||||
not any(SplitImpl split).hasEntryScope(pred, succ)
|
||||
or
|
||||
rnk = max(SplitImpl split | split.hasEntryScope(pred, succ) | split.getKind().getListRank(succ))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `pred` with splits `predSplits` can exit the enclosing callable
|
||||
* `succ` with type `t`.
|
||||
*/
|
||||
private predicate succExitSplits(
|
||||
ControlFlowElement pred, Splits predSplits, CfgScope succ, SuccessorType t
|
||||
) {
|
||||
exists(Reachability::SameSplitsBlock b, Completion c | pred = b.getAnElement() |
|
||||
b.isReachable(predSplits) and
|
||||
t = getAMatchingSuccessorType(c) and
|
||||
scopeLast(succ, pred, c) and
|
||||
forall(SplitImpl predSplit | predSplit = predSplits.getASplit() |
|
||||
predSplit.hasExitScope(succ, pred, c)
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Provides a predicate for the successor relation with split information,
|
||||
* as well as logic used to construct the type `TSplits` representing sets
|
||||
* of splits. Only sets of splits that can be reached are constructed, hence
|
||||
* the predicates are mutually recursive.
|
||||
*
|
||||
* For the successor relation
|
||||
*
|
||||
* ```ql
|
||||
* succSplits(ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Splits succSplits, Completion c)
|
||||
* ```
|
||||
*
|
||||
* the following invariants are maintained:
|
||||
*
|
||||
* 1. `pred` is reachable with split set `predSplits`.
|
||||
* 2. For all `split` in `predSplits`:
|
||||
* - If `split.hasSuccessor(pred, succ, c)` then `split` in `succSplits`.
|
||||
* 3. For all `split` in `predSplits`:
|
||||
* - If `split.hasExit(pred, succ, c)` and not `split.hasEntry(pred, succ, c)` then
|
||||
* `split` not in `succSplits`.
|
||||
* 4. For all `split` with kind not in `predSplits`:
|
||||
* - If `split.hasEntry(pred, succ, c)` then `split` in `succSplits`.
|
||||
* 5. For all `split` in `succSplits`:
|
||||
* - `split.hasSuccessor(pred, succ, c)` and `split` in `predSplits`, or
|
||||
* - `split.hasEntry(pred, succ, c)`.
|
||||
*
|
||||
* The algorithm divides into four cases:
|
||||
*
|
||||
* 1. The set of splits for the successor is the same as the set of splits
|
||||
* for the predecessor:
|
||||
* a) The successor is in the same `SameSplitsBlock` as the predecessor.
|
||||
* b) The successor is *not* in the same `SameSplitsBlock` as the predecessor.
|
||||
* 2. The set of splits for the successor is different from the set of splits
|
||||
* for the predecessor:
|
||||
* a) The set of splits for the successor is *maybe* non-empty.
|
||||
* b) The set of splits for the successor is *always* empty.
|
||||
*
|
||||
* Only case 2a may introduce new sets of splits, so only predicates from
|
||||
* this case are used in the definition of `TSplits`.
|
||||
*
|
||||
* The predicates in this module are named after the cases above.
|
||||
*/
|
||||
private module SuccSplits {
|
||||
private predicate succInvariant1(
|
||||
Reachability::SameSplitsBlock b, ControlFlowElement pred, Splits predSplits,
|
||||
ControlFlowElement succ, Completion c
|
||||
) {
|
||||
pred = b.getAnElement() and
|
||||
b.isReachable(predSplits) and
|
||||
succ(pred, succ, c)
|
||||
}
|
||||
|
||||
private predicate case1b0(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c
|
||||
) {
|
||||
exists(Reachability::SameSplitsBlock b |
|
||||
// Invariant 1
|
||||
succInvariant1(b, pred, predSplits, succ, c)
|
||||
|
|
||||
(succ = b.getAnElement() implies succ = b) and
|
||||
// Invariant 4
|
||||
not exists(SplitImpl split | split.hasEntry(pred, succ, c))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Case 1b.
|
||||
*
|
||||
* Invariants 1 and 4 hold in the base case, and invariants 2, 3, and 5 are
|
||||
* maintained for all splits in `predSplits` (= `succSplits`), except
|
||||
* possibly for the splits in `except`.
|
||||
*
|
||||
* The predicate is written using explicit recursion, as opposed to a `forall`,
|
||||
* to avoid negative recursion.
|
||||
*/
|
||||
private predicate case1bForall(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c, Splits except
|
||||
) {
|
||||
case1b0(pred, predSplits, succ, c) and
|
||||
except = predSplits
|
||||
or
|
||||
exists(SplitImpl split |
|
||||
case1bForallCons(pred, predSplits, succ, c, split, except) and
|
||||
split.hasSuccessor(pred, succ, c)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate case1bForallCons(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c,
|
||||
SplitImpl exceptHead, Splits exceptTail
|
||||
) {
|
||||
case1bForall(pred, predSplits, succ, c, TSplitsCons(exceptHead, exceptTail))
|
||||
}
|
||||
|
||||
private predicate case1(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c
|
||||
) {
|
||||
// Case 1a
|
||||
exists(Reachability::SameSplitsBlock b | succInvariant1(b, pred, predSplits, succ, c) |
|
||||
succ = b.getAnElement() and
|
||||
not succ = b
|
||||
)
|
||||
or
|
||||
// Case 1b
|
||||
case1bForall(pred, predSplits, succ, c, TSplitsNil())
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private SplitImpl succInvariant1GetASplit(
|
||||
Reachability::SameSplitsBlock b, ControlFlowElement pred, Splits predSplits,
|
||||
ControlFlowElement succ, Completion c
|
||||
) {
|
||||
succInvariant1(b, pred, predSplits, succ, c) and
|
||||
result = predSplits.getASplit()
|
||||
}
|
||||
|
||||
private predicate case2aux(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c
|
||||
) {
|
||||
exists(Reachability::SameSplitsBlock b |
|
||||
succInvariant1(b, pred, predSplits, succ, c) and
|
||||
(succ = b.getAnElement() implies succ = b)
|
||||
|
|
||||
succInvariant1GetASplit(b, pred, predSplits, succ, c).hasExit(pred, succ, c)
|
||||
or
|
||||
any(SplitImpl split).hasEntry(pred, succ, c)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `succSplits` should not inherit a split of kind `sk` from
|
||||
* `predSplits`, except possibly because of a split in `except`.
|
||||
*
|
||||
* The predicate is written using explicit recursion, as opposed to a `forall`,
|
||||
* to avoid negative recursion.
|
||||
*/
|
||||
private predicate case2aNoneInheritedOfKindForall(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c, SplitKind sk,
|
||||
Splits except
|
||||
) {
|
||||
case2aux(pred, predSplits, succ, c) and
|
||||
sk.appliesTo(succ) and
|
||||
except = predSplits
|
||||
or
|
||||
exists(Splits mid, SplitImpl split |
|
||||
case2aNoneInheritedOfKindForall(pred, predSplits, succ, c, sk, mid) and
|
||||
mid = TSplitsCons(split, except)
|
||||
|
|
||||
split.getKind() = any(SplitKind sk0 | sk0 != sk and sk0.appliesTo(succ))
|
||||
or
|
||||
split.hasExit(pred, succ, c)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate entryOfKind(
|
||||
ControlFlowElement pred, ControlFlowElement succ, Completion c, SplitImpl split, SplitKind sk
|
||||
) {
|
||||
split.hasEntry(pred, succ, c) and
|
||||
sk = split.getKind()
|
||||
}
|
||||
|
||||
/** Holds if `succSplits` should not have a split of kind `sk`. */
|
||||
pragma[nomagic]
|
||||
private predicate case2aNoneOfKind(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c, SplitKind sk
|
||||
) {
|
||||
// None inherited from predecessor
|
||||
case2aNoneInheritedOfKindForall(pred, predSplits, succ, c, sk, TSplitsNil()) and
|
||||
// None newly entered into
|
||||
not entryOfKind(pred, succ, c, _, sk)
|
||||
}
|
||||
|
||||
/** Holds if `succSplits` should not have a split of kind `sk` at rank `rnk`. */
|
||||
pragma[nomagic]
|
||||
private predicate case2aNoneAtRank(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c, int rnk
|
||||
) {
|
||||
exists(SplitKind sk | case2aNoneOfKind(pred, predSplits, succ, c, sk) |
|
||||
rnk = sk.getListRank(succ)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private SplitImpl case2auxGetAPredecessorSplit(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c
|
||||
) {
|
||||
case2aux(pred, predSplits, succ, c) and
|
||||
result = predSplits.getASplit()
|
||||
}
|
||||
|
||||
/** Gets a split that should be in `succSplits`. */
|
||||
pragma[nomagic]
|
||||
private SplitImpl case2aSome(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c, SplitKind sk
|
||||
) {
|
||||
(
|
||||
// Inherited from predecessor
|
||||
result = case2auxGetAPredecessorSplit(pred, predSplits, succ, c) and
|
||||
result.hasSuccessor(pred, succ, c)
|
||||
or
|
||||
// Newly entered into
|
||||
exists(SplitKind sk0 |
|
||||
case2aNoneInheritedOfKindForall(pred, predSplits, succ, c, sk0, TSplitsNil())
|
||||
|
|
||||
entryOfKind(pred, succ, c, result, sk0)
|
||||
)
|
||||
) and
|
||||
sk = result.getKind()
|
||||
}
|
||||
|
||||
/** Gets a split that should be in `succSplits` at rank `rnk`. */
|
||||
pragma[nomagic]
|
||||
SplitImpl case2aSomeAtRank(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c, int rnk
|
||||
) {
|
||||
exists(SplitKind sk | result = case2aSome(pred, predSplits, succ, c, sk) |
|
||||
rnk = sk.getListRank(succ)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Case 2a.
|
||||
*
|
||||
* As opposed to the other cases, in this case we need to construct a new set
|
||||
* of splits `succSplits`. Since this involves constructing the very IPA type,
|
||||
* we cannot recurse directly over the structure of `succSplits`. Instead, we
|
||||
* recurse over the ranks of all splits that *might* be in `succSplits`.
|
||||
*
|
||||
* - Invariant 1 holds in the base case,
|
||||
* - invariant 2 holds for all splits with rank at least `rnk`,
|
||||
* - invariant 3 holds for all splits in `predSplits`,
|
||||
* - invariant 4 holds for all splits in `succSplits` with rank at least `rnk`,
|
||||
* and
|
||||
* - invariant 4 holds for all splits in `succSplits` with rank at least `rnk`.
|
||||
*/
|
||||
predicate case2aFromRank(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Splits succSplits,
|
||||
Completion c, int rnk
|
||||
) {
|
||||
case2aux(pred, predSplits, succ, c) and
|
||||
succSplits = TSplitsNil() and
|
||||
rnk = max(any(SplitKind sk).getListRank(succ)) + 1
|
||||
or
|
||||
case2aFromRank(pred, predSplits, succ, succSplits, c, rnk + 1) and
|
||||
case2aNoneAtRank(pred, predSplits, succ, c, rnk)
|
||||
or
|
||||
exists(Splits mid, SplitImpl split | split = case2aCons(pred, predSplits, succ, mid, c, rnk) |
|
||||
succSplits = TSplitsCons(split, mid)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private SplitImpl case2aCons(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Splits succSplits,
|
||||
Completion c, int rnk
|
||||
) {
|
||||
case2aFromRank(pred, predSplits, succ, succSplits, c, rnk + 1) and
|
||||
result = case2aSomeAtRank(pred, predSplits, succ, c, rnk)
|
||||
}
|
||||
|
||||
/**
|
||||
* Case 2b.
|
||||
*
|
||||
* Invariants 1, 4, and 5 hold in the base case, and invariants 2 and 3 are
|
||||
* maintained for all splits in `predSplits`, except possibly for the splits
|
||||
* in `except`.
|
||||
*
|
||||
* The predicate is written using explicit recursion, as opposed to a `forall`,
|
||||
* to avoid negative recursion.
|
||||
*/
|
||||
private predicate case2bForall(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c, Splits except
|
||||
) {
|
||||
// Invariant 1
|
||||
case2aux(pred, predSplits, succ, c) and
|
||||
// Invariants 4 and 5
|
||||
not any(SplitKind sk).appliesTo(succ) and
|
||||
except = predSplits
|
||||
or
|
||||
exists(SplitImpl split | case2bForallCons(pred, predSplits, succ, c, split, except) |
|
||||
// Invariants 2 and 3
|
||||
split.hasExit(pred, succ, c)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate case2bForallCons(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c,
|
||||
SplitImpl exceptHead, Splits exceptTail
|
||||
) {
|
||||
case2bForall(pred, predSplits, succ, c, TSplitsCons(exceptHead, exceptTail))
|
||||
}
|
||||
|
||||
private predicate case2(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Splits succSplits,
|
||||
Completion c
|
||||
) {
|
||||
case2aFromRank(pred, predSplits, succ, succSplits, c, 1)
|
||||
or
|
||||
case2bForall(pred, predSplits, succ, c, TSplitsNil()) and
|
||||
succSplits = TSplitsNil()
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `succ` with splits `succSplits` is a successor of type `t` for `pred`
|
||||
* with splits `predSplits`.
|
||||
*/
|
||||
predicate succSplits(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Splits succSplits,
|
||||
Completion c
|
||||
) {
|
||||
case1(pred, predSplits, succ, c) and
|
||||
succSplits = predSplits
|
||||
or
|
||||
case2(pred, predSplits, succ, succSplits, c)
|
||||
}
|
||||
}
|
||||
|
||||
import SuccSplits
|
||||
|
||||
/** Provides logic for calculating reachable control flow nodes. */
|
||||
private module Reachability {
|
||||
/**
|
||||
* Holds if `cfe` is a control flow element where the set of possible splits may
|
||||
* be different from the set of possible splits for one of `cfe`'s predecessors.
|
||||
* That is, `cfe` starts a new block of elements with the same set of splits.
|
||||
*/
|
||||
private predicate startsSplits(ControlFlowElement cfe) {
|
||||
scopeFirst(_, cfe)
|
||||
or
|
||||
exists(SplitImpl s |
|
||||
s.hasEntry(_, cfe, _)
|
||||
or
|
||||
s.hasExit(_, cfe, _)
|
||||
)
|
||||
or
|
||||
exists(ControlFlowElement pred, SplitImpl split, Completion c | succ(pred, cfe, c) |
|
||||
split.appliesTo(pred) and
|
||||
not split.hasSuccessor(pred, cfe, c)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate intraSplitsSucc(ControlFlowElement pred, ControlFlowElement succ) {
|
||||
succ(pred, succ, _) and
|
||||
not startsSplits(succ)
|
||||
}
|
||||
|
||||
private predicate splitsBlockContains(ControlFlowElement start, ControlFlowElement cfe) =
|
||||
fastTC(intraSplitsSucc/2)(start, cfe)
|
||||
|
||||
/**
|
||||
* A block of control flow elements where the set of splits is guaranteed
|
||||
* to remain unchanged, represented by the first element in the block.
|
||||
*/
|
||||
class SameSplitsBlock extends ControlFlowElement {
|
||||
SameSplitsBlock() { startsSplits(this) }
|
||||
|
||||
/** Gets a control flow element in this block. */
|
||||
ControlFlowElement getAnElement() {
|
||||
splitsBlockContains(this, result)
|
||||
or
|
||||
result = this
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private SameSplitsBlock getASuccessor(Splits predSplits, Splits succSplits) {
|
||||
exists(ControlFlowElement pred | pred = this.getAnElement() |
|
||||
succSplits(pred, predSplits, result, succSplits, _)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the elements of this block are reachable from a callable entry
|
||||
* point, with the splits `splits`.
|
||||
*/
|
||||
predicate isReachable(Splits splits) {
|
||||
// Base case
|
||||
succEntrySplits(_, this, splits, _)
|
||||
or
|
||||
// Recursive case
|
||||
exists(SameSplitsBlock pred, Splits predSplits | pred.isReachable(predSplits) |
|
||||
this = pred.getASuccessor(predSplits, splits)
|
||||
)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
cached
|
||||
private module Cached {
|
||||
/**
|
||||
* If needed, call this predicate from `ControlFlowGraphImplSpecific.qll` in order to
|
||||
* force a stage-dependency on the `ControlFlowGraphImplShared.qll` stage and therby
|
||||
* collapsing the two stages.
|
||||
*/
|
||||
cached
|
||||
predicate forceCachingInSameStage() { any() }
|
||||
|
||||
cached
|
||||
newtype TSplits =
|
||||
TSplitsNil() or
|
||||
TSplitsCons(SplitImpl head, Splits tail) {
|
||||
exists(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c, int rnk
|
||||
|
|
||||
case2aFromRank(pred, predSplits, succ, tail, c, rnk + 1) and
|
||||
head = case2aSomeAtRank(pred, predSplits, succ, c, rnk)
|
||||
)
|
||||
or
|
||||
succEntrySplitsCons(_, _, head, tail, _)
|
||||
}
|
||||
|
||||
cached
|
||||
string splitsToString(Splits splits) {
|
||||
splits = TSplitsNil() and
|
||||
result = ""
|
||||
or
|
||||
exists(SplitImpl head, Splits tail, string headString, string tailString |
|
||||
splits = TSplitsCons(head, tail)
|
||||
|
|
||||
headString = head.toString() and
|
||||
tailString = tail.toString() and
|
||||
if tailString = ""
|
||||
then result = headString
|
||||
else
|
||||
if headString = ""
|
||||
then result = tailString
|
||||
else result = headString + ", " + tailString
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Internal representation of control flow nodes in the control flow graph.
|
||||
* The control flow graph is pruned for unreachable nodes.
|
||||
*/
|
||||
cached
|
||||
newtype TNode =
|
||||
TEntryNode(CfgScope scope) { succEntrySplits(scope, _, _, _) } or
|
||||
TAnnotatedExitNode(CfgScope scope, boolean normal) {
|
||||
exists(Reachability::SameSplitsBlock b, SuccessorType t | b.isReachable(_) |
|
||||
succExitSplits(b.getAnElement(), _, scope, t) and
|
||||
if isAbnormalExitType(t) then normal = false else normal = true
|
||||
)
|
||||
} or
|
||||
TExitNode(CfgScope scope) {
|
||||
exists(Reachability::SameSplitsBlock b | b.isReachable(_) |
|
||||
succExitSplits(b.getAnElement(), _, scope, _)
|
||||
)
|
||||
} or
|
||||
TElementNode(ControlFlowElement cfe, Splits splits) {
|
||||
exists(Reachability::SameSplitsBlock b | b.isReachable(splits) | cfe = b.getAnElement())
|
||||
}
|
||||
|
||||
/** Gets a successor node of a given flow type, if any. */
|
||||
cached
|
||||
TNode getASuccessor(TNode pred, SuccessorType t) {
|
||||
// Callable entry node -> callable body
|
||||
exists(ControlFlowElement succElement, Splits succSplits, CfgScope scope |
|
||||
result = TElementNode(succElement, succSplits) and
|
||||
pred = TEntryNode(scope) and
|
||||
succEntrySplits(scope, succElement, succSplits, t)
|
||||
)
|
||||
or
|
||||
exists(ControlFlowElement predElement, Splits predSplits |
|
||||
pred = TElementNode(predElement, predSplits)
|
||||
|
|
||||
// Element node -> callable exit (annotated)
|
||||
exists(CfgScope scope, boolean normal |
|
||||
result = TAnnotatedExitNode(scope, normal) and
|
||||
succExitSplits(predElement, predSplits, scope, t) and
|
||||
if isAbnormalExitType(t) then normal = false else normal = true
|
||||
)
|
||||
or
|
||||
// Element node -> element node
|
||||
exists(ControlFlowElement succElement, Splits succSplits, Completion c |
|
||||
result = TElementNode(succElement, succSplits)
|
||||
|
|
||||
succSplits(predElement, predSplits, succElement, succSplits, c) and
|
||||
t = getAMatchingSuccessorType(c)
|
||||
)
|
||||
)
|
||||
or
|
||||
// Callable exit (annotated) -> callable exit
|
||||
exists(CfgScope scope |
|
||||
pred = TAnnotatedExitNode(scope, _) and
|
||||
result = TExitNode(scope) and
|
||||
successorTypeIsSimple(t)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets a first control flow element executed within `cfe`.
|
||||
*/
|
||||
cached
|
||||
ControlFlowElement getAControlFlowEntryNode(ControlFlowElement cfe) { first(cfe, result) }
|
||||
|
||||
/**
|
||||
* Gets a potential last control flow element executed within `cfe`.
|
||||
*/
|
||||
cached
|
||||
ControlFlowElement getAControlFlowExitNode(ControlFlowElement cfe) { last(cfe, result, _) }
|
||||
}
|
||||
|
||||
import Cached
|
||||
|
||||
/**
|
||||
* Import this module into a `.ql` file of `@kind graph` to render a CFG. The
|
||||
* graph is restricted to nodes from `RelevantNode`.
|
||||
*/
|
||||
module TestOutput {
|
||||
abstract class RelevantNode extends Node { }
|
||||
|
||||
query predicate nodes(RelevantNode n, string attr, string val) {
|
||||
attr = "semmle.order" and
|
||||
val =
|
||||
any(int i |
|
||||
n =
|
||||
rank[i](RelevantNode p, Location l |
|
||||
l = p.getLocation()
|
||||
|
|
||||
p
|
||||
order by
|
||||
l.getFile().getBaseName(), l.getFile().getAbsolutePath(), l.getStartLine(),
|
||||
l.getStartColumn()
|
||||
)
|
||||
).toString()
|
||||
}
|
||||
|
||||
query predicate edges(RelevantNode pred, RelevantNode succ, string attr, string val) {
|
||||
exists(SuccessorType t | succ = getASuccessor(pred, t) |
|
||||
attr = "semmle.label" and
|
||||
if successorTypeIsSimple(t) then val = "" else val = t.toString()
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
/** Provides a set of splitting-related consistency queries. */
|
||||
module Consistency {
|
||||
query predicate nonUniqueSetRepresentation(Splits s1, Splits s2) {
|
||||
forex(Split s | s = s1.getASplit() | s = s2.getASplit()) and
|
||||
forex(Split s | s = s2.getASplit() | s = s1.getASplit()) and
|
||||
s1 != s2
|
||||
}
|
||||
|
||||
query predicate breakInvariant2(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Splits succSplits,
|
||||
SplitImpl split, Completion c
|
||||
) {
|
||||
succSplits(pred, predSplits, succ, succSplits, c) and
|
||||
split = predSplits.getASplit() and
|
||||
split.hasSuccessor(pred, succ, c) and
|
||||
not split = succSplits.getASplit()
|
||||
}
|
||||
|
||||
query predicate breakInvariant3(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Splits succSplits,
|
||||
SplitImpl split, Completion c
|
||||
) {
|
||||
succSplits(pred, predSplits, succ, succSplits, c) and
|
||||
split = predSplits.getASplit() and
|
||||
split.hasExit(pred, succ, c) and
|
||||
not split.hasEntry(pred, succ, c) and
|
||||
split = succSplits.getASplit()
|
||||
}
|
||||
|
||||
query predicate breakInvariant4(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Splits succSplits,
|
||||
SplitImpl split, Completion c
|
||||
) {
|
||||
succSplits(pred, predSplits, succ, succSplits, c) and
|
||||
split.hasEntry(pred, succ, c) and
|
||||
not split.getKind() = predSplits.getASplit().getKind() and
|
||||
not split = succSplits.getASplit()
|
||||
}
|
||||
|
||||
query predicate breakInvariant5(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Splits succSplits,
|
||||
SplitImpl split, Completion c
|
||||
) {
|
||||
succSplits(pred, predSplits, succ, succSplits, c) and
|
||||
split = succSplits.getASplit() and
|
||||
not (split.hasSuccessor(pred, succ, c) and split = predSplits.getASplit()) and
|
||||
not split.hasEntry(pred, succ, c)
|
||||
}
|
||||
|
||||
query predicate multipleSuccessors(Node node, SuccessorType t, Node successor) {
|
||||
not node instanceof TEntryNode and
|
||||
strictcount(getASuccessor(node, t)) > 1 and
|
||||
successor = getASuccessor(node, t)
|
||||
}
|
||||
}
|
||||
@@ -0,0 +1,69 @@
|
||||
private import csharp as CS
|
||||
private import ControlFlowGraphImpl as Impl
|
||||
private import Completion as Comp
|
||||
private import Splitting as Splitting
|
||||
private import SuccessorType as ST
|
||||
private import semmle.code.csharp.Caching
|
||||
|
||||
class ControlFlowTreeBase = Impl::ControlFlowTree::Range;
|
||||
|
||||
class ControlFlowElement = CS::ControlFlowElement;
|
||||
|
||||
class Completion = Comp::Completion;
|
||||
|
||||
/**
|
||||
* Hold if `c` represents normal evaluation of a statement or an
|
||||
* expression.
|
||||
*/
|
||||
predicate completionIsNormal(Completion c) { c instanceof Comp::NormalCompletion }
|
||||
|
||||
/**
|
||||
* Hold if `c` represents simple (normal) evaluation of a statement or an
|
||||
* expression.
|
||||
*/
|
||||
predicate completionIsSimple(Completion c) { c instanceof Comp::SimpleCompletion }
|
||||
|
||||
/** Holds if `c` is a valid completion for `e`. */
|
||||
predicate completionIsValidFor(Completion c, ControlFlowElement e) { c.isValidFor(e) }
|
||||
|
||||
class CfgScope = Impl::CfgScope;
|
||||
|
||||
/** Gets the CFG scope for `e`. */
|
||||
CfgScope getCfgScope(ControlFlowElement e) {
|
||||
Stages::ControlFlowStage::forceCachingInSameStage() and
|
||||
result = e.getEnclosingCallable()
|
||||
}
|
||||
|
||||
predicate scopeFirst = Impl::scopeFirst/2;
|
||||
|
||||
predicate scopeLast = Impl::scopeLast/3;
|
||||
|
||||
/** The maximum number of splits allowed for a given node. */
|
||||
int maxSplits() { result = 5 }
|
||||
|
||||
class SplitKindBase = Splitting::TSplitKind;
|
||||
|
||||
class Split = Splitting::Split;
|
||||
|
||||
class SuccessorType = ST::SuccessorType;
|
||||
|
||||
/** Gets a successor type that matches completion `c`. */
|
||||
SuccessorType getAMatchingSuccessorType(Completion c) { result = c.getAMatchingSuccessorType() }
|
||||
|
||||
/**
|
||||
* Hold if `c` represents simple (normal) evaluation of a statement or an
|
||||
* expression.
|
||||
*/
|
||||
predicate successorTypeIsSimple(SuccessorType t) {
|
||||
t instanceof ST::SuccessorTypes::NormalSuccessor
|
||||
}
|
||||
|
||||
/** Holds if `t` is an abnormal exit type out of a callable. */
|
||||
predicate isAbnormalExitType(SuccessorType t) {
|
||||
t instanceof ST::SuccessorTypes::ExceptionSuccessor or
|
||||
t instanceof ST::SuccessorTypes::ExitSuccessor
|
||||
}
|
||||
|
||||
class Location = CS::Location;
|
||||
|
||||
class Node = CS::ControlFlow::Node;
|
||||
@@ -11,9 +11,6 @@ private import SuccessorTypes
|
||||
private import semmle.code.csharp.controlflow.ControlFlowGraph::ControlFlow
|
||||
private import semmle.code.csharp.controlflow.internal.PreSsa
|
||||
|
||||
/** The maximum number of splits allowed for a given node. */
|
||||
private int maxSplits() { result = 5 }
|
||||
|
||||
cached
|
||||
private module Cached {
|
||||
private import semmle.code.csharp.Caching
|
||||
@@ -51,42 +48,9 @@ private module Cached {
|
||||
branch in [false, true]
|
||||
} or
|
||||
TLoopSplit(LoopSplitting::AnalyzableLoopStmt loop)
|
||||
|
||||
cached
|
||||
newtype TSplits =
|
||||
TSplitsNil() or
|
||||
TSplitsCons(SplitImpl head, Splits tail) {
|
||||
exists(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c, int rnk
|
||||
|
|
||||
case2aFromRank(pred, predSplits, succ, tail, c, rnk + 1) and
|
||||
head = case2aSomeAtRank(pred, predSplits, succ, c, rnk)
|
||||
)
|
||||
or
|
||||
succEntrySplitsCons(_, _, head, tail, _)
|
||||
}
|
||||
|
||||
cached
|
||||
string splitsToString(Splits splits) {
|
||||
splits = TSplitsNil() and
|
||||
result = ""
|
||||
or
|
||||
exists(SplitImpl head, Splits tail, string headString, string tailString |
|
||||
splits = TSplitsCons(head, tail)
|
||||
|
|
||||
headString = head.toString() and
|
||||
tailString = tail.toString() and
|
||||
if tailString = ""
|
||||
then result = headString
|
||||
else
|
||||
if headString = ""
|
||||
then result = tailString
|
||||
else result = headString + ", " + tailString
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
private import Cached
|
||||
import Cached
|
||||
|
||||
/**
|
||||
* A split for a control flow element. For example, a tag that determines how to
|
||||
@@ -97,127 +61,6 @@ class Split extends TSplit {
|
||||
string toString() { none() }
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if split kinds `sk1` and `sk2` may overlap. That is, they may apply
|
||||
* to at least one common control flow element inside callable `c`.
|
||||
*/
|
||||
private predicate overlapping(Callable c, SplitKind sk1, SplitKind sk2) {
|
||||
exists(ControlFlowElement cfe |
|
||||
sk1.appliesTo(cfe) and
|
||||
sk2.appliesTo(cfe) and
|
||||
c = cfe.getEnclosingCallable()
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* A split kind. Each control flow node can have at most one split of a
|
||||
* given kind.
|
||||
*/
|
||||
abstract class SplitKind extends TSplitKind {
|
||||
/** Gets a split of this kind. */
|
||||
SplitImpl getASplit() { result.getKind() = this }
|
||||
|
||||
/** Holds if some split of this kind applies to control flow element `cfe`. */
|
||||
predicate appliesTo(ControlFlowElement cfe) { this.getASplit().appliesTo(cfe) }
|
||||
|
||||
/**
|
||||
* Gets a unique integer representing this split kind. The integer is used
|
||||
* to represent sets of splits as ordered lists.
|
||||
*/
|
||||
abstract int getListOrder();
|
||||
|
||||
/** Gets the rank of this split kind among all overlapping kinds for `c`. */
|
||||
private int getRank(Callable c) {
|
||||
this = rank[result](SplitKind sk | overlapping(c, this, sk) | sk order by sk.getListOrder())
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if this split kind is enabled for control flow element `cfe`. For
|
||||
* performance reasons, the number of splits is restricted by the `maxSplits()`
|
||||
* predicate.
|
||||
*/
|
||||
predicate isEnabled(ControlFlowElement cfe) {
|
||||
this.appliesTo(cfe) and
|
||||
this.getRank(cfe.getEnclosingCallable()) <= maxSplits()
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the rank of this split kind among all the split kinds that apply to
|
||||
* control flow element `cfe`. The rank is based on the order defined by
|
||||
* `getListOrder()`.
|
||||
*/
|
||||
int getListRank(ControlFlowElement cfe) {
|
||||
this.isEnabled(cfe) and
|
||||
this = rank[result](SplitKind sk | sk.appliesTo(cfe) | sk order by sk.getListOrder())
|
||||
}
|
||||
|
||||
/** Gets a textual representation of this split kind. */
|
||||
abstract string toString();
|
||||
}
|
||||
|
||||
// This class only exists to not pollute the externally visible `Split` class
|
||||
// with internal helper predicates
|
||||
abstract class SplitImpl extends Split {
|
||||
/** Gets the kind of this split. */
|
||||
abstract SplitKind getKind();
|
||||
|
||||
/**
|
||||
* Holds if this split is entered when control passes from `pred` to `succ` with
|
||||
* completion `c`.
|
||||
*
|
||||
* Invariant: `hasEntry(pred, succ, c) implies succ(pred, succ, c)`.
|
||||
*/
|
||||
abstract predicate hasEntry(ControlFlowElement pred, ControlFlowElement succ, Completion c);
|
||||
|
||||
/**
|
||||
* Holds if this split is entered when control passes from `scope` to the entry point
|
||||
* `first`.
|
||||
*
|
||||
* Invariant: `hasEntryScope(scope, first) implies scopeFirst(scope, first)`.
|
||||
*/
|
||||
abstract predicate hasEntryScope(CfgScope scope, ControlFlowElement first);
|
||||
|
||||
/**
|
||||
* Holds if this split is left when control passes from `pred` to `succ` with
|
||||
* completion `c`.
|
||||
*
|
||||
* Invariant: `hasExit(pred, succ, c) implies succ(pred, succ, c)`.
|
||||
*/
|
||||
abstract predicate hasExit(ControlFlowElement pred, ControlFlowElement succ, Completion c);
|
||||
|
||||
/**
|
||||
* Holds if this split is left when control passes from `last` out of the enclosing
|
||||
* scope `scope` with completion `c`.
|
||||
*
|
||||
* Invariant: `hasExitScope(last, scope, c) implies scopeLast(scope, last, c)`
|
||||
*/
|
||||
abstract predicate hasExitScope(ControlFlowElement last, CfgScope scope, Completion c);
|
||||
|
||||
/**
|
||||
* Holds if this split is maintained when control passes from `pred` to `succ` with
|
||||
* completion `c`.
|
||||
*
|
||||
* Invariant: `hasSuccessor(pred, succ, c) implies succ(pred, succ, c)`
|
||||
*/
|
||||
abstract predicate hasSuccessor(ControlFlowElement pred, ControlFlowElement succ, Completion c);
|
||||
|
||||
/** Holds if this split applies to control flow element `cfe`. */
|
||||
final predicate appliesTo(ControlFlowElement cfe) {
|
||||
this.hasEntry(_, cfe, _)
|
||||
or
|
||||
this.hasEntryScope(_, cfe)
|
||||
or
|
||||
exists(ControlFlowElement pred | this.appliesTo(pred) | this.hasSuccessor(pred, cfe, _))
|
||||
}
|
||||
|
||||
/** The `succ` relation restricted to predecessors `pred` that this split applies to. */
|
||||
pragma[noinline]
|
||||
final predicate appliesSucc(ControlFlowElement pred, ControlFlowElement succ, Completion c) {
|
||||
this.appliesTo(pred) and
|
||||
succ(pred, succ, c)
|
||||
}
|
||||
}
|
||||
|
||||
module InitializerSplitting {
|
||||
private import semmle.code.csharp.ExprOrStmtParent
|
||||
|
||||
@@ -382,7 +225,7 @@ module InitializerSplitting {
|
||||
succ.getEnclosingCallable() = this.getConstructor()
|
||||
}
|
||||
|
||||
override predicate hasExitScope(ControlFlowElement last, CfgScope scope, Completion c) {
|
||||
override predicate hasExitScope(CfgScope scope, ControlFlowElement last, Completion c) {
|
||||
this.appliesTo(last) and
|
||||
scopeLast(scope, last, c) and
|
||||
scope = this.getConstructor()
|
||||
@@ -499,7 +342,7 @@ module ConditionalCompletionSplitting {
|
||||
if c instanceof ConditionalCompletion then completion = c else any()
|
||||
}
|
||||
|
||||
override predicate hasExitScope(ControlFlowElement last, CfgScope scope, Completion c) {
|
||||
override predicate hasExitScope(CfgScope scope, ControlFlowElement last, Completion c) {
|
||||
this.appliesTo(last) and
|
||||
scopeLast(scope, last, c) and
|
||||
if c instanceof ConditionalCompletion then completion = c else any()
|
||||
@@ -612,7 +455,7 @@ module AssertionSplitting {
|
||||
)
|
||||
}
|
||||
|
||||
override predicate hasExitScope(ControlFlowElement last, CfgScope scope, Completion c) {
|
||||
override predicate hasExitScope(CfgScope scope, ControlFlowElement last, Completion c) {
|
||||
this.appliesTo(last) and
|
||||
last = a and
|
||||
scopeLast(scope, last, c) and
|
||||
@@ -853,7 +696,7 @@ module FinallySplitting {
|
||||
)
|
||||
}
|
||||
|
||||
override predicate hasExitScope(ControlFlowElement last, CfgScope scope, Completion c) {
|
||||
override predicate hasExitScope(CfgScope scope, ControlFlowElement last, Completion c) {
|
||||
scopeLast(scope, last, c) and
|
||||
(
|
||||
exit(last, c, _)
|
||||
@@ -1033,7 +876,7 @@ module ExceptionHandlerSplitting {
|
||||
)
|
||||
}
|
||||
|
||||
override predicate hasExitScope(ControlFlowElement last, CfgScope scope, Completion c) {
|
||||
override predicate hasExitScope(CfgScope scope, ControlFlowElement last, Completion c) {
|
||||
// Exit out from last `catch` clause (no catch clauses match)
|
||||
this.hasLastExit(last, c) and
|
||||
scopeLast(scope, last, c)
|
||||
@@ -1292,7 +1135,7 @@ module BooleanSplitting {
|
||||
)
|
||||
}
|
||||
|
||||
override predicate hasExitScope(ControlFlowElement last, CfgScope scope, Completion c) {
|
||||
override predicate hasExitScope(CfgScope scope, ControlFlowElement last, Completion c) {
|
||||
exists(PreBasicBlock bb | this.appliesToBlock(bb, c) |
|
||||
last = bb.getLastElement() and
|
||||
scopeLast(scope, last, c)
|
||||
@@ -1486,7 +1329,7 @@ module LoopSplitting {
|
||||
loop.stop(pred, succ, c)
|
||||
}
|
||||
|
||||
override predicate hasExitScope(ControlFlowElement last, CfgScope scope, Completion c) {
|
||||
override predicate hasExitScope(CfgScope scope, ControlFlowElement last, Completion c) {
|
||||
this.appliesToPredecessor(last, c) and
|
||||
scopeLast(scope, last, c)
|
||||
}
|
||||
@@ -1498,463 +1341,3 @@ module LoopSplitting {
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* A set of control flow node splits. The set is represented by a list of splits,
|
||||
* ordered by ascending rank.
|
||||
*/
|
||||
class Splits extends TSplits {
|
||||
/** Gets a textual representation of this set of splits. */
|
||||
string toString() { result = splitsToString(this) }
|
||||
|
||||
/** Gets a split belonging to this set of splits. */
|
||||
SplitImpl getASplit() {
|
||||
exists(SplitImpl head, Splits tail | this = TSplitsCons(head, tail) |
|
||||
result = head
|
||||
or
|
||||
result = tail.getASplit()
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
private predicate succEntrySplitsFromRank(
|
||||
CfgScope pred, ControlFlowElement succ, Splits splits, int rnk
|
||||
) {
|
||||
splits = TSplitsNil() and
|
||||
scopeFirst(pred, succ) and
|
||||
rnk = 0
|
||||
or
|
||||
exists(SplitImpl head, Splits tail | succEntrySplitsCons(pred, succ, head, tail, rnk) |
|
||||
splits = TSplitsCons(head, tail)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate succEntrySplitsCons(
|
||||
Callable pred, ControlFlowElement succ, SplitImpl head, Splits tail, int rnk
|
||||
) {
|
||||
succEntrySplitsFromRank(pred, succ, tail, rnk - 1) and
|
||||
head.hasEntryScope(pred, succ) and
|
||||
rnk = head.getKind().getListRank(succ)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `succ` with splits `succSplits` is the first element that is executed
|
||||
* when entering callable `pred`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
predicate succEntrySplits(CfgScope pred, ControlFlowElement succ, Splits succSplits, SuccessorType t) {
|
||||
exists(int rnk |
|
||||
scopeFirst(pred, succ) and
|
||||
t instanceof NormalSuccessor and
|
||||
succEntrySplitsFromRank(pred, succ, succSplits, rnk)
|
||||
|
|
||||
rnk = 0 and
|
||||
not any(SplitImpl split).hasEntryScope(pred, succ)
|
||||
or
|
||||
rnk = max(SplitImpl split | split.hasEntryScope(pred, succ) | split.getKind().getListRank(succ))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `pred` with splits `predSplits` can exit the enclosing callable
|
||||
* `succ` with type `t`.
|
||||
*/
|
||||
predicate succExitSplits(ControlFlowElement pred, Splits predSplits, CfgScope succ, SuccessorType t) {
|
||||
exists(Reachability::SameSplitsBlock b, Completion c | pred = b.getAnElement() |
|
||||
b.isReachable(predSplits) and
|
||||
t = c.getAMatchingSuccessorType() and
|
||||
scopeLast(succ, pred, c) and
|
||||
forall(SplitImpl predSplit | predSplit = predSplits.getASplit() |
|
||||
predSplit.hasExitScope(pred, succ, c)
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Provides a predicate for the successor relation with split information,
|
||||
* as well as logic used to construct the type `TSplits` representing sets
|
||||
* of splits. Only sets of splits that can be reached are constructed, hence
|
||||
* the predicates are mutually recursive.
|
||||
*
|
||||
* For the successor relation
|
||||
*
|
||||
* ```ql
|
||||
* succSplits(ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Splits succSplits, Completion c)
|
||||
* ```
|
||||
*
|
||||
* the following invariants are maintained:
|
||||
*
|
||||
* 1. `pred` is reachable with split set `predSplits`.
|
||||
* 2. For all `split` in `predSplits`:
|
||||
* - If `split.hasSuccessor(pred, succ, c)` then `split` in `succSplits`.
|
||||
* 3. For all `split` in `predSplits`:
|
||||
* - If `split.hasExit(pred, succ, c)` and not `split.hasEntry(pred, succ, c)` then
|
||||
* `split` not in `succSplits`.
|
||||
* 4. For all `split` with kind not in `predSplits`:
|
||||
* - If `split.hasEntry(pred, succ, c)` then `split` in `succSplits`.
|
||||
* 5. For all `split` in `succSplits`:
|
||||
* - `split.hasSuccessor(pred, succ, c)` and `split` in `predSplits`, or
|
||||
* - `split.hasEntry(pred, succ, c)`.
|
||||
*
|
||||
* The algorithm divides into four cases:
|
||||
*
|
||||
* 1. The set of splits for the successor is the same as the set of splits
|
||||
* for the predecessor:
|
||||
* a) The successor is in the same `SameSplitsBlock` as the predecessor.
|
||||
* b) The successor is *not* in the same `SameSplitsBlock` as the predecessor.
|
||||
* 2. The set of splits for the successor is different from the set of splits
|
||||
* for the predecessor:
|
||||
* a) The set of splits for the successor is *maybe* non-empty.
|
||||
* b) The set of splits for the successor is *always* empty.
|
||||
*
|
||||
* Only case 2a may introduce new sets of splits, so only predicates from
|
||||
* this case are used in the definition of `TSplits`.
|
||||
*
|
||||
* The predicates in this module are named after the cases above.
|
||||
*/
|
||||
private module SuccSplits {
|
||||
private predicate succInvariant1(
|
||||
Reachability::SameSplitsBlock b, ControlFlowElement pred, Splits predSplits,
|
||||
ControlFlowElement succ, Completion c
|
||||
) {
|
||||
pred = b.getAnElement() and
|
||||
b.isReachable(predSplits) and
|
||||
succ(pred, succ, c)
|
||||
}
|
||||
|
||||
private predicate case1b0(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c
|
||||
) {
|
||||
exists(Reachability::SameSplitsBlock b |
|
||||
// Invariant 1
|
||||
succInvariant1(b, pred, predSplits, succ, c)
|
||||
|
|
||||
(succ = b.getAnElement() implies succ = b) and
|
||||
// Invariant 4
|
||||
not exists(SplitImpl split | split.hasEntry(pred, succ, c))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Case 1b.
|
||||
*
|
||||
* Invariants 1 and 4 hold in the base case, and invariants 2, 3, and 5 are
|
||||
* maintained for all splits in `predSplits` (= `succSplits`), except
|
||||
* possibly for the splits in `except`.
|
||||
*
|
||||
* The predicate is written using explicit recursion, as opposed to a `forall`,
|
||||
* to avoid negative recursion.
|
||||
*/
|
||||
private predicate case1bForall(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c, Splits except
|
||||
) {
|
||||
case1b0(pred, predSplits, succ, c) and
|
||||
except = predSplits
|
||||
or
|
||||
exists(SplitImpl split |
|
||||
case1bForallCons(pred, predSplits, succ, c, split, except) and
|
||||
split.hasSuccessor(pred, succ, c)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate case1bForallCons(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c,
|
||||
SplitImpl exceptHead, Splits exceptTail
|
||||
) {
|
||||
case1bForall(pred, predSplits, succ, c, TSplitsCons(exceptHead, exceptTail))
|
||||
}
|
||||
|
||||
private predicate case1(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c
|
||||
) {
|
||||
// Case 1a
|
||||
exists(Reachability::SameSplitsBlock b | succInvariant1(b, pred, predSplits, succ, c) |
|
||||
succ = b.getAnElement() and
|
||||
not succ = b
|
||||
)
|
||||
or
|
||||
// Case 1b
|
||||
case1bForall(pred, predSplits, succ, c, TSplitsNil())
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private SplitImpl succInvariant1GetASplit(
|
||||
Reachability::SameSplitsBlock b, ControlFlowElement pred, Splits predSplits,
|
||||
ControlFlowElement succ, Completion c
|
||||
) {
|
||||
succInvariant1(b, pred, predSplits, succ, c) and
|
||||
result = predSplits.getASplit()
|
||||
}
|
||||
|
||||
private predicate case2aux(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c
|
||||
) {
|
||||
exists(Reachability::SameSplitsBlock b |
|
||||
succInvariant1(b, pred, predSplits, succ, c) and
|
||||
(succ = b.getAnElement() implies succ = b)
|
||||
|
|
||||
succInvariant1GetASplit(b, pred, predSplits, succ, c).hasExit(pred, succ, c)
|
||||
or
|
||||
any(SplitImpl split).hasEntry(pred, succ, c)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `succSplits` should not inherit a split of kind `sk` from
|
||||
* `predSplits`, except possibly because of a split in `except`.
|
||||
*
|
||||
* The predicate is written using explicit recursion, as opposed to a `forall`,
|
||||
* to avoid negative recursion.
|
||||
*/
|
||||
private predicate case2aNoneInheritedOfKindForall(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c, SplitKind sk,
|
||||
Splits except
|
||||
) {
|
||||
case2aux(pred, predSplits, succ, c) and
|
||||
sk.appliesTo(succ) and
|
||||
except = predSplits
|
||||
or
|
||||
exists(Splits mid, SplitImpl split |
|
||||
case2aNoneInheritedOfKindForall(pred, predSplits, succ, c, sk, mid) and
|
||||
mid = TSplitsCons(split, except)
|
||||
|
|
||||
split.getKind() = any(SplitKind sk0 | sk0 != sk and sk0.appliesTo(succ))
|
||||
or
|
||||
split.hasExit(pred, succ, c)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate entryOfKind(
|
||||
ControlFlowElement pred, ControlFlowElement succ, Completion c, SplitImpl split, SplitKind sk
|
||||
) {
|
||||
split.hasEntry(pred, succ, c) and
|
||||
sk = split.getKind()
|
||||
}
|
||||
|
||||
/** Holds if `succSplits` should not have a split of kind `sk`. */
|
||||
pragma[nomagic]
|
||||
private predicate case2aNoneOfKind(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c, SplitKind sk
|
||||
) {
|
||||
// None inherited from predecessor
|
||||
case2aNoneInheritedOfKindForall(pred, predSplits, succ, c, sk, TSplitsNil()) and
|
||||
// None newly entered into
|
||||
not entryOfKind(pred, succ, c, _, sk)
|
||||
}
|
||||
|
||||
/** Holds if `succSplits` should not have a split of kind `sk` at rank `rnk`. */
|
||||
pragma[nomagic]
|
||||
private predicate case2aNoneAtRank(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c, int rnk
|
||||
) {
|
||||
exists(SplitKind sk | case2aNoneOfKind(pred, predSplits, succ, c, sk) |
|
||||
rnk = sk.getListRank(succ)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private SplitImpl case2auxGetAPredecessorSplit(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c
|
||||
) {
|
||||
case2aux(pred, predSplits, succ, c) and
|
||||
result = predSplits.getASplit()
|
||||
}
|
||||
|
||||
/** Gets a split that should be in `succSplits`. */
|
||||
pragma[nomagic]
|
||||
private SplitImpl case2aSome(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c, SplitKind sk
|
||||
) {
|
||||
(
|
||||
// Inherited from predecessor
|
||||
result = case2auxGetAPredecessorSplit(pred, predSplits, succ, c) and
|
||||
result.hasSuccessor(pred, succ, c)
|
||||
or
|
||||
// Newly entered into
|
||||
exists(SplitKind sk0 |
|
||||
case2aNoneInheritedOfKindForall(pred, predSplits, succ, c, sk0, TSplitsNil())
|
||||
|
|
||||
entryOfKind(pred, succ, c, result, sk0)
|
||||
)
|
||||
) and
|
||||
sk = result.getKind()
|
||||
}
|
||||
|
||||
/** Gets a split that should be in `succSplits` at rank `rnk`. */
|
||||
pragma[nomagic]
|
||||
SplitImpl case2aSomeAtRank(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c, int rnk
|
||||
) {
|
||||
exists(SplitKind sk | result = case2aSome(pred, predSplits, succ, c, sk) |
|
||||
rnk = sk.getListRank(succ)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Case 2a.
|
||||
*
|
||||
* As opposed to the other cases, in this case we need to construct a new set
|
||||
* of splits `succSplits`. Since this involves constructing the very IPA type,
|
||||
* we cannot recurse directly over the structure of `succSplits`. Instead, we
|
||||
* recurse over the ranks of all splits that *might* be in `succSplits`.
|
||||
*
|
||||
* - Invariant 1 holds in the base case,
|
||||
* - invariant 2 holds for all splits with rank at least `rnk`,
|
||||
* - invariant 3 holds for all splits in `predSplits`,
|
||||
* - invariant 4 holds for all splits in `succSplits` with rank at least `rnk`,
|
||||
* and
|
||||
* - invariant 4 holds for all splits in `succSplits` with rank at least `rnk`.
|
||||
*/
|
||||
predicate case2aFromRank(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Splits succSplits,
|
||||
Completion c, int rnk
|
||||
) {
|
||||
case2aux(pred, predSplits, succ, c) and
|
||||
succSplits = TSplitsNil() and
|
||||
rnk = max(any(SplitKind sk).getListRank(succ)) + 1
|
||||
or
|
||||
case2aFromRank(pred, predSplits, succ, succSplits, c, rnk + 1) and
|
||||
case2aNoneAtRank(pred, predSplits, succ, c, rnk)
|
||||
or
|
||||
exists(Splits mid, SplitImpl split | split = case2aCons(pred, predSplits, succ, mid, c, rnk) |
|
||||
succSplits = TSplitsCons(split, mid)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private SplitImpl case2aCons(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Splits succSplits,
|
||||
Completion c, int rnk
|
||||
) {
|
||||
case2aFromRank(pred, predSplits, succ, succSplits, c, rnk + 1) and
|
||||
result = case2aSomeAtRank(pred, predSplits, succ, c, rnk)
|
||||
}
|
||||
|
||||
/**
|
||||
* Case 2b.
|
||||
*
|
||||
* Invariants 1, 4, and 5 hold in the base case, and invariants 2 and 3 are
|
||||
* maintained for all splits in `predSplits`, except possibly for the splits
|
||||
* in `except`.
|
||||
*
|
||||
* The predicate is written using explicit recursion, as opposed to a `forall`,
|
||||
* to avoid negative recursion.
|
||||
*/
|
||||
private predicate case2bForall(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c, Splits except
|
||||
) {
|
||||
// Invariant 1
|
||||
case2aux(pred, predSplits, succ, c) and
|
||||
// Invariants 4 and 5
|
||||
not any(SplitKind sk).appliesTo(succ) and
|
||||
except = predSplits
|
||||
or
|
||||
exists(SplitImpl split | case2bForallCons(pred, predSplits, succ, c, split, except) |
|
||||
// Invariants 2 and 3
|
||||
split.hasExit(pred, succ, c)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate case2bForallCons(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c,
|
||||
SplitImpl exceptHead, Splits exceptTail
|
||||
) {
|
||||
case2bForall(pred, predSplits, succ, c, TSplitsCons(exceptHead, exceptTail))
|
||||
}
|
||||
|
||||
private predicate case2(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Splits succSplits,
|
||||
Completion c
|
||||
) {
|
||||
case2aFromRank(pred, predSplits, succ, succSplits, c, 1)
|
||||
or
|
||||
case2bForall(pred, predSplits, succ, c, TSplitsNil()) and
|
||||
succSplits = TSplitsNil()
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `succ` with splits `succSplits` is a successor of type `t` for `pred`
|
||||
* with splits `predSplits`.
|
||||
*/
|
||||
predicate succSplits(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Splits succSplits,
|
||||
Completion c
|
||||
) {
|
||||
case1(pred, predSplits, succ, c) and
|
||||
succSplits = predSplits
|
||||
or
|
||||
case2(pred, predSplits, succ, succSplits, c)
|
||||
}
|
||||
}
|
||||
|
||||
import SuccSplits
|
||||
|
||||
/** Provides logic for calculating reachable control flow nodes. */
|
||||
module Reachability {
|
||||
/**
|
||||
* Holds if `cfe` is a control flow element where the set of possible splits may
|
||||
* be different from the set of possible splits for one of `cfe`'s predecessors.
|
||||
* That is, `cfe` starts a new block of elements with the same set of splits.
|
||||
*/
|
||||
private predicate startsSplits(ControlFlowElement cfe) {
|
||||
scopeFirst(_, cfe)
|
||||
or
|
||||
exists(SplitImpl s |
|
||||
s.hasEntry(_, cfe, _)
|
||||
or
|
||||
s.hasExit(_, cfe, _)
|
||||
)
|
||||
or
|
||||
exists(ControlFlowElement pred, SplitImpl split, Completion c | succ(pred, cfe, c) |
|
||||
split.appliesTo(pred) and
|
||||
not split.hasSuccessor(pred, cfe, c)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate intraSplitsSucc(ControlFlowElement pred, ControlFlowElement succ) {
|
||||
succ(pred, succ, _) and
|
||||
not startsSplits(succ)
|
||||
}
|
||||
|
||||
private predicate splitsBlockContains(ControlFlowElement start, ControlFlowElement cfe) =
|
||||
fastTC(intraSplitsSucc/2)(start, cfe)
|
||||
|
||||
/**
|
||||
* A block of control flow elements where the set of splits is guaranteed
|
||||
* to remain unchanged, represented by the first element in the block.
|
||||
*/
|
||||
class SameSplitsBlock extends ControlFlowElement {
|
||||
SameSplitsBlock() { startsSplits(this) }
|
||||
|
||||
/** Gets a control flow element in this block. */
|
||||
ControlFlowElement getAnElement() {
|
||||
splitsBlockContains(this, result)
|
||||
or
|
||||
result = this
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private SameSplitsBlock getASuccessor(Splits predSplits, Splits succSplits) {
|
||||
exists(ControlFlowElement pred | pred = this.getAnElement() |
|
||||
succSplits(pred, predSplits, result, succSplits, _)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the elements of this block are reachable from a callable entry
|
||||
* point, with the splits `splits`.
|
||||
*/
|
||||
predicate isReachable(Splits splits) {
|
||||
// Base case
|
||||
succEntrySplits(_, this, splits, _)
|
||||
or
|
||||
// Recursive case
|
||||
exists(SameSplitsBlock pred, Splits predSplits | pred.isReachable(predSplits) |
|
||||
this = pred.getASuccessor(predSplits, splits)
|
||||
)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
@@ -677,7 +677,7 @@
|
||||
| Initializers.cs:8:5:8:16 | enter Initializers | Initializers.cs:8:5:8:16 | exit Initializers | 16 |
|
||||
| Initializers.cs:10:5:10:16 | enter Initializers | Initializers.cs:10:5:10:16 | exit Initializers | 16 |
|
||||
| Initializers.cs:12:10:12:10 | enter M | Initializers.cs:12:10:12:10 | exit M | 22 |
|
||||
| Initializers.cs:18:20:18:20 | 1 | Initializers.cs:18:16:18:20 | ... = ... | 2 |
|
||||
| Initializers.cs:18:16:18:16 | enter H | Initializers.cs:18:16:18:20 | ... = ... | 3 |
|
||||
| Initializers.cs:20:11:20:23 | enter NoConstructor | Initializers.cs:20:11:20:23 | exit NoConstructor | 9 |
|
||||
| Initializers.cs:31:9:31:11 | enter Sub | Initializers.cs:31:9:31:11 | exit Sub | 12 |
|
||||
| Initializers.cs:33:9:33:11 | enter Sub | Initializers.cs:33:9:33:11 | exit Sub | 9 |
|
||||
|
||||
@@ -1,7 +1,7 @@
|
||||
preBasicBlockConsistency
|
||||
nonUniqueSetRepresentation
|
||||
breakInvariant2
|
||||
breakInvariant3
|
||||
breakInvariant4
|
||||
breakInvariant5
|
||||
multipleSuccessors
|
||||
preBasicBlockConsistency
|
||||
|
||||
@@ -4,6 +4,7 @@ import semmle.code.csharp.controlflow.internal.PreBasicBlocks
|
||||
import ControlFlow
|
||||
import semmle.code.csharp.controlflow.internal.ControlFlowGraphImpl
|
||||
import semmle.code.csharp.controlflow.internal.Splitting
|
||||
import Consistency
|
||||
|
||||
predicate bbStartInconsistency(ControlFlowElement cfe) {
|
||||
exists(ControlFlow::BasicBlock bb | bb.getFirstNode() = cfe.getAControlFlowNode()) and
|
||||
@@ -49,58 +50,3 @@ query predicate preBasicBlockConsistency(ControlFlowElement cfe1, ControlFlowEle
|
||||
bbIntraSuccInconsistency(cfe1, cfe2) and
|
||||
s = "intra succ inconsistency"
|
||||
}
|
||||
|
||||
query predicate nonUniqueSetRepresentation(Splits s1, Splits s2) {
|
||||
forex(Nodes::Split s | s = s1.getASplit() | s = s2.getASplit()) and
|
||||
forex(Nodes::Split s | s = s2.getASplit() | s = s1.getASplit()) and
|
||||
s1 != s2
|
||||
}
|
||||
|
||||
query predicate breakInvariant2(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Splits succSplits,
|
||||
SplitImpl split, Completion c
|
||||
) {
|
||||
succSplits(pred, predSplits, succ, succSplits, c) and
|
||||
split = predSplits.getASplit() and
|
||||
split.hasSuccessor(pred, succ, c) and
|
||||
not split = succSplits.getASplit()
|
||||
}
|
||||
|
||||
query predicate breakInvariant3(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Splits succSplits,
|
||||
SplitImpl split, Completion c
|
||||
) {
|
||||
succSplits(pred, predSplits, succ, succSplits, c) and
|
||||
split = predSplits.getASplit() and
|
||||
split.hasExit(pred, succ, c) and
|
||||
not split.hasEntry(pred, succ, c) and
|
||||
split = succSplits.getASplit()
|
||||
}
|
||||
|
||||
query predicate breakInvariant4(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Splits succSplits,
|
||||
SplitImpl split, Completion c
|
||||
) {
|
||||
succSplits(pred, predSplits, succ, succSplits, c) and
|
||||
split.hasEntry(pred, succ, c) and
|
||||
not split.getKind() = predSplits.getASplit().getKind() and
|
||||
not split = succSplits.getASplit()
|
||||
}
|
||||
|
||||
query predicate breakInvariant5(
|
||||
ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Splits succSplits,
|
||||
SplitImpl split, Completion c
|
||||
) {
|
||||
succSplits(pred, predSplits, succ, succSplits, c) and
|
||||
split = succSplits.getASplit() and
|
||||
not (split.hasSuccessor(pred, succ, c) and split = predSplits.getASplit()) and
|
||||
not split.hasEntry(pred, succ, c)
|
||||
}
|
||||
|
||||
query predicate multipleSuccessors(
|
||||
ControlFlow::Node node, SuccessorType t, ControlFlow::Node successor
|
||||
) {
|
||||
not node instanceof ControlFlow::Nodes::EntryNode and
|
||||
strictcount(node.getASuccessorByType(t)) > 1 and
|
||||
successor = node.getASuccessorByType(t)
|
||||
}
|
||||
|
||||
@@ -2504,6 +2504,7 @@ dominance
|
||||
| Initializers.cs:15:39:15:39 | access to local variable i | Initializers.cs:15:59:15:60 | "" |
|
||||
| Initializers.cs:15:42:15:61 | object creation of type Initializers | Initializers.cs:15:37:15:63 | { ..., ... } |
|
||||
| Initializers.cs:15:59:15:60 | "" | Initializers.cs:15:42:15:61 | object creation of type Initializers |
|
||||
| Initializers.cs:18:16:18:16 | enter H | Initializers.cs:18:20:18:20 | 1 |
|
||||
| Initializers.cs:18:20:18:20 | 1 | Initializers.cs:18:16:18:20 | ... = ... |
|
||||
| Initializers.cs:20:11:20:23 | enter NoConstructor | Initializers.cs:22:23:22:23 | this access |
|
||||
| Initializers.cs:20:11:20:23 | exit NoConstructor (normal) | Initializers.cs:20:11:20:23 | exit NoConstructor |
|
||||
@@ -6631,6 +6632,7 @@ postDominance
|
||||
| Initializers.cs:15:42:15:61 | object creation of type Initializers | Initializers.cs:15:59:15:60 | "" |
|
||||
| Initializers.cs:15:59:15:60 | "" | Initializers.cs:15:39:15:39 | access to local variable i |
|
||||
| Initializers.cs:18:16:18:20 | ... = ... | Initializers.cs:18:20:18:20 | 1 |
|
||||
| Initializers.cs:18:20:18:20 | 1 | Initializers.cs:18:16:18:16 | enter H |
|
||||
| Initializers.cs:20:11:20:23 | exit NoConstructor | Initializers.cs:20:11:20:23 | exit NoConstructor (normal) |
|
||||
| Initializers.cs:20:11:20:23 | exit NoConstructor (normal) | Initializers.cs:23:23:23:27 | ... = ... |
|
||||
| Initializers.cs:22:23:22:23 | this access | Initializers.cs:20:11:20:23 | enter NoConstructor |
|
||||
@@ -11274,7 +11276,7 @@ blockDominance
|
||||
| Initializers.cs:8:5:8:16 | enter Initializers | Initializers.cs:8:5:8:16 | enter Initializers |
|
||||
| Initializers.cs:10:5:10:16 | enter Initializers | Initializers.cs:10:5:10:16 | enter Initializers |
|
||||
| Initializers.cs:12:10:12:10 | enter M | Initializers.cs:12:10:12:10 | enter M |
|
||||
| Initializers.cs:18:20:18:20 | 1 | Initializers.cs:18:20:18:20 | 1 |
|
||||
| Initializers.cs:18:16:18:16 | enter H | Initializers.cs:18:16:18:16 | enter H |
|
||||
| Initializers.cs:20:11:20:23 | enter NoConstructor | Initializers.cs:20:11:20:23 | enter NoConstructor |
|
||||
| Initializers.cs:31:9:31:11 | enter Sub | Initializers.cs:31:9:31:11 | enter Sub |
|
||||
| Initializers.cs:33:9:33:11 | enter Sub | Initializers.cs:33:9:33:11 | enter Sub |
|
||||
@@ -14866,7 +14868,7 @@ postBlockDominance
|
||||
| Initializers.cs:8:5:8:16 | enter Initializers | Initializers.cs:8:5:8:16 | enter Initializers |
|
||||
| Initializers.cs:10:5:10:16 | enter Initializers | Initializers.cs:10:5:10:16 | enter Initializers |
|
||||
| Initializers.cs:12:10:12:10 | enter M | Initializers.cs:12:10:12:10 | enter M |
|
||||
| Initializers.cs:18:20:18:20 | 1 | Initializers.cs:18:20:18:20 | 1 |
|
||||
| Initializers.cs:18:16:18:16 | enter H | Initializers.cs:18:16:18:16 | enter H |
|
||||
| Initializers.cs:20:11:20:23 | enter NoConstructor | Initializers.cs:20:11:20:23 | enter NoConstructor |
|
||||
| Initializers.cs:31:9:31:11 | enter Sub | Initializers.cs:31:9:31:11 | enter Sub |
|
||||
| Initializers.cs:33:9:33:11 | enter Sub | Initializers.cs:33:9:33:11 | enter Sub |
|
||||
|
||||
File diff suppressed because it is too large
Load Diff
@@ -1,11 +1,9 @@
|
||||
/**
|
||||
* @kind graph
|
||||
*/
|
||||
|
||||
import csharp
|
||||
import Common
|
||||
import semmle.code.csharp.controlflow.internal.ControlFlowGraphImplShared::TestOutput
|
||||
|
||||
query predicate edges(
|
||||
SourceControlFlowNode node, SourceControlFlowNode successor, string attr, string val
|
||||
) {
|
||||
exists(ControlFlow::SuccessorType t | successor = node.getASuccessorByType(t) |
|
||||
attr = "semmle.label" and
|
||||
val = t.toString()
|
||||
)
|
||||
}
|
||||
private class MyRelevantNode extends RelevantNode, SourceControlFlowNode { }
|
||||
|
||||
Reference in New Issue
Block a user