147:12 Tian Tan,Yue Li,Xiaoxing Ma,Chang Xu,and Yannis Smaragdakis i:x=new T()cE contextsOf(m) [NEW] (c,oi〉∈pt(c,x) x=yc∈contextsOfm) (c,oi〉∈pt(c,y）oi∈pptx) [ASSIGN] (C,oi》Ept(c,x) x=yfc∈contextsOfm)(c',oi〉∈pt(c,y) (c",oj〉efpt(c',oi,f月oj∈ppt(x [LOAD] (c",oj》∈pc,x) x.f=yc∈contextsOfm) (c',oi〉∈pt(c,x)(e",oj》∈pt(e,y -[STORE] (c",oi》∈fpt(c',oi,f) j:x=y.g(a1,..an)cE contextsOf m) (e,oi〉ept(c,y)oi∈ppt(m m'=dispatch(oi,g) cs=selectCs(m')c=gencs(c',oi,c.j) (ca,oa)∈pt(c,ak),1≤k≤n oa∈ppt(m (c',or〉ept(c,mret)or∈ppt CALL] econtextsOf(m')e',oi〉∈pt(c,mthis) (c,a）ept(c,mpk)(e,or〉ept(c,x) Fig.6.Rules for selective context-sensitive pointer analysis.The premises enclosed in boxes are specific to Unity-Relay-based pointer analysis. is always more precise than (or as precise as)the other one.For such comparison,we introduce notation kEk'to represent that using context element k is less precise than (or as precise as)k'. The variants of some kinds of context elements are comparable,e.g.,obj and type.As type is a coarser context abstraction over(and always less precise than)object [Smaragdakis et al.2011], we have type E obj,and accordingly,Itype lobj.In other cases,such as lobj and Icall,their precision are theoretically incomparable.We will discuss how to handle such cases at the end of this section.For now,we assume that all concerned context-sensitivity variants are comparable. Now we define cs s cs': cs≤cs'ifcs=CIV(I≤I'AkSk) where cs lk and cs'=I'k' (1) Formula(1)states that any context sensitivity variant is not less precise than CI,and cs<cs'only when both length and kind of context elements of cs are at most as precise as those of cs'. Next we can formalize the C.S.selector of Unity as a function selectCS-unity(m): selectCS-unity (m)=max <ses selectCSi(m) (2) Based on <max <s es chooses the most precise cs from a set of selective approaches S for method m.selectCS;corresponds to the selector function for Si.By specifying selectCS in [CALL]to selectCS-unity,we get a pointer analysis guided by Unity,i.e.,PA-Unitys. Proc.ACM Program.Lang.,Vol.5.No.OOPSLA,Article 147.Publication date:October 2021.147:12 Tian Tan, Yue Li, Xiaoxing Ma, Chang Xu, and Yannis Smaragdakis 𝑖 : 𝑥 = 𝑛𝑒𝑤 𝑇 () 𝑐 ∈ contextsOf(𝑚) ⟨𝑐, 𝑜𝑖⟩ ∈ 𝑝𝑡(𝑐, 𝑥) [New] 𝑥 = 𝑦 𝑐 ∈ contextsOf(𝑚) ⟨𝑐, 𝑜𝑖⟩ ∈ 𝑝𝑡(𝑐, 𝑦) 𝑜𝑖 ∈ ppt(𝑥) ⟨𝑐, 𝑜𝑖⟩ ∈ 𝑝𝑡(𝑐, 𝑥) [Assign] 𝑥 = 𝑦.𝑓 𝑐 ∈ contextsOf(𝑚) ⟨𝑐 ′ , 𝑜𝑖⟩ ∈ pt(𝑐, 𝑦) ⟨𝑐 ′′, 𝑜 𝑗⟩ ∈ fpt(𝑐 ′ , 𝑜𝑖 , 𝑓 ) 𝑜 𝑗 ∈ ppt(𝑥) ⟨𝑐 ′′, 𝑜 𝑗⟩ ∈ pt(𝑐, 𝑥) [Load] 𝑥.𝑓 = 𝑦 𝑐 ∈ contextsOf(𝑚) ⟨𝑐 ′ , 𝑜𝑖⟩ ∈ 𝑝𝑡(𝑐, 𝑥) ⟨𝑐 ′′, 𝑜 𝑗⟩ ∈ 𝑝𝑡(𝑐, 𝑦) ⟨𝑐 ′′, 𝑜 𝑗⟩ ∈ fpt(𝑐 ′ , 𝑜𝑖 , 𝑓 ) [Store] 𝑗 : 𝑥 = 𝑦.𝑔(𝑎1, ..., 𝑎𝑛) 𝑐 ∈ contextsOf(𝑚) ⟨𝑐 ′ , 𝑜𝑖⟩ ∈ 𝑝𝑡(𝑐, 𝑦) 𝑜𝑖 ∈ ppt(𝑚′ 𝑡ℎ𝑖𝑠) 𝑚′ = dispatch(𝑜𝑖 , 𝑔) 𝑐𝑠 = selectCS(𝑚′ ) 𝑐 𝑡 = gen𝑐𝑠 (𝑐 ′ , 𝑜𝑖 , 𝑐, 𝑗) ⟨𝑐 𝑎 , 𝑜𝑎⟩ ∈ 𝑝𝑡(𝑐, 𝑎𝑘 ), 1 ≤ 𝑘 ≤ 𝑛 𝑜𝑎 ∈ ppt(𝑚′ 𝑝𝑘 ) ⟨𝑐 𝑟 , 𝑜𝑟⟩ ∈ 𝑝𝑡(𝑐 𝑡 ,𝑚′ 𝑟𝑒𝑡) 𝑜𝑟 ∈ ppt(𝑥) 𝑐 𝑡 ∈ contextsOf(𝑚′ ) ⟨𝑐 ′ , 𝑜𝑖⟩ ∈ 𝑝𝑡(𝑐 𝑡 ,𝑚′ 𝑡ℎ𝑖𝑠) ⟨𝑐 𝑎 , 𝑜𝑎⟩ ∈ 𝑝𝑡(𝑐 𝑡 ,𝑚′ 𝑝𝑘 ) ⟨𝑐 𝑟 , 𝑜𝑟⟩ ∈ 𝑝𝑡(𝑐, 𝑥) [Call] Fig. 6. Rules for selective context-sensitive pointer analysis. The premises enclosed in boxes are specific to Unity-Relay-based pointer analysis. is always more precise than (or as precise as) the other one. For such comparison, we introduce notation 𝑘 ⊑ 𝑘 ′ to represent that using context element 𝑘 is less precise than (or as precise as) 𝑘 ′ . The variants of some kinds of context elements are comparable, e.g., obj and type. As type is a coarser context abstraction over (and always less precise than) object [Smaragdakis et al. 2011], we have type ⊑ obj, and accordingly, 𝑙type ⪯ 𝑙obj. In other cases, such as 𝑙obj and 𝑙call, their precision are theoretically incomparable. We will discuss how to handle such cases at the end of this section. For now, we assume that all concerned context-sensitivity variants are comparable. Now we define 𝑐𝑠 ⪯ 𝑐𝑠′ : 𝑐𝑠 ⪯ 𝑐𝑠′ iff 𝑐𝑠 = CI ∨ (𝑙 ⩽ 𝑙 ′ ∧ 𝑘 ⊑ 𝑘 ′ ) where 𝑐𝑠 = 𝑙𝑘 and 𝑐𝑠′ = 𝑙 ′ 𝑘 ′ (1) Formula (1) states that any context sensitivity variant is not less precise than CI, and 𝑐𝑠 ⪯ 𝑐𝑠′ only when both length and kind of context elements of 𝑐𝑠 are at most as precise as those of 𝑐𝑠′ . Next we can formalize the C.S. selector of Unity as a function selectCS-unity𝑆 (𝑚): selectCS-unity𝑆 (𝑚) = max ⪯𝑆𝑖 ∈𝑆 selectCS𝑖(𝑚) (2) Based on ⪯, max ⪯𝑆𝑖 ∈𝑆 chooses the most precise 𝑐𝑠 from a set of selective approaches 𝑆 for method 𝑚. selectCS𝑖 corresponds to the selector function for 𝑆𝑖 . By specifying selectCS in [Call] to selectCS-unity𝑆 , we get a pointer analysis guided by Unity, i.e., PA-Unity𝑆 . Proc. ACM Program. Lang., Vol. 5, No. OOPSLA, Article 147. Publication date: October 2021