3 Formalism We formalise SOLAR,illustrated in Fig.2,for REFJAVA,which is Java restricted to a small core of its reflection API.SOLAR is flow-insensitive but context- sensitive.However.our formalisation is context-insensitive. 3.1 The REFJAVA Language REFJAVA consists of all Java programs(under Assumptions 1-4)except that the Java reflection API is restricted to the four methods in Fig.1:Class.forName(), newInstance(),getMethod()and invoke().Our formalism is designed to allow its straightforward generalization to the entire API.For example,reflective field accesses via getField(),get()and set()can be handled similarly.As is stan- dard,a Java program is represented only by five kinds of statements in the SSA form,as shown in Fig.5.For simplicity,we assume that all the methods of a class accessed reflectively are its instance members,i.e.,v null in invoke(v,...) in Fig.1.We will discuss how to handle static members in Section 3.9. 3.2 Road Map Inference As depicted in Fig.3,SOLAR's in- ference system,which consists of five components,works together with a pointer analysis..The arrow←→be tween a component and the pointer analysis indicates that each is both a producer and consumer of the other. Fig.3.SOLAR's inference system. Let us see how SOLAR resolves the invoke()call in Fig.1.If cName2 and mName2 are string constants,Propagation will create a Method metaobject(pointed to by m)carrying its known class and method information and pass it to Target Search (1).If cName2 or mName2 is not a constant,a Method metaobject marked as such is created and passed to Inference(2),which will infer the missing information and pass a freshly gener- ated Method metaobject enriched with the missing information to Target Search (3).Then Target Search maps a Method metaobject to its reflective target mtd in its declaring class().Finally,Transformation turns the reflective call in line 15 into a regular call v.mtd(...)and pass it to the pointer analysis (5).Lazy Heap Modeling handles newInstance()in Fig.1 to resolve the dynamic type of v based on the information discovered by Propagation (@)or Inference (b). 3.3 Notations We will use the notations in Fig.4.A method signature consists of the method name and descriptor (i.e.,return type and parameter types)and,a method is specified by its method signature and the class where it is declared or inherited. CO and MO represent the set of Class and Method metaobjects,respectively. In particular,ct denotes a Class metaobject of a known class t and c"a Class metaobject of an unknown class u.As illustrated earlier with Fig.1,we write of3 Formalism We formalise Solar, illustrated in Fig. 2, for RefJava, which is Java restricted to a small core of its reflection API. Solar is flow-insensitive but context￾sensitive. However, our formalisation is context-insensitive. 3.1 The RefJava Language RefJava consists of all Java programs (under Assumptions 1 – 4) except that the Java reflection API is restricted to the four methods in Fig. 1: Class.forName(), newInstance(), getMethod() and invoke(). Our formalism is designed to allow its straightforward generalization to the entire API. For example, reflective field accesses via getField(), get() and set() can be handled similarly. As is stan￾dard, a Java program is represented only by five kinds of statements in the SSA form, as shown in Fig. 5. For simplicity, we assume that all the methods of a class accessed reflectively are its instance members, i.e., v ‰ null in invoke(v,...) in Fig. 1. We will discuss how to handle static members in Section 3.9. 3.2 Road Map Inference Transformation Pointer Analysis Propagation Lazy Heap Modeling Target Search 1 4 3 2 a 5 b Fig. 3. Solar’s inference system. As depicted in Fig. 3, Solar’s in￾ference system, which consists of five components, works together with a pointer analysis. The arrow ÐÑ be￾tween a component and the pointer analysis indicates that each is both a producer and consumer of the other. Let us see how Solar resolves the invoke() call in Fig. 1. If cName2 and mName2 are string constants, Propagation will create a Method metaobject (pointed to by m) carrying its known class and method information and pass it to Target Search ( 1 ). If cName2 or mName2 is not a constant, a Method metaobject marked as such is created and passed to Inference ( 2 ), which will infer the missing information and pass a freshly gener￾ated Method metaobject enriched with the missing information to Target Search ( 3 ). Then Target Search maps a Method metaobject to its reflective target mtd in its declaring class ( 4 ). Finally, Transformation turns the reflective call in line 15 into a regular call v.mtd(...) and pass it to the pointer analysis ( 5 ). Lazy Heap Modeling handles newInstance() in Fig. 1 to resolve the dynamic type of v based on the information discovered by Propagation ( a ) orInference ( b ). 3.3 Notations We will use the notations in Fig. 4. A method signature consists of the method name and descriptor (i.e., return type and parameter types) and, a method is specified by its method signature and the class where it is declared or inherited. CO and MO represent the set of Class and Method metaobjects, respectively. In particular, c t denotes a Class metaobject of a known class t and c u a Class metaobject of an unknown class u. As illustrated earlier with Fig. 1, we write o t i