soundly resolved(with the metaobjects created being modelled appropriately). Due to Assumption 4,there is no need to consider newInstance()calls since they are soundly resolved if all invoke()calls are.For convenience,we define: AllKwn(v)=o∈pt(o) (2) which means that the dynamic type of every object pointed to by v is known. Consider Fig.7.For the Method metaobjects m with known classes t,these targets can be soundly resolved by Target Search,except that the signatures s can be further refined by applying [-Ixvsic).For the Method objects m"with unknown class types u,the targets accessed are inferred by [I-INVTrl and [-INvS2T). Let us consider a call to (A)m.invoke(y,args).SOLAR attempts to infer the missing classes of its Method metaobjects in two ways,by applying [I-INVTr]and UI-INVS2T].Such a call is soundly resolved if the following condition holds: SC(m.invoke(y,args)=AllKwn(y)vHm#∈pt(m):s.nm≠u Ptp(args)≠②(3) If the first disjunct holds,applying [-INVTP]to invoke()can over-approximate its target methods from the types of all objects pointed to by y.Thus,every Method metaobject m4 E pt(m)is refined into a new one m for every of e pt(y). If the second disjunct holds,then [-Ixvs2T]comes into play.Its targets are over-approximated based on the known method names s.nm and the types of the objects pointed to by args.Thus,every Method metaobject mE pt(m)is refined into a new one m,where s.tr<:A and s.pe Ptp(args).Note that s.t,is leveraged only when it is not u.The post-dominating cast (A)is considered not to exist if A Object.In this case,u Object holds (only for u). Theorem 1.SOLAR is sound for REFJAVA if SC(c)holds at every reflective call c of the form "(A)m.invoke(y,args)"under Assumptions 1-4. 3.6 Identifying Unsoundly Resolved Reflective Calls SOLAR flags a call c to invoke()as resolved unsoundly if SC(c)is false.This can be conservative as some points-to information at c can be over-approximate. However,our evaluation shows that SoLAR can analyze 7 out of the 10 large programs considered scalably with full automation,implying that its inference system is powerful and precise.In addition,all 13 unsound calls reported by SOLAR in the remaining three programs are truly unsound,as discussed in Sec- tion 4.4,validating SOLAR's effectiveness in identifying unsoundness. 3.7 Identifying Imprecisely Resolved Reflective Calls Presently,SoLAR performs this task depicted in Fig.2,by simply ranking the reflective call sites according to the number of reflective targets inferred.This simple metric often gives a good indication about the sources of imprecision. 3.8 PROBE For evaluation purposes,we instantiate PROBE,as shown in Fig.2,from SOLAR as follows.We refrain from performing SOLAR's LHM(by retaining [L-UKWTe)butsoundly resolved (with the metaobjects created being modelled appropriately). Due to Assumption 4, there is no need to consider newInstance() calls since they are soundly resolved if all invoke() calls are. For convenience, we define: AllKwnpvq “ E o u i P ptpvq (2) which means that the dynamic type of every object pointed to by v is known. Consider Fig. 7. For the Method metaobjects m t s with known classes t, these targets can be soundly resolved by Target Search, except that the signatures s can be further refined by applying [I-InvSig]. For the Method objects m u s with unknown class types u, the targets accessed are inferred by [I-InvTp] and [I-InvS2T]. Let us consider a call to (A) m.invoke(y, args). Solar attempts to infer the missing classes of its Method metaobjects in two ways, by applying [I-InvTp] and [I-InvS2T]. Such a call is soundly resolved if the following condition holds: SCpm.invoke(y,args)q “ AllKwnpyq_ @ m u s P ptpmq : s.nm ‰ u^P tppargsq ‰ ∅ (3) If the first disjunct holds, applying [I-InvTp] to invoke() can over-approximate its target methods from the types of all objects pointed to by y. Thus, every Method metaobject m u P ptpmq is refined into a new one m t for every o t i P ptpyq. If the second disjunct holds, then [I-InvS2T] comes into play. Its targets are over-approximated based on the known method names s.nm and the types of the objects pointed to by args. Thus, every Method metaobject m u s P ptpmq is refined into a new one m t s , where s.tr !: A and s.p P P tppargsq ‰ ∅. Note that s.tr is leveraged only when it is not u. The post-dominating cast (A) is considered not to exist if A = Object. In this case, u !: Object holds (only for u). Theorem 1. Solar is sound for RefJava if SCpcq holds at every reflective call c of the form “(A) m.invoke(y, args)” under Assumptions 1 – 4. 3.6 Identifying Unsoundly Resolved Reflective Calls Solar flags a call c to invoke() as resolved unsoundly if SCpcq is false. This can be conservative as some points-to information at c can be over-approximate. However, our evaluation shows that Solar can analyze 7 out of the 10 large programs considered scalably with full automation, implying that its inference system is powerful and precise. In addition, all 13 unsound calls reported by Solar in the remaining three programs are truly unsound, as discussed in Sec￾tion 4.4, validating Solar’s effectiveness in identifying unsoundness. 3.7 Identifying Imprecisely Resolved Reflective Calls Presently, Solar performs this task depicted in Fig. 2, by simply ranking the reflective call sites according to the number of reflective targets inferred. This simple metric often gives a good indication about the sources of imprecision. 3.8 Probe For evaluation purposes, we instantiate Probe, as shown in Fig. 2, from Solar as follows. We refrain from performing Solar’s LHM (by retaining [L-UkwTp] but