Path-Sensitive Analysis for Linear Arithmetic and Uninterpreted Functions
Abstract
We describe data structures and algorithms for performing a
path-sensitive program analysis to discover equivalences of
expressions involving linear arithmetic or uninterpreted functions. We
assume that conditionals are abstracted as boolean variables, which
may be repeated to reflect equivalent conditionals. We introduce
"free conditional expression diagrams" (FCEDs), which extend binary
decision diagrams (BDDs) with internal nodes corresponding to linear
arithmetic operators or uninterpreted functions. FCEDs can represent
values of expressions in a program involving conditionals and linear
arithmetic (or uninterpreted functions). We show how to construct them
easily from a program, and give a randomized linear time algorithm (or
quadratic time for uninterpreted functions) for comparing FCEDs for
equality. FCEDs are compact due to maximal representation sharing for
portions of the program with independent conditionals. They inherit
from BDDs the precise reasoning about boolean expressions needed to
handle dependent conditionals.