@@ -190,30 +190,40 @@ private Type elementType(RefType t) {
190190 )
191191}
192192
193+ private predicate upcastEnhancedForStmtAux ( BaseSsaUpdate v , RefType t , RefType t1 , RefType t2 ) {
194+ exists ( EnhancedForStmt for |
195+ for .getVariable ( ) = v .getDefiningExpr ( ) and
196+ v .getSourceVariable ( ) .getType ( ) .getErasure ( ) = t2 and
197+ t = boxIfNeeded ( elementType ( for .getExpr ( ) .getType ( ) ) ) and
198+ t .getErasure ( ) = t1
199+ )
200+ }
201+
193202/**
194203 * Holds if `v` is the iteration variable of an enhanced for statement, `t` is
195204 * the type of the elements being iterated over, and this type is more precise
196205 * than the type of `v`.
197206 */
198207private predicate upcastEnhancedForStmt ( BaseSsaUpdate v , RefType t ) {
199- exists ( EnhancedForStmt for , RefType t1 , RefType t2 |
200- for .getVariable ( ) = v .getDefiningExpr ( ) and
201- v .getSourceVariable ( ) .getType ( ) .getErasure ( ) = t2 and
202- t = boxIfNeeded ( elementType ( for .getExpr ( ) .getType ( ) ) ) and
203- t .getErasure ( ) = t1 and
208+ exists ( RefType t1 , RefType t2 |
209+ upcastEnhancedForStmtAux ( v , t , t1 , t2 ) and
204210 t1 .getASourceSupertype + ( ) = t2
205211 )
206212}
207213
214+ private predicate downcastSuccessorAux ( CastExpr cast , BaseSsaVariable v , RefType t , RefType t1 , RefType t2 ) {
215+ cast .getExpr ( ) = v .getAUse ( ) and
216+ t = cast .getType ( ) and
217+ t1 = t .getErasure ( ) and
218+ t2 = v .getSourceVariable ( ) .getType ( ) .getErasure ( )
219+ }
220+
208221/**
209222 * Holds if `va` is an access to a value that has previously been downcast to `t`.
210223 */
211224private predicate downcastSuccessor ( VarAccess va , RefType t ) {
212225 exists ( CastExpr cast , BaseSsaVariable v , RefType t1 , RefType t2 |
213- cast .getExpr ( ) = v .getAUse ( ) and
214- t = cast .getType ( ) and
215- t1 = t .getErasure ( ) and
216- t2 = v .getSourceVariable ( ) .getType ( ) .getErasure ( ) and
226+ downcastSuccessorAux ( cast , v , t , t1 , t2 ) and
217227 t1 .getASourceSupertype + ( ) = t2 and
218228 va = v .getAUse ( ) and
219229 dominates ( cast , va ) and
0 commit comments