15-817A Model Checking and Abstract InterpretationData Flow AnalysisSoonho [email protected]/1/26Computer Science DepartmentCarnegie Mellon UniversityMotivating Example: Reaching DefinitionsA definition d reaches a point p if there is a path from the point immediately following d to pd0: y = 3d1: x = 10d2: y = 11 if ed5: z = xd6: x = 4d3: x = 1d4: y = 2B0B1B2In[B0]In[B1]In[B2]Out[B2]Out[B1]In[B3]B3Out[B0]Motivating Example: Reaching DefinitionsA definition d reaches a point p if there is a path from the point immediately following d to pd0: y = 3d1: x = 10d2: y = 11 if ed5: z = xd6: x = 4d3: x = 1d4: y = 2B0B1B2In[B0]In[B1]In[B2]Out[B2]Out[B1]In[B3]B3Out[B0]{ }Motivating Example: Reaching DefinitionsA definition d reaches a point p if there is a path from the point immediately following d to pd0: y = 3d1: x = 10d2: y = 11 if ed5: z = xd6: x = 4d3: x = 1d4: y = 2B0B1B2In[B0]In[B1]In[B2]Out[B2]Out[B1]In[B3]B3Out[B0]{ }{d1,d2}Motivating Example: Reaching DefinitionsA definition d reaches a point p if there is a path from the point immediately following d to pd0: y = 3d1: x = 10d2: y = 11 if ed5: z = xd6: x = 4d3: x = 1d4: y = 2B0B1B2In[B0]In[B1]In[B2]Out[B2]Out[B1]In[B3]B3Out[B0]{ }{d1,d2}{d1,d2}Motivating Example: Reaching DefinitionsA definition d reaches a point p if there is a path from the point immediately following d to pd0: y = 3d1: x = 10d2: y = 11 if ed5: z = xd6: x = 4d3: x = 1d4: y = 2B0B1B2In[B0]In[B1]In[B2]Out[B2]Out[B1]In[B3]B3Out[B0]{ }{d1,d2}{d1,d2}{d3,d4}Motivating Example: Reaching DefinitionsA definition d reaches a point p if there is a path from the point immediately following d to pd0: y = 3d1: x = 10d2: y = 11 if ed5: z = xd6: x = 4d3: x = 1d4: y = 2B0B1B2In[B0]In[B1]In[B2]Out[B2]Out[B1]In[B3]B3Out[B0]{ }{d1,d2}{d1,d2}{d3,d4}{d1,d2}Motivating Example: Reaching DefinitionsA definition d reaches a point p if there is a path from the point immediately following d to pd0: y = 3d1: x = 10d2: y = 11 if ed5: z = xd6: x = 4d3: x = 1d4: y = 2B0B1B2In[B0]In[B1]In[B2]Out[B2]Out[B1]In[B3]B3Out[B0]{ }{d1,d2}{d1,d2}{d3,d4}{d1,d2}{d2,d5,d6}Motivating Example: Reaching DefinitionsA definition d reaches a point p if there is a path from the point immediately following d to pd0: y = 3d1: x = 10d2: y = 11 if ed5: z = xd6: x = 4d3: x = 1d4: y = 2B0B1B2In[B0]In[B1]In[B2]Out[B2]Out[B1]In[B3]B3Out[B0]{d1,d2}{d2,d5,d6}{ }{d1,d2} {d1,d2}{d3,d4}{d2,d3,d4,d5,d6}Transfer Function (statement-level)d0: y = 3s0In[s0]Out[s0]What is the relation between In[s0] and Out[s0]?fd(x)=gend∪ (x − killd)Out[s0]=fd0(In[s0])is definition generated:gend= {d}gendwhereis set of all other defs to x in the rest of programkilldTransfer Function (statement-level) d0: y = 3d1: x = 10d2: y = 11 if ed5: z = xd6: x = 4d3: x = 1d4: y = 2B0B1B2In[B0]In[B1]In[B2]Out[B2]Out[B1]In[B3]B3Out[B0]gend0= {d0}killd0= {d2,d4}fd0(x)=gend0∪ (x − killd0)= {d0} ∪ (x − {d2,d4})Transfer Function (block-level)What is the relation between In[B0] and Out[B0]?d0: y = 3d1: x = 10d2: y = 11 if eB0In[B0]Out[B0]Out[s0]=fB(In[s0])fB(x)=fdn◦ ··· ◦ fd0(x)d0: y = 3d1: x = 10d2: y = 11 if ed5: z = xd6: x = 4d3: x = 1d4: y = 2B0B1B2In[B0]In[B1]In[B2]Out[B2]Out[B1]In[B3]B3Out[B0]Transfer Function (block-level)Out[B0]={d1,d2} ∪ (In[B0] − {d3,d4,d6,d0})Out[B1]={d3,d4} ∪ (In[B1] − {d0,d1,d2,d6})Out[B2]={d5,d6} ∪ (In[B2] − {d1,d3})B0In[B0]Out[B0]Meet Operator d5: z = xd6: x = 4d3: x = 1d4: y = 2B1B2In[B1]In[B2]Out[B2]Out[B1]In[B3]B3What is the relation between Out[B1], Out[B2], and Out[B0]?In[B]=�B�:pred(B)Out[B�]Meet Operator d5: z = xd6: x = 4d3: x = 1d4: y = 2B1B2In[B1]In[B2]Out[B2]Out[B1]In[B3]B3What is the relation between Out[B1], Out[B2], and Out[B0]?In[B]=�B�:pred(B)Out[B�]“A definition d reaches a point p if there is a path from the point immediately following d to p”Why ?�Meet Operator d5: z = xd6: x = 4d3: x = 1d4: y = 2B1B2In[B1]In[B2]Out[B2]Out[B1]In[B3]B3What is the relation between Out[B1], Out[B2], and Out[B0]?In[B]=�B�:pred(B)Out[B�]“A definition d reaches a point p if for all path from the point immediately following d to p”What if “MUST reach definition”?In[B]=�B�:pred(B)Out[B�]Meet Operator d5: z = xd6: x = 4d3: x = 1d4: y = 2B1B2In[B1]In[B2]Out[B2]Out[B1]In[B3]B3What is the relation between Out[B1], Out[B2], and Out[B0]?In[B]=�B�:pred(B)Out[B�]In[B]=�B�:pred(B)Out[B�]In general�and depends on the problem.d0: y = 3d1: x = 10d2: y = 11 if ed5: z = xd6: x = 4d3: x = 1d4: y = 2B0B1B2In[B0]In[B1]In[B2]Out[B2]Out[B1]In[B3]B3Out[B0]B0In[B0]Out[B0]Meet Operator In[B1]=Out[B0]In[B2]=Out[B0]In[B3]=Out[B1] ∪ Out[B2]d0: y = 3d1: x = 10d2: y = 11 if ed5: z = xd6: x = 4d3: x = 1d4: y = 2B0B1B2In[B0]In[B1]In[B2]Out[B2]Out[B1]In[B3]B3Out[B0]B0In[B0]Out[B0]Boundary ConditionIn[B1]=Out[B0]In[B2]=Out[B0]In[B3]=Out[B1] ∪ Out[B2]Out[B0]={d1,d2} ∪ (In[B0] − {d3,d4,d6,d0})Out[B1]={d3,d4} ∪ (In[B1] − {d0,d1,d2,d6})Out[B2]={d5,d6} ∪ (In[B2] − {d1,d3})So far, we have...d0: y = 3d1: x = 10d2: y = 11 if ed5: z = xd6: x = 4d3: x = 1d4: y = 2B0B1B2In[B0]In[B1]In[B2]Out[B2]Out[B1]In[B3]B3Out[B0]B0In[B0]Out[B0]Boundary ConditionWhat In[B0] should be ?In[B0]={}It depends on the problem.Extracting ConstraintsIn[B1]=Out[B0]In[B2]=Out[B0]In[B3]=Out[B1] ∪ Out[B2]Out[B0]={d1,d2} ∪ (In[B0] − {d3,d4,d6,d0})Out[B1]={d3,d4} ∪ (In[B1] − {d0,d1,d2,d6})Out[B2]={d5,d6} ∪ (In[B2] − {d1,d3})In[B0]={} d0: y = 3d1: x = 10d2: y = 11 if ed5: z = xd6: x = 4d3: x = 1d4: y = 2B0B1B2In[B0]In[B1]In[B2]Out[B2]Out[B1]In[B3]B3Out[B0]Transfer FunctionBoundary ConditionMeet OperatorSolving ConstraintsIn[B1]=Out[B0]In[B2]=Out[B0]In[B3]=Out[B1] ∪ Out[B2]Out[B0]={d1,d2} ∪ (In[B0] − {d3,d4,d6,d0})Out[B1]={d3,d4} ∪ (In[B1] − {d0,d1,d2,d6})Out[B2]={d5,d6} ∪ (In[B2] − {d1,d3})In[B0]={}Transfer FunctionBoundary ConditionMeet OperatorGoal: Find satisfying the above constraints.(In[B0],In[B1],In[B2],In[B3],Out[B0],Out[B1],Out[B2])Solving ConstraintsIn[B1]=Out[B0]In[B2]=Out[B0]In[B3]=Out[B1] ∪ Out[B2]Out[B0]={d1,d2} ∪ (In[B0] − {d3,d4,d6,d0})Out[B1]={d3,d4} ∪ (In[B1] − {d0,d1,d2,d6})Out[B2]={d5,d6} ∪ (In[B2] − {d1,d3})In[B0]={}Transfer FunctionBoundary ConditionMeet OperatorF (In[B0],In[B1],In[B2],In[B3],Out[B0],Out[B1],Out[B2]) =(In[B0],In[B1],In[B2],In[B3],Out[B0],Out[B1],Out[B2])Goal: Find satisfying the above