On-demand strong update analysis via value-flow refinement

Abstract

We present a new Strong UPdate Analysis for C programs, called Supa, that enables computing points-to information on-demand via value-flow refinement, in environments with small time and memory budgets such as IDEs. We formulate Supa by solving a graph-reachability problem on a value- flow graph representation of the program, so that strong updates are performed where needed, as long as the total analysis budget is not exhausted. Supa facilitates efficiency and precision tradeoffs by allowing different pointer analyses to be applied in a hybrid multi-stage analysis framework.