XX:14 Program Tailoring:Slicing by Sequential Criteria 4.3 Properties We prove that TAILOR is sound(Theorem 3),by showing that SCDFA and SCEXT are sound with respect to GICFG (Theorems 1 and 2),and consequently,that every tailored program is SC-erecutable,i.e.,executable along all execution paths passing through a given SC. We make use of the notations statement s,81,52,,8m∈S given in Figure 8 in our proofs.S is a execution e:s1s25m∈EG set of statements in GICFC.EG rep- sequence sg:s1s2..sm∈SC resents all runtime executions of the relation EG×SC e sq program represented by GICFG and relation EC x S e→s each execution e consists of a se- execution set Esg={e∈Ec|ewsq} quence of statements in S.We write statement set Ss9={s∈S|e∈Es9,e→s} e ~sq if execution e contains all the Figure 8 Notations used in proofs. statements in a statement sequence sq=8182...sm in exactly the same order,ending at sm.We write es if execution e contains statement s.Esq is the set of all executions that pass through a given sequence sq.Finally,Ss9 is the set of all statements that appear in all possible executions e(passing through sq),where e EEs9. The following theorem states that SCDFA is sound with respect to GICFG. Theorem 1(Soundness of SCDFA).Let GICFG be the ICFG of a program.Let SC be given (as defined in Section3).fsg∈SC,then s∈ssg→TAILORED(s). Proof.We show that for every execution e such that e~sq,where sq E SC,TAlLORED(s), which is given in (12),holds for all statements s such that es.Let sq s1s2...sm. Since e~sq,every statement si must appear at least once in e or more in the presence of control-flow cycles.For convenience,let s be a fictitious statement at the beginning of e.Let sm+l be the last occurrence of sm in e,i.e.,the last statement in e.Let si be the first occurrence of si in e after s,where 1si<m.We can now divide e into m+I sub-executions,where represents the sub-sequence between (exclusive)and s(inclusive).We will still write eis if ei contains a statement s. As e sq is an execution,then e represents a realizable path,which must appear in GICFG.In SCDFA,its BU and TD passes are distributive over 2 given in(1),performed context-sensitively.Thus,we only need to focus on this path.Note that in our formulation of SCDFA,a statement si and its corresponding node ni in GICFG are used interchangebly. During the BU pass in terms of(2)-(6),we must have: V1≤i≤m:V ni s..te:→ni:sisi+1…sm∈PANTIo(n) (15) Vnm+1s.t.em+1→nm+1:sm∈PANTIou(nm+i） (16) which implies sq∈PANTIout(ENTRY)(since Vn1s.t.e1→n1:s1s2·sn∈PANTIout(n1). During the TD pass,sqE PAVAlL(ENTRY)by (7).By (8)-(11),we must have: H1≤i≤m:Vn:s.t.e→n:ssi+1…sm∈PAVAIL(n) (17) Vnm+1s.t.em+1→nm+1:e∈PAVAILi(nm+1) (18) (Note that (18)is needed only if em+1 is non-empty,which happens when sm is in a control-flow cycle.)Hence,TAlLORED(s)holds for every statement s such that es. For a SC,we write a(GICFG,SC)to represent the set of all executions in GicrG that pass at least one sequence in SC,i.e.,a(GCrC,SC)c.Theorem 1 can also be stated equivalently as follows:TAlLORED(s)holds for every sE{s eEa(GICFG,SC),e-s}.XX:14 Program Tailoring: Slicing by Sequential Criteria 4.3 Properties We prove that Tailor is sound (Theorem 3), by showing that SCDFA and SCEXT are sound with respect to GICFG (Theorems 1 and 2), and consequently, that every tailored program is SC-executable, i.e., executable along all execution paths passing through a given SC. statement s, s1, s2, ..., sm ∈ S execution e : s1s2...sm ∈ E G sequence sq : s1s2...sm ∈ SC relation E G × SC e sq relation E G × S e → s execution set E sq = {e ∈ E G | e sq} statement set S sq = {s ∈ S | e ∈ E sq, e → s} Figure 8 Notations used in proofs. We make use of the notations given in Figure 8 in our proofs. S is a set of statements in GICFG. E G rep￾resents all runtime executions of the program represented by GICFG and each execution e consists of a se￾quence of statements in S. We write e sq if execution e contains all the statements in a statement sequence sq = s1s2 · · · sm in exactly the same order, ending at sm. We write e → s if execution e contains statement s. E sq is the set of all executions that pass through a given sequence sq. Finally, S sq is the set of all statements that appear in all possible executions e (passing through sq), where e ∈ E sq . The following theorem states that SCDFA is sound with respect to GICFG. I Theorem 1 (Soundness of SCDFA). Let GICFG be the ICFG of a program. Let SC be given (as defined in Section 3). If sq ∈ SC, then s ∈ S sq =⇒ TAILORED(s). Proof. We show that for every execution e such that e sq, where sq ∈ SC, TAILORED(s), which is given in (12), holds for all statements s such that e → s. Let sq = s1s2...sm. Since e sq, every statement si must appear at least once in e or more in the presence of control-flow cycles. For convenience, let s 0 e be a fictitious statement at the beginning of e. Let s m+1 e be the last occurrence of sm in e, i.e., the last statement in e. Let s i e be the first occurrence of si in e after s i−1 e , where 1 6 i 6 m. We can now divide e into m + 1 sub-executions, e1, e2, · · · , em+1, where ei , represents the sub-sequence between s i−1 e (exclusive) and s i e (inclusive). We will still write ei → s if ei contains a statement s. As e sq is an execution, then e represents a realizable path, which must appear in GICFG. In SCDFA, its BU and TD passes are distributive over 2 D given in (1), performed context-sensitively. Thus, we only need to focus on this path. Note that in our formulation of SCDFA, a statement si and its corresponding node ni in GICFG are used interchangebly. During the BU pass in terms of (2) – (6), we must have: ∀ 1 6 i 6 m : ∀ ni s.t. ei → ni : sisi+1 · · · sm ∈ PANTIout(ni) (15) ∀ nm+1 s.t. em+1 → nm+1 : sm ∈ PANTIout(nm+1) (16) which implies sq ∈ PANTIout(ENTRY) (since ∀ n1 s.t. e1 → n1 : s1s2 · · · sn ∈ PANTIout(n1)). During the TD pass, sq ∈ PAVAILin(ENTRY) by (7). By (8) – (11), we must have: ∀ 1 6 i 6 m : ∀ ni s.t. ei → ni : sisi+1 · · · sm ∈ PAVAILin(ni) (17) ∀ nm+1 s.t. em+1 → nm+1 :  ∈ PAVAILin(nm+1) (18) (Note that (18) is needed only if em+1 is non-empty, which happens when sm is in a control-flow cycle.) Hence, TAILORED(s) holds for every statement s such that e → s. J For a SC, we write α(GICFG, SC) to represent the set of all executions in GICFG that pass at least one sequence in SC, i.e., α(GICFG, SC) = S sq∈SC E sq. Theorem 1 can also be stated equivalently as follows: TAILORED(s) holds for every s ∈ {s | e ∈ α(GICFG, SC), e → s}