CFG: Model IfElsifAstNode in post-order

This commit is contained in:
Tom Hvitved
2020-12-14 14:31:53 +01:00
parent bb88858633
commit 9aadeedeb9
5 changed files with 283 additions and 246 deletions

View File

@@ -47,53 +47,59 @@ private class If_or_elisif =
class IfElsifAstNode extends AstNode, If_or_elisif {
AstNode getConditionNode() { none() }
AstNode getConsequenceNode() { none() }
AstNode getAlternativeNode() { none() }
AstNode getBranch(boolean b) { 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() }
override AstNode getBranch(boolean b) {
b = true and result = this.getConsequence()
or
b = false and 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() }
override AstNode getBranch(boolean b) {
b = true and result = this.getConsequence()
or
b = false and result = this.getAlternative()
}
}
private class ConditionalAstNode extends IfElsifAstNode, Conditional {
override AstNode getConditionNode() { result = this.getCondition() }
override AstNode getConsequenceNode() { result = this.getConsequence() }
override AstNode getAlternativeNode() { result = this.getAlternative() }
override AstNode getBranch(boolean b) {
b = true and result = this.getConsequence()
or
b = false and result = this.getAlternative()
}
}
private class IfModifierAstNode extends IfElsifAstNode, IfModifier {
override AstNode getConditionNode() { result = this.getCondition() }
override AstNode getConsequenceNode() { result = this.getBody() }
override AstNode getBranch(boolean b) { b = true and result = this.getBody() }
}
private class UnlessAstNode extends IfElsifAstNode, Unless {
override AstNode getConditionNode() { result = this.getCondition() }
override AstNode getConsequenceNode() { result = this.getAlternative() }
override AstNode getAlternativeNode() { result = this.getConsequence() }
override AstNode getBranch(boolean b) {
b = false and result = this.getConsequence()
or
b = true and result = this.getAlternative()
}
}
private class UnlessModifierAstNode extends IfElsifAstNode, UnlessModifier {
override AstNode getConditionNode() { result = this.getCondition() }
override AstNode getAlternativeNode() { result = this.getBody() }
override AstNode getBranch(boolean b) { b = false and result = this.getBody() }
}
private class CondLoop = @while or @while_modifier or @until or @until_modifier;

View File

@@ -148,7 +148,12 @@ private predicate mustHaveBooleanCompletion(AstNode n) {
* that `n` evaluates to determines a true/false branch successor.
*/
private predicate inBooleanContext(AstNode n) {
n = any(IfElsifAstNode parent).getConditionNode()
exists(IfElsifAstNode i |
n = i.getConditionNode()
or
inBooleanContext(i) and
n = i.getBranch(_)
)
or
n = any(ConditionalLoopAstNode parent).getConditionNode()
or
@@ -175,6 +180,18 @@ private predicate inBooleanContext(AstNode n) {
c.getChild(_) = w and
w.getPattern(_).getChild() = n
)
or
exists(Then parent, int lst |
inBooleanContext(parent) and
n = parent.getChild(lst) and
not exists(parent.getChild(lst + 1))
)
or
exists(Else parent, int lst |
inBooleanContext(parent) and
n = parent.getChild(lst) and
not exists(parent.getChild(lst + 1))
)
}
/**

View File

@@ -639,34 +639,27 @@ module Trees {
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.getConditionNode(), last, c) and
c instanceof TrueCompletion and
not exists(this.getConsequenceNode())
or
last(this.getConsequenceNode(), last, c)
or
last(this.getAlternativeNode(), last, c)
private class IfElsifTree extends PostOrderTree, IfElsifAstNode {
final override predicate propagatesAbnormal(AstNode child) {
child = this.getConditionNode() or child = this.getBranch(_)
}
final override predicate first(AstNode first) { first(this.getConditionNode(), first) }
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)
exists(boolean b |
last(this.getConditionNode(), pred, c) and
b = c.(BooleanCompletion).getValue()
|
first(this.getBranch(b), succ)
or
c instanceof FalseCompletion and first(this.getAlternativeNode(), succ)
not exists(this.getBranch(b)) and
succ = this
)
or
last(this.getBranch(_), pred, c) and
succ = this and
c instanceof NormalCompletion
}
}

View File

@@ -229,6 +229,9 @@ private module ConditionalCompletionSplitting {
or
last(succ.(ParenthesizedStatement).getChild(), pred, c) and
completion = c
or
last(succ.(IfElsifAstNode).getBranch(_), pred, c) and
completion = c
)
}