Clarification on Rewrite in Simplify_LT.cpp

[prasmish]

Hi everyone,
I was going through the rewrites in Simplify_LT.cpp and I came across the line which is rewrite(x - y < z, x < z + y). My concern is that changing the expression from x - y < z to x < y+z can make the expression overflow when initially it was not an overflow expression. Here I am assuming the x,y and z are of int32 type. Can anyone help me in this?

For example:

  bounded_input(x, y) = cast<int32_t>(BoundaryConditions::repeat_edge(input_buf)(x, y));
  exp(x,y) = (bounded_input(x, y)*1007+bounded_input(x, y)*51) - (bounded_input(x, y)*bounded_input(x, y));
  neww(x,y) = 100*exp(x,y) - exp(x-1,y)*exp(x,y-1);
  myFunc(x, y) = select((neww(x, y)) >= 1900000000, 255, 0);`

Now in the code generated by halide, it roughly translate to something like, select(100*exp(x,y) < exp(x-1,y)*exp(x,y-1) + 1900000000, 0, 255); In this translated version, there is the possibility that code provided by programmer was not going to overflow but the translated code does overflow.

@abadams

[abadams]

You've identified a real problem we have that we haven't gotten around to fixing. We use the simplifier to prove facts about integers, so there are rewrites that are valid in the integers. Many are not valid in any type that can overflow. We sloppily use Int(32) as a stand-in for infinite integers. Surprisingly, this has been mostly fine. The problem only rears its head when users write fixed-point code that uses Int(32) types and reasons about overflow. I suggest using UInt(32) instead, which is the same for +/-/*, and just casting to Int(32) for any comparisons, or min/max operations.

The actual solution is to add a separate index type for our internal uses and define overflow for Int(32) in user code. This is going to be a lot of work though.

[prasmish]

Thank you for your comment! It was very helpful, and I now have a better understanding of the issue.