About These Slides

(1)

Uday Khedker

(www.cse.iitb.ac.in/˜uday)

Department of Computer Science and Engineering, Indian Institute of Technology, Bombay

Dec 2019

(2)

About These Slides

(3)

These slides constitute the lecture notes for CS618 Program Analysis course at IIT Bombay and have been made available as teaching material accompanying the book:

• Uday Khedker, Amitabha Sanyal, and Bageshri Karkare. Data Flow Analysis: Theory and Practice. CRC Press (Taylor and Francis Group).

2009.

(Indian edition published by Ane Books in 2013)

Apart from the above book, some slides are based on the material from the following book

• M. S. Hecht. Flow Analysis of Computer Programs. Elsevier North-Holland Inc. 1977.

These slides are being made available under GNU FDL v1.2 or later purely for academic or research use.

(4)

n1

a= 1 b= 2 c=a+b

n1

n2 c=a+b d=a∗b n2

n3

d=c−1 a= 2 b= 1 c=a+b

n3

Dec 2019 IIT Bombay

(5)

n1

a= 1 b= 2 c=a+b

n1

n2 c=a+b d=a∗b n2

n3

d=c−1 a= 2 b= 1 c=a+b

n3

Execution Sequence ha, b, c, di

n1

hud,ud,ud,udi ^IN

(6)

n1

a= 1 b= 2 c=a+b

n1

n2 c=a+b d=a∗b n2

n3

d=c−1 a= 2 b= 1 c=a+b

n3

n1

hud,ud,ud,udi ^IN h1,2,3,udi ^OUT

Dec 2019 IIT Bombay

(7)

n1

a= 1 b= 2 c=a+b

n1

n2 c=a+b d=a∗b n2

n3

d=c−1 a= 2 b= 1 c=a+b

n3

n1

n2

h1,2,3,2i

(8)

n1

a= 1 b= 2 c=a+b

n1

n2 c=a+b d=a∗b n2

n3

d=c−1 a= 2 b= 1 c=a+b

n3

n1

n2

h1,2,3,2i

n3

h2,1,3,2i

Dec 2019 IIT Bombay

(9)

n1

a= 1 b= 2 c=a+b

n1

n2 c=a+b d=a∗b n2

n3

d=c−1 a= 2 b= 1 c=a+b

n3

n1

n2

h1,2,3,2i

n3

h2,1,3,2i

n2

h2,1,3,2i

(10)

n1

a= 1 b= 2 c=a+b

n1

n2 c=a+b d=a∗b n2

n3

d=c−1 a= 2 b= 1 c=a+b

n3

n1

n2

h1,2,3,2i

n3

h2,1,3,2i

n2

h2,1,3,2i

n3

h2,1,3,2i

Dec 2019 IIT Bombay

(11)

n1

a= 1 b= 2 c=a+b

n1

n2 c=a+b d=a∗b n2

n3

d=c−1 a= 2 b= 1 c=a+b

n3

n1

n2

h1,2,3,2i

n3

h2,1,3,2i

n2

h2,1,3,2i

n3

h2,1,3,2i

n2

h2,1,3,2i

(12)

n1

a= 1 b= 2 c=a+b

n1

n2 c=a+b d=a∗b n2

n3

d=c−1 a= 2 b= 1 c=a+b

n3

n1

n2

h1,2,3,2i

n3

h2,1,3,2i

n2

h2,1,3,2i

n3

h2,1,3,2i

n2

h2,1,3,2i

n3

h2,1,3,2i

. . .

Dec 2019 IIT Bombay

(13)

n1

a= 1 b= 2 c=a+b

n1

n2 c=a+b d=a∗b n2

n3

d=c−1 a= 2 b= 1 c=a+b

n3

n1

n2

h1,2,3,2i

n3

h2,1,3,2i

n2

h2,1,3,2i

n3

h2,1,3,2i

n2

h2,1,3,2i

n3

h2,1,3,2i

. . .

Summary Values h∅,∅,∅,∅i

