Skip to content

Commit

Permalink
Merge branch 'main' into 13332-codeql-model-editor-csharp
Browse files Browse the repository at this point in the history
  • Loading branch information
felicitymay authored Feb 28, 2024
2 parents efff014 + ab11068 commit 377ef59
Show file tree
Hide file tree
Showing 55 changed files with 2,190 additions and 2,107 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -11,8 +11,7 @@
| copy.cpp:13:9:13:9 | operator= | protected_cc::Sub2& protected_cc::Sub2::operator=(protected_cc::Sub2 const&) | | |
| copy.cpp:13:9:13:9 | operator= | protected_cc::Sub2& protected_cc::Sub2::operator=(protected_cc::Sub2&&) | | |
| copy.cpp:17:9:17:9 | HasMember | void protected_cc::HasMember::HasMember() | deleted | |
| copy.cpp:17:9:17:9 | HasMember | void protected_cc::HasMember::HasMember(protected_cc::HasMember const&) | | |
| copy.cpp:17:9:17:9 | HasMember | void protected_cc::HasMember::HasMember(protected_cc::HasMember&&) | | |
| copy.cpp:17:9:17:9 | HasMember | void protected_cc::HasMember::HasMember(protected_cc::HasMember const&) | deleted | |
| copy.cpp:17:9:17:9 | operator= | protected_cc::HasMember& protected_cc::HasMember::operator=(protected_cc::HasMember const&) | | |
| copy.cpp:17:9:17:9 | operator= | protected_cc::HasMember& protected_cc::HasMember::operator=(protected_cc::HasMember&&) | | |
| copy.cpp:25:5:25:5 | C | void deleted_cc::C::C(deleted_cc::C const&) | deleted | |
Expand Down
1 change: 0 additions & 1 deletion cpp/ql/test/library-tests/specifiers2/specifiers2.expected
Original file line number Diff line number Diff line change
Expand Up @@ -186,7 +186,6 @@
| Variable | specifiers2pp.cpp:16:13:16:22 | privateInt | privateInt | private |
| Variable | specifiers2pp.cpp:17:21:17:30 | mutableInt | mutableInt | private |
| Variable | specifiers2pp.cpp:20:13:20:24 | protectedInt | protectedInt | protected |
| Variable | specifiers2pp.cpp:52:25:52:27 | vci | vci | static |
| VariableDeclarationEntry | specifiers2.c:5:12:5:12 | declaration of i | i | extern |
| VariableDeclarationEntry | specifiers2.c:6:12:6:12 | declaration of i | i | extern |
| VariableDeclarationEntry | specifiers2.c:8:12:8:12 | declaration of j | j | extern |
Expand Down
4 changes: 0 additions & 4 deletions csharp/ql/consistency-queries/DataFlowConsistency.ql
Original file line number Diff line number Diff line change
Expand Up @@ -47,8 +47,6 @@ private module Input implements InputSig<CsharpDataFlow> {
or
not exists(LocalFlow::getAPostUpdateNodeForArg(n.getControlFlowNode()))
or
n instanceof ImplicitCapturedArgumentNode
or
n instanceof ParamsArgumentNode
or
n.asExpr() instanceof CIL::Expr
Expand Down Expand Up @@ -104,8 +102,6 @@ private module Input implements InputSig<CsharpDataFlow> {
not split = cfn.getASplit()
)
or
call instanceof TransitiveCapturedDataFlowCall
or
call.(NonDelegateDataFlowCall).getDispatchCall().isReflection()
)
}
Expand Down
17 changes: 17 additions & 0 deletions csharp/ql/consistency-queries/VariableCaptureConsistency.ql
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
import csharp
import semmle.code.csharp.dataflow.internal.DataFlowPrivate::VariableCapture::Flow::ConsistencyChecks
private import semmle.code.csharp.dataflow.internal.DataFlowPrivate::VariableCapture::Flow::ConsistencyChecks as ConsistencyChecks
private import semmle.code.csharp.controlflow.BasicBlocks
private import semmle.code.csharp.controlflow.internal.ControlFlowGraphImpl

