UCLA COMSCI 232 - Assertion Checking over Combined Abstraction of Linear Arithmetic and Uninterpreted Functions

Unformatted text preview:

Assertion Checking over Combined Abstractionof Linear Arithmetic and UninterpretedFunctionsSumit Gulwani1and Ashish Tiwari21Microsoft Research, Redmond, WA 98052, [email protected] International, Menlo Park, CA 94025, [email protected]. This paper presents results on the problem of checking equal-ity assertions in programs whose expressions have been abstracted usingcombination of linear arithmetic and uninterpreted functions, and whoseconditionals are treated as non-deterministic.We first show that the problem of assertion checking for this combinedabstraction is coNP-hard, even for loop-free programs. This result is quitesurprising since assertion checking for the individual abstractions of lin-ear arithmetic and uninterpreted functions can be performed efficientlyin polynomial time.Next, we give an assertion checking algorithm for this combined abstrac-tion, thereby proving decidability of this problem despite the underlyinglattice having infinite height. Our algorithm is based on an importantconnection between unification theory and program analysis. Specifically,we show that weakest preconditions can b e strengthened by replacingequalities by their unifiers, without losing any precision, during back-ward analysis of programs.1 IntroductionWe use the term equality assertion or simply assertion to refer to an equal-ity between two program expressions. B y assertion checking, we mean checkingwhether a given assertion is an invariant at a given program point.Reasoning about assertions in programs is an undecidable problem. Hence,assertion checking is typically performed over some (sound) abstraction of theprogram. This may give rise to false positives, i.e., some assertions that aretrue in the origina l program may not be true in the abstract version. There isan efficiency-precision trade-off in the choice of the abstraction. A more preciseabstraction leads to fewer false positives but is also harder to re ason about.Linear arithmetic and uninterpreted functions3are two most commonly usedexpression languages for cre ating program abstractio ns. There are several papers3An uninterpreted function F of arity n satisfies only one axiom: If ei= e′ifor1 ≤ i ≤ n, then F (e1, . . , en) = F (e′1, . . , e′n). Uninterpreted functions are commonlyused to abstract programming language operators that are otherwise hard to reasonabout. They are also used to abstract procedure calls.a1:= 0; a2:= 0;b1:= 1; b2:= F(1);c1:= 3; c2:= F(4);a1:= a1+1; a2:= a2+2;b1:= F(b1); b2:= F(b2);c1:= F(1+c1); c2:= F(c2+1);a1< 100FalseTrueAssert(a2=2a1);Assert(b2= F(b1));Assert(c2=F(c1+1));Fig. 1. This program illustrates the difference between precision of performing analysisover the abstractions of linear arithmetic (which can verify only the first assertion),uninterpreted functions (which can verify only the second assertion), and their combina-tion (which can verify all assertions). F denotes some function without any side-effectsand can be modeled as an uninterpreted function for purpose of proving the assertions.that describe how to do assertion checking for each of these abstractions. (Sec-tion 6 on related work describes some of this work.) The combined expr e ssionlanguage of linear arithmetic a nd uninter preted functions yields a more preciseabstraction than the ones obtained from either of these two expression languages.For example, consider the prog ram shown in Figure 1. Note that all assertions a tthe end of the program ar e true. If this program is analyzed over the a bstractionof linear arithmetic (using, fo r example, the abstract interpreter descr ibed in [14]or [6]), then o nly the first assertion can be validated. This is because discoveringthe relationship between b1and b2, and between c1and c2, involves reas oningabout uninterpreted functions. Similarly, if this program is analyzed over the ab-straction of uninterpreted functions (using, for example, the abstract interpreterdescribed in [10]), then only the second as sertion can be validated. However, ananalysis over the combined abstraction of linear arithmetic and uninter pretedfunctions can verify all assertions.Even though there has been a lot of work for reasoning about the abstrac-tions of linear arithmetic and that of uninterpreted functions, the problem ofassertion checking over the combined abstrac tio n of linear arithmetic a nd unin-terpreted functions has not been considered before. In this pape r, we considerthe problem of checking equality assertions in programs whose expressions havebeen abstracted using linear arithmetic and uninterpreted functions. We alsoabstract all program conditionals as non-deterministic because otherwis e theproblem is easily shown to be undecidable even for the individual abstractionsof linear arithmetic [17] and uninterpreted functions [16]. (An analy sis that per-forms an imprecise reasoning over the combined abstraction of linear arithmetic2and uninterpreted functions but takes conditional guards into account wouldalso be useful in practice, and can be used, for example, for array bounds check-ing. The related work section mentions our recent work on combining abstrac tinter preters, which can be used to construct such an analysis.) The abstractedprogram model is formally described in Sectio n 2.In Section 3, we show that the problem of assertion checking in the com-bined abstraction of linear arithmetic and uninterpreted functions is coNP-hard.This is true even for loop-free programs, in which case it is coNP-complete. Thisresult is quite surprising because assertion checking in the individual abstrac-tions of linear arithmetic and uninterpreted functions entails polynomial-timealgorithms (even for programs with loops). Karr’s a lgorithm [14, 17] ca n be usedto perform assertion checking when program expressions have been abstrac tedusing linear arithmetic operators. Gulwani and Necula’s algorithm [9, 10] per-forms assertion checking in progr ams whose ex pressions have been abstractedusing uninterpreted functions. Both these algorithms run in polynomial time.However, our coNP-hardness result shows tha t there is no way to combine thesealgorithms to do assertion checking for the combined abstraction in polynomialtime (unless P=coNP). A similar combination problem has been studied ex-tensively in the context of decision procedures. Nelson and Oppen have given afamous combination result for combining decision procedures for disjoint, convexand quantifier-free theories


View Full Document

UCLA COMSCI 232 - Assertion Checking over Combined Abstraction of Linear Arithmetic and Uninterpreted Functions

Documents in this Course
Load more
Download Assertion Checking over Combined Abstraction of Linear Arithmetic and Uninterpreted Functions
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Assertion Checking over Combined Abstraction of Linear Arithmetic and Uninterpreted Functions and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Assertion Checking over Combined Abstraction of Linear Arithmetic and Uninterpreted Functions 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?