Detection of infeasible paths using Presburger arithmetic
Kuniaki Naoi, Naohisa Takahashi · Systems and Computers in Japan · 1999
An efficient method is proposed to determine the truth of a prenex-normal form Presburger sentence bounded only by existential quantifiers (EPP-sentence), which is used for detecting infeasible paths (IFPs). Detection of IFPs makes it generally possible to perform various kinds of program analyses more accurately along a computation path. In conventional determination methods for the truth of general Presburger sentences, there are cases where the amount of computation is extremely large and IFPs cannot be detected within a practical time. In the proposed method, the matrix of coefficients for variables (coefficient matrix) is triangulated using a theorem in number theory. If the rank of the triangulated coefficient matrix is less than the degree of the matrix, the coefficient matrix is triangulated using a method for solving one linear equation with three or more unknowns. Furthermore, the truth of the EPP-sentence is determined using back-substitution. The proposed method is particularly effective when the absolute values of the coefficients associated with the variables in the EPP-sentence are large; that is, when the absolute values of coefficients for path condition in IFP detection are large. We confirm that an implementation of the proposed method reduces computation time by a factor of up to 3 million times compared with the previous method. ©1999 Scripta Technica, Syst Comp Jpn, 30(9): 74–87, 1999