From 6660cb4417dc59fa805c8016a94cfae5da54327b Mon Sep 17 00:00:00 2001 From: Arthur Baars Date: Fri, 27 Nov 2020 16:30:36 +0100 Subject: [PATCH] CFG: for-in loop --- .../controlflow/ControlFlowGraph.qll | 53 +++++++++- .../controlflow/internal/Completion.qll | 25 ++++- .../internal/ControlFlowGraphImpl.qll | 98 +++++++++++++++++++ 3 files changed, 173 insertions(+), 3 deletions(-) diff --git a/ql/src/codeql_ruby/controlflow/ControlFlowGraph.qll b/ql/src/codeql_ruby/controlflow/ControlFlowGraph.qll index 3fb4058aa7e..e5080230046 100644 --- a/ql/src/codeql_ruby/controlflow/ControlFlowGraph.qll +++ b/ql/src/codeql_ruby/controlflow/ControlFlowGraph.qll @@ -179,6 +179,15 @@ module SuccessorTypes { final override string toString() { result = "successor" } } + /** + * A conditional control flow successor. Either a Boolean successor (`BooleanSuccessor`), + * or an emptiness successor (`EmptinessSuccessor`). + */ + abstract class ConditionalSuccessor extends SuccessorType { + /** Gets the Boolean value of this successor. */ + abstract boolean getValue(); + } + /** * A Boolean control flow successor. * @@ -194,13 +203,53 @@ module SuccessorTypes { * * `x >= 0` has both a `true` successor and a `false` successor. */ - class BooleanSuccessor extends SuccessorType, TBooleanSuccessor { + class BooleanSuccessor extends ConditionalSuccessor, TBooleanSuccessor { /** Gets the Boolean value. */ - final boolean getValue() { this = TBooleanSuccessor(result) } + final override boolean getValue() { this = TBooleanSuccessor(result) } final override string toString() { result = getValue().toString() } } + /** + * An emptiness control flow successor. + * + * For example, this program fragment: + * + * ```rb + * for arg in args do + * puts arg + * end + * puts "done"; + * ``` + * + * has a control flow graph containing emptiness successors: + * + * ``` + * args + * | + * for------<----- + * / \ \ + * / \ | + * / \ | + * / \ | + * empty non-empty | + * | \ | + * puts "done" \ | + * arg | + * | | + * puts arg | + * \___/ + * ``` + */ + class EmptinessSuccessor extends ConditionalSuccessor, TEmptinessSuccessor { + /** Holds if this is an empty successor. */ + predicate isEmpty() { this = TEmptinessSuccessor(true) } + + override boolean getValue() { this = TEmptinessSuccessor(result) } + + override string toString() { if this.isEmpty() then result = "empty" else result = "non-empty" } + } + /** * A `return` control flow successor. * diff --git a/ql/src/codeql_ruby/controlflow/internal/Completion.qll b/ql/src/codeql_ruby/controlflow/internal/Completion.qll index 29f51c46111..9ed60d2572f 100644 --- a/ql/src/codeql_ruby/controlflow/internal/Completion.qll +++ b/ql/src/codeql_ruby/controlflow/internal/Completion.qll @@ -13,6 +13,7 @@ private import SuccessorTypes private newtype TCompletion = TSimpleCompletion() or TBooleanCompletion(boolean b) { b = true or b = false } or + TEmptinessCompletion(boolean isEmpty) { isEmpty = true or isEmpty = false } or TReturnCompletion() or TBreakCompletion() or TNextCompletion() or @@ -151,11 +152,18 @@ class SimpleCompletion extends NormalCompletion, TSimpleCompletion { override string toString() { result = "simple" } } +/** + * A completion that represents evaluation of an expression, whose value determines + * the successor. Either a Boolean completion (`BooleanCompletion`) + * or an emptiness completion (`EmptinessCompletion`). + */ +abstract class ConditionalCompletion extends NormalCompletion { } + /** * A completion that represents evaluation of an expression * with a Boolean value. */ -class BooleanCompletion extends NormalCompletion, TBooleanCompletion { +class BooleanCompletion extends ConditionalCompletion, TBooleanCompletion { private boolean value; BooleanCompletion() { this = TBooleanCompletion(value) } @@ -181,6 +189,21 @@ class FalseCompletion extends BooleanCompletion { FalseCompletion() { this.getValue() = false } } +/** + * A completion that represents evaluation of an emptiness test, for example + * a test in a `for in` statement. + */ +class EmptinessCompletion extends ConditionalCompletion, TEmptinessCompletion { + /** Holds if the emptiness test evaluates to `true`. */ + predicate isEmpty() { this = TEmptinessCompletion(true) } + + override EmptinessSuccessor getAMatchingSuccessorType() { + if isEmpty() then result.getValue() = true else result.getValue() = false + } + + override string toString() { if this.isEmpty() then result = "empty" else result = "non-empty" } +} + /** * A completion that represents evaluation of a statement or an * expression resulting in a return. diff --git a/ql/src/codeql_ruby/controlflow/internal/ControlFlowGraphImpl.qll b/ql/src/codeql_ruby/controlflow/internal/ControlFlowGraphImpl.qll index eeca3675c03..84ca1c39936 100644 --- a/ql/src/codeql_ruby/controlflow/internal/ControlFlowGraphImpl.qll +++ b/ql/src/codeql_ruby/controlflow/internal/ControlFlowGraphImpl.qll @@ -304,6 +304,97 @@ private module Trees { final override AstNode getChildNode(int i) { result = this.getChild(i) } } + /** + * Control flow of a for-in loop + * + * For example, this program fragment: + * + * ```rb + * for arg in args do + * puts arg + * end + * puts "done"; + * ``` + * + * has the following control flow graph: + * + * ``` + * args + * | + * for------<----- + * / \ \ + * / \ | + * / \ | + * / \ | + * empty non-empty | + * | \ | + * puts "done" \ | + * arg | + * | | + * puts arg | + * \___/ + * ``` + */ + private class ForTree extends ControlFlowTree, For { + final override predicate propagatesAbnormal(AstNode child) { + child = this.getPattern(_) or child = this.getValue() + } + + final override predicate first(AstNode node) { node = this.getValue() } + + final override predicate last(AstNode last, Completion c) { + last = this and + c.(EmptinessCompletion).isEmpty() + 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 + ) + } + + /** + * for pattern in value do body end + * ``` + * value +-> for +--[non empty]--> pattern -> body -> for + * |--[empty]--> exit + * ``` + */ + final override predicate succ(AstNode pred, AstNode succ, Completion c) { + last(this.getValue(), pred, c) and + succ = this and + c instanceof SimpleCompletion + or + pred = this and + first(this.getPattern(0), succ) and + c instanceof EmptinessCompletion and + not c.(EmptinessCompletion).isEmpty() + or + exists(int i, ControlFlowTree next | + last(this.getPattern(i), pred, c) and + first(next, succ) and + c instanceof SimpleCompletion + | + next = this.getPattern(i + 1) + or + not exists(this.getPattern(i + 1)) and next = this.getBody() + ) + or + last(this.getBody(), pred, c) and + succ = this and + c.continuesLoop() + or + last(this.getBody(), pred, any(RedoCompletion rc)) and + first(this.getBody(), succ) and + c instanceof SimpleCompletion + } + } + private class IdentifierTree extends LeafTree, Identifier { } private class IfElsifTree extends PreOrderTree, IfElsifAstNode { @@ -333,6 +424,12 @@ private module Trees { } } + private class InTree extends StandardPreOrderTree, In { + final override AstNode getChildNode(int i) { result = this.getChild() and i = 0 } + + override predicate isHidden() { any() } + } + private class IntegerTree extends LeafTree, Integer { } class LogicalAndTree extends PostOrderTree, LogicalAndAstNode { @@ -535,6 +632,7 @@ private module Cached { newtype TSuccessorType = TSuccessorSuccessor() or TBooleanSuccessor(boolean b) { b = true or b = false } or + TEmptinessSuccessor(boolean isEmpty) { isEmpty = true or isEmpty = false } or TReturnSuccessor() or TBreakSuccessor() or TNextSuccessor() or