mirror of
https://github.com/github/codeql.git
synced 2026-04-27 09:45:15 +02:00
Merge pull request #271 from github/hvitved/cfg/shared
Adopt shared CFG library
This commit is contained in:
4
Makefile
4
Makefile
@@ -65,3 +65,7 @@ extractor: $(FILES) $(BIN_FILES)
|
||||
cp ql/lib/ruby.dbscheme extractor-pack/ruby.dbscheme
|
||||
cp target/release/ruby-extractor$(EXE) extractor-pack/tools/$(CODEQL_PLATFORM)/extractor$(EXE)
|
||||
cp target/release/ruby-autobuilder$(EXE) extractor-pack/tools/$(CODEQL_PLATFORM)/autobuilder$(EXE)
|
||||
|
||||
test: extractor dbscheme
|
||||
codeql pack install ql/test
|
||||
codeql test run --check-databases --check-unused-labels --check-repeated-labels --check-redefined-labels --check-use-before-definition --search-path . --consistency-queries ql/consistency-queries ql/test
|
||||
|
||||
2
codeql
2
codeql
Submodule codeql updated: d282f6a356...c8a5397085
@@ -1 +1 @@
|
||||
import codeql.ruby.controlflow.internal.Consistency
|
||||
import codeql.ruby.controlflow.internal.ControlFlowGraphImplShared::Consistency
|
||||
|
||||
@@ -62,11 +62,11 @@ class ExitNode extends CfgNode, TExitNode {
|
||||
* (dead) code or not important for control flow, and multiple when there are different
|
||||
* splits for the AST node.
|
||||
*/
|
||||
class AstCfgNode extends CfgNode, TAstCfgNode {
|
||||
class AstCfgNode extends CfgNode, TElementNode {
|
||||
private Splits splits;
|
||||
private AstNode n;
|
||||
|
||||
AstCfgNode() { this = TAstCfgNode(n, splits) }
|
||||
AstCfgNode() { this = TElementNode(n, splits) }
|
||||
|
||||
final override AstNode getNode() { result = n }
|
||||
|
||||
|
||||
@@ -29,7 +29,7 @@ class CfgScope extends Scope {
|
||||
*
|
||||
* Only nodes that can be reached from an entry point are included in the CFG.
|
||||
*/
|
||||
class CfgNode extends TCfgNode {
|
||||
class CfgNode extends TNode {
|
||||
/** Gets a textual representation of this control flow node. */
|
||||
string toString() { none() }
|
||||
|
||||
|
||||
@@ -1,32 +0,0 @@
|
||||
/**
|
||||
* Import this module into a `.ql` file of `@kind graph` to render a CFG. The
|
||||
* graph is restricted to nodes from `RelevantCfgNode`.
|
||||
*/
|
||||
|
||||
private import codeql.Locations
|
||||
import codeql.ruby.CFG
|
||||
|
||||
abstract class RelevantCfgNode extends CfgNode { }
|
||||
|
||||
query predicate nodes(RelevantCfgNode n, string attr, string val) {
|
||||
attr = "semmle.order" and
|
||||
val =
|
||||
any(int i |
|
||||
n =
|
||||
rank[i](RelevantCfgNode p, Location l |
|
||||
l = p.getLocation()
|
||||
|
|
||||
p
|
||||
order by
|
||||
l.getFile().getBaseName(), l.getFile().getAbsolutePath(), l.getStartLine(),
|
||||
l.getStartColumn()
|
||||
)
|
||||
).toString()
|
||||
}
|
||||
|
||||
query predicate edges(RelevantCfgNode pred, RelevantCfgNode succ, string attr, string val) {
|
||||
exists(SuccessorType t | succ = pred.getASuccessor(t) |
|
||||
attr = "semmle.label" and
|
||||
if t instanceof SuccessorTypes::NormalSuccessor then val = "" else val = t.toString()
|
||||
)
|
||||
}
|
||||
@@ -1,53 +0,0 @@
|
||||
private import codeql.ruby.AST
|
||||
private import codeql.ruby.CFG
|
||||
private import Completion
|
||||
private import Splitting
|
||||
|
||||
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(
|
||||
AstNode pred, Splits predSplits, AstNode 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(
|
||||
AstNode pred, Splits predSplits, AstNode 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(
|
||||
AstNode pred, Splits predSplits, AstNode 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(
|
||||
AstNode pred, Splits predSplits, AstNode 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(CfgNode node, SuccessorType t, CfgNode successor) {
|
||||
not node instanceof CfgNodes::EntryNode and
|
||||
strictcount(node.getASuccessor(t)) > 1 and
|
||||
successor = node.getASuccessor(t)
|
||||
}
|
||||
@@ -35,13 +35,11 @@ private import codeql.ruby.AST
|
||||
private import codeql.ruby.ast.internal.AST as ASTInternal
|
||||
private import codeql.ruby.ast.internal.Scope
|
||||
private import codeql.ruby.ast.Scope
|
||||
private import codeql.ruby.ast.internal.Synthesis
|
||||
private import codeql.ruby.ast.internal.TreeSitter
|
||||
private import codeql.ruby.ast.internal.Variable
|
||||
private import codeql.ruby.controlflow.ControlFlowGraph
|
||||
private import Completion
|
||||
private import SuccessorTypes
|
||||
private import Splitting
|
||||
import ControlFlowGraphImplShared
|
||||
|
||||
module CfgScope {
|
||||
abstract class Range_ extends AstNode {
|
||||
@@ -85,59 +83,6 @@ module CfgScope {
|
||||
}
|
||||
}
|
||||
|
||||
abstract private class ControlFlowTree extends AstNode {
|
||||
ControlFlowTree() { not any(Synthesis s).excludeFromControlFlowTree(this) }
|
||||
|
||||
/**
|
||||
* Holds if `first` is the first element executed within this AST node.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
abstract predicate first(AstNode first);
|
||||
|
||||
/**
|
||||
* Holds if `last` with completion `c` is a potential last element executed
|
||||
* within this AST node.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
abstract predicate last(AstNode last, Completion c);
|
||||
|
||||
/** Holds if abnormal execution of `child` should propagate upwards. */
|
||||
abstract predicate propagatesAbnormal(AstNode child);
|
||||
|
||||
/**
|
||||
* Holds if `succ` is a control flow successor for `pred`, given that `pred`
|
||||
* finishes with completion `c`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
abstract predicate succ(AstNode pred, AstNode succ, Completion c);
|
||||
}
|
||||
|
||||
/** Holds if `first` is the first element executed within AST node `n`. */
|
||||
predicate first(ControlFlowTree n, AstNode first) { n.first(first) }
|
||||
|
||||
/**
|
||||
* Holds if `last` with completion `c` is a potential last element executed
|
||||
* within AST node `n`.
|
||||
*/
|
||||
predicate last(ControlFlowTree n, AstNode last, Completion c) {
|
||||
n.last(last, c)
|
||||
or
|
||||
exists(AstNode child |
|
||||
n.propagatesAbnormal(child) and
|
||||
last(child, 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(AstNode pred, AstNode succ, Completion c) {
|
||||
any(ControlFlowTree cft).succ(pred, succ, c)
|
||||
}
|
||||
|
||||
/** Holds if `first` is first executed when entering `scope`. */
|
||||
pragma[nomagic]
|
||||
predicate succEntry(CfgScope::Range_ scope, AstNode first) { scope.entry(first) }
|
||||
@@ -146,47 +91,6 @@ predicate succEntry(CfgScope::Range_ scope, AstNode first) { scope.entry(first)
|
||||
pragma[nomagic]
|
||||
predicate succExit(CfgScope::Range_ scope, AstNode last, Completion c) { scope.exit(last, c) }
|
||||
|
||||
/**
|
||||
* An AST node where the children are evaluated following a standard left-to-right
|
||||
* evaluation. The actual evaluation order is determined by the predicate
|
||||
* `getChildNode()`.
|
||||
*/
|
||||
abstract private class StandardTree extends ControlFlowTree {
|
||||
/** Gets the `i`th child node, in order of evaluation. */
|
||||
abstract ControlFlowTree getChildNode(int i);
|
||||
|
||||
private ControlFlowTree getChildNodeRanked(int i) {
|
||||
result =
|
||||
rank[i + 1](ControlFlowTree child, int j | child = this.getChildNode(j) | child order by j)
|
||||
}
|
||||
|
||||
/** Gets the first child node of this element. */
|
||||
final AstNode getFirstChildNode() { result = this.getChildNodeRanked(0) }
|
||||
|
||||
/** Gets the last child node of this node. */
|
||||
final AstNode getLastChildNode() {
|
||||
exists(int last |
|
||||
result = this.getChildNodeRanked(last) and
|
||||
not exists(this.getChildNodeRanked(last + 1))
|
||||
)
|
||||
}
|
||||
|
||||
override predicate propagatesAbnormal(AstNode child) { child = this.getChildNode(_) }
|
||||
|
||||
pragma[nomagic]
|
||||
override predicate succ(AstNode pred, AstNode succ, Completion c) {
|
||||
exists(int i |
|
||||
last(this.getChildNodeRanked(i), pred, c) and
|
||||
c instanceof NormalCompletion and
|
||||
first(this.getChildNodeRanked(i + 1), succ)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
abstract private class PreOrderTree extends ControlFlowTree {
|
||||
final override predicate first(AstNode first) { first = this }
|
||||
}
|
||||
|
||||
// TODO: remove this class; it should be replaced with an implicit non AST node
|
||||
private class ForIn extends AstNode, ASTInternal::TForIn {
|
||||
final override string toString() { result = "In" }
|
||||
@@ -206,66 +110,10 @@ private class ForRange extends ForExpr {
|
||||
}
|
||||
}
|
||||
|
||||
abstract private class StandardPreOrderTree extends StandardTree, PreOrderTree {
|
||||
final override predicate last(AstNode last, Completion c) {
|
||||
last(this.getLastChildNode(), last, c)
|
||||
or
|
||||
not exists(this.getLastChildNode()) and
|
||||
c.isValidFor(this) and
|
||||
last = this
|
||||
}
|
||||
|
||||
final override predicate succ(AstNode pred, AstNode succ, Completion c) {
|
||||
StandardTree.super.succ(pred, succ, c)
|
||||
or
|
||||
pred = this and
|
||||
first(this.getFirstChildNode(), succ) and
|
||||
c instanceof SimpleCompletion
|
||||
}
|
||||
}
|
||||
|
||||
abstract private class PostOrderTree extends ControlFlowTree {
|
||||
override predicate last(AstNode last, Completion c) {
|
||||
last = this and
|
||||
c.isValidFor(last)
|
||||
}
|
||||
}
|
||||
|
||||
abstract private class StandardPostOrderTree extends StandardTree, PostOrderTree {
|
||||
final override predicate first(AstNode first) {
|
||||
first(this.getFirstChildNode(), first)
|
||||
or
|
||||
not exists(this.getFirstChildNode()) and
|
||||
first = this
|
||||
}
|
||||
|
||||
final override predicate succ(AstNode pred, AstNode succ, Completion c) {
|
||||
StandardTree.super.succ(pred, succ, c)
|
||||
or
|
||||
last(this.getLastChildNode(), pred, c) and
|
||||
succ = this and
|
||||
c instanceof NormalCompletion
|
||||
}
|
||||
}
|
||||
|
||||
abstract private class LeafTree extends PreOrderTree, PostOrderTree {
|
||||
override predicate propagatesAbnormal(AstNode child) { none() }
|
||||
|
||||
override predicate succ(AstNode pred, AstNode succ, Completion c) { none() }
|
||||
}
|
||||
|
||||
abstract class ScopeTree extends StandardTree, LeafTree {
|
||||
final override predicate propagatesAbnormal(AstNode child) { none() }
|
||||
|
||||
final override predicate succ(AstNode pred, AstNode succ, Completion c) {
|
||||
StandardTree.super.succ(pred, succ, c)
|
||||
}
|
||||
}
|
||||
|
||||
/** Defines the CFG by dispatch on the various AST types. */
|
||||
module Trees {
|
||||
private class AliasStmtTree extends StandardPreOrderTree, AliasStmt {
|
||||
final override ControlFlowTree getChildNode(int i) {
|
||||
final override ControlFlowTree getChildElement(int i) {
|
||||
result = this.getNewName() and i = 0
|
||||
or
|
||||
result = this.getOldName() and i = 1
|
||||
@@ -273,17 +121,17 @@ module Trees {
|
||||
}
|
||||
|
||||
private class ArgumentListTree extends StandardTree, ArgumentList {
|
||||
final override ControlFlowTree getChildNode(int i) { result = this.getElement(i) }
|
||||
final override ControlFlowTree getChildElement(int i) { result = this.getElement(i) }
|
||||
|
||||
final override predicate first(AstNode first) { first(this.getFirstChildNode(), first) }
|
||||
final override predicate first(AstNode first) { first(this.getFirstChildElement(), first) }
|
||||
|
||||
final override predicate last(AstNode last, Completion c) {
|
||||
last(this.getLastChildNode(), last, c)
|
||||
last(this.getLastChildElement(), last, c)
|
||||
}
|
||||
}
|
||||
|
||||
private class ArrayLiteralTree extends StandardPostOrderTree, ArrayLiteral {
|
||||
final override ControlFlowTree getChildNode(int i) { result = this.getElement(i) }
|
||||
final override ControlFlowTree getChildElement(int i) { result = this.getElement(i) }
|
||||
}
|
||||
|
||||
private class AssignExprTree extends StandardPostOrderTree, AssignExpr {
|
||||
@@ -294,7 +142,7 @@ module Trees {
|
||||
)
|
||||
}
|
||||
|
||||
final override ControlFlowTree getChildNode(int i) {
|
||||
final override ControlFlowTree getChildElement(int i) {
|
||||
result = this.getLeftOperand() and i = 0
|
||||
or
|
||||
result = this.getRightOperand() and i = 1
|
||||
@@ -313,7 +161,7 @@ module Trees {
|
||||
// Logical AND and OR are handled separately
|
||||
BinaryOperationTree() { not this instanceof BinaryLogicalOperation }
|
||||
|
||||
final override ControlFlowTree getChildNode(int i) {
|
||||
final override ControlFlowTree getChildElement(int i) {
|
||||
result = this.getLeftOperand() and i = 0
|
||||
or
|
||||
result = this.getRightOperand() and i = 1
|
||||
@@ -321,7 +169,7 @@ module Trees {
|
||||
}
|
||||
|
||||
private class BlockArgumentTree extends StandardPostOrderTree, BlockArgument {
|
||||
final override ControlFlowTree getChildNode(int i) { result = this.getValue() and i = 0 }
|
||||
final override ControlFlowTree getChildElement(int i) { result = this.getValue() and i = 0 }
|
||||
}
|
||||
|
||||
abstract private class NonDefaultValueParameterTree extends ControlFlowTree, NamedParameter {
|
||||
@@ -549,7 +397,7 @@ module Trees {
|
||||
}
|
||||
|
||||
private class CallTree extends StandardPostOrderTree, Call {
|
||||
override ControlFlowTree getChildNode(int i) { result = this.getArgument(i) }
|
||||
override ControlFlowTree getChildElement(int i) { result = this.getArgument(i) }
|
||||
}
|
||||
|
||||
private class CaseTree extends PreOrderTree, CaseExpr {
|
||||
@@ -855,13 +703,13 @@ module Trees {
|
||||
private class GlobalVariableTree extends LeafTree, GlobalVariableAccess { }
|
||||
|
||||
private class HashLiteralTree extends StandardPostOrderTree, HashLiteral {
|
||||
final override ControlFlowTree getChildNode(int i) { result = this.getElement(i) }
|
||||
final override ControlFlowTree getChildElement(int i) { result = this.getElement(i) }
|
||||
}
|
||||
|
||||
private class HashSplatParameterTree extends NonDefaultValueParameterTree, HashSplatParameter { }
|
||||
|
||||
private class HereDocTree extends StandardPreOrderTree, HereDoc {
|
||||
final override ControlFlowTree getChildNode(int i) { result = this.getComponent(i) }
|
||||
final override ControlFlowTree getChildElement(int i) { result = this.getComponent(i) }
|
||||
}
|
||||
|
||||
private class InstanceVariableTree extends LeafTree, InstanceVariableAccess { }
|
||||
@@ -938,7 +786,7 @@ module Trees {
|
||||
}
|
||||
|
||||
private class MethodCallTree extends CallTree, MethodCall {
|
||||
final override ControlFlowTree getChildNode(int i) {
|
||||
final override ControlFlowTree getChildElement(int i) {
|
||||
result = this.getReceiver() and i = 0
|
||||
or
|
||||
result = this.getArgument(i - 1)
|
||||
@@ -996,7 +844,7 @@ module Trees {
|
||||
}
|
||||
|
||||
private class PairTree extends StandardPostOrderTree, Pair {
|
||||
final override ControlFlowTree getChildNode(int i) {
|
||||
final override ControlFlowTree getChildElement(int i) {
|
||||
result = this.getKey() and i = 0
|
||||
or
|
||||
result = this.getValue() and i = 1
|
||||
@@ -1004,7 +852,7 @@ module Trees {
|
||||
}
|
||||
|
||||
private class RangeLiteralTree extends StandardPostOrderTree, RangeLiteral {
|
||||
final override ControlFlowTree getChildNode(int i) {
|
||||
final override ControlFlowTree getChildElement(int i) {
|
||||
result = this.getBegin() and i = 0
|
||||
or
|
||||
result = this.getEnd() and i = 1
|
||||
@@ -1114,7 +962,7 @@ module Trees {
|
||||
private class RetryStmtTree extends LeafTree, RetryStmt { }
|
||||
|
||||
private class ReturningStmtTree extends StandardPostOrderTree, ReturningStmt {
|
||||
final override ControlFlowTree getChildNode(int i) { result = this.getValue() and i = 0 }
|
||||
final override ControlFlowTree getChildElement(int i) { result = this.getValue() and i = 0 }
|
||||
}
|
||||
|
||||
private class SelfTree extends LeafTree, Self { }
|
||||
@@ -1208,19 +1056,19 @@ module Trees {
|
||||
}
|
||||
|
||||
private class StringConcatenationTree extends StandardTree, StringConcatenation {
|
||||
final override ControlFlowTree getChildNode(int i) { result = this.getString(i) }
|
||||
final override ControlFlowTree getChildElement(int i) { result = this.getString(i) }
|
||||
|
||||
final override predicate first(AstNode first) { first(this.getFirstChildNode(), first) }
|
||||
final override predicate first(AstNode first) { first(this.getFirstChildElement(), first) }
|
||||
|
||||
final override predicate last(AstNode last, Completion c) {
|
||||
last(this.getLastChildNode(), last, c)
|
||||
last(this.getLastChildElement(), last, c)
|
||||
}
|
||||
}
|
||||
|
||||
private class StringlikeLiteralTree extends StandardPostOrderTree, StringlikeLiteral {
|
||||
StringlikeLiteralTree() { not this instanceof HereDoc }
|
||||
|
||||
final override ControlFlowTree getChildNode(int i) { result = this.getComponent(i) }
|
||||
final override ControlFlowTree getChildElement(int i) { result = this.getComponent(i) }
|
||||
}
|
||||
|
||||
private class ToplevelTree extends BodyStmtTree, Toplevel {
|
||||
@@ -1240,18 +1088,18 @@ module Trees {
|
||||
}
|
||||
|
||||
private class TuplePatternTree extends StandardPostOrderTree, TuplePattern {
|
||||
final override ControlFlowTree getChildNode(int i) { result = this.getElement(i) }
|
||||
final override ControlFlowTree getChildElement(int i) { result = this.getElement(i) }
|
||||
}
|
||||
|
||||
private class UnaryOperationTree extends StandardPostOrderTree, UnaryOperation {
|
||||
// Logical NOT is handled separately
|
||||
UnaryOperationTree() { not this instanceof NotExpr }
|
||||
|
||||
final override ControlFlowTree getChildNode(int i) { result = this.getOperand() and i = 0 }
|
||||
final override ControlFlowTree getChildElement(int i) { result = this.getOperand() and i = 0 }
|
||||
}
|
||||
|
||||
private class UndefStmtTree extends StandardPreOrderTree, UndefStmt {
|
||||
final override ControlFlowTree getChildNode(int i) { result = this.getMethodName(i) }
|
||||
final override ControlFlowTree getChildElement(int i) { result = this.getMethodName(i) }
|
||||
}
|
||||
|
||||
private class WhenTree extends PreOrderTree, WhenExpr {
|
||||
@@ -1310,31 +1158,10 @@ private module Cached {
|
||||
/** Gets the CFG scope of node `n`. */
|
||||
cached
|
||||
CfgScope getCfgScopeImpl(AstNode n) {
|
||||
forceCachingInSameStage() and
|
||||
result = parent*(ASTInternal::fromGenerated(scopeOf(ASTInternal::toGeneratedInclSynth(n))))
|
||||
}
|
||||
|
||||
private predicate isAbnormalExitType(SuccessorType t) {
|
||||
t instanceof RaiseSuccessor or t instanceof ExitSuccessor
|
||||
}
|
||||
|
||||
cached
|
||||
newtype TCfgNode =
|
||||
TEntryNode(CfgScope scope) { succEntrySplits(scope, _, _, _) } or
|
||||
TAnnotatedExitNode(CfgScope scope, boolean normal) {
|
||||
exists(Reachability::SameSplitsBlock b, SuccessorType t | b.isReachable(_) |
|
||||
succExitSplits(b.getANode(), _, scope, t) and
|
||||
if isAbnormalExitType(t) then normal = false else normal = true
|
||||
)
|
||||
} or
|
||||
TExitNode(CfgScope scope) {
|
||||
exists(Reachability::SameSplitsBlock b | b.isReachable(_) |
|
||||
succExitSplits(b.getANode(), _, scope, _)
|
||||
)
|
||||
} or
|
||||
TAstCfgNode(AstNode n, Splits splits) {
|
||||
exists(Reachability::SameSplitsBlock b | b.isReachable(splits) | n = b.getANode())
|
||||
}
|
||||
|
||||
cached
|
||||
newtype TSuccessorType =
|
||||
TSuccessorSuccessor() or
|
||||
@@ -1348,49 +1175,6 @@ private module Cached {
|
||||
TRetrySuccessor() or
|
||||
TRaiseSuccessor() or // TODO: Add exception type?
|
||||
TExitSuccessor()
|
||||
|
||||
/** Gets a successor node of a given flow type, if any. */
|
||||
cached
|
||||
CfgNode getASuccessor(CfgNode pred, SuccessorType t) {
|
||||
exists(CfgScope scope, AstNode succElement, Splits succSplits |
|
||||
pred = TEntryNode(scope) and
|
||||
succEntrySplits(scope, succElement, succSplits, t) and
|
||||
result = TAstCfgNode(succElement, succSplits)
|
||||
)
|
||||
or
|
||||
exists(AstNode predNode, Splits predSplits | pred = TAstCfgNode(predNode, predSplits) |
|
||||
exists(CfgScope scope, boolean normal |
|
||||
succExitSplits(predNode, predSplits, scope, t) and
|
||||
(if isAbnormalExitType(t) then normal = false else normal = true) and
|
||||
result = TAnnotatedExitNode(scope, normal)
|
||||
)
|
||||
or
|
||||
exists(AstNode succElement, Splits succSplits, Completion c |
|
||||
succSplits(predNode, predSplits, succElement, succSplits, c) and
|
||||
t = c.getAMatchingSuccessorType() and
|
||||
result = TAstCfgNode(succElement, succSplits)
|
||||
)
|
||||
)
|
||||
or
|
||||
exists(CfgScope scope |
|
||||
pred = TAnnotatedExitNode(scope, _) and
|
||||
t instanceof SuccessorTypes::NormalSuccessor and
|
||||
result = TExitNode(scope)
|
||||
)
|
||||
}
|
||||
|
||||
/** Gets a first control flow element executed within `n`. */
|
||||
cached
|
||||
AstNode getAControlFlowEntryNode(AstNode n) { first(n, result) }
|
||||
|
||||
/** Gets a potential last control flow element executed within `n`. */
|
||||
cached
|
||||
AstNode getAControlFlowExitNode(AstNode n) { last(n, result, _) }
|
||||
}
|
||||
|
||||
import Cached
|
||||
|
||||
/** An AST node that is split into multiple control flow nodes. */
|
||||
class SplitAstNode extends AstNode {
|
||||
SplitAstNode() { strictcount(CfgNode n | n.getNode() = this) > 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,74 @@
|
||||
private import ruby as rb
|
||||
private import ControlFlowGraphImpl as Impl
|
||||
private import Completion as Comp
|
||||
private import codeql.ruby.ast.internal.Synthesis
|
||||
private import Splitting as Splitting
|
||||
private import codeql.ruby.CFG as CFG
|
||||
|
||||
/** The base class for `ControlFlowTree`. */
|
||||
class ControlFlowTreeBase extends rb::AstNode {
|
||||
ControlFlowTreeBase() { not any(Synthesis s).excludeFromControlFlowTree(this) }
|
||||
}
|
||||
|
||||
class ControlFlowElement = rb::AstNode;
|
||||
|
||||
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 = CFG::CfgScope;
|
||||
|
||||
predicate getCfgScope = Impl::getCfgScope/1;
|
||||
|
||||
/** Holds if `first` is first executed when entering `scope`. */
|
||||
predicate scopeFirst(CfgScope scope, ControlFlowElement first) {
|
||||
scope.(Impl::CfgScope::Range_).entry(first)
|
||||
}
|
||||
|
||||
/** Holds if `scope` is exited when `last` finishes with completion `c`. */
|
||||
predicate scopeLast(CfgScope scope, ControlFlowElement last, Completion c) {
|
||||
scope.(Impl::CfgScope::Range_).exit(last, c)
|
||||
}
|
||||
|
||||
/** The maximum number of splits allowed for a given node. */
|
||||
int maxSplits() { result = 5 }
|
||||
|
||||
class SplitKindBase = Splitting::TSplitKind;
|
||||
|
||||
class Split = Splitting::Split;
|
||||
|
||||
class SuccessorType = CFG::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 CFG::SuccessorTypes::NormalSuccessor
|
||||
}
|
||||
|
||||
/** Holds if `t` is an abnormal exit type out of a CFG scope. */
|
||||
predicate isAbnormalExitType(SuccessorType t) {
|
||||
t instanceof CFG::SuccessorTypes::RaiseSuccessor or
|
||||
t instanceof CFG::SuccessorTypes::ExitSuccessor
|
||||
}
|
||||
|
||||
class Location = rb::Location;
|
||||
|
||||
class Node = CFG::CfgNode;
|
||||
@@ -8,14 +8,11 @@ private import ControlFlowGraphImpl
|
||||
private import SuccessorTypes
|
||||
private import codeql.ruby.controlflow.ControlFlowGraph
|
||||
|
||||
/** The maximum number of splits allowed for a given node. */
|
||||
private int maxSplits() { result = 5 }
|
||||
|
||||
cached
|
||||
private module Cached {
|
||||
cached
|
||||
newtype TSplitKind =
|
||||
TConditionalCompletionSplitKind() or
|
||||
TConditionalCompletionSplitKind() { forceCachingInSameStage() } or
|
||||
TEnsureSplitKind(int nestLevel) { nestLevel = any(Trees::BodyStmtTree t).getNestLevel() }
|
||||
|
||||
cached
|
||||
@@ -24,40 +21,9 @@ private module Cached {
|
||||
TEnsureSplit(EnsureSplitting::EnsureSplitType type, int nestLevel) {
|
||||
nestLevel = any(Trees::BodyStmtTree t).getNestLevel()
|
||||
}
|
||||
|
||||
cached
|
||||
newtype TSplits =
|
||||
TSplitsNil() or
|
||||
TSplitsCons(SplitImpl head, Splits tail) {
|
||||
exists(AstNode pred, Splits predSplits, AstNode 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 node. */
|
||||
class Split extends TSplit {
|
||||
@@ -65,118 +31,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 AST node inside `scope`.
|
||||
*/
|
||||
private predicate overlapping(CfgScope scope, SplitKind sk1, SplitKind sk2) {
|
||||
exists(AstNode n |
|
||||
sk1.appliesTo(n) and
|
||||
sk2.appliesTo(n) and
|
||||
scope = getCfgScope(n)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* A split kind. Each control flow node can have at most one split of a
|
||||
* given kind.
|
||||
*/
|
||||
abstract private class SplitKind extends TSplitKind {
|
||||
/** 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(AstNode 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(AstNode 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(AstNode 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();
|
||||
}
|
||||
|
||||
// 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(AstNode pred, AstNode succ, Completion c);
|
||||
|
||||
/**
|
||||
* Holds if this split is entered when control passes from `scope` to the entry point
|
||||
* `first`.
|
||||
*
|
||||
* Invariant: `hasEntryScope(scope, first) implies succEntry(scope, first)`.
|
||||
*/
|
||||
abstract predicate hasEntryScope(CfgScope scope, AstNode 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(AstNode pred, AstNode 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 succExit(scope, last, c)`
|
||||
*/
|
||||
abstract predicate hasExitScope(CfgScope scope, AstNode 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(AstNode pred, AstNode succ, Completion c);
|
||||
|
||||
/** Holds if this split applies to AST node `n`. */
|
||||
final predicate appliesTo(AstNode n) {
|
||||
this.hasEntry(_, n, _)
|
||||
or
|
||||
this.hasEntryScope(_, n)
|
||||
or
|
||||
exists(AstNode pred | this.appliesTo(pred) | this.hasSuccessor(pred, n, _))
|
||||
}
|
||||
}
|
||||
|
||||
private module ConditionalCompletionSplitting {
|
||||
/**
|
||||
* A split for conditional completions. For example, in
|
||||
@@ -480,446 +334,3 @@ module EnsureSplitting {
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* 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, AstNode succ, Splits splits, int rnk) {
|
||||
splits = TSplitsNil() and
|
||||
succEntry(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, AstNode 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 scope `pred`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
predicate succEntrySplits(CfgScope pred, AstNode succ, Splits succSplits, SuccessorType t) {
|
||||
exists(int rnk |
|
||||
succEntry(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 `last` with splits `predSplits` can exit the enclosing scope
|
||||
* `scope` with type `t`.
|
||||
*/
|
||||
predicate succExitSplits(AstNode last, Splits predSplits, CfgScope scope, SuccessorType t) {
|
||||
exists(Reachability::SameSplitsBlock b, Completion c | last = b.getANode() |
|
||||
b.isReachable(predSplits) and
|
||||
t = c.getAMatchingSuccessorType() and
|
||||
succExit(scope, last, c) and
|
||||
forall(SplitImpl predSplit | predSplit = predSplits.getASplit() |
|
||||
predSplit.hasExitScope(scope, last, 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(AstNode pred, Splits predSplits, AstNode 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, AstNode pred, Splits predSplits, AstNode succ, Completion c
|
||||
) {
|
||||
pred = b.getANode() and
|
||||
b.isReachable(predSplits) and
|
||||
succ(pred, succ, c)
|
||||
}
|
||||
|
||||
private predicate case1b0(AstNode pred, Splits predSplits, AstNode succ, Completion c) {
|
||||
exists(Reachability::SameSplitsBlock b |
|
||||
// Invariant 1
|
||||
succInvariant1(b, pred, predSplits, succ, c)
|
||||
|
|
||||
(succ = b.getANode() 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(
|
||||
AstNode pred, Splits predSplits, AstNode 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(
|
||||
AstNode pred, Splits predSplits, AstNode succ, Completion c, SplitImpl exceptHead,
|
||||
Splits exceptTail
|
||||
) {
|
||||
case1bForall(pred, predSplits, succ, c, TSplitsCons(exceptHead, exceptTail))
|
||||
}
|
||||
|
||||
private predicate case1(AstNode pred, Splits predSplits, AstNode succ, Completion c) {
|
||||
// Case 1a
|
||||
exists(Reachability::SameSplitsBlock b | succInvariant1(b, pred, predSplits, succ, c) |
|
||||
succ = b.getANode() and
|
||||
not succ = b
|
||||
)
|
||||
or
|
||||
// Case 1b
|
||||
case1bForall(pred, predSplits, succ, c, TSplitsNil())
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private SplitImpl succInvariant1GetASplit(
|
||||
Reachability::SameSplitsBlock b, AstNode pred, Splits predSplits, AstNode succ, Completion c
|
||||
) {
|
||||
succInvariant1(b, pred, predSplits, succ, c) and
|
||||
result = predSplits.getASplit()
|
||||
}
|
||||
|
||||
private predicate case2aux(AstNode pred, Splits predSplits, AstNode succ, Completion c) {
|
||||
exists(Reachability::SameSplitsBlock b |
|
||||
succInvariant1(b, pred, predSplits, succ, c) and
|
||||
(succ = b.getANode() 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(
|
||||
AstNode pred, Splits predSplits, AstNode 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(
|
||||
AstNode pred, AstNode 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(
|
||||
AstNode pred, Splits predSplits, AstNode 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(
|
||||
AstNode pred, Splits predSplits, AstNode succ, Completion c, int rnk
|
||||
) {
|
||||
exists(SplitKind sk | case2aNoneOfKind(pred, predSplits, succ, c, sk) |
|
||||
rnk = sk.getListRank(succ)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private SplitImpl case2auxGetAPredecessorSplit(
|
||||
AstNode pred, Splits predSplits, AstNode 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(
|
||||
AstNode pred, Splits predSplits, AstNode 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(AstNode pred, Splits predSplits, AstNode 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(
|
||||
AstNode pred, Splits predSplits, AstNode 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(
|
||||
AstNode pred, Splits predSplits, AstNode 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(
|
||||
AstNode pred, Splits predSplits, AstNode 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(
|
||||
AstNode pred, Splits predSplits, AstNode succ, Completion c, SplitImpl exceptHead,
|
||||
Splits exceptTail
|
||||
) {
|
||||
case2bForall(pred, predSplits, succ, c, TSplitsCons(exceptHead, exceptTail))
|
||||
}
|
||||
|
||||
private predicate case2(
|
||||
AstNode pred, Splits predSplits, AstNode 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(
|
||||
AstNode pred, Splits predSplits, AstNode 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 `n` is an AST node where the set of possible splits may be different
|
||||
* from the set of possible splits for one of `n`'s predecessors. That is, `n`
|
||||
* starts a new block of elements with the same set of splits.
|
||||
*/
|
||||
private predicate startsSplits(AstNode n) {
|
||||
succEntry(_, n)
|
||||
or
|
||||
exists(SplitImpl s |
|
||||
s.hasEntry(_, n, _)
|
||||
or
|
||||
s.hasExit(_, n, _)
|
||||
)
|
||||
or
|
||||
exists(AstNode pred, SplitImpl split, Completion c | succ(pred, n, c) |
|
||||
split.appliesTo(pred) and
|
||||
not split.hasSuccessor(pred, n, c)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate intraSplitsSucc(AstNode pred, AstNode succ) {
|
||||
succ(pred, succ, _) and
|
||||
not startsSplits(succ)
|
||||
}
|
||||
|
||||
private predicate splitsBlockContains(AstNode start, AstNode n) =
|
||||
fastTC(intraSplitsSucc/2)(start, n)
|
||||
|
||||
/**
|
||||
* A block of AST nodes where the set of splits is guaranteed to remain unchanged,
|
||||
* represented by the first element in the block.
|
||||
*/
|
||||
class SameSplitsBlock extends AstNode {
|
||||
SameSplitsBlock() { startsSplits(this) }
|
||||
|
||||
/** Gets an AST node in this block. */
|
||||
AstNode getANode() {
|
||||
splitsBlockContains(this, result)
|
||||
or
|
||||
result = this
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private SameSplitsBlock getASuccessor(Splits predSplits, Splits succSplits) {
|
||||
exists(AstNode pred | pred = this.getANode() |
|
||||
succSplits(pred, predSplits, result, succSplits, _)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the elements of this block are reachable from an 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)
|
||||
)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
@@ -284,8 +284,7 @@ private module SsaDefReaches {
|
||||
predicate ssaDefReachesReadWithinBlock(SourceVariable v, Definition def, BasicBlock bb, int i) {
|
||||
exists(int rnk |
|
||||
ssaDefReachesRank(bb, def, rnk, v) and
|
||||
rnk = ssaRefRank(bb, i, v, SsaRead()) and
|
||||
variableRead(bb, i, v, _)
|
||||
rnk = ssaRefRank(bb, i, v, SsaRead())
|
||||
)
|
||||
}
|
||||
|
||||
|
||||
@@ -2,8 +2,9 @@
|
||||
* @kind graph
|
||||
*/
|
||||
|
||||
import codeql.ruby.controlflow.internal.Cfg
|
||||
import codeql.ruby.CFG
|
||||
import codeql.ruby.controlflow.internal.ControlFlowGraphImpl::TestOutput
|
||||
|
||||
class MyRelevantCfgNode extends RelevantCfgNode {
|
||||
MyRelevantCfgNode() { exists(this) }
|
||||
class MyRelevantNode extends RelevantNode {
|
||||
MyRelevantNode() { exists(this) }
|
||||
}
|
||||
|
||||
@@ -1,30 +1,34 @@
|
||||
{
|
||||
"SSA": [
|
||||
"codeql/csharp/ql/src/semmle/code/csharp/dataflow/internal/SsaImplCommon.qll",
|
||||
"codeql/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImplCommon.qll",
|
||||
"ql/lib/codeql/ruby/dataflow/internal/SsaImplCommon.qll"
|
||||
],
|
||||
"DataFlow Common": [
|
||||
"codeql/csharp/ql/src/semmle/code/csharp/dataflow/internal/DataFlowImplCommon.qll",
|
||||
"codeql/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImplCommon.qll",
|
||||
"ql/lib/codeql/ruby/dataflow/internal/DataFlowImplCommon.qll"
|
||||
],
|
||||
"DataFlow": [
|
||||
"codeql/csharp/ql/src/semmle/code/csharp/dataflow/internal/DataFlowImpl.qll",
|
||||
"codeql/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl.qll",
|
||||
"ql/lib/codeql/ruby/dataflow/internal/DataFlowImpl.qll"
|
||||
],
|
||||
"DataFlow Consistency": [
|
||||
"codeql/csharp/ql/src/semmle/code/csharp/dataflow/internal/DataFlowImplConsistency.qll",
|
||||
"codeql/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImplConsistency.qll",
|
||||
"ql/lib/codeql/ruby/dataflow/internal/DataFlowImplConsistency.qll"
|
||||
],
|
||||
"TaintTracking": [
|
||||
"codeql/csharp/ql/src/semmle/code/csharp/dataflow/internal/tainttracking1/TaintTrackingImpl.qll",
|
||||
"codeql/csharp/ql/lib/semmle/code/csharp/dataflow/internal/tainttracking1/TaintTrackingImpl.qll",
|
||||
"ql/lib/codeql/ruby/dataflow/internal/tainttracking1/TaintTrackingImpl.qll"
|
||||
],
|
||||
"TypeTracker": [
|
||||
"codeql/python/ql/src/semmle/python/dataflow/new/internal/TypeTracker.qll",
|
||||
"codeql/python/ql/lib/semmle/python/dataflow/new/internal/TypeTracker.qll",
|
||||
"ql/lib/codeql/ruby/typetracking/TypeTracker.qll"
|
||||
],
|
||||
"Inline Test Expectations": [
|
||||
"codeql/python/ql/test/TestUtilities/InlineExpectationsTest.qll",
|
||||
"ql/test/TestUtilities/InlineExpectationsTest.qll"
|
||||
]
|
||||
}
|
||||
"Inline Test Expectations": [
|
||||
"codeql/python/ql/test/TestUtilities/InlineExpectationsTest.qll",
|
||||
"ql/test/TestUtilities/InlineExpectationsTest.qll"
|
||||
],
|
||||
"CFG": [
|
||||
"codeql/csharp/ql/lib/semmle/code/csharp/controlflow/internal/ControlFlowGraphImplShared.qll",
|
||||
"ql/lib/codeql/ruby/controlflow/internal/ControlFlowGraphImplShared.qll"
|
||||
]
|
||||
}
|
||||
Reference in New Issue
Block a user