Skip to content

Commit 896e377

Browse files
committed
C#: Replace Ssa::ExplicitDefinition with SsaExplicitWrite.
1 parent 3525301 commit 896e377

18 files changed

Lines changed: 67 additions & 90 deletions

File tree

csharp/ql/consistency-queries/SsaConsistency.ql

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,8 @@ query predicate localDeclWithSsaDef(LocalVariableDeclExpr d) {
77
// Local variables in C# must be initialized before every use, so uninitialized
88
// local variables should not have an SSA definition, as that would imply that
99
// the declaration is live (can reach a use without passing through a definition)
10-
exists(ExplicitDefinition def |
11-
d = def.getADefinition().(AssignableDefinitions::LocalVariableDefinition).getDeclaration()
10+
exists(SsaExplicitWrite def |
11+
d = def.getDefinition().(AssignableDefinitions::LocalVariableDefinition).getDeclaration()
1212
|
1313
not d = any(ForeachStmt fs).getVariableDeclExpr() and
1414
not d = any(SpecificCatchClause scc).getVariableDeclExpr() and

csharp/ql/lib/semmle/code/csharp/Assignable.qll

Lines changed: 1 addition & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -488,13 +488,7 @@ class AssignableDefinition extends TAssignableDefinition {
488488
*/
489489
pragma[nomagic]
490490
AssignableRead getAFirstRead() {
491-
exists(Ssa::ExplicitDefinition def | result = Ssa::ssaGetAFirstUse(def) |
492-
this = def.getADefinition()
493-
)
494-
or
495-
exists(Ssa::ImplicitParameterDefinition def | result = Ssa::ssaGetAFirstUse(def) |
496-
this.(AssignableDefinitions::ImplicitParameterDefinition).getParameter() = def.getParameter()
497-
)
491+
exists(SsaExplicitWrite def | result = Ssa::ssaGetAFirstUse(def) | this = def.getDefinition())
498492
}
499493

500494
/** Gets a textual representation of this assignable definition. */

csharp/ql/lib/semmle/code/csharp/controlflow/Guards.qll

Lines changed: 3 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -588,7 +588,7 @@ private SsaDefinition getAnSsaQualifier(Expr e, ControlFlowNode cfn) {
588588
private AssignableAccess getATrackedAccess(SsaDefinition def, ControlFlowNode cfn) {
589589
result = def.getARead() and cfn = result.getControlFlowNode()
590590
or
591-
result = def.(Ssa::ExplicitDefinition).getADefinition().getTargetAccess() and
591+
result = def.(SsaExplicitWrite).getDefinition().getTargetAccess() and
592592
cfn = def.getControlFlowNode()
593593
}
594594

@@ -830,9 +830,7 @@ module Internal {
830830
).getARead()
831831
}
832832

833-
private predicate nullDef(Ssa::ExplicitDefinition def) {
834-
nullValueImplied(def.getADefinition().getSource())
835-
}
833+
private predicate nullDef(SsaExplicitWrite def) { nullValueImplied(def.getValue()) }
836834

837835
predicate nonNullValueImplied(Expr e) {
838836
nonNullValue(e)
@@ -845,9 +843,7 @@ module Internal {
845843
).getARead()
846844
}
847845

848-
private predicate nonNullDef(Ssa::ExplicitDefinition def) {
849-
nonNullValueImplied(def.getADefinition().getSource())
850-
}
846+
private predicate nonNullDef(SsaExplicitWrite def) { nonNullValueImplied(def.getValue()) }
851847

852848
/** A callable that always returns a non-`null` value. */
853849
private class NonNullCallable extends Callable {

csharp/ql/lib/semmle/code/csharp/dataflow/Nullness.qll

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -80,9 +80,7 @@ class AlwaysNullExpr extends Expr {
8080
}
8181

8282
/** Holds if SSA definition `def` is always `null`. */
83-
private predicate nullDef(Ssa::ExplicitDefinition def) {
84-
def.getADefinition().getSource() instanceof AlwaysNullExpr
85-
}
83+
private predicate nullDef(SsaExplicitWrite def) { def.getValue() instanceof AlwaysNullExpr }
8684

8785
/** An expression that is never `null`. */
8886
class NonNullExpr extends Expr {
@@ -108,10 +106,10 @@ class NonNullExpr extends Expr {
108106
}
109107

110108
/** Holds if SSA definition `def` is never `null`. */
111-
private predicate nonNullDef(Ssa::ExplicitDefinition def) {
112-
def.getADefinition().getSource() instanceof NonNullExpr
109+
private predicate nonNullDef(SsaExplicitWrite def) {
110+
def.getValue() instanceof NonNullExpr
113111
or
114-
exists(AssignableDefinition ad | ad = def.getADefinition() |
112+
exists(AssignableDefinition ad | ad = def.getDefinition() |
115113
ad instanceof AssignableDefinitions::PatternDefinition
116114
or
117115
ad =
@@ -201,7 +199,7 @@ private predicate defMaybeNull(SsaDefinition def, ControlFlowNode node, string m
201199
not de = any(Ssa::PhiNode phi).getARead() and
202200
// Don't use a check as reason if there is a `null` assignment
203201
// or argument
204-
not def.(Ssa::ExplicitDefinition).getADefinition().getSource() instanceof MaybeNullExpr and
202+
not def.(SsaExplicitWrite).getValue() instanceof MaybeNullExpr and
205203
not isMaybeNullArgument(def, _)
206204
)
207205
or
@@ -219,7 +217,7 @@ private predicate defMaybeNull(SsaDefinition def, ControlFlowNode node, string m
219217
msg = "because the parameter has a null default value"
220218
or
221219
// If the source of a variable is `null` then the variable may be `null`
222-
exists(AssignableDefinition adef | adef = def.(Ssa::ExplicitDefinition).getADefinition() |
220+
exists(AssignableDefinition adef | adef = def.(SsaExplicitWrite).getDefinition() |
223221
adef.getSource() = maybeNullExpr(node.asExpr()) and
224222
reason = adef.getExpr() and
225223
msg = "because of $@ assignment"
@@ -351,7 +349,7 @@ class Dereference extends G::DereferenceableExpr {
351349

352350
private predicate isAlwaysNull0(SsaDefinition def) {
353351
forall(SsaDefinition input | input = getAnUltimateDefinition(def) |
354-
input.(Ssa::ExplicitDefinition).getADefinition().getSource() instanceof AlwaysNullExpr
352+
input.(SsaExplicitWrite).getValue() instanceof AlwaysNullExpr
355353
) and
356354
not nonNullDef(def) and
357355
this = def.getARead() and

csharp/ql/lib/semmle/code/csharp/dataflow/SSA.qll

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -438,19 +438,25 @@ module Ssa {
438438
}
439439

440440
/**
441+
* DEPRECATED: Use `SsaExplicitWrite` instead.
442+
*
441443
* An SSA definition that corresponds to an explicit assignable definition.
442444
*/
443-
class ExplicitDefinition extends Definition, SsaImpl::WriteDefinition {
445+
deprecated class ExplicitDefinition extends Definition, SsaImpl::WriteDefinition {
444446
AssignableDefinition ad;
445447

446448
ExplicitDefinition() { SsaImpl::explicitDefinition(this, _, ad) }
447449

448450
/**
451+
* DEPRECATED: Use `SsaExplicitWrite.getDefinition()` instead.
452+
*
449453
* Gets an underlying assignable definition. The result is always unique,
450454
* except for pathological `out`/`ref` assignments like `M(out x, out x)`,
451455
* where there may be more than one underlying definition.
452456
*/
453-
final AssignableDefinition getADefinition() { result = SsaImpl::getADefinition(this) }
457+
deprecated final AssignableDefinition getADefinition() {
458+
result = SsaImpl::getADefinition(this)
459+
}
454460

455461
/**
456462
* DEPRECATED.

csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowPrivate.qll

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -252,7 +252,7 @@ module VariableCapture {
252252
or
253253
exists(SsaDefinition def, AssignableDefinition adef |
254254
LocalFlow::defAssigns(adef, _, _, e1) and
255-
def.getAnUltimateDefinition().(Ssa::ExplicitDefinition).getADefinition() = adef and
255+
def.getAnUltimateDefinition().(SsaExplicitWrite).getDefinition() = adef and
256256
def.getARead().getControlFlowNode() = e2
257257
)
258258
}
@@ -580,8 +580,8 @@ module LocalFlow {
580580
or
581581
ThisFlow::adjacentThisRefs(nodeFrom.(PostUpdateNode).getPreUpdateNode(), nodeTo)
582582
or
583-
exists(AssignableDefinition def, ControlFlowNode cfn, Ssa::ExplicitDefinition ssaDef |
584-
ssaDef.getADefinition() = def and
583+
exists(AssignableDefinition def, ControlFlowNode cfn, SsaExplicitWrite ssaDef |
584+
ssaDef.getDefinition() = def and
585585
ssaDef.getControlFlowNode() = cfn and
586586
nodeFrom = TAssignableDefinitionNode(def, cfn) and
587587
nodeTo.(SsaDefinitionNode).getDefinition() = ssaDef
@@ -2205,12 +2205,11 @@ private predicate readContentStep(Node node1, Content c, Node node2) {
22052205
c instanceof ElementContent
22062206
or
22072207
exists(
2208-
ForeachStmt fs, Ssa::ExplicitDefinition def,
2209-
AssignableDefinitions::LocalVariableDefinition defTo
2208+
ForeachStmt fs, SsaExplicitWrite def, AssignableDefinitions::LocalVariableDefinition defTo
22102209
|
22112210
node1.asExpr() = fs.getIterableExpr() and
22122211
defTo.getDeclaration() = fs.getVariableDeclExpr() and
2213-
def.getADefinition() = defTo and
2212+
def.getDefinition() = defTo and
22142213
node2.(SsaDefinitionNode).getDefinition() = def and
22152214
c instanceof ElementContent
22162215
)

csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -810,7 +810,7 @@ private module Cached {
810810
}
811811

812812
cached
813-
AssignableDefinition getADefinition(Ssa::ExplicitDefinition def) {
813+
deprecated AssignableDefinition getADefinition(Ssa::ExplicitDefinition def) {
814814
exists(Ssa::SourceVariable v, AssignableDefinition ad | explicitDefinition(def, v, ad) |
815815
result = ad or
816816
result = getASameOutRefDefAfter(v, ad)
@@ -843,7 +843,9 @@ private module Cached {
843843
}
844844

845845
cached
846-
predicate explicitDefinition(WriteDefinition def, Ssa::SourceVariable v, AssignableDefinition ad) {
846+
deprecated predicate explicitDefinition(
847+
WriteDefinition def, Ssa::SourceVariable v, AssignableDefinition ad
848+
) {
847849
exists(BasicBlock bb, int i |
848850
def.definesAt(v, bb, i) and
849851
variableDefinition(bb, i, v, ad)
@@ -1008,7 +1010,7 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
10081010
* as we, conservatively, consider such definitions to be certain.
10091011
*/
10101012
predicate allowFlowIntoUncertainDef(UncertainWriteDefinition def) {
1011-
def instanceof Ssa::ExplicitDefinition
1013+
def instanceof SsaExplicitWrite
10121014
or
10131015
def =
10141016
any(Ssa::ImplicitQualifierDefinition qdef |

csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/RangeUtils.qll

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ private module Impl {
1919
}
2020

2121
/** Holds if SSA definition `def` equals `e + delta`. */
22-
predicate ssaUpdateStep(ExplicitDefinition def, ExprNode e, int delta) {
22+
predicate ssaUpdateStep(SsaExplicitWrite def, ExprNode e, int delta) {
2323
exists(ControlFlowNode cfn | cfn = def.getControlFlowNode() |
2424
e = cfn.(ExprNode::Assignment).getRightOperand() and
2525
delta = 0 and

csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll

Lines changed: 10 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ module Private {
3535

3636
class Expr = CS::ControlFlowNodes::ExprNode;
3737

38-
class VariableUpdate = CS::Ssa::ExplicitDefinition;
38+
class VariableUpdate = CS::SsaExplicitWrite;
3939

4040
class Field = CS::Field;
4141

@@ -122,37 +122,25 @@ private module Impl {
122122
}
123123

124124
/** Returns the underlying variable update of the explicit SSA variable `v`. */
125-
Ssa::ExplicitDefinition getExplicitSsaAssignment(Ssa::ExplicitDefinition v) { result = v }
125+
SsaExplicitWrite getExplicitSsaAssignment(SsaExplicitWrite v) { result = v }
126126

127127
/** Returns the assignment of the variable update `def`. */
128-
ExprNode getExprFromSsaAssignment(Ssa::ExplicitDefinition def) {
129-
exists(AssignableDefinition adef |
130-
adef = def.getADefinition() and
131-
hasChild(adef.getExpr(), adef.getSource(), def.getControlFlowNode(), result)
132-
)
133-
or
134-
exists(AssignableDefinitions::AssignOperationDefinition adef |
135-
adef = def.getADefinition() and
136-
result.getExpr() = adef.getSource()
137-
)
138-
}
128+
ExprNode getExprFromSsaAssignment(SsaExplicitWrite def) { result.getExpr() = def.getValue() }
139129

140130
/** Holds if `def` can have any sign. */
141-
predicate explicitSsaDefWithAnySign(Ssa::ExplicitDefinition def) {
142-
not exists(def.getADefinition().getSource()) and
143-
not def.getElement() instanceof MutatorOperation
131+
predicate explicitSsaDefWithAnySign(SsaExplicitWrite def) {
132+
not exists(def.getValue()) and
133+
not def.getDefiningExpr() instanceof MutatorOperation
144134
}
145135

146136
/** Returns the operand of the operation if `def` is a decrement. */
147-
ExprNode getDecrementOperand(Ssa::ExplicitDefinition def) {
148-
hasChild(def.getElement(), def.getElement().(DecrementOperation).getOperand(),
149-
def.getControlFlowNode(), result)
137+
ExprNode getDecrementOperand(SsaExplicitWrite def) {
138+
result.getExpr() = def.getDefiningExpr().(DecrementOperation).getOperand()
150139
}
151140

152141
/** Returns the operand of the operation if `def` is an increment. */
153-
ExprNode getIncrementOperand(Ssa::ExplicitDefinition def) {
154-
hasChild(def.getElement(), def.getElement().(IncrementOperation).getOperand(),
155-
def.getControlFlowNode(), result)
142+
ExprNode getIncrementOperand(SsaExplicitWrite def) {
143+
result.getExpr() = def.getDefiningExpr().(IncrementOperation).getOperand()
156144
}
157145

158146
/** Gets the variable underlying the implicit SSA variable `def`. */

csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaUtils.qll

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -17,9 +17,9 @@ class SsaVariable extends SsaDefinition {
1717

1818
/** Gets a node that reads `src` via an SSA explicit definition. */
1919
ExprNode getAnExplicitDefinitionRead(ExprNode src) {
20-
exists(ExplicitDefinition def |
20+
exists(SsaExplicitWrite def |
2121
def.getARead().getControlFlowNode() = result and
22-
hasChild(def.getElement(), def.getADefinition().getSource(), def.getControlFlowNode(), src)
22+
hasChild(def.getDefiningExpr(), def.getValue(), def.getControlFlowNode(), src)
2323
)
2424
}
2525

@@ -45,15 +45,15 @@ ExprNode ssaRead(SsaDefinition v, int delta) {
4545
delta = d1 + c.getIntValue()
4646
)
4747
or
48-
v.(ExplicitDefinition).getControlFlowNode().(ExprNode::PreIncrExpr) = result and delta = 0
48+
v.(SsaExplicitWrite).getControlFlowNode().(ExprNode::PreIncrExpr) = result and delta = 0
4949
or
50-
v.(ExplicitDefinition).getControlFlowNode().(ExprNode::PreDecrExpr) = result and delta = 0
50+
v.(SsaExplicitWrite).getControlFlowNode().(ExprNode::PreDecrExpr) = result and delta = 0
5151
or
52-
v.(ExplicitDefinition).getControlFlowNode().(ExprNode::PostIncrExpr) = result and delta = 1 // x++ === ++x - 1
52+
v.(SsaExplicitWrite).getControlFlowNode().(ExprNode::PostIncrExpr) = result and delta = 1 // x++ === ++x - 1
5353
or
54-
v.(ExplicitDefinition).getControlFlowNode().(ExprNode::PostDecrExpr) = result and delta = -1 // x-- === --x + 1
54+
v.(SsaExplicitWrite).getControlFlowNode().(ExprNode::PostDecrExpr) = result and delta = -1 // x-- === --x + 1
5555
or
56-
v.(ExplicitDefinition).getControlFlowNode().(ExprNode::Assignment) = result and delta = 0
56+
v.(SsaExplicitWrite).getControlFlowNode().(ExprNode::Assignment) = result and delta = 0
5757
or
5858
result.(ExprNode::AssignExpr).getRightOperand() = ssaRead(v, delta)
5959
}

0 commit comments

Comments
 (0)