147:10 Tian Tan,Yue Li,Xiaoxing Ma,Chang Xu,and Yannis Smaragdakis A)guided by any input selective approach,and can expect Relay-o2 to scale as long as A scales. However,the pass ordering may affect the final precision of Relay(although experimental results show that such effect is very minor).For example,assume two variables v1 and v2 point to {ol,02} and (o3,04)respectively under CI.Pass 1 identifies o2 as a spurious object for v1,and pass 2 can identify o4 as a false object if and only if it is aware that v1 does not point to o2 with the help of the result from pass 1.But when we swap the order of pass 1 and pass 2,v2 may still point to o4 (actually a spurious object)at the conclusion of all passes,resulting in different precision.We will discuss the pass ordering issue using the experimental results in Section 6.2. 4 FORMALISM AND PROPERTIES We formalize the Unity-Relay framework,prove its key properties,and discuss its important features.Specifically,we detail how to unify various context-sensitivity approaches with different context elements and lengths,and how to guide selective context-sensitive pointer analysis in each pass to filter spurious objects using the results from the previous pass,while achieving soundness and precision guarantees. 4.1 Domain and Notations Our notation is shown in Figure 5.For formalization purposes,two domains of context elements, K and B are introduced.The former denotes the kinds of context elements,i.e.,obj for object sensitivity,type for type-sensitivity and call for call-site sensitivity(identified by their locations in the program)while the latter denotes the concrete context elements forming each context c E C. For instance,in object sensitivity,c consists of a list of heap objects (allocation sites)o;EB.Each context-sensitivity variant cs E CS can be expressed as a pair of context length l and a kind of context element k,denoted by lk,e.g.,2obj or 1type,hence we have CS =NxK,where N denotes the natural numbers. pt and fpt denote the analysis results.pt(c,x)represents the points-to set of variable x under context c.fpt(c,oi,f)represents the points-to set of instance field f of an abstract object o;under context c.The objects in the points-to sets of pt and fot are also qualified by contexts,i.e.,heap contexts. gencs denotes the function that generates contexts according to the length and kind of context elements of cs,which will be further explained in Section 4.2.contextsOfmaps a method to a set of contexts under which the method is analyzed.selectCS is the core of selective context sensitivity, which selects a proper context-sensitivity variant cs for each method.We use S to denote a set of selective approaches,indexed by subscript:Si.If a pointer analysis PA is guided by a selective approach Si,we refer to it as PA-Si. 4.2 Selective Context-Sensitive Pointer Analysis We present a formulation of general selective context-sensitive pointer analysis in Figure 6,which covers five basic statements:object allocation ([NEw)),local assignment ([AssIGN]),field load ([LoAD)) and store ([STORE]),and method call ([CALL]).Similar to [Sridharan et al.2013;Tan et al.2016],we elide the rules for static members and arrays,as the former is straightforward and the latter can be modeled as load and store to an artificial field of each array.In Figure 6,the premises within boxes are only related to Unity-Relay,and thus can be ignored for now. For each rule in Figure 6,m denotes the method containing the corresponding statement(in blue color).Here we only explain [NEw]and [CALL]as the other three rules are standard. In context-sensitive pointer analysis,an abstract object is typically represented by a heap context and the label of the allocation site,as in our [NEw]rule.For simplicity,we directly use the context of the method containing the allocation site(i.e.,c)as the heap context for the created abstract Proc.ACM Program.Lang.,Vol.5.No.OOPSLA,Article 147.Publication date:October 2021.147:10 Tian Tan, Yue Li, Xiaoxing Ma, Chang Xu, and Yannis Smaragdakis A) guided by any input selective approach, and can expect Relay-o2 to scale as long as A scales. However, the pass ordering may affect the final precision of Relay (although experimental results show that such effect is very minor). For example, assume two variables v1 and v2 point to {o1,o2} and {o3,o4} respectively under CI. Pass 1 identifies o2 as a spurious object for v1, and pass 2 can identify o4 as a false object if and only if it is aware that v1 does not point to o2 with the help of the result from pass 1. But when we swap the order of pass 1 and pass 2, v2 may still point to o4 (actually a spurious object) at the conclusion of all passes, resulting in different precision. We will discuss the pass ordering issue using the experimental results in Section 6.2. 4 FORMALISM AND PROPERTIES We formalize the Unity-Relay framework, prove its key properties, and discuss its important features. Specifically, we detail how to unify various context-sensitivity approaches with different context elements and lengths, and how to guide selective context-sensitive pointer analysis in each pass to filter spurious objects using the results from the previous pass, while achieving soundness and precision guarantees. 4.1 Domain and Notations Our notation is shown in Figure 5. For formalization purposes, two domains of context elements, K and E are introduced. The former denotes the kinds of context elements, i.e., obj for object sensitivity, type for type-sensitivity and call for call-site sensitivity (identified by their locations in the program) while the latter denotes the concrete context elements forming each context 𝑐 ∈ C. For instance, in object sensitivity, 𝑐 consists of a list of heap objects (allocation sites) 𝑜𝑖 ∈ E . Each context-sensitivity variant 𝑐𝑠 ∈ CS can be expressed as a pair of context length 𝑙 and a kind of context element 𝑘, denoted by 𝑙𝑘, e.g., 2obj or 1type, hence we have CS = N × K, where N denotes the natural numbers. pt and fpt denote the analysis results. pt(𝑐, 𝑥) represents the points-to set of variable 𝑥 under context 𝑐. fpt(𝑐, 𝑜𝑖 , 𝑓 ) represents the points-to set of instance field 𝑓 of an abstract object 𝑜𝑖 under context 𝑐. The objects in the points-to sets of pt and fpt are also qualified by contexts, i.e., heap contexts. gen𝑐𝑠 denotes the function that generates contexts according to the length and kind of context elements of 𝑐𝑠, which will be further explained in Section 4.2. contextsOf maps a method to a set of contexts under which the method is analyzed. selectCS is the core of selective context sensitivity, which selects a proper context-sensitivity variant 𝑐𝑠 for each method. We use 𝑆 to denote a set of selective approaches, indexed by subscript: 𝑆𝑖 . If a pointer analysis PA is guided by a selective approach 𝑆𝑖 , we refer to it as PA-𝑆𝑖 . 4.2 Selective Context-Sensitive Pointer Analysis We present a formulation of general selective context-sensitive pointer analysis in Figure 6, which covers five basic statements: object allocation ([New]), local assignment ([Assign]), field load ([Load]) and store ([Store]), and method call ([Call]). Similar to [Sridharan et al. 2013; Tan et al. 2016], we elide the rules for static members and arrays, as the former is straightforward and the latter can be modeled as load and store to an artificial field of each array. In Figure 6, the premises within boxes are only related to Unity-Relay, and thus can be ignored for now. For each rule in Figure 6, 𝑚 denotes the method containing the corresponding statement (in blue color). Here we only explain [New] and [Call] as the other three rules are standard. In context-sensitive pointer analysis, an abstract object is typically represented by a heap context and the label of the allocation site, as in our [New] rule. For simplicity, we directly use the context of the method containing the allocation site (i.e., 𝑐) as the heap context for the created abstract Proc. ACM Program. Lang., Vol. 5, No. OOPSLA, Article 147. Publication date: October 2021