Static Analysis in Disjunctive Numerical DomainsSriram Sankaranarayanan , Franjo Ivancic, Ilya Shlyakhter, Aarti Gupta |
|
The convexity of numerical domains such as polyhedra, oc tagons,
intervals and linear equalities enables tractable analysis of soft
ware for buffer overflows, null pointer dereferences and floating
point errors. However, convexity also causes the analysis to fail in
many common cases. Powerset extensions can remedy this shortcoming by
considering disjunctions of predicates. Unfortunately, analysis using
powerset domains can be exponentially more expensive as compared to
analysis on the base domain. In this paper, we prove structural
properties of fixed points computed in commonly used powerset
extensions. We show that a fixed point computed on a powerset
extension is also a fixed point in the base domain computed on an
``elaboration'' of the program's CFG structure. Using this insight, we
build analysis algorithms that approach path sensitive static analysis
algorithms by performing the fixed point computation on the base
domain while discovering an ``elaboration'' on the fly. Using
restrictions on the nature of the elaborations, we design algorithms
that scale polynomially in terms of the number of disjuncts. We have
implemented a lighteight static analyzer for C programs with
encouraging initial results.
|
| ps pdf |
| Static Analysis Symposium (SAS 2006), volume 4134 of Lecture Notes in Computer Science, pp. 3-17, Springer-Verlag. |
| Copyright (C) Springer-Verlag. Copy has been made available online for personal use only. Do not redistribute without permission. |