Duration: 1:25:56

543 views

8

The talk will discuss the benefits of using logic-based declarative languages, especially for program analysis. The main focus will be on the Doop framework for points-to analysis of Java programs. Doop builds on the idea of specifying pointer analysis algorithms declaratively, using Datalog: a logic-based language for defining (recursive) relations. We carry the declarative approach further than past work by describing the full end-to-end analysis in Datalog and optimizing aggressively using a novel technique that takes into account Datalog incremental evaluation. As a result, Doop decisively redefines the state-of-the-art in pointer analysis, and challenges our understanding of how to build scalable precise program analyses. Doop's precise analyses are the first to achieve scalability without the use of binary decision diagrams (BDDs) and outperform BDD-based analyses by substantial amounts. We compare Doop with Lhot┬┤ak and HendrenΓÇÖs Paddle. For the exact same logical points-to definitions (and, consequently, identical precision) Doop is more than 15x faster than Paddle for common precise (context-sensitive) analyses of the DaCapo benchmarks. Additionally, Doop scales to very precise analyses that are impossible with Paddle and Whaley et al.ΓÇÖs bddbddb, directly addressing open problems in past literature. Finally, our implementation is modular and can be easily configured to analyses with a wide range of characteristics, largely due to its declarativeness. Generalizing from Doop and Datalog, we will discuss a broader plan for using declarative languages with a logical flavor for various domains in future work.