Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
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
75 changes: 33 additions & 42 deletions csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll
Original file line number Diff line number Diff line change
Expand Up @@ -7,12 +7,21 @@ module BaseSsa {
private import AssignableDefinitions
private import codeql.ssa.Ssa as SsaImplCommon

cached
private module BaseSsaStage {
cached
predicate ref() { any() }

cached
predicate backref() { (exists(any(SsaDefinition def).getARead()) implies any()) }
}

/**
* Holds if the `i`th node of basic block `bb` is assignable definition `def`,
* targeting local scope variable `v`.
*/
private predicate definitionAt(
AssignableDefinition def, BasicBlock bb, int i, SsaInput::SourceVariable v
AssignableDefinition def, BasicBlock bb, int i, SsaImplInput::SourceVariable v
) {
bb.getNode(i) = def.getExpr().getControlFlowNode() and
v = def.getTarget() and
Expand All @@ -24,7 +33,7 @@ module BaseSsa {
)
}

private predicate implicitEntryDef(Callable c, EntryBasicBlock bb, SsaInput::SourceVariable v) {
private predicate entryDef(Callable c, BasicBlock bb, SsaImplInput::SourceVariable v) {
exists(EntryBasicBlock entry |
c = entry.getEnclosingCallable() and
// In case `c` has multiple bodies, we want each body to get its own implicit
Expand Down Expand Up @@ -79,16 +88,17 @@ module BaseSsa {
}
}

private module SsaInput implements SsaImplCommon::InputSig<Location, BasicBlock> {
private module SsaImplInput implements SsaImplCommon::InputSig<Location, BasicBlock> {
class SourceVariable = SimpleLocalScopeVariable;

predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain) {
BaseSsaStage::ref() and
exists(AssignableDefinition def |
definitionAt(def, bb, i, v) and
if def.isCertain() then certain = true else certain = false
)
or
implicitEntryDef(_, bb, v) and
entryDef(_, bb, v) and
i = -1 and
certain = true
}
Expand All @@ -102,54 +112,35 @@ module BaseSsa {
}
}

private module SsaImpl = SsaImplCommon::Make<Location, Cfg, SsaInput>;
private module SsaImpl = SsaImplCommon::Make<Location, Cfg, SsaImplInput>;

class Definition extends SsaImpl::Definition {
final AssignableRead getARead() {
exists(BasicBlock bb, int i |
SsaImpl::ssaDefReachesRead(_, this, bb, i) and
result.getControlFlowNode() = bb.getNode(i)
)
}
private module SsaInput implements SsaImpl::SsaInputSig {
private import csharp as CS

final AssignableDefinition getDefinition() {
exists(BasicBlock bb, int i, SsaInput::SourceVariable v |
this.definesAt(v, bb, i) and
definitionAt(result, bb, i, v)
)
}
class Expr = CS::Expr;

final predicate isImplicitEntryDefinition(SsaInput::SourceVariable v) {
exists(BasicBlock bb |
this.definesAt(v, bb, -1) and
implicitEntryDef(_, bb, v)
)
}
class Parameter = CS::Parameter;

private Definition getAPhiInputOrPriorDefinition() {
result = this.(PhiNode).getAnInput() or
SsaImpl::uncertainWriteDefinitionInput(this, result)
}
class VariableWrite extends AssignableDefinition {
Expr asExpr() { result = this.getExpr() }

Expr getValue() { result = this.getSource() }

final Definition getAnUltimateDefinition() {
result = this.getAPhiInputOrPriorDefinition*() and
not result instanceof PhiNode
predicate isParameterInit(Parameter p) {
this.(ImplicitParameterDefinition).getParameter() = p
}
}

override Location getLocation() {
result = this.getDefinition().getLocation()
predicate explicitWrite(VariableWrite w, BasicBlock bb, int i, SsaImplInput::SourceVariable v) {
definitionAt(w, bb, i, v)
or
exists(Callable c, BasicBlock bb, SsaInput::SourceVariable v |
this.definesAt(v, bb, -1) and
implicitEntryDef(c, bb, v) and
result = c.getLocation()
)
entryDef(_, bb, v) and
i = -1 and
w.isParameterInit(v)
}
}

class PhiNode extends SsaImpl::PhiNode, Definition {
override Location getLocation() { result = this.getBasicBlock().getLocation() }
module Ssa = SsaImpl::MakeSsa<SsaInput>;

final Definition getAnInput() { SsaImpl::phiHasInputFromBlock(this, result, _) }
}
import Ssa
}
Original file line number Diff line number Diff line change
Expand Up @@ -15,8 +15,8 @@ module Steps {
* Gets a read that may read the value assigned at definition `def`.
*/
private AssignableRead getARead(AssignableDefinition def) {
exists(BaseSsa::Definition ssaDef |
ssaDef.getAnUltimateDefinition().getDefinition() = def and
exists(BaseSsa::SsaDefinition ssaDef |
ssaDef.getAnUltimateDefinition().(BaseSsa::SsaExplicitWrite).getDefinition() = def and
result = ssaDef.getARead()
)
or
Expand Down
4 changes: 2 additions & 2 deletions csharp/ql/lib/semmle/code/csharp/dispatch/Dispatch.qll
Original file line number Diff line number Diff line change
Expand Up @@ -355,8 +355,8 @@ private module Internal {
1 < strictcount(this.getADynamicTarget().getUnboundDeclaration()) and
c = this.getCall().getEnclosingCallable().getUnboundDeclaration() and
(
exists(BaseSsa::Definition def, Parameter p |
def.isImplicitEntryDefinition(p) and
exists(BaseSsa::SsaParameterInit def, Parameter p |
def.getParameter() = p and
this.getSyntheticQualifier() = def.getARead() and
p.getPosition() = i and
c.getAParameter() = p and
Expand Down
Original file line number Diff line number Diff line change
@@ -1,13 +1,19 @@
import csharp
import semmle.code.csharp.dataflow.internal.BaseSSA

from AssignableRead ar, BaseSsa::Definition ssaDef, AssignableDefinition def, LocalScopeVariable v
from
AssignableRead ar, BaseSsa::SsaExplicitWrite ssaDef, AssignableDefinition def,
LocalScopeVariable v
where
ar = ssaDef.getARead() and
def = ssaDef.getDefinition() and
v = def.getTarget() and
not exists(Ssa::ExplicitDefinition edef |
edef.getADefinition() = def and
edef.getARead() = ar
) and
not exists(Ssa::ImplicitParameterDefinition edef |
edef.getParameter() = def.(AssignableDefinitions::ImplicitParameterDefinition).getParameter() and
edef.getARead() = ar
)
select ar, def
Loading