We apply linear algebra techniques to precise interprocedural dataflow
analysis. Specifically, we describe analyses that determine for each
program point identities that are valid among the program variables
whenever control reaches that program point. Our analyses fully
interpret assignment statements with affine expressions on the right
hand side while considering other assignments as non-deterministic and
ignoring conditions at branches. Under this abstraction, the analysis
computes the set of all AFFINE IDENTITIES and, more generally,
all POLYNOMIAL IDENTITIES OF BOUNDED DEGREE precisely. The
running time of our algorithm is linear in the program size and
polynomial in the number of occurring variables. We also show how to
deal with local variables and indicate how to handle parameters and
return values of procedures.
