0 0 12 views

**Unformatted text preview: **

15 817A Model Checking and Abstract Interpretation Data Flow Analysis Soonho Kong soonhok cs cmu edu 2011 1 26 Computer Science Department Carnegie Mellon University Motivating Example Reaching Definitions In B0 B0 d0 y 3 d1 x 10 d2 y 11 if e Out B0 In B1 In B2 B1 d3 x 1 d4 y 2 d5 z x d6 x 4 Out B1 B2 Out B2 In B3 B3 A definition d reaches a point p if there is a path from the point immediately following d to p Motivating Example Reaching Definitions In B0 B0 d0 y 3 d1 x 10 d2 y 11 if e Out B0 In B1 In B2 B1 d3 x 1 d4 y 2 d5 z x d6 x 4 Out B1 B2 Out B2 In B3 B3 A definition d reaches a point p if there is a path from the point immediately following d to p Motivating Example Reaching Definitions In B0 B0 d0 y 3 d1 x 10 d2 y 11 if e Out B0 d1 d2 In B1 In B2 B1 d3 x 1 d4 y 2 d5 z x d6 x 4 Out B1 B2 Out B2 In B3 B3 A definition d reaches a point p if there is a path from the point immediately following d to p Motivating Example Reaching Definitions In B0 B0 d0 y 3 d1 x 10 d2 y 11 if e Out B0 d1 d2 d1 d2 In B1 B1 d3 x 1 d4 y 2 In B2 d5 z x d6 x 4 Out B1 B2 Out B2 In B3 B3 A definition d reaches a point p if there is a path from the point immediately following d to p Motivating Example Reaching Definitions In B0 B0 d0 y 3 d1 x 10 d2 y 11 if e Out B0 d1 d2 d1 d2 In B1 B1 d3 x 1 d4 y 2 d3 d4 Out B1 In B2 d5 z x d6 x 4 B2 Out B2 In B3 B3 A definition d reaches a point p if there is a path from the point immediately following d to p Motivating Example Reaching Definitions In B0 B0 d0 y 3 d1 x 10 d2 y 11 if e Out B0 d1 d2 d1 d2 In B1 B1 d3 x 1 d4 y 2 d3 d4 Out B1 d1 d2 B2 d5 z x d6 x 4 In B2 Out B2 In B3 B3 A definition d reaches a point p if there is a path from the point immediately following d to p Motivating Example Reaching Definitions In B0 B0 d0 y 3 d1 x 10 d2 y 11 if e Out B0 d1 d2 d1 d2 In B1 B1 d3 x 1 d4 y 2 d3 d4 Out B1 d1 d2 B2 d5 z x d6 x 4 In B2 d2 d5 d6 Out B2 In B3 B3 A definition d reaches a point p if there