Fix integer overflow when composing nested affine views

[adityaanikam]

Fixes #1244.

IViewFactory#intView flattens a nested affine view by composing the coefficients in int arithmetic:

int av = (view.p ? 1 : -1) * view.a * a;
int bv = a * view.b + b;

Either product can leave the int range even when every value the expression can take is small. In the reported case, x ranges over [46341, 46342] and the composed expression is at most 46341, but flattening (x - 46341) * 46341 computes bv as 46341 * -46341 = -2147488281, which underflows and wraps to +2147479015. The view built from that is wrong in both directions: a valid solution is pruned and the model reported unsatisfiable, and an assignment that violates the posted constraint is returned as a solution.

Changes proposed in this PR:

• Compose the coefficients in long and keep the nested view when either does not fit in an int, falling back to the new IntAffineView<>(var, a, b) construction the non-flattening branch already used. No new view type is needed and views stay enabled.
• Add two regression tests to IntAffineViewTest, one per direction reported in the issue.
• Add myself to the authors of both modified classes, as CONTRIBUTING asks.

On scope: the issue also suggests guarding the scaled bounds of the base variable, in addition to the coefficients. I left that out. It only changes behaviour when av and bv both fit but av * base does not, and in that situation this patch and the current code take the same branch, so I could not write a test that distinguishes them. I would rather not add a condition with no regression test behind it. Worth noting if you do want it covered: getLB() and getUB() compute (...) * a + b as a single int expression, so an overflowing intermediate cancels there and the bound is still correct; contains() is the one that would suffer, because it does value -= b and then divides, and the division does not undo the wrap. Happy to add it if you would like it handled.

I did not touch CHANGES.md, since there is no unreleased section to add to.

Verified with a negative control: reverting only IViewFactory.java and keeping the tests fails exactly the two new tests out of 150 in the class, with expected [true] but found [false] for the pruned solution and expected [46342] but found [46341] for the invalid one. Restoring the fix passes all 150.

@chocoteam/core-developer

[ArthurGodet]

Just a small change to do (to keep simplified imbricated if/else-if), but otherwise, changes seem fine to me. Thanks for your contribution !

[mergify]

Tick the box to add this pull request to the merge queue (same as @mergifyio queue).

• Queue this pull request