IntroductionAnalysis for Linear ArithmeticProblem DefinitionFCED ConstructionRandomized Equivalence TestingCompleteness and Probabilistic Soundness of the AlgorithmTime and Space ComplexityAnalysis for Uninterpreted FunctionsProblem DefinitionFCED ConstructionRandomized Equivalence TestingCompleteness and Probabilistic Soundness of the AlgorithmTime and Space ComplexityComparison with Related WorkConclusion and Future WorkPublished in “Static Analysis Symposium”, SAS, 2004Path-Sensitive Analysis for Linear Arithmeticand Uninterpreted FunctionsSumit Gulwani and George C. NeculaUniversity of California, Berkeley{gulwani,necula}@cs.berkeley.eduAbstract. We describe data structures and algorithms for performinga path-sensitive program analysis to discover equivalences of expressionsinvolving linear arithmetic or uninterpreted functions. We assume thatconditionals are abstracted as boolean variables, which may be repeatedto reflect equivalent conditionals. We introduce free conditional expres-sion diagrams (FCEDs), which extend binary decision diagrams (BDDs)with internal nodes corresponding to linear arithmetic operators or un-interpreted functions. FCEDs can represent values of expressions in aprogram involving conditionals and linear arithmetic (or uninterpretedfunctions). We show how to construct them easily from a program, andgive a randomized linear time algorithm (or quadratic time for uninter-preted functions) for comparing FCEDs for equality. FCEDs are compactdue to maximal representation sharing for portions of the program withindep ende nt conditionals. They inherit from BDDs the precise reasoningab out boolean expressions needed to handle dependent conditionals.1 IntroductionData structures and algorithms for manipulating boolean expressions (e.g., bi-nary decision diagrams) have played a crucial role in the success of model check-ing for hardware and software systems. Software programs are often transformedusing boolean abstraction [4] to boolean programs: arithmetic operations andother operators are modeled c onservatively by their effect on a number of booleanvariables that encode predicates on program state. In this pap e r, we show thatwe can reason efficiently and precisely about programs that contain not onlyboolean expressions but also linear arithmetic and uninterpreted functions. Suchalgorithms are useful when the desired level of precision cannot be achieved withboolean abstraction of linear arithmetic expressions in a program.Consider the program fragment shown in Figure 1. The atomic boolean ex-pressions in the conditionals (e.g. x < y, y == z ) have been abstracted as booleanvariables c1and c2. We assume that the conditional abstraction procedure canThis research was supported in part by the National Science Foundation Grant CCR-0081588, and gifts from Microsoft Research. The information presented here doesnot necessarily reflect the position or the policy of the Government and no officialendorsement should be inferred.328Fig. 1. An example program fragment.sometimes detect equivalences of atomic boolean expressions (e.g. x < y andy > x are equivalent), as is the case for the first and last conditionals in theprogram. Suppose our goal is to determine the validity of the two assertions inthe program. The first assertion holds because it is established on all four pathsthat can reach it. The second assertion holds only because the first and last con-ditionals use identical guards. A good algorithm for verifying these assertionsshould be able to handle such dependent conditionals (Two conditionals are de-pendent if truth-value of one depends on the other), or in other words perform apath-sensitive analysis, without individually examining an exponential numberof paths that arise for portions of the program with independent conditionals.Since there is no obvious boolean abstraction for this example, we need toreason about the linear arithmetic directly. There are two kinds of algorithmsknown to solve this problem. On one extreme, there are abstract/random inter-pretation based polynomial-time algorithms, which perform a path-insensitiveanalysis. Karr described a deterministic algorithm [22] based on abstract inter-pretation [11]. Recently, we gave a faster randomized algorithm [18] based onrandom interpretation. These algorithms are able to decide the first assertionin the program since the first two conditionals preceding it are independent ofeach other. However, these algorithms cannot verify that the second assertionholds, because they would attempt to do so over all the eight paths through theprogram, including four infeasible ones.329Fig. 2. The MTBDD representation for symbolic values of variables of the pro-gram in Figure 1. The internal nodes are conditionals whose left child corre-sponds to the conditional being true. The leaves are canonicalized linear arith-metic expressions.Fig. 3. The VDG/FCED representations for symbolic values of variables of theprogram in Figure 1. The internal nodes also involve arithmetic operations. Thisleads to succinct representations, and allows sharing.On the other extreme, there are multi-terminal binary decision diagram(MTBDD) [15] based algorithms that consider all feasible paths in a programexplicitly, and hence are able to decide both assertions in our example. However,these algorithms run in exponential time even when most of the conditionals in aprogram are independent of each other, which is quite often the case. MTBDDsare binary decision diagrams whose leaves are not boolean values but canonical-ized linear expressions. For the example program, the MTBDDs correspondingto final values of the various variables are shown in Figure 2. These MTBDDs usethe same ordering of boolean variables and the same canonicalization for leaves.With MTBDDs we can verify both assertions; however note that checking equal-ity b e tween w and y essentially involves performing the check individually oneach of the four paths from the beginning of the program to the first assertion.Also note that there is little opportunity for sharing subexpressions in a MTBDDdue to the need to push computations down to the leaves and to canonicalize theleaves. This algorithm is exponential in the number of boolean variables in theprogram. Its weak point is the handling of sequences of independent conditionalsand its strong point is that it can naturally handle dependent conditionals, justlike a BDD does for a boolean program.In this paper, we describe