PS: Implement CFG for if statements and switches.

This commit is contained in:
Mathias Vorreiter Pedersen
2024-09-06 10:06:42 +01:00
parent fd29c470c0
commit 4c59de4fde
3 changed files with 164 additions and 10 deletions

View File

@@ -69,10 +69,11 @@ module SuccessorTypes {
* A conditional control flow successor. Either a Boolean successor (`BooleanSuccessor`)
* or a matching successor (`MatchingSuccessor`)
*/
class ConditionalSuccessor extends SuccessorType {
abstract class ConditionalSuccessor extends SuccessorType {
boolean value;
ConditionalSuccessor() { this = CfgImpl::TBooleanSuccessor(value) }
bindingset[value]
ConditionalSuccessor() { any() }
/** Gets the Boolean value of this successor. */
final boolean getValue() { result = value }
@@ -80,7 +81,13 @@ module SuccessorTypes {
override string toString() { result = this.getValue().toString() }
}
class BooleanSuccessor extends ConditionalSuccessor, CfgImpl::TBooleanSuccessor { }
class BooleanSuccessor extends ConditionalSuccessor, CfgImpl::TBooleanSuccessor {
BooleanSuccessor() { this = CfgImpl::TBooleanSuccessor(value) }
}
class MatchingSuccessor extends ConditionalSuccessor, CfgImpl::TMatchingSuccessor {
MatchingSuccessor() { this = CfgImpl::TMatchingSuccessor(value) }
}
class ReturnSuccessor extends SuccessorType, CfgImpl::TReturnSuccessor {
final override string toString() { result = "return" }
@@ -94,8 +101,8 @@ module SuccessorTypes {
final override string toString() { result = "continue" }
}
class RaiseSuccessor extends SuccessorType, CfgImpl::TRaiseSuccessor {
final override string toString() { result = "raise" }
class ThrowSuccessor extends SuccessorType, CfgImpl::TThrowSuccessor {
final override string toString() { result = "throw" }
}
class ExitSuccessor extends SuccessorType, CfgImpl::TExitSuccessor {

View File

@@ -8,16 +8,18 @@ private import powershell
private import semmle.code.powershell.controlflow.ControlFlowGraph
private import ControlFlowGraphImpl as CfgImpl
private import SuccessorTypes
private import codeql.util.Boolean
// TODO: We most likely need a TrapCompletion as well
private newtype TCompletion =
TSimpleCompletion() or
TBooleanCompletion(boolean b) { b in [false, true] } or
TBooleanCompletion(Boolean b) or
TReturnCompletion() or
TBreakCompletion() or
TContinueCompletion() or
TRaiseCompletion() or
TExitCompletion()
TExitCompletion() or
TMatchingCompletion(Boolean b)
pragma[noinline]
private predicate completionIsValidForStmt(Ast n, Completion c) {
@@ -40,6 +42,14 @@ abstract class Completion extends TCompletion {
not isBooleanConstant(n, _) and
this = TBooleanCompletion(_)
)
or
mustHaveMatchingCompletion(n) and
(
exists(boolean value | isMatchingConstant(n, value) | this = TMatchingCompletion(value))
or
not isMatchingConstant(n, _) and
this = TMatchingCompletion(_)
)
}
private predicate isValidForSpecific(Ast n) { this.isValidForSpecific0(n) }
@@ -74,11 +84,18 @@ private predicate isBooleanConstant(Ast n, boolean value) {
none() // TODO
}
private predicate isMatchingConstant(Ast n, boolean value) {
inMatchingContext(n) and
none() // TODO
}
/**
* Holds if a normal completion of `n` must be a Boolean completion.
*/
private predicate mustHaveBooleanCompletion(Ast n) { inBooleanContext(n) }
private predicate mustHaveMatchingCompletion(Ast n) { inMatchingContext(n) }
/**
* Holds if `n` is used in a Boolean context. That is, the value
* that `n` evaluates to determines a true/false branch successor.
@@ -128,6 +145,20 @@ private predicate inBooleanContext(Ast n) {
)
}
/**
* From: https://learn.microsoft.com/en-us/powershell/module/microsoft.powershell.core/about/about_switch?view=powershell-7.4:
* ```
* switch [-regex | -wildcard | -exact] [-casesensitive] (<test-expression>)
* {
* "string" | number | variable | { <value-scriptblock> } { <action-scriptblock> }
* default { <action-scriptblock> } # optional
* }
* ```
*/
private predicate inMatchingContext(Ast n) {
n = any(SwitchStmt switch).getAPattern()
}
/**
* A completion that represents normal evaluation of a statement or an
* expression.
@@ -159,7 +190,7 @@ abstract class ConditionalCompletion extends NormalCompletion {
* A completion that represents evaluation of an expression
* with a Boolean value.
*/
class BooleanCompletion extends ConditionalCompletion, NormalCompletion, TBooleanCompletion {
class BooleanCompletion extends ConditionalCompletion, TBooleanCompletion {
BooleanCompletion() { this = TBooleanCompletion(value) }
/** Gets the dual Boolean completion. */
@@ -180,6 +211,18 @@ class FalseCompletion extends BooleanCompletion {
FalseCompletion() { this.getValue() = false }
}
class MatchCompletion extends ConditionalCompletion, TMatchingCompletion {
MatchCompletion() { this = TMatchingCompletion(value) }
override MatchingSuccessor getAMatchingSuccessorType() { result.getValue() = value }
predicate isMatch() { this.getValue() = true }
predicate isNonMatch() { this.getValue() = false }
override string toString() { if this.isMatch() then result = "match" else result = "nonmatch" }
}
/**
* A completion that represents evaluation of a statement or an
* expression resulting in a return.

View File

@@ -5,6 +5,7 @@
private import powershell
private import codeql.controlflow.Cfg as CfgShared
private import codeql.util.Boolean
private import semmle.code.powershell.controlflow.ControlFlowGraph
private import Completion
@@ -418,6 +419,108 @@ module Trees {
}
}
class IfStmtTree extends PreOrderTree instanceof IfStmt {
final override predicate propagatesAbnormal(AstNode child) {
child = super.getACondition()
or
child = super.getAThen()
or
child = super.getElse()
}
final override predicate last(AstNode last, Completion c) {
last(super.getAThen(), last, c)
or
last(super.getElse(), last, c)
}
final override predicate succ(AstNode pred, AstNode succ, Completion c) {
this = pred and
first(super.getCondition(0), succ) and
completionIsSimple(c)
or
exists(int i, boolean value |
last(super.getCondition(i), pred, c) and value = c.(BooleanCompletion).getValue()
|
value = true and
first(super.getThen(i), succ)
or
value = false and
(
first(super.getCondition(i + 1), succ)
or
i = super.getNumberOfConditions() - 1 and
first(super.getElse(), succ)
)
)
}
}
class SwitchStmtTree extends PreOrderTree instanceof SwitchStmt {
final override predicate propagatesAbnormal(AstNode child) {
child = super.getCondition()
or
child = super.getACase()
or
child = super.getDefault()
or
child = super.getAPattern()
}
final override predicate last(AstNode last, Completion c) {
// There are no cases and no default
not exists(super.getACase()) and
not exists(super.getDefault()) and
last(super.getCondition(), last, c) and
completionIsNormal(c)
or
// The last element can be the last statement in the default block
last(super.getDefault(), last, c)
or
// ... or any of the last elements in a case block
last(super.getACase(), last, c)
or
// No default and we reached the final pattern and failed to match
not exists(super.getDefault()) and
last(super.getPattern(super.getNumberOfCases() - 1), last, c) and
c.(MatchCompletion).isNonMatch()
}
final override predicate succ(AstNode pred, AstNode succ, Completion c) {
// Preorder: Flow from the switch to the condition
pred = this and
first(super.getCondition(), succ) and
completionIsSimple(c)
or
// Flow from the condition to the first pattern
last(super.getCondition(), pred, c) and
completionIsNormal(c) and
first(super.getPattern(0), succ)
or
// Flow from a match to:
// 1. the corresponding case if the match succeeds, or
// 2. the next pattern if the match failed, or
// 3. the default case if this is the last pattern and the match failed.
exists(int i, boolean match |
last(super.getPattern(i), pred, c) and c.(MatchCompletion).getValue() = match
|
// Case 1
match = true and
first(super.getCase(i), succ)
or
match = false and
(
// Case 2
first(super.getPattern(i + 1), succ)
or
// Case 3
i = super.getNumberOfCases() - 1 and
first(super.getDefault(), succ)
)
)
}
}
class GotoStmtTree extends LeafTree instanceof GotoStmt { }
class FunctionStmtTree extends LeafTree instanceof Function { }
@@ -470,12 +573,13 @@ private module Cached {
cached
newtype TSuccessorType =
TSuccessorSuccessor() or
TBooleanSuccessor(boolean b) { b in [false, true] } or
TBooleanSuccessor(Boolean b) or
TReturnSuccessor() or
TBreakSuccessor() or
TContinueSuccessor() or
TRaiseSuccessor() or
TExitSuccessor()
TExitSuccessor() or
TMatchingSuccessor(Boolean b)
}
import Cached