C#: Clean up.

This commit is contained in:
Anders Schack-Mulligen
2026-03-13 14:21:21 +01:00
parent 4c77e0f315
commit e7edf15031
4 changed files with 0 additions and 270 deletions

View File

@@ -1,246 +0,0 @@
import csharp
private class ControlFlowScope extends ControlFlowElement {
private boolean exactScope;
ControlFlowScope() {
exists(ControlFlowReachabilityConfiguration c |
c.candidate(_, _, this, exactScope, _) or
c.candidateDef(_, _, this, exactScope, _)
)
}
predicate isExact() { exactScope = true }
predicate isNonExact() { exactScope = false }
}
private newtype TControlFlowElementOrBasicBlock =
TControlFlowElement(ControlFlowElement cfe) or
TBasicBlock(ControlFlow::BasicBlock bb)
class ControlFlowElementOrBasicBlock extends TControlFlowElementOrBasicBlock {
ControlFlowElement asControlFlowElement() { this = TControlFlowElement(result) }
ControlFlow::BasicBlock asBasicBlock() { this = TBasicBlock(result) }
string toString() {
result = this.asControlFlowElement().toString()
or
result = this.asBasicBlock().toString()
}
Location getLocation() {
result = this.asControlFlowElement().getLocation()
or
result = this.asBasicBlock().getLocation()
}
}
private predicate isBasicBlock(ControlFlowElementOrBasicBlock c) { c instanceof TBasicBlock }
private predicate isNonExactScope(ControlFlowElementOrBasicBlock c) {
c.asControlFlowElement().(ControlFlowScope).isNonExact()
}
private predicate step(ControlFlowElementOrBasicBlock pred, ControlFlowElementOrBasicBlock succ) {
pred.asBasicBlock().getANode().getAstNode() = succ.asControlFlowElement()
or
pred.asControlFlowElement() = succ.asControlFlowElement().getAChild()
}
private predicate basicBlockInNonExactScope(
ControlFlowElementOrBasicBlock bb, ControlFlowElementOrBasicBlock scope
) = doublyBoundedFastTC(step/2, isBasicBlock/1, isNonExactScope/1)(bb, scope)
pragma[noinline]
private ControlFlow::BasicBlock getABasicBlockInScope(ControlFlowScope scope, boolean exactScope) {
basicBlockInNonExactScope(TBasicBlock(result), TControlFlowElement(scope)) and
exactScope = false
or
scope.isExact() and
result.getANode().getAstNode() = scope and
exactScope = true
}
/**
* A helper class for determining control-flow reachability for pairs of
* elements.
*
* This is useful when defining for example expression-based data-flow steps in
* the presence of control-flow splitting, where a data-flow step should make
* sure to stay in the same split.
*
* For example, in
*
* ```csharp
* if (b)
* ....
* var x = "foo";
* if (b)
* ....
* ```
*
* there should only be steps from `[b = true] "foo"` to `[b = true] SSA def(x)`
* and `[b = false] "foo"` to `[b = false] SSA def(x)`, and for example not from
* `[b = true] "foo"` to `[b = false] SSA def(x)`
*/
abstract class ControlFlowReachabilityConfiguration extends string {
bindingset[this]
ControlFlowReachabilityConfiguration() { any() }
/**
* Holds if `e1` and `e2` are expressions for which we want to find a
* control-flow path that follows control flow successors (resp.
* predecessors, as specified by `isSuccessor`) inside the syntactic scope
* `scope`. The Boolean `exactScope` indicates whether a transitive child
* of `scope` is allowed (`exactScope = false`).
*/
predicate candidate(
Expr e1, Expr e2, ControlFlowElement scope, boolean exactScope, boolean isSuccessor
) {
none()
}
/**
* Holds if `e` and `def` are elements for which we want to find a
* control-flow path that follows control flow successors (resp.
* predecessors, as specified by `isSuccessor`) inside the syntactic scope
* `scope`. The Boolean `exactScope` indicates whether a transitive child
* of `scope` is allowed (`exactScope = false`).
*/
predicate candidateDef(
Expr e, AssignableDefinition def, ControlFlowElement scope, boolean exactScope,
boolean isSuccessor
) {
none()
}
pragma[nomagic]
private predicate reachesBasicBlockExprBase(
Expr e1, Expr e2, boolean isSuccessor, ControlFlow::Nodes::ElementNode cfn1, int i,
ControlFlow::BasicBlock bb
) {
this.candidate(e1, e2, _, _, isSuccessor) and
cfn1 = e1.getAControlFlowNode() and
bb.getNode(i) = cfn1
}
pragma[nomagic]
private predicate reachesBasicBlockExprRec(
Expr e1, Expr e2, boolean isSuccessor, ControlFlow::Nodes::ElementNode cfn1,
ControlFlow::BasicBlock bb
) {
exists(ControlFlow::BasicBlock mid |
this.reachesBasicBlockExpr(e1, e2, isSuccessor, cfn1, mid)
|
isSuccessor = true and
bb = mid.getASuccessor()
or
isSuccessor = false and
bb = mid.getAPredecessor()
)
}
pragma[nomagic]
private predicate reachesBasicBlockExpr(
Expr e1, Expr e2, boolean isSuccessor, ControlFlow::Nodes::ElementNode cfn1,
ControlFlow::BasicBlock bb
) {
this.reachesBasicBlockExprBase(e1, e2, isSuccessor, cfn1, _, bb)
or
exists(ControlFlowElement scope, boolean exactScope |
this.candidate(e1, e2, scope, exactScope, isSuccessor) and
this.reachesBasicBlockExprRec(e1, e2, isSuccessor, cfn1, bb) and
bb = getABasicBlockInScope(scope, exactScope)
)
}
pragma[nomagic]
private predicate reachesBasicBlockDefinitionBase(
Expr e, AssignableDefinition def, boolean isSuccessor, ControlFlow::Nodes::ElementNode cfn,
int i, ControlFlow::BasicBlock bb
) {
this.candidateDef(e, def, _, _, isSuccessor) and
cfn = e.getAControlFlowNode() and
bb.getNode(i) = cfn
}
pragma[nomagic]
private predicate reachesBasicBlockDefinitionRec(
Expr e, AssignableDefinition def, boolean isSuccessor, ControlFlow::Nodes::ElementNode cfn,
ControlFlow::BasicBlock bb
) {
exists(ControlFlow::BasicBlock mid |
this.reachesBasicBlockDefinition(e, def, isSuccessor, cfn, mid)
|
isSuccessor = true and
bb = mid.getASuccessor()
or
isSuccessor = false and
bb = mid.getAPredecessor()
)
}
pragma[nomagic]
private predicate reachesBasicBlockDefinition(
Expr e, AssignableDefinition def, boolean isSuccessor, ControlFlow::Nodes::ElementNode cfn,
ControlFlow::BasicBlock bb
) {
this.reachesBasicBlockDefinitionBase(e, def, isSuccessor, cfn, _, bb)
or
exists(ControlFlowElement scope, boolean exactScope |
this.candidateDef(e, def, scope, exactScope, isSuccessor) and
this.reachesBasicBlockDefinitionRec(e, def, isSuccessor, cfn, bb) and
bb = getABasicBlockInScope(scope, exactScope)
)
}
/**
* Holds if there is a control-flow path from `cfn1` to `cfn2`, where `cfn1` is a
* control-flow node for `e1` and `cfn2` is a control-flow node for `e2`.
*/
pragma[nomagic]
predicate hasExprPath(Expr e1, ControlFlow::Node cfn1, Expr e2, ControlFlow::Node cfn2) {
exists(ControlFlow::BasicBlock bb, boolean isSuccessor, int i, int j |
this.reachesBasicBlockExprBase(e1, e2, isSuccessor, cfn1, i, bb) and
cfn2 = bb.getNode(j) and
cfn2 = e2.getAControlFlowNode()
|
isSuccessor = true and j >= i
or
isSuccessor = false and i >= j
)
or
exists(ControlFlow::BasicBlock bb |
this.reachesBasicBlockExprRec(e1, e2, _, cfn1, bb) and
cfn2 = bb.getANode() and
cfn2 = e2.getAControlFlowNode()
)
}
/**
* Holds if there is a control-flow path from `cfn` to `cfnDef`, where `cfn` is a
* control-flow node for `e` and `cfnDef` is a control-flow node for `def`.
*/
pragma[nomagic]
predicate hasDefPath(
Expr e, ControlFlow::Node cfn, AssignableDefinition def, ControlFlow::Node cfnDef
) {
exists(ControlFlow::BasicBlock bb, boolean isSuccessor, int i, int j |
this.reachesBasicBlockDefinitionBase(e, def, isSuccessor, cfn, i, bb) and
cfnDef = bb.getNode(j) and
def.getExpr().getAControlFlowNode() = cfnDef
|
isSuccessor = true and j >= i
or
isSuccessor = false and i >= j
)
or
exists(ControlFlow::BasicBlock bb |
this.reachesBasicBlockDefinitionRec(e, def, _, cfn, bb) and
def.getExpr().getAControlFlowNode() = cfnDef and
cfnDef = bb.getANode()
)
}
}

