Effective Soundness-Guided Reflection Analysis Yue Li,Tian Tan,and Jingling Xue Programming Languages and Compilers Group School of Computer Science and Engineering,UNSW Australia Abstract.We introduce SOLAR.the first reflection analysis that allows its soundness to be reasoned about when some assumptions are met and produces significantly improved under-approximations otherwise.In both settings,SoLAR has three novel aspects:(1)lazy heap modeling for reflective allocation sites,(2)collective inference for improving the inferences on related reflective calls,and (3)automatic identification of "problematic"reflective calls that may threaten its soundness,precision and scalability,thereby enabling their improvement via lightweight anno- tations.We evaluate SOLAR against two state-of-the-art solutions,DooP and ELF,with the three treated as under-approximate reflection analyses, using 11 large Java benchmarks and applications.SoLAR is significantly more sound while achieving nearly the same precision and running only several-fold more slowly,subject to only 7 annotations in 3 programs. 1 Introduction Reflection is increasingly used in a range of software and framework architec- tures,allowing a software system to choose and change implementations of ser- vices at run-time,but posing significant challenges to static program analysis. In the case of Java programs,refection has always been an obstacle for pointer analysis [1-10],a fundamental static analysis on which virtually all others [11- 16]are built.All pointer analysis tools for Java [2,17-19]either ignore reflection or handle it partially since their underlying best-effort reflection analyses [5,17, 18,20-22]provide only under-approximated handling of reflection heuristically. However,such unsoundness can render much of the codebase invisible for analysis.There is a recent community initiative [23]calling for the development of soundy analysis to handle "hard"language features(such as reflection).A soundy analysis is one that is as sound as possible without excessively compro- mising precision and/or scalability.Thus,improving or even achieving soundness in reflection analysis will provide significant benefits to many clients,such as pro- gram verifiers,optimizing compilers,bug detectors and security analyzers. In this paper,we make the following contributions: We introduce SoLAR,the first reflection analysis that allows its soundness to be reasoned about when some reasonable assumptions are met and yields significantly improved under-approximations otherwise(Section 2).We have developed SoLAR by adopting three novel aspects in its design:(N1)lazy heap modeling for refective allocation sites.(N2)collective inference for
Effective Soundness-Guided Reflection Analysis Yue Li, Tian Tan, and Jingling Xue Programming Languages and Compilers Group School of Computer Science and Engineering, UNSW Australia Abstract. We introduce Solar, the first reflection analysis that allows its soundness to be reasoned about when some assumptions are met and produces significantly improved under-approximations otherwise. In both settings, Solar has three novel aspects: (1) lazy heap modeling for reflective allocation sites, (2) collective inference for improving the inferences on related reflective calls, and (3) automatic identification of “problematic” reflective calls that may threaten its soundness, precision and scalability, thereby enabling their improvement via lightweight annotations. We evaluate Solar against two state-of-the-art solutions, Doop and Elf, with the three treated as under-approximate reflection analyses, using 11 large Java benchmarks and applications. Solar is significantly more sound while achieving nearly the same precision and running only several-fold more slowly, subject to only 7 annotations in 3 programs. 1 Introduction Reflection is increasingly used in a range of software and framework architectures, allowing a software system to choose and change implementations of services at run-time, but posing significant challenges to static program analysis. In the case of Java programs, reflection has always been an obstacle for pointer analysis [1–10], a fundamental static analysis on which virtually all others [11– 16] are built. All pointer analysis tools for Java [2, 17–19] either ignore reflection or handle it partially since their underlying best-effort reflection analyses [5, 17, 18, 20–22] provide only under-approximated handling of reflection heuristically. However, such unsoundness can render much of the codebase invisible for analysis. There is a recent community initiative [23] calling for the development of soundy analysis to handle “hard” language features (such as reflection). A soundy analysis is one that is as sound as possible without excessively compromising precision and/or scalability. Thus, improving or even achieving soundness in reflection analysis will provide significant benefits to many clients, such as program verifiers, optimizing compilers, bug detectors and security analyzers. In this paper, we make the following contributions: – We introduce Solar, the first reflection analysis that allows its soundness to be reasoned about when some reasonable assumptions are met and yields significantly improved under-approximations otherwise (Section 2). We have developed Solar by adopting three novel aspects in its design: (N1) lazy heap modeling for reflective allocation sites, (N2) collective inference for
related reflective calls,and (N3)automatic identification of "problematic" reflective calls that may threaten its soundness,precision and scalability. -We formalize SoLAR as part of a pointer analysis for Java(including a small core of its reflection APl)and reason about its soundness under a set of assumptions(Section 3).We have produced an open source implementation on top of Doop [18,which is a modern pointer analysis tool for Java. We evaluate SOLAR against two state-of-the-art reflection analyses,Doop [5] and ELF [21],with 11 large Java benchmarks/applications (Section 4),where all the three are treated as under-approximate analyses(due to,e.g.,native code).By instrumenting these programs under their associated inputs(when available).SOLAR is the only one to achieve total recall(for all reflective tar- gets accessed),with 371%(148%)more target methods resolved than Doop (ELF)in total,which translates into 49700(40570)more true caller-callee re- lations statically calculated w.r.t.these inputs alone.SoLAR has done so by maintaining nearly the same precision as and running only several-fold more slowly than ELF and DooP,subject to only 7 annotations in 3 programs. 2 Methodology Fig.1 illustrates an example of reflection usage abstracted in real code.In line 2, a Class metaobject c1 is created by calling Class.forName(cName)to represent the class named cName,where cName,i.e.,cName1 in line 10 is an input string to be read from a command line or a configuration file.In line 3.an object o is refectively created as an instance of c1 by calling c1.newInstance()and then assigned to v with the declared type as Java.lang.Object in line 10. Subsequently,o is used in two common scenarios.In the if branch,o is downcast to a specific type,A,and then used appropriately.The else branch is more interesting.In line 14,a Method metaobject m is created by calling getMethod() indirectly in line 7,with its class name,method name and formal parameters specified by cName2,mName2 and "..."(elided)in line 7,respectively.In line 15, this method is called reflectively on the receiver object o(pointed to by v)with the actual argument being passed in an array,new object[]{x,y}. 1 Object createObj(String cName){ 9 void foo(xx.Yy....) Class c1=Class.forName(cName) 10 Object v=createObj(cName1)://cName1 is an input string retum c1.newinstance0: if(.)( 12 Aa=(A)v: 13 }else{ 5 Method getMtd(String cName.String mName){14 Method m=getMtd(cName2,mName2): 6 Class c2=Class.forName(cName): 5 m.invoke(v,new Object](x,y)): retum c2.getMethod(mName....) 16 8} 17} Fig.1.An example of reflection usage abstracted from JDK 1.6.0_45. A refection analysis infers,i.e..resolves statically the reflective targets ac- cessed at reflective call sites.As usual,soundnesss demands over-approximation. Reflection introduces many challenges for static analysis.First,a modern reflec- tion API is large and complex.Second,reflection is typically used as a means
related reflective calls, and (N3) automatic identification of “problematic” reflective calls that may threaten its soundness, precision and scalability. – We formalize Solar as part of a pointer analysis for Java (including a small core of its reflection API) and reason about its soundness under a set of assumptions (Section 3). We have produced an open source implementation on top of Doop [18], which is a modern pointer analysis tool for Java. – We evaluate Solar against two state-of-the-art reflection analyses, Doop [5] and Elf [21], with 11 large Java benchmarks/applications (Section 4), where all the three are treated as under-approximate analyses (due to, e.g., native code). By instrumenting these programs under their associated inputs (when available), Solar is the only one to achieve total recall (for all reflective targets accessed), with 371% (148%) more target methods resolved than Doop (Elf) in total, which translates into 49700 (40570) more true caller-callee relations statically calculated w.r.t. these inputs alone. Solar has done so by maintaining nearly the same precision as and running only several-fold more slowly than Elf and Doop, subject to only 7 annotations in 3 programs. 2 Methodology Fig. 1 illustrates an example of reflection usage abstracted in real code. In line 2, a Class metaobject c1 is created by calling Class.forName(cName) to represent the class named cName, where cName, i.e., cName1 in line 10 is an input string to be read from a command line or a configuration file. In line 3, an object o is reflectively created as an instance of c1 by calling c1.newInstance() and then assigned to v with the declared type as Java.lang.Object in line 10. Subsequently, o is used in two common scenarios. In the if branch, o is downcast to a specific type, A, and then used appropriately. The else branch is more interesting. In line 14, a Method metaobject m is created by calling getMethod() indirectly in line 7, with its class name, method name and formal parameters specified by cName2, mName2 and “. . . ” (elided) in line 7, respectively. In line 15, this method is called reflectively on the receiver object o (pointed to by v) with the actual argument being passed in an array, new Object[] {x, y}. 1 Object createObj(String cName) { 2 Class c1 = Class.forName(cName); 3 return c1.newInstance(); 4 } 5 Method getMtd(String cName, String mName) { 6 Class c2 = Class.forName(cName); 7 return c2.getMethod(mName, ... ); 8 } 9 void foo(X x, Y y, … ) { 10 Object v = createObj(cName1); //cName1 is an input string 11 if ( … ) { 12 A a = (A) v; 13 } else { 14 Method m = getMtd(cName2, mName2); 15 m.invoke(v, new Object[] {x, y}); 16 } 17 } … … Fig. 1. An example of reflection usage abstracted from JDK 1.6.0 45. A reflection analysis infers, i.e., resolves statically the reflective targets accessed at reflective call sites. As usual, soundnesss demands over-approximation. Reflection introduces many challenges for static analysis. First, a modern reflection API is large and complex. Second, reflection is typically used as a means
of supporting dynamic adaptation of object-oriented software.As such.metaob- jects are often created reflectively as shown in Fig.1 from input strings.Thus, reflective object creation via newInstance()is hard to model statically.Finally. picking judicious approximations to balance soundness,precision and scalability is non-trivial.A simple-minded sound modeling of a reflective call (e.g.,by as- suming arbitrary behaviour)would destroy precision.Imprecision,in turn,often destroys scalability because too many spurious results would be computed. SOLAR automates reflection analysis for Java by working with a pointer anal- ysis.We first define some assumptions (Section 2.1).We then look at the three limitations of the prior work (Section 2.2).Finally,we introduce SOLAR to ad- dress these limitations by adopting three novel aspects in its design(Section 2.3). 2.1 Assumptions The first three are made previously on reflection analysis for Java [20,21].The last one is introduced to allow reflective allocation sites to be modeled lazily. Assumption 1 (Closed-World).Only the classes reachable from the class path at analysis time can be used during program erecution. This assumption is reasonable since we cannot expect static analysis to han- dle all classes that a program may conceivably download from the net and load at runtime.In addition,Java native methods are excluded as well. Assumption 2 (Well-Behaved Class Loaders).The name of the class returned by a call to Class.forName(cName)equals cName. Assumption 3(Correct Casts).Type cast operations applied to the results of reflective calls are correct,without throwing a ClassCastException. Assumption 4 (Object Reachability).Every object o created reflectively in a call to newInstance()fows into (i.e.,is used in)either (1)a type cast operation ...(T)v or (2)a call to invoke(v,...),get(v)or set(v,...),where v points to o,along every execution path in the program. As discussed in Section 4.2,Assumption 4 is found to hold for most reflective allocation sites in real code(as illustrated in Fig.1).Here,(1)and(2)represent two kinds of usage points at which the class types of object o will be inferred lazily.This makes it possible to handle reflective allocation sites more accurately than before and to reason about the soundness of SoLAR for the first time. 2.2 Past Work:Best-Effort Reflection Resolution All the existing solutions [5,17,18,20-22]adopt a best-effort approach to reflec- tion analysis,and consequently,suffer from the following three limitations: L1.Eager Heap Modeling An abstract object o created at a call to,e.g., c.newInstance()is modeled eagerly if its type c can be inferred from a string constant or intraprocedural post-dominant cast,and ignored otherwise.Specifi- cally,.if c represents a known class name,e.g,“A”,then o's type is“A”.Other- wise,an intraprocedurally post-dominating cast operation (T)operating on the result of the newInstance()call will allow c to be over-approximated as T or any of its subtypes.This eager approach often fails in real code shown in Fig.1, where cNamel is an input string and the cast is not post-dominating.Thus,its
of supporting dynamic adaptation of object-oriented software. As such, metaobjects are often created reflectively as shown in Fig. 1 from input strings. Thus, reflective object creation via newInstance() is hard to model statically. Finally, picking judicious approximations to balance soundness, precision and scalability is non-trivial. A simple-minded sound modeling of a reflective call (e.g., by assuming arbitrary behaviour) would destroy precision. Imprecision, in turn, often destroys scalability because too many spurious results would be computed. Solar automates reflection analysis for Java by working with a pointer analysis. We first define some assumptions (Section 2.1). We then look at the three limitations of the prior work (Section 2.2). Finally, we introduce Solar to address these limitations by adopting three novel aspects in its design (Section 2.3). 2.1 Assumptions The first three are made previously on reflection analysis for Java [20, 21]. The last one is introduced to allow reflective allocation sites to be modeled lazily. Assumption 1 (Closed-World). Only the classes reachable from the class path at analysis time can be used during program execution. This assumption is reasonable since we cannot expect static analysis to handle all classes that a program may conceivably download from the net and load at runtime. In addition, Java native methods are excluded as well. Assumption 2 (Well-Behaved Class Loaders). The name of the class returned by a call to Class.forName(cName) equals cName. Assumption 3 (Correct Casts). Type cast operations applied to the results of reflective calls are correct, without throwing a ClassCastException. Assumption 4 (Object Reachability). Every object o created reflectively in a call to newInstance() flows into (i.e., is used in) either (1) a type cast operation ...= (T) v or (2) a call to invoke(v,...), get(v) or set(v,...), where v points to o, along every execution path in the program. As discussed in Section 4.2, Assumption 4 is found to hold for most reflective allocation sites in real code (as illustrated in Fig. 1). Here, (1) and (2) represent two kinds of usage points at which the class types of object o will be inferred lazily. This makes it possible to handle reflective allocation sites more accurately than before and to reason about the soundness of Solar for the first time. 2.2 Past Work: Best-Effort Reflection Resolution All the existing solutions [5, 17, 18, 20–22] adopt a best-effort approach to reflection analysis, and consequently, suffer from the following three limitations: L1. Eager Heap Modeling An abstract object o created at a call to, e.g., c.newInstance() is modeled eagerly if its type c can be inferred from a string constant or intraprocedural post-dominant cast, and ignored otherwise. Specifi- cally, if c represents a known class name, e.g., “A”, then o’s type is “A”. Otherwise, an intraprocedurally post-dominating cast operation (T) operating on the result of the newInstance() call will allow c to be over-approximated as T or any of its subtypes. This eager approach often fails in real code shown in Fig. 1, where cName1 is an input string and the cast is not post-dominating. Thus, its
newInstance()call is ignored.Recently.in DoOP (r5459247-beta)18,the ob- jects created in line 10(or line 3)are assumed to be of type A by taking advantage of the non-post-dominating cast (A)in line 12 to analyze more code.However, the objects with other types created along both the if and else branches are ignored.In prior work,such under-approximate handling of newInstance()is a significant source of unsoundness,as a large part of the program called on the thus ignored objects has been rendered invisible for analysis. L2.Isolated Inferences Many reflective calls(e.g.,those in Fig.1)are related but analysed mostly in isolation,resulting in under-approximated behaviours.In [21],we presented a self-inferencing reflection analysis,called ELF,that can infer more targets at a reflective call site than before [5,17,18,20,22],by exploiting more information available(e.g.,from its arguments and return type).However, due to eager heap modeling,ELF will still ignore the invoke()call in line 15 as v points to objects of unknown types as discussed above. L3.Design-Time Soundness,Precision and Scalability When analysing a program heuristically,a best-effort approach does not know which reflective calls may potentially affect its soundness,precision and scalability.As a result, a developer is out of luck with a program if such best-effort analysis is either unscalable or scalable but with undesired soundness or precision or both. 2.3 SOLAR:Soundness-Guided Reflection Resolution Fig.2 illustrates the SoLAR design,with its three novel aspects marked by N1 -N3,where Ni is introduced to overcome the afore-mentioned limitation Li. Jave Scalable Satisfied Programs N1 Lazy Heap Modeling Prover N2 Collective inference Urscalable PROBE Lightweight Arnotations impreicse Unsound Reflective Cals Fig.2.SOLAR:a soundness-guided analysis with three novel aspects,N1-N3. N1.Lazy Heap Modeling (LHM)SOLAR handles reflective object creation lazily by delaying the creation of objects at their usage points where their types may be inferred,achieving significantly improved soundness and precision. Let us describe the basic idea behind using the example in Fig.1.As cName at c1 Class.forName(cName)in line 2 is unknown,SOLAR will create a Class metaobject ciu that represents this unknown class and assign it to c1.As ci points to c1"at the allocation site v=c1.newInstance()in line 3,SOLAR will create an abstract object o of an unknown type for the site to mark it as being unresolved yet.Subsequently,o will flow into two usage points:Case(I)a type cast operation in line 12 and Case (II)a reflective method call site in line 15. In Case (I),where o is downcast to A,its type u is inferred to be A or any of its subtypes.Let t1,...,tn be all the inferred types.Then o is split into n
newInstance() call is ignored. Recently, in Doop (r5459247-beta) [18], the objects created in line 10 (or line 3) are assumed to be of type A by taking advantage of the non-post-dominating cast (A) in line 12 to analyze more code. However, the objects with other types created along both the if and else branches are ignored. In prior work, such under-approximate handling of newInstance() is a significant source of unsoundness, as a large part of the program called on the thus ignored objects has been rendered invisible for analysis. L2. Isolated Inferences Many reflective calls (e.g., those in Fig. 1) are related but analysed mostly in isolation, resulting in under-approximated behaviours. In [21], we presented a self-inferencing reflection analysis, called Elf, that can infer more targets at a reflective call site than before [5, 17, 18, 20, 22], by exploiting more information available (e.g., from its arguments and return type). However, due to eager heap modeling, Elf will still ignore the invoke() call in line 15 as v points to objects of unknown types as discussed above. L3. Design-Time Soundness, Precision and Scalability When analysing a program heuristically, a best-effort approach does not know which reflective calls may potentially affect its soundness, precision and scalability. As a result, a developer is out of luck with a program if such best-effort analysis is either unscalable or scalable but with undesired soundness or precision or both. 2.3 Solar: Soundness-Guided Reflection Resolution Fig. 2 illustrates the Solar design, with its three novel aspects marked by N1 – N3, where Ni is introduced to overcome the afore-mentioned limitation Li. Scalable Unscalable Satisfied Soundness Proven Java Programs Violated Impreicse Unsound N1 Lazy Heap Modelling Soundness Criteria Imprecision Criteria ( by Customized Thresholds ) PROBE Reflective Calls Lightweight Annotations Automatic Identification of Problematic Reflective Calls N2 Collective Inference N3 Fig. 2. Solar: a soundness-guided analysis with three novel aspects, N1 – N3. N1. Lazy Heap Modeling (LHM) Solar handles reflective object creation lazily by delaying the creation of objects at their usage points where their types may be inferred, achieving significantly improved soundness and precision. Let us describe the basic idea behind using the example in Fig. 1. As cName at c1 = Class.forName(cName) in line 2 is unknown, Solar will create a Class metaobject c1u that represents this unknown class and assign it to c1. As c1 points to c1u at the allocation site v = c1.newInstance() in line 3, Solar will create an abstract object o u 3 of an unknown type for the site to mark it as being unresolved yet. Subsequently, o u 3 will flow into two usage points: Case (I) a type cast operation in line 12 and Case (II) a reflective method call site in line 15. In Case (I), where o u 3 is downcast to A, its type u is inferred to be A or any of its subtypes. Let t1, . . . , tn be all the inferred types. Then o u 3 is split into n
distinct objects o3,...,o"to be assigned to a in line 12.In Case (II),SOLAR will infer u by performing a collective inference as described below,based on the information available in line 15.Let t,...,tm be all the inferred types.Then og is split into m distinct objectsoto be assigned to v in line 15. According to Assumption 4 that states a key observation validated later,a reflectively created object like o is typically used in either Case(I)or Case(II) along every program path.The only but rare exception is that o is created but never used later.Then the corresponding constructor must be annotated to be analyzed statically unless ignoring it will not affect the points-to information. N2.Collective Inference SoLAR builds on the prior work [5,17,18,20,22,21] by relying on collective inference emphasized for the first time in reflection anal- ysis.Let us return to the invoke()call,which cannot be analyzed previously. As v points to o,SoLAR can infer u based on the information available at the call site.This happens when Case (1)cName2 is known or Case(2)cName2 is unknown but mName2 is known.In SOLAR,inference is performed "collectively" whereby inferences on related reflective calls(lines 3,6 and 15 for Case(1)and lines 3.7 and 15 for Case(2))can mutually reinforce each other.We will examine the second case,i.e.,the more complex of the two,in Section 3.4.3.This paper is the first to do so by exploiting the connection between newInstance()(via LHM)and reflective calls for manipulating methods and fields. N3.Automatic Identification of "Problematic"Reflective Calls Due to this capability,SoLAR is the first that can reason about its soundness.When such reasoning is not possible due to,e.g.,native code,SoLAR reduces to an effective under-approximate analysis due to its soundness-guided design,allowing a disciplined tradeoff to be made among soundness,precision and scalability. If SOLAR is scalable for a program,SoLAR can automatically identify "prob- lematic"reflective calls (as opposed to reporting input strings as in [20])that may threaten its soundness and precision to enable both to be improved with lightweight annotations.If SoLAR is unscalable for a program,a simplified ver- sion of SOLAR,denoted PROBE in Fig.2,is called for next.With some "prob- lematic"reflective calls to be annotated,SoLAR will re-analyze the program, scalably after one or more iterations of this "probing"process.We envisage providing a range of PROBE variants with different tradeoffs among soundness, precision and scalability,so that the scalability of PROBE is always guaranteed. Consider Fig.1 again.If both cName2 and mName2 are unknown (given that the type of o is unknown),then SoLAR will flag the invoke()call in line 15 as being potentially unsoundly resolved,detected automatically by verifying Condition(3)in Section 3.5.In addition,SoLAR will also automatically highlight reflective calls that may be potentially imprecisely resolved.Their lightweight annotations will allow SoLAR to yield improved soundness and precision. Discussion Under Assumptions 1-4,we can establish the soundness of So- LAR by verifying a soundness criterion (given in Section 3.5).Otherwise,our soundness-guided approach has made SoLAR demonstrably more effective than existing under-approximate reflection analyses [5,17,20,21]as validated later
distinct objects o t1 3 ,. . . , o tn 3 to be assigned to a in line 12. In Case (II), Solar will infer u by performing a collective inference as described below, based on the information available in line 15. Let t 1 1 , . . . , t1 m be all the inferred types. Then o u 3 is split into m distinct objects o t 1 1 3 ,. . . , o t 1 m 3 to be assigned to v in line 15. According to Assumption 4 that states a key observation validated later, a reflectively created object like o u 3 is typically used in either Case (I) or Case (II) along every program path. The only but rare exception is that o u 3 is created but never used later. Then the corresponding constructor must be annotated to be analyzed statically unless ignoring it will not affect the points-to information. N2. Collective Inference Solar builds on the prior work [5, 17, 18, 20, 22, 21] by relying on collective inference emphasized for the first time in reflection analysis. Let us return to the invoke() call, which cannot be analyzed previously. As v points to o u 3 , Solar can infer u based on the information available at the call site. This happens when Case (1) cName2 is known or Case (2) cName2 is unknown but mName2 is known. In Solar, inference is performed “collectively”, whereby inferences on related reflective calls (lines 3, 6 and 15 for Case (1) and lines 3, 7 and 15 for Case (2)) can mutually reinforce each other. We will examine the second case, i.e., the more complex of the two, in Section 3.4.3. This paper is the first to do so by exploiting the connection between newInstance() (via LHM) and reflective calls for manipulating methods and fields. N3. Automatic Identification of “Problematic” Reflective Calls Due to this capability, Solar is the first that can reason about its soundness. When such reasoning is not possible due to, e.g., native code, Solar reduces to an effective under-approximate analysis due to its soundness-guided design, allowing a disciplined tradeoff to be made among soundness, precision and scalability. If Solar is scalable for a program, Solar can automatically identify “problematic” reflective calls (as opposed to reporting input strings as in [20]) that may threaten its soundness and precision to enable both to be improved with lightweight annotations. If Solar is unscalable for a program, a simplified version of Solar, denoted Probe in Fig. 2, is called for next. With some “problematic” reflective calls to be annotated, Solar will re-analyze the program, scalably after one or more iterations of this “probing” process. We envisage providing a range of Probe variants with different tradeoffs among soundness, precision and scalability, so that the scalability of Probe is always guaranteed. Consider Fig. 1 again. If both cName2 and mName2 are unknown (given that the type of o u 3 is unknown), then Solar will flag the invoke() call in line 15 as being potentially unsoundly resolved, detected automatically by verifying Condition (3) in Section 3.5. In addition, Solar will also automatically highlight reflective calls that may be potentially imprecisely resolved. Their lightweight annotations will allow Solar to yield improved soundness and precision. Discussion Under Assumptions 1 – 4, we can establish the soundness of Solar by verifying a soundness criterion (given in Section 3.5). Otherwise, our soundness-guided approach has made Solar demonstrably more effective than existing under-approximate reflection analyses [5, 17, 20, 21] as validated later