query predicate uniqueEnclosingCallable(BasicBlock bb, string msg) {
ConsistencyChecks::uniqueEnclosingCallable(bb, msg) and
getNodeCfgScope(bb.getFirstNode()) instanceof Callable
}

query predicate consistencyOverview(string msg, int n) { none() }

query predicate uniqueCallableLocation(Callable c, string msg) {
ConsistencyChecks::uniqueCallableLocation(c, msg) and
count(c.getBody()) = 1
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
---
category: majorAnalysis
---
* Improved support for flow through captured variables that properly adheres to inter-procedural control flow.
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
---
category: minorAnalysis
---
* C# 12: Add QL library support (`ExperimentalAttribute`) for the experimental attribute.
102 changes: 59 additions & 43 deletions csharp/ql/lib/semmle/code/csharp/controlflow/internal/PreSsa.qll
Original file line number Diff line number Diff line change
Expand Up @@ -31,9 +31,52 @@ module PreSsa {
}

predicate implicitEntryDef(Callable c, SsaInput::BasicBlock bb, SsaInput::SourceVariable v) {
not v instanceof LocalScopeVariable and
c = v.getACallable() and
scopeFirst(c, bb)
scopeFirst(c, bb) and
(
not v instanceof LocalScopeVariable
or
v.(SimpleLocalScopeVariable).isReadonlyCapturedBy(c)
)
}

/** Holds if `a` is assigned in callable `c`. */
pragma[nomagic]
private predicate assignableDefinition(Assignable a, Callable c) {
exists(AssignableDefinition def |
def.getTarget() = a and
c = def.getEnclosingCallable()
|
not c instanceof Constructor or
a instanceof LocalScopeVariable
)
}

pragma[nomagic]
private predicate assignableUniqueWriter(Assignable a, Callable c) {
c = unique(Callable c0 | assignableDefinition(a, c0) | c0)
}

/** Holds if `a` is accessed in callable `c`. */
pragma[nomagic]
private predicate assignableAccess(Assignable a, Callable c) {
exists(AssignableAccess aa | aa.getTarget() = a | c = aa.getEnclosingCallable())
}

/**
* A local scope variable that is amenable to SSA analysis.
*
* This is either a local variable that is not captured, or one
* where all writes happen in the defining callable.
*/
class SimpleLocalScopeVariable extends LocalScopeVariable {
SimpleLocalScopeVariable() { assignableUniqueWriter(this, this.getCallable()) }

/** Holds if this local scope variable is read-only captured by `c`. */
predicate isReadonlyCapturedBy(Callable c) {
assignableAccess(this, c) and
c != this.getCallable()
}
}

module SsaInput implements SsaImplCommon::InputSig<Location> {
Expand All @@ -47,40 +90,6 @@ module PreSsa {
ExitBasicBlock() { scopeLast(_, this.getLastElement(), _) }
}

/** Holds if `a` is assigned in non-constructor callable `c`. */
pragma[nomagic]
private predicate assignableDefinition(Assignable a, Callable c) {
exists(AssignableDefinition def | def.getTarget() = a |
c = def.getEnclosingCallable() and
not c instanceof Constructor
)
}

/** Holds if `a` is accessed in callable `c`. */
pragma[nomagic]
private predicate assignableAccess(Assignable a, Callable c) {
exists(AssignableAccess aa | aa.getTarget() = a | c = aa.getEnclosingCallable())
}

pragma[nomagic]
private predicate assignableNoCapturing(Assignable a, Callable c) {
assignableAccess(a, c) and
/*
* The code below is equivalent to
* ```ql
* not exists(Callable other | assignableDefinition(a, other) | other != c)
* ```
* but it avoids a Cartesian product in the compiler generated antijoin
* predicate.
*/

(
not assignableDefinition(a, _)
or
c = unique(Callable c0 | assignableDefinition(a, c0) | c0)
)
}

pragma[noinline]
private predicate assignableNoComplexQualifiers(Assignable a) {
forall(QualifiableExpr qe | qe.(AssignableAccess).getTarget() = a | qe.targetIsThisInstance())
Expand All @@ -94,15 +103,22 @@ module PreSsa {
private Callable c;

SourceVariable() {
assignableAccess(this, c) and
(
this instanceof LocalScopeVariable
this instanceof SimpleLocalScopeVariable
or
this = any(Field f | not f.isVolatile())
or
this = any(TrivialProperty tp | not tp.isOverridableOrImplementable())
) and
assignableNoCapturing(this, c) and
assignableNoComplexQualifiers(this)
(
this = any(Field f | not f.isVolatile())
or
this = any(TrivialProperty tp | not tp.isOverridableOrImplementable())
) and
(
not assignableDefinition(this, _)
or
assignableUniqueWriter(this, c)
) and
assignableNoComplexQualifiers(this)
)
}

/** Gets a callable in which this simple assignable can be analyzed. */
Expand Down
24 changes: 2 additions & 22 deletions csharp/ql/lib/semmle/code/csharp/dataflow/Nullness.qll
Original file line number Diff line number Diff line change
Expand Up @@ -218,19 +218,6 @@ private predicate isNullDefaultArgument(Ssa::ExplicitDefinition def, AlwaysNullE
)
}

/**
* Holds if `edef` is an implicit entry definition for a captured variable that
* may be guarded, because a call to the capturing callable is guarded.
*/
private predicate isMaybeGuardedCapturedDef(Ssa::ImplicitEntryDefinition edef) {
exists(Ssa::ExplicitDefinition def, ControlFlow::Nodes::ElementNode c, G::Guard g, NullValue nv |
def.isCapturedVariableDefinitionFlowIn(edef, c, _) and
g = def.getARead() and
g.controlsNode(c, nv) and
nv.isNonNull()
)
}

/** Holds if `def` is an SSA definition that may be `null`. */
private predicate defMaybeNull(Ssa::Definition def, string msg, Element reason) {
not nonNullDef(def) and
Expand Down Expand Up @@ -268,7 +255,6 @@ private predicate defMaybeNull(Ssa::Definition def, string msg, Element reason)
exists(Dereference d | dereferenceAt(_, _, def, d) |
d.hasNullableType() and
not def instanceof Ssa::PhiNode and
not isMaybeGuardedCapturedDef(def) and
reason = def.getSourceVariable().getAssignable() and
msg = "because it has a nullable type"
)
Expand Down Expand Up @@ -583,14 +569,8 @@ class Dereference extends G::DereferenceableExpr {
*/
predicate isAlwaysNull(Ssa::SourceVariable v) {
this = v.getAnAccess() and
// Exclude fields, properties, and captured variables, as they may not have an
// accurate SSA representation
v.getAssignable() =
any(LocalScopeVariable lsv |
strictcount(Callable c |
c = any(AssignableDefinition ad | ad.getTarget() = lsv).getEnclosingCallable()
) = 1
) and
// Exclude fields and properties, as they may not have an accurate SSA representation
v.getAssignable() instanceof LocalScopeVariable and
(
forex(Ssa::Definition def0 | this = def0.getARead() | this.isAlwaysNull0(def0))
or
Expand Down
22 changes: 10 additions & 12 deletions csharp/ql/lib/semmle/code/csharp/dataflow/SSA.qll
Original file line number Diff line number Diff line change
Expand Up @@ -447,6 +447,8 @@ module Ssa {
final AssignableDefinition getADefinition() { result = SsaImpl::getADefinition(this) }

/**
* DEPRECATED.
*
* Holds if this definition updates a captured local scope variable, and the updated
* value may be read from the implicit entry definition `def` using one or more calls
* (as indicated by `additionalCalls`), starting from call `c`.
Expand All @@ -467,13 +469,15 @@ module Ssa {
* If this definition is the update of `i` on line 5, then the value may be read inside
* `M2` via the call on line 6.
*/
final predicate isCapturedVariableDefinitionFlowIn(
deprecated final predicate isCapturedVariableDefinitionFlowIn(
ImplicitEntryDefinition def, ControlFlow::Nodes::ElementNode c, boolean additionalCalls
) {
SsaImpl::isCapturedVariableDefinitionFlowIn(this, def, c, additionalCalls)
none()
}

/**
* DEPRECATED.
*
* Holds if this definition updates a captured local scope variable, and the updated
* value may be read from the implicit call definition `cdef` using one or more calls
* (as indicated by `additionalCalls`).
Expand All @@ -494,10 +498,10 @@ module Ssa {
* If this definition is the update of `i` on line 4, then the value may be read outside
* of `M2` via the call on line 5.
*/
final predicate isCapturedVariableDefinitionFlowOut(
deprecated final predicate isCapturedVariableDefinitionFlowOut(
ImplicitCallDefinition cdef, boolean additionalCalls
) {
SsaImpl::isCapturedVariableDefinitionFlowOut(this, cdef, additionalCalls)
none()
}

override Element getElement() { result = ad.getElement() }
Expand Down Expand Up @@ -526,8 +530,6 @@ module Ssa {
or
SsaImpl::updatesNamedFieldOrProp(bb, i, _, v, _)
or
SsaImpl::updatesCapturedVariable(bb, i, _, v, _, _)
or
SsaImpl::variableWriteQualifier(bb, i, v, _)
)
}
Expand Down Expand Up @@ -572,10 +574,9 @@ module Ssa {
private Call c;

ImplicitCallDefinition() {
exists(ControlFlow::BasicBlock bb, SourceVariable v, int i | this.definesAt(v, bb, i) |
exists(ControlFlow::BasicBlock bb, SourceVariable v, int i |
this.definesAt(v, bb, i) and
SsaImpl::updatesNamedFieldOrProp(bb, i, c, v, _)
or
SsaImpl::updatesCapturedVariable(bb, i, c, v, _, _)
)
}

Expand All @@ -593,9 +594,6 @@ module Ssa {
result.getEnclosingCallable() = setter and
result.getTarget() = this.getSourceVariable().getAssignable()
)
or
SsaImpl::updatesCapturedVariable(_, _, this.getCall(), _, result, _) and
result.getTarget() = this.getSourceVariable().getAssignable()
}

override string toString() {
Expand Down
32 changes: 23 additions & 9 deletions csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,16 @@ module BaseSsa {
)
}

private predicate implicitEntryDef(
Callable c, ControlFlow::BasicBlocks::EntryBlock bb, SsaInput::SourceVariable v
) {
v.isReadonlyCapturedBy(c) and
c = bb.getCallable()
}

private module SsaInput implements SsaImplCommon::InputSig<Location> {
private import semmle.code.csharp.controlflow.internal.PreSsa

class BasicBlock = ControlFlow::BasicBlock;

BasicBlock getImmediateBasicBlockDominator(BasicBlock bb) {
Expand All @@ -35,20 +44,17 @@ module BaseSsa {

class ExitBasicBlock = ControlFlow::BasicBlocks::ExitBlock;

pragma[noinline]
private Callable getAnAssigningCallable(LocalScopeVariable v) {
result = any(AssignableDefinition def | def.getTarget() = v).getEnclosingCallable()
}

class SourceVariable extends LocalScopeVariable {
SourceVariable() { not getAnAssigningCallable(this) != getAnAssigningCallable(this) }
}
class SourceVariable = PreSsa::SimpleLocalScopeVariable;

predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain) {
exists(AssignableDefinition def |
definitionAt(def, bb, i, v) and
if def.isCertain() then certain = true else certain = false
)
or
implicitEntryDef(_, bb, v) and
i = -1 and
certain = true
}

predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain) {
Expand Down Expand Up @@ -87,7 +93,15 @@ module BaseSsa {
not result instanceof PhiNode
}

Location getLocation() { result = this.getDefinition().getLocation() }
Location getLocation() {
result = this.getDefinition().getLocation()
or
exists(Callable c, SsaInput::BasicBlock bb, SsaInput::SourceVariable v |
this.definesAt(v, bb, -1) and
implicitEntryDef(c, bb, v) and
result = c.getLocation()
)
}
}

class PhiNode extends SsaImpl::PhiNode, Definition {
Expand Down
Loading

0 comments on commit 377ef59

Please sign in to comment.