Skip to content

C#: Adopt shared SSA data-flow integration #16936

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hvitved merged 2 commits into from
Sep 17, 2024
Merged

C#: Adopt shared SSA data-flow integration #16936

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
89a2381
C#: Adopt shared SSA data-flow integration
hvitved Jul 3, 2024
d0eae97
Address review comment
hvitved Sep 16, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ module BaseSsa {
) {
exists(ControlFlow::ControlFlow::BasicBlocks::EntryBlock entry |
c = entry.getCallable() and
// In case `c` has multiple bodies, we want each body to gets its own implicit
// In case `c` has multiple bodies, we want each body to get its own implicit
// entry definition. In case `c` doesn't have multiple bodies, the line below
// is simply the same as `bb = entry`, because `entry.getFirstNode().getASuccessor()`
// will be in the entry block.
Expand Down
235 changes: 93 additions & 142 deletions csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowPrivate.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -267,8 +267,9 @@ module VariableCapture {
private predicate closureFlowStep(ControlFlow::Nodes::ExprNode e1, ControlFlow::Nodes::ExprNode e2) {
e1 = LocalFlow::getALastEvalNode(e2)
or
exists(Ssa::Definition def |
LocalFlow::ssaDefAssigns(def.getAnUltimateDefinition(), e1) and
exists(Ssa::Definition def, AssignableDefinition adef |
LocalFlow::defAssigns(adef, _, e1) and
def.getAnUltimateDefinition().(Ssa::ExplicitDefinition).getADefinition() = adef and
exists(def.getAReadAtNode(e2))
)
}
Expand Down Expand Up @@ -492,6 +493,30 @@ module VariableCapture {
}
}

/** Provides logic related to SSA. */
module SsaFlow {
private module Impl = SsaImpl::DataFlowIntegration;

Impl::Node asNode(Node n) {
n = TSsaNode(result)
or
result.(Impl::ExprNode).getExpr() = n.(ExprNode).getControlFlowNode()
or
result.(Impl::ExprPostUpdateNode).getExpr() =
n.(PostUpdateNode).getPreUpdateNode().(ExprNode).getControlFlowNode()
or
result.(Impl::ParameterNode).getParameter() = n.(ExplicitParameterNode).getSsaDefinition()
}

predicate localFlowStep(SsaImpl::DefinitionExt def, Node nodeFrom, Node nodeTo, boolean isUseStep) {
Impl::localFlowStep(def, asNode(nodeFrom), asNode(nodeTo), isUseStep)
}

predicate localMustFlowStep(SsaImpl::DefinitionExt def, Node nodeFrom, Node nodeTo) {
Impl::localMustFlowStep(def, asNode(nodeFrom), asNode(nodeTo))
}
}

/** Provides predicates related to local data flow. */
module LocalFlow {
class LocalExprStepConfiguration extends ControlFlowReachabilityConfiguration {
Expand Down Expand Up @@ -617,105 +642,6 @@ module LocalFlow {
any(LocalExprStepConfiguration x).hasDefPath(_, value, def, cfnDef)
}

predicate ssaDefAssigns(Ssa::ExplicitDefinition ssaDef, ControlFlow::Nodes::ExprNode value) {
exists(AssignableDefinition def, ControlFlow::Node cfnDef |
any(LocalExprStepConfiguration conf).hasDefPath(_, value, def, cfnDef) and
ssaDef.getADefinition() = def and
ssaDef.getControlFlowNode() = cfnDef
)
}

/**
* An uncertain SSA definition. Either an uncertain explicit definition or an
* uncertain qualifier definition.
*
* Restricts `Ssa::UncertainDefinition` by excluding implicit call definitions,
* as we---conservatively---consider such definitions to be certain.
*/
class UncertainExplicitSsaDefinition extends Ssa::UncertainDefinition {
UncertainExplicitSsaDefinition() {
this instanceof Ssa::ExplicitDefinition
or
this =
any(Ssa::ImplicitQualifierDefinition qdef |
qdef.getQualifierDefinition() instanceof UncertainExplicitSsaDefinition
)
}
}

/** An SSA definition into which another SSA definition may flow. */
private class SsaInputDefinitionExtNode extends SsaDefinitionExtNode {
SsaInputDefinitionExtNode() {
def instanceof Ssa::PhiNode
or
def instanceof SsaImpl::PhiReadNode
or
def instanceof LocalFlow::UncertainExplicitSsaDefinition
}
}

/**
* Holds if `nodeFrom` is a last node referencing SSA definition `def`, which
* can reach `next`.
*/
private predicate localFlowSsaInputFromDef(
Node nodeFrom, SsaImpl::DefinitionExt def, SsaInputDefinitionExtNode next
) {
exists(ControlFlow::BasicBlock bb, int i |
SsaImpl::lastRefBeforeRedefExt(def, bb, i, next.getDefinitionExt()) and
def.definesAt(_, bb, i, _) and
def = getSsaDefinitionExt(nodeFrom) and
nodeFrom != next
)
}

/**
* Holds if `read` is a last node reading SSA definition `def`, which
* can reach `next`.
*/
predicate localFlowSsaInputFromRead(
Node read, SsaImpl::DefinitionExt def, SsaInputDefinitionExtNode next
) {
exists(ControlFlow::BasicBlock bb, int i |
SsaImpl::lastRefBeforeRedefExt(def, bb, i, next.getDefinitionExt()) and
read.asExprAtNode(bb.getNode(i)) instanceof AssignableRead
)
}

private SsaImpl::DefinitionExt getSsaDefinitionExt(Node n) {
result = n.(SsaDefinitionExtNode).getDefinitionExt()
or
result = n.(ExplicitParameterNode).getSsaDefinition()
}

/**
* Holds if there is a local use-use flow step from `nodeFrom` to `nodeTo`
* involving SSA definition `def`.
*/
predicate localSsaFlowStepUseUse(SsaImpl::DefinitionExt def, Node nodeFrom, Node nodeTo) {
exists(ControlFlow::Node cfnFrom, ControlFlow::Node cfnTo |
SsaImpl::adjacentReadPairSameVarExt(def, cfnFrom, cfnTo) and
nodeTo = TExprNode(cfnTo) and
nodeFrom = TExprNode(cfnFrom)
)
}

/**
* Holds if there is a local flow step from `nodeFrom` to `nodeTo` involving
* SSA definition `def`.
*/
predicate localSsaFlowStep(SsaImpl::DefinitionExt def, Node nodeFrom, Node nodeTo) {
// Flow from SSA definition/parameter to first read
def = getSsaDefinitionExt(nodeFrom) and
SsaImpl::firstReadSameVarExt(def, nodeTo.(ExprNode).getControlFlowNode())
or
// Flow from read to next read
localSsaFlowStepUseUse(def, nodeFrom.(PostUpdateNode).getPreUpdateNode(), nodeTo)
or
// Flow into phi (read)/uncertain SSA definition node from def
localFlowSsaInputFromDef(nodeFrom, def, nodeTo)
}

/**
* Holds if the source variable of SSA definition `def` is an instance field.
*/
Expand Down Expand Up @@ -800,10 +726,7 @@ module LocalFlow {
node2.asExpr() instanceof AssignExpr
)
or
exists(SsaImpl::Definition def |
def = getSsaDefinitionExt(node1) and
exists(SsaImpl::getAReadAtNode(def, node2.(ExprNode).getControlFlowNode()))
)
SsaFlow::localMustFlowStep(_, node1, node2)
or
node2 = node1.(LocalFunctionCreationNode).getAnAccess(true)
or
Expand All @@ -827,23 +750,14 @@ predicate simpleLocalFlowStep(Node nodeFrom, Node nodeTo, string model) {
(
LocalFlow::localFlowStepCommon(nodeFrom, nodeTo)
or
exists(SsaImpl::DefinitionExt def |
exists(SsaImpl::DefinitionExt def, boolean isUseStep |
SsaFlow::localFlowStep(def, nodeFrom, nodeTo, isUseStep) and
not LocalFlow::usesInstanceField(def) and
not def instanceof VariableCapture::CapturedSsaDefinitionExt
|
LocalFlow::localSsaFlowStep(def, nodeFrom, nodeTo)
or
LocalFlow::localSsaFlowStepUseUse(def, nodeFrom, nodeTo) and
not FlowSummaryImpl::Private::Steps::prohibitsUseUseFlow(nodeFrom, _) and
nodeFrom != nodeTo
isUseStep = false
or
// Flow into phi (read)/uncertain SSA definition node from read
exists(Node read | LocalFlow::localFlowSsaInputFromRead(read, def, nodeTo) |
nodeFrom = read and
not FlowSummaryImpl::Private::Steps::prohibitsUseUseFlow(nodeFrom, _)
or
nodeFrom.(PostUpdateNode).getPreUpdateNode() = read
)
not FlowSummaryImpl::Private::Steps::prohibitsUseUseFlow(nodeFrom, _)
Copy link
Contributor

@aschackmull aschackmull Sep 16, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There's a pipeline duplication here, better add isUseStep = true to the second disjunct.

)
or
nodeTo.(ObjectCreationNode).getPreUpdateNode() = nodeFrom.(ObjectInitializerNode)
Expand Down Expand Up @@ -1113,11 +1027,7 @@ private module Cached {
cached
newtype TNode =
TExprNode(ControlFlow::Nodes::ElementNode cfn) { cfn.getAstNode() instanceof Expr } or
TSsaDefinitionExtNode(SsaImpl::DefinitionExt def) {
// Handled by `TExplicitParameterNode` below
not def instanceof Ssa::ImplicitParameterDefinition and
def.getBasicBlock() = any(DataFlowCallable c).getAControlFlowNode().getBasicBlock()
} or
TSsaNode(SsaImpl::DataFlowIntegration::SsaNode node) or
TAssignableDefinitionNode(AssignableDefinition def, ControlFlow::Node cfn) {
cfn = def.getExpr().getAControlFlowNode()
} or
Expand Down Expand Up @@ -1180,17 +1090,7 @@ private module Cached {
predicate localFlowStepImpl(Node nodeFrom, Node nodeTo) {
LocalFlow::localFlowStepCommon(nodeFrom, nodeTo)
or
LocalFlow::localSsaFlowStepUseUse(_, nodeFrom, nodeTo) and
nodeFrom != nodeTo
or
LocalFlow::localSsaFlowStep(_, nodeFrom, nodeTo)
or
// Flow into phi (read)/uncertain SSA definition node from read
exists(Node read | LocalFlow::localFlowSsaInputFromRead(read, _, nodeTo) |
nodeFrom = read
or
nodeFrom.(PostUpdateNode).getPreUpdateNode() = read
)
SsaFlow::localFlowStep(_, nodeFrom, nodeTo, _)
or
// Simple flow through library code is included in the exposed local
// step relation, even though flow is technically inter-procedural
Expand Down Expand Up @@ -1254,7 +1154,7 @@ import Cached

/** Holds if `n` should be hidden from path explanations. */
predicate nodeIsHidden(Node n) {
n instanceof SsaDefinitionExtNode
n instanceof SsaNode
or
exists(Parameter p | p = n.(ParameterNode).getParameter() | not p.fromSource())
or
Expand Down Expand Up @@ -1288,13 +1188,16 @@ predicate nodeIsHidden(Node n) {
n instanceof CaptureNode
}

/** An SSA definition, viewed as a node in a data flow graph. */
class SsaDefinitionExtNode extends NodeImpl, TSsaDefinitionExtNode {
/** An SSA node. */
abstract class SsaNode extends NodeImpl, TSsaNode {
SsaImpl::DataFlowIntegration::SsaNode node;
SsaImpl::DefinitionExt def;

SsaDefinitionExtNode() { this = TSsaDefinitionExtNode(def) }
SsaNode() {
this = TSsaNode(node) and
def = node.getDefinitionExt()
}

/** Gets the underlying SSA definition. */
SsaImpl::DefinitionExt getDefinitionExt() { result = def }

override DataFlowCallable getEnclosingCallableImpl() {
Expand All @@ -1307,9 +1210,57 @@ class SsaDefinitionExtNode extends NodeImpl, TSsaDefinitionExtNode {
result = def.(Ssa::Definition).getControlFlowNode()
}

override Location getLocationImpl() { result = def.getLocation() }
override Location getLocationImpl() { result = node.getLocation() }

override string toStringImpl() { result = def.toString() }
override string toStringImpl() { result = node.toString() }
}

/** An (extended) SSA definition, viewed as a node in a data flow graph. */
class SsaDefinitionExtNode extends SsaNode {
override SsaImpl::DataFlowIntegration::SsaDefinitionExtNode node;
}

/**
* A node that represents an input to an SSA phi (read) definition.
*
* This allows for barrier guards to filter input to phi nodes. For example, in
*
* ```csharp
* var x = taint;
* if (x != "safe")
* {
* x = "safe";
* }
* sink(x);
* ```
*
* the `false` edge out of `x != "safe"` guards the input from `x = taint` into the
* `phi` node after the condition.
*
* It is also relevant to filter input into phi read nodes:
*
* ```csharp
* var x = taint;
* if (b)
* {
* if (x != "safe1")
* {
* return;
* }
* } else {
* if (x != "safe2")
* {
* return;
* }
* }
*
* sink(x);
* ```
*
* both inputs into the phi read node after the outer condition are guarded.
*/
class SsaInputNode extends SsaNode {
override SsaImpl::DataFlowIntegration::SsaInputNode node;
}

/** A definition, viewed as a node in a data flow graph. */
Expand Down Expand Up @@ -2907,7 +2858,7 @@ private predicate delegateCreationStep(Node nodeFrom, Node nodeTo) {
/** Extra data-flow steps needed for lambda flow analysis. */
predicate additionalLambdaFlowStep(Node nodeFrom, Node nodeTo, boolean preservesValue) {
exists(SsaImpl::DefinitionExt def |
LocalFlow::localSsaFlowStep(def, nodeFrom, nodeTo) and
SsaFlow::localFlowStep(def, nodeFrom, nodeTo, _) and
preservesValue = true
|
LocalFlow::usesInstanceField(def)
Expand Down
8 changes: 7 additions & 1 deletion csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowPublic.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -171,8 +171,14 @@ signature predicate guardChecksSig(Guard g, Expr e, AbstractValue v);
* in data flow and taint tracking.
*/
module BarrierGuard<guardChecksSig/3 guardChecks> {
private import SsaImpl as SsaImpl

/** Gets a node that is safely guarded by the given guard check. */
ExprNode getABarrierNode() {
pragma[nomagic]
Node getABarrierNode() {
SsaFlow::asNode(result) =
SsaImpl::DataFlowIntegration::BarrierGuard<guardChecks/3>::getABarrierNode()
or
exists(Guard g, Expr e, AbstractValue v |
guardChecks(g, e, v) and
g.controlsNode(result.getControlFlowNode(), e, v)
Comment on lines 182 to 184
Copy link
Contributor

@aschackmull aschackmull Jul 19, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why is this second disjunct not redundant now? Does it cover more than ssa variable reads?

Copy link
Contributor Author

@hvitved hvitved Aug 6, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good question: Yes, it covers more than SSA variable reads (it uses GVN, which--although it is unsound in general--is likely to produce valid guards).

Expand Down
Loading