Using ZBDDs in Points-to Analysis

Binary Decision Diagrams (BDDs) have recently become widely accepted as a space-efficient method of representing relations in points-to analyses. When BDDs are used to represent relations, each element of a domain is assigned a bit pattern to represent it, but not every bit pattern represents an element. The circuit design, model checking, and verification communities have achieved significant reductions in BDD sizes using Zero-Suppressed BDDs (ZBDDs) to avoid the overhead of these don’t-care bit patterns. We adapt BDD-based program analyses to use ZBDDs instead of BDDs. Our experimental evaluation studies the space requirements of ZBDDs for both context-insensitive and contextsensitive program analyses and shows that ZBDDs can greatly reduce the space requirements for expensive context-sensitive points-to analysis. Using ZBDDs to reduce the size of the relations allows a compiler or other software analysis tools to analyze larger programs with greater precision. We also provide a ...

• Type: Conference
• Year: 2007
• Where: LCPC
• Authors: Ondrej Lhoták, Stephen Curial, José Nelson Amaral
• Keywords: Binary Decision Diagrams, Bit Patterns, Distributed And Parallel Computing, LCPC 2007, Program Analyses