Initial results from randomly testing simplifiers

I’ve created tests for simplifiers using Hypothesis, available at https://github.com/alexeyr/tvm/tree/hypothesis. What I do is:

  1. Generate an arithmetical tvm.Expr (boolean operations to be added later) together with its value.
  2. Run the simplifiers (tvm.arith.Analyzer().canonical_simplify, tvm.arith.Analyzer().rewrite_simplify and tvm.ir_pass.CanonicalSimplify) on it.
  3. Compile and evaluate the result.

There don’t seem to be too many failures, but there are some. Examples:

AssertionError:
Not equal to tolerance rtol=1e-07, atol=1e-07

(mismatch 100.0%)
 x: array([65407], dtype=int32)
 y: array([65408], dtype=int32)
...
Exception: rewrite_simplify invalidly simplified max(65408, int32(((uint16)129*(uint16)65535))) to int32(((uint16)129*(uint16)65535))

(the first one is the evaluation result).

TVMError: Traceback (most recent call last):
  [bt] (8) /workspace/src/romanov/tvm/build-docker/libtvm.so(+0x8626d4) [0x7f31e8d066d4]
  [bt] (7) /workspace/src/romanov/tvm/build-docker/libtvm.so(+0x2286ec) [0x7f31e86cc6ec]
  [bt] (6) /workspace/src/romanov/tvm/build-docker/libtvm.so(+0x2286ec) [0x7f31e86cc6ec]
  [bt] (5) /workspace/src/romanov/tvm/build-docker/libtvm.so(+0x88d458) [0x7f31e8d31458]
  [bt] (4) /workspace/src/romanov/tvm/build-docker/libtvm.so(+0x85574c) [0x7f31e8cf974c]
  [bt] (3) /workspace/src/romanov/tvm/build-docker/libtvm.so(+0x88a059) [0x7f31e8d2e059]
  [bt] (2) /workspace/src/romanov/tvm/build-docker/libtvm.so(+0x85e040) [0x7f31e8d02040]
  [bt] (1) /workspace/src/romanov/tvm/build-docker/libtvm.so(+0x890f02) [0x7f31e8d34f02]
  [bt] (0) /workspace/src/romanov/tvm/build-docker/libtvm.so(+0x144ad2) [0x7f31e85e8ad2]
  File "/workspace/src/romanov/tvm/src/codegen/llvm/codegen_llvm.cc", line 715
TVMError: unknown intrinsic signed_integer_overflow
...
Exception: canonical_simplify invalidly simplified ((int32((int8)0) + int32((uint32)2147483648))*-1) to ((0 - int32((int8)0)) - int32((uint32)2147483648))

I also tried evaluating both sides using TVM, and this doesn’t seem to produce any failures; but that may just be because tvm.build itself runs the simplifiers. Is there a way to disable this?