No value of any variable has been seen, hence∅

This choice is based on the assumption that the execution paths are so set up (using conditions) that no variable is read before it is defined

If variables are assumed to have some uninitialized value, thenIcan be used asBIvalue

(14)

n1

a= 1 b= 2 c=a+b

n1

n2 c=a+b d=a∗b n2

n3

d=c−1 a= 2 b= 1 c=a+b

n3

n1

n2

h1,2,3,2i

n3

h2,1,3,2i

n2

h2,1,3,2i

n3

h2,1,3,2i

n2

h2,1,3,2i

n3

h2,1,3,2i

. . .

h{1},{2},{3},∅i

Dec 2019 IIT Bombay

(15)

n1

a= 1 b= 2 c=a+b

n1

n2 c=a+b d=a∗b n2

n3

d=c−1 a= 2 b= 1 c=a+b

n3

n1

n2

h1,2,3,2i

n3

h2,1,3,2i

n2

h2,1,3,2i

n3

h2,1,3,2i

n2

h2,1,3,2i

n3

h2,1,3,2i

. . .

h{1},{2},{3},∅i

hI,I,{3},{2}i hI,I,{3},{2}i

We overapproximate {1,2}toIimplying that ‘multiple values’

mean ‘any value’

(16)

n1

a= 1 b= 2 c=a+b

n1

n2 c=a+b d=a∗b n2

n3

d=c−1 a= 2 b= 1 c=a+b

n3

n1

n2

h1,2,3,2i

n3

h2,1,3,2i

n2

h2,1,3,2i

n3

h2,1,3,2i

n2

h2,1,3,2i

n3

h2,1,3,2i

. . .

h{1},{2},{3},∅i

hI,I,{3},{2}i hI,I,{3},{2}i

Dec 2019 IIT Bombay

(17)

n1

a= 1 b= 2 c=a+b

n1

n2 c=a+b d=a∗b n2

n3

d=c−1 a= 2 b= 1 c=a+b

n3

n1

n2

h1,2,3,2i

n3

h2,1,3,2i

n2

h2,1,3,2i

n3

h2,1,3,2i

n2

h2,1,3,2i

n3

h2,1,3,2i

. . .

h{1},{2},{3},∅i

hI,I,{3},{2}i hI,I,{3},{2}i

hI,I,{3},{2}i

(18)

n1

a= 1 b= 2 c=a+b

n1

n2 c=a+b d=a∗b n2

n3

d=c−1 a= 2 b= 1 c=a+b

n3

n1

n2

h1,2,3,2i

n3

h2,1,3,2i

n2

h2,1,3,2i

n3

h2,1,3,2i

n2

h2,1,3,2i

n3

h2,1,3,2i

. . .

h{1},{2},{3},∅i

hI,I,{3},{2}i hI,I,{3},{2}i

hI,I,{3},{2}i

h{2},{1},{3},{2}i

Dec 2019 IIT Bombay

(19)

n1

a= 1 b= 2 c=a+b

n1

n2 c=a+b d=a∗b n2

n3

d=c−1 a= 2 b= 1 c=a+b

n3

h{1},{2},{3},∅i

hI,I,{3},{2}i hI,I,{3},{2}i

hI,I,{3},{2}i

h{2},{1},{3},{2}i

Desired Solution

(20)

• Tuples of the formhη₁, η₂, . . . , η_ki Or sets of pairs (vi, η_i) or (vi7→η_i) where η_i is the data flow value fori^th variable

Unlike live variables analysis, valueη_i is not 0 or 1 (i.e. true or false).

Instead, it is one of the following:

◦ ∅indicating that no values is known forvi

◦ Iindicating that variablevi could have multiple values

◦ Set{c1}if the value ofvi is known to bec1at compile time

Dec 2019 IIT Bombay

(21)

Entities

• In (simple) live variables analysis, data flow values of different entities are independent

Liveness of variablebdoes not depend on that of any other variable

