中国科学技术大学：《程序分析与程序验证》课程教学资源（课件讲稿）第2章 数据流分析（Nielson等）Principles of Program Analysis - Data Flow Analysis

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

Labels labels(S)is the entire set of labels in the statement S: labels:Stmt→P(Lab) labels([x :a]e)=ep labels([skip])= {3 labels(S1;S2)= labels(S1)U labels(S2) labels(if [b]e then S1 else S2)= eU labels(S1)U labels(S2) labels(while [b]e do s)={e}U labels(S) Example labels([z:=1]1;hi1e[x>0]2d0([z:=z*y]3;[x:=x-1]4)={1,2,3,4} PPA Section 2.1 F.Nielson H.Riis Nielson C.Hankin (May 2005) 6

Labels labels(S) is the entire set of labels in the statement S: labels : Stmt → P(Lab) labels([x := a] ` ) = {`} labels([skip] ` ) = {`} labels(S1; S2) = labels(S1) ∪ labels(S2) labels(if [b] ` then S1 else S2) = {`} ∪ labels(S1) ∪ labels(S2) labels(while [b] ` do S) = {`} ∪ labels(S) Example labels([z:=1] 1 ; while [x>0] 2 do ([z:=z*y] 3 ; [x:=x-1] 4 )) = {1, 2, 3, 4} PPA Section 2.1 c F.Nielson & H.Riis Nielson & C.Hankin (May 2005) 6

Flows and reverse flows flow(S)and flow(S)are representations of how control flows in S: flow,flowR:Stmt→P(Lab×Lab) flow([x :=a])=0 flow([skip]e)=0 flow(S1;S2)=flow(S1)U flow(S2) U{(e,init(S2))ee final(S1)} flow(if [b]e then S1 else S2)=flow(S1)U flow(S2) U{(e,init(S1)),(e,init(S2))} flow(while [b]e do s)=flow(S)U{(e,init(S))} U{(e,)|∈fina1(S)} flow(S)={(,e')(e',e)E flow(S)} PPA Section 2.1 C F.Nielson H.Riis Nielson C.Hankin (May 2005) 7

Flows and reverse flows flow(S) and flowR(S) are representations of how control flows in S: flow, flowR : Stmt → P(Lab × Lab) flow([x := a] ` ) = ∅ flow([skip] ` ) = ∅ flow(S1; S2) = flow(S1) ∪ flow(S2) ∪ {(`, init(S2)) | ` ∈ final(S1)} flow(if [b] ` then S1 else S2) = flow(S1) ∪ flow(S2) ∪ {(`, init(S1)), (`, init(S2))} flow(while [b] ` do S) = flow(S) ∪ {(`, init(S))} ∪ {(` 0 , `) | ` 0 ∈ final(S)} flowR(S) = {(`, `0 ) | (` 0 , `) ∈ flow(S)} PPA Section 2.1 c F.Nielson & H.Riis Nielson & C.Hankin (May 2005) 7

Elementary blocks A statement consists of a set of elementary blocks blocks Stmt P(Blocks) blocks([x :a])={[x:=a]} blocks([skip])={[skip]e} blocks(S1;S2)=blocks(S1)U blocks(S2) blocks(if [b]e then S1 else S2)={[b]e}Ublocks(S1)U blocks(S2) blocks(while [b]t do s)={[b]tU blocks(S) A statement s is label consistent if and only if any two elementary statements [S1]and [S2]with the same label in S are equal:S1=S2 A statement where all labels are unique is automatically label consistent PPA Section 2.1 C F.Nielson H.Riis Nielson C.Hankin (May 2005) 8

Elementary blocks A statement consists of a set of elementary blocks blocks : Stmt → P(Blocks) blocks([x := a] ` ) = {[x := a] ` } blocks([skip] ` ) = {[skip] ` } blocks(S1; S2) = blocks(S1) ∪ blocks(S2) blocks(if [b] ` then S1 else S2) = {[b] ` } ∪ blocks(S1) ∪ blocks(S2) blocks(while [b] ` do S) = {[b] ` } ∪ blocks(S) A statement S is label consistent if and only if any two elementary statements [S1] ` and [S2] ` with the same label in S are equal: S1 = S2 A statement where all labels are unique is automatically label consistent PPA Section 2.1 c F.Nielson & H.Riis Nielson & C.Hankin (May 2005) 8

Intraprocedural Analysis Classical analyses: Available Expressions Analysis Reaching Definitions Analysis Very Busy Expressions Analysis Live Variables Analysis Derived analysis: Use-Definition and Definition-Use Analysis PPA Section 2.1 C F.Nielson H.Riis Nielson C.Hankin (May 2005) 9

Intraprocedural Analysis Classical analyses: • Available Expressions Analysis • Reaching Definitions Analysis • Very Busy Expressions Analysis • Live Variables Analysis Derived analysis: • Use-Definition and Definition-Use Analysis PPA Section 2.1 c F.Nielson & H.Riis Nielson & C.Hankin (May 2005) 9

Available Expressions Analysis The aim of the Available Expressions Analysis is to determine For each program point,which expressions must have already been computed,and not later modified,on all paths to the pro- gram point. Example: point of interest 业 [x:-a+b]1;[y:=a*b]2;while[y>a+b]3do([a:=a+1]4;[x:=-a+b]5) The analysis enables a transformation into [x:=a+b]1;[y:=a*b]2;while[y>x]3do([a:=a+1]4;[x:=a+b]5) PPA Section 2.1 F.Nielson H.Riis Nielson C.Hankin (May 2005) 10

Available Expressions Analysis The aim of the Available Expressions Analysis is to determine For each program point, which expressions must have already been computed, and not later modified, on all paths to the pro￾gram point. Example: point of interest ⇓ [x:= a+b ] 1 ; [y:=a*b] 2 ; while [y> a+b ] 3 do ([a:=a+1] 4 ; [x:= a+b ] 5 ) The analysis enables a transformation into [x:= a+b] 1 ; [y:=a*b] 2 ; while [y> x ] 3 do ([a:=a+1] 4 ; [x:= a+b] 5 ) PPA Section 2.1 c F.Nielson & H.Riis Nielson & C.Hankin (May 2005) 10