Principles of Program Analysis: Data Flow Analysis Transparencies based on Chapter 2 of the book:Flemming Nielson, Hanne Riis Nielson and Chris Hankin:Principles of Program Analysis. Springer Verlag 2005.CFlemming Nielson Hanne Riis Nielson Chris Hankin. PPA Chapter 2 C F.Nielson H.Riis Nielson C.Hankin (May 2005) 1
Principles of Program Analysis: Data Flow Analysis Transparencies based on Chapter 2 of the book: Flemming Nielson, Hanne Riis Nielson and Chris Hankin: Principles of Program Analysis. Springer Verlag 2005. c Flemming Nielson & Hanne Riis Nielson & Chris Hankin. PPA Chapter 2 c F.Nielson & H.Riis Nielson & C.Hankin (May 2005) 1
Example Language Syntax of While-programs a ::xn a1 Opa a2 b ::=true false not b b1 opb 62 a1 opr a2 S::=[x :a][skip]e S1;S2 if [b]t then S1 else S2 while [b]e do S Example:[z:=1]1;while [x>0]2 do ([z:=z*y]3;[x:=x-1]4) Abstract syntax-parentheses are inserted to disambiguate the syntax PPA Section 2.1 C)F.Nielson H.Riis Nielson C.Hankin (May 2005) 2
Example Language Syntax of While-programs a ::= x | n | a1 opa a2 b ::= true | false | not b | b1 opb b2 | a1 opr a2 S ::= [x := a] ` | [skip] ` | S1; S2 | if [b] ` then S1 else S2 | while [b] ` do S Example: [z:=1] 1; while [x>0] 2 do ([z:=z*y] 3; [x:=x-1] 4) Abstract syntax – parentheses are inserted to disambiguate the syntax PPA Section 2.1 c F.Nielson & H.Riis Nielson & C.Hankin (May 2005) 2
Building an "Abstract Flowchart'' Example:[z:=1]1;while [x>0]2 do ([z:=z*y]3;[x:=x-1]4) init(..)=1 [z:=1]1 fina1()={2} no abe1s()={1,2,3,4} [x>0]2 yes fow()={(1,2),(2,3), [z:=z*y]3 (3,4),(4,2)} f1ow尺(.…)={(2,1)，(2,4)， [x:=x-14 (3,2),(4,3)} PPA Section 2.1 C F.Nielson H.Riis Nielson C.Hankin (May 2005) 3
Building an “Abstract Flowchart” Example: [z:=1] 1; while [x>0] 2 do ([z:=z*y] 3; [x:=x-1] 4) init(· · ·) = 1 final(· · ·) = {2} labels(· · ·) = {1, 2, 3, 4} flow(· · ·) = {(1, 2), (2, 3), (3, 4), (4, 2)} flowR(· · ·) = {(2, 1), (2, 4), (3, 2), (4, 3)} [x:=x-1] 4 [z:=z*y] 3 [x>0] 2 [z:=1] 1 ❄ ❄ ❄ ✲ ❄ ❄ yes no PPA Section 2.1 c F.Nielson & H.Riis Nielson & C.Hankin (May 2005) 3
Initial labels init(S)is the label of the first elementary block of S: init:Stmt→Lab init([a :=a])=e init([skip]e)= init(S1;S2)= :init(S1) init(if []e then S1 else S2) = init(while [b]t do s)=e Example: init([z:=1];whi1e[x>0]2do([z:=z*y]3:[x:=x-1]4)=1 PPA Section 2.1 F.Nielson H.Riis Nielson C.Hankin (May 2005) 4
Initial labels init(S) is the label of the first elementary block of S: init : Stmt → Lab init([x := a] ` ) = ` init([skip] ` ) = ` init(S1; S2) = init(S1) init(if [b] ` then S1 else S2) = ` init(while [b] ` do S) = ` Example: init([z:=1] 1 ; while [x>0] 2 do ([z:=z*y] 3 ; [x:=x-1] 4 )) = 1 PPA Section 2.1 c F.Nielson & H.Riis Nielson & C.Hankin (May 2005) 4
Final labels final(S)is the set of labels of the last elementary blocks of S: fina/:Stmt→P(Lab) final([a :a]e)-ep final([skip])= {3 final(S1;S2)=final(S2) final(if [b]e then S1 else S2)=final(S1)U final(S2) final(while [o]e do s)={e} Example: fina1([z:=1]1;hi1e[x>0]2do([z:=z*y]3:[x:=x-1]4)={2} PPA Section 2.1 F.Nielson H.Riis Nielson C.Hankin (May 2005) 5
Final labels final(S) is the set of labels of the last elementary blocks of S: final : Stmt → P(Lab) final([x := a] ` ) = {`} final([skip] ` ) = {`} final(S1; S2) = final(S2) final(if [b] ` then S1 else S2) = final(S1) ∪ final(S2) final(while [b] ` do S) = {`} Example: final([z:=1] 1 ; while [x>0] 2 do ([z:=z*y] 3 ; [x:=x-1] 4 )) = {2} PPA Section 2.1 c F.Nielson & H.Riis Nielson & C.Hankin (May 2005) 5