Y.Li,T.Tan,Y.Zhang,and J.Xue XX:15 The following theorem states that SCEXT is sound since only infeasible paths are ignored. Theorem 2(Soundness of SCEXT).Let ESC be ertended from a given SC by applying SCEXT in GICFG,then a(GICFG,SC)=a(GICFG,ESC). Proof.According to the algorithm of SCEXT operating in GICFG (Section 4.2),all possible object-sensitive calling contexts for a method containing the first point F in a sequence of SC are considered as the extension points of F.According to (13)and(14),no feasible paths with respect to SC are excluded if an extension point of F is not selected.Thus,only infeasible paths with respect to SC are ignored when SC is extended into ESC this way. Theorem 3 (Soundness of TAILOR).TAILOR is sound with respect to GICFG. Proof.Follows from Theorems 1 and 2. Theorem 4(SC-Executability).T(SC)obtained in GICFG is SC-executable. Proof.By Theorem 3,a(GICFG,SC)is included in the tailored program. 5 Implementation We have implemented TAILOR (http://www.cse.unsw.edu.au/-corg/tailor)in SOoT, a framework for analyzing and optimizing Java programs [51].To build the ICFG for a program,we apply SooT's SPARK pointer analysis [27].During the ICFG construction, Soor models the effects of native methods by using abstract Java code and creates the corresponding control-flow edges.In addition,Soor considers both explicit and implicit exceptions and treats the exceptional edges as normal control-flow edges.Finally,Soor models thread creation and running as method calls by assuming that threads execute in a sequential order.How to build ICFGs to support multi-threading soundly,precisely and scalably for Java programs is a big challenge in its own right. TAILOR has two main components,SCEXT and SCDFA.When extending SCs,we make use of the points-to information provided by SPARK to find the required object allocation sites object-sensitively.To perform SCDFA,we choose HEROS [10]as the IFDS solver for its BU and TD data-flow problems,because it can be easily plugged into the Soor framework. 6 Evaluation Program tailoring is designed to be sound for a program(with respect to its ICFG,as proved in Section 4),with useful precision and good scalability for large object-oriented programs. This section serves to evaluate the last two goals by answering three research questions: RQ1:Is TAILOR useful to support program debugging and understanding,in practice? RQ2:Is TAILOR useful to support program analysis,in practice? RQ3:Is TAILOR scalable for large object-oriented programs,in practice? To address RQ1 and RQ2,we conduct two real-world case studies.In one study,we demonstrate that TAILOR can assist a state-of-the-art slicing tool,a thin slicer [47]implemen- ted in WALA [52],to simplify debugging and understanding tasks.In the other study,we demonstrate that TAILOR can enable a sophisticated pointer analysis algorithm,S-2OBJ [24], provided in a state-of-the-art pointer analysis tool for Java,Doop [14],to investigate the multi-object typestate(reflective)behavior in programs for which S-20BJ is unscalable as a whole-program analysis.In both studies,all SCs used are deduced from the results generated by state-of-the-art clients,CLARA [9]and SOLAR [29],rather than injected manually. EC00P2016Y. Li, T. Tan, Y. Zhang, and J. Xue XX:15 The following theorem states that SCEXT is sound since only infeasible paths are ignored. I Theorem 2 (Soundness of SCEXT). Let ESC be extended from a given SC by applying SCEXT in GICFG, then α(GICFG, SC) = α(GICFG, ESC). Proof. According to the algorithm of SCEXT operating in GICFG (Section 4.2), all possible object-sensitive calling contexts for a method containing the first point F in a sequence of SC are considered as the extension points of F. According to (13) and (14), no feasible paths with respect to SC are excluded if an extension point of F is not selected. Thus, only infeasible paths with respect to SC are ignored when SC is extended into ESC this way. J I Theorem 3 (Soundness of Tailor). Tailor is sound with respect to GICFG. Proof. Follows from Theorems 1 and 2. J I Theorem 4 (SC-Executability). T (SC) obtained in GICFG is SC-executable. Proof. By Theorem 3, α(GICFG, SC) is included in the tailored program. J 5 Implementation We have implemented Tailor (http://www.cse.unsw.edu.au/~corg/tailor) in Soot, a framework for analyzing and optimizing Java programs [51]. To build the ICFG for a program, we apply Soot’s Spark pointer analysis [27]. During the ICFG construction, Soot models the effects of native methods by using abstract Java code and creates the corresponding control-flow edges. In addition, Soot considers both explicit and implicit exceptions and treats the exceptional edges as normal control-flow edges. Finally, Soot models thread creation and running as method calls by assuming that threads execute in a sequential order. How to build ICFGs to support multi-threading soundly, precisely and scalably for Java programs is a big challenge in its own right. Tailor has two main components, SCEXT and SCDFA. When extending SCs, we make use of the points-to information provided by Spark to find the required object allocation sites object-sensitively. To perform SCDFA, we choose Heros [10] as the IFDS solver for its BU and TD data-flow problems, because it can be easily plugged into the Soot framework. 6 Evaluation Program tailoring is designed to be sound for a program (with respect to its ICFG, as proved in Section 4), with useful precision and good scalability for large object-oriented programs. This section serves to evaluate the last two goals by answering three research questions: RQ1: Is Tailor useful to support program debugging and understanding, in practice? RQ2: Is Tailor useful to support program analysis, in practice? RQ3: Is Tailor scalable for large object-oriented programs, in practice? To address RQ1 and RQ2, we conduct two real-world case studies. In one study, we demonstrate that Tailor can assist a state-of-the-art slicing tool, a thin slicer [47] implemen￾ted in WALA [52], to simplify debugging and understanding tasks. In the other study, we demonstrate that Tailor can enable a sophisticated pointer analysis algorithm, S-2Obj [24], provided in a state-of-the-art pointer analysis tool for Java, Doop [14], to investigate the multi-object typestate (reflective) behavior in programs for which S-2Obj is unscalable as a whole-program analysis. In both studies, all SCs used are deduced from the results generated by state-of-the-art clients, Clara [9] and Solar [29], rather than injected manually. E COO P 2 0 1 6