Inferring Numerical Abstract Domain Types from Concrete Program States

Abstract

The effectiveness of interpretation-based numerical analyses depends on the choice of abstract domain. Domains such as Zones and Octagons differ in expressiveness and cost, so the goal is to identify the least expressive domain that is sufficient for a given analysis context. The challenge is that this choice varies across variables and program locations, while obtaining variable-location domain recommendations using lightweight static techniques can be difficult. This paper proposes an approach for inferring the recommended numerical domain type for each variable at each program location from concrete program states. We use MultisetGA to generate test suites that yield large, strategically distributed sets of unique concrete states, with at least 1,000 states per location. We then use AbsDiakon, an extension of Daikon, to infer invariants matching numerical abstract-domain templates. These templated invariants are analyzed to identify the domain type recommended for each variable. Our preliminary results show that, over all variable-location pairs, the inferred recommendations exactly match the computed reference domains in 85.6% of cases, are more expressive in 14.4% of cases, and are never less expressive.