@@ -113,15 +113,15 @@ predicate dereference(Expr e) {
113113 *
114114 * The `VarAccess` is included for nicer error reporting.
115115 */
116- private ControlFlowNode varDereference ( SsaVariable v , VarAccess va ) {
116+ private ControlFlowNode varDereference ( SsaDefinition v , VarAccess va ) {
117117 dereference ( result .asExpr ( ) ) and
118118 result .asExpr ( ) = sameValue ( v , va )
119119}
120120
121121/**
122122 * The first dereference of a variable in a given `BasicBlock`.
123123 */
124- private predicate firstVarDereferenceInBlock ( BasicBlock bb , SsaVariable v , VarAccess va ) {
124+ private predicate firstVarDereferenceInBlock ( BasicBlock bb , SsaDefinition v , VarAccess va ) {
125125 exists ( ControlFlowNode n |
126126 varDereference ( v , va ) = n and
127127 n .getBasicBlock ( ) = bb and
@@ -135,14 +135,14 @@ private predicate firstVarDereferenceInBlock(BasicBlock bb, SsaVariable v, VarAc
135135}
136136
137137/** A variable suspected of being `null`. */
138- private predicate varMaybeNull ( SsaVariable v , ControlFlowNode node , string msg , Expr reason ) {
138+ private predicate varMaybeNull ( SsaDefinition v , ControlFlowNode node , string msg , Expr reason ) {
139139 // A variable compared to null might be null.
140140 exists ( Expr e |
141141 reason = e and
142142 msg = "as suggested by $@ null guard" and
143143 guardSuggestsVarMaybeNull ( e , v ) and
144- node = v .getCfgNode ( ) and
145- not v instanceof SsaPhiNode and
144+ node = v .getControlFlowNode ( ) and
145+ not v instanceof SsaPhiDefinition and
146146 not clearlyNotNull ( v ) and
147147 // Comparisons in finally blocks are excluded since missing exception edges in the CFG could otherwise yield FPs.
148148 not exists ( TryStmt try | try .getFinally ( ) = e .getEnclosingStmt ( ) .getEnclosingStmt * ( ) ) and
@@ -151,13 +151,13 @@ private predicate varMaybeNull(SsaVariable v, ControlFlowNode node, string msg,
151151 not exists ( MethodCall ma | ma .getAnArgument ( ) .getAChildExpr * ( ) = e )
152152 ) and
153153 // Don't use a guard as reason if there is a null assignment.
154- not v .( SsaExplicitUpdate ) .getDefiningExpr ( ) .( VariableAssign ) .getSource ( ) = nullExpr ( )
154+ not v .( SsaExplicitWrite ) .getDefiningExpr ( ) .( VariableAssign ) .getSource ( ) = nullExpr ( )
155155 )
156156 or
157157 // A parameter might be null if there is a null argument somewhere.
158158 exists ( Parameter p , Expr arg |
159- v .( SsaImplicitInit ) . isParameterDefinition ( p ) and
160- node = v .getCfgNode ( ) and
159+ v .( SsaParameterInit ) . getParameter ( ) = p and
160+ node = v .getControlFlowNode ( ) and
161161 p .getAnArgument ( ) = arg and
162162 reason = arg and
163163 msg = "because of $@ null argument" and
@@ -167,7 +167,7 @@ private predicate varMaybeNull(SsaVariable v, ControlFlowNode node, string msg,
167167 or
168168 // If the source of a variable is null then the variable may be null.
169169 exists ( VariableAssign def |
170- v .( SsaExplicitUpdate ) .getDefiningExpr ( ) = def and
170+ v .( SsaExplicitWrite ) .getDefiningExpr ( ) = def and
171171 def .getSource ( ) = nullExpr ( node .asExpr ( ) ) and
172172 reason = def and
173173 msg = "because of $@ assignment"
@@ -179,26 +179,26 @@ private Expr nonEmptyExpr() {
179179 // An array creation with a known positive size is trivially non-empty.
180180 result .( ArrayCreationExpr ) .getFirstDimensionSize ( ) > 0
181181 or
182- exists ( SsaVariable v |
182+ exists ( SsaDefinition v |
183183 // A use of an array variable is non-empty if...
184- result = v .getAUse ( ) and
184+ result = v .getARead ( ) and
185185 v .getSourceVariable ( ) .getType ( ) instanceof Array
186186 |
187187 // ...its definition is non-empty...
188- v .( SsaExplicitUpdate ) . getDefiningExpr ( ) . ( VariableAssign ) . getSource ( ) = nonEmptyExpr ( )
188+ v .( SsaExplicitWrite ) . getValue ( ) = nonEmptyExpr ( )
189189 or
190190 // ...or it is guarded by a condition proving its length to be non-zero.
191191 exists ( ConditionBlock cond , boolean branch , FieldAccess length |
192192 cond .controls ( result .getBasicBlock ( ) , branch ) and
193193 cond .getCondition ( ) = nonZeroGuard ( length , branch ) and
194194 length .getField ( ) .hasName ( "length" ) and
195- length .getQualifier ( ) = v .getAUse ( )
195+ length .getQualifier ( ) = v .getARead ( )
196196 )
197197 )
198198 or
199- exists ( SsaVariable v |
199+ exists ( SsaDefinition v |
200200 // A use of a Collection variable is non-empty if...
201- result = v .getAUse ( ) and
201+ result = v .getARead ( ) and
202202 v .getSourceVariable ( ) .getType ( ) instanceof CollectionType and
203203 exists ( ConditionBlock cond , boolean branch , Expr c |
204204 // ...it is guarded by a condition...
@@ -216,13 +216,13 @@ private Expr nonEmptyExpr() {
216216 // ...and the condition proves that it is non-empty, either by using the `isEmpty` method...
217217 c .( MethodCall ) .getMethod ( ) .hasName ( "isEmpty" ) and
218218 branch = false and
219- c .( MethodCall ) .getQualifier ( ) = v .getAUse ( )
219+ c .( MethodCall ) .getQualifier ( ) = v .getARead ( )
220220 or
221221 // ...or a check on its `size`.
222222 exists ( MethodCall size |
223223 c = nonZeroGuard ( size , branch ) and
224224 size .getMethod ( ) .hasName ( "size" ) and
225- size .getQualifier ( ) = v .getAUse ( )
225+ size .getQualifier ( ) = v .getARead ( )
226226 )
227227 )
228228 )
@@ -249,9 +249,9 @@ private predicate impossibleEdge(BasicBlock bb1, BasicBlock bb2) {
249249}
250250
251251private module NullnessConfig implements ControlFlowReachability:: ConfigSig {
252- predicate source ( ControlFlowNode node , SsaVariable def ) { varMaybeNull ( def , node , _, _) }
252+ predicate source ( ControlFlowNode node , SsaDefinition def ) { varMaybeNull ( def , node , _, _) }
253253
254- predicate sink ( ControlFlowNode node , SsaVariable def ) { varDereference ( def , _) = node }
254+ predicate sink ( ControlFlowNode node , SsaDefinition def ) { varDereference ( def , _) = node }
255255
256256 predicate barrierValue ( GuardValue gv ) { gv .isNullness ( false ) }
257257
@@ -266,7 +266,7 @@ private module NullnessFlow = ControlFlowReachability::Flow<NullnessConfig>;
266266 * Holds if the dereference of `v` at `va` might be `null`.
267267 */
268268predicate nullDeref ( SsaSourceVariable v , VarAccess va , string msg , Expr reason ) {
269- exists ( SsaVariable origin , SsaVariable ssa , ControlFlowNode src , ControlFlowNode sink |
269+ exists ( SsaDefinition origin , SsaDefinition ssa , ControlFlowNode src , ControlFlowNode sink |
270270 varMaybeNull ( origin , src , msg , reason ) and
271271 NullnessFlow:: flow ( src , origin , sink , ssa ) and
272272 ssa .getSourceVariable ( ) = v and
@@ -278,9 +278,9 @@ predicate nullDeref(SsaSourceVariable v, VarAccess va, string msg, Expr reason)
278278 * A dereference of a variable that is always `null`.
279279 */
280280predicate alwaysNullDeref ( SsaSourceVariable v , VarAccess va ) {
281- exists ( BasicBlock bb , SsaVariable ssa |
282- forall ( SsaVariable def | def = ssa .getAnUltimateDefinition ( ) |
283- def .( SsaExplicitUpdate ) . getDefiningExpr ( ) . ( VariableAssign ) . getSource ( ) = alwaysNullExpr ( )
281+ exists ( BasicBlock bb , SsaDefinition ssa |
282+ forall ( SsaDefinition def | def = ssa .getAnUltimateDefinition ( ) |
283+ def .( SsaExplicitWrite ) . getValue ( ) = alwaysNullExpr ( )
284284 )
285285 or
286286 nullGuardControls ( ssa , true , bb ) and
0 commit comments