to represent an abstract object created at an allocation site i if it is an instance of a known class t and o!of (an unknown class type)otherwise.For a Method metaobject,we write m if it is a member in a known class t and my otherwise, with its signature being s.In particular,we write m as a shorthand for m when s is unknown (with the return type s.t,being ignored),i.e.,when s.nm s.p =u. class type teT Class metaobject ct,c"E CO method name nm∈N Method metaobject*mg,mi,g,:∈M0=个×Sm parameter types pE P TO UTI UT2... method signature*seSm=个×N×企 method m∈M=TXT×N×P return type* 8.tr∈T local variable c.m∈y method name* s.nm∈A abstract heap object of,o5,,oi,o,…∈parameter types*s-p∈p Fig.4.Notations (=Xfu),where u is an unknown class type or an unknown method signature).A superscript *marks a domain that contains u. 3.4 The SOLAR's Inference System We present the inference rules used by all the components in Fig.3,starting with the pointer analysis and moving to the five components of SoLAR. 3.4.1 Pointer Analysis Fig.5 gives a standard formulation of a flow-insensitive Andersen's pointer analysis for REFJAVA.pt(r)represents the points-to set of a pointer z.An array object is analyzed with its elements collapsed to a single field,denoted arr.For example,x[i]y can be seen as x.arr y.In [A-NEw), of uniquely identifies the abstract object created as an instance of t at this allocation site,labeled by i.In [A-LD]and [A-sr],the field accesses are handled. 9N时0阿o时2国ks x=y {oi}∈pt(x) x=y.m(argi:....argn)of E pt(y)m'=dispatch(of,m) o)Ept(m))pt(me)9t)V1≤k≤：p(args)EpmA-Cu叫 Fig.5.Rules for Pointer Analysis. In [A-CALL](for non-reflective calls),the function dispatch(o;,m)is used to resolve the virtual dispatch of method m on the receiver object of to be m'(when m is invokable on of).Following [24],we assume that m'has a formal parameter mthis for the receiver object and mpl,...,mpn for the remaining parameters, and a pseudo-variable met is used to hold the return value of m'. 3.4.2 Propagation Fig.6 gives the rules for forName()and getMethod() calls.Depending on whether their arguments are string constants or not,differ- ent kinds of Class and Method metaobjects are created.SC is a set of string constants and toClass returns a Class metaobject c,where t is the class speci- fied by the string value returned by val(o;)(with val:H-java.lang.String). By design,ct and m will flow to Target Search but all the others,i.e.,c",m" and m will fow to Inference,where the missing information is inferred.During Propagation,only the name of a method signature s (i.e.,s.nm)can be discovered but its other parts are unknown:s.t=s.p u.to represent an abstract object created at an allocation site i if it is an instance of a known class t and o u i of (an unknown class type) otherwise. For a Method metaobject, we write m t s if it is a member in a known class t and m u s otherwise, with its signature being s. In particular, we write mu as a shorthand for ms when s is unknown (with the return type s.tr being ignored), i.e., when s.nm “ s.p “ u. class type t P T Class metaobject c t , c u P CO method name nm P N Method metaobject* m t s , m t u, m u s , m u u P MO = Tp ˆ Sm parameter types p P P “ T 0 Y T 1 Y T 2 . . . method signature* s P Sm = Tp ˆ Np ˆ Pp method m P M “ T ˆ T ˆ N ˆ P return type* s.tr P Tp local variable c, m P V method name* s.nm P Np abstract heap object o t 1 , ot 2 , . . . , ou 1 , ou 2 , ¨ ¨ ¨ P H parameter types* s.p P Pp Fig. 4. Notations (Xp “ X Y tuu, where u is an unknown class type or an unknown method signature). A superscript ‘*’ marks a domain that contains u. 3.4 The Solar’s Inference System We present the inference rules used by all the components in Fig. 3, starting with the pointer analysis and moving to the five components of Solar. 3.4.1 Pointer Analysis Fig. 5 gives a standard formulation of a flow-insensitive Andersen’s pointer analysis for RefJava. pt(x) represents the points-to set of a pointer x. An array object is analyzed with its elements collapsed to a single field, denoted arr. For example, x[i] = y can be seen as x.arr = y. In [A-New], o t i uniquely identifies the abstract object created as an instance of t at this allocation site, labeled by i. In [A-Ld] and [A-St], the field accesses are handled. i : x “ new tpq to t i u P ptpxq [A-New] x “ y ptpyq Ď ptpxq [A-Cpy] x “ y.f o t i P pt(y) ptpo t i .fq Ď pt(x) [A-Ld] x.f “ y o t i P pt(x) pt(y) Ď ptpo t i .fq [A-St] x “ y.mparg1 , ..., argnq oi P pt(y) m1 “ dispatchpoi , mq toi u Ď ptpm1 this) ptpm1 ret) Ď pt(x) @ 1 ď k ď n : ptpargkq Ď ptpm1 pk) [A-Call] Fig. 5. Rules for Pointer Analysis. In [A-Call] (for non-reflective calls), the function dispatchpoi , mq is used to resolve the virtual dispatch of method m on the receiver object oi to be m1 (when m is invokable on oi ). Following [24], we assume that m1 has a formal parameter m1 this for the receiver object and m1 p1 , . . . , m1 pn for the remaining parameters, and a pseudo-variable m1 ret is used to hold the return value of m1 . 3.4.2 Propagation Fig. 6 gives the rules for forName() and getMethod() calls. Depending on whether their arguments are string constants or not, differ￾ent kinds of Class and Method metaobjects are created. SC is a set of string constants and toClass returns a Class metaobject c t , where t is the class speci- fied by the string value returned by val(oi) (with val : H Ñ java.lang.String). By design, c t and m t s will flow to Target Search but all the others, i.e., c u , m u and mu will flow to Inference, where the missing information is inferred. During Propagation, only the name of a method signature s (i.e., s.nm) can be discovered but its other parts are unknown: s.tr “ s.p “ u