Skip to content

Commit

Permalink
C#: Adopt shared SSA data-flow integration
Browse files Browse the repository at this point in the history
  • Loading branch information
@hvitved
hvitved committed Jul 4, 2024
1 parent 615f2a2 commit 35c9233
Show file tree
Hide file tree
Showing 11 changed files with 1,700 additions and 937 deletions.
2 changes: 1 addition & 1 deletion csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll
View file
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
308 changes: 166 additions & 142 deletions csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowPrivate.qll
View file
Original file line number Diff line number Diff line change
Expand Up @@ -257,7 +257,7 @@ module VariableCapture {
e1 = LocalFlow::getALastEvalNode(e2)
or
exists(Ssa::Definition def |
LocalFlow::ssaDefAssigns(def.getAnUltimateDefinition(), e1) and
SsaFlow::Input::ssaDefAssigns(def.getAnUltimateDefinition(), e1) and
exists(def.getAReadAtNode(e2))
)
}
Expand Down Expand Up @@ -481,6 +481,103 @@ module VariableCapture {
}
}

/** Provides logic related to SSA. */
module SsaFlow {
module Input implements SsaImpl::Impl::DataFlowIntegrationInputSig {
private import csharp as Cs

Check warning

Code scanning / CodeQL

Names only differing by case Warning

Cs is only different by casing from CS that is used elsewhere for modules.

class Expr extends ControlFlow::Node {
predicate hasCfgNode(ControlFlow::BasicBlock bb, int i) { this = bb.getNode(i) }
}

predicate ssaDefAssigns(SsaImpl::WriteDefinition def, Expr value) {
exists(AssignableDefinition adef, ControlFlow::Node cfnDef |
any(LocalFlow::LocalExprStepConfiguration conf).hasDefPath(_, value, adef, cfnDef) and
def.(Ssa::ExplicitDefinition).getADefinition() = adef and
def.(Ssa::ExplicitDefinition).getControlFlowNode() = cfnDef
)
}

class Parameter = Cs::Parameter;

predicate ssaDefInitializesParam(SsaImpl::WriteDefinition def, Parameter p) {
def.(Ssa::ImplicitParameterDefinition).getParameter() = p
}

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

Check warning

Code scanning / CodeQL

Predicate QLDoc style. Warning

The QLDoc for a predicate without a result should start with 'Holds'.
predicate allowFlowIntoUncertainDef(SsaImpl::UncertainWriteDefinition def) {
def instanceof Ssa::ExplicitDefinition
or
def =
any(Ssa::ImplicitQualifierDefinition qdef |
allowFlowIntoUncertainDef(qdef.getQualifierDefinition())
)
}
}

module Impl = SsaImpl::Impl::DataFlowIntegration<Input>;

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
TExplicitParameterNode(result.(Impl::ParameterNode).getParameter()) = n
}

predicate localFlowStep(SsaImpl::DefinitionExt def, Node nodeFrom, Node nodeTo) {
Impl::localFlowStep(def, asNode(nodeFrom), asNode(nodeTo)) and
// exclude flow directly from RHS to SSA definition, as we instead want to
// go from RHS to matching assingnable definition, and from there to SSA definition
not Input::ssaDefAssigns(def, nodeFrom.(ExprNode).getControlFlowNode())
}

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

module BarrierGuardsInput implements Impl::BarrierGuardsInputSig {
private import semmle.code.csharp.controlflow.BasicBlocks
private import semmle.code.csharp.controlflow.Guards as Guards

class Guard extends Guards::Guard {
predicate hasCfgNode(ControlFlow::BasicBlock bb, int i) {
this.getAControlFlowNode() = bb.getNode(i)
}
}

/** Holds if the guard `guard` controls block `bb` upon evaluating to `branch`. */
predicate guardControlsBlock(Guard guard, ControlFlow::BasicBlock bb, boolean branch) {
exists(ConditionBlock conditionBlock, ControlFlow::SuccessorTypes::ConditionalSuccessor s |
guard.getAControlFlowNode() = conditionBlock.getLastNode() and
s.getValue() = branch and
conditionBlock.controls(bb, s)
)
}

/** Gets an immediate conditional successor of basic block `bb`, if any. */
ControlFlow::BasicBlock getAConditionalBasicBlockSuccessor(
ControlFlow::BasicBlock bb, boolean branch
) {
exists(ControlFlow::SuccessorTypes::ConditionalSuccessor s |
result = bb.getASuccessorByType(s) and
s.getValue() = branch
)
}
}

module BarrierGuardsImpl = Impl::BarrierGuards<BarrierGuardsInput>;
}

/** Provides predicates related to local data flow. */
module LocalFlow {
class LocalExprStepConfiguration extends ControlFlowReachabilityConfiguration {
Expand Down Expand Up @@ -606,105 +703,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 @@ -788,10 +786,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 @@ -816,22 +811,10 @@ predicate simpleLocalFlowStep(Node nodeFrom, Node nodeTo, string model) {
LocalFlow::localFlowStepCommon(nodeFrom, nodeTo)
or
exists(SsaImpl::DefinitionExt def |
SsaFlow::localFlowStep(def, nodeFrom, nodeTo) 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
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 def instanceof VariableCapture::CapturedSsaDefinitionExt and
not FlowSummaryImpl::Private::Steps::prohibitsUseUseFlow(nodeFrom, _)
)
or
nodeTo.(ObjectCreationNode).getPreUpdateNode() = nodeFrom.(ObjectInitializerNode)
Expand Down Expand Up @@ -1097,10 +1080,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
} or
TSsaNode(SsaFlow::Impl::SsaNode node) or
TAssignableDefinitionNode(AssignableDefinition def, ControlFlow::Node cfn) {
cfn = def.getExpr().getAControlFlowNode()
} or
Expand Down Expand Up @@ -1165,17 +1145,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 @@ -1239,7 +1209,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 @@ -1273,13 +1243,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 {
SsaFlow::Impl::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 @@ -1292,9 +1265,60 @@ 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 = node.toString() }
}

/** An (extended) SSA definition, viewed as a node in a data flow graph. */
class SsaDefinitionExtNode extends SsaNode {
override SsaFlow::Impl::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 SsaFlow::Impl::SsaInputNode node;
ControlFlow::BasicBlock input;

Check notice

Code scanning / CodeQL

Field only used in CharPred Note

Field is only used in CharPred.

override string toStringImpl() { result = def.toString() }
SsaInputNode() { node.isInputInto(def, input) }
}

/** A definition, viewed as a node in a data flow graph. */
Expand Down Expand Up @@ -2844,7 +2868,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
Loading

0 comments on commit 35c9233

Please sign in to comment.