I found one special case of this transform for 'slt 0', so I removed that and added the general transform.

Here are Alive programs that try to verify the correctness of the logic:

http://rise4fun.com/Alive/GH

(is there a better way to write the no-overflow constraints?)

Name: slt_no_overflow

Pre: ((C1 < 0) && (C2 < 0)) || ((C1 >= 0) && (C2 >= 0)) || (((C2 - C1) < 0) && (C2 < 0)) || (((C2 - C1) >= 0) && (C2 >= 0))

%a = add nsw i8 %x, C1

%b = icmp slt %a, C2

=>

%b = icmp slt %x, C2 - C1

Name: sgt_no_overflow

Pre: ((C1 < 0) && (C2 < 0)) || ((C1 >= 0) && (C2 >= 0)) || (((C2 - C1) < 0) && (C2 < 0)) || (((C2 - C1) >= 0) && (C2 >= 0))

%a = add nsw i8 %x, C1

%b = icmp sgt %a, C2

=>

%b = icmp sgt %x, C2 - C1

And here are the cases where the subtraction does overflow:

http://rise4fun.com/Alive/ao

Name: slt_overflow_false

Pre: C2 < 0 && C1 >= 0 && (C2 - C1) >= 0

%a = add nsw i8 %x, C1

%b = icmp slt %a, C2

=>

%b = false

Name: slt_overflow_true

Pre: C2 >= 0 && C1 < 0 && (C2 - C1) < 0

%a = add nsw i8 %x, C1

%b = icmp slt %a, C2

=>

%b = true

Name: sgt_overflow_true

Pre: C2 < 0 && C1 >= 0 && (C2 - C1) >= 0

%a = add nsw i8 %x, C1

%b = icmp sgt %a, C2

=>

%b = true

Name: sgt_overflow_false

Pre: C2 >= 0 && C1 < 0 && (C2 - C1) < 0

%a = add nsw i8 %x, C1

%b = icmp sgt %a, C2

=>

%b = false