Path sensitive MFP solutions in presence of intersecting infeasible control flow path segments

Data flow analysis computes Maximum Fix Point (MFP) solution which represents an over approximation of the data reaching a program point along all control flow paths (cfps). Some of these cfps may be infeasible; meaning, the necessary pre-condition for execution of cfp is not satisfiable in any run of the program. Approximations that do not discern data along infeasible cfps may lead to imprecision, because they include spurious information. Recent methods progressively separate the data along feasible and infeasible prefixes of infeasible cfps to ignore data corresponding to prefix that is infeasible. A criteria called minimal infeasible path segment is used to identify the cluster of infeasible cfps which can be considered equivalent for maintaining separate data. Clustering is useful because it avoids the possibly exponential cost of keeping the data along each infeasible cfp separate. The recent clustering approach is imprecise in presence of shared edges between cfps from two different clusters. In this work, we formalize the interaction between clusters and provide a more general and effective criteria for clustering the infeasible cfps. Our experiments indicate up to 2-3 times increase in the precision over previous approach, with average 100% increase in memory and time required for the analysis. This is possible because our empirical observation indicates that on average 70% clusters overlap with other clusters.