Bebop

摘要

Flow-sensitive data analyses can lose precision because they assume that all paths in a control-flow graph are executable (feasible). Path-sensitive dataflow analyses can rule out infeasible paths by tracking correlations between dataflow facts. To track such correlations, in general, requires recording a set of sets of facts per statement in a program. Naive representation of such sets can lead to a very high memory consumption and running time.

We reformulate an interprocedural dataflow algorithm by Reps, Horwitz and Sagiv (based on context-free graph reachability) into a traditional interprocedural flow-sensitive dataflow algorithm. We then show how to use Binary Decision Diagrams (BDDs), a data structure from the model checking community, to turn this reformulated algorithm into an interprocedural path-sensitive dataflow analysis algorithm that tracks a set of set of facts per program statement. We have implemented this algorithm in a tool called ebop.