CFG: for-in loop

This commit is contained in:
Arthur Baars
2020-11-27 16:30:36 +01:00
parent 165b2b37dc
commit 6660cb4417
3 changed files with 173 additions and 3 deletions

View File

@@ -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.
*

View File

@@ -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.

View File

@@ -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