Computing Maximum Fixed Point Solutions over Feasible Paths in Data Flow Analyses
Komal Pathade, Uday Khedker

TL;DR
This paper introduces a generic feasible path maximum fixed point (FPMFP) approach for data flow analysis that improves precision by excluding infeasible paths without CFG restructuring, demonstrated on program analysis benchmarks.
Contribution
It defines a path-sensitive fixed point solution that excludes infeasible paths using external information, avoiding CFG restructuring and enhancing analysis precision.
Findings
Reduced def-use pairs by up to 13.6%
Eliminated up to 100% of uninitialized variable alarms
FPMFP computation is 2.9 times slower than standard MFP
Abstract
The control flow graph (CFG) representation of a procedure used by virtually all flow-sensitive program analyses, admits a large number of infeasible control flow paths i.e., these paths do not occur in any execution of the program. Hence the information reaching along infeasible paths in an analysis is spurious. This affects the precision of the conventional maximum fixed point (MFP) solution of the data flow analysis, because it includes the information reaching along all control flow paths. The existing approaches for removing this imprecision are either specific to a data flow problem with no straightforward generalization or involve control flow graph restructuring which may exponentially blow up the size of the CFG. We lift the notion of MFP solution to define the notion of feasible path MFP (FPMFP) solutions that exclude the data flowing along known infeasible paths. The notion…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Software Testing and Debugging Techniques · Parallel Computing and Optimization Techniques