View File

@@ -2,7 +2,6 @@ private import csharp
private import DataFlowPublic
private import DataFlowDispatch
private import DataFlowImplCommon
private import ControlFlowReachability
private import FlowSummaryImpl as FlowSummaryImpl
private import semmle.code.csharp.dataflow.FlowSummary as FlowSummary
private import semmle.code.csharp.dataflow.internal.ExternalFlow
@@ -259,24 +258,6 @@ private module ThisFlow {
}
}
/**
* Holds if there is a control-flow path from `n1` to `n2`. `n2` is either an
* expression node or an SSA definition node.
*/
pragma[nomagic]
predicate hasNodePath(ControlFlowReachabilityConfiguration conf, ExprNode n1, Node n2) {
exists(ControlFlow::Node cfn1, ControlFlow::Node cfn2 | conf.hasExprPath(_, cfn1, _, cfn2) |
cfn1 = n1.getControlFlowNode() and
cfn2 = n2.(ExprNode).getControlFlowNode()
)
or
exists(ControlFlow::Node cfn, AssignableDefinition def, ControlFlow::Node cfnDef |
conf.hasDefPath(_, cfn, def, cfnDef) and
cfn = n1.getControlFlowNode() and
n2 = TAssignableDefinitionNode(def, cfnDef)
)
}
/** Provides logic related to captured variables. */
module VariableCapture {
private import codeql.dataflow.VariableCapture as Shared

View File

@@ -4,7 +4,6 @@ private import FlowSummaryImpl as FlowSummaryImpl
private import semmle.code.csharp.Caching
private import semmle.code.csharp.dataflow.internal.DataFlowDispatch
private import semmle.code.csharp.dataflow.internal.DataFlowPrivate
private import semmle.code.csharp.dataflow.internal.ControlFlowReachability
private import semmle.code.csharp.dispatch.Dispatch
private import semmle.code.csharp.commons.ComparisonTest
// import `TaintedMember` definitions from other files to avoid potential reevaluation