Very Busy Expressions Analysis kill and gen functions killB([x:=a])={a∈AExp*|x∈FV(a} killB([skip]e) =0 killvB([]) =0 genvB([x :a]e) 三 AExp(a) genvB([skip]) 三 0 genvB([])= AExp(6) data flow equations:VB= VBerit(e)= 00 ife∈final(S*) InVBentry(e')(e',e)E flowR(S,)}otherwise VBentry(e)=(VBerit(e)\killvB(Be))UgenvB(Be) where B∈blocks(S*) PPA Section 2.1 F.Nielson H.Riis Nielson C.Hankin (May 2005) 26
Very Busy Expressions Analysis kill and gen functions killVB([x := a] `) = {a 0 ∈ AExp? | x ∈ FV(a 0)} killVB([skip] `) = ∅ killVB([b] `) = ∅ genVB([x := a] `) = AExp(a) genVB([skip] `) = ∅ genVB([b] `) = AExp(b) data flow equations: VB= VBexit(`) = ( ∅ if ` ∈ final(S?) T {VBentry(` 0) | (` 0 , `) ∈ flowR(S?)} otherwise VBentry(`) = (VBexit(`)\killVB(B`)) ∪ genVB(B`) where B` ∈ blocks(S?) PPA Section 2.1 c F.Nielson & H.Riis Nielson & C.Hankin (May 2005) 26
Example: if [a>b]then ([x:=b-a]2;[y:=a-b]3)else ([y:=b-a]4;[x:=a-b]5) kill and gen function: killB(e)genvB(e) 1 0 0 2 0 {b-a} 0 {a-b} 4 0 {b-a} 5 0 {a-b} PPA Section 2.1 F.Nielson H.Riis Nielson C.Hankin (May 2005) 27
Example: if [a>b] 1 then ([x:=b-a] 2 ; [y:=a-b] 3 ) else ([y:=b-a] 4 ; [x:=a-b] 5 ) kill and gen function: ` killVB(`) genVB(`) 1 ∅ ∅ 2 ∅ {b-a} 3 ∅ {a-b} 4 ∅ {b-a} 5 ∅ {a-b} PPA Section 2.1 c F.Nielson & H.Riis Nielson & C.Hankin (May 2005) 27
Example (cont.) if [a>b]1 then ([x:=b-a]2;[y:=a-b]3)else ([y:=b-a]4;[x:=a-b]5) Equations: VBentry(1) =VBerit(1) VBentry(2) 三 VBerit(2)U{b-a} VBentry(3) ={a-b} VBentry(4) 三 VBerit(4)U{b-a} VBentry(5) = {a-b} VBerit(1) = VBentry(2)nVBentry(4) VBerit(2) 三 VBentry(3) VBerit(3) = 0 VBerit(4) 三 VBentry(5) VBerit(5) = 0 PPA Section 2.1 CF.Nielson H.Riis Nielson C.Hankin (May 2005) 28
Example (cont.): if [a>b] 1 then ([x:=b-a] 2 ; [y:=a-b] 3 ) else ([y:=b-a] 4 ; [x:=a-b] 5 ) Equations: VBentry(1) = VBexit(1) VBentry(2) = VBexit(2) ∪ {b-a} VBentry(3) = {a-b} VBentry(4) = VBexit(4) ∪ {b-a} VBentry(5) = {a-b} VBexit(1) = VBentry(2) ∩ VBentry(4) VBexit(2) = VBentry(3) VBexit(3) = ∅ VBexit(4) = VBentry(5) VBexit(5) = ∅ PPA Section 2.1 c F.Nielson & H.Riis Nielson & C.Hankin (May 2005) 28
Example (cont.): if [a>b]1 then ([x:=b-a]2;[y:=a-b]3)else ([y:=b-a]4;[x:=a-b]5) Largest solution: e VBentry(e)VBerit(e) 1 {a-b,b-a} {a-b,b-a} 2 {a-b,b-a} {a-b} 3 {a-b} 0 4 {a-b,b-a} {a-b} 5 {a-b} 0 PPA Section 2.1 C F.Nielson H.Riis Nielson C.Hankin (May 2005) 29
Example (cont.): if [a>b] 1 then ([x:=b-a] 2 ; [y:=a-b] 3 ) else ([y:=b-a] 4 ; [x:=a-b] 5 ) Largest solution: ` VBentry(`) VBexit(`) 1 {a-b, b-a} {a-b, b-a} 2 {a-b, b-a} {a-b} 3 {a-b} ∅ 4 {a-b, b-a} {a-b} 5 {a-b} ∅ PPA Section 2.1 c F.Nielson & H.Riis Nielson & C.Hankin (May 2005) 29
Why largest solution? (while [x>i]do [skip]e);[x:=x+1]e" Equations: VBentry(e) =VBexit(e) VBentr(e) = VBerit(e') 北J no VBentry(e")= {x+1} yes VBexit(e)= VBentry(e)nVBentry(") VBerit(e') VBentry(e) L小 VBerit(e")= 0 After some simplifications:VBexit(e)=VBexit()n{x+1} Two solutions to this equation:{x+1}and 0 PPA Section 2.1 C F.Nielson H.Riis Nielson C.Hankin (May 2005) 30
Why largest solution? (while [x>1] ` do [skip] ` 0 ); [x:=x+1] ` 00 Equations: VBentry(`) = VBexit(`) VBentry(` 0 ) = VBexit(` 0 ) VBentry(` 00) = {x+1} VBexit(`) = VBentry(` 0 ) ∩ VBentry(` 00) VBexit(` 0 ) = VBentry(`) VBexit(` 00) = ∅ [· · ·] ` 00 [· · ·] ` 0 [· · ·] ` ❄ ❄ ❄ ✲ ❄ yes no After some simplifications: VBexit(`) = VBexit(`) ∩ {x+1} Two solutions to this equation: {x+1} and ∅ PPA Section 2.1 c F.Nielson & H.Riis Nielson & C.Hankin (May 2005) 30