Page 1 Data-?ow Analysis: Theoretical Foundations - Part 2 Y .N. Srikant Department of Computer Science Indian Institute of Science Bangalore 560 012 NPTEL Course on Compiler Design Y .N. Srikant Theoretical Foundations of DFA Page 2 Data-?ow Analysis: Theoretical Foundations - Part 2 Y .N. Srikant Department of Computer Science Indian Institute of Science Bangalore 560 012 NPTEL Course on Compiler Design Y .N. Srikant Theoretical Foundations of DFA Foundations of Data-?ow Analysis Basic questions to be answered 1 Under what situations is the iterative DFA algorithm correct? 2 How precise is the solution produced by it? 3 Will the algorithm converge? 4 What is the meaning of a “solution”? The above questions can be answered accurately by a DFA framework Further, reusable components of the DFA algorithm can be identi?ed once a framework is de?ned A DFA framework (D;V;^;F) consists of D : A direction of the data?ow, either forward or backward V : A domain of values ^ : A meet operator (V;^) form a semi-lattice F : A family of transfer functions, V! V F includes constant transfer functions for the ENTRY/EXIT nodes as well Y .N. Srikant Theoretical Foundations of DFA Page 3 Data-?ow Analysis: Theoretical Foundations - Part 2 Y .N. Srikant Department of Computer Science Indian Institute of Science Bangalore 560 012 NPTEL Course on Compiler Design Y .N. Srikant Theoretical Foundations of DFA Foundations of Data-?ow Analysis Basic questions to be answered 1 Under what situations is the iterative DFA algorithm correct? 2 How precise is the solution produced by it? 3 Will the algorithm converge? 4 What is the meaning of a “solution”? The above questions can be answered accurately by a DFA framework Further, reusable components of the DFA algorithm can be identi?ed once a framework is de?ned A DFA framework (D;V;^;F) consists of D : A direction of the data?ow, either forward or backward V : A domain of values ^ : A meet operator (V;^) form a semi-lattice F : A family of transfer functions, V! V F includes constant transfer functions for the ENTRY/EXIT nodes as well Y .N. Srikant Theoretical Foundations of DFA Properties of the Iterative DFA Algorithm If the iterative algorithm converges, the result is a solution to the DF equations Proof: If the equations are not satis?ed by the time the loop ends, atleast one of the OUT sets changes and we iterate again If the framework is monotone, then the solution found is the maximum ?xpoint (MFP) of the DF equations An MFP solution is such that in any other solution, values of IN[B] and OUT[B] are the corresponding values of the MFP (i.e., less precise) Proof: We can show by induction that the values of IN[B] and OUT[B] only decrease (in the sense of relation) as the algorithm iterates Y .N. Srikant Theoretical Foundations of DFA Page 4 Data-?ow Analysis: Theoretical Foundations - Part 2 Y .N. Srikant Department of Computer Science Indian Institute of Science Bangalore 560 012 NPTEL Course on Compiler Design Y .N. Srikant Theoretical Foundations of DFA Foundations of Data-?ow Analysis Basic questions to be answered 1 Under what situations is the iterative DFA algorithm correct? 2 How precise is the solution produced by it? 3 Will the algorithm converge? 4 What is the meaning of a “solution”? The above questions can be answered accurately by a DFA framework Further, reusable components of the DFA algorithm can be identi?ed once a framework is de?ned A DFA framework (D;V;^;F) consists of D : A direction of the data?ow, either forward or backward V : A domain of values ^ : A meet operator (V;^) form a semi-lattice F : A family of transfer functions, V! V F includes constant transfer functions for the ENTRY/EXIT nodes as well Y .N. Srikant Theoretical Foundations of DFA Properties of the Iterative DFA Algorithm If the iterative algorithm converges, the result is a solution to the DF equations Proof: If the equations are not satis?ed by the time the loop ends, atleast one of the OUT sets changes and we iterate again If the framework is monotone, then the solution found is the maximum ?xpoint (MFP) of the DF equations An MFP solution is such that in any other solution, values of IN[B] and OUT[B] are the corresponding values of the MFP (i.e., less precise) Proof: We can show by induction that the values of IN[B] and OUT[B] only decrease (in the sense of relation) as the algorithm iterates Y .N. Srikant Theoretical Foundations of DFA Properties of the Iterative DFA Algorithm (2) If the semi-lattice of the framework is monotone and is of ?nite height, then the algorithm is guaranteed to converge Proof: Data?ow values decrease with each iteration Max no. of iterations = height of the lattice no. of nodes in the ?ow graph Y .N. Srikant Theoretical Foundations of DFA Page 5 Data-?ow Analysis: Theoretical Foundations - Part 2 Y .N. Srikant Department of Computer Science Indian Institute of Science Bangalore 560 012 NPTEL Course on Compiler Design Y .N. Srikant Theoretical Foundations of DFA Foundations of Data-?ow Analysis Basic questions to be answered 1 Under what situations is the iterative DFA algorithm correct? 2 How precise is the solution produced by it? 3 Will the algorithm converge? 4 What is the meaning of a “solution”? The above questions can be answered accurately by a DFA framework Further, reusable components of the DFA algorithm can be identi?ed once a framework is de?ned A DFA framework (D;V;^;F) consists of D : A direction of the data?ow, either forward or backward V : A domain of values ^ : A meet operator (V;^) form a semi-lattice F : A family of transfer functions, V! V F includes constant transfer functions for the ENTRY/EXIT nodes as well Y .N. Srikant Theoretical Foundations of DFA Properties of the Iterative DFA Algorithm If the iterative algorithm converges, the result is a solution to the DF equations Proof: If the equations are not satis?ed by the time the loop ends, atleast one of the OUT sets changes and we iterate again If the framework is monotone, then the solution found is the maximum ?xpoint (MFP) of the DF equations An MFP solution is such that in any other solution, values of IN[B] and OUT[B] are the corresponding values of the MFP (i.e., less precise) Proof: We can show by induction that the values of IN[B] and OUT[B] only decrease (in the sense of relation) as the algorithm iterates Y .N. Srikant Theoretical Foundations of DFA Properties of the Iterative DFA Algorithm (2) If the semi-lattice of the framework is monotone and is of ?nite height, then the algorithm is guaranteed to converge Proof: Data?ow values decrease with each iteration Max no. of iterations = height of the lattice no. of nodes in the ?ow graph Y .N. Srikant Theoretical Foundations of DFA Meaning of the Ideal Data-?ow Solution Find all possible execution paths from the start node to the beginning of B (Assuming forward ?ow) Compute the data-?ow value at the end of each path (using composition of transfer functions) and apply the^ operator to these values to ?nd their glb No execution of the program can produce a smaller value for that program point IDEAL[B] = ^ P; a possible execution path from start node to B f P (v init ) Answers greater (in the sense of) than IDEAL are incorrect (one or more execution paths have been ignored) Any value smaller than or equal to IDEAL is conservative, i.e., safe (one or more infeasible paths have been included) Closer the value to IDEAL, more precise it is Y .N. Srikant Theoretical Foundations of DFARead More