A Framework for Tracking Branch Conditions

An operational data flow analysis framework for tracking controlling expressions of conditional branches is defined in this work. The framework is based on control flow graphs and applies to various procedural languages. In this framework, environments assigned to edges and nodes of control flow graphs are basically conjunctions of certain predicate formulas. These formulas include: atomic constituents of controlling expressions of program branches and their negations; equalities originating from program assignments and their negations; equivalences between program expressions and constants and their negations; linear-ordering inequalities between program expressions and constants. Analysis is executed by a worklist-based fixpoint algorithm which interprets conditional branches and ignores some impossible paths. This analysis algorithm incorporates a simple inference procedure that derives validity or inconsistency of environment constituents by exploiting both positive and negative information. The analysis algorithm is shown to be conservative; its asymptotic time complexity is cubic. Tracking branch conditions enables such optimizations as elimination of unreachable code, elimination of redundant conditional branches, and removal of conditional branches from some execution paths. Two novel optimizations enabled by the analysis are presented. These optimizations eliminate conditional branches from some paths after replicating code. They leverage upon additional local analysis