Experiment on a Modular Program Aanlysis That Saves Memory

We present a modular fixpoint computation that consumes smaller memory than a global fixpoint iterations yet with no loss of accuracy. Our motivation comes from designing a scalable global program analysis. Program analysis is to compute a fixpoint of a system of equations. For large-scale global analysis for bug-finding or verification, analysis ’ memory consumption is more decisive factor for its usability than its time consumption. Our method is to re-arrange the original system of equations into two hierarchies. We partition the equations into smaller sets, and then we prepare a set of equations that “links ” the partitions. After solving the set of link equations with nested fixpoint iterations, we solve each partition separately. If the size of link equations set is small, than we can solve each partition and the set of linker equations with smaller memories. This method is implemented inside a realistic C analyzer. From our experiment of analyzing 5,000LOC- 20,000LOC GNU programs, we observed our modular method have 50-71 % memory peak saving