Method For Recognition Of Acyclic Instruction Patterns

摘要

A method which determines by an optimizing compiler whether any variable in the given program equals to the given acyclic mathematical function f(x,y, . . . ) applied to the given variables x, y, . . . in the program. In one embodiment, the method includes expressing the bits of the value of the function f(x,y, . . . ) as a Boolean function of the bits of the inputs x, y, . . . ; expressing, for every variable v and program statement s, the value taken by v when s is executed as a Boolean function V(s,v)(x, y, . . . ) of the bits of x, y, . . . ; and expressing, for every statement s, the condition under which the statement is executed as a Boolean function C(s)(x, y, . . . ) of the bits of the inputs x, y, . . . . Finally, a determination is made using a Boolean satisfiability oracle of whether, for the given variable v and program statement s, the following Boolean expression holds: C(s)(x,y, . . . )=>V(s,v)(x,y . . . )=f(x,y, . . . ). In a second embodiment, the method includes expressing the value of f(x,y, . . . ) as a plurality of functions f_j(x,y, . . . ) having the corresponding predicate P_j(x,y, . . . ); expressing, for every variable v and program statement s, the value taken by v when s is executed as a plurality of functions V_j(s,v)(x,y, . . . ), one for each predicate P_j(x,y, . . . ); and expressing, for every statement s, the condition under which the statement is executed as a plurality of functions C_j(s)(x,y, . . . ), one for each predicate P_j(x,y, . . . ). Finally, a determination is of whether for the given variable v and program statement s, V_j(s,v)(x,y, . . . )=f_j(x,y, . . . ) whenever the predicate P_j(x,y, . . . ) and the condition C_j(s)(x,y, . . . ) are true.