mirror of
https://github.com/github/codeql.git
synced 2025-12-16 16:53:25 +01:00
Initial CFG skeleton code
This commit is contained in:
Tom Hvitved
2
.github/workflows/qltest.yml
vendored
2
.github/workflows/qltest.yml
vendored
@@ -30,5 +30,5 @@ jobs:
|
||||
- name: Build Extractor
|
||||
run: env "PATH=$PATH:${{ github.workspace }}/codeql" ./create-extractor-pack.sh
|
||||
- name: Run QL tests
|
||||
run: codeql/codeql test run --search-path "${{ github.workspace }}" ql/test
|
||||
run: codeql/codeql test run --check-databases --check-unused-labels --search-path "${{ github.workspace }}" --consistency-queries ql/consistency-queries ql/test
|
||||
|
||||
|
||||
5
.gitignore
vendored
5
.gitignore
vendored
@@ -1,4 +1,7 @@
|
||||
/target
|
||||
extractor-pack
|
||||
.vscode/launch.json
|
||||
ql/src/.cache
|
||||
.cache
|
||||
ql/test/**/*.testproj
|
||||
ql/test/**/*.actual
|
||||
ql/test/**/CONSISTENCY
|
||||
|
||||
1
ql/consistency-queries/CfgConsistency.ql
Normal file
1
ql/consistency-queries/CfgConsistency.ql
Normal file
@@ -0,0 +1 @@
|
||||
import codeql_ruby.controlflow.internal.Consistency
|
||||
5
ql/consistency-queries/qlpack.yml
Normal file
5
ql/consistency-queries/qlpack.yml
Normal file
@@ -0,0 +1,5 @@
|
||||
name: codeql-ruby-consistency-queries
|
||||
version: 0.0.0
|
||||
libraryPathDependencies:
|
||||
- codeql-ruby
|
||||
extractor: ruby
|
||||
404
ql/src/codeql_ruby/controlflow/BasicBlocks.qll
Normal file
404
ql/src/codeql_ruby/controlflow/BasicBlocks.qll
Normal file
@@ -0,0 +1,404 @@
|
||||
/** Provides classes representing basic blocks. */
|
||||
|
||||
import codeql_ruby.ast
|
||||
private import codeql_ruby.controlflow.ControlFlowGraph
|
||||
private import internal.ControlFlowGraphImpl
|
||||
private import SuccessorTypes
|
||||
|
||||
/**
|
||||
* A basic block, that is, a maximal straight-line sequence of control flow nodes
|
||||
* without branches or joins.
|
||||
*/
|
||||
class BasicBlock extends TBasicBlockStart {
|
||||
/** Gets the scope of this basic block. */
|
||||
CfgScope getScope() { result = this.getAPredecessor().getScope() }
|
||||
|
||||
/** Gets an immediate successor of this basic block, if any. */
|
||||
BasicBlock getASuccessor() { result = this.getASuccessor(_) }
|
||||
|
||||
/** Gets an immediate successor of this basic block of a given type, if any. */
|
||||
BasicBlock getASuccessor(SuccessorType t) {
|
||||
result.getFirstNode() = this.getLastNode().getASuccessor(t)
|
||||
}
|
||||
|
||||
/** Gets an immediate predecessor of this basic block, if any. */
|
||||
BasicBlock getAPredecessor() { result.getASuccessor() = this }
|
||||
|
||||
/** Gets an immediate predecessor of this basic block of a given type, if any. */
|
||||
BasicBlock getAPredecessor(SuccessorType t) { result.getASuccessor(t) = this }
|
||||
|
||||
/** Gets the control flow node at a specific (zero-indexed) position in this basic block. */
|
||||
CfgNode getNode(int pos) { bbIndex(this.getFirstNode(), result, pos) }
|
||||
|
||||
/** Gets a control flow node in this basic block. */
|
||||
CfgNode getANode() { result = this.getNode(_) }
|
||||
|
||||
/** Gets the first control flow node in this basic block. */
|
||||
CfgNode getFirstNode() { this = TBasicBlockStart(result) }
|
||||
|
||||
/** Gets the last control flow node in this basic block. */
|
||||
CfgNode getLastNode() { result = this.getNode(this.length() - 1) }
|
||||
|
||||
/** Gets the length of this basic block. */
|
||||
int length() { result = strictcount(this.getANode()) }
|
||||
|
||||
/**
|
||||
* Holds if this basic block immediately dominates basic block `bb`.
|
||||
*
|
||||
* That is, all paths reaching basic block `bb` from some entry point
|
||||
* basic block must go through this basic block (which is an immediate
|
||||
* predecessor of `bb`).
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```rb
|
||||
* def m b
|
||||
* if b
|
||||
* return 0
|
||||
* end
|
||||
* return 1
|
||||
* end
|
||||
* ```
|
||||
*
|
||||
* The basic block starting on line 2 immediately dominates the
|
||||
* basic block on line 5 (all paths from the entry point of `m`
|
||||
* to `return 1` must go through the `if` block).
|
||||
*/
|
||||
predicate immediatelyDominates(BasicBlock bb) { bbIDominates(this, bb) }
|
||||
|
||||
/**
|
||||
* Holds if this basic block strictly dominates basic block `bb`.
|
||||
*
|
||||
* That is, all paths reaching basic block `bb` from some entry point
|
||||
* basic block must go through this basic block (which must be different
|
||||
* from `bb`).
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```rb
|
||||
* def m b
|
||||
* if b
|
||||
* return 0
|
||||
* end
|
||||
* return 1
|
||||
* end
|
||||
* ```
|
||||
*
|
||||
* The basic block starting on line 2 strictly dominates the
|
||||
* basic block on line 5 (all paths from the entry point of `m`
|
||||
* to `return 1` must go through the `if` block).
|
||||
*/
|
||||
predicate strictlyDominates(BasicBlock bb) { bbIDominates+(this, bb) }
|
||||
|
||||
/**
|
||||
* Holds if this basic block dominates basic block `bb`.
|
||||
*
|
||||
* That is, all paths reaching basic block `bb` from some entry point
|
||||
* basic block must go through this basic block.
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```rb
|
||||
* def m b
|
||||
* if b
|
||||
* return 0
|
||||
* end
|
||||
* return 1
|
||||
* end
|
||||
* ```
|
||||
*
|
||||
* The basic block starting on line 2 dominates the basic
|
||||
* basic block on line 5 (all paths from the entry point of `m`
|
||||
* to `return 1` must go through the `if` block).
|
||||
*/
|
||||
predicate dominates(BasicBlock bb) {
|
||||
bb = this or
|
||||
this.strictlyDominates(bb)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `df` is in the dominance frontier of this basic block.
|
||||
* That is, this basic block dominates a predecessor of `df`, but
|
||||
* does not dominate `df` itself.
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```rb
|
||||
* def m x
|
||||
* if x < 0
|
||||
* x = -x
|
||||
* if x > 10
|
||||
* x = x - 1
|
||||
* end
|
||||
* end
|
||||
* puts x
|
||||
* end
|
||||
* ```
|
||||
*
|
||||
* The basic block on line 8 is in the dominance frontier
|
||||
* of the basic block starting on line 3 because that block
|
||||
* dominates the basic block on line 4, which is a predecessor of
|
||||
* `puts x`. Also, the basic block starting on line 3 does not
|
||||
* dominate the basic block on line 8.
|
||||
*/
|
||||
predicate inDominanceFrontier(BasicBlock df) {
|
||||
this.dominatesPredecessor(df) and
|
||||
not strictlyDominates(df)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if this basic block dominates a predecessor of `df`.
|
||||
*/
|
||||
private predicate dominatesPredecessor(BasicBlock df) { this.dominates(df.getAPredecessor()) }
|
||||
|
||||
/**
|
||||
* Gets the basic block that immediately dominates this basic block, if any.
|
||||
*
|
||||
* That is, all paths reaching this basic block from some entry point
|
||||
* basic block must go through the result, which is an immediate basic block
|
||||
* predecessor of this basic block.
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```rb
|
||||
* def m b
|
||||
* if b
|
||||
* return 0
|
||||
* end
|
||||
* return 1
|
||||
* end
|
||||
* ```
|
||||
*
|
||||
* The basic block starting on line 2 is an immediate dominator of
|
||||
* the basic block on line 5 (all paths from the entry point of `m`
|
||||
* to `return 1` must go through the `if` block, and the `if` block
|
||||
* is an immediate predecessor of `return 1`).
|
||||
*/
|
||||
BasicBlock getImmediateDominator() { bbIDominates(result, this) }
|
||||
|
||||
/**
|
||||
* Holds if this basic block strictly post-dominates basic block `bb`.
|
||||
*
|
||||
* That is, all paths reaching a normal exit point basic block from basic
|
||||
* block `bb` must go through this basic block (which must be different
|
||||
* from `bb`).
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```rb
|
||||
* def m b
|
||||
* if b
|
||||
* puts "b"
|
||||
* end
|
||||
* puts "m"
|
||||
* end
|
||||
* ```
|
||||
*
|
||||
* The basic block on line 5 strictly post-dominates the basic block on
|
||||
* line 3 (all paths to the exit point of `m` from `puts "b"` must go
|
||||
* through `puts "m"`).
|
||||
*/
|
||||
predicate strictlyPostDominates(BasicBlock bb) { bbIPostDominates+(this, bb) }
|
||||
|
||||
/**
|
||||
* Holds if this basic block post-dominates basic block `bb`.
|
||||
*
|
||||
* That is, all paths reaching a normal exit point basic block from basic
|
||||
* block `bb` must go through this basic block.
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```rb
|
||||
* def m b
|
||||
* if b
|
||||
* puts "b"
|
||||
* end
|
||||
* puts "m"
|
||||
* end
|
||||
* ```
|
||||
*
|
||||
* The basic block on line 5 post-dominates the basic block on line 3
|
||||
* (all paths to the exit point of `m` from `puts "b"` must go through
|
||||
* `puts "m"`).
|
||||
*/
|
||||
predicate postDominates(BasicBlock bb) {
|
||||
this.strictlyPostDominates(bb) or
|
||||
this = bb
|
||||
}
|
||||
|
||||
/** Holds if this basic block is in a loop in the control flow graph. */
|
||||
predicate inLoop() { this.getASuccessor+() = this }
|
||||
|
||||
/** Gets a textual representation of this basic block. */
|
||||
string toString() { result = this.getFirstNode().toString() }
|
||||
|
||||
/** Gets the location of this basic block. */
|
||||
Location getLocation() { result = this.getFirstNode().getLocation() }
|
||||
}
|
||||
|
||||
cached
|
||||
private module Cached {
|
||||
/** Internal representation of basic blocks. */
|
||||
cached
|
||||
newtype TBasicBlock = TBasicBlockStart(CfgNode cfn) { startsBB(cfn) }
|
||||
|
||||
/** Holds if `cfn` starts a new basic block. */
|
||||
private predicate startsBB(CfgNode cfn) {
|
||||
not exists(cfn.getAPredecessor()) and exists(cfn.getASuccessor())
|
||||
or
|
||||
cfn.isJoin()
|
||||
or
|
||||
cfn.getAPredecessor().isBranch()
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `succ` is a control flow successor of `pred` within
|
||||
* the same basic block.
|
||||
*/
|
||||
private predicate intraBBSucc(CfgNode pred, CfgNode succ) {
|
||||
succ = pred.getASuccessor() and
|
||||
not startsBB(succ)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `cfn` is the `i`th node in basic block `bb`.
|
||||
*
|
||||
* In other words, `i` is the shortest distance from a node `bb`
|
||||
* that starts a basic block to `cfn` along the `intraBBSucc` relation.
|
||||
*/
|
||||
cached
|
||||
predicate bbIndex(CfgNode bbStart, CfgNode cfn, int i) =
|
||||
shortestDistances(startsBB/1, intraBBSucc/2)(bbStart, cfn, i)
|
||||
|
||||
/**
|
||||
* Holds if the first node of basic block `succ` is a control flow
|
||||
* successor of the last node of basic block `pred`.
|
||||
*/
|
||||
private predicate succBB(BasicBlock pred, BasicBlock succ) { succ = pred.getASuccessor() }
|
||||
|
||||
/** Holds if `dom` is an immediate dominator of `bb`. */
|
||||
cached
|
||||
predicate bbIDominates(BasicBlock dom, BasicBlock bb) =
|
||||
idominance(entryBB/1, succBB/2)(_, dom, bb)
|
||||
|
||||
/** Holds if `pred` is a basic block predecessor of `succ`. */
|
||||
private predicate predBB(BasicBlock succ, BasicBlock pred) { succBB(pred, succ) }
|
||||
|
||||
/** Holds if `bb` is an exit basic block that represents normal exit. */
|
||||
private predicate normalExitBB(BasicBlock bb) {
|
||||
bb.getANode().(CfgNodes::AnnotatedExitNode).isNormal()
|
||||
}
|
||||
|
||||
/** Holds if `dom` is an immediate post-dominator of `bb`. */
|
||||
cached
|
||||
predicate bbIPostDominates(BasicBlock dom, BasicBlock bb) =
|
||||
idominance(normalExitBB/1, predBB/2)(_, dom, bb)
|
||||
|
||||
/**
|
||||
* Gets the `i`th predecessor of join block `jb`, with respect to some
|
||||
* arbitrary order.
|
||||
*/
|
||||
cached
|
||||
JoinBlockPredecessor getJoinBlockPredecessor(JoinBlock jb, int i) {
|
||||
result =
|
||||
rank[i + 1](JoinBlockPredecessor jbp |
|
||||
jbp = jb.getAPredecessor()
|
||||
|
|
||||
jbp order by JoinBlockPredecessors::getId(jbp), JoinBlockPredecessors::getSplitString(jbp)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
private import Cached
|
||||
|
||||
/** Holds if `bb` is an entry basic block. */
|
||||
private predicate entryBB(BasicBlock bb) { bb.getFirstNode() instanceof CfgNodes::EntryNode }
|
||||
|
||||
/**
|
||||
* An entry basic block, that is, a basic block whose first node is
|
||||
* an entry node.
|
||||
*/
|
||||
class EntryBasicBlock extends BasicBlock {
|
||||
EntryBasicBlock() { entryBB(this) }
|
||||
|
||||
override CfgScope getScope() { this.getFirstNode() = TEntryNode(result) }
|
||||
}
|
||||
|
||||
/**
|
||||
* An annotated exit basic block, that is, a basic block whose last node is
|
||||
* an annotated exit node.
|
||||
*/
|
||||
class AnnotatedExitBasicBlock extends BasicBlock {
|
||||
AnnotatedExitBasicBlock() { this.getANode() instanceof CfgNodes::AnnotatedExitNode }
|
||||
}
|
||||
|
||||
/**
|
||||
* An exit basic block, that is, a basic block whose last node is
|
||||
* an exit node.
|
||||
*/
|
||||
class ExitBasicBlock extends BasicBlock {
|
||||
ExitBasicBlock() { this.getLastNode() instanceof CfgNodes::ExitNode }
|
||||
}
|
||||
|
||||
private module JoinBlockPredecessors {
|
||||
private import CfgNodes
|
||||
|
||||
private predicate id(AstNode x, AstNode y) { x = y }
|
||||
|
||||
private predicate idOf(AstNode x, int y) = equivalenceRelation(id/2)(x, y)
|
||||
|
||||
int getId(JoinBlockPredecessor jbp) {
|
||||
idOf(jbp.getFirstNode().(AstCfgNode).getNode(), result)
|
||||
or
|
||||
idOf(jbp.(EntryBasicBlock).getScope(), result)
|
||||
}
|
||||
|
||||
string getSplitString(JoinBlockPredecessor jbp) {
|
||||
result = jbp.getFirstNode().(AstCfgNode).getSplitsString()
|
||||
or
|
||||
not exists(jbp.getFirstNode().(AstCfgNode).getSplitsString()) and
|
||||
result = ""
|
||||
}
|
||||
}
|
||||
|
||||
/** A basic block with more than one predecessor. */
|
||||
class JoinBlock extends BasicBlock {
|
||||
JoinBlock() { getFirstNode().isJoin() }
|
||||
|
||||
/**
|
||||
* Gets the `i`th predecessor of this join block, with respect to some
|
||||
* arbitrary order.
|
||||
*/
|
||||
JoinBlockPredecessor getJoinBlockPredecessor(int i) { result = getJoinBlockPredecessor(this, i) }
|
||||
}
|
||||
|
||||
/** A basic block that is an immediate predecessor of a join block. */
|
||||
class JoinBlockPredecessor extends BasicBlock {
|
||||
JoinBlockPredecessor() { this.getASuccessor() instanceof JoinBlock }
|
||||
}
|
||||
|
||||
/** A basic block that terminates in a condition, splitting the subsequent control flow. */
|
||||
class ConditionBlock extends BasicBlock {
|
||||
ConditionBlock() { this.getLastNode().isCondition() }
|
||||
|
||||
/**
|
||||
* Holds if basic block `succ` is immediately controlled by this basic
|
||||
* block with conditional value `s`. That is, `succ` is an immediate
|
||||
* successor of this block, and `succ` can only be reached from
|
||||
* the callable entry point by going via the `s` edge out of this basic block.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate immediatelyControls(BasicBlock succ, BooleanSuccessor s) {
|
||||
succ = this.getASuccessor(s) and
|
||||
forall(BasicBlock pred | pred = succ.getAPredecessor() and pred != this | succ.dominates(pred))
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if basic block `controlled` is controlled by this basic block with
|
||||
* conditional value `s`. That is, `controlled` can only be reached from
|
||||
* the callable entry point by going via the `s` edge out of this basic block.
|
||||
*/
|
||||
predicate controls(BasicBlock controlled, BooleanSuccessor s) {
|
||||
exists(BasicBlock succ | this.immediatelyControls(succ, s) | succ.dominates(controlled))
|
||||
}
|
||||
}
|
||||
309
ql/src/codeql_ruby/controlflow/ControlFlowGraph.qll
Normal file
309
ql/src/codeql_ruby/controlflow/ControlFlowGraph.qll
Normal file
@@ -0,0 +1,309 @@
|
||||
/** Provides classes representing the control flow graph. */
|
||||
|
||||
import codeql_ruby.ast
|
||||
private import codeql_ruby.controlflow.BasicBlocks
|
||||
private import SuccessorTypes
|
||||
private import internal.ControlFlowGraphImpl
|
||||
private import internal.Splitting
|
||||
private import internal.Completion
|
||||
|
||||
/** An AST node with an associated control-flow graph. */
|
||||
class CfgScope = Method; // TODO: add more cases (e.g. bodies of lambdas/do blocks)
|
||||
|
||||
/**
|
||||
* A control flow node.
|
||||
*
|
||||
* A control flow node is a node in the control flow graph (CFG). There is a
|
||||
* many-to-one relationship between CFG nodes and AST nodes.
|
||||
*
|
||||
* Only nodes that can be reached from an entry point are included in the CFG.
|
||||
*/
|
||||
class CfgNode extends TCfgNode {
|
||||
/** Gets a textual representation of this control flow node. */
|
||||
string toString() { none() }
|
||||
|
||||
/** Gets the AST node that this node corresponds to, if any. */
|
||||
AstNode getNode() { none() }
|
||||
|
||||
/** Gets the location of this control flow node. */
|
||||
Location getLocation() { result = this.getNode().getLocation() }
|
||||
|
||||
/** Holds if this control flow node has conditional successors. */
|
||||
final predicate isCondition() { exists(this.getASuccessor(any(BooleanSuccessor bs))) }
|
||||
|
||||
/** Gets the scope of this node. */
|
||||
final CfgScope getScope() { result = this.getBasicBlock().getScope() }
|
||||
|
||||
/** Gets the basic block that this control flow node belongs to. */
|
||||
BasicBlock getBasicBlock() { result.getANode() = this }
|
||||
|
||||
/** Gets a successor node of a given type, if any. */
|
||||
final CfgNode getASuccessor(SuccessorType t) { result = getASuccessor(this, t) }
|
||||
|
||||
/** Gets an immediate successor, if any. */
|
||||
final CfgNode getASuccessor() { result = this.getASuccessor(_) }
|
||||
|
||||
/** Gets an immediate predecessor node of a given flow type, if any. */
|
||||
final CfgNode getAPredecessor(SuccessorType t) { result.getASuccessor(t) = this }
|
||||
|
||||
/** Gets an immediate predecessor, if any. */
|
||||
final CfgNode getAPredecessor() { result = this.getAPredecessor(_) }
|
||||
|
||||
/** Holds if this node has more than one predecessor. */
|
||||
final predicate isJoin() { strictcount(this.getAPredecessor()) > 1 }
|
||||
|
||||
/** Holds if this node has more than one successor. */
|
||||
final predicate isBranch() { strictcount(this.getASuccessor()) > 1 }
|
||||
}
|
||||
|
||||
/** Provides different types of control flow nodes. */
|
||||
module CfgNodes {
|
||||
/** An entry node for a given scope. */
|
||||
class EntryNode extends CfgNode, TEntryNode {
|
||||
private CfgScope scope;
|
||||
|
||||
EntryNode() { this = TEntryNode(scope) }
|
||||
|
||||
final override EntryBasicBlock getBasicBlock() { result = CfgNode.super.getBasicBlock() }
|
||||
|
||||
final override Location getLocation() { result = scope.getLocation() }
|
||||
|
||||
final override string toString() { result = "enter " + scope.getName() }
|
||||
}
|
||||
|
||||
/** An exit node for a given scope, annotated with the type of exit. */
|
||||
class AnnotatedExitNode extends CfgNode, TAnnotatedExitNode {
|
||||
private CfgScope scope;
|
||||
private boolean normal;
|
||||
|
||||
AnnotatedExitNode() { this = TAnnotatedExitNode(scope, normal) }
|
||||
|
||||
/** Holds if this node represent a normal exit. */
|
||||
final predicate isNormal() { normal = true }
|
||||
|
||||
final override AnnotatedExitBasicBlock getBasicBlock() {
|
||||
result = CfgNode.super.getBasicBlock()
|
||||
}
|
||||
|
||||
final override Location getLocation() { result = scope.getLocation() }
|
||||
|
||||
final override string toString() {
|
||||
exists(string s |
|
||||
normal = true and s = "normal"
|
||||
or
|
||||
normal = false and s = "abnormal"
|
||||
|
|
||||
result = "exit " + scope.getName() + " (" + s + ")"
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
/** An exit node for a given scope. */
|
||||
class ExitNode extends CfgNode, TExitNode {
|
||||
private CfgScope scope;
|
||||
|
||||
ExitNode() { this = TExitNode(scope) }
|
||||
|
||||
final override Location getLocation() { result = scope.getLocation() }
|
||||
|
||||
final override string toString() { result = "exit " + scope.getName() }
|
||||
}
|
||||
|
||||
/**
|
||||
* A node for an AST node.
|
||||
*
|
||||
* Each AST node maps to zero or more `AstCfgNode`s: zero when the node in unreachable
|
||||
* (dead) code or not important for control flow, and multiple when there are different
|
||||
* splits for the AST node.
|
||||
*/
|
||||
class AstCfgNode extends CfgNode, TAstNode {
|
||||
private Splits splits;
|
||||
private AstNode n;
|
||||
|
||||
AstCfgNode() { this = TAstNode(n, splits) }
|
||||
|
||||
final override AstNode getNode() { result = n }
|
||||
|
||||
final override string toString() {
|
||||
result = "[" + this.getSplitsString() + "] " + n.toString()
|
||||
or
|
||||
not exists(this.getSplitsString()) and result = n.toString()
|
||||
}
|
||||
|
||||
/** Gets a comma-separated list of strings for each split in this node, if any. */
|
||||
final string getSplitsString() {
|
||||
result = splits.toString() and
|
||||
result != ""
|
||||
}
|
||||
|
||||
/** Gets a split for this control flow node, if any. */
|
||||
final Split getASplit() { result = splits.getASplit() }
|
||||
}
|
||||
}
|
||||
|
||||
/** The type of a control flow successor. */
|
||||
class SuccessorType extends TSuccessorType {
|
||||
/** Gets a textual representation of successor type. */
|
||||
string toString() { none() }
|
||||
}
|
||||
|
||||
/** Provides different types of control flow successor types. */
|
||||
module SuccessorTypes {
|
||||
/** A normal control flow successor. */
|
||||
class NormalSuccessor extends SuccessorType, TSuccessorSuccessor {
|
||||
final override string toString() { result = "successor" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A Boolean control flow successor.
|
||||
*
|
||||
* For example, in
|
||||
*
|
||||
* ```rb
|
||||
* if x >= 0
|
||||
* puts "positive"
|
||||
* else
|
||||
* puts "negative"
|
||||
* end
|
||||
* ```
|
||||
*
|
||||
* `x >= 0` has both a `true` successor and a `false` successor.
|
||||
*/
|
||||
class BooleanSuccessor extends SuccessorType, TBooleanSuccessor {
|
||||
/** Gets the Boolean value. */
|
||||
final boolean getValue() { this = TBooleanSuccessor(result) }
|
||||
|
||||
final override string toString() { result = getValue().toString() }
|
||||
}
|
||||
|
||||
/**
|
||||
* A `return` control flow successor.
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```rb
|
||||
* def sum(x,y)
|
||||
* return x + y
|
||||
* end
|
||||
* ```
|
||||
*
|
||||
* The exit node of `sum` is a `return` successor of the `return x + y`
|
||||
* statement.
|
||||
*/
|
||||
class ReturnSuccessor extends SuccessorType, TReturnSuccessor {
|
||||
final override string toString() { result = "return" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A `break` control flow successor.
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```rb
|
||||
* def m
|
||||
* while x >= 0
|
||||
* x -= 1
|
||||
* if num > 100
|
||||
* break
|
||||
* end
|
||||
* end
|
||||
* puts "done"
|
||||
* end
|
||||
* ```
|
||||
*
|
||||
* The node `puts "done"` is `break` successor of the node `break`.
|
||||
*/
|
||||
class BreakSuccessor extends SuccessorType, TBreakSuccessor {
|
||||
final override string toString() { result = "break" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A `next` control flow successor.
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```rb
|
||||
* def m
|
||||
* while x >= 0
|
||||
* x -= 1
|
||||
* if num > 100
|
||||
* next
|
||||
* end
|
||||
* end
|
||||
* puts "done"
|
||||
* end
|
||||
* ```
|
||||
*
|
||||
* The node `x >= 0` is `next` successor of the node `next`.
|
||||
*/
|
||||
class NextSuccessor extends SuccessorType, TNextSuccessor {
|
||||
final override string toString() { result = "next" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A `redo` control flow successor.
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```rb
|
||||
* def m
|
||||
* while x >= 0
|
||||
* x -= 1
|
||||
* if num > 100
|
||||
* redo
|
||||
* end
|
||||
* end
|
||||
* puts "done"
|
||||
* end
|
||||
* ```
|
||||
*
|
||||
* The node `x -= 1` is `redo` successor of the node `redo`.
|
||||
*/
|
||||
class RedoSuccessor extends SuccessorType, TRedoSuccessor {
|
||||
final override string toString() { result = "redo" }
|
||||
}
|
||||
|
||||
/**
|
||||
* An exceptional control flow successor.
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```rb
|
||||
* def m x
|
||||
* if x > 2
|
||||
* raise "x > 2"
|
||||
* end
|
||||
* puts "x <= 2"
|
||||
* end
|
||||
* ```
|
||||
*
|
||||
* The exit node of `m` is an exceptional successor of the node
|
||||
* `raise "x > 2"`.
|
||||
*/
|
||||
class RaiseSuccessor extends SuccessorType, TRaiseSuccessor {
|
||||
final override string toString() { result = "raise" }
|
||||
}
|
||||
|
||||
/**
|
||||
* An exit control flow successor.
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```rb
|
||||
* def m x
|
||||
* if x > 2
|
||||
* exit 1
|
||||
* end
|
||||
* puts "x <= 2"
|
||||
* end
|
||||
* ```
|
||||
*
|
||||
* The exit node of `m` is an exit successor of the node
|
||||
* `exit 1`.
|
||||
*/
|
||||
class ExitSuccessor extends SuccessorType, TExitSuccessor {
|
||||
final override string toString() { result = "exit" }
|
||||
}
|
||||
}
|
||||
73
ql/src/codeql_ruby/controlflow/internal/AstNodes.qll
Normal file
73
ql/src/codeql_ruby/controlflow/internal/AstNodes.qll
Normal file
@@ -0,0 +1,73 @@
|
||||
/**
|
||||
* Provides various helper classes for AST nodes. The definitions in this file
|
||||
* will likely be part of the hand-written user-facing AST layer.
|
||||
*/
|
||||
|
||||
import codeql_ruby.ast
|
||||
|
||||
class LogicalNotAstNode extends Unary {
|
||||
AstNode operand;
|
||||
|
||||
LogicalNotAstNode() {
|
||||
this.getOperator().toString() in ["!", "not"] and
|
||||
operand = this.getOperand()
|
||||
}
|
||||
}
|
||||
|
||||
class LogicalAndAstNode extends Binary {
|
||||
AstNode left;
|
||||
AstNode right;
|
||||
|
||||
LogicalAndAstNode() {
|
||||
this.getOperator().toString() in ["&&", "and"] and
|
||||
left = this.getLeft() and
|
||||
right = this.getRight()
|
||||
}
|
||||
|
||||
AstNode getAnOperand() { result in [left, right] }
|
||||
}
|
||||
|
||||
class LogicalOrAstNode extends Binary {
|
||||
AstNode left;
|
||||
AstNode right;
|
||||
|
||||
LogicalOrAstNode() {
|
||||
this.getOperator().toString() in ["||", "or"] and
|
||||
left = this.getLeft() and
|
||||
right = this.getRight()
|
||||
}
|
||||
|
||||
AstNode getAnOperand() { result in [left, right] }
|
||||
}
|
||||
|
||||
private class If_or_elisif = @if or @elsif;
|
||||
|
||||
class IfElsifAstNode extends AstNode, If_or_elisif {
|
||||
AstNode getConditionNode() { none() }
|
||||
|
||||
AstNode getConsequenceNode() { none() }
|
||||
|
||||
AstNode getAlternativeNode() { none() }
|
||||
}
|
||||
|
||||
private class IfAstNode extends IfElsifAstNode, If {
|
||||
override AstNode getConditionNode() { result = this.getCondition() }
|
||||
|
||||
override AstNode getConsequenceNode() { result = this.getConsequence() }
|
||||
|
||||
override AstNode getAlternativeNode() { result = this.getAlternative() }
|
||||
}
|
||||
|
||||
private class ElsifAstNode extends IfElsifAstNode, Elsif {
|
||||
override AstNode getConditionNode() { result = this.getCondition() }
|
||||
|
||||
override AstNode getConsequenceNode() { result = this.getConsequence() }
|
||||
|
||||
override AstNode getAlternativeNode() { result = this.getAlternative() }
|
||||
}
|
||||
|
||||
class ParenthesizedStatement extends ParenthesizedStatements {
|
||||
ParenthesizedStatement() { strictcount(int i | exists(this.getChild(i))) = 1 }
|
||||
|
||||
AstNode getChild() { result = this.getChild(0) }
|
||||
}
|
||||
10
ql/src/codeql_ruby/controlflow/internal/Cfg.ql
Normal file
10
ql/src/codeql_ruby/controlflow/internal/Cfg.ql
Normal file
@@ -0,0 +1,10 @@
|
||||
import codeql_ruby.controlflow.ControlFlowGraph
|
||||
|
||||
query predicate nodes(CfgNode n) { any() }
|
||||
|
||||
query predicate edges(CfgNode pred, CfgNode succ, string attr, string val) {
|
||||
exists(SuccessorType t | succ = pred.getASuccessor(t) |
|
||||
attr = "semmle.label" and
|
||||
val = t.toString()
|
||||
)
|
||||
}
|
||||
282
ql/src/codeql_ruby/controlflow/internal/Completion.qll
Normal file
282
ql/src/codeql_ruby/controlflow/internal/Completion.qll
Normal file
@@ -0,0 +1,282 @@
|
||||
/**
|
||||
* Provides classes representing control flow completions.
|
||||
*
|
||||
* A completion represents how a statement or expression terminates.
|
||||
*/
|
||||
|
||||
import codeql_ruby.ast
|
||||
private import codeql_ruby.controlflow.ControlFlowGraph
|
||||
private import AstNodes
|
||||
private import NonReturning
|
||||
private import SuccessorTypes
|
||||
|
||||
private newtype TCompletion =
|
||||
TSimpleCompletion() or
|
||||
TBooleanCompletion(boolean b) { b = true or b = false } or
|
||||
TReturnCompletion() or
|
||||
TBreakCompletion() or
|
||||
TNextCompletion() or
|
||||
TRedoCompletion() or
|
||||
TRaiseCompletion() or // TODO: Add exception type?
|
||||
TExitCompletion() or
|
||||
TNestedCompletion(Completion inner, Completion outer) {
|
||||
outer = TSimpleCompletion() and
|
||||
inner = TBreakCompletion()
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate completionIsValidForStmt(AstNode n, Completion c) {
|
||||
n instanceof Break and
|
||||
c = TBreakCompletion()
|
||||
or
|
||||
n instanceof Next and
|
||||
c = TNextCompletion()
|
||||
or
|
||||
n instanceof Redo and
|
||||
c = TRedoCompletion()
|
||||
or
|
||||
n instanceof Return and
|
||||
c = TReturnCompletion()
|
||||
}
|
||||
|
||||
/** A completion of a statement or an expression. */
|
||||
abstract class Completion extends TCompletion {
|
||||
/** Holds if this completion is valid for node `n`. */
|
||||
predicate isValidFor(AstNode n) {
|
||||
this = n.(NonReturningCall).getACompletion()
|
||||
or
|
||||
completionIsValidForStmt(n, this)
|
||||
or
|
||||
mustHaveBooleanCompletion(n) and
|
||||
(
|
||||
exists(boolean value | isBooleanConstant(n, value) | this = TBooleanCompletion(value))
|
||||
or
|
||||
not isBooleanConstant(n, _) and
|
||||
this = TBooleanCompletion(_)
|
||||
)
|
||||
or
|
||||
not n instanceof NonReturningCall and
|
||||
not completionIsValidForStmt(n, _) and
|
||||
not mustHaveBooleanCompletion(n) and
|
||||
this = TSimpleCompletion()
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if this completion will continue a loop when it is the completion
|
||||
* of a loop body.
|
||||
*/
|
||||
predicate continuesLoop() {
|
||||
this instanceof NormalCompletion or
|
||||
this instanceof NextCompletion
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the inner completion. This is either the inner completion,
|
||||
* when the completion is nested, or the completion itself.
|
||||
*/
|
||||
Completion getInnerCompletion() { result = this }
|
||||
|
||||
/**
|
||||
* Gets the outer completion. This is either the outer completion,
|
||||
* when the completion is nested, or the completion itself.
|
||||
*/
|
||||
Completion getOuterCompletion() { result = this }
|
||||
|
||||
/** Gets a successor type that matches this completion. */
|
||||
abstract SuccessorType getAMatchingSuccessorType();
|
||||
|
||||
/** Gets a textual representation of this completion. */
|
||||
abstract string toString();
|
||||
}
|
||||
|
||||
/** Holds if node `n` has the Boolean constant value `value`. */
|
||||
private predicate isBooleanConstant(AstNode n, boolean value) {
|
||||
mustHaveBooleanCompletion(n) and
|
||||
(
|
||||
n.(Constant).getValue() = "true" and
|
||||
value = true
|
||||
or
|
||||
n.(Constant).getValue() = "false" and
|
||||
value = false
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if a normal completion of `n` must be a Boolean completion.
|
||||
*/
|
||||
private predicate mustHaveBooleanCompletion(AstNode n) {
|
||||
inBooleanContext(n) and
|
||||
not n instanceof NonReturningCall
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `n` is used in a Boolean context. That is, the value
|
||||
* that `n` evaluates to determines a true/false branch successor.
|
||||
*/
|
||||
private predicate inBooleanContext(AstNode n) {
|
||||
n = any(IfElsifAstNode parent).getConditionNode()
|
||||
or
|
||||
n = any(While parent).getCondition()
|
||||
or
|
||||
exists(LogicalAndAstNode parent |
|
||||
n = parent.getLeft()
|
||||
or
|
||||
inBooleanContext(parent) and
|
||||
n = parent.getRight()
|
||||
)
|
||||
or
|
||||
exists(LogicalOrAstNode parent |
|
||||
n = parent.getLeft()
|
||||
or
|
||||
inBooleanContext(parent) and
|
||||
n = parent.getRight()
|
||||
)
|
||||
or
|
||||
n = any(LogicalNotAstNode parent | inBooleanContext(parent)).getOperand()
|
||||
or
|
||||
n = any(ParenthesizedStatement parent | inBooleanContext(parent)).getChild()
|
||||
}
|
||||
|
||||
/**
|
||||
* A completion that represents normal evaluation of a statement or an
|
||||
* expression.
|
||||
*/
|
||||
abstract class NormalCompletion extends Completion { }
|
||||
|
||||
/** A simple (normal) completion. */
|
||||
class SimpleCompletion extends NormalCompletion, TSimpleCompletion {
|
||||
override NormalSuccessor getAMatchingSuccessorType() { any() }
|
||||
|
||||
override string toString() { result = "simple" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A completion that represents evaluation of an expression
|
||||
* with a Boolean value.
|
||||
*/
|
||||
class BooleanCompletion extends NormalCompletion, TBooleanCompletion {
|
||||
private boolean value;
|
||||
|
||||
BooleanCompletion() { this = TBooleanCompletion(value) }
|
||||
|
||||
/** Gets the Boolean value of this completion. */
|
||||
boolean getValue() { result = value }
|
||||
|
||||
/** Gets the dual Boolean completion. */
|
||||
BooleanCompletion getDual() { result = TBooleanCompletion(value.booleanNot()) }
|
||||
|
||||
override BooleanSuccessor getAMatchingSuccessorType() { result.getValue() = value }
|
||||
|
||||
override string toString() { result = value.toString() }
|
||||
}
|
||||
|
||||
/** A Boolean `true` completion. */
|
||||
class TrueCompletion extends BooleanCompletion {
|
||||
TrueCompletion() { this.getValue() = true }
|
||||
}
|
||||
|
||||
/** A Boolean `false` completion. */
|
||||
class FalseCompletion extends BooleanCompletion {
|
||||
FalseCompletion() { this.getValue() = false }
|
||||
}
|
||||
|
||||
/**
|
||||
* A completion that represents evaluation of a statement or an
|
||||
* expression resulting in a return.
|
||||
*/
|
||||
class ReturnCompletion extends Completion, TReturnCompletion {
|
||||
override ReturnSuccessor getAMatchingSuccessorType() { any() }
|
||||
|
||||
override string toString() { result = "return" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A completion that represents evaluation of a statement or an
|
||||
* expression resulting in a break from a loop.
|
||||
*/
|
||||
class BreakCompletion extends Completion, TBreakCompletion {
|
||||
override BreakSuccessor getAMatchingSuccessorType() { any() }
|
||||
|
||||
override string toString() { result = "break" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A completion that represents evaluation of a statement or an
|
||||
* expression resulting in a continuation of a loop.
|
||||
*/
|
||||
class NextCompletion extends Completion, TNextCompletion {
|
||||
override NextSuccessor getAMatchingSuccessorType() { any() }
|
||||
|
||||
override string toString() { result = "next" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A completion that represents evaluation of a statement or an
|
||||
* expression resulting in a redo of a loop iteration.
|
||||
*/
|
||||
class RedoCompletion extends Completion, TRedoCompletion {
|
||||
override RedoSuccessor getAMatchingSuccessorType() { any() }
|
||||
|
||||
override string toString() { result = "redo" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A completion that represents evaluation of a statement or an
|
||||
* expression resulting in a thrown exception.
|
||||
*/
|
||||
class RaiseCompletion extends Completion, TRaiseCompletion {
|
||||
override RaiseSuccessor getAMatchingSuccessorType() { any() }
|
||||
|
||||
override string toString() { result = "raise" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A completion that represents evaluation of a statement or an
|
||||
* expression resulting in an abort/exit.
|
||||
*/
|
||||
class ExitCompletion extends Completion, TExitCompletion {
|
||||
override ExitSuccessor getAMatchingSuccessorType() { any() }
|
||||
|
||||
override string toString() { result = "exit" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A nested completion. For example, in
|
||||
*
|
||||
* ```rb
|
||||
* def m
|
||||
* while x >= 0
|
||||
* x -= 1
|
||||
* if num > 100
|
||||
* break
|
||||
* end
|
||||
* end
|
||||
* puts "done"
|
||||
* end
|
||||
* ```
|
||||
*
|
||||
* the `while` loop can have a nested completion where the inner completion
|
||||
* is a `break` and the outer completion is a simple successor.
|
||||
*/
|
||||
class NestedCompletion extends Completion, TNestedCompletion {
|
||||
Completion inner;
|
||||
Completion outer;
|
||||
|
||||
NestedCompletion() { this = TNestedCompletion(inner, outer) }
|
||||
|
||||
override Completion getInnerCompletion() { result = inner }
|
||||
|
||||
override Completion getOuterCompletion() { result = outer }
|
||||
|
||||
override SuccessorType getAMatchingSuccessorType() {
|
||||
inner = TBreakCompletion() and
|
||||
outer = TSimpleCompletion() and
|
||||
result instanceof BreakSuccessor
|
||||
}
|
||||
|
||||
override string toString() { result = outer + " [" + inner + "]" }
|
||||
}
|
||||
|
||||
private class NestedNormalCompletion extends NormalCompletion, NestedCompletion {
|
||||
NestedNormalCompletion() { outer instanceof NormalCompletion }
|
||||
}
|
||||
53
ql/src/codeql_ruby/controlflow/internal/Consistency.qll
Normal file
53
ql/src/codeql_ruby/controlflow/internal/Consistency.qll
Normal file
@@ -0,0 +1,53 @@
|
||||
import codeql_ruby.ast
|
||||
import codeql_ruby.controlflow.ControlFlowGraph
|
||||
import Completion
|
||||
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)
|
||||
}
|
||||
550
ql/src/codeql_ruby/controlflow/internal/ControlFlowGraphImpl.qll
Normal file
550
ql/src/codeql_ruby/controlflow/internal/ControlFlowGraphImpl.qll
Normal file
@@ -0,0 +1,550 @@
|
||||
/**
|
||||
* Provides auxiliary classes and predicates used to construct the basic successor
|
||||
* relation on control flow elements.
|
||||
*
|
||||
* The implementation is centered around the concept of a _completion_, which
|
||||
* models how the execution of a statement or expression terminates.
|
||||
* Completions are represented as an algebraic data type `Completion` defined in
|
||||
* `Completion.qll`.
|
||||
*
|
||||
* The CFG is built by structural recursion over the AST. To achieve this the
|
||||
* CFG edges related to a given AST node, `n`, are divided into three categories:
|
||||
*
|
||||
* 1. The in-going edge that points to the first CFG node to execute when
|
||||
* `n` is going to be executed.
|
||||
* 2. The out-going edges for control flow leaving `n` that are going to some
|
||||
* other node in the surrounding context of `n`.
|
||||
* 3. The edges that have both of their end-points entirely within the AST
|
||||
* node and its children.
|
||||
*
|
||||
* The edges in (1) and (2) are inherently non-local and are therefore
|
||||
* initially calculated as half-edges, that is, the single node, `k`, of the
|
||||
* edge contained within `n`, by the predicates `k = first(n)` and `k = last(n, _)`,
|
||||
* respectively. The edges in (3) can then be enumerated directly by the predicate
|
||||
* `succ` by calling `first` and `last` recursively on the children of `n` and
|
||||
* connecting the end-points. This yields the entire CFG, since all edges are in
|
||||
* (3) for _some_ AST node.
|
||||
*
|
||||
* The second parameter of `last` is the completion, which is necessary to distinguish
|
||||
* the out-going edges from `n`. Note that the completion changes as the calculation of
|
||||
* `last` proceeds outward through the AST; for example, a `BreakCompletion` is
|
||||
* caught up by its surrounding loop and turned into a `NormalCompletion`.
|
||||
*/
|
||||
|
||||
import codeql_ruby.ast
|
||||
private import AstNodes
|
||||
private import codeql_ruby.controlflow.ControlFlowGraph
|
||||
private import Completion
|
||||
private import SuccessorTypes
|
||||
private import Splitting
|
||||
|
||||
abstract private class ControlFlowTree extends AstNode {
|
||||
/**
|
||||
* 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 this node should be hidden in the CFG. That is, edges
|
||||
* `pred -> this -> succ` are converted to a single edge `pred -> succ`.
|
||||
*/
|
||||
predicate isHidden() { none() }
|
||||
}
|
||||
|
||||
/** 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
|
||||
)
|
||||
}
|
||||
|
||||
private predicate succImpl(AstNode pred, AstNode succ, Completion c) {
|
||||
any(ControlFlowTree cft).succ(pred, succ, c)
|
||||
}
|
||||
|
||||
private predicate isHidden(ControlFlowTree t) { t.isHidden() }
|
||||
|
||||
private predicate succImplIfHidden(AstNode pred, AstNode succ) {
|
||||
isHidden(pred) and
|
||||
succImpl(pred, succ, any(SimpleCompletion c))
|
||||
}
|
||||
|
||||
/**
|
||||
* 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) {
|
||||
exists(AstNode n |
|
||||
succImpl(pred, n, c) and
|
||||
succImplIfHidden*(n, succ) and
|
||||
not isHidden(pred) and
|
||||
not isHidden(succ)
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if `first` is first executed when entering `scope`. */
|
||||
pragma[nomagic]
|
||||
predicate succEntry(CfgScope scope, AstNode first) {
|
||||
exists(AstNode n |
|
||||
first(scope, n) and
|
||||
succImplIfHidden*(n, first) and
|
||||
not isHidden(first)
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if `last` with completion `c` can exit `scope`. */
|
||||
pragma[nomagic]
|
||||
predicate succExit(AstNode last, CfgScope scope, Completion c) {
|
||||
exists(AstNode n |
|
||||
last(scope, n, c) and
|
||||
succImplIfHidden*(last, n) and
|
||||
not isHidden(last)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* 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 StandardNode extends ControlFlowTree {
|
||||
/** Gets the `i`th child node, in order of evaluation. */
|
||||
abstract AstNode getChildNode(int i);
|
||||
|
||||
private AstNode getChildNodeRanked(int i) {
|
||||
result = rank[i + 1](AstNode 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 |
|
||||
last = max(int i | exists(this.getChildNodeRanked(i))) and
|
||||
result = this.getChildNodeRanked(last)
|
||||
)
|
||||
}
|
||||
|
||||
/** Gets the `i`th child, which is not the last node. */
|
||||
pragma[nomagic]
|
||||
private AstNode getNonLastChildNode(int i) {
|
||||
result = this.getChildNodeRanked(i) and
|
||||
not result = this.getLastChildNode()
|
||||
}
|
||||
|
||||
final override predicate propagatesAbnormal(AstNode child) { child = this.getChildNode(_) }
|
||||
|
||||
pragma[nomagic]
|
||||
override predicate succ(AstNode pred, AstNode succ, Completion c) {
|
||||
exists(int i |
|
||||
last(this.getNonLastChildNode(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 }
|
||||
}
|
||||
|
||||
abstract private class StandardPreOrderTree extends StandardNode, 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) {
|
||||
StandardNode.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 StandardNode, 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) {
|
||||
StandardNode.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 {
|
||||
final override predicate propagatesAbnormal(AstNode child) { none() }
|
||||
|
||||
final override predicate succ(AstNode pred, AstNode succ, Completion c) { none() }
|
||||
}
|
||||
|
||||
/** Defines the CFG by dispatch on the various AST types. */
|
||||
private module Trees {
|
||||
private class ArgumentListTree extends StandardPostOrderTree, ArgumentList {
|
||||
final override AstNode getChildNode(int i) { result = this.getChild(i) }
|
||||
|
||||
override predicate isHidden() { any() }
|
||||
}
|
||||
|
||||
private class ArrayTree extends StandardPostOrderTree, Array {
|
||||
final override AstNode getChildNode(int i) { result = this.getChild(i) }
|
||||
}
|
||||
|
||||
private class AssignmentTree extends StandardPostOrderTree, Assignment {
|
||||
final override AstNode getChildNode(int i) {
|
||||
result = this.getLeft() and i = 0
|
||||
or
|
||||
result = this.getRight() and i = 1
|
||||
}
|
||||
}
|
||||
|
||||
private class BinaryTree extends StandardPostOrderTree, Binary {
|
||||
BinaryTree() { not this instanceof LogicalAndAstNode and not this instanceof LogicalOrAstNode }
|
||||
|
||||
final override AstNode getChildNode(int i) {
|
||||
result = this.getLeft() and i = 0
|
||||
or
|
||||
result = this.getRight() and i = 1
|
||||
}
|
||||
}
|
||||
|
||||
private class BlockParameterTree extends LeafTree, BlockParameter { }
|
||||
|
||||
private class BlockParametersTree extends StandardPostOrderTree, BlockParameters {
|
||||
final override AstNode getChildNode(int i) { result = this.getChild(i) }
|
||||
|
||||
override predicate isHidden() { any() }
|
||||
}
|
||||
|
||||
private class BreakTree extends StandardPostOrderTree, Break {
|
||||
final override AstNode getChildNode(int i) { result = this.getChild() and i = 0 }
|
||||
}
|
||||
|
||||
private class CallTree extends StandardPostOrderTree, Call {
|
||||
final override AstNode getChildNode(int i) {
|
||||
result = this.getReceiver() and i = 0
|
||||
or
|
||||
result = this.getMethod() and i = 1
|
||||
}
|
||||
}
|
||||
|
||||
private class DoTree extends StandardPreOrderTree, Do {
|
||||
final override AstNode getChildNode(int i) { result = this.getChild(i) }
|
||||
|
||||
override predicate isHidden() { any() }
|
||||
}
|
||||
|
||||
private class ElseTree extends StandardPreOrderTree, Else {
|
||||
final override AstNode getChildNode(int i) { result = this.getChild(i) }
|
||||
|
||||
override predicate isHidden() { any() }
|
||||
}
|
||||
|
||||
private class IdentifierTree extends LeafTree, Identifier { }
|
||||
|
||||
private class IfElsifTree extends PreOrderTree, IfElsifAstNode {
|
||||
final override predicate propagatesAbnormal(AstNode child) { child = this.getConditionNode() }
|
||||
|
||||
final override predicate last(AstNode last, Completion c) {
|
||||
last(this.getConditionNode(), last, c) and
|
||||
c instanceof FalseCompletion and
|
||||
not exists(this.getAlternativeNode())
|
||||
or
|
||||
last(this.getConsequenceNode(), last, c)
|
||||
or
|
||||
last(this.getAlternativeNode(), last, c)
|
||||
}
|
||||
|
||||
final override predicate succ(AstNode pred, AstNode succ, Completion c) {
|
||||
pred = this and
|
||||
first(this.getConditionNode(), succ) and
|
||||
c instanceof SimpleCompletion
|
||||
or
|
||||
last(this.getConditionNode(), pred, c) and
|
||||
(
|
||||
c instanceof TrueCompletion and first(this.getConsequenceNode(), succ)
|
||||
or
|
||||
c instanceof FalseCompletion and first(this.getAlternativeNode(), succ)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
private class IntegerTree extends LeafTree, Integer { }
|
||||
|
||||
class LogicalAndTree extends PostOrderTree, LogicalAndAstNode {
|
||||
final override predicate propagatesAbnormal(AstNode child) { child in [left, right] }
|
||||
|
||||
final override predicate first(AstNode first) { first(left, first) }
|
||||
|
||||
final override predicate succ(AstNode pred, AstNode succ, Completion c) {
|
||||
last(left, pred, c) and
|
||||
c instanceof TrueCompletion and
|
||||
first(right, succ)
|
||||
or
|
||||
last(left, pred, c) and
|
||||
c instanceof FalseCompletion and
|
||||
succ = this
|
||||
or
|
||||
last(right, pred, c) and
|
||||
c instanceof NormalCompletion and
|
||||
succ = this
|
||||
}
|
||||
}
|
||||
|
||||
class LogicalOrTree extends PostOrderTree, LogicalOrAstNode {
|
||||
final override predicate propagatesAbnormal(AstNode child) { child in [left, right] }
|
||||
|
||||
final override predicate first(AstNode first) { first(left, first) }
|
||||
|
||||
final override predicate succ(AstNode pred, AstNode succ, Completion c) {
|
||||
last(left, pred, c) and
|
||||
c instanceof FalseCompletion and
|
||||
first(right, succ)
|
||||
or
|
||||
last(left, pred, c) and
|
||||
c instanceof TrueCompletion and
|
||||
succ = this
|
||||
or
|
||||
last(right, pred, c) and
|
||||
c instanceof NormalCompletion and
|
||||
succ = this
|
||||
}
|
||||
}
|
||||
|
||||
class LogicalNotTree extends PostOrderTree, LogicalNotAstNode {
|
||||
final override predicate propagatesAbnormal(AstNode child) { child = operand }
|
||||
|
||||
final override predicate first(AstNode first) { first(operand, first) }
|
||||
|
||||
final override predicate succ(AstNode pred, AstNode succ, Completion c) {
|
||||
succ = this and
|
||||
(
|
||||
last(operand, pred, c.(BooleanCompletion).getDual())
|
||||
or
|
||||
last(operand, pred, c) and
|
||||
c instanceof SimpleCompletion
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
private class MethodTree extends StandardPreOrderTree, Method {
|
||||
final override AstNode getChildNode(int i) { result = this.getChild(i) }
|
||||
|
||||
override predicate isHidden() { any() }
|
||||
}
|
||||
|
||||
private class MethodCallTree extends StandardPostOrderTree, MethodCall {
|
||||
final override AstNode getChildNode(int i) {
|
||||
result = this.getArguments() and i = 0
|
||||
or
|
||||
result = this.getMethod() and i = 1
|
||||
or
|
||||
result = this.getBlock() and i = 2
|
||||
}
|
||||
}
|
||||
|
||||
private class NextTree extends StandardPostOrderTree, Next {
|
||||
final override AstNode getChildNode(int i) { result = this.getChild() and i = 0 }
|
||||
}
|
||||
|
||||
private class OperatorAssignmentTree extends StandardPostOrderTree, OperatorAssignment {
|
||||
final override AstNode getChildNode(int i) {
|
||||
result = this.getLeft() and i = 0
|
||||
or
|
||||
result = this.getRight() and i = 1
|
||||
}
|
||||
}
|
||||
|
||||
private class ParenthesizedStatementsTree extends StandardPostOrderTree, ParenthesizedStatements {
|
||||
final override AstNode getChildNode(int i) { result = this.getChild(i) }
|
||||
}
|
||||
|
||||
private class RedoTree extends StandardPostOrderTree, Redo {
|
||||
final override AstNode getChildNode(int i) { result = this.getChild() and i = 0 }
|
||||
}
|
||||
|
||||
private class ReturnTree extends StandardPostOrderTree, Return {
|
||||
final override AstNode getChildNode(int i) { result = this.getChild() and i = 0 }
|
||||
}
|
||||
|
||||
private class StringTree extends LeafTree, String { }
|
||||
|
||||
private class ThenTree extends StandardPreOrderTree, Then {
|
||||
final override AstNode getChildNode(int i) { result = this.getChild(i) }
|
||||
|
||||
override predicate isHidden() { any() }
|
||||
}
|
||||
|
||||
private class UnaryTree extends StandardPostOrderTree, Unary {
|
||||
UnaryTree() { not this instanceof LogicalNotAstNode }
|
||||
|
||||
final override AstNode getChildNode(int i) { result = this.getOperand() and i = 0 }
|
||||
}
|
||||
|
||||
private class WhileTree extends PreOrderTree, While {
|
||||
final override predicate propagatesAbnormal(AstNode child) { child = this.getCondition() }
|
||||
|
||||
final override predicate last(AstNode last, Completion c) {
|
||||
last(this.getCondition(), last, c) and
|
||||
c instanceof FalseCompletion
|
||||
or
|
||||
last(this.getBody(), last, c) and
|
||||
not c.continuesLoop() and
|
||||
not c instanceof BreakCompletion and
|
||||
not c instanceof RedoCompletion
|
||||
or
|
||||
c =
|
||||
any(NestedCompletion nc |
|
||||
last(this.getBody(), last, nc.getInnerCompletion().(BreakCompletion)) and
|
||||
nc.getOuterCompletion() instanceof SimpleCompletion
|
||||
)
|
||||
}
|
||||
|
||||
final override predicate succ(AstNode pred, AstNode succ, Completion c) {
|
||||
pred = this and
|
||||
first(this.getCondition(), succ) and
|
||||
c instanceof SimpleCompletion
|
||||
or
|
||||
last(this.getCondition(), pred, c) and
|
||||
c instanceof TrueCompletion and
|
||||
first(this.getBody(), succ)
|
||||
or
|
||||
last(this.getBody(), pred, c) and
|
||||
first(this.getCondition(), succ) and
|
||||
c.continuesLoop()
|
||||
or
|
||||
last(this.getBody(), pred, any(RedoCompletion rc)) and
|
||||
first(this.getBody(), succ) and
|
||||
c instanceof SimpleCompletion
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
cached
|
||||
private module Cached {
|
||||
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
|
||||
TAstNode(AstNode n, Splits splits) {
|
||||
exists(Reachability::SameSplitsBlock b | b.isReachable(splits) | n = b.getANode())
|
||||
}
|
||||
|
||||
cached
|
||||
newtype TSuccessorType =
|
||||
TSuccessorSuccessor() or
|
||||
TBooleanSuccessor(boolean b) { b = true or b = false } or
|
||||
TReturnSuccessor() or
|
||||
TBreakSuccessor() or
|
||||
TNextSuccessor() or
|
||||
TRedoSuccessor() 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 = TAstNode(succElement, succSplits)
|
||||
)
|
||||
or
|
||||
exists(AstNode predNode, Splits predSplits | pred = TAstNode(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 = TAstNode(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 }
|
||||
}
|
||||
22
ql/src/codeql_ruby/controlflow/internal/NonReturning.qll
Normal file
22
ql/src/codeql_ruby/controlflow/internal/NonReturning.qll
Normal file
@@ -0,0 +1,22 @@
|
||||
/** Provides a simple analysis for identifying calls that will not return. */
|
||||
|
||||
import codeql_ruby.ast
|
||||
private import Completion
|
||||
|
||||
/** A call that definitely does not return (conservative analysis). */
|
||||
abstract class NonReturningCall extends AstNode {
|
||||
/** Gets a valid completion for this non-returning call. */
|
||||
abstract Completion getACompletion();
|
||||
}
|
||||
|
||||
private class RaiseCall extends NonReturningCall, MethodCall {
|
||||
RaiseCall() { this.getMethod().toString() = "raise" }
|
||||
|
||||
override RaiseCompletion getACompletion() { any() }
|
||||
}
|
||||
|
||||
private class ExitCall extends NonReturningCall, MethodCall {
|
||||
ExitCall() { this.getMethod().toString() in ["abort", "exit"] }
|
||||
|
||||
override ExitCompletion getACompletion() { any() }
|
||||
}
|
||||
690
ql/src/codeql_ruby/controlflow/internal/Splitting.qll
Normal file
690
ql/src/codeql_ruby/controlflow/internal/Splitting.qll
Normal file
@@ -0,0 +1,690 @@
|
||||
/**
|
||||
* Provides classes and predicates relevant for splitting the control flow graph.
|
||||
*/
|
||||
|
||||
import codeql_ruby.ast
|
||||
private import AstNodes
|
||||
private import Completion
|
||||
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()
|
||||
|
||||
cached
|
||||
newtype TSplit = TConditionalCompletionSplit(BooleanCompletion c)
|
||||
|
||||
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
|
||||
|
||||
/** A split for a control flow node. */
|
||||
class Split extends TSplit {
|
||||
/** Gets a textual representation of this split. */
|
||||
string toString() { none() }
|
||||
}
|
||||
|
||||
private CfgScope getScope(AstNode n) { result.getAFieldOrChild*() = n }
|
||||
|
||||
/**
|
||||
* 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 = getScope(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(getScope(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(last, scope, c) implies succExit(last, scope, c)`
|
||||
*/
|
||||
abstract predicate hasExitScope(AstNode 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(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
|
||||
*
|
||||
* ```rb
|
||||
* def method x
|
||||
* if x < 2 and x > 0
|
||||
* puts "x is 1"
|
||||
* end
|
||||
* end
|
||||
* ```
|
||||
*
|
||||
* we record whether `x < 2` and `x > 0` evaluate to `true` or `false`, and
|
||||
* restrict the edges out of `x < 2 and x > 0` accordingly.
|
||||
*/
|
||||
class ConditionalCompletionSplit extends Split, TConditionalCompletionSplit {
|
||||
BooleanCompletion completion;
|
||||
|
||||
ConditionalCompletionSplit() { this = TConditionalCompletionSplit(completion) }
|
||||
|
||||
override string toString() { result = completion.toString() }
|
||||
}
|
||||
|
||||
private class ConditionalCompletionSplitKind extends SplitKind, TConditionalCompletionSplitKind {
|
||||
override int getListOrder() { result = 0 }
|
||||
|
||||
override predicate isEnabled(AstNode n) { this.appliesTo(n) }
|
||||
|
||||
override string toString() { result = "ConditionalCompletion" }
|
||||
}
|
||||
|
||||
int getNextListOrder() { result = 1 }
|
||||
|
||||
private class ConditionalCompletionSplitImpl extends SplitImpl, ConditionalCompletionSplit {
|
||||
override ConditionalCompletionSplitKind getKind() { any() }
|
||||
|
||||
override predicate hasEntry(AstNode pred, AstNode succ, Completion c) {
|
||||
succ(pred, succ, c) and
|
||||
last(succ, _, completion) and
|
||||
(
|
||||
last(succ.(LogicalNotAstNode).getOperand(), pred, c) and
|
||||
completion.(BooleanCompletion).getDual() = c
|
||||
or
|
||||
last(succ.(LogicalAndAstNode).getAnOperand(), pred, c) and
|
||||
completion = c
|
||||
or
|
||||
last(succ.(LogicalOrAstNode).getAnOperand(), pred, c) and
|
||||
completion = c
|
||||
or
|
||||
last(succ.(ParenthesizedStatement).getChild(), pred, c) and
|
||||
completion = c
|
||||
)
|
||||
}
|
||||
|
||||
override predicate hasEntryScope(CfgScope scope, AstNode succ) { none() }
|
||||
|
||||
override predicate hasExit(AstNode pred, AstNode succ, Completion c) {
|
||||
this.appliesTo(pred) and
|
||||
succ(pred, succ, c) and
|
||||
if c instanceof BooleanCompletion then completion = c else any()
|
||||
}
|
||||
|
||||
override predicate hasExitScope(AstNode last, CfgScope scope, Completion c) {
|
||||
this.appliesTo(last) and
|
||||
succExit(last, scope, c) and
|
||||
if c instanceof BooleanCompletion then completion = c else any()
|
||||
}
|
||||
|
||||
override predicate hasSuccessor(AstNode pred, AstNode succ, Completion c) { none() }
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* 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(last, scope, c) and
|
||||
forall(SplitImpl predSplit | predSplit = predSplits.getASplit() |
|
||||
predSplit.hasExitScope(last, scope, 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)
|
||||
)
|
||||
}
|
||||
}
|
||||
}
|
||||
319
ql/test/library-tests/controlflow/graph/Cfg.expected
Normal file
319
ql/test/library-tests/controlflow/graph/Cfg.expected
Normal file
@@ -0,0 +1,319 @@
|
||||
nodes
|
||||
| exit.rb:1:1:6:3 | enter m1 |
|
||||
| exit.rb:1:1:6:3 | exit m1 |
|
||||
| exit.rb:1:1:6:3 | exit m1 (abnormal) |
|
||||
| exit.rb:1:1:6:3 | exit m1 (normal) |
|
||||
| exit.rb:2:3:4:5 | If |
|
||||
| exit.rb:2:6:2:6 | x |
|
||||
| exit.rb:2:6:2:10 | Binary |
|
||||
| exit.rb:2:10:2:10 | 2 |
|
||||
| exit.rb:3:5:3:8 | exit |
|
||||
| exit.rb:3:5:3:10 | MethodCall |
|
||||
| exit.rb:3:10:3:10 | 1 |
|
||||
| exit.rb:5:3:5:6 | puts |
|
||||
| exit.rb:5:3:5:15 | MethodCall |
|
||||
| exit.rb:5:8:5:15 | String |
|
||||
| exit.rb:8:1:13:3 | enter m2 |
|
||||
| exit.rb:8:1:13:3 | exit m2 |
|
||||
| exit.rb:8:1:13:3 | exit m2 (abnormal) |
|
||||
| exit.rb:8:1:13:3 | exit m2 (normal) |
|
||||
| exit.rb:9:3:11:5 | If |
|
||||
| exit.rb:9:6:9:6 | x |
|
||||
| exit.rb:9:6:9:10 | Binary |
|
||||
| exit.rb:9:10:9:10 | 2 |
|
||||
| exit.rb:10:5:10:9 | abort |
|
||||
| exit.rb:10:5:10:18 | MethodCall |
|
||||
| exit.rb:10:11:10:18 | String |
|
||||
| exit.rb:12:3:12:6 | puts |
|
||||
| exit.rb:12:3:12:15 | MethodCall |
|
||||
| exit.rb:12:8:12:15 | String |
|
||||
| ifs.rb:1:1:9:3 | enter m1 |
|
||||
| ifs.rb:1:1:9:3 | exit m1 |
|
||||
| ifs.rb:1:1:9:3 | exit m1 (normal) |
|
||||
| ifs.rb:2:3:8:5 | If |
|
||||
| ifs.rb:2:6:2:6 | x |
|
||||
| ifs.rb:2:6:2:10 | Binary |
|
||||
| ifs.rb:2:10:2:10 | 2 |
|
||||
| ifs.rb:3:5:3:8 | puts |
|
||||
| ifs.rb:3:5:3:30 | MethodCall |
|
||||
| ifs.rb:3:10:3:30 | String |
|
||||
| ifs.rb:4:3:7:35 | Elsif |
|
||||
| ifs.rb:4:9:4:9 | x |
|
||||
| ifs.rb:4:9:4:14 | Binary |
|
||||
| ifs.rb:4:9:4:24 | [false] Binary |
|
||||
| ifs.rb:4:9:4:24 | [true] Binary |
|
||||
| ifs.rb:4:9:4:38 | [false] Binary |
|
||||
| ifs.rb:4:9:4:38 | [true] Binary |
|
||||
| ifs.rb:4:14:4:14 | 2 |
|
||||
| ifs.rb:4:20:4:20 | x |
|
||||
| ifs.rb:4:20:4:24 | Binary |
|
||||
| ifs.rb:4:24:4:24 | 0 |
|
||||
| ifs.rb:4:30:4:38 | [false] Unary |
|
||||
| ifs.rb:4:30:4:38 | [true] Unary |
|
||||
| ifs.rb:4:31:4:38 | [false] ParenthesizedStatements |
|
||||
| ifs.rb:4:31:4:38 | [true] ParenthesizedStatements |
|
||||
| ifs.rb:4:32:4:32 | x |
|
||||
| ifs.rb:4:32:4:37 | Binary |
|
||||
| ifs.rb:4:37:4:37 | 5 |
|
||||
| ifs.rb:5:5:5:8 | puts |
|
||||
| ifs.rb:5:5:5:17 | MethodCall |
|
||||
| ifs.rb:5:10:5:17 | String |
|
||||
| ifs.rb:7:5:7:8 | puts |
|
||||
| ifs.rb:7:5:7:35 | MethodCall |
|
||||
| ifs.rb:7:10:7:35 | String |
|
||||
| ifs.rb:11:1:16:3 | enter m2 |
|
||||
| ifs.rb:11:1:16:3 | exit m2 |
|
||||
| ifs.rb:11:1:16:3 | exit m2 (normal) |
|
||||
| ifs.rb:12:3:14:5 | If |
|
||||
| ifs.rb:12:6:12:6 | b |
|
||||
| ifs.rb:13:5:13:12 | Return |
|
||||
| ifs.rb:13:12:13:12 | 0 |
|
||||
| ifs.rb:15:3:15:10 | Return |
|
||||
| ifs.rb:15:10:15:10 | 1 |
|
||||
| ifs.rb:18:1:26:3 | enter m3 |
|
||||
| ifs.rb:18:1:26:3 | exit m3 |
|
||||
| ifs.rb:18:1:26:3 | exit m3 (normal) |
|
||||
| ifs.rb:19:3:24:5 | If |
|
||||
| ifs.rb:19:6:19:6 | x |
|
||||
| ifs.rb:19:6:19:10 | Binary |
|
||||
| ifs.rb:19:10:19:10 | 0 |
|
||||
| ifs.rb:20:5:20:5 | x |
|
||||
| ifs.rb:20:5:20:10 | Assignment |
|
||||
| ifs.rb:20:9:20:10 | Unary |
|
||||
| ifs.rb:20:10:20:10 | x |
|
||||
| ifs.rb:21:5:23:7 | If |
|
||||
| ifs.rb:21:8:21:8 | x |
|
||||
| ifs.rb:21:8:21:13 | Binary |
|
||||
| ifs.rb:21:12:21:13 | 10 |
|
||||
| ifs.rb:22:7:22:7 | x |
|
||||
| ifs.rb:22:7:22:15 | Assignment |
|
||||
| ifs.rb:22:11:22:11 | x |
|
||||
| ifs.rb:22:11:22:15 | Binary |
|
||||
| ifs.rb:22:15:22:15 | 1 |
|
||||
| ifs.rb:25:3:25:6 | puts |
|
||||
| ifs.rb:25:3:25:8 | MethodCall |
|
||||
| ifs.rb:25:8:25:8 | x |
|
||||
| loops.rb:1:1:6:3 | enter m1 |
|
||||
| loops.rb:1:1:6:3 | exit m1 |
|
||||
| loops.rb:1:1:6:3 | exit m1 (normal) |
|
||||
| loops.rb:2:3:5:5 | While |
|
||||
| loops.rb:2:9:2:9 | x |
|
||||
| loops.rb:2:9:2:14 | Binary |
|
||||
| loops.rb:2:14:2:14 | 0 |
|
||||
| loops.rb:3:5:3:8 | puts |
|
||||
| loops.rb:3:5:3:10 | MethodCall |
|
||||
| loops.rb:3:10:3:10 | x |
|
||||
| loops.rb:4:5:4:5 | x |
|
||||
| loops.rb:4:5:4:10 | OperatorAssignment |
|
||||
| loops.rb:4:10:4:10 | 1 |
|
||||
| loops.rb:8:1:22:3 | enter m2 |
|
||||
| loops.rb:8:1:22:3 | exit m2 |
|
||||
| loops.rb:8:1:22:3 | exit m2 (normal) |
|
||||
| loops.rb:9:3:20:5 | While |
|
||||
| loops.rb:9:9:9:9 | x |
|
||||
| loops.rb:9:9:9:14 | Binary |
|
||||
| loops.rb:9:14:9:14 | 0 |
|
||||
| loops.rb:10:5:10:8 | puts |
|
||||
| loops.rb:10:5:10:10 | MethodCall |
|
||||
| loops.rb:10:10:10:10 | x |
|
||||
| loops.rb:11:5:11:5 | x |
|
||||
| loops.rb:11:5:11:10 | OperatorAssignment |
|
||||
| loops.rb:11:10:11:10 | 1 |
|
||||
| loops.rb:12:5:18:7 | If |
|
||||
| loops.rb:12:8:12:8 | x |
|
||||
| loops.rb:12:8:12:14 | Binary |
|
||||
| loops.rb:12:12:12:14 | 100 |
|
||||
| loops.rb:13:7:13:11 | Break |
|
||||
| loops.rb:14:5:17:10 | Elsif |
|
||||
| loops.rb:14:11:14:11 | x |
|
||||
| loops.rb:14:11:14:16 | Binary |
|
||||
| loops.rb:14:15:14:16 | 50 |
|
||||
| loops.rb:15:7:15:10 | Next |
|
||||
| loops.rb:16:5:17:10 | Elsif |
|
||||
| loops.rb:16:11:16:11 | x |
|
||||
| loops.rb:16:11:16:16 | Binary |
|
||||
| loops.rb:16:15:16:16 | 10 |
|
||||
| loops.rb:17:7:17:10 | Redo |
|
||||
| loops.rb:19:5:19:8 | puts |
|
||||
| loops.rb:19:5:19:15 | MethodCall |
|
||||
| loops.rb:19:10:19:15 | String |
|
||||
| loops.rb:21:3:21:6 | puts |
|
||||
| loops.rb:21:3:21:13 | MethodCall |
|
||||
| loops.rb:21:8:21:13 | String |
|
||||
| raise.rb:1:1:6:3 | enter m1 |
|
||||
| raise.rb:1:1:6:3 | exit m1 |
|
||||
| raise.rb:1:1:6:3 | exit m1 (abnormal) |
|
||||
| raise.rb:1:1:6:3 | exit m1 (normal) |
|
||||
| raise.rb:2:3:4:5 | If |
|
||||
| raise.rb:2:6:2:6 | x |
|
||||
| raise.rb:2:6:2:10 | Binary |
|
||||
| raise.rb:2:10:2:10 | 2 |
|
||||
| raise.rb:3:5:3:9 | raise |
|
||||
| raise.rb:3:5:3:17 | MethodCall |
|
||||
| raise.rb:3:11:3:17 | String |
|
||||
| raise.rb:5:3:5:6 | puts |
|
||||
| raise.rb:5:3:5:15 | MethodCall |
|
||||
| raise.rb:5:8:5:15 | String |
|
||||
edges
|
||||
| exit.rb:1:1:6:3 | enter m1 | exit.rb:2:3:4:5 | If | semmle.label | successor |
|
||||
| exit.rb:1:1:6:3 | exit m1 (abnormal) | exit.rb:1:1:6:3 | exit m1 | semmle.label | successor |
|
||||
| exit.rb:1:1:6:3 | exit m1 (normal) | exit.rb:1:1:6:3 | exit m1 | semmle.label | successor |
|
||||
| exit.rb:2:3:4:5 | If | exit.rb:2:6:2:6 | x | semmle.label | successor |
|
||||
| exit.rb:2:6:2:6 | x | exit.rb:2:10:2:10 | 2 | semmle.label | successor |
|
||||
| exit.rb:2:6:2:10 | Binary | exit.rb:3:10:3:10 | 1 | semmle.label | true |
|
||||
| exit.rb:2:6:2:10 | Binary | exit.rb:5:8:5:15 | String | semmle.label | false |
|
||||
| exit.rb:2:10:2:10 | 2 | exit.rb:2:6:2:10 | Binary | semmle.label | successor |
|
||||
| exit.rb:3:5:3:8 | exit | exit.rb:3:5:3:10 | MethodCall | semmle.label | successor |
|
||||
| exit.rb:3:5:3:10 | MethodCall | exit.rb:1:1:6:3 | exit m1 (abnormal) | semmle.label | exit |
|
||||
| exit.rb:3:10:3:10 | 1 | exit.rb:3:5:3:8 | exit | semmle.label | successor |
|
||||
| exit.rb:5:3:5:6 | puts | exit.rb:5:3:5:15 | MethodCall | semmle.label | successor |
|
||||
| exit.rb:5:3:5:15 | MethodCall | exit.rb:1:1:6:3 | exit m1 (normal) | semmle.label | successor |
|
||||
| exit.rb:5:8:5:15 | String | exit.rb:5:3:5:6 | puts | semmle.label | successor |
|
||||
| exit.rb:8:1:13:3 | enter m2 | exit.rb:9:3:11:5 | If | semmle.label | successor |
|
||||
| exit.rb:8:1:13:3 | exit m2 (abnormal) | exit.rb:8:1:13:3 | exit m2 | semmle.label | successor |
|
||||
| exit.rb:8:1:13:3 | exit m2 (normal) | exit.rb:8:1:13:3 | exit m2 | semmle.label | successor |
|
||||
| exit.rb:9:3:11:5 | If | exit.rb:9:6:9:6 | x | semmle.label | successor |
|
||||
| exit.rb:9:6:9:6 | x | exit.rb:9:10:9:10 | 2 | semmle.label | successor |
|
||||
| exit.rb:9:6:9:10 | Binary | exit.rb:10:11:10:18 | String | semmle.label | true |
|
||||
| exit.rb:9:6:9:10 | Binary | exit.rb:12:8:12:15 | String | semmle.label | false |
|
||||
| exit.rb:9:10:9:10 | 2 | exit.rb:9:6:9:10 | Binary | semmle.label | successor |
|
||||
| exit.rb:10:5:10:9 | abort | exit.rb:10:5:10:18 | MethodCall | semmle.label | successor |
|
||||
| exit.rb:10:5:10:18 | MethodCall | exit.rb:8:1:13:3 | exit m2 (abnormal) | semmle.label | exit |
|
||||
| exit.rb:10:11:10:18 | String | exit.rb:10:5:10:9 | abort | semmle.label | successor |
|
||||
| exit.rb:12:3:12:6 | puts | exit.rb:12:3:12:15 | MethodCall | semmle.label | successor |
|
||||
| exit.rb:12:3:12:15 | MethodCall | exit.rb:8:1:13:3 | exit m2 (normal) | semmle.label | successor |
|
||||
| exit.rb:12:8:12:15 | String | exit.rb:12:3:12:6 | puts | semmle.label | successor |
|
||||
| ifs.rb:1:1:9:3 | enter m1 | ifs.rb:2:3:8:5 | If | semmle.label | successor |
|
||||
| ifs.rb:1:1:9:3 | exit m1 (normal) | ifs.rb:1:1:9:3 | exit m1 | semmle.label | successor |
|
||||
| ifs.rb:2:3:8:5 | If | ifs.rb:2:6:2:6 | x | semmle.label | successor |
|
||||
| ifs.rb:2:6:2:6 | x | ifs.rb:2:10:2:10 | 2 | semmle.label | successor |
|
||||
| ifs.rb:2:6:2:10 | Binary | ifs.rb:3:10:3:30 | String | semmle.label | true |
|
||||
| ifs.rb:2:6:2:10 | Binary | ifs.rb:4:3:7:35 | Elsif | semmle.label | false |
|
||||
| ifs.rb:2:10:2:10 | 2 | ifs.rb:2:6:2:10 | Binary | semmle.label | successor |
|
||||
| ifs.rb:3:5:3:8 | puts | ifs.rb:3:5:3:30 | MethodCall | semmle.label | successor |
|
||||
| ifs.rb:3:5:3:30 | MethodCall | ifs.rb:1:1:9:3 | exit m1 (normal) | semmle.label | successor |
|
||||
| ifs.rb:3:10:3:30 | String | ifs.rb:3:5:3:8 | puts | semmle.label | successor |
|
||||
| ifs.rb:4:3:7:35 | Elsif | ifs.rb:4:9:4:9 | x | semmle.label | successor |
|
||||
| ifs.rb:4:9:4:9 | x | ifs.rb:4:14:4:14 | 2 | semmle.label | successor |
|
||||
| ifs.rb:4:9:4:14 | Binary | ifs.rb:4:9:4:24 | [false] Binary | semmle.label | false |
|
||||
| ifs.rb:4:9:4:14 | Binary | ifs.rb:4:20:4:20 | x | semmle.label | true |
|
||||
| ifs.rb:4:9:4:24 | [false] Binary | ifs.rb:4:9:4:38 | [false] Binary | semmle.label | false |
|
||||
| ifs.rb:4:9:4:24 | [true] Binary | ifs.rb:4:32:4:32 | x | semmle.label | true |
|
||||
| ifs.rb:4:9:4:38 | [false] Binary | ifs.rb:7:10:7:35 | String | semmle.label | false |
|
||||
| ifs.rb:4:9:4:38 | [true] Binary | ifs.rb:5:10:5:17 | String | semmle.label | true |
|
||||
| ifs.rb:4:14:4:14 | 2 | ifs.rb:4:9:4:14 | Binary | semmle.label | successor |
|
||||
| ifs.rb:4:20:4:20 | x | ifs.rb:4:24:4:24 | 0 | semmle.label | successor |
|
||||
| ifs.rb:4:20:4:24 | Binary | ifs.rb:4:9:4:24 | [false] Binary | semmle.label | false |
|
||||
| ifs.rb:4:20:4:24 | Binary | ifs.rb:4:9:4:24 | [true] Binary | semmle.label | true |
|
||||
| ifs.rb:4:24:4:24 | 0 | ifs.rb:4:20:4:24 | Binary | semmle.label | successor |
|
||||
| ifs.rb:4:30:4:38 | [false] Unary | ifs.rb:4:9:4:38 | [false] Binary | semmle.label | false |
|
||||
| ifs.rb:4:30:4:38 | [true] Unary | ifs.rb:4:9:4:38 | [true] Binary | semmle.label | true |
|
||||
| ifs.rb:4:31:4:38 | [false] ParenthesizedStatements | ifs.rb:4:30:4:38 | [true] Unary | semmle.label | false |
|
||||
| ifs.rb:4:31:4:38 | [true] ParenthesizedStatements | ifs.rb:4:30:4:38 | [false] Unary | semmle.label | true |
|
||||
| ifs.rb:4:32:4:32 | x | ifs.rb:4:37:4:37 | 5 | semmle.label | successor |
|
||||
| ifs.rb:4:32:4:37 | Binary | ifs.rb:4:31:4:38 | [false] ParenthesizedStatements | semmle.label | false |
|
||||
| ifs.rb:4:32:4:37 | Binary | ifs.rb:4:31:4:38 | [true] ParenthesizedStatements | semmle.label | true |
|
||||
| ifs.rb:4:37:4:37 | 5 | ifs.rb:4:32:4:37 | Binary | semmle.label | successor |
|
||||
| ifs.rb:5:5:5:8 | puts | ifs.rb:5:5:5:17 | MethodCall | semmle.label | successor |
|
||||
| ifs.rb:5:5:5:17 | MethodCall | ifs.rb:1:1:9:3 | exit m1 (normal) | semmle.label | successor |
|
||||
| ifs.rb:5:10:5:17 | String | ifs.rb:5:5:5:8 | puts | semmle.label | successor |
|
||||
| ifs.rb:7:5:7:8 | puts | ifs.rb:7:5:7:35 | MethodCall | semmle.label | successor |
|
||||
| ifs.rb:7:5:7:35 | MethodCall | ifs.rb:1:1:9:3 | exit m1 (normal) | semmle.label | successor |
|
||||
| ifs.rb:7:10:7:35 | String | ifs.rb:7:5:7:8 | puts | semmle.label | successor |
|
||||
| ifs.rb:11:1:16:3 | enter m2 | ifs.rb:12:3:14:5 | If | semmle.label | successor |
|
||||
| ifs.rb:11:1:16:3 | exit m2 (normal) | ifs.rb:11:1:16:3 | exit m2 | semmle.label | successor |
|
||||
| ifs.rb:12:3:14:5 | If | ifs.rb:12:6:12:6 | b | semmle.label | successor |
|
||||
| ifs.rb:12:6:12:6 | b | ifs.rb:13:12:13:12 | 0 | semmle.label | true |
|
||||
| ifs.rb:12:6:12:6 | b | ifs.rb:15:10:15:10 | 1 | semmle.label | false |
|
||||
| ifs.rb:13:5:13:12 | Return | ifs.rb:11:1:16:3 | exit m2 (normal) | semmle.label | return |
|
||||
| ifs.rb:13:12:13:12 | 0 | ifs.rb:13:5:13:12 | Return | semmle.label | successor |
|
||||
| ifs.rb:15:3:15:10 | Return | ifs.rb:11:1:16:3 | exit m2 (normal) | semmle.label | return |
|
||||
| ifs.rb:15:10:15:10 | 1 | ifs.rb:15:3:15:10 | Return | semmle.label | successor |
|
||||
| ifs.rb:18:1:26:3 | enter m3 | ifs.rb:19:3:24:5 | If | semmle.label | successor |
|
||||
| ifs.rb:18:1:26:3 | exit m3 (normal) | ifs.rb:18:1:26:3 | exit m3 | semmle.label | successor |
|
||||
| ifs.rb:19:3:24:5 | If | ifs.rb:19:6:19:6 | x | semmle.label | successor |
|
||||
| ifs.rb:19:6:19:6 | x | ifs.rb:19:10:19:10 | 0 | semmle.label | successor |
|
||||
| ifs.rb:19:6:19:10 | Binary | ifs.rb:20:5:20:5 | x | semmle.label | true |
|
||||
| ifs.rb:19:6:19:10 | Binary | ifs.rb:25:8:25:8 | x | semmle.label | false |
|
||||
| ifs.rb:19:10:19:10 | 0 | ifs.rb:19:6:19:10 | Binary | semmle.label | successor |
|
||||
| ifs.rb:20:5:20:5 | x | ifs.rb:20:10:20:10 | x | semmle.label | successor |
|
||||
| ifs.rb:20:5:20:10 | Assignment | ifs.rb:21:5:23:7 | If | semmle.label | successor |
|
||||
| ifs.rb:20:9:20:10 | Unary | ifs.rb:20:5:20:10 | Assignment | semmle.label | successor |
|
||||
| ifs.rb:20:10:20:10 | x | ifs.rb:20:9:20:10 | Unary | semmle.label | successor |
|
||||
| ifs.rb:21:5:23:7 | If | ifs.rb:21:8:21:8 | x | semmle.label | successor |
|
||||
| ifs.rb:21:8:21:8 | x | ifs.rb:21:12:21:13 | 10 | semmle.label | successor |
|
||||
| ifs.rb:21:8:21:13 | Binary | ifs.rb:22:7:22:7 | x | semmle.label | true |
|
||||
| ifs.rb:21:8:21:13 | Binary | ifs.rb:25:8:25:8 | x | semmle.label | false |
|
||||
| ifs.rb:21:12:21:13 | 10 | ifs.rb:21:8:21:13 | Binary | semmle.label | successor |
|
||||
| ifs.rb:22:7:22:7 | x | ifs.rb:22:11:22:11 | x | semmle.label | successor |
|
||||
| ifs.rb:22:7:22:15 | Assignment | ifs.rb:25:8:25:8 | x | semmle.label | successor |
|
||||
| ifs.rb:22:11:22:11 | x | ifs.rb:22:15:22:15 | 1 | semmle.label | successor |
|
||||
| ifs.rb:22:11:22:15 | Binary | ifs.rb:22:7:22:15 | Assignment | semmle.label | successor |
|
||||
| ifs.rb:22:15:22:15 | 1 | ifs.rb:22:11:22:15 | Binary | semmle.label | successor |
|
||||
| ifs.rb:25:3:25:6 | puts | ifs.rb:25:3:25:8 | MethodCall | semmle.label | successor |
|
||||
| ifs.rb:25:3:25:8 | MethodCall | ifs.rb:18:1:26:3 | exit m3 (normal) | semmle.label | successor |
|
||||
| ifs.rb:25:8:25:8 | x | ifs.rb:25:3:25:6 | puts | semmle.label | successor |
|
||||
| loops.rb:1:1:6:3 | enter m1 | loops.rb:2:3:5:5 | While | semmle.label | successor |
|
||||
| loops.rb:1:1:6:3 | exit m1 (normal) | loops.rb:1:1:6:3 | exit m1 | semmle.label | successor |
|
||||
| loops.rb:2:3:5:5 | While | loops.rb:2:9:2:9 | x | semmle.label | successor |
|
||||
| loops.rb:2:9:2:9 | x | loops.rb:2:14:2:14 | 0 | semmle.label | successor |
|
||||
| loops.rb:2:9:2:14 | Binary | loops.rb:1:1:6:3 | exit m1 (normal) | semmle.label | false |
|
||||
| loops.rb:2:9:2:14 | Binary | loops.rb:3:10:3:10 | x | semmle.label | true |
|
||||
| loops.rb:2:14:2:14 | 0 | loops.rb:2:9:2:14 | Binary | semmle.label | successor |
|
||||
| loops.rb:3:5:3:8 | puts | loops.rb:3:5:3:10 | MethodCall | semmle.label | successor |
|
||||
| loops.rb:3:5:3:10 | MethodCall | loops.rb:4:5:4:5 | x | semmle.label | successor |
|
||||
| loops.rb:3:10:3:10 | x | loops.rb:3:5:3:8 | puts | semmle.label | successor |
|
||||
| loops.rb:4:5:4:5 | x | loops.rb:4:10:4:10 | 1 | semmle.label | successor |
|
||||
| loops.rb:4:5:4:10 | OperatorAssignment | loops.rb:2:9:2:9 | x | semmle.label | successor |
|
||||
| loops.rb:4:10:4:10 | 1 | loops.rb:4:5:4:10 | OperatorAssignment | semmle.label | successor |
|
||||
| loops.rb:8:1:22:3 | enter m2 | loops.rb:9:3:20:5 | While | semmle.label | successor |
|
||||
| loops.rb:8:1:22:3 | exit m2 (normal) | loops.rb:8:1:22:3 | exit m2 | semmle.label | successor |
|
||||
| loops.rb:9:3:20:5 | While | loops.rb:9:9:9:9 | x | semmle.label | successor |
|
||||
| loops.rb:9:9:9:9 | x | loops.rb:9:14:9:14 | 0 | semmle.label | successor |
|
||||
| loops.rb:9:9:9:14 | Binary | loops.rb:10:10:10:10 | x | semmle.label | true |
|
||||
| loops.rb:9:9:9:14 | Binary | loops.rb:21:8:21:13 | String | semmle.label | false |
|
||||
| loops.rb:9:14:9:14 | 0 | loops.rb:9:9:9:14 | Binary | semmle.label | successor |
|
||||
| loops.rb:10:5:10:8 | puts | loops.rb:10:5:10:10 | MethodCall | semmle.label | successor |
|
||||
| loops.rb:10:5:10:10 | MethodCall | loops.rb:11:5:11:5 | x | semmle.label | successor |
|
||||
| loops.rb:10:10:10:10 | x | loops.rb:10:5:10:8 | puts | semmle.label | successor |
|
||||
| loops.rb:11:5:11:5 | x | loops.rb:11:10:11:10 | 1 | semmle.label | successor |
|
||||
| loops.rb:11:5:11:10 | OperatorAssignment | loops.rb:12:5:18:7 | If | semmle.label | successor |
|
||||
| loops.rb:11:10:11:10 | 1 | loops.rb:11:5:11:10 | OperatorAssignment | semmle.label | successor |
|
||||
| loops.rb:12:5:18:7 | If | loops.rb:12:8:12:8 | x | semmle.label | successor |
|
||||
| loops.rb:12:8:12:8 | x | loops.rb:12:12:12:14 | 100 | semmle.label | successor |
|
||||
| loops.rb:12:8:12:14 | Binary | loops.rb:13:7:13:11 | Break | semmle.label | true |
|
||||
| loops.rb:12:8:12:14 | Binary | loops.rb:14:5:17:10 | Elsif | semmle.label | false |
|
||||
| loops.rb:12:12:12:14 | 100 | loops.rb:12:8:12:14 | Binary | semmle.label | successor |
|
||||
| loops.rb:13:7:13:11 | Break | loops.rb:21:8:21:13 | String | semmle.label | break |
|
||||
| loops.rb:14:5:17:10 | Elsif | loops.rb:14:11:14:11 | x | semmle.label | successor |
|
||||
| loops.rb:14:11:14:11 | x | loops.rb:14:15:14:16 | 50 | semmle.label | successor |
|
||||
| loops.rb:14:11:14:16 | Binary | loops.rb:15:7:15:10 | Next | semmle.label | true |
|
||||
| loops.rb:14:11:14:16 | Binary | loops.rb:16:5:17:10 | Elsif | semmle.label | false |
|
||||
| loops.rb:14:15:14:16 | 50 | loops.rb:14:11:14:16 | Binary | semmle.label | successor |
|
||||
| loops.rb:15:7:15:10 | Next | loops.rb:9:9:9:9 | x | semmle.label | next |
|
||||
| loops.rb:16:5:17:10 | Elsif | loops.rb:16:11:16:11 | x | semmle.label | successor |
|
||||
| loops.rb:16:11:16:11 | x | loops.rb:16:15:16:16 | 10 | semmle.label | successor |
|
||||
| loops.rb:16:11:16:16 | Binary | loops.rb:17:7:17:10 | Redo | semmle.label | true |
|
||||
| loops.rb:16:11:16:16 | Binary | loops.rb:19:10:19:15 | String | semmle.label | false |
|
||||
| loops.rb:16:15:16:16 | 10 | loops.rb:16:11:16:16 | Binary | semmle.label | successor |
|
||||
| loops.rb:17:7:17:10 | Redo | loops.rb:10:10:10:10 | x | semmle.label | successor |
|
||||
| loops.rb:19:5:19:8 | puts | loops.rb:19:5:19:15 | MethodCall | semmle.label | successor |
|
||||
| loops.rb:19:5:19:15 | MethodCall | loops.rb:9:9:9:9 | x | semmle.label | successor |
|
||||
| loops.rb:19:10:19:15 | String | loops.rb:19:5:19:8 | puts | semmle.label | successor |
|
||||
| loops.rb:21:3:21:6 | puts | loops.rb:21:3:21:13 | MethodCall | semmle.label | successor |
|
||||
| loops.rb:21:3:21:13 | MethodCall | loops.rb:8:1:22:3 | exit m2 (normal) | semmle.label | successor |
|
||||
| loops.rb:21:8:21:13 | String | loops.rb:21:3:21:6 | puts | semmle.label | successor |
|
||||
| raise.rb:1:1:6:3 | enter m1 | raise.rb:2:3:4:5 | If | semmle.label | successor |
|
||||
| raise.rb:1:1:6:3 | exit m1 (abnormal) | raise.rb:1:1:6:3 | exit m1 | semmle.label | successor |
|
||||
| raise.rb:1:1:6:3 | exit m1 (normal) | raise.rb:1:1:6:3 | exit m1 | semmle.label | successor |
|
||||
| raise.rb:2:3:4:5 | If | raise.rb:2:6:2:6 | x | semmle.label | successor |
|
||||
| raise.rb:2:6:2:6 | x | raise.rb:2:10:2:10 | 2 | semmle.label | successor |
|
||||
| raise.rb:2:6:2:10 | Binary | raise.rb:3:11:3:17 | String | semmle.label | true |
|
||||
| raise.rb:2:6:2:10 | Binary | raise.rb:5:8:5:15 | String | semmle.label | false |
|
||||
| raise.rb:2:10:2:10 | 2 | raise.rb:2:6:2:10 | Binary | semmle.label | successor |
|
||||
| raise.rb:3:5:3:9 | raise | raise.rb:3:5:3:17 | MethodCall | semmle.label | successor |
|
||||
| raise.rb:3:5:3:17 | MethodCall | raise.rb:1:1:6:3 | exit m1 (abnormal) | semmle.label | raise |
|
||||
| raise.rb:3:11:3:17 | String | raise.rb:3:5:3:9 | raise | semmle.label | successor |
|
||||
| raise.rb:5:3:5:6 | puts | raise.rb:5:3:5:15 | MethodCall | semmle.label | successor |
|
||||
| raise.rb:5:3:5:15 | MethodCall | raise.rb:1:1:6:3 | exit m1 (normal) | semmle.label | successor |
|
||||
| raise.rb:5:8:5:15 | String | raise.rb:5:3:5:6 | puts | semmle.label | successor |
|
||||
1
ql/test/library-tests/controlflow/graph/Cfg.qlref
Normal file
1
ql/test/library-tests/controlflow/graph/Cfg.qlref
Normal file
@@ -0,0 +1 @@
|
||||
codeql_ruby/controlflow/internal/Cfg.ql
|
||||
13
ql/test/library-tests/controlflow/graph/exit.rb
Normal file
13
ql/test/library-tests/controlflow/graph/exit.rb
Normal file
@@ -0,0 +1,13 @@
|
||||
def m1 x
|
||||
if x > 2
|
||||
exit 1
|
||||
end
|
||||
puts "x <= 2"
|
||||
end
|
||||
|
||||
def m2 x
|
||||
if x > 2
|
||||
abort "abort!"
|
||||
end
|
||||
puts "x <= 2"
|
||||
end
|
||||
26
ql/test/library-tests/controlflow/graph/ifs.rb
Normal file
26
ql/test/library-tests/controlflow/graph/ifs.rb
Normal file
@@ -0,0 +1,26 @@
|
||||
def m1 x
|
||||
if x > 2
|
||||
puts "x is greater than 2"
|
||||
elsif x <= 2 and x > 0 and !(x == 5)
|
||||
puts "x is 1"
|
||||
else
|
||||
puts "I can't guess the number"
|
||||
end
|
||||
end
|
||||
|
||||
def m2 b
|
||||
if b
|
||||
return 0
|
||||
end
|
||||
return 1
|
||||
end
|
||||
|
||||
def m3 x
|
||||
if x < 0
|
||||
x = -x
|
||||
if x > 10
|
||||
x = x - 1
|
||||
end
|
||||
end
|
||||
puts x
|
||||
end
|
||||
22
ql/test/library-tests/controlflow/graph/loops.rb
Normal file
22
ql/test/library-tests/controlflow/graph/loops.rb
Normal file
@@ -0,0 +1,22 @@
|
||||
def m1 x
|
||||
while x >= 0
|
||||
puts x
|
||||
x -= 1
|
||||
end
|
||||
end
|
||||
|
||||
def m2 x
|
||||
while x >= 0
|
||||
puts x
|
||||
x -= 1
|
||||
if x > 100
|
||||
break
|
||||
elsif x > 50
|
||||
next
|
||||
elsif x > 10
|
||||
redo
|
||||
end
|
||||
puts "Iter"
|
||||
end
|
||||
puts "Done"
|
||||
end
|
||||
6
ql/test/library-tests/controlflow/graph/raise.rb
Normal file
6
ql/test/library-tests/controlflow/graph/raise.rb
Normal file
@@ -0,0 +1,6 @@
|
||||
def m1 x
|
||||
if x > 2
|
||||
raise "x > 2"
|
||||
end
|
||||
puts "x <= 2"
|
||||
end
|
||||
Reference in New Issue
Block a user