147:14 Tian Tan,Yue Li,Xiaoxing Ma,Chang Xu,and Yannis Smaragdakis current(and future)passes,as they are identified as spurious points-to information by previous analyses. Filtering prevents spurious objects from being propagated to variables.[NEw]does not propagate spurious objects(for statement i:x=new T(),x must point to oi).[STORE]propagates objects to instance fields(not variables),and the stored objects can only be accessed by a load operation.Then with the filtering by ppt in [LoAD],spurious objects from instance fields will not be propagated to other variables.Thus we do not need to apply filtering for [NEw]and [SToRE]. With filtering,the precision achieved in each pass can be transmitted to and accumulated in later passes. LEMMA 4.4 (SOUNDNESS OF FILTERING).In Figure 6,if ppt(_)are the results of a sound pointer analysis PA,then the resulting filtered pointer analysis PA'is also sound. ProoF.By [AssIGN],[LoAD],and [CALL],the filtering only removes the points-to results which are absent in PA.Since PA is sound,it will not filter out true points-to results.Hence the filtering based on PA does not affect soundness in PA'. ◇ THEOREM 4.5(SOUNDNESS OF Relay).For any pass;in Relay,PA-Relay'is sound. PRooF.For any passi in Relay,we assume that PA-Relayi may use any approach in S,i.e.,the approaches in S can be arranged in any order.By the rules in Figure 6,PA-Relay without pointer analysis filtering is sound(refer to the proof of Theorem 4.1).As passi of Relay does not have filtering,PA-Relay is sound(regardless of the approach it uses).The filtering of PA-Relay;is based on the results of PA-RelaysThus,by Lemma 4.4,no matter what approaches PA-Relay and PA-Relay'use(i.e.,the order of approaches is irrelevant),if PA-Relay is sound,PA-Relay is sound.By induction,for any passi,PA-Relay;is sound. ◇ THEOREM 4.6(PRECISION OF Relay).Given a set of selective approaches S,VSiE S:PA-S;3 PA-RelayPA-Relays(the last pass of Relay)for both Relay-01 and Relay-02. PROoF.Similarly to the proof of Theorem 4.5,we assume that PA-Relay;may use any approach in S.By Equations (3)and(4),for each method,the cs selected by selectCS-relay (of both Relay-o1 and Relay-02)is more precise than that selected by selectCSi,thus,VSiES:PA-S;<PA-Relay regardless of what approach S;is.By pointer analysis filtering,each variable x in pass;must point to fewer (or the same)objects than x in passi-1.i.e..PA-Relay PA-Relay:in other words. each pass is more precise than all its previous passes,no matter what approaches these passes use(ie the order of approaches is irrelevant).As PA-Relays is the last pass of Relay,we have VSES:PA-RelayPA-Relay Hence,VSeS:PA-S;<PA-RelayPA-Relays Interestingly,Theorem 4.6 holds for Relay-02 regardless of whether the context-sensitivity variants selected by selectCS-relay are comparable or not.Since by Equation(4).Relay-02 selects the same context-sensitivity variants as the selective approach Si in passi,and further by the precision accumulation(via filtering),PA-Relay;is at least as precise as(practically more precise than)PA-Si.Accordingly,the last pass of Relay-02 is at least as precise as any PA-Si. As for Unity and Relay-o1,in the case that some selected variants are theoretically incom- parable,e.g.,2obj and 2call,their precision guarantee does not hold in theory.But in practice, users can choose an appropriate one empirically.E.g.,2obj is typically much more precise than 2call [Kastrinis and Smaragdakis 2013;Tan et al.2016].In this way,we can still obtain from Unity-Relay a pointer analysis that is likely more precise than any S;in practice. Proc.ACM Program.Lang.,Vol.5.No.OOPSLA,Article 147.Publication date:October 2021.147:14 Tian Tan, Yue Li, Xiaoxing Ma, Chang Xu, and Yannis Smaragdakis current (and future) passes, as they are identified as spurious points-to information by previous analyses. Filtering prevents spurious objects from being propagated to variables. [New] does not propagate spurious objects (for statement 𝑖 : 𝑥 = 𝑛𝑒𝑤 𝑇 (), 𝑥 must point to 𝑜𝑖 ). [Store] propagates objects to instance fields (not variables), and the stored objects can only be accessed by a load operation. Then with the filtering by ppt in [Load], spurious objects from instance fields will not be propagated to other variables. Thus we do not need to apply filtering for [New] and [Store]. With filtering, the precision achieved in each pass can be transmitted to and accumulated in later passes. Lemma 4.4 (Soundness of Filtering). In Figure 6, if ppt(_) are the results of a sound pointer analysis PA, then the resulting filtered pointer analysis PA′ is also sound. Proof. By [Assign], [Load], and [Call], the filtering only removes the points-to results which are absent in PA. Since PA is sound, it will not filter out true points-to results. Hence the filtering based on PA does not affect soundness in PA′ . □ Theorem 4.5 (Soundness of Relay). For any pass𝑖 in Relay, PA-Relay𝑆 𝑖 is sound. Proof. For any pass𝑖 in Relay, we assume that PA-Relay𝑆 𝑖 may use any approach in 𝑆, i.e., the approaches in 𝑆 can be arranged in any order. By the rules in Figure 6, PA-Relay𝑆 𝑖 without pointer analysis filtering is sound (refer to the proof of Theorem 4.1). As pass1 of Relay does not have filtering, PA-Relay𝑆 1 is sound (regardless of the approach it uses). The filtering of PA-Relay𝑆 𝑖 is based on the results of PA-Relay𝑆 𝑖−1 . Thus, by Lemma 4.4, no matter what approaches PA-Relay𝑆 𝑖−1 and PA-Relay𝑆 𝑖 use (i.e., the order of approaches is irrelevant), if PA-Relay𝑆 𝑖−1 is sound, PA-Relay𝑆 𝑖 is sound. By induction, for any pass𝑖 , PA-Relay𝑆 𝑖 is sound. □ Theorem 4.6 (Precision of Relay). Given a set of selective approaches S, ∀𝑆𝑖 ∈ 𝑆 : PA-𝑆𝑖 ⪯ PA-Relay𝑆 𝑖 ⪯ PA-Relay𝑆 |𝑆 | (the last pass of Relay) for both Relay-o1 and Relay-o2. Proof. Similarly to the proof of Theorem 4.5, we assume that PA-Relay𝑆 𝑖 may use any approach in 𝑆. By Equations (3) and (4), for each method, the 𝑐𝑠 selected by selectCS-relay𝑆 𝑖 (of both Relay-o1 and Relay-o2) is more precise than that selected by selectCS𝑖 , thus, ∀𝑆𝑖 ∈ 𝑆 : PA-𝑆𝑖 ⪯ PA-Relay𝑆 𝑖 regardless of what approach 𝑆𝑖 is. By pointer analysis filtering, each variable 𝑥 in pass𝑖 must point to fewer (or the same) objects than 𝑥 in pass𝑖−1, i.e., PA-Relay𝑆 𝑖−1 ⪯ PA-Relay𝑆 𝑖 ; in other words, each pass is more precise than all its previous passes, no matter what approaches these passes use (i.e., the order of approaches is irrelevant). As PA-Relay𝑆 |𝑆 | is the last pass of Relay, we have ∀𝑆𝑖 ∈ 𝑆 : PA-Relay𝑆 𝑖 ⪯ PA-Relay𝑆 |𝑆 | . Hence, ∀𝑆𝑖 ∈ 𝑆 : PA-𝑆𝑖 ⪯ PA-Relay𝑆 𝑖 ⪯ PA-Relay𝑆 |𝑆 | . □ Interestingly, Theorem 4.6 holds for Relay-o2 regardless of whether the context-sensitivity variants selected by selectCS-relay𝑆 𝑖 are comparable or not. Since by Equation (4), Relay-o2 selects the same context-sensitivity variants as the selective approach 𝑆𝑖 in pass𝑖 , and further by the precision accumulation (via filtering), PA-Relay𝑆 𝑖 is at least as precise as (practically more precise than) PA-𝑆𝑖 . Accordingly, the last pass of Relay-o2 is at least as precise as any PA-𝑆𝑖 . As for Unity and Relay-o1, in the case that some selected variants are theoretically incom￾parable, e.g., 2obj and 2call, their precision guarantee does not hold in theory. But in practice, users can choose an appropriate one empirically. E.g., 2obj is typically much more precise than 2call [Kastrinis and Smaragdakis 2013; Tan et al. 2016]. In this way, we can still obtain from Unity-Relay a pointer analysis that is likely more precise than any 𝑆𝑖 in practice. Proc. ACM Program. Lang., Vol. 5, No. OOPSLA, Article 147. Publication date: October 2021