• Given a statementa=b∗c, can the constantness of abe determined independently of the constantness ofbandc?

No

This is similar to strong liveness analysis

(22)

• Merging the pairsa7→s1 anda7→s2

a7→s1 a7→s2

a7→s2

⊓ a7→ ∅ a7→I a7→ {c1} a7→ ∅ a7→ ∅ a7→I a7→ {c1} a7→I a7→I a7→I a7→I a7→ {c2} a7→ {c2} a7→I Ifc1=c2 a7→ {c1}

Otherwisea7→I

• The merge (or technically, the “meet”) operator is neither∩nor∪ What are its properties?

Dec 2019 IIT Bombay

(23)

• Flow function fora=b∗c

a=b∗c b7→s1 c7→s2

mult b7→ ∅ b7→I b7→ {c1} c7→ ∅ a7→ ∅ a7→I a7→ ∅ c7→I a7→I a7→I a7→I c7→ {c2} a7→ ∅ a7→I a7→ {c1∗c2}

• This cannot be expressed in the form

fn(X) = Genn∪(X−Killn)

where Gennand Killn are constant effects of blockn

(24)

n1

a= 1 b= 2 c=a+b

n1

n2 c=a+b d=a∗b n2

n3

d=c−1 a= 2 b= 1 c=a+b

n3

Dec 2019 IIT Bombay

(25)

n1

a= 1 b= 2 c=a+b

n1

n2 c=a+b d=a∗b n2

n3

d=c−1 a= 2 b= 1 c=a+b

n3

Iteration

#1 h∅,∅,∅,∅i

h1,2,3,∅i

h1,2,3,∅i h1,2,3,2i

h1,2,3,2i

h2,1,3,2i

For convenience, we omit the braces for

singleton sets

(26)

n1

a= 1 b= 2 c=a+b

n1

n2 c=a+b d=a∗b n2

n3

d=c−1 a= 2 b= 1 c=a+b

n3

Iteration

#1 h∅,∅,∅,∅i

h1,2,3,∅i

h1,2,3,∅i h1,2,3,2i

h1,2,3,2i

h2,1,3,2i

Iteration

#2 h∅,∅,∅,∅i

h1,2,3,∅i

hI,I,3,2i hI,I,I,Ii

hI,I,I,Ii

h2,1,3,Ii

Dec 2019 IIT Bombay

(27)

n1

a= 1 b= 2 c=a+b

n1

n2 c=a+b d=a∗b n2

n3

d=c−1 a= 2 b= 1 c=a+b

n3

Iteration

#1 h∅,∅,∅,∅i

h1,2,3,∅i

h1,2,3,∅i h1,2,3,2i

h1,2,3,2i

h2,1,3,2i

Iteration

#2 h∅,∅,∅,∅i

h1,2,3,∅i

hI,I,3,2i hI,I,I,Ii

hI,I,I,Ii

h2,1,3,Ii

Iteration

#3 h∅,∅,∅,∅i

h1,2,3,∅i

hI,I,3,Ii hI,I,I,Ii

hI,I,I,Ii

h2,1,3,Ii

(28)

n1

a= 1 b= 2 c=a+b

n1

n2 c=a+b d=a∗b n2

n3

d=c−1 a= 2 b= 1 c=a+b

n3

Desired solution h∅,∅,∅,∅i

h1,2,3,∅i

hI,I,3,2i hI,I,3,2i

hI,I,3,2i

h2,1,3,2i Iteration

#1 h∅,∅,∅,∅i

h1,2,3,∅i

h1,2,3,∅i h1,2,3,2i

h1,2,3,2i

h2,1,3,2i

Iteration

#2 h∅,∅,∅,∅i

h1,2,3,∅i

hI,I,3,2i hI,I,I,Ii

hI,I,I,Ii

h2,1,3,Ii

Iteration

#3 h∅,∅,∅,∅i

h1,2,3,∅i

hI,I,3,Ii hI,I,I,Ii

hI,I,I,Ii

