earlier.SOLAR can infer the classes t where this method is declared by [I-INvS2T). Finally,SOLAR will add all inferred Method objects m to pt(m)at the call site. 3.4.4 Target Search For a Method object m in a known class t(with s being possibly u),we define MTD:MO-P(M)to find all target methods matched: MTD(m)=mtdLookUp(t',s.tr,s.nm;s.p) (1) t<:t' where mtdLookUp is the standard lookup function for finding the methods ac- cording to a declaring class t'and a signature s except that (1)the return type s.tr is also considered and(2)any u that appears in s is treated as a wild card. 3.4.5 Transformation Fig.8 gives the rules used for transforming a reflective call into a regular statement,which will be analyzed by the pointer analysis. x=m.invoke(y,args)m E pt(m)m'E MTD(m')oE pt(args) of E pt(of.arr)t"is declaring type of mpk k[1.n]t'<:t" [T-INV] of C pt(argk)x =y.m'(arg1:...,argn) Fig.8.Rules for Transformation. Let us examine [T-INv]in more detail.The second argument args points to a 1- D array of type Object []with its elements collapsed to a single field arr during the pointer analysis,unless args can be analyzed exactly intraprocedurally in our current implementation.Let argi,...,argn be the n freshly created arguments to be passed to each potential target method m'found by Target Search.Let mpi,...,mo be the n parameters (excluding this)of m',such that the declaring type of mk is t".We include o to pt(argk)only when holds in order to filter out the objects that cannot be assigned to mk Finally,the regular call obtained can be analyzed by [A-CALL]in Fig.5. 3.4.6 Lazy Heap Modeling Fig.9 gives the rules for resolving newInstance() lazily.In [L-KWTel,for each Class object ct pointed to by c',an object,of,is created as an instance of this known type at allocation site i straightaway.In IL-UKWTP),as illustrated with Fig.1,o is created to enable LHM if c'points to a cu instead.Then its lazy object creation happens at a type cast by applying [L-CAsr)(with o"blocked from flowing from x to a)and an invoke()call site by applying [L-INv).Note that A is assumed not to be Object in [L-CAsr]. i:v=.newInstance(cept()LKwTr i:v=d.newinstance(cept(c)UKWT {oi}∈pt(v) {or}∈pt(v) Aa=(A)x opt(）te:AL-CAST]=m.incoke(）oiept(y)∈ptm）t《:tL-liW {oi}∈pt(a) (o =pt(y) Fig.9.Rules for Lazy Heap Modeling. 3.5 Soundness Criterion REFJAVA consists of the four methods from the Java reflection API as shown in Fig.1.SoLAR is sound if their calls are resolved soundly under Assumptions 1 -4.By construction,calls to Class.forName()and getMethod()are alwaysearlier. Solar can infer the classes t where this method is declared by [I-InvS2T]. Finally, Solar will add all inferred Method objects m t s to ptpmq at the call site. 3.4.4 Target Search For a Method object m t s in a known class t (with s being possibly u), we define MT D : MO Ñ PpMq to find all target methods matched: MT Dpm t sq “ ď tă:t 1 mtdLookU ppt 1 , s.tr, s.nm, s.pq (1) where mtdLookU p is the standard lookup function for finding the methods ac￾cording to a declaring class t 1 and a signature s except that (1) the return type s.tr is also considered and (2) any u that appears in s is treated as a wild card. 3.4.5 Transformation Fig. 8 gives the rules used for transforming a reflective call into a regular statement, which will be analyzed by the pointer analysis. x “ m.invoke(y, args) m t P pt(m) m1 P MTDpm t q oi P pt(args) o t 1 j P ptpoi .arrq t 2 is declaring type of m1 pk k P r1, ns t 1 ă: t 2 to t 1 j u Ď ptpargkq x “ y.m1 parg1 , ..., argnq [T-Inv] Fig. 8. Rules for Transformation. Let us examine [T-Inv] in more detail. The second argument args points to a 1- D array of type Object[], with its elements collapsed to a single field arr during the pointer analysis, unless args can be analyzed exactly intraprocedurally in our current implementation. Let arg1,. . . , argn be the n freshly created arguments to be passed to each potential target method m1 found by Target Search. Let m1 p1 , . . . , m1 pn be the n parameters (excluding this) of m1 , such that the declaring type of m1 pk is t 2 . We include o t 1 j to ptpargk q only when t 1 ă: t 2 holds in order to filter out the objects that cannot be assigned to m1 pk. Finally, the regular call obtained can be analyzed by [A-Call] in Fig. 5. 3.4.6 Lazy Heap Modeling Fig. 9 gives the rules for resolving newInstance() lazily. In [L-KwTp], for each Class object c t pointed to by c 1 , an object, o t i , is created as an instance of this known type at allocation site i straightaway. In [L-UkwTp], as illustrated with Fig. 1, o u i is created to enable LHM if c 1 points to a c u instead. Then its lazy object creation happens at a type cast by applying [L-Cast] (with o u i blocked from flowing from x to a) and an invoke() call site by applying [L-Inv]. Note that A is assumed not to be Object in [L-Cast]. i : v “ c 1 .newInstancepq c t P pt(c1 ) to t i u Ď pt(v) [L-KwTp] i : v “ c 1 .newInstancepq c u P pt(c1 ) to u i u Ď pt(v) [L-UkwTp] A a “ pAq x o u i P pt(x) t ă: A to t i u Ď ptpaq [L-Cast] x “ m.invokepy, ...q o u i P pt(y) m t P pt(m) t 1 !: t to t 1 i u Ď pt(y) [L-Inv] Fig. 9. Rules for Lazy Heap Modeling. 3.5 Soundness Criterion RefJava consists of the four methods from the Java reflection API as shown in Fig. 1. Solar is sound if their calls are resolved soundly under Assumptions 1 – 4. By construction, calls to Class.forName() and getMethod() are always