Optimization of signed division by most powers of 2 is wrong

Speaking of this code: https://github.com/google/xls/blob/main/xls/passes/arith_simplification_pass.cc#L391-L410

I believe the rewrite of signed division by any power of 2 that's greater than 1 is wrong.

For example, optimize signed divide by 2. It's rewritten to a SRA by 2, which is further rewritten to:

  bit_slice.6: bits[9] = bit_slice(x, start=1, width=9, id=6)
  ret sign_ext.7: bits[10] = sign_ext(bit_slice.6, new_bit_count=10, id=7)

I tested the optimized IR with the interpreter:

  auto interp_and_check = [&f](int x, int expected) {
    XLS_ASSERT_OK_AND_ASSIGN(InterpreterResult<Value> r,
                             InterpretFunction(f, {Value(SBits(x, N))}));
    EXPECT_EQ(r.value, Value(SBits(expected, N)));
  };
  interp_and_check(-1, 0);

I believe the correct result is 0. That is, RoundTowardZero(-1/2) = 0. The interpretation of the optimized function disagrees:

  r.value
    Which is: bits[10]:1023
  Value(SBits(expected, N))
    Which is: bits[10]:0

Clearly, -1/2 is not 1023. So arith_simplification_pass is wrong.

I recommend that you disable this optimization immediately. If you're willing to wait a few days/weeks, I will have a solution for all signed and unsigned division by a constant (not just positive powers of 2).

The input to the pass was:

  auto p = CreatePackage();
  FunctionBuilder fb(TestName(), p.get());
  fb.SDiv(fb.Param("x", p->GetBitsType(N)),
          fb.Literal(Value(SBits(2, 10))));
  XLS_ASSERT_OK_AND_ASSIGN(Function * f, fb.Build());
  ASSERT_THAT(Run(p.get()), IsOkAndHolds(true));

google / xls

Optimization of signed division by most powers of 2 is wrong #732