Gen and Kill What is the effect of each statement on the set of facts? entry Stmt Gen Kil训 x:=a+b x:=a+b a+b y:=a*b y>a y:=a*b a*b a:=a+l exit a+l, a:=a+l a+b, a*b x:=a+b 18
Gen and Kill • What is the effect of each statement on the set of facts? 18
Computing Available Expressions 0 entry x:=a+b {a+b} y:=a*b {a b,a b} {a+b} y>a a b,a b} {a+b} exit {a+b} a:=a+l 0 x :=a+b {a+b} 19
Computing Available Expressions 19
Terminology A join point is a program point where two branches meet Available expressions is a forward must problem Forward Data flow from in to out Must Property must hold on all paths to the join Dataflow analysis requires facts that summarize all paths to a join point Symbolic execution analyzes each path separately 20
Terminology • A join point is a program point where two branches meet • Available expressions is a forward must problem ➢ Forward = Data flow from in to out ➢ Must = Property must hold on all paths to the join • Dataflow analysis requires facts that summarize all paths to a join point ➢ Symbolic execution analyzes each path separately 20
Data Flow Equations ·Let s be a statement succ(s)={immediate successor statements of s ② pred(s)=immediate predecessor statements of s ③ In(s)=program point just before executing s ④ Out(s)=program point just after executing s In(s)=ns epred(s)Out(s) Out(s)=Gen(s)U(In(s)-Kill(s)) 21
Data Flow Equations • Let s be a statement ① succ(s) = { immediate successor statements of s } ② pred(s) = { immediate predecessor statements of s } ③ In(s) = program point just before executing s ④ Out(s) = program point just after executing s • In(s) = ∩s’ Є pred(s) Out(s’) • Out(s) = Gen(s) ∪ (In(s) - Kill(s)) 21