h2,1,3,Ii

Dec 2019 IIT Bombay

(29)

n1

a= 1 b= 2 c=a+b

n1

n2 c=a+b d=a∗b n2

n3

d=c−1 a= 2 b= 1 c=a+b

n3

Desired solution h∅,∅,∅,∅i

h1,2,3,∅i

hI,I,3,2i hI,I,3,2i

hI,I,3,2i

h2,1,3,2i Iteration

#1 h∅,∅,∅,∅i

h1,2,3,∅i

h1,2,3,∅i h1,2,3,2i

h1,2,3,2i

h2,1,3,2i

Iteration

#2 h∅,∅,∅,∅i

h1,2,3,∅i

hI,I,3,2i hI,I,I,Ii

hI,I,I,Ii

h2,1,3,Ii

Iteration

#3 h∅,∅,∅,∅i

h1,2,3,∅i

hI,I,3,Ii hI,I,I,Ii

hI,I,I,Ii

h2,1,3,Ii hI,I,3,Ii hI,I,I,Ii

hI,I,I,Ii

hI,I,3,2i hI,I,3,2i

hI,I,3,2i

(30)

(⊤)b

∅

−∞

. . .

₋₂ ₋₁ ₀ ₁ ₂

. . .

∞

(⊥)b I

b

⊓ hv,⊤i hvb ,⊥ib hv,c1i hv,⊤ib hv,⊤i hvb ,⊥ib hv,c1i hv,⊥ib hv,⊥i hvb ,⊥ib hv,⊥ib

hv,c2i hv,c2i hv,⊥ib Ifc1=c2thenhv,c1ielsehv,⊥ib

Dec 2019 IIT Bombay

(31)

• Inn/Outn values are mappingsVar→Lb: Inn,Outn∈Var→bL

• Overall latticeL is a set of mappingsVar→bL: L=Var→Lb

• ⊓andb⊓get defined by⊑and⊑b

◦ Partial order is restricted to data flow values of the same variable Data flow values of different variables are incomparable

(x,v1)⊑(y,v2) ⇔ x=y∧v1⊑vb 2

OR x 7→v1⊑y 7→v2 ⇔ x=y∧v1⊑vb 2

◦ For meet operation, we assume thatX is a total function Partial functions are made total by using⊤valueb

X⊓Y =

(x,v1⊓vb 2)|(x,v1)∈X,(x,v2)∈Y OR X⊓Y =

x7→v1⊓vb 2|x 7→v1∈X,x7→v2∈Y

(32)

Accessing and manipulating a mappingX ⊆A→B

• X(a) denotes the image ofa∈A X(a)∈B

• X[a7→v] changes the image ofainX tov

X[a7→v] = (X− {(a,u)|u∈B}) ∪ {(a,v)}

Dec 2019 IIT Bombay

(33)

Inn =





BI= y,⊤b

|y ∈Var n=Start

p∈pred(n)

Outp otherwise

Outn = fn(Inn)

fn(X) =











X[y 7→c] nisy =c,y ∈Var,c∈Const Xh

y 7→⊥bi

nisinput(y),y ∈var X[y 7→X(z)] nisy =z,y ∈Var,z ∈Var X[y 7→eval(e,X)] nisy =e,y ∈Var,e∈Expr

X otherwise

(34)

Inn =





BI= y,⊤b

|y ∈Var n=Start

p∈pred(n)

Outp otherwise

Outn = fn(Inn)

fn(X) =











X[y 7→c] nisy =c,y ∈Var,c∈Const Xh

y 7→⊥bi

nisinput(y),y ∈var X[y 7→X(z)] nisy =z,y ∈Var,z ∈Var X[y 7→eval(e,X)] nisy =e,y ∈Var,e∈Expr

X otherwise

eval(e,X) =









⊥b a∈Opd(e)∩Var,X(a) =⊥b

⊤b a∈Opd(e)∩Var,X(a) =⊤b

−X(a) eis −a X(a)⊕X(b) eis a⊕b

