System and method for scalable flow and context-sensitive pointer alias analysis
A system and method for pointer analysis for computer program verification includes forming a subset or cluster of pointers from pointers in a program by applying increasingly accurate alias analyses in a cascaded fashion such that each analysis works on a subset of pointers generated by a previous analysis's results. Aliases are computed for any pointer by computing aliases in the subsets in parallel instead of an entire program. For carrying out context and flow-sensitive alias analysis, function summaries are computed on small subsets in a top-down manner based on the points-to hierarchy which reduces the sizes of the summaries.
1. A method for pointer analysis for computer program verification, comprising:
forming a subset or cluster of pointers from pointers in a program by applying increasingly accurate alias analyses in a cascaded fashion such that each analysis works on a subset of pointers generated by a previous analysis's results; and
computing aliases, using a processor, for any pointer by decomposing the subset or cluster of pointers into smaller subsets and computing a separate alias analysis in each of the smaller subsets in parallel instead of carrying out the alias analysis for all pointers in the program.
2. The method as recited in claim 1 , wherein forming a subset or cluster of pointers includes dividing pointers into clusters based upon a property that a computation of the aliases of a pointer in the program can be reduced to the computation of its aliases in each of the subsets in which pointer appears.
3. The method as recited in claim 1 , wherein applying increasingly accurate alias analyses includes applying Steensgaard's analysis to define clusters as sets of pointers aliased as encoded in a Steensgaard points-to graph.
4. The method as recited in claim 3 , wherein applying increasingly accurate alias analyses includes applying Andersen's analysis to the defined clusters from the Steensgaard's analysis.
5. The method as recited in claim 1 , wherein computing context-sensitive aliases includes performing a summarization-based flow and context-sensitive alias analysis for each small cluster from Steensgaard and/or Andersen clustering in parallel.
6. The method as recited in claim 1 , wherein computing aliases includes computing function summaries for a reduced number of functions.
7. The method as recited in claim 1 , wherein function summaries for context and flow-sensitive alias analysis are computed in a top-down manner on a points-to hierarchy to reduce a size of summary tuples.
8. A non-transitory computer readable storage medium for pointer analysis for computer program verification comprising a computer readable program, wherein the computer readable program when executed on a computer causes the computer to perform the steps of:
forming a subset or cluster of pointers from pointers in a program by applying increasingly accurate alias analyses in a cascaded fashion such that each analysis works on a subset of pointers generated by a previous analysis's results; and
computing aliases for any pointer by decomposing the subset or cluster of pointers into smaller subsets and computing a separate alias analysis in each of the smaller subsets in parallel instead of carrying out the alias analysis for all pointers in the program.
9. The non-transitory computer readable storage medium as recited in claim 8 , wherein forming a subset or cluster of pointers includes dividing pointers into clusters based upon a property that a computation of the aliases of a pointer in the program can be reduced to the computation of its aliases in each of the subsets in which pointer appears.
10. The non-transitory computer readable storage medium as recited in claim 9 , wherein computing context-sensitive aliases includes performing a summarization-based flow and context-sensitive alias analysis for each small cluster from Steensgaard and/or Andersen clustering in parallel.
11. The non-transitory computer readable storage medium as recited in claim 9 , wherein computing aliases includes computing function summaries for a reduced number of functions.
12. The non-transitory computer readable storage medium as recited in claim 9 , wherein function summaries for context and flow-sensitive alias analysis are computed in a top-down manner on a points-to hierarchy to reduce a size of summary tuples.
13. The non-transitory computer readable storage medium as recited in claim 9 , wherein applying increasingly accurate alias analyses includes applying Steensgaard's analysis to define clusters as sets of pointers aliased as encoded in a Steensgaard points-to graph.
14. The non-transitory computer readable storage medium as recited in claim 13 , wherein applying increasingly accurate alias analyses includes applying Andersen's analysis to the defined clusters from the Steensgaard's analysis.