Mixing Type Checking and Symbolic Execution (Extended Version)

View/ Open
Date
2010-03-23Author
Khoo, Yit Phang
Chang, Bor-Yuh Evan
Foster, Jeffrey S.
Metadata
Show full item recordAbstract
Static analysis designers must carefully balance precision and
efficiency. In our experience, many static analysis tools are built
around an elegant, core algorithm, but that algorithm is then
extensively tweaked to add just enough precision for the coding idioms
seen in practice, without sacrificing too much efficiency. There are
several downsides to adding precision in this way: the tool's
implementation becomes much more complicated; it can be hard for an
end-user to interpret the tool's results; and as software systems vary
tremendously in their coding styles, it may require significant
algorithmic engineering to enhance a tool to perform well in a
particular software domain.
In this paper, we present Mix, a novel system that mixes type checking
and symbolic execution. The key aspect of our approach is that these
analyses are applied independently on disjoint parts of the program, in
an off-the-shelf manner. At the boundaries between nested type checked
and symbolically executed code regions, we use special mix rules to
communicate information between the off-the-shelf systems. The resulting
mixture is a provably sound analysis that is more precise than type
checking alone and more efficient than exclusive symbolic execution. In
addition, we also describe a prototype implementation, Mixy, for C. Mixy
checks for potential null dereferences by mixing a null/non-null type
qualifier inference system with a symbolic executor