Dec 2019 IIT Bombay

(35)

• Construct a CFG corresponding to this program and perform constant propagation

int f ()

{ int a, b, c, d;

for (i=0; i<n; i++) { if (i==m+3)

a=b+1;

else if(i==m+2) b=c+1;

else if(i==m+1) c=d+1;

else if(i==m) d=2;

} }

• Repeat the analysis assumingBIto be⊥b for all variables

(36)

n1

a= 1 b= 2 c=a+b

n1

n2 c=a+b d=a∗b n2

n3

d=c−1 a= 2 b= 1 c=a+b

n3

Dec 2019 IIT Bombay

(37)

n1

a= 1 b= 2 c=a+b

n1

n2 c=a+b d=a∗b n2

n3

d=c−1 a= 2 b= 1 c=a+b

n3

a= 1,b= 2

• x=h1,2,3,⊤ib (AlongOutn1→Inn2)

(38)

n1

a= 1 b= 2 c=a+b

n1

n2 c=a+b d=a∗b n2

n3

d=c−1 a= 2 b= 1 c=a+b

n3

a= 1,b= 2

a= 2,b= 1

• y =h2,1,3,2i(AlongOutn3→Inn2)

Dec 2019 IIT Bombay

(39)

n1

a= 1 b= 2 c=a+b

n1

n2 c=a+b d=a∗b n2

n3

d=c−1 a= 2 b= 1 c=a+b

n3

a= 1,b= 2

a= 2,b= 1

• Function application for blockn2before merging f(x)⊓f(y) = f(h1,2,3,⊤i)b ⊓f(h2,1,3,2i)

= h1,2,3,2i ⊓ h2,1,3,2i

= h⊥,b ⊥,b 3,2i

(40)

n1

a= 1 b= 2 c=a+b

n1

n2 c=a+b d=a∗b n2

n3

d=c−1 a= 2 b= 1 c=a+b

n3

a= 1,b= 2

a= 2,b= 1

= h1,2,3,2i ⊓ h2,1,3,2i

= h⊥,b ⊥,b 3,2i

• Function application for blockn2after merging f(x⊓y) = f(h1,2,3,⊤i ⊓ h2,b 1,3,2i)

= f(h⊥,b ⊥,b 3,2i)

= h⊥,b ⊥,b ⊥,b ⊥ib

Dec 2019 IIT Bombay

(41)

n1

a= 1 b= 2 c=a+b

n1

n2 c=a+b d=a∗b n2

n3

d=c−1 a= 2 b= 1 c=a+b

n3

a= 1,b= 2

a= 2,b= 1

= h1,2,3,2i ⊓ h2,1,3,2i

= h⊥,b ⊥,b 3,2i

• Function application for blockn2after merging f(x⊓y) = f(h1,2,3,⊤i ⊓ h2,b 1,3,2i)

= f(h⊥,b ⊥,b 3,2i)

= h⊥,b ⊥,b ⊥,b ⊥ib

• f(x⊓y)⊏f(x)⊓f(y)

(42)

a= 1 b= 2

a= 2 b= 1

c=a+b

Dec 2019 IIT Bombay

(43)

a= 1 b= 2

a= 2 b= 1

c=a+b

a= 1 a= 2 b= 1 b= 2 Possible combinations due to merging

(44)

a= 1 b= 2

a= 2 b= 1

c=a+b

c=a+b= 3

• Correct combination.

Dec 2019 IIT Bombay

(45)

a= 1 b= 2

a= 2 b= 1

c=a+b

c=a+b= 3

• Correct combination.

(46)

a= 1 b= 2

a= 2 b= 1

c=a+b

c=a+b= 2

• Wrong combination.

• Mutually exclusive information.

• No execution path along which this information holds.

Dec 2019 IIT Bombay

(47)

a= 1 b= 2

a= 2 b= 1

c=a+b

c=a+b= 4

• Wrong combination.

• Mutually exclusive information.

• No execution path along which this information holds.