Path-Sensitive Analysis for Linear Arithmetic and Uninterpreted Functions

Sumit Gulwani and George C. Necula

EECS Department
University of California, Berkeley
Technical Report No. UCB/CSD-04-1325
May 2004

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2004/CSD-04-1325.pdf

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.


BibTeX citation:

@techreport{Gulwani:CSD-04-1325,
    Author = {Gulwani, Sumit and Necula, George C.},
    Title = {Path-Sensitive Analysis for Linear Arithmetic and Uninterpreted Functions},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2004},
    Month = {May},
    URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2004/5751.html},
    Number = {UCB/CSD-04-1325},
    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.}
}

EndNote citation:

%0 Report
%A Gulwani, Sumit
%A Necula, George C.
%T Path-Sensitive Analysis for Linear Arithmetic and Uninterpreted Functions
%I EECS Department, University of California, Berkeley
%D 2004
%@ UCB/CSD-04-1325
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2004/5751.html
%F Gulwani:CSD-04-1325