Method for recognition of full-word saturating addition and subtraction

1. A method of recognizing full-word saturating addition and subtraction in a program for every basis statement A of the form z=ADD(x,y) or z=SUB(x,y), the method performed on a computer comprising:

inserting the statement z sat =ADDSAT(x,y) or z sat =SUBSAT(x,y) immediately following the statement A;

computing bits values BITS(E,v) properties of the variable v at edges E in the program;

computing condition COND(E) properties under which the edges E are executed in the program;

computing reach REACH(E,v) properties indicating which values of the variable v reaches a use of variable z in statement S at edges E in the program for overflow or underflow or normal occurrences;

replacing z in a statement S that uses z with the use of z sat if all of the following conditions hold for the statement S: a) the only values of z that reach S cause SATMAX to be assigned to z when overflow has occurred, b) the only values of z that reach S cause SATMIN to be assigned to z if underflow has occurred, and c) the only values of z that reach S are from the basis statement A if no underflow and no overflow has occurred; and

removing statements made unnecessary by the replacement of uses of z with z sat in the previous step.

2. The method according to claim 1 , including defining overflow, underflow and “normal” predicates for REACH as follows wherein X, Y, Z are the signs of variables x, y, z respectively:

Form of the basis statement A

Predicate

z = ADD(x,y)

z = SUB(x,y)

Overflow condition F OF

F OF = X Y Z

F OF = X Y Z

Underflow condition

F UF = X Y Z

F UF = X Y Z

F UF

No overflow and no

F N = F OF F UF

underflow (“normal”)

F N.

3. The method according to claim 2 , wherein the REACH properties include a constant value C OF (E,v) taken by the variable v when the edge E is executed, if overflow had occurred; a constant value C UF (E,v) taken by the variable v when the edge E is executed, if underflow had occurred; and a Boolean flag ISZ(E,v) which indicates whether v carries the same value as the variable z in the basis statement A when the edge E is executed and neither overflow nor underflow had occurred.

4. The method according to claim 1 wherein the occurrences of overflow or underflow or normal is determined as a function of the sign bits of X, Y and Z.

5. The method according to claim 1 , including solving the equations using dense techniques.

6. The method according to claim 1 , including solving the equations using sparse program representation.

7. The method according to claim 1 , wherein the values, properties and conditions are approximated using global data flow analysis, which includes a lattice for approximating BITS, COND, REACH and a system of equations relating approximations to various program points.

8. The method according to claim 7 , including compressing of lattice vectors assigned to the variables.

9. In a method of formulation and solving program analysis equations on a computer that facilitate recognition of full word saturating addition and subtraction, the method of formulation comprising, for each basis addition statement z=x+y or subtraction statement z=x−y, formulating data flow equations that describe the following properties of the program statements being analyzed:

a) values BITS of program variables x, y, z as Boolean functions of the sign bits of X, Y and Z;

b) condition COND under which program statements S are executed as Boolean functions of the sign bits of X, Yand Z;

c) condition REACH of which values of the variables reaches a use of variable z in statements S for overflow or underflow or normal occurrences; and

replacing z in a statement S of the program that uses z with the use of z sat if and only if all of the following conditions hold for that statement S: 1) the only values of z that reach S assigns cause SATMAX to be assigned to z when overflow has occurred, 2) only values of z that reach S assigns cause SATMIN to be assigned to z if underflow has occurred, and 3) only values of z that reach S are from the basis statement if no underflow and no overflow has occurred.

10. The method according to claim 9 , wherein the occurrences of overflow or underflow or normal is determined as a function of the sign bits of X Y and Z.

11. The method according to claim 9 , including removing statements made unnecessary by the replacement of uses of z with z sat .

12. The method according to claim 9 , including solving the equations for BITS, COND and REACH using dense techniques.

13. The method according to claim 9 , including solving the equations for BITS, COND and REACH using sparse program representation.

14. The method according to claim 9 , wherein the values and conditions are approximated using global data flow analysis, which includes a lattice for approximating BITS, COND, REACH and a system of equations relating approximations to various program points.

15. The method according to claim 14 , including compressing of lattice vectors assigned to the variables.

16. The method according to claim 9 , wherein REACH includes a constant value C OF (E,v) taken by the variable v when the edge E is executed, if overflow had occurred; a constant value C UF (E,v) taken by the variable v when the edge E is executed, if underflow had occurred; and a Boolean flag ISZ(E,v) which indicates whether v carries the same value as the variable z in the basis statement when the edge E is executed and neither overflow nor underflow had occurred.