I’ve created tests for simplifiers using Hypothesis, available at https://github.com/alexeyr/tvm/tree/hypothesis. What I do is:
- Generate an arithmetical
tvm.Expr
(boolean operations to be added later) together with its value. - Run the simplifiers (
tvm.arith.Analyzer().canonical_simplify
,tvm.arith.Analyzer().rewrite_simplify
andtvm.ir_pass.CanonicalSimplify
) on it